mmtheorems69 - 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-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 6801-6900 - Page 69 of 123

Type	Label	Description
Statement
Theorem	expord2 6801	The power of a positive number smaller than 1 decreases as its exponent increases.
|- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (0 < A /\ A < 1)) -> (M < N <-> (A^N) < (A^M)))
Theorem	expword2i 6802	Weak ordering relationship for exponentiation. (Contributed by Paul Chapman, 14-Jan-2008.)
|- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (0 < A /\ A <_ 1 /\ M < N)) -> (A^N) <_ (A^M))
Theorem	expmwordi 6803	Weak mantissa ordering relationship for exponentiation.
|- (((A e. RR /\ B e. RR /\ N e. NN0) /\ (0 <_ A /\ A <_ B)) -> (A^N) <_ (B^N))
Theorem	exple1 6804	Nonnegative integer exponentiation with a mantissa between 0 and 1 inclusive is less than or equal to 1. (Contributed by Paul Chapman, 29-Dec-2007.)
|- (((A e. RR /\ 0 <_ A /\ A <_ 1) /\ N e. NN0) -> (A^N) <_ 1)
Theorem	expubnd 6805	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	sqval 6806	Value of the square of a complex number. (Contributed by Raph Levien, 10-Apr-2004.)
|- (A e. CC -> (A^2) = (A x. A))
Theorem	sqneg 6807	The square of the negative of a number.)
|- (A e. CC -> (-uA^2) = (A^2))
Theorem	sqcl 6808	Closure of square.
|- (A e. CC -> (A^2) e. CC)
Theorem	sqmul 6809	Distribution of square over multiplication.
|- ((A e. CC /\ B e. CC) -> ((A x. B)^2) = ((A^2) x. (B^2)))
Theorem	sqeq0 6810	A number is zero iff its square is zero.
|- (A e. CC -> ((A^2) = 0 <-> A = 0))
Theorem	sqvali 6811	Value of square. Inference version.
|- A e. CC   =>   |- (A^2) = (A x. A)
Theorem	sqcli 6812	Closure of square.
|- A e. CC   =>   |- (A^2) e. CC
Theorem	sqeq0i 6813	A number is zero iff its square is zero.
|- A e. CC   =>   |- ((A^2) = 0 <-> A = 0)
Theorem	sqmuli 6814	Distribution of square over multiplication.
|- A e. CC   &   |- B e. CC   =>   |- ((A x. B)^2) = ((A^2) x. (B^2))
Theorem	sqdivi 6815	Distribution of square over division.
|- A e. CC   &   |- B e. CC   &   |- B =/= 0   =>   |- ((A / B)^2) = ((A^2) / (B^2))
Theorem	sqrecii 6816	Square of reciprocal.
|- A e. CC   &   |- A =/= 0   =>   |- ((1 / A)^2) = (1 / (A^2))
Theorem	sqne0 6817	A number is nonzero iff its square is nonzero.
|- (A e. CC -> ((A^2) =/= 0 <-> A =/= 0))
Theorem	resqcl 6818	Closure of the square of a real number.
|- (A e. RR -> (A^2) e. RR)
Theorem	sqgt0 6819	The square of a non-zero real is positive.
|- ((A e. RR /\ A =/= 0) -> 0 < (A^2))
Theorem	resqcli 6820	Closure of square in reals.
|- A e. RR   =>   |- (A^2) e. RR
Theorem	lt2sqi 6821	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	le2sqi 6822	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	sq11i 6823	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	sqgt0i 6824	The square of a non-zero real is positive.
|- A e. RR   =>   |- (A =/= 0 -> 0 < (A^2))
Theorem	sqge0i 6825	A square of a real is nonnegative.
|- A e. RR   =>   |- 0 <_ (A^2)
Theorem	sq11 6826	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	lt2sq 6827	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	le2sq 6828	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	le2sq2 6829	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	sqge0 6830	A square of a real is nonnegative.
|- (A e. RR -> 0 <_ (A^2))
Theorem	sumsqne0i 6831	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 6832	The square of 0 is 0.
|- (0^2) = 0
Theorem	sq0i 6833	If a number is zero, its square is zero. (Contributed by FL, 10-Dec-2006.)
|- (A = 0 -> (A^2) = 0)
Theorem	sq1 6834	The square of 1 is 1.
|- (1^2) = 1
Theorem	sq2 6835	The square of 2 is 4.
|- (2^2) = 4
Theorem	sq3 6836	The square of 3 is 9.
|- (3^2) = 9
Theorem	cu2 6837	The cube of 2 is 8.
|- (2^3) = 8
Theorem	sqlecan 6838	Cancel one factor of a square in a <_ comparison. Unlike lemul1 5973, 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	subsq 6839	Factor the difference of two squares.
|- ((A e. CC /\ B e. CC) -> ((A^2) - (B^2)) = ((A + B) x. (A - B)))
Theorem	subsq2 6840	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	binom2i 6841	The square of a binomial.
|- A e. CC   &   |- B e. CC   =>   |- ((A + B)^2) = (((A^2) + (2 x. (A x. B))) + (B^2))
Theorem	binom2aiOLD 6842	Product of sum and difference.
|- A e. CC   &   |- B e. CC   =>   |- ((A + B) x. (A - B)) = ((A^2) - (B^2))
Theorem	subsqi 6843	Factor the difference of two squares.
|- A e. CC   &   |- B e. CC   =>   |- ((A^2) - (B^2)) = ((A + B) x. (A - B))
Theorem	sqeqori 6844	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	subsq0i 6845	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	sqeqor 6846	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	binom2 6847	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	sq01 6848	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 6849	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	bernneqOLD 6850	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 6851	Variation of Bernoulli's inequality bernneq 6849.
|- ((A e. RR /\ N e. NN0 /\ 0 <_ A) -> (((A - 1) x. N) + 1) <_ (A^N))
Theorem	expnbnd 6852	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	expnlbnd 6853	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)
Theorem	expnlbnd2 6854	The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound.
|- ((A e. RR+ /\ B e. RR /\ 1 < B) -> E.j e. NN A.k e. NN (j <_ k -> (1 / (B^k)) < A))
Theorem	digit2 6855	Two ways to express the K th digit in the decimal (when base B = 10) expansion of a number A. K = 1 corresponds to the first digit after the decimal point.
|- ((A e. RR /\ B e. NN /\ K e. NN) -> ((|_` ((B^K) x. A)) mod B) = ((|_` ((B^K) x. A)) - (B x. (|_` ((B^(K - 1)) x. A)))))
Theorem	digit1 6856	Two ways to express the K th digit in the decimal expansion of a number A (when base B = 10). K = 1 corresponds to the first digit after the decimal point.
|- ((A e. RR /\ B e. NN /\ K e. NN) -> ((|_` ((B^K) x. A)) mod B) = (((|_` ((B^K) x. A)) mod (B^K)) - ((B x. (|_` ((B^(K - 1)) x. A))) mod (B^K))))
Discriminant
Theorem	discrlem1 6857	Lemma for discriminant theorem.
Theorem	discrlem2 6858	Lemma for discriminant theorem.
Theorem	discrlem3 6859	Lemma for discriminant theorem.
Theorem	discrlem 6860	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	nnsqcli 6861	The square of a natural number is a natural number.
|- N e. NN   =>   |- (N^2) e. NN
Theorem	nnlesqi 6862	A natural number is less than or equal to its square.
|- N e. NN   =>   |- N <_ (N^2)
Theorem	nnesqi 6863	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	nn0le2msqi 6864	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 6865	A rather pretty lemma for nn0opthi 6867. (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 6866	Lemma for nn0opthi 6867.
Theorem	nn0opthi 6867	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 2474 that works for any set. (Contributed by Raph Levien, 10-Dec-2002.)
|- 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	nn0opth2i 6868	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opthi 6867.
|- 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	nn0opth2 6869	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opthi 6867.
|- (((A e. NN0 /\ B e. NN0) /\ (C e. NN0 /\ D e. NN0)) -> ((((A + B)^2) + B) = (((C + D)^2) + D) <-> (A = C /\ B = D)))
Square root
Syntax	csqr 6870	Extend class notation to include positive square root of a positive real number.
class sqr
Definition	df-sqr 6871	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 sqrcli 6901 for its closure, sqrval 6872 for its value, sqrsqi 6921 and sqsqri 6922 for its relationship to squares, and sqr11i 6904 for uniqueness.
|- sqr = {<.x, y>. | ((x e. RR /\ 0 <_ x) /\ y = sup({z e. RR | (0 <_ z /\ (z x. z) <_ x)}, RR, < ))}
Theorem	sqrval 6872	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 6873	Square root of zero.
|- (sqr` 0) = 0
Theorem	sqrlem1 6874	Lemma for square root theorem.
Theorem	sqrlem2 6875	Lemma for square root theorem.
Theorem	sqrlem3 6876	Lemma for square root theorem.
Theorem	sqrlem4 6877	Lemma for square root theorem.
Theorem	sqrlem5 6878	Lemma for square root theorem.
Theorem	sqrlem6 6879	Lemma for square root theorem.
Theorem	sqrlem7 6880	Lemma for square root theorem.
Theorem	sqrlem8 6881	Lemma for square root theorem.
Theorem	sqrlem9 6882	Lemma for square root theorem.
Theorem	sqrlem10 6883	Lemma for square root theorem.
Theorem	sqrlem11 6884	Lemma for square root theorem.
Theorem	sqrlem12 6885	Lemma for square root theorem.
Theorem	sqrlem13 6886	Lemma for square root theorem.
Theorem	sqrlem14 6887	Lemma for square root theorem.
Theorem	sqrlem15 6888	Lemma for square root theorem.
Theorem	sqrlem16 6889	Lemma for square root theorem.
Theorem	sqrlem17 6890	Lemma for square root theorem.
Theorem	sqrlem18 6891	Lemma for square root theorem.
Theorem	sqrlem19 6892	Lemma for square root theorem.
Theorem	sqrlem20 6893	Lemma for square root theorem.
Theorem	sqrlem21 6894	Lemma for square root theorem.
Theorem	sqrlem22 6895	Lemma for square root theorem.
Theorem	sqrlem23 6896	Lemma for square root theorem.
Theorem	sqrlem24 6897	Lemma for square root closure.
Theorem	sqrgt0ii 6898	The square root of a positive real is positive.
|- A e. RR   &   |- 0 < A   =>   |- 0 < (sqr` A)
Theorem	sqrlem26 6899	Lemma for square root theorem.
Theorem	sqrthi 6900	Square root theorem. Theorem I.35 of [Apostol] p. 29. (A bit of trivia: This theorem was added to the database before the number 2 was defined and before exponents were defined. Thus you will see (1 + 1) and (x x. x) throughout its lemmas.)
|- A e. RR   =>   |- (0 <_ A -> ((sqr` A) x. (sqr` A)) = A)