P. 424 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42301-42400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	absdvdsabsb 42301	Divisibility is invariant under taking the absolute value on both sides. (Contributed by SN, 15-Sep-2024.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) ∥ (abs‘𝑁)))
Theorem	gcdnn0id 42302	The gcd of a nonnegative integer and itself is the integer. (Contributed by SN, 25-Aug-2024.)
⊢ (𝑁 ∈ ℕ0 → (𝑁 gcd 𝑁) = 𝑁)
Theorem	gcdle1d 42303	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 42304	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 42305	Deduction associated with dvdsexpim 16484. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ∥ (𝐵↑𝑁))
Theorem	dvdsexpnn 42306	dvdssqlem 16495 generalized to positive integer exponents. (Contributed by SN, 20-Aug-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))
Theorem	dvdsexpnn0 42307	dvdsexpnn 42306 generalized to include zero bases. (Contributed by SN, 15-Sep-2024.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))
Theorem	dvdsexpb 42308	dvdssq 16496 generalized to positive integer exponents. (Contributed by SN, 15-Sep-2024.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))
Theorem	posqsqznn 42309	When a positive rational squared is an integer, the rational is a positive integer. zsqrtelqelz 16687 with all terms squared and positive. (Contributed by SN, 23-Aug-2024.)
⊢ (𝜑 → (𝐴↑2) ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ ℚ)    &   ⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℕ)
Theorem	zdivgd 42310*	Two ways to express "𝑁 is an integer multiple of 𝑀". Originally a subproof of zdiv 12564. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℂ)    &   ⊢ (𝜑 → 𝑀 ≠ 0)    ⇒   ⊢ (𝜑 → (∃𝑘 ∈ ℤ (𝑀 · 𝑘) = 𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ))
Theorem	efsubd 42311	Difference of exponents law for exponential function, deduction form. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (exp‘(𝐴 − 𝐵)) = ((exp‘𝐴) / (exp‘𝐵)))
Theorem	ef11d 42312*	General condition for the exponential function to be one-to-one. efper 26404 shows that exponentiation is periodic. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((exp‘𝐴) = (exp‘𝐵) ↔ ∃𝑛 ∈ ℤ 𝐴 = (𝐵 + ((i · (2 · π)) · 𝑛))))
Theorem	logccne0d 42313	The logarithm isn't 0 if its argument isn't 0 or 1, deduction form. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐴 ≠ 1)    ⇒   ⊢ (𝜑 → (log‘𝐴) ≠ 0)
Theorem	cxp112d 42314*	General condition for complex exponentiation to be one-to-one with respect to the second argument. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 1)    ⇒   ⊢ (𝜑 → ((𝐶↑𝑐𝐴) = (𝐶↑𝑐𝐵) ↔ ∃𝑛 ∈ ℤ 𝐴 = (𝐵 + (((i · (2 · π)) · 𝑛) / (log‘𝐶)))))
Theorem	cxp111d 42315*	General condition for complex exponentiation to be one-to-one with respect to the first argument. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴↑𝑐𝐶) = (𝐵↑𝑐𝐶) ↔ ∃𝑛 ∈ ℤ (log‘𝐴) = ((log‘𝐵) + (((i · (2 · π)) · 𝑛) / 𝐶))))
Theorem	cxpi11d 42316*	i to the powers of 𝐴 and 𝐵 are equal iff 𝐴 and 𝐵 are a multiple of 4 apart. EDITORIAL: This theorem may be revised to a more convenient form. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((i↑𝑐𝐴) = (i↑𝑐𝐵) ↔ ∃𝑛 ∈ ℤ 𝐴 = (𝐵 + (4 · 𝑛))))
Theorem	logne0d 42317	Deduction form of logne0 26504. See logccne0d 42313 for a more general version. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 ≠ 1)    ⇒   ⊢ (𝜑 → (log‘𝐴) ≠ 0)
Theorem	rxp112d 42318	Real exponentiation is one-to-one with respect to the second argument. (TODO: Note that the base 𝐶 must be positive since -𝐶↑𝐴 is 𝐶↑𝐴 · e↑iπ𝐴, so in the negative case 𝐴 = 𝐵 + 2𝑘). (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 1)    &   ⊢ (𝜑 → (𝐶↑𝑐𝐴) = (𝐶↑𝑐𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	log11d 42319	The natural logarithm is one-to-one. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((log‘𝐴) = (log‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	rplog11d 42320	The natural logarithm is one-to-one on positive reals. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((log‘𝐴) = (log‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	rxp11d 42321	Real exponentiation is one-to-one with respect to the first argument. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    &   ⊢ (𝜑 → (𝐴↑𝑐𝐶) = (𝐵↑𝑐𝐶))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
21.30.4  Trigonometry and Calculus
Theorem	tanhalfpim 42322	The tangent of π / 2 minus a number is the cotangent, here represented by cos𝐴 / sin𝐴. (Contributed by SN, 2-Sep-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (sin‘𝐴) ≠ 0)    ⇒   ⊢ (𝜑 → (tan‘((π / 2) − 𝐴)) = ((cos‘𝐴) / (sin‘𝐴)))
Theorem	sinpim 42323	Sine of a number subtracted from π. (Contributed by SN, 19-Nov-2025.)
⊢ (𝐴 ∈ ℂ → (sin‘(π − 𝐴)) = (sin‘𝐴))
Theorem	cospim 42324	Cosine of a number subtracted from π. (Contributed by SN, 19-Nov-2025.)
⊢ (𝐴 ∈ ℂ → (cos‘(π − 𝐴)) = -(cos‘𝐴))
Theorem	tan3rdpi 42325	The tangent of π / 3 is √3. (Contributed by SN, 2-Sep-2025.)
⊢ (tan‘(π / 3)) = (√‘3)
Theorem	sin2t3rdpi 42326	The sine of 2 · (π / 3) is (√3) / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (sin‘(2 · (π / 3))) = ((√‘3) / 2)
Theorem	cos2t3rdpi 42327	The cosine of 2 · (π / 3) is -1 / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (cos‘(2 · (π / 3))) = -(1 / 2)
Theorem	sin4t3rdpi 42328	The sine of 4 · (π / 3) is -(√3) / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (sin‘(4 · (π / 3))) = -((√‘3) / 2)
Theorem	cos4t3rdpi 42329	The cosine of 4 · (π / 3) is -1 / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (cos‘(4 · (π / 3))) = -(1 / 2)
Theorem	asin1half 42330	The arcsine of 1 / 2 is π / 6. (Contributed by SN, 31-Aug-2025.)
⊢ (arcsin‘(1 / 2)) = (π / 6)
Theorem	acos1half 42331	The arccosine of 1 / 2 is π / 3. (Contributed by SN, 31-Aug-2024.)
⊢ (arccos‘(1 / 2)) = (π / 3)
Theorem	dvun 42332	Condition for the union of the derivatives of two disjoint functions to be equal to the derivative of the union of the two functions. If 𝐴 and 𝐵 are open sets, this condition (dvun.n) is satisfied by isopn3i 22985. (Contributed by SN, 30-Sep-2025.)
⊢ 𝐽 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐺:𝐵⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑆)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → (((int‘𝐽)‘𝐴) ∪ ((int‘𝐽)‘𝐵)) = ((int‘𝐽)‘(𝐴 ∪ 𝐵)))    ⇒   ⊢ (𝜑 → ((𝑆 D 𝐹) ∪ (𝑆 D 𝐺)) = (𝑆 D (𝐹 ∪ 𝐺)))
Theorem	redvmptabs 42333*	The derivative of the absolute value, for real numbers. (Contributed by SN, 30-Sep-2025.)
⊢ 𝐷 = (ℝ ∖ {0})    ⇒   ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (abs‘𝑥))) = (𝑥 ∈ 𝐷 ↦ if(𝑥 < 0, -1, 1))
Theorem	readvrec2 42334*	The antiderivative of 1/x in real numbers, without using the absolute value function. (Contributed by SN, 1-Oct-2025.)
⊢ 𝐷 = (ℝ ∖ {0})    ⇒   ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ ((log‘(𝑥↑2)) / 2))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥))
Theorem	readvrec 42335*	For real numbers, the antiderivative of 1/x is ln|x|. (Contributed by SN, 30-Sep-2025.)
⊢ 𝐷 = (ℝ ∖ {0})    ⇒   ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (log‘(abs‘𝑥)))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥))
Theorem	resuppsinopn 42336	The support of sin (df-supp 8101) restricted to the reals is an open set. (Contributed by SN, 7-Oct-2025.)
⊢ 𝐷 = {𝑦 ∈ ℝ ∣ (sin‘𝑦) ≠ 0}    ⇒   ⊢ 𝐷 ∈ (topGen‘ran (,))
Theorem	readvcot 42337*	Real antiderivative of cotangent. (Contributed by SN, 7-Oct-2025.)
⊢ 𝐷 = {𝑦 ∈ ℝ ∣ (sin‘𝑦) ≠ 0}    ⇒   ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (log‘(abs‘(sin‘𝑥))))) = (𝑥 ∈ 𝐷 ↦ ((cos‘𝑥) / (sin‘𝑥)))
21.30.5  Independence of ax-mulcom This section mainly concerns the independence of ax-mulcom 11092, which is the only real and complex number axiom whose independence is open ( https://us.metamath.org/mpeuni/mmcomplex.html 11092). In particular, this is a combination of attempts to prove more and more properties of real and complex numbers without ax-mulcom 11092. Completing this direction would show that ax-mulcom 11092 is not independent. Alternatively, one could search for a model satisfying all axioms except ax-mulcom 11092, thus showing it is independent. A few models satisfying non-commutativity which only violate one other axiom are provided at https://gist.github.com/icecream17/933f95d820e0b8f1cab0d4293b68eaf9 11092. I conjecture that if it is possible to prove ax-mulcom 11092 from the other axioms, then all the other axioms are needed. In abstract terms, the symbol ℝ would have to correspond to an infinite non-commutative left-near-field with a Dedekind-complete order compatible with its ring operations. (Note: https://en.wikipedia.org/wiki/Near-field_(mathematics) 11092 does not require commutativity despite having "field" in the name.) Needless to say, this is a very undeveloped area of math. In addition, such a structure for ℝ would have to, together with the structure for the symbol ℂ, satisfy ax-resscn 11085, ax-icn 11087, ax-i2m1 11096, and most crucially ax-cnre 11101. None of the theorems in this section should be moved to main. If there is a naming conflict, feel free to add the prefix "sn-".
Syntax	cresub 42338	Real number subtraction.
class −ℝ
Definition	df-resub 42339*	Define subtraction between real numbers. This operator saves a few axioms over df-sub 11367 in certain situations. Theorem resubval 42340 shows its value, resubadd 42352 relates it to addition, and rersubcl 42351 proves its closure. It is the restriction of df-sub 11367 to the reals: subresre 42404. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ −ℝ = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (℩𝑧 ∈ ℝ (𝑦 + 𝑧) = 𝑥))
Theorem	resubval 42340*	Value of real subtraction, which is the (unique) real 𝑥 such that 𝐵 + 𝑥 = 𝐴. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (℩𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴))
Theorem	renegeulemv 42341*	Lemma for renegeu 42343 and similar. Derive existential uniqueness from existence. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴)
Theorem	renegeulem 42342*	Lemma for renegeu 42343 and similar. Remove a change in bound variables from renegeulemv 42341. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴)    ⇒   ⊢ (𝜑 → ∃!𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴)
Theorem	renegeu 42343*	Existential uniqueness of real negatives. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
Theorem	rernegcl 42344	Closure law for negative reals. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ (𝐴 ∈ ℝ → (0 −ℝ 𝐴) ∈ ℝ)
Theorem	renegadd 42345	Relationship between real negation and addition. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 −ℝ 𝐴) = 𝐵 ↔ (𝐴 + 𝐵) = 0))
Theorem	renegid 42346	Addition of a real number and its negative. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ (𝐴 ∈ ℝ → (𝐴 + (0 −ℝ 𝐴)) = 0)
Theorem	reneg0addlid 42347	Negative zero is a left additive identity. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ (𝐴 ∈ ℝ → ((0 −ℝ 0) + 𝐴) = 𝐴)
Theorem	resubeulem1 42348	Lemma for resubeu 42350. 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 42349	Lemma for resubeu 42350. A value which when added to 𝐴, results in 𝐵. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + ((0 −ℝ 𝐴) + ((0 −ℝ (0 + 0)) + 𝐵))) = 𝐵)
Theorem	resubeu 42350*	Existential uniqueness of real differences. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 𝐵)
Theorem	rersubcl 42351	Closure for real subtraction. Based on subcl 11380. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) ∈ ℝ)
Theorem	resubadd 42352	Relation between real subtraction and addition. Based on subadd 11384. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴))
Theorem	resubaddd 42353	Relationship between subtraction and addition. Based on subaddd 11511. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴))
Theorem	resubf 42354	Real subtraction is an operation on the real numbers. Based on subf 11383. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ −ℝ :(ℝ × ℝ)⟶ℝ
Theorem	repncan2 42355	Addition and subtraction of equals. Compare pncan2 11388. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐴) = 𝐵)
Theorem	repncan3 42356	Addition and subtraction of equals. Based on pncan3 11389. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + (𝐵 −ℝ 𝐴)) = 𝐵)
Theorem	readdsub 42357	Law for addition and subtraction. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐶) = ((𝐴 −ℝ 𝐶) + 𝐵))
Theorem	reladdrsub 42358	Move LHS of a sum into RHS of a (real) difference. Version of mvlladdd 11549 with real subtraction. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 = (𝐶 −ℝ 𝐴))
Theorem	reltsub1 42359	Subtraction from both sides of 'less than'. Compare ltsub1 11634. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 −ℝ 𝐶) < (𝐵 −ℝ 𝐶)))
Theorem	reltsubadd2 42360	'Less than' relationship between addition and subtraction. Compare ltsubadd2 11609. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶)))
Theorem	resubcan2 42361	Cancellation law for real subtraction. Compare subcan2 11407. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) = (𝐵 −ℝ 𝐶) ↔ 𝐴 = 𝐵))
Theorem	resubsub4 42362	Law for double subtraction. Compare subsub4 11415. (Contributed by Steven Nguyen, 14-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) −ℝ 𝐶) = (𝐴 −ℝ (𝐵 + 𝐶)))
Theorem	rennncan2 42363	Cancellation law for real subtraction. Compare nnncan2 11419. (Contributed by Steven Nguyen, 14-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) −ℝ (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐵))
Theorem	renpncan3 42364	Cancellation law for real subtraction. Compare npncan3 11420. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) + (𝐶 −ℝ 𝐴)) = (𝐶 −ℝ 𝐵))
Theorem	repnpcan 42365	Cancellation law for addition and real subtraction. Compare pnpcan 11421. (Contributed by Steven Nguyen, 19-May-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ (𝐴 + 𝐶)) = (𝐵 −ℝ 𝐶))
Theorem	reppncan 42366	Cancellation law for mixed addition and real subtraction. Compare ppncan 11424. (Contributed by SN, 3-Sep-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) + (𝐵 −ℝ 𝐶)) = (𝐴 + 𝐵))
Theorem	resubidaddlidlem 42367	Lemma for resubidaddlid 42368. A special case of npncan 11403. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 −ℝ 𝐵) = (𝐵 −ℝ 𝐶))    ⇒   ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) + (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐶))
Theorem	resubidaddlid 42368	Any real number subtracted from itself forms a left additive identity. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 −ℝ 𝐴) + 𝐵) = 𝐵)
Theorem	resubdi 42369	Distribution of multiplication over real subtraction. (Contributed by Steven Nguyen, 3-Jun-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐵 −ℝ 𝐶)) = ((𝐴 · 𝐵) −ℝ (𝐴 · 𝐶)))
Theorem	re1m1e0m0 42370	Equality of two left-additive identities. See resubidaddlid 42368. Uses ax-i2m1 11096. (Contributed by SN, 25-Dec-2023.)
⊢ (1 −ℝ 1) = (0 −ℝ 0)
Theorem	sn-00idlem1 42371	Lemma for sn-00id 42374. (Contributed by SN, 25-Dec-2023.)
⊢ (𝐴 ∈ ℝ → (𝐴 · (0 −ℝ 0)) = (𝐴 −ℝ 𝐴))
Theorem	sn-00idlem2 42372	Lemma for sn-00id 42374. (Contributed by SN, 25-Dec-2023.)
⊢ ((0 −ℝ 0) ≠ 0 → (0 −ℝ 0) = 1)
Theorem	sn-00idlem3 42373	Lemma for sn-00id 42374. (Contributed by SN, 25-Dec-2023.)
⊢ ((0 −ℝ 0) = 1 → (0 + 0) = 0)
Theorem	sn-00id 42374	00id 11309 proven without ax-mulcom 11092 but using ax-1ne0 11097. (Though note that the current version of 00id 11309 can be changed to avoid ax-icn 11087, ax-addcl 11088, ax-mulcl 11090, ax-i2m1 11096, ax-cnre 11101. Most of this is by using 0cnALT3 42226 instead of 0cn 11126). (Contributed by SN, 25-Dec-2023.) (Proof modification is discouraged.)
⊢ (0 + 0) = 0
Theorem	re0m0e0 42375	Real number version of 0m0e0 12261 proven without ax-mulcom 11092. (Contributed by SN, 23-Jan-2024.)
⊢ (0 −ℝ 0) = 0
Theorem	readdlid 42376	Real number version of addlid 11317. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (0 + 𝐴) = 𝐴)
Theorem	sn-addlid 42377	addlid 11317 without ax-mulcom 11092. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
Theorem	remul02 42378	Real number version of mul02 11312 proven without ax-mulcom 11092. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (0 · 𝐴) = 0)
Theorem	sn-0ne2 42379	0ne2 12348 without ax-mulcom 11092. (Contributed by SN, 23-Jan-2024.)
⊢ 0 ≠ 2
Theorem	remul01 42380	Real number version of mul01 11313 proven without ax-mulcom 11092. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 · 0) = 0)
Theorem	sn-remul0ord 42381	A product is zero iff one of its factors are zero. (Contributed by SN, 24-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) = 0 ↔ (𝐴 = 0 ∨ 𝐵 = 0)))
Theorem	resubid 42382	Subtraction of a real number from itself (compare subid 11401). (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 𝐴) = 0)
Theorem	readdrid 42383	Real number version of addrid 11314 without ax-mulcom 11092. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 + 0) = 𝐴)
Theorem	resubid1 42384	Real number version of subid1 11402 without ax-mulcom 11092. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 0) = 𝐴)
Theorem	renegneg 42385	A real number is equal to the negative of its negative. Compare negneg 11432. (Contributed by SN, 13-Feb-2024.)
⊢ (𝐴 ∈ ℝ → (0 −ℝ (0 −ℝ 𝐴)) = 𝐴)
Theorem	readdcan2 42386	Commuted version of readdcan 11308 without ax-mulcom 11092. (Contributed by SN, 21-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵))
Theorem	renegid2 42387	Commuted version of renegid 42346. (Contributed by SN, 4-May-2024.)
⊢ (𝐴 ∈ ℝ → ((0 −ℝ 𝐴) + 𝐴) = 0)
Theorem	remulneg2d 42388	Product with negative is negative of product. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 · (0 −ℝ 𝐵)) = (0 −ℝ (𝐴 · 𝐵)))
Theorem	sn-it0e0 42389	Proof of it0e0 12365 without ax-mulcom 11092. Informally, a real number times 0 is 0, and ∃𝑟 ∈ ℝ𝑟 = i · 𝑠 by ax-cnre 11101 and renegid2 42387. (Contributed by SN, 30-Apr-2024.)
⊢ (i · 0) = 0
Theorem	sn-negex12 42390*	A combination of cnegex 11315 and cnegex2 11316, this proof takes cnre 11131 𝐴 = 𝑟 + i · 𝑠 and shows that i · -𝑠 + -𝑟 is both a left and right inverse. (Contributed by SN, 5-May-2024.) (Proof shortened by SN, 4-Jul-2025.)
⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ ((𝐴 + 𝑏) = 0 ∧ (𝑏 + 𝐴) = 0))
Theorem	sn-negex 42391*	Proof of cnegex 11315 without ax-mulcom 11092. (Contributed by SN, 30-Apr-2024.)
⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝐴 + 𝑏) = 0)
Theorem	sn-negex2 42392*	Proof of cnegex2 11316 without ax-mulcom 11092. (Contributed by SN, 5-May-2024.)
⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝑏 + 𝐴) = 0)
Theorem	sn-addcand 42393	addcand 11337 without ax-mulcom 11092. Note how the proof is almost identical to addcan 11318. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶))
Theorem	sn-addrid 42394	addrid 11314 without ax-mulcom 11092. (Contributed by SN, 5-May-2024.)
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
Theorem	sn-addcan2d 42395	addcan2d 11338 without ax-mulcom 11092. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵))
Theorem	reixi 42396	ixi 11767 without ax-mulcom 11092. (Contributed by SN, 5-May-2024.)
⊢ (i · i) = (0 −ℝ 1)
Theorem	rei4 42397	i4 14129 without ax-mulcom 11092. (Contributed by SN, 27-May-2024.)
⊢ ((i · i) · (i · i)) = 1
Theorem	sn-addid0 42398	A number that sums to itself is zero. Compare addid0 11557, readdridaddlidd 42231. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐴) = 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	sn-mul01 42399	mul01 11313 without ax-mulcom 11092. (Contributed by SN, 5-May-2024.)
⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0)
Theorem	sn-subeu 42400*	negeu 11371 without ax-mulcom 11092 and complex number version of resubeu 42350. (Contributed by SN, 5-May-2024.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐴 + 𝑥) = 𝐵)