mmtheorems67 - Metamath Proof Explorer

Jump to page: Contents + 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-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10722

Statement List for Metamath Proof Explorer - 6601-6700 - Page 67 of 108

Type	Label	Description
Statement
Theorem	expubndt 6601	An upper bound on A^N when 2 <_ A.
|- ((A e. RR /\ N e. NN0 /\ 2 <_ A) -> (A^N) <_ ((2^N) x. ((A - 1)^N)))
Theorem	sqvalt 6602	Value of the square of a complex number. (Contributed by Raph Levien, 10-Apr-2004.)
|- (A e. CC -> (A^2) = (A x. A))
Theorem	sqnegt 6603	The square of the negative of a number.)
|- (A e. CC -> (-uA^2) = (A^2))
Theorem	sqclt 6604	Closure of square.
|- (A e. CC -> (A^2) e. CC)
Theorem	sqmult 6605	Distribution of square over multiplication.
|- ((A e. CC /\ B e. CC) -> ((A x. B)^2) = ((A^2) x. (B^2)))
Theorem	sqeq0t 6606	A number is zero iff its square is zero.
|- (A e. CC -> ((A^2) = 0 <-> A = 0))
Theorem	sqval 6607	Value of square. Inference version.
|- A e. CC   =>   |- (A^2) = (A x. A)
Theorem	sqcl 6608	Closure of square.
|- A e. CC   =>   |- (A^2) e. CC
Theorem	sqeq0 6609	A number is zero iff its square is zero.
|- A e. CC   =>   |- ((A^2) = 0 <-> A = 0)
Theorem	sqmul 6610	Distribution of square over multiplication.
|- A e. CC   &   |- B e. CC   =>   |- ((A x. B)^2) = ((A^2) x. (B^2))
Theorem	sqdiv 6611	Distribution of square over division.
|- A e. CC   &   |- B e. CC   &   |- B =/= 0   =>   |- ((A / B)^2) = ((A^2) / (B^2))
Theorem	sqreci 6612	Square of reciprocal.
|- A e. CC   &   |- A =/= 0   =>   |- ((1 / A)^2) = (1 / (A^2))
Theorem	sqne0t 6613	A number is nonzero iff its square is nonzero.
|- (A e. CC -> ((A^2) =/= 0 <-> A =/= 0))
Theorem	resqclt 6614	Closure of the square of a real number.
|- (A e. RR -> (A^2) e. RR)
Theorem	sqgt0t 6615	The square of a non-zero real is positive.
|- ((A e. RR /\ A =/= 0) -> 0 < (A^2))
Theorem	resqcl 6616	Closure of square in reals.
|- A e. RR   =>   |- (A^2) e. RR
Theorem	lt2sq 6617	The square function on nonnegative reals is strictly monotonic.
|- A e. RR   &   |- B e. RR   =>   |- ((0 <_ A /\ 0 <_ B) -> (A < B <-> (A^2) < (B^2)))
Theorem	le2sq 6618	The square function on nonnegative reals is monotonic.
|- A e. RR   &   |- B e. RR   =>   |- ((0 <_ A /\ 0 <_ B) -> (A <_ B <-> (A^2) <_ (B^2)))
Theorem	sq11 6619	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	sqgt0 6620	The square of a non-zero real is positive.
|- A e. RR   =>   |- (A =/= 0 -> 0 < (A^2))
Theorem	sqge0 6621	A square of a real is nonnegative.
|- A e. RR   =>   |- 0 <_ (A^2)
Theorem	sq11t 6622	The square function is one-to-one for nonnegative reals.
|- (((A e. RR /\ 0 <_ A) /\ (B e. RR /\ 0 <_ B)) -> ((A^2) = (B^2) <-> A = B))
Theorem	lt2sqt 6623	The square function on nonnegative reals is strictly monotonic.
|- (((A e. RR /\ 0 <_ A) /\ (B e. RR /\ 0 <_ B)) -> (A < B <-> (A^2) < (B^2)))
Theorem	le2sqt 6624	The square function on nonnegative reals is monotonic.
|- (((A e. RR /\ 0 <_ A) /\ (B e. RR /\ 0 <_ B)) -> (A <_ B <-> (A^2) <_ (B^2)))
Theorem	le2sqit 6625	The square of a 'less than or equal to' ordering.
|- (((A e. RR /\ 0 <_ A) /\ (B e. RR /\ A <_ B)) -> (A^2) <_ (B^2))
Theorem	sqge0t 6626	A square of a real is nonnegative.
|- (A e. RR -> 0 <_ (A^2))
Theorem	sumsqne0 6627	The sum of two squares is nonzero iff one of its terms is nonzero.
|- A e. RR   &   |- B e. RR   =>   |- ((A =/= 0 \/ B =/= 0) <-> ((A^2) + (B^2)) =/= 0)
Theorem	sq0 6628	The square of 0 is 0.
|- (0^2) = 0
Theorem	sq0i 6629	If a number is zero, its square is zero. (Contributed by FL, 10-Dec-2006.)
|- (A = 0 -> (A^2) = 0)
Theorem	sq1 6630	The square of 1 is 1.
|- (1^2) = 1
Theorem	sq2 6631	The square of 2 is 4.
|- (2^2) = 4
Theorem	sq3 6632	The square of 3 is 9.
|- (3^2) = 9
Theorem	cu2 6633	The cube of 2 is 8.
|- (2^3) = 8
Theorem	sqlecant 6634	Cancel one factor of a square in a <_ comparison. Unlike lemul1t 5825, the common factor A may be zero.
|- (((A e. RR /\ 0 <_ A) /\ (B e. RR /\ 0 <_ B)) -> ((A^2) <_ (B x. A) <-> A <_ B))
Theorem	subsqt 6635	Factor the difference of two squares.
|- ((A e. CC /\ B e. CC) -> ((A^2) - (B^2)) = ((A + B) x. (A - B)))
Theorem	subsq2t 6636	Express the difference of the squares of two numbers as a polynomial in the difference of the numbers.
|- ((A e. CC /\ B e. CC) -> ((A^2) - (B^2)) = (((A - B)^2) + ((2 x. B) x. (A - B))))
Theorem	binom2 6637	The square of a binomial.
|- A e. CC   &   |- B e. CC   =>   |- ((A + B)^2) = (((A^2) + (2 x. (A x. B))) + (B^2))
Theorem	binom2aOLD 6638	Product of sum and difference.
|- A e. CC   &   |- B e. CC   =>   |- ((A + B) x. (A - B)) = ((A^2) - (B^2))
Theorem	subsq 6639	Factor the difference of two squares.
|- A e. CC   &   |- B e. CC   =>   |- ((A^2) - (B^2)) = ((A + B) x. (A - B))
Theorem	sqeqor 6640	The squares of two complex numbers are equal iff one number equals the other or its negative. Lemma 15-4.7 of [Gleason] p. 311 and its converse.
|- A e. CC   &   |- B e. CC   =>   |- ((A^2) = (B^2) <-> (A = B \/ A = -uB))
Theorem	subsq0 6641	The two solutions to the difference of squares set equal to zero.
|- A e. CC   &   |- B e. CC   =>   |- (((A^2) - (B^2)) = 0 <-> (A = B \/ A = -uB))
Theorem	sqeqort 6642	The squares of two complex numbers are equal iff one number equals the other or its negative. Lemma 15-4.7 of [Gleason] p. 311 and its converse. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ((A e. CC /\ B e. CC) -> ((A^2) = (B^2) <-> (A = B \/ A = -uB)))
Theorem	binom2t 6643	The square of a binomial. (Contributed by FL, 10-Dec-2006.)
|- ((A e. CC /\ B e. CC) -> ((A + B)^2) = (((A^2) + (2 x. (A x. B))) + (B^2)))
Theorem	sq01t 6644	If a complex number equals its square, it must be 0 or 1.
|- (A e. CC -> ((A^2) = A <-> (A = 0 \/ A = 1)))
Theorem	bernneq 6645	Bernoulli's inequality, due to Johan Bernoulli (1667-1748).
|- ((A e. RR /\ N e. NN0 /\ -u1 <_ A) -> (1 + (A x. N)) <_ ((1 + A)^N))
Theorem	bernneq2 6646	Variation of Bernoulli's inequality bernneq 6645.
|- ((A e. RR /\ N e. NN0 /\ 0 <_ A) -> (((A - 1) x. N) + 1) <_ (A^N))
Theorem	expnbndt 6647	Exponentiation with a mantissa greater than 1 has no upper bound.
|- ((A e. RR /\ B e. RR /\ 1 < B) -> E.k e. NN A < (B^k))
Theorem	expnlbndt 6648	The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound.
|- ((A e. RR+ /\ B e. RR /\ 1 < B) -> E.k e. NN (1 / (B^k)) < A)
Discriminant
Theorem	discrlem1 6649	Lemma for discriminant theorem.
Theorem	discrlem2 6650	Lemma for discriminant theorem.
Theorem	discrlem3 6651	Lemma for discriminant theorem.
Theorem	discrlem 6652	If a quadratic polynomial with real coefficients is nonnegative for all values, then its discriminant is non-positive. The antecedent 0 <_ A is redundant but simplifies the proof.
|- 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)
More natural number properties
Theorem	nnsqcl 6653	The square of a natural number is a natural number.
|- N e. NN   =>   |- (N^2) e. NN
Theorem	nnlesq 6654	A natural number is less than or equal to its square.
|- N e. NN   =>   |- N <_ (N^2)
Theorem	nnesq 6655	A natural number is even iff its square is even.
|- N e. NN   =>   |- ((N / 2) e. NN <-> ((N^2) / 2) e. NN)
Ordered pair theorem for nonnegative integers
Theorem	nn0le2msqt 6656	The square function on nonnegative integers is monotonic. (Contributed by Raph Levien, 10-Dec-2002.)
|- A e. NN0   &   |- B e. NN0   =>   |- (A <_ B <-> (A x. A) <_ (B x. B))
Theorem	nn0opthlem1 6657	A rather pretty lemma for nn0opth 6659. (Contributed by Raph Levien, 10-Dec-2002.)
|- A e. NN0   &   |- C e. NN0   =>   |- (A < C <-> ((A x. A) + (2 x. A)) < (C x. C))
Theorem	nn0opthlem2 6658	Lemma for nn0opth 6659.
Theorem	nn0opth 6659	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)