![]() |
Metamath
Proof Explorer Theorem List (p. 413 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 | sqdeccom12 41201 | The square of a number in terms of its digits switched. (Contributed by Steven Nguyen, 3-Jan-2023.) |
β’ π΄ β β0 & β’ π΅ β β0 β β’ ((;π΄π΅ Β· ;π΄π΅) β (;π΅π΄ Β· ;π΅π΄)) = (;99 Β· ((π΄ Β· π΄) β (π΅ Β· π΅))) | ||
Theorem | sq3deccom12 41202 | Variant of sqdeccom12 41201 with a three digit square. (Contributed by Steven Nguyen, 3-Jan-2023.) |
β’ π΄ β β0 & β’ π΅ β β0 & β’ πΆ β β0 & β’ (π΄ + πΆ) = π· β β’ ((;;π΄π΅πΆ Β· ;;π΄π΅πΆ) β (;π·π΅ Β· ;π·π΅)) = (;99 Β· ((;π΄π΅ Β· ;π΄π΅) β (πΆ Β· πΆ))) | ||
Theorem | 4t5e20 41203 | 4 times 5 equals 20. (Contributed by SN, 30-Mar-2025.) |
β’ (4 Β· 5) = ;20 | ||
Theorem | sq9 41204 | The square of 9 is 81. (Contributed by SN, 30-Mar-2025.) |
β’ (9β2) = ;81 | ||
Theorem | 235t711 41205 |
Calculate a product by long multiplication as a base comparison with other
multiplication algorithms.
Conveniently, 711 has two ones which greatly simplifies calculations like 235 Β· 1. There isn't a higher level mulcomli 11223 saving the lower level uses of mulcomli 11223 within 235 Β· 7 since mulcom2 doesn't exist, but if commuted versions of theorems like 7t2e14 12786 are added then this proof would benefit more than ex-decpmul 41206. For practicality, this proof doesn't have "e167085" at the end of its name like 2p2e4 12347 or 8t7e56 12797. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.) |
β’ (;;235 Β· ;;711) = ;;;;;167085 | ||
Theorem | ex-decpmul 41206 | Example usage of decpmul 41200. This proof is significantly longer than 235t711 41205. There is more unnecessary carrying compared to 235t711 41205. Although saving 5 visual steps, using mulcomli 11223 early on increases the compressed proof length. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (;;235 Β· ;;711) = ;;;;;167085 | ||
Theorem | fz1sumconst 41207* | The sum of π constant terms (π is not free in πΆ). (Contributed by SN, 21-Mar-2025.) |
β’ (π β π β β0) & β’ (π β πΆ β β) β β’ (π β Ξ£π β (1...π)πΆ = (π Β· πΆ)) | ||
Theorem | fz1sump1 41208* | Add one more term to a sum. Special case of fsump1 15702 generalized to π β β0. (Contributed by SN, 22-Mar-2025.) |
β’ (π β π β β0) & β’ ((π β§ π β (1...(π + 1))) β π΄ β β) & β’ (π = (π + 1) β π΄ = π΅) β β’ (π β Ξ£π β (1...(π + 1))π΄ = (Ξ£π β (1...π)π΄ + π΅)) | ||
Theorem | oddnumth 41209* | The Odd Number Theorem. The sum of the first π odd numbers is πβ2. A corollary of arisum 15806. (Contributed by SN, 21-Mar-2025.) |
β’ (π β β0 β Ξ£π β (1...π)((2 Β· π) β 1) = (πβ2)) | ||
Theorem | nicomachus 41210* | Nicomachus's Theorem. The sum of the odd numbers from πβ2 β π + 1 to πβ2 + π β 1 is πβ3. Proof 2 from https://proofwiki.org/wiki/Nicomachus%27s_Theorem. (Contributed by SN, 21-Mar-2025.) |
β’ (π β β0 β Ξ£π β (1...π)(((πβ2) β π) + ((2 Β· π) β 1)) = (πβ3)) | ||
Theorem | sumcubes 41211* | The sum of the first π perfect cubes is the sum of the first π nonnegative integers, squared. This is the Proof by Nicomachus from https://proofwiki.org/wiki/Sum_of_Sequence_of_Cubes using induction and index shifting to collect all the odd numbers. (Contributed by SN, 22-Mar-2025.) |
β’ (π β β0 β Ξ£π β (1...π)(πβ3) = (Ξ£π β (1...π)πβ2)) | ||
Theorem | oexpreposd 41212 | Lemma for dffltz 41376. TODO-SN?: This can be used to show exp11d 41216 holds for all integers when the exponent is odd. The more standard Β¬ 2 β₯ π should be used. (Contributed by SN, 4-Mar-2023.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β Β¬ (π / 2) β β) β β’ (π β (0 < π β 0 < (πβπ))) | ||
Theorem | ltexp1d 41213 | ltmul1d 13057 for exponentiation of positive reals. (Contributed by Steven Nguyen, 22-Aug-2023.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) & β’ (π β π β β) β β’ (π β (π΄ < π΅ β (π΄βπ) < (π΅βπ))) | ||
Theorem | ltexp1dd 41214 | Raising both sides of 'less than' to the same positive integer preserves ordering. (Contributed by Steven Nguyen, 24-Aug-2023.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) & β’ (π β π β β) & β’ (π β π΄ < π΅) β β’ (π β (π΄βπ) < (π΅βπ)) | ||
Theorem | exp11nnd 41215 | sq11d 14221 for positive real bases and positive integer exponents. The base cannot be generalized much further, since if π is even then we have π΄βπ = -π΄βπ. (Contributed by SN, 14-Sep-2023.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) & β’ (π β π β β) & β’ (π β (π΄βπ) = (π΅βπ)) β β’ (π β π΄ = π΅) | ||
Theorem | exp11d 41216 | exp11nnd 41215 for nonzero integer exponents. (Contributed by SN, 14-Sep-2023.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) & β’ (π β π β β€) & β’ (π β π β 0) & β’ (π β (π΄βπ) = (π΅βπ)) β β’ (π β π΄ = π΅) | ||
Theorem | 0dvds0 41217 | 0 divides 0. (Contributed by SN, 15-Sep-2024.) |
β’ 0 β₯ 0 | ||
Theorem | absdvdsabsb 41218 | Divisibility is invariant under taking the absolute value on both sides. (Contributed by SN, 15-Sep-2024.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β (absβπ) β₯ (absβπ))) | ||
Theorem | dvdsexpim 41219 | dvdssqim 16496 generalized to nonnegative exponents. (Contributed by Steven Nguyen, 2-Apr-2023.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π β β0) β (π΄ β₯ π΅ β (π΄βπ) β₯ (π΅βπ))) | ||
Theorem | gcdnn0id 41220 | The gcd of a nonnegative integer and itself is the integer. (Contributed by SN, 25-Aug-2024.) |
β’ (π β β0 β (π gcd π) = π) | ||
Theorem | gcdle1d 41221 | The greatest common divisor of a positive integer and another integer is less than or equal to the positive integer. (Contributed by SN, 25-Aug-2024.) |
β’ (π β π β β) & β’ (π β π β β€) β β’ (π β (π gcd π) β€ π) | ||
Theorem | gcdle2d 41222 | The greatest common divisor of a positive integer and another integer is less than or equal to the positive integer. (Contributed by SN, 25-Aug-2024.) |
β’ (π β π β β€) & β’ (π β π β β) β β’ (π β (π gcd π) β€ π) | ||
Theorem | dvdsexpad 41223 | Deduction associated with dvdsexpim 41219. (Contributed by SN, 21-Aug-2024.) |
β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ (π β π β β0) & β’ (π β π΄ β₯ π΅) β β’ (π β (π΄βπ) β₯ (π΅βπ)) | ||
Theorem | nn0rppwr 41224 | If π΄ and π΅ are relatively prime, then so are π΄βπ and π΅βπ. rppwr 16501 extended to nonnegative integers. Less general than rpexp12i 16661. (Contributed by Steven Nguyen, 4-Apr-2023.) |
β’ ((π΄ β β0 β§ π΅ β β0 β§ π β β0) β ((π΄ gcd π΅) = 1 β ((π΄βπ) gcd (π΅βπ)) = 1)) | ||
Theorem | expgcd 41225 | Exponentiation distributes over GCD. sqgcd 16502 extended to nonnegative exponents. (Contributed by Steven Nguyen, 4-Apr-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β0) β ((π΄ gcd π΅)βπ) = ((π΄βπ) gcd (π΅βπ))) | ||
Theorem | nn0expgcd 41226 | Exponentiation distributes over GCD. nn0gcdsq 16688 extended to nonnegative exponents. expgcd 41225 extended to nonnegative bases. (Contributed by Steven Nguyen, 5-Apr-2023.) |
β’ ((π΄ β β0 β§ π΅ β β0 β§ π β β0) β ((π΄ gcd π΅)βπ) = ((π΄βπ) gcd (π΅βπ))) | ||
Theorem | zexpgcd 41227 | Exponentiation distributes over GCD. zgcdsq 16689 extended to nonnegative exponents. nn0expgcd 41226 extended to integer bases by symmetry. (Contributed by Steven Nguyen, 5-Apr-2023.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π β β0) β ((π΄ gcd π΅)βπ) = ((π΄βπ) gcd (π΅βπ))) | ||
Theorem | numdenexp 41228 | numdensq 16690 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
β’ ((π΄ β β β§ π β β0) β ((numerβ(π΄βπ)) = ((numerβπ΄)βπ) β§ (denomβ(π΄βπ)) = ((denomβπ΄)βπ))) | ||
Theorem | numexp 41229 | numsq 16691 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
β’ ((π΄ β β β§ π β β0) β (numerβ(π΄βπ)) = ((numerβπ΄)βπ)) | ||
Theorem | denexp 41230 | densq 16692 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
β’ ((π΄ β β β§ π β β0) β (denomβ(π΄βπ)) = ((denomβπ΄)βπ)) | ||
Theorem | dvdsexpnn 41231 | dvdssqlem 16503 generalized to positive integer exponents. (Contributed by SN, 20-Aug-2024.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β) β (π΄ β₯ π΅ β (π΄βπ) β₯ (π΅βπ))) | ||
Theorem | dvdsexpnn0 41232 | dvdsexpnn 41231 generalized to include zero bases. (Contributed by SN, 15-Sep-2024.) |
β’ ((π΄ β β0 β§ π΅ β β0 β§ π β β) β (π΄ β₯ π΅ β (π΄βπ) β₯ (π΅βπ))) | ||
Theorem | dvdsexpb 41233 | dvdssq 16504 generalized to positive integer exponents. (Contributed by SN, 15-Sep-2024.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π β β) β (π΄ β₯ π΅ β (π΄βπ) β₯ (π΅βπ))) | ||
Theorem | posqsqznn 41234 | When a positive rational squared is an integer, the rational is a positive integer. zsqrtelqelz 16694 with all terms squared and positive. (Contributed by SN, 23-Aug-2024.) |
β’ (π β (π΄β2) β β€) & β’ (π β π΄ β β) & β’ (π β 0 < π΄) β β’ (π β π΄ β β) | ||
Theorem | zrtelqelz 41235 | zsqrtelqelz 16694 generalized to positive integer roots. (Contributed by Steven Nguyen, 6-Apr-2023.) |
β’ ((π΄ β β€ β§ π β β β§ (π΄βπ(1 / π)) β β) β (π΄βπ(1 / π)) β β€) | ||
Theorem | zrtdvds 41236 | A positive integer root divides its integer. (Contributed by Steven Nguyen, 6-Apr-2023.) |
β’ ((π΄ β β€ β§ π β β β§ (π΄βπ(1 / π)) β β) β (π΄βπ(1 / π)) β₯ π΄) | ||
Theorem | rtprmirr 41237 | The root of a prime number is irrational. (Contributed by Steven Nguyen, 6-Apr-2023.) |
β’ ((π β β β§ π β (β€β₯β2)) β (πβπ(1 / π)) β (β β β)) | ||
Syntax | cresub 41238 | Real number subtraction. |
class ββ | ||
Definition | df-resub 41239* | Define subtraction between real numbers. This operator saves a few axioms over df-sub 11446 in certain situations. Theorem resubval 41240 shows its value, resubadd 41252 relates it to addition, and rersubcl 41251 proves its closure. It is the restriction of df-sub 11446 to the reals: subresre 41303. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ββ = (π₯ β β, π¦ β β β¦ (β©π§ β β (π¦ + π§) = π₯)) | ||
Theorem | resubval 41240* | Value of real subtraction, which is the (unique) real π₯ such that π΅ + π₯ = π΄. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ ββ π΅) = (β©π₯ β β (π΅ + π₯) = π΄)) | ||
Theorem | renegeulemv 41241* | Lemma for renegeu 41243 and similar. Derive existential uniqueness from existence. (Contributed by Steven Nguyen, 28-Jan-2023.) |
β’ (π β π΅ β β) & β’ (π β βπ¦ β β (π΅ + π¦) = π΄) β β’ (π β β!π₯ β β (π΅ + π₯) = π΄) | ||
Theorem | renegeulem 41242* | Lemma for renegeu 41243 and similar. Remove a change in bound variables from renegeulemv 41241. (Contributed by Steven Nguyen, 28-Jan-2023.) |
β’ (π β π΅ β β) & β’ (π β βπ¦ β β (π΅ + π¦) = π΄) β β’ (π β β!π¦ β β (π΅ + π¦) = π΄) | ||
Theorem | renegeu 41243* | Existential uniqueness of real negatives. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ (π΄ β β β β!π₯ β β (π΄ + π₯) = 0) | ||
Theorem | rernegcl 41244 | Closure law for negative reals. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ (π΄ β β β (0 ββ π΄) β β) | ||
Theorem | renegadd 41245 | Relationship between real negation and addition. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β ((0 ββ π΄) = π΅ β (π΄ + π΅) = 0)) | ||
Theorem | renegid 41246 | Addition of a real number and its negative. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ (π΄ β β β (π΄ + (0 ββ π΄)) = 0) | ||
Theorem | reneg0addlid 41247 | Negative zero is a left additive identity. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ (π΄ β β β ((0 ββ 0) + π΄) = π΄) | ||
Theorem | resubeulem1 41248 | Lemma for resubeu 41250. A value which when added to zero, results in negative zero. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ (π΄ β β β (0 + (0 ββ (0 + 0))) = (0 ββ 0)) | ||
Theorem | resubeulem2 41249 | Lemma for resubeu 41250. A value which when added to π΄, results in π΅. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ + ((0 ββ π΄) + ((0 ββ (0 + 0)) + π΅))) = π΅) | ||
Theorem | resubeu 41250* | Existential uniqueness of real differences. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β β!π₯ β β (π΄ + π₯) = π΅) | ||
Theorem | rersubcl 41251 | Closure for real subtraction. Based on subcl 11459. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ ββ π΅) β β) | ||
Theorem | resubadd 41252 | Relation between real subtraction and addition. Based on subadd 11463. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) = πΆ β (π΅ + πΆ) = π΄)) | ||
Theorem | resubaddd 41253 | Relationship between subtraction and addition. Based on subaddd 11589. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((π΄ ββ π΅) = πΆ β (π΅ + πΆ) = π΄)) | ||
Theorem | resubf 41254 | Real subtraction is an operation on the real numbers. Based on subf 11462. (Contributed by Steven Nguyen, 7-Jan-2023.) |
β’ ββ :(β Γ β)βΆβ | ||
Theorem | repncan2 41255 | Addition and subtraction of equals. Compare pncan2 11467. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ + π΅) ββ π΄) = π΅) | ||
Theorem | repncan3 41256 | Addition and subtraction of equals. Based on pncan3 11468. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ + (π΅ ββ π΄)) = π΅) | ||
Theorem | readdsub 41257 | Law for addition and subtraction. (Contributed by Steven Nguyen, 28-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) ββ πΆ) = ((π΄ ββ πΆ) + π΅)) | ||
Theorem | reladdrsub 41258 | Move LHS of a sum into RHS of a (real) difference. Version of mvlladdd 11625 with real subtraction. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (π΄ + π΅) = πΆ) β β’ (π β π΅ = (πΆ ββ π΄)) | ||
Theorem | reltsub1 41259 | Subtraction from both sides of 'less than'. Compare ltsub1 11710. (Contributed by SN, 13-Feb-2024.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ < π΅ β (π΄ ββ πΆ) < (π΅ ββ πΆ))) | ||
Theorem | reltsubadd2 41260 | 'Less than' relationship between addition and subtraction. Compare ltsubadd2 11685. (Contributed by SN, 13-Feb-2024.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) < πΆ β π΄ < (π΅ + πΆ))) | ||
Theorem | resubcan2 41261 | Cancellation law for real subtraction. Compare subcan2 11485. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ πΆ) = (π΅ ββ πΆ) β π΄ = π΅)) | ||
Theorem | resubsub4 41262 | Law for double subtraction. Compare subsub4 11493. (Contributed by Steven Nguyen, 14-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) ββ πΆ) = (π΄ ββ (π΅ + πΆ))) | ||
Theorem | rennncan2 41263 | Cancellation law for real subtraction. Compare nnncan2 11497. (Contributed by Steven Nguyen, 14-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ πΆ) ββ (π΅ ββ πΆ)) = (π΄ ββ π΅)) | ||
Theorem | renpncan3 41264 | Cancellation law for real subtraction. Compare npncan3 11498. (Contributed by Steven Nguyen, 28-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ ββ π΅) + (πΆ ββ π΄)) = (πΆ ββ π΅)) | ||
Theorem | repnpcan 41265 | Cancellation law for addition and real subtraction. Compare pnpcan 11499. (Contributed by Steven Nguyen, 19-May-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) ββ (π΄ + πΆ)) = (π΅ ββ πΆ)) | ||
Theorem | reppncan 41266 | Cancellation law for mixed addition and real subtraction. Compare ppncan 11502. (Contributed by SN, 3-Sep-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + πΆ) + (π΅ ββ πΆ)) = (π΄ + π΅)) | ||
Theorem | resubidaddlidlem 41267 | Lemma for resubidaddlid 41268. A special case of npncan 11481. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β (π΄ ββ π΅) = (π΅ ββ πΆ)) β β’ (π β ((π΄ ββ π΅) + (π΅ ββ πΆ)) = (π΄ ββ πΆ)) | ||
Theorem | resubidaddlid 41268 | Any real number subtracted from itself forms a left additive identity. (Contributed by Steven Nguyen, 8-Jan-2023.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ ββ π΄) + π΅) = π΅) | ||
Theorem | resubdi 41269 | Distribution of multiplication over real subtraction. (Contributed by Steven Nguyen, 3-Jun-2023.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄ Β· (π΅ ββ πΆ)) = ((π΄ Β· π΅) ββ (π΄ Β· πΆ))) | ||
Theorem | re1m1e0m0 41270 | Equality of two left-additive identities. See resubidaddlid 41268. Uses ax-i2m1 11178. (Contributed by SN, 25-Dec-2023.) |
β’ (1 ββ 1) = (0 ββ 0) | ||
Theorem | sn-00idlem1 41271 | Lemma for sn-00id 41274. (Contributed by SN, 25-Dec-2023.) |
β’ (π΄ β β β (π΄ Β· (0 ββ 0)) = (π΄ ββ π΄)) | ||
Theorem | sn-00idlem2 41272 | Lemma for sn-00id 41274. (Contributed by SN, 25-Dec-2023.) |
β’ ((0 ββ 0) β 0 β (0 ββ 0) = 1) | ||
Theorem | sn-00idlem3 41273 | Lemma for sn-00id 41274. (Contributed by SN, 25-Dec-2023.) |
β’ ((0 ββ 0) = 1 β (0 + 0) = 0) | ||
Theorem | sn-00id 41274 | 00id 11389 proven without ax-mulcom 11174 but using ax-1ne0 11179. (Though note that the current version of 00id 11389 can be changed to avoid ax-icn 11169, ax-addcl 11170, ax-mulcl 11172, ax-i2m1 11178, ax-cnre 11183. Most of this is by using 0cnALT3 41174 instead of 0cn 11206). (Contributed by SN, 25-Dec-2023.) (Proof modification is discouraged.) |
β’ (0 + 0) = 0 | ||
Theorem | re0m0e0 41275 | Real number version of 0m0e0 12332 proven without ax-mulcom 11174. (Contributed by SN, 23-Jan-2024.) |
β’ (0 ββ 0) = 0 | ||
Theorem | readdlid 41276 | Real number version of addlid 11397. (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (0 + π΄) = π΄) | ||
Theorem | sn-addlid 41277 | addlid 11397 without ax-mulcom 11174. (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (0 + π΄) = π΄) | ||
Theorem | remul02 41278 | Real number version of mul02 11392 proven without ax-mulcom 11174. (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (0 Β· π΄) = 0) | ||
Theorem | sn-0ne2 41279 | 0ne2 12419 without ax-mulcom 11174. (Contributed by SN, 23-Jan-2024.) |
β’ 0 β 2 | ||
Theorem | remul01 41280 | Real number version of mul01 11393 proven without ax-mulcom 11174. (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (π΄ Β· 0) = 0) | ||
Theorem | resubid 41281 | Subtraction of a real number from itself (compare subid 11479). (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (π΄ ββ π΄) = 0) | ||
Theorem | readdrid 41282 | Real number version of addrid 11394 without ax-mulcom 11174. (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (π΄ + 0) = π΄) | ||
Theorem | resubid1 41283 | Real number version of subid1 11480 without ax-mulcom 11174. (Contributed by SN, 23-Jan-2024.) |
β’ (π΄ β β β (π΄ ββ 0) = π΄) | ||
Theorem | renegneg 41284 | A real number is equal to the negative of its negative. Compare negneg 11510. (Contributed by SN, 13-Feb-2024.) |
β’ (π΄ β β β (0 ββ (0 ββ π΄)) = π΄) | ||
Theorem | readdcan2 41285 | Commuted version of readdcan 11388 without ax-mulcom 11174. (Contributed by SN, 21-Feb-2024.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + πΆ) = (π΅ + πΆ) β π΄ = π΅)) | ||
Theorem | renegid2 41286 | Commuted version of renegid 41246. (Contributed by SN, 4-May-2024.) |
β’ (π΄ β β β ((0 ββ π΄) + π΄) = 0) | ||
Theorem | remulneg2d 41287 | Product with negative is negative of product. (Contributed by SN, 25-Jan-2025.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΄ Β· (0 ββ π΅)) = (0 ββ (π΄ Β· π΅))) | ||
Theorem | sn-it0e0 41288 | Proof of it0e0 12434 without ax-mulcom 11174. Informally, a real number times 0 is 0, and βπ β βπ = i Β· π by ax-cnre 11183 and renegid2 41286. (Contributed by SN, 30-Apr-2024.) |
β’ (i Β· 0) = 0 | ||
Theorem | sn-negex12 41289* | A combination of cnegex 11395 and cnegex2 11396, this proof takes cnre 11211 π΄ = π + i Β· π and shows that i Β· -π + -π is both a left and right inverse. (Contributed by SN, 5-May-2024.) |
β’ (π΄ β β β βπ β β ((π΄ + π) = 0 β§ (π + π΄) = 0)) | ||
Theorem | sn-negex 41290* | Proof of cnegex 11395 without ax-mulcom 11174. (Contributed by SN, 30-Apr-2024.) |
β’ (π΄ β β β βπ β β (π΄ + π) = 0) | ||
Theorem | sn-negex2 41291* | Proof of cnegex2 11396 without ax-mulcom 11174. (Contributed by SN, 5-May-2024.) |
β’ (π΄ β β β βπ β β (π + π΄) = 0) | ||
Theorem | sn-addcand 41292 | addcand 11417 without ax-mulcom 11174. Note how the proof is almost identical to addcan 11398. (Contributed by SN, 5-May-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((π΄ + π΅) = (π΄ + πΆ) β π΅ = πΆ)) | ||
Theorem | sn-addrid 41293 | addrid 11394 without ax-mulcom 11174. (Contributed by SN, 5-May-2024.) |
β’ (π΄ β β β (π΄ + 0) = π΄) | ||
Theorem | sn-addcan2d 41294 | addcan2d 11418 without ax-mulcom 11174. (Contributed by SN, 5-May-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((π΄ + πΆ) = (π΅ + πΆ) β π΄ = π΅)) | ||
Theorem | reixi 41295 | ixi 11843 without ax-mulcom 11174. (Contributed by SN, 5-May-2024.) |
β’ (i Β· i) = (0 ββ 1) | ||
Theorem | rei4 41296 | i4 14168 without ax-mulcom 11174. (Contributed by SN, 27-May-2024.) |
β’ ((i Β· i) Β· (i Β· i)) = 1 | ||
Theorem | sn-addid0 41297 | A number that sums to itself is zero. Compare addid0 11633, readdridaddlidd 41178. (Contributed by SN, 5-May-2024.) |
β’ (π β π΄ β β) & β’ (π β (π΄ + π΄) = π΄) β β’ (π β π΄ = 0) | ||
Theorem | sn-mul01 41298 | mul01 11393 without ax-mulcom 11174. (Contributed by SN, 5-May-2024.) |
β’ (π΄ β β β (π΄ Β· 0) = 0) | ||
Theorem | sn-subeu 41299* | negeu 11450 without ax-mulcom 11174 and complex number version of resubeu 41250. (Contributed by SN, 5-May-2024.) |
β’ ((π΄ β β β§ π΅ β β) β β!π₯ β β (π΄ + π₯) = π΅) | ||
Theorem | sn-subcl 41300 | subcl 11459 without ax-mulcom 11174. (Contributed by SN, 5-May-2024.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ β π΅) β β) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |