mmtheorems80 - 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-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Statement List for Metamath Proof Explorer - 7901-8000 - Page 80 of 175

Type	Label	Description
Statement
Theorem	expnbnd 7901	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 7902	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 7903	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 7904	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 7905	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 7906	Lemma for discriminant theorem.
Theorem	discrlem2 7907	Lemma for discriminant theorem.
Theorem	discrlem3 7908	Lemma for discriminant theorem.
Theorem	discrlem 7909	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 7910	The square of a natural number is a natural number.
|- N e. NN   =>   |- (N^2) e. NN
Theorem	nnlesqi 7911	A natural number is less than or equal to its square.
|- N e. NN   =>   |- N <_ (N^2)
Theorem	nnesqi 7912	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 7913	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 7914	A rather pretty lemma for nn0opthi 7916. (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 7915	Lemma for nn0opthi 7916.
Theorem	nn0opthi 7916	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 3053 that works for any set. (Contributed by Raph Levien, 10-Dec-2002. Proof shortened by Scott Fenton, 7-Sep-2010.)
|- 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 7917	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See comments for nn0opthi 7916.
|- 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 7918	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opthi 7916.
|- (((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 7919	Extend class notation to include positive square root of a positive real number.
class sqr
Definition	df-sqr 7920	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 7950 for its closure, sqrval 7921 for its value, sqrsqi 7970 and sqsqri 7971 for its relationship to squares, and sqr11i 7953 for uniqueness.
|- sqr = {<.x, y>. | ((x e. RR /\ 0 <_ x) /\ y = sup({z e. RR | (0 <_ z /\ (z x. z) <_ x)}, RR, < ))}
Theorem	sqrval 7921	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 7922	Square root of zero.
|- (sqr` 0) = 0
Theorem	sqrlem1 7923	Lemma for square root theorem.
Theorem	sqrlem2 7924	Lemma for square root theorem.
Theorem	sqrlem3 7925	Lemma for square root theorem.
Theorem	sqrlem4 7926	Lemma for square root theorem.
Theorem	sqrlem5 7927	Lemma for square root theorem.
Theorem	sqrlem6 7928	Lemma for square root theorem.
Theorem	sqrlem7 7929	Lemma for square root theorem.
Theorem	sqrlem8 7930	Lemma for square root theorem.
Theorem	sqrlem9 7931	Lemma for square root theorem.
Theorem	sqrlem10 7932	Lemma for square root theorem.
Theorem	sqrlem11 7933	Lemma for square root theorem.
Theorem	sqrlem12 7934	Lemma for square root theorem.
Theorem	sqrlem13 7935	Lemma for square root theorem.
Theorem	sqrlem14 7936	Lemma for square root theorem.
Theorem	sqrlem15 7937	Lemma for square root theorem.
Theorem	sqrlem16 7938	Lemma for square root theorem.
Theorem	sqrlem17 7939	Lemma for square root theorem.
Theorem	sqrlem18 7940	Lemma for square root theorem.
Theorem	sqrlem19 7941	Lemma for square root theorem.
Theorem	sqrlem20 7942	Lemma for square root theorem.
Theorem	sqrlem21 7943	Lemma for square root theorem.
Theorem	sqrlem22 7944	Lemma for square root theorem.
Theorem	sqrlem23 7945	Lemma for square root theorem.
Theorem	sqrlem24 7946	Lemma for square root closure.
Theorem	sqrgt0ii 7947	The square root of a positive real is positive.
|- A e. RR   &   |- 0 < A   =>   |- 0 < (sqr` A)
Theorem	sqrlem26 7948	Lemma for square root theorem.
Theorem	sqrthi 7949	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)
Theorem	sqrcli 7950	The square root of a nonnegative real is a real.
|- A e. RR   =>   |- (0 <_ A -> (sqr` A) e. RR)
Theorem	sqrgt0i 7951	The square root of a positive real is positive.
|- A e. RR   =>   |- (0 < A -> 0 < (sqr` A))
Theorem	sqrge0i 7952	The square root of a nonnegative real is nonnegative.
|- A e. RR   =>   |- (0 <_ A -> 0 <_ (sqr` A))
Theorem	sqr11i 7953	The square root function is one-to-one.
|- A e. RR   &   |- B e. RR   =>   |- ((0 <_ A /\ 0 <_ B) -> ((sqr` A) = (sqr` B) <-> A = B))
Theorem	sqrmulii 7954	Square root distributes over multiplication.
|- A e. RR   &   |- B e. RR   &   |- 0 <_ A   &   |- 0 <_ B   =>   |- (sqr` (A x. B)) = ((sqr` A) x. (sqr` B))
Theorem	sqrmuli 7955	Square root distributes over multiplication.
|- A e. RR   &   |- B e. RR   =>   |- ((0 <_ A /\ 0 <_ B) -> (sqr` (A x. B)) = ((sqr` A) x. (sqr` B)))
Theorem	sqrmsq2i 7956	Relationship between square root and squares.
|- A e. RR   &   |- B e. RR   =>   |- ((0 <_ A /\ 0 <_ B) -> ((sqr` A) = B <-> A = (B x. B)))
Theorem	sqrlei 7957	Square root is monotonic.
|- A e. RR   &   |- B e. RR   =>   |- ((0 <_ A /\ 0 <_ B) -> (A <_ B <-> (sqr` A) <_ (sqr` B)))
Theorem	sqrlti 7958	Square root is strictly monotonic. (Contributed by Roy F. Longton, 8-Aug-2005.)
|- A e. RR   &   |- B e. RR   =>   |- ((0 <_ A /\ 0 <_ B) -> (A < B <-> (sqr` A) < (sqr` B)))
Theorem	sqrmsqi 7959	Square root of square.
|- A e. RR   =>   |- (0 <_ A -> (sqr` (A x. A)) = A)
Theorem	sqrcl 7960	The square root of a nonnegative real is a real.
|- ((A e. RR /\ 0 <_ A) -> (sqr` A) e. RR)
Theorem	sqrgt0 7961	The square root of a positive real is positive.
|- ((A e. RR /\ 0 < A) -> 0 < (sqr` A))
Theorem	sqrge0 7962	The square root of a nonnegative real is nonnegative.
|- ((A e. RR /\ 0 <_ A) -> 0 <_ (sqr` A))
Theorem	sqrle 7963	Square root is monotonic.
|- (((A e. RR /\ B e. RR) /\ (0 <_ A /\ 0 <_ B)) -> (A <_ B <-> (sqr` A) <_ (sqr` B)))
Theorem	sqr00 7964	A square root is zero iff its argument is 0.
|- ((A e. RR /\ 0 <_ A) -> ((sqr` A) = 0 <-> A = 0))
Theorem	rpsqrcl 7965	The square root of a positive real is a postive real.
|- (A e. RR+ -> (sqr` A) e. RR+)
Theorem	sqr1 7966	The square root of 1 is 1.
|- (sqr` 1) = 1
Theorem	sqr4 7967	The square root of 4 is 2.
|- (sqr` 4) = 2
Theorem	sqr9 7968	The square root of 9 is 3.
|- (sqr` 9) = 3
Theorem	sqr2gt1lt2 7969	The square root of 2 is bounded by 1 and 2. (Contributed by Roy F. Longton, 8-Aug-2005.)
|- (1 < (sqr` 2) /\ (sqr` 2) < 2)
Theorem	sqrsqi 7970	Square root of square.
|- A e. RR   =>   |- (0 <_ A -> (sqr` (A^2)) = A)
Theorem	sqsqri 7971	Square of square root.
|- A e. RR   =>   |- (0 <_ A -> ((sqr` A)^2) = A)
Theorem	sqrsq 7972	Square root of square.
|- ((A e. RR /\ 0 <_ A) -> (sqr` (A^2)) = A)
Theorem	sqsqr 7973	Square of square root.
|- ((A e. RR /\ 0 <_ A) -> ((sqr` A)^2) = A)
Irrationality of square root of 2
Theorem	sqr2irrlem1 7974	Lemma for irrationality of square root of 2. Technical lemma used to simplify the main induction step.
Theorem	sqr2irrlem2 7975	Lemma for irrationality of square root of 2. Eliminates hypotheses with weak deduction theorem.
Theorem	sqr2irrlem3 7976	Main theorem for irrationality of square root of 2. There are no natural numbers such that the square of one is twice the square of the other. Uses strong induction.
|- -. E.x e. NN E.y e. NN (x^2) = (2 x. (y^2))
Theorem	sqr2irrlem4 7977	Lemma for irrationality of square root of 2.
Theorem	sqr2irrlem5 7978	Lemma for irrationality of square root of 2. Eliminates hypotheses with weak deduction theorem.
Theorem	sqr2irr 7979	The square root of 2 is irrational.
|- (sqr` 2) e/ QQ
Theorem	sqr2re 7980	The square root of 2 exists and is a real number.
|- (sqr` 2) e. RR
Imaginary and complex number properties
Theorem	irec 7981	The reciprocal of _i.
|- (1 / _i) = -u_i
Theorem	i2 7982	_i squared.
|- (_i^2) = -u1
Theorem	i3 7983	_i cubed.
|- (_i^3) = -u_i
Theorem	i4 7984	_i to the fourth power.
|- (_i^4) = 1
Theorem	inelr 7985	The imaginary unit _i is not a real number.
|- -. _i e. RR
Theorem	crulem 7986	Lemma for crui 7987.
Theorem	crui 7987	The representation of complex numbers in terms of real and imaginary parts is unique. Proposition 10-1.3 of [Gleason] p. 130.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   &   |- D e. RR   =>   |- ((A + (_i x. B)) = (C + (_i x. D)) <-> (A = C /\ B = D))
Theorem	cru 7988	The representation of complex numbers in terms of real and imaginary parts is unique. Proposition 10-1.3 of [Gleason] p. 130.
|- (((A e. RR /\ B e. RR) /\ (C e. RR /\ D e. RR)) -> ((A + (_i x. B)) = (C + (_i x. D)) <-> (A = C /\ B = D)))
Theorem	crne0i 7989	The real representation of complex numbers is nonzero iff one of its terms is nonzero.
|- A e. RR   &   |- B e. RR   =>   |- ((A =/= 0 \/ B =/= 0) <-> (A + (_i x. B)) =/= 0)
Theorem	crmuli 7990	Multiplication rule for complex number representation. Remark in [Apostol] p. 361. In normal use, the arguments are the real components of two complex numbers, but the theorem works for complex components as well.
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- D e. CC   =>   |- ((A + (_i x. B)) x. (C + (_i x. D))) = (((A x. C) - (B x. D)) + (_i x. ((A x. D) + (B x. C))))
Theorem	crreczi 7991	Reciprocal of a complex number in terms of real and imaginary components. Remark in [Apostol] p. 361.
|- A e. RR   &   |- B e. RR   =>   |- ((A =/= 0 \/ B =/= 0) -> (1 / (A + (_i x. B))) = ((A - (_i x. B)) / ((A^2) + (B^2))))
Theorem	creur 7992	The real part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130.
|- (A e. CC -> E!x e. RR E.y e. RR A = (x + (_i x. y)))
Theorem	creui 7993	The imaginary part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130.
|- (A e. CC -> E!y e. RR E.x e. RR A = (x + (_i x. y)))
Theorem	rimul 7994	A real number times the imaginary unit is real only if the number is 0.
|- ((A e. RR /\ (_i x. A) e. RR) -> A = 0)
Theorem	nthruc 7995	The sequence NN, ZZ, QQ, RR, and CC forms a chain of proper subsets. In each case the proper subset relationship is shown by demonstrating a number that belongs to one set but not the other. We show that zero belongs to ZZ but not NN, one-half belongs to QQ but not ZZ, the square root of 2 belongs to RR but not QQ, and finally that the imaginary number _i belongs to CC but not RR. See nthruz 7996 for a further refinement.
|- ((NN C. ZZ /\ ZZ C. QQ) /\ (QQ C. RR /\ RR C. CC))
Theorem	nthruz 7996	The sequence NN, NN0, and ZZ forms a chain of proper subsets. In each case the proper subset relationship is shown by demonstrating a number that belongs to one set but not the other. We show that zero belongs to NN0 but not NN and minus one belongs to ZZ but not NN0. This theorem refines the chain of proper subsets nthruc 7995.
|- (NN C. NN0 /\ NN0 C. ZZ)
Real and imaginary parts; conjugate; absolute value
Syntax	cre 7997	Extend class notation to include real part of a complex number.
class Re
Syntax	cim 7998	Extend class notation to include imaginary part of a complex number.
class Im
Syntax	ccj 7999	Extend class notation to include complex conjugate function.
class *
Syntax	cabs 8000	Extend class notation to include a function for the absolute value (modulus) of a complex number.
class abs