![]() |
Metamath
Proof Explorer Theorem List (p. 409 of 473) | < 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-29860) |
![]() (29861-31383) |
![]() (31384-47242) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | gcdnn0id 40801 | The gcd of a nonnegative integer and itself is the integer. (Contributed by SN, 25-Aug-2024.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁 gcd 𝑁) = 𝑁) | ||
Theorem | gcdle1d 40802 | 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 40803 | 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 40804 | Deduction associated with dvdsexpim 40800. (Contributed by SN, 21-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ∥ 𝐵) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∥ (𝐵↑𝑁)) | ||
Theorem | nn0rppwr 40805 | If 𝐴 and 𝐵 are relatively prime, then so are 𝐴↑𝑁 and 𝐵↑𝑁. rppwr 16440 extended to nonnegative integers. Less general than rpexp12i 16600. (Contributed by Steven Nguyen, 4-Apr-2023.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑𝑁) gcd (𝐵↑𝑁)) = 1)) | ||
Theorem | expgcd 40806 | Exponentiation distributes over GCD. sqgcd 16441 extended to nonnegative exponents. (Contributed by Steven Nguyen, 4-Apr-2023.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵)↑𝑁) = ((𝐴↑𝑁) gcd (𝐵↑𝑁))) | ||
Theorem | nn0expgcd 40807 | Exponentiation distributes over GCD. nn0gcdsq 16627 extended to nonnegative exponents. expgcd 40806 extended to nonnegative bases. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵)↑𝑁) = ((𝐴↑𝑁) gcd (𝐵↑𝑁))) | ||
Theorem | zexpgcd 40808 | Exponentiation distributes over GCD. zgcdsq 16628 extended to nonnegative exponents. nn0expgcd 40807 extended to integer bases by symmetry. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵)↑𝑁) = ((𝐴↑𝑁) gcd (𝐵↑𝑁))) | ||
Theorem | numdenexp 40809 | numdensq 16629 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → ((numer‘(𝐴↑𝑁)) = ((numer‘𝐴)↑𝑁) ∧ (denom‘(𝐴↑𝑁)) = ((denom‘𝐴)↑𝑁))) | ||
Theorem | numexp 40810 | numsq 16630 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (numer‘(𝐴↑𝑁)) = ((numer‘𝐴)↑𝑁)) | ||
Theorem | denexp 40811 | densq 16631 extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (denom‘(𝐴↑𝑁)) = ((denom‘𝐴)↑𝑁)) | ||
Theorem | dvdsexpnn 40812 | dvdssqlem 16442 generalized to positive integer exponents. (Contributed by SN, 20-Aug-2024.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁))) | ||
Theorem | dvdsexpnn0 40813 | dvdsexpnn 40812 generalized to include zero bases. (Contributed by SN, 15-Sep-2024.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁))) | ||
Theorem | dvdsexpb 40814 | dvdssq 16443 generalized to positive integer exponents. (Contributed by SN, 15-Sep-2024.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁))) | ||
Theorem | posqsqznn 40815 | When a positive rational squared is an integer, the rational is a positive integer. zsqrtelqelz 16633 with all terms squared and positive. (Contributed by SN, 23-Aug-2024.) |
⊢ (𝜑 → (𝐴↑2) ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℚ) & ⊢ (𝜑 → 0 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℕ) | ||
Theorem | cxpgt0d 40816 | A positive real raised to a real power is positive. (Contributed by SN, 6-Apr-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℝ) ⇒ ⊢ (𝜑 → 0 < (𝐴↑𝑐𝑁)) | ||
Theorem | zrtelqelz 40817 | zsqrtelqelz 16633 generalized to positive integer roots. (Contributed by Steven Nguyen, 6-Apr-2023.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑐(1 / 𝑁)) ∈ ℚ) → (𝐴↑𝑐(1 / 𝑁)) ∈ ℤ) | ||
Theorem | zrtdvds 40818 | A positive integer root divides its integer. (Contributed by Steven Nguyen, 6-Apr-2023.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑐(1 / 𝑁)) ∈ ℕ) → (𝐴↑𝑐(1 / 𝑁)) ∥ 𝐴) | ||
Theorem | rtprmirr 40819 | The root of a prime number is irrational. (Contributed by Steven Nguyen, 6-Apr-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑃↑𝑐(1 / 𝑁)) ∈ (ℝ ∖ ℚ)) | ||
Syntax | cresub 40820 | Real number subtraction. |
class −ℝ | ||
Definition | df-resub 40821* | Define subtraction between real numbers. This operator saves a few axioms over df-sub 11387 in certain situations. Theorem resubval 40822 shows its value, resubadd 40834 relates it to addition, and rersubcl 40833 proves its closure. It is the restriction of df-sub 11387 to the reals: subresre 40885. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ −ℝ = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (℩𝑧 ∈ ℝ (𝑦 + 𝑧) = 𝑥)) | ||
Theorem | resubval 40822* | Value of real subtraction, which is the (unique) real 𝑥 such that 𝐵 + 𝑥 = 𝐴. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (℩𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴)) | ||
Theorem | renegeulemv 40823* | Lemma for renegeu 40825 and similar. Derive existential uniqueness from existence. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴) | ||
Theorem | renegeulem 40824* | Lemma for renegeu 40825 and similar. Remove a change in bound variables from renegeulemv 40823. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴) ⇒ ⊢ (𝜑 → ∃!𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴) | ||
Theorem | renegeu 40825* | Existential uniqueness of real negatives. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) | ||
Theorem | rernegcl 40826 | Closure law for negative reals. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → (0 −ℝ 𝐴) ∈ ℝ) | ||
Theorem | renegadd 40827 | Relationship between real negation and addition. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 −ℝ 𝐴) = 𝐵 ↔ (𝐴 + 𝐵) = 0)) | ||
Theorem | renegid 40828 | Addition of a real number and its negative. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → (𝐴 + (0 −ℝ 𝐴)) = 0) | ||
Theorem | reneg0addid2 40829 | Negative zero is a left additive identity. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → ((0 −ℝ 0) + 𝐴) = 𝐴) | ||
Theorem | resubeulem1 40830 | Lemma for resubeu 40832. 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 40831 | Lemma for resubeu 40832. A value which when added to 𝐴, results in 𝐵. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + ((0 −ℝ 𝐴) + ((0 −ℝ (0 + 0)) + 𝐵))) = 𝐵) | ||
Theorem | resubeu 40832* | Existential uniqueness of real differences. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 𝐵) | ||
Theorem | rersubcl 40833 | Closure for real subtraction. Based on subcl 11400. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) ∈ ℝ) | ||
Theorem | resubadd 40834 | Relation between real subtraction and addition. Based on subadd 11404. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) | ||
Theorem | resubaddd 40835 | Relationship between subtraction and addition. Based on subaddd 11530. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) | ||
Theorem | resubf 40836 | Real subtraction is an operation on the real numbers. Based on subf 11403. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ −ℝ :(ℝ × ℝ)⟶ℝ | ||
Theorem | repncan2 40837 | Addition and subtraction of equals. Compare pncan2 11408. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐴) = 𝐵) | ||
Theorem | repncan3 40838 | Addition and subtraction of equals. Based on pncan3 11409. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + (𝐵 −ℝ 𝐴)) = 𝐵) | ||
Theorem | readdsub 40839 | Law for addition and subtraction. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐶) = ((𝐴 −ℝ 𝐶) + 𝐵)) | ||
Theorem | reladdrsub 40840 | Move LHS of a sum into RHS of a (real) difference. Version of mvlladdd 11566 with real subtraction. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → 𝐵 = (𝐶 −ℝ 𝐴)) | ||
Theorem | reltsub1 40841 | Subtraction from both sides of 'less than'. Compare ltsub1 11651. (Contributed by SN, 13-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 −ℝ 𝐶) < (𝐵 −ℝ 𝐶))) | ||
Theorem | reltsubadd2 40842 | 'Less than' relationship between addition and subtraction. Compare ltsubadd2 11626. (Contributed by SN, 13-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶))) | ||
Theorem | resubcan2 40843 | Cancellation law for real subtraction. Compare subcan2 11426. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) = (𝐵 −ℝ 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | resubsub4 40844 | Law for double subtraction. Compare subsub4 11434. (Contributed by Steven Nguyen, 14-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) −ℝ 𝐶) = (𝐴 −ℝ (𝐵 + 𝐶))) | ||
Theorem | rennncan2 40845 | Cancellation law for real subtraction. Compare nnncan2 11438. (Contributed by Steven Nguyen, 14-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) −ℝ (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐵)) | ||
Theorem | renpncan3 40846 | Cancellation law for real subtraction. Compare npncan3 11439. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) + (𝐶 −ℝ 𝐴)) = (𝐶 −ℝ 𝐵)) | ||
Theorem | repnpcan 40847 | Cancellation law for addition and real subtraction. Compare pnpcan 11440. (Contributed by Steven Nguyen, 19-May-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ (𝐴 + 𝐶)) = (𝐵 −ℝ 𝐶)) | ||
Theorem | reppncan 40848 | Cancellation law for mixed addition and real subtraction. Compare ppncan 11443. (Contributed by SN, 3-Sep-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) + (𝐵 −ℝ 𝐶)) = (𝐴 + 𝐵)) | ||
Theorem | resubidaddid1lem 40849 | Lemma for resubidaddid1 40850. A special case of npncan 11422. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → (𝐴 −ℝ 𝐵) = (𝐵 −ℝ 𝐶)) ⇒ ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) + (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐶)) | ||
Theorem | resubidaddid1 40850 | Any real number subtracted from itself forms a left additive identity. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 −ℝ 𝐴) + 𝐵) = 𝐵) | ||
Theorem | resubdi 40851 | Distribution of multiplication over real subtraction. (Contributed by Steven Nguyen, 3-Jun-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐵 −ℝ 𝐶)) = ((𝐴 · 𝐵) −ℝ (𝐴 · 𝐶))) | ||
Theorem | re1m1e0m0 40852 | Equality of two left-additive identities. See resubidaddid1 40850. Uses ax-i2m1 11119. (Contributed by SN, 25-Dec-2023.) |
⊢ (1 −ℝ 1) = (0 −ℝ 0) | ||
Theorem | sn-00idlem1 40853 | Lemma for sn-00id 40856. (Contributed by SN, 25-Dec-2023.) |
⊢ (𝐴 ∈ ℝ → (𝐴 · (0 −ℝ 0)) = (𝐴 −ℝ 𝐴)) | ||
Theorem | sn-00idlem2 40854 | Lemma for sn-00id 40856. (Contributed by SN, 25-Dec-2023.) |
⊢ ((0 −ℝ 0) ≠ 0 → (0 −ℝ 0) = 1) | ||
Theorem | sn-00idlem3 40855 | Lemma for sn-00id 40856. (Contributed by SN, 25-Dec-2023.) |
⊢ ((0 −ℝ 0) = 1 → (0 + 0) = 0) | ||
Theorem | sn-00id 40856 | 00id 11330 proven without ax-mulcom 11115 but using ax-1ne0 11120. (Though note that the current version of 00id 11330 can be changed to avoid ax-icn 11110, ax-addcl 11111, ax-mulcl 11113, ax-i2m1 11119, ax-cnre 11124. Most of this is by using 0cnALT3 40762 instead of 0cn 11147). (Contributed by SN, 25-Dec-2023.) (Proof modification is discouraged.) |
⊢ (0 + 0) = 0 | ||
Theorem | re0m0e0 40857 | Real number version of 0m0e0 12273 proven without ax-mulcom 11115. (Contributed by SN, 23-Jan-2024.) |
⊢ (0 −ℝ 0) = 0 | ||
Theorem | readdid2 40858 | Real number version of addid2 11338. (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℝ → (0 + 𝐴) = 𝐴) | ||
Theorem | sn-addid2 40859 | addid2 11338 without ax-mulcom 11115. (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴) | ||
Theorem | remul02 40860 | Real number version of mul02 11333 proven without ax-mulcom 11115. (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℝ → (0 · 𝐴) = 0) | ||
Theorem | sn-0ne2 40861 | 0ne2 12360 without ax-mulcom 11115. (Contributed by SN, 23-Jan-2024.) |
⊢ 0 ≠ 2 | ||
Theorem | remul01 40862 | Real number version of mul01 11334 proven without ax-mulcom 11115. (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℝ → (𝐴 · 0) = 0) | ||
Theorem | resubid 40863 | Subtraction of a real number from itself (compare subid 11420). (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 𝐴) = 0) | ||
Theorem | readdid1 40864 | Real number version of addid1 11335 without ax-mulcom 11115. (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℝ → (𝐴 + 0) = 𝐴) | ||
Theorem | resubid1 40865 | Real number version of subid1 11421 without ax-mulcom 11115. (Contributed by SN, 23-Jan-2024.) |
⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 0) = 𝐴) | ||
Theorem | renegneg 40866 | A real number is equal to the negative of its negative. Compare negneg 11451. (Contributed by SN, 13-Feb-2024.) |
⊢ (𝐴 ∈ ℝ → (0 −ℝ (0 −ℝ 𝐴)) = 𝐴) | ||
Theorem | readdcan2 40867 | Commuted version of readdcan 11329 without ax-mulcom 11115. (Contributed by SN, 21-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | renegid2 40868 | Commuted version of renegid 40828. (Contributed by SN, 4-May-2024.) |
⊢ (𝐴 ∈ ℝ → ((0 −ℝ 𝐴) + 𝐴) = 0) | ||
Theorem | remulneg2d 40869 | Product with negative is negative of product. (Contributed by SN, 25-Jan-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 · (0 −ℝ 𝐵)) = (0 −ℝ (𝐴 · 𝐵))) | ||
Theorem | sn-it0e0 40870 | Proof of it0e0 12375 without ax-mulcom 11115. Informally, a real number times 0 is 0, and ∃𝑟 ∈ ℝ𝑟 = i · 𝑠 by ax-cnre 11124 and renegid2 40868. (Contributed by SN, 30-Apr-2024.) |
⊢ (i · 0) = 0 | ||
Theorem | sn-negex12 40871* | A combination of cnegex 11336 and cnegex2 11337, this proof takes cnre 11152 𝐴 = 𝑟 + i · 𝑠 and shows that i · -𝑠 + -𝑟 is both a left and right inverse. (Contributed by SN, 5-May-2024.) |
⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ ((𝐴 + 𝑏) = 0 ∧ (𝑏 + 𝐴) = 0)) | ||
Theorem | sn-negex 40872* | Proof of cnegex 11336 without ax-mulcom 11115. (Contributed by SN, 30-Apr-2024.) |
⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝐴 + 𝑏) = 0) | ||
Theorem | sn-negex2 40873* | Proof of cnegex2 11337 without ax-mulcom 11115. (Contributed by SN, 5-May-2024.) |
⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝑏 + 𝐴) = 0) | ||
Theorem | sn-addcand 40874 | addcand 11358 without ax-mulcom 11115. Note how the proof is almost identical to addcan 11339. (Contributed by SN, 5-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | sn-addid1 40875 | addid1 11335 without ax-mulcom 11115. (Contributed by SN, 5-May-2024.) |
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) | ||
Theorem | sn-addcan2d 40876 | addcan2d 11359 without ax-mulcom 11115. (Contributed by SN, 5-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | reixi 40877 | ixi 11784 without ax-mulcom 11115. (Contributed by SN, 5-May-2024.) |
⊢ (i · i) = (0 −ℝ 1) | ||
Theorem | rei4 40878 | i4 14108 without ax-mulcom 11115. (Contributed by SN, 27-May-2024.) |
⊢ ((i · i) · (i · i)) = 1 | ||
Theorem | sn-addid0 40879 | A number that sums to itself is zero. Compare addid0 11574, readdid1addid2d 40766. (Contributed by SN, 5-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐴) = 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = 0) | ||
Theorem | sn-mul01 40880 | mul01 11334 without ax-mulcom 11115. (Contributed by SN, 5-May-2024.) |
⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0) | ||
Theorem | sn-subeu 40881* | negeu 11391 without ax-mulcom 11115 and complex number version of resubeu 40832. (Contributed by SN, 5-May-2024.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐴 + 𝑥) = 𝐵) | ||
Theorem | sn-subcl 40882 | subcl 11400 without ax-mulcom 11115. (Contributed by SN, 5-May-2024.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ) | ||
Theorem | sn-subf 40883 | subf 11403 without ax-mulcom 11115. (Contributed by SN, 5-May-2024.) |
⊢ − :(ℂ × ℂ)⟶ℂ | ||
Theorem | resubeqsub 40884 | Equivalence between real subtraction and subtraction. (Contributed by SN, 5-May-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (𝐴 − 𝐵)) | ||
Theorem | subresre 40885 | Subtraction restricted to the reals. (Contributed by SN, 5-May-2024.) |
⊢ −ℝ = ( − ↾ (ℝ × ℝ)) | ||
Theorem | addinvcom 40886 | A number commutes with its additive inverse. Compare remulinvcom 40887. (Contributed by SN, 5-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) = 0) ⇒ ⊢ (𝜑 → (𝐵 + 𝐴) = 0) | ||
Theorem | remulinvcom 40887 | A left multiplicative inverse is a right multiplicative inverse. Proven without ax-mulcom 11115. (Contributed by SN, 5-Feb-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴 · 𝐵) = 1) ⇒ ⊢ (𝜑 → (𝐵 · 𝐴) = 1) | ||
Theorem | remulid2 40888 | Commuted version of ax-1rid 11121 without ax-mulcom 11115. (Contributed by SN, 5-Feb-2024.) |
⊢ (𝐴 ∈ ℝ → (1 · 𝐴) = 𝐴) | ||
Theorem | sn-1ticom 40889 | Lemma for sn-mulid2 40890 and it1ei 40891. (Contributed by SN, 27-May-2024.) |
⊢ (1 · i) = (i · 1) | ||
Theorem | sn-mulid2 40890 | mulid2 11154 without ax-mulcom 11115. (Contributed by SN, 27-May-2024.) |
⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴) | ||
Theorem | it1ei 40891 | 1 is a multiplicative identity for i (see sn-mulid2 40890 for commuted version). (Contributed by SN, 1-Jun-2024.) |
⊢ (i · 1) = i | ||
Theorem | ipiiie0 40892 | The multiplicative inverse of i (per i4 14108) is also its additive inverse. (Contributed by SN, 30-Jun-2024.) |
⊢ (i + (i · (i · i))) = 0 | ||
Theorem | remulcand 40893 | Commuted version of remulcan2d 40765 without ax-mulcom 11115. (Contributed by SN, 21-Feb-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | sn-0tie0 40894 | Lemma for sn-mul02 40895. Commuted version of sn-it0e0 40870. (Contributed by SN, 30-Jun-2024.) |
⊢ (0 · i) = 0 | ||
Theorem | sn-mul02 40895 | mul02 11333 without ax-mulcom 11115. See https://github.com/icecream17/Stuff/blob/main/math/0A%3D0.md 11115 for an outline. (Contributed by SN, 30-Jun-2024.) |
⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0) | ||
Theorem | sn-ltaddpos 40896 | ltaddpos 11645 without ax-mulcom 11115. (Contributed by SN, 13-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴))) | ||
Theorem | sn-ltaddneg 40897 | ltaddneg 11370 without ax-mulcom 11115. (Contributed by SN, 25-Jan-2025.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ (𝐵 + 𝐴) < 𝐵)) | ||
Theorem | reposdif 40898 | Comparison of two numbers whose difference is positive. Compare posdif 11648. (Contributed by SN, 13-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 −ℝ 𝐴))) | ||
Theorem | relt0neg1 40899 | Comparison of a real and its negative to zero. Compare lt0neg1 11661. (Contributed by SN, 13-Feb-2024.) |
⊢ (𝐴 ∈ ℝ → (𝐴 < 0 ↔ 0 < (0 −ℝ 𝐴))) | ||
Theorem | relt0neg2 40900 | Comparison of a real and its negative to zero. Compare lt0neg2 11662. (Contributed by SN, 13-Feb-2024.) |
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ (0 −ℝ 𝐴) < 0)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |