![]() |
Metamath
Proof Explorer Theorem List (p. 142 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sqge0 14101 | The square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.) |
โข (๐ด โ โ โ 0 โค (๐ดโ2)) | ||
Theorem | sqge0d 14102 | The square of a real is nonnegative, deduction form. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ 0 โค (๐ดโ2)) | ||
Theorem | zsqcl2 14103 | The square of an integer is a nonnegative integer. (Contributed by Mario Carneiro, 18-Apr-2014.) (Revised by Mario Carneiro, 14-Jul-2014.) |
โข (๐ด โ โค โ (๐ดโ2) โ โ0) | ||
Theorem | 0expd 14104 | Value of zero raised to a positive integer power. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ โ โ) โ โข (๐ โ (0โ๐) = 0) | ||
Theorem | exp0d 14105 | Value of a complex number raised to the zeroth power. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ดโ0) = 1) | ||
Theorem | exp1d 14106 | Value of a complex number raised to the first power. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ดโ1) = ๐ด) | ||
Theorem | expeq0d 14107 | If a positive integer power is zero, then its base is zero. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ) & โข (๐ โ (๐ดโ๐) = 0) โ โข (๐ โ ๐ด = 0) | ||
Theorem | sqvald 14108 | Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ดโ2) = (๐ด ยท ๐ด)) | ||
Theorem | sqcld 14109 | Closure of square. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ดโ2) โ โ) | ||
Theorem | sqeq0d 14110 | A number is zero iff its square is zero. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ (๐ดโ2) = 0) โ โข (๐ โ ๐ด = 0) | ||
Theorem | expcld 14111 | Closure law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (๐ดโ๐) โ โ) | ||
Theorem | expp1d 14112 | Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) | ||
Theorem | expaddd 14113 | Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))) | ||
Theorem | expmuld 14114 | Product of exponents law for positive integer exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐)) | ||
Theorem | sqrecd 14115 | Square of reciprocal is reciprocal of square. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ ((1 / ๐ด)โ2) = (1 / (๐ดโ2))) | ||
Theorem | expclzd 14116 | Closure law for integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) & โข (๐ โ ๐ โ โค) โ โข (๐ โ (๐ดโ๐) โ โ) | ||
Theorem | expne0d 14117 | A nonnegative integer power is nonzero if its base is nonzero. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) & โข (๐ โ ๐ โ โค) โ โข (๐ โ (๐ดโ๐) โ 0) | ||
Theorem | expnegd 14118 | Value of a nonzero complex number raised to the negative of an integer power. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) & โข (๐ โ ๐ โ โค) โ โข (๐ โ (๐ดโ-๐) = (1 / (๐ดโ๐))) | ||
Theorem | exprecd 14119 | An integer power of a reciprocal is the reciprocal of the integer power with same exponent. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) & โข (๐ โ ๐ โ โค) โ โข (๐ โ ((1 / ๐ด)โ๐) = (1 / (๐ดโ๐))) | ||
Theorem | expp1zd 14120 | Value of a nonzero complex number raised to an integer power plus one. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) & โข (๐ โ ๐ โ โค) โ โข (๐ โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) | ||
Theorem | expm1d 14121 | Value of a nonzero complex number raised to an integer power minus one. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) & โข (๐ โ ๐ โ โค) โ โข (๐ โ (๐ดโ(๐ โ 1)) = ((๐ดโ๐) / ๐ด)) | ||
Theorem | expsubd 14122 | Exponent subtraction law for integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) โ โข (๐ โ (๐ดโ(๐ โ ๐)) = ((๐ดโ๐) / (๐ดโ๐))) | ||
Theorem | sqmuld 14123 | Distribution of squaring over multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ ((๐ด ยท ๐ต)โ2) = ((๐ดโ2) ยท (๐ตโ2))) | ||
Theorem | sqdivd 14124 | Distribution of squaring over division. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ 0) โ โข (๐ โ ((๐ด / ๐ต)โ2) = ((๐ดโ2) / (๐ตโ2))) | ||
Theorem | expdivd 14125 | Nonnegative integer exponentiation of a quotient. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ 0) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ ((๐ด / ๐ต)โ๐) = ((๐ดโ๐) / (๐ตโ๐))) | ||
Theorem | mulexpd 14126 | Nonnegative integer exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ ((๐ด ยท ๐ต)โ๐) = ((๐ดโ๐) ยท (๐ตโ๐))) | ||
Theorem | znsqcld 14127 | The square of a nonzero integer is a positive integer. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ 0) โ โข (๐ โ (๐โ2) โ โ) | ||
Theorem | reexpcld 14128 | Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (๐ดโ๐) โ โ) | ||
Theorem | expge0d 14129 | A nonnegative real raised to a nonnegative integer is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) & โข (๐ โ 0 โค ๐ด) โ โข (๐ โ 0 โค (๐ดโ๐)) | ||
Theorem | expge1d 14130 | A real greater than or equal to 1 raised to a nonnegative integer is greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) & โข (๐ โ 1 โค ๐ด) โ โข (๐ โ 1 โค (๐ดโ๐)) | ||
Theorem | ltexp2a 14131 | Exponent ordering relationship for exponentiation of a fixed real base greater than 1 to integer exponents. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
โข (((๐ด โ โ โง ๐ โ โค โง ๐ โ โค) โง (1 < ๐ด โง ๐ < ๐)) โ (๐ดโ๐) < (๐ดโ๐)) | ||
Theorem | expmordi 14132 | Base ordering relationship for exponentiation of nonnegative reals to a fixed positive integer power. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด < ๐ต) โง ๐ โ โ) โ (๐ดโ๐) < (๐ตโ๐)) | ||
Theorem | rpexpmord 14133 | Base ordering relationship for exponentiation of positive reals to a fixed positive integer exponent. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
โข ((๐ โ โ โง ๐ด โ โ+ โง ๐ต โ โ+) โ (๐ด < ๐ต โ (๐ดโ๐) < (๐ตโ๐))) | ||
Theorem | expcan 14134 | Cancellation law for integer exponentiation of reals. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
โข (((๐ด โ โ โง ๐ โ โค โง ๐ โ โค) โง 1 < ๐ด) โ ((๐ดโ๐) = (๐ดโ๐) โ ๐ = ๐)) | ||
Theorem | ltexp2 14135 | Strict ordering law for exponentiation of a fixed real base greater than 1 to integer exponents. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 5-Jun-2014.) |
โข (((๐ด โ โ โง ๐ โ โค โง ๐ โ โค) โง 1 < ๐ด) โ (๐ < ๐ โ (๐ดโ๐) < (๐ดโ๐))) | ||
Theorem | leexp2 14136 | Ordering law for exponentiation of a fixed real base greater than 1 to integer exponents. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข (((๐ด โ โ โง ๐ โ โค โง ๐ โ โค) โง 1 < ๐ด) โ (๐ โค ๐ โ (๐ดโ๐) โค (๐ดโ๐))) | ||
Theorem | leexp2a 14137 | Weak ordering relationship for exponentiation of a fixed real base greater than or equal to 1 to integer exponents. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 5-Jun-2014.) |
โข ((๐ด โ โ โง 1 โค ๐ด โง ๐ โ (โคโฅโ๐)) โ (๐ดโ๐) โค (๐ดโ๐)) | ||
Theorem | ltexp2r 14138 | The integer powers of a fixed positive real smaller than 1 decrease as the exponent increases. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 5-Jun-2014.) |
โข (((๐ด โ โ+ โง ๐ โ โค โง ๐ โ โค) โง ๐ด < 1) โ (๐ < ๐ โ (๐ดโ๐) < (๐ดโ๐))) | ||
Theorem | leexp2r 14139 | Weak ordering relationship for exponentiation of a fixed real base in [0, 1] to integer exponents. (Contributed by Paul Chapman, 14-Jan-2008.) (Revised by Mario Carneiro, 29-Apr-2014.) |
โข (((๐ด โ โ โง ๐ โ โ0 โง ๐ โ (โคโฅโ๐)) โง (0 โค ๐ด โง ๐ด โค 1)) โ (๐ดโ๐) โค (๐ดโ๐)) | ||
Theorem | leexp1a 14140 | Weak base ordering relationship for exponentiation of real bases to a fixed nonnegative integer exponent. (Contributed by NM, 18-Dec-2005.) |
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ0) โง (0 โค ๐ด โง ๐ด โค ๐ต)) โ (๐ดโ๐) โค (๐ตโ๐)) | ||
Theorem | exple1 14141 | A real between 0 and 1 inclusive raised to a nonnegative integer power is less than or equal to 1. (Contributed by Paul Chapman, 29-Dec-2007.) (Revised by Mario Carneiro, 5-Jun-2014.) |
โข (((๐ด โ โ โง 0 โค ๐ด โง ๐ด โค 1) โง ๐ โ โ0) โ (๐ดโ๐) โค 1) | ||
Theorem | expubnd 14142 | An upper bound on ๐ดโ๐ when 2 โค ๐ด. (Contributed by NM, 19-Dec-2005.) |
โข ((๐ด โ โ โง ๐ โ โ0 โง 2 โค ๐ด) โ (๐ดโ๐) โค ((2โ๐) ยท ((๐ด โ 1)โ๐))) | ||
Theorem | sumsqeq0 14143 | The sum of two squres of reals is zero if and only if both reals are zero. (Contributed by NM, 29-Apr-2005.) (Revised by Stefan O'Rear, 5-Oct-2014.) (Proof shortened by Mario Carneiro, 28-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด = 0 โง ๐ต = 0) โ ((๐ดโ2) + (๐ตโ2)) = 0)) | ||
Theorem | sqvali 14144 | Value of square. Inference version. (Contributed by NM, 1-Aug-1999.) |
โข ๐ด โ โ โ โข (๐ดโ2) = (๐ด ยท ๐ด) | ||
Theorem | sqcli 14145 | Closure of square. (Contributed by NM, 2-Aug-1999.) |
โข ๐ด โ โ โ โข (๐ดโ2) โ โ | ||
Theorem | sqeq0i 14146 | A complex number is zero iff its square is zero. (Contributed by NM, 2-Oct-1999.) |
โข ๐ด โ โ โ โข ((๐ดโ2) = 0 โ ๐ด = 0) | ||
Theorem | sqrecii 14147 | The square of a reciprocal is the reciprocal of the square. (Contributed by NM, 17-Sep-1999.) |
โข ๐ด โ โ & โข ๐ด โ 0 โ โข ((1 / ๐ด)โ2) = (1 / (๐ดโ2)) | ||
Theorem | sqmuli 14148 | Distribution of squaring over multiplication. (Contributed by NM, 3-Sep-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((๐ด ยท ๐ต)โ2) = ((๐ดโ2) ยท (๐ตโ2)) | ||
Theorem | sqdivi 14149 | Distribution of squaring over division. (Contributed by NM, 20-Aug-2001.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ต โ 0 โ โข ((๐ด / ๐ต)โ2) = ((๐ดโ2) / (๐ตโ2)) | ||
Theorem | resqcli 14150 | Closure of square in reals. (Contributed by NM, 2-Aug-1999.) |
โข ๐ด โ โ โ โข (๐ดโ2) โ โ | ||
Theorem | sqgt0i 14151 | The square of a nonzero real is positive. (Contributed by NM, 17-Sep-1999.) |
โข ๐ด โ โ โ โข (๐ด โ 0 โ 0 < (๐ดโ2)) | ||
Theorem | sqge0i 14152 | The square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.) |
โข ๐ด โ โ โ โข 0 โค (๐ดโ2) | ||
Theorem | lt2sqi 14153 | The square function on nonnegative reals is increasing. (Contributed by NM, 12-Sep-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 โค ๐ด โง 0 โค ๐ต) โ (๐ด < ๐ต โ (๐ดโ2) < (๐ตโ2))) | ||
Theorem | le2sqi 14154 | The square function on nonnegative reals is nondecreasing. (Contributed by NM, 12-Sep-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 โค ๐ด โง 0 โค ๐ต) โ (๐ด โค ๐ต โ (๐ดโ2) โค (๐ตโ2))) | ||
Theorem | sq11i 14155 | The square function is one-to-one for nonnegative reals. (Contributed by NM, 27-Oct-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 โค ๐ด โง 0 โค ๐ต) โ ((๐ดโ2) = (๐ตโ2) โ ๐ด = ๐ต)) | ||
Theorem | sq0 14156 | The square of 0 is 0. (Contributed by NM, 6-Jun-2006.) |
โข (0โ2) = 0 | ||
Theorem | sq0i 14157 | If a number is zero, then its square is zero. (Contributed by FL, 10-Dec-2006.) |
โข (๐ด = 0 โ (๐ดโ2) = 0) | ||
Theorem | sq0id 14158 | If a number is zero, then its square is zero. Deduction form of sq0i 14157. Converse of sqeq0d 14110. (Contributed by David Moews, 28-Feb-2017.) |
โข (๐ โ ๐ด = 0) โ โข (๐ โ (๐ดโ2) = 0) | ||
Theorem | sq1 14159 | The square of 1 is 1. (Contributed by NM, 22-Aug-1999.) |
โข (1โ2) = 1 | ||
Theorem | neg1sqe1 14160 | The square of -1 is 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
โข (-1โ2) = 1 | ||
Theorem | sq2 14161 | The square of 2 is 4. (Contributed by NM, 22-Aug-1999.) |
โข (2โ2) = 4 | ||
Theorem | sq3 14162 | The square of 3 is 9. (Contributed by NM, 26-Apr-2006.) |
โข (3โ2) = 9 | ||
Theorem | sq4e2t8 14163 | The square of 4 is 2 times 8. (Contributed by AV, 20-Jul-2021.) |
โข (4โ2) = (2 ยท 8) | ||
Theorem | cu2 14164 | The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.) |
โข (2โ3) = 8 | ||
Theorem | irec 14165 | The reciprocal of i. (Contributed by NM, 11-Oct-1999.) |
โข (1 / i) = -i | ||
Theorem | i2 14166 | i squared. (Contributed by NM, 6-May-1999.) |
โข (iโ2) = -1 | ||
Theorem | i3 14167 | i cubed. (Contributed by NM, 31-Jan-2007.) |
โข (iโ3) = -i | ||
Theorem | i4 14168 | i to the fourth power. (Contributed by NM, 31-Jan-2007.) |
โข (iโ4) = 1 | ||
Theorem | nnlesq 14169 | A positive integer is less than or equal to its square. For general integers, see zzlesq 14170. (Contributed by NM, 15-Sep-1999.) (Revised by Mario Carneiro, 12-Sep-2015.) |
โข (๐ โ โ โ ๐ โค (๐โ2)) | ||
Theorem | zzlesq 14170 | An integer is less than or equal to its square. (Contributed by BJ, 6-Feb-2025.) |
โข (๐ โ โค โ ๐ โค (๐โ2)) | ||
Theorem | iexpcyc 14171 | Taking i to the ๐พ-th power is the same as using the ๐พ mod 4 -th power instead, by i4 14168. (Contributed by Mario Carneiro, 7-Jul-2014.) |
โข (๐พ โ โค โ (iโ(๐พ mod 4)) = (iโ๐พ)) | ||
Theorem | expnass 14172 | A counterexample showing that exponentiation is not associative. (Contributed by Stefan Allan and Gรฉrard Lang, 21-Sep-2010.) |
โข ((3โ3)โ3) < (3โ(3โ3)) | ||
Theorem | sqlecan 14173 | Cancel one factor of a square in a โค comparison. Unlike lemul1 12066, the common factor ๐ด may be zero. (Contributed by NM, 17-Jan-2008.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ดโ2) โค (๐ต ยท ๐ด) โ ๐ด โค ๐ต)) | ||
Theorem | subsq 14174 | Factor the difference of two squares. (Contributed by NM, 21-Feb-2008.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ2) โ (๐ตโ2)) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) | ||
Theorem | subsq2 14175 | Express the difference of the squares of two numbers as a polynomial in the difference of the numbers. (Contributed by NM, 21-Feb-2008.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ2) โ (๐ตโ2)) = (((๐ด โ ๐ต)โ2) + ((2 ยท ๐ต) ยท (๐ด โ ๐ต)))) | ||
Theorem | binom2i 14176 | The square of a binomial. (Contributed by NM, 11-Aug-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((๐ด + ๐ต)โ2) = (((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2)) | ||
Theorem | subsqi 14177 | Factor the difference of two squares. (Contributed by NM, 7-Feb-2005.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((๐ดโ2) โ (๐ตโ2)) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต)) | ||
Theorem | sqeqori 14178 | 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 NM, 15-Jan-2006.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((๐ดโ2) = (๐ตโ2) โ (๐ด = ๐ต โจ ๐ด = -๐ต)) | ||
Theorem | subsq0i 14179 | The two solutions to the difference of squares set equal to zero. (Contributed by NM, 25-Apr-2006.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (((๐ดโ2) โ (๐ตโ2)) = 0 โ (๐ด = ๐ต โจ ๐ด = -๐ต)) | ||
Theorem | sqeqor 14180 | 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.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ2) = (๐ตโ2) โ (๐ด = ๐ต โจ ๐ด = -๐ต))) | ||
Theorem | binom2 14181 | The square of a binomial. (Contributed by FL, 10-Dec-2006.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต)โ2) = (((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2))) | ||
Theorem | binom21 14182 | Special case of binom2 14181 where ๐ต = 1. (Contributed by Scott Fenton, 11-May-2014.) |
โข (๐ด โ โ โ ((๐ด + 1)โ2) = (((๐ดโ2) + (2 ยท ๐ด)) + 1)) | ||
Theorem | binom2sub 14183 | Expand the square of a subtraction. (Contributed by Scott Fenton, 10-Jun-2013.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โ ๐ต)โ2) = (((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2))) | ||
Theorem | binom2sub1 14184 | Special case of binom2sub 14183 where ๐ต = 1. (Contributed by AV, 2-Aug-2021.) |
โข (๐ด โ โ โ ((๐ด โ 1)โ2) = (((๐ดโ2) โ (2 ยท ๐ด)) + 1)) | ||
Theorem | binom2subi 14185 | Expand the square of a subtraction. (Contributed by Scott Fenton, 13-Jun-2013.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((๐ด โ ๐ต)โ2) = (((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2)) | ||
Theorem | mulbinom2 14186 | The square of a binomial with factor. (Contributed by AV, 19-Jul-2021.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (((๐ถ ยท ๐ด) + ๐ต)โ2) = ((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) + (๐ตโ2))) | ||
Theorem | binom3 14187 | The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต)โ3) = (((๐ดโ3) + (3 ยท ((๐ดโ2) ยท ๐ต))) + ((3 ยท (๐ด ยท (๐ตโ2))) + (๐ตโ3)))) | ||
Theorem | sq01 14188 | If a complex number equals its square, it must be 0 or 1. (Contributed by NM, 6-Jun-2006.) |
โข (๐ด โ โ โ ((๐ดโ2) = ๐ด โ (๐ด = 0 โจ ๐ด = 1))) | ||
Theorem | zesq 14189 | An integer is even iff its square is even. (Contributed by Mario Carneiro, 12-Sep-2015.) |
โข (๐ โ โค โ ((๐ / 2) โ โค โ ((๐โ2) / 2) โ โค)) | ||
Theorem | nnesq 14190 | A positive integer is even iff its square is even. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.) |
โข (๐ โ โ โ ((๐ / 2) โ โ โ ((๐โ2) / 2) โ โ)) | ||
Theorem | crreczi 14191 | Reciprocal of a complex number in terms of real and imaginary components. Remark in [Apostol] p. 361. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Jeff Hankins, 16-Dec-2013.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((๐ด โ 0 โจ ๐ต โ 0) โ (1 / (๐ด + (i ยท ๐ต))) = ((๐ด โ (i ยท ๐ต)) / ((๐ดโ2) + (๐ตโ2)))) | ||
Theorem | bernneq 14192 | Bernoulli's inequality, due to Johan Bernoulli (1667-1748). (Contributed by NM, 21-Feb-2005.) |
โข ((๐ด โ โ โง ๐ โ โ0 โง -1 โค ๐ด) โ (1 + (๐ด ยท ๐)) โค ((1 + ๐ด)โ๐)) | ||
Theorem | bernneq2 14193 | Variation of Bernoulli's inequality bernneq 14192. (Contributed by NM, 18-Oct-2007.) |
โข ((๐ด โ โ โง ๐ โ โ0 โง 0 โค ๐ด) โ (((๐ด โ 1) ยท ๐) + 1) โค (๐ดโ๐)) | ||
Theorem | bernneq3 14194 | A corollary of bernneq 14192. (Contributed by Mario Carneiro, 11-Mar-2014.) |
โข ((๐ โ (โคโฅโ2) โง ๐ โ โ0) โ ๐ < (๐โ๐)) | ||
Theorem | expnbnd 14195* | Exponentiation with a base greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007.) |
โข ((๐ด โ โ โง ๐ต โ โ โง 1 < ๐ต) โ โ๐ โ โ ๐ด < (๐ตโ๐)) | ||
Theorem | expnlbnd 14196* | The reciprocal of exponentiation with a base greater than 1 has no positive lower bound. (Contributed by NM, 18-Jul-2008.) |
โข ((๐ด โ โ+ โง ๐ต โ โ โง 1 < ๐ต) โ โ๐ โ โ (1 / (๐ตโ๐)) < ๐ด) | ||
Theorem | expnlbnd2 14197* | The reciprocal of exponentiation with a base greater than 1 has no positive lower bound. (Contributed by NM, 18-Jul-2008.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) |
โข ((๐ด โ โ+ โง ๐ต โ โ โง 1 < ๐ต) โ โ๐ โ โ โ๐ โ (โคโฅโ๐)(1 / (๐ตโ๐)) < ๐ด) | ||
Theorem | expmulnbnd 14198* | Exponentiation with a base greater than 1 is not bounded by any linear function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
โข ((๐ด โ โ โง ๐ต โ โ โง 1 < ๐ต) โ โ๐ โ โ0 โ๐ โ (โคโฅโ๐)(๐ด ยท ๐) < (๐ตโ๐)) | ||
Theorem | digit2 14199 | Two ways to express the ๐พ th digit in the decimal (when base ๐ต = 10) expansion of a number ๐ด. ๐พ = 1 corresponds to the first digit after the decimal point. (Contributed by NM, 25-Dec-2008.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ ((โโ((๐ตโ๐พ) ยท ๐ด)) mod ๐ต) = ((โโ((๐ตโ๐พ) ยท ๐ด)) โ (๐ต ยท (โโ((๐ตโ(๐พ โ 1)) ยท ๐ด))))) | ||
Theorem | digit1 14200 | Two ways to express the ๐พ th digit in the decimal expansion of a number ๐ด (when base ๐ต = 10). ๐พ = 1 corresponds to the first digit after the decimal point. (Contributed by NM, 3-Jan-2009.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ ((โโ((๐ตโ๐พ) ยท ๐ด)) mod ๐ต) = (((โโ((๐ตโ๐พ) ยท ๐ด)) mod (๐ตโ๐พ)) โ ((๐ต ยท (โโ((๐ตโ(๐พ โ 1)) ยท ๐ด))) mod (๐ตโ๐พ)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |