Metamath Proof Explorer - mmtheorems48

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 4701-4800 - Page 48 of 58

Type	Label	Description
Statement
Theorem	le2sqe 4701	Two nonnegative reals compare the same as their squares.
|- A e. RR   &   |- B e. RR   =>   |- ((0 <_ A /\ 0 <_ B) -> (A <_ B <-> (A^2) <_ (B^2)))
Theorem	sqe11 4702	The square function is one-to-one for nonnegative reals.
|- A e. RR   &   |- B e. RR   =>   |- ((0 <_ A /\ 0 <_ B) -> ((A^2) = (B^2) <-> A = B))
Theorem	sqegt0 4703	The square of a non-zero real is positive.
|- A e. RR   =>   |- (A =/= 0 -> 0 < (A^2))
Theorem	sqege0 4704	A square of a real is nonnegative.
|- A e. RR   =>   |- 0 <_ (A^2)
Theorem	sqe11t 4705	The square function is one-to-one for nonnegative reals.
|- ((A e. RR /\ B e. RR) -> ((0 <_ A /\ 0 <_ B) -> ((A^2) = (B^2) <-> A = B)))
Theorem	lt2sqet 4706	Two nonnegative numbers compare the same as their squares.
|- ((A e. RR /\ B e. RR) -> ((0 <_ A /\ 0 <_ B) -> (A < B <-> (A^2) < (B^2))))
Theorem	le2sqet 4707	Two nonnegative numbers compare the same as their squares.
|- ((A e. RR /\ B e. RR) -> ((0 <_ A /\ 0 <_ B) -> (A <_ B <-> (A^2) <_ (B^2))))
Theorem	sqege0t 4708	A square of a real is nonnegative.
|- (A e. RR -> 0 <_ (A^2))
Theorem	sq1 4709	The square of 1 is 1.
|- (1^2) = 1
Theorem	sq2 4710	The square of 2 is 4.
|- (2^2) = 4
Theorem	cu2 4711	The cube of 2 is 8.
|- (2^3) = 8
Theorem	binom 4712	Binomial expansion.
|- A e. CC   &   |- B e. CC   =>   |- ((A + B)^2) = (((A^2) + (2 x. (A x. B))) + (B^2))
Theorem	discrlem1 4713	Lemma for discriminant theorem.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   &   |- D = -u(B / (2 x. A))   &   |- 0 < A   =>   |- (0 <_ (((A x. (D^2)) + (B x. D)) + C) <-> ((B^2) - (4 x. (A x. C))) <_ 0)
Theorem	discrlem2 4714	Lemma for discriminant theorem.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   &   |- D = -u(B / (2 x. A))   &   |- (D e. RR -> 0 <_ (((A x. (D^2)) + (B x. D)) + C))   =>   |- (0 < A -> ((B^2) - (4 x. (A x. C))) <_ 0)
Theorem	discrlem3 4715	Lemma for discriminant theorem.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   &   |- D = ((C + 1) / -uB)   &   |- (D e. RR -> 0 <_ (((A x. (D^2)) + (B x. D)) + C))   =>   |- (0 = A -> ((B^2) - (4 x. (A x. C))) <_ 0)
Theorem	discrlem 4716	If a quadratic polynomial (with a nonnegative high-order coefficient) is nonnegative for all values, then its discriminant is non-positive.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   &   |- A.x e. RR 0 <_ (((A x. (x^2)) + (B x. x)) + C)   =>   |- (0 <_ A -> ((B^2) - (4 x. (A x. C))) <_ 0)
Theorem	nnsqcl 4717	The square of a natural number is a natural number.
|- A e. NN   =>   |- (A^2) e. NN
Theorem	nnlesq 4718	A natural number is less than or equal to its square.
|- A e. NN   =>   |- A <_ (A^2)
Theorem	nneo 4719	A natural number is even or odd but not both.
|- A e. NN   =>   |- ((A / 2) e. NN <-> -. ((A + 1) / 2) e. NN)
Theorem	nnesq 4720	A natural number is even iff its square is even.
|- A e. NN   =>   |- ((A / 2) e. NN <-> ((A^2) / 2) e. NN)
Theorem	nn0le2sqet 4721	Two nonnegative integers compare the same as their squares. (Contributed by Raph Levien, 10-Dec-02.)
|- A e. NN0   &   |- B e. NN0   =>   |- (A <_ B <-> (A x. A) <_ (B x. B))
Theorem	nn0opthlem1 4722	A rather pretty lemma for nn0opth 4724. (Contributed by Raph Levien, 10-Dec-02.)
|- A e. NN0   &   |- C e. NN0   =>   |- (A < C <-> ((A x. A) + (2 x. A)) < (C x. C))
Theorem	nn0opthlem2 4723	Lemma for nn0opth 4724. (Contributed by Raph Levien, 10-Dec-02.)
|- A e. NN0   &   |- B e. NN0   &   |- C e. NN0   &   |- D e. NN0   =>   |- ((B <_ A /\ D <_ C) -> (A < C -> -. ((A x. A) + B) = ((C x. C) + D)))
Theorem	nn0opth 4724	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. We can represent an ordered pair of nonnegative integers A and B by (((A + B) x. (A + B)) + B). If two such ordered pairs are equal, their first elements are equal and their second elements are equal. Contrast this ordered pair representation with the standard one df-op 1815 that works for any set. (Contributed by Raph Levien, 10-Dec-02.)
|- A e. NN0   &   |- B e. NN0   &   |- C e. NN0   &   |- D e. NN0   =>   |- ((((A + B) x. (A + B)) + B) = (((C + D) x. (C + D)) + D) <-> (A = C /\ B = D))
Theorem	nn0opth2 4725	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opth 4724.
|- A e. NN0   &   |- B e. NN0   &   |- C e. NN0   &   |- D e. NN0   =>   |- ((((A + B)^2) + B) = (((C + D)^2) + D) <-> (A = C /\ B = D))
Theorem	nn0opth2t 4726	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opth 4724.
|- (((A e. NN0 /\ B e. NN0) /\ (C e. NN0 /\ D e. NN0)) -> ((((A + B)^2) + B) = (((C + D)^2) + D) <-> (A = C /\ B = D)))
Syntax	csqr 4727	Extend class notation to include positive square root of a positive real number.
class sqr
Definition	df-sqr 4728	Define a function whose value is the square root of a nonnegative real number. The square root of x is the supremum of all reals whose square is less than x. See sqrcl 4758 for its closure, sqrval 4729 for its value, sqrsqe 4774 and sqsqr 4775 for its relationship to squares, and sqr11 4761 for uniqueness.
|- sqr = {<.x, y>. | ((x e. RR /\ 0 <_ x) /\ y = sup({z e. RR | (0 <_ z /\ (z x. z) <_ x)}, RR, < ))}
Theorem	sqrval 4729	Value of square root function.
|- ((A e. RR /\ 0 <_ A) -> (sqr` A) = sup({x e. RR | (0 <_ x /\ (x x. x) <_ A)}, RR, < ))
Theorem	sqr0 4730	Square root of zero.
|- (sqr` 0) = 0
Theorem	sqrlem1 4731	Lemma for square root theorem.
|- A e. RR   &   |- 0 < A   =>   |- A < ((1 + A) x. (1 + A))
Theorem	sqrlem2 4732	Lemma for square root theorem.
|- A e. RR   &   |- 0 < A   =>   |- ((A / (1 + A)) x. (A / (1 + A))) < A
Theorem	sqrlem3 4733	Lemma for square root theorem.
|- A e. RR   &   |- 0 < A   =>   |- 0 < (A / (1 + A))
Theorem	sqrlem4 4734	Lemma for square root theorem.
|- A e. RR   &   |- 0 < A   &   |- S = {x e. RR | (0 <_ x /\ (x x. x) <_ A)}   =>   |- (D e. S <-> (D e. RR /\ (0 <_ D /\ (D x. D) <_ A)))
Theorem	sqrlem5 4735	Lemma for square root theorem.
|- A e. RR   &   |- 0 < A   &   |- S = {x e. RR | (0 <_ x /\ (x x. x) <_ A)}   =>   |- ((D e. RR /\ (0 < D /\ (D x. D) < A)) -> D e. S)
Theorem	sqrlem6 4736	Lemma for square root theorem.
|- A e. RR   &   |- 0 < A   &   |- S = {x e. RR | (0 <_ x /\ (x x. x) <_ A)}   =>   |- (S (_ RR /\ S =/= (/) /\ E.x e. RR A.y e. S y < x)
Theorem	sqrlem7 4737	Lemma for square root theorem.
|- A e. RR   &   |- 0 < A   &   |- S = {x e. RR | (0 <_ x /\ (x x. x) <_ A)}   &   |- B = sup(S, RR, < )   =>   |- B e. RR
Theorem	sqrlem8 4738	Lemma for square root theorem.
|- A e. RR   &   |- 0 < A   &   |- S = {x e. RR | (0 <_ x /\ (x x. x) <_ A)}   &   |- B = sup(S, RR, < )   =>   |- 0 < B
Theorem	sqrlem9 4739	Lemma for square root theorem.
|- A e. RR   &   |- 0 < A   &   |- B e. RR   &   |- C e. RR   &   |- 0 < B   &   |- A < (B x. B)   &   |- C = ((B + (A / B)) / (1 + 1))   =>   |- 0 < C
Theorem	sqrlem10 4740	Lemma for square root theorem.
|- A e. RR   &   |- 0 < A   &   |- B e. RR   &   |- C e. RR   &   |- 0 < B   &   |- A < (B x. B)   &   |- C = ((B + (A / B)) / (1 + 1))   =>   |- C < B
Theorem	sqrlem11 4741	Lemma for square root theorem.
|- A e. RR   &   |- 0 < A   &   |- B e. RR   &   |- C e. RR   &   |- 0 < B   &   |- A < (B x. B)   &   |- C = ((B + (A / B)) / (1 + 1))   =>   |- A < (C x. C)
Theorem	sqrlem12 4742	Lemma for square root theorem.
|- A e. RR   &   |- 0 < A   &   |- B e. RR   &   |- C e. RR   &   |- 0 < B   &   |- A < (B x. B)   &   |- C = ((B + (A /