P. 433 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43201-43300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	expeq1d 43201	A nonnegative real number is one if and only if it is one when raised to a positive integer. (Contributed by SN, 3-Jul-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → ((𝐴↑𝑁) = 1 ↔ 𝐴 = 1))
Theorem	expeqidd 43202	A nonnegative real number is zero or one if and only if it is itself when raised to an integer greater than one. (Contributed by SN, 3-Jul-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → ((𝐴↑𝑁) = 𝐴 ↔ (𝐴 = 0 ∨ 𝐴 = 1)))
Theorem	exp11d 43203	exp11nnd 14327 for nonzero integer exponents. (Contributed by SN, 14-Sep-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ≠ 0)    &   ⊢ (𝜑 → (𝐴↑𝑁) = (𝐵↑𝑁))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	0dvds0 43204	0 divides 0. (Contributed by SN, 15-Sep-2024.)
⊢ 0 ∥ 0
Theorem	absdvdsabsb 43205	Divisibility is invariant under taking the absolute value on both sides. (Contributed by SN, 15-Sep-2024.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) ∥ (abs‘𝑁)))
Theorem	gcdnn0id 43206	The gcd of a nonnegative integer and itself is the integer. (Contributed by SN, 25-Aug-2024.)
⊢ (𝑁 ∈ ℕ0 → (𝑁 gcd 𝑁) = 𝑁)
Theorem	gcdle1d 43207	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 43208	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 43209	Deduction associated with dvdsexpim 16649. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∥ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ∥ (𝐵↑𝑁))
Theorem	dvdsexpnn 43210	dvdssqlem 16660 generalized to positive integer exponents. (Contributed by SN, 20-Aug-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))
Theorem	dvdsexpnn0 43211	dvdsexpnn 43210 generalized to include zero bases. (Contributed by SN, 15-Sep-2024.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))
Theorem	dvdsexpb 43212	dvdssq 16661 generalized to positive integer exponents. (Contributed by SN, 15-Sep-2024.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))
Theorem	posqsqznn 43213	When a positive rational squared is an integer, the rational is a positive integer. zsqrtelqelz 16853 with all terms squared and positive. (Contributed by SN, 23-Aug-2024.)
⊢ (𝜑 → (𝐴↑2) ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ ℚ)    &   ⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℕ)
Theorem	zdivgd 43214*	Two ways to express "𝑁 is an integer multiple of 𝑀". Originally a subproof of zdiv 12694. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℂ)    &   ⊢ (𝜑 → 𝑀 ≠ 0)    ⇒   ⊢ (𝜑 → (∃𝑘 ∈ ℤ (𝑀 · 𝑘) = 𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ))
Theorem	efsubd 43215	Difference of exponents law for exponential function, deduction form. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (exp‘(𝐴 − 𝐵)) = ((exp‘𝐴) / (exp‘𝐵)))
Theorem	ef11d 43216*	General condition for the exponential function to be one-to-one. efper 26717 shows that exponentiation is periodic. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((exp‘𝐴) = (exp‘𝐵) ↔ ∃𝑛 ∈ ℤ 𝐴 = (𝐵 + ((i · (2 · π)) · 𝑛))))
Theorem	logccne0d 43217	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 43218*	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 43219*	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 43220*	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 43221	Deduction form of logne0 26817. See logccne0d 43217 for a more general version. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 ≠ 1)    ⇒   ⊢ (𝜑 → (log‘𝐴) ≠ 0)
Theorem	rxp112d 43222	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 43223	The natural logarithm is one-to-one. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((log‘𝐴) = (log‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	rplog11d 43224	The natural logarithm is one-to-one on positive reals. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((log‘𝐴) = (log‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	rxp11d 43225	Real exponentiation is one-to-one with respect to the first argument. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    &   ⊢ (𝜑 → (𝐴↑𝑐𝐶) = (𝐵↑𝑐𝐶))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
21.32.4  Trigonometry and Calculus
Theorem	tanhalfpim 43226	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 43227	Sine of a number subtracted from π. (Contributed by SN, 19-Nov-2025.)
⊢ (𝐴 ∈ ℂ → (sin‘(π − 𝐴)) = (sin‘𝐴))
Theorem	cospim 43228	Cosine of a number subtracted from π. (Contributed by SN, 19-Nov-2025.)
⊢ (𝐴 ∈ ℂ → (cos‘(π − 𝐴)) = -(cos‘𝐴))
Theorem	tan3rdpi 43229	The tangent of π / 3 is √3. (Contributed by SN, 2-Sep-2025.)
⊢ (tan‘(π / 3)) = (√‘3)
Theorem	sin2t3rdpi 43230	The sine of 2 · (π / 3) is (√3) / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (sin‘(2 · (π / 3))) = ((√‘3) / 2)
Theorem	cos2t3rdpi 43231	The cosine of 2 · (π / 3) is -1 / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (cos‘(2 · (π / 3))) = -(1 / 2)
Theorem	sin4t3rdpi 43232	The sine of 4 · (π / 3) is -(√3) / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (sin‘(4 · (π / 3))) = -((√‘3) / 2)
Theorem	cos4t3rdpi 43233	The cosine of 4 · (π / 3) is -1 / 2. (Contributed by SN, 19-Nov-2025.)
⊢ (cos‘(4 · (π / 3))) = -(1 / 2)
Theorem	asin1half 43234	The arcsine of 1 / 2 is π / 6. (Contributed by SN, 31-Aug-2025.)
⊢ (arcsin‘(1 / 2)) = (π / 6)
Theorem	acos1half 43235	The arccosine of 1 / 2 is π / 3. (Contributed by SN, 31-Aug-2024.)
⊢ (arccos‘(1 / 2)) = (π / 3)
Theorem	dvun 43236	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 23311. (Contributed by SN, 30-Sep-2025.)
⊢ 𝐽 = (𝐾 ↾t 𝑆)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐺:𝐵⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑆)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → (((int‘𝐽)‘𝐴) ∪ ((int‘𝐽)‘𝐵)) = ((int‘𝐽)‘(𝐴 ∪ 𝐵)))    ⇒   ⊢ (𝜑 → ((𝑆 D 𝐹) ∪ (𝑆 D 𝐺)) = (𝑆 D (𝐹 ∪ 𝐺)))
Theorem	redvmptabs 43237*	The derivative of the absolute value, for real numbers. (Contributed by SN, 30-Sep-2025.)
⊢ 𝐷 = (ℝ ∖ {0})    ⇒   ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (abs‘𝑥))) = (𝑥 ∈ 𝐷 ↦ if(𝑥 < 0, -1, 1))
Theorem	readvrec2 43238*	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 43239*	For real numbers, the antiderivative of 1/x is ln|x|. (Contributed by SN, 30-Sep-2025.)
⊢ 𝐷 = (ℝ ∖ {0})    ⇒   ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (log‘(abs‘𝑥)))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥))
Theorem	resuppsinopn 43240	The support of sin (df-supp 8162) restricted to the reals is an open set. (Contributed by SN, 7-Oct-2025.)
⊢ 𝐷 = {𝑦 ∈ ℝ ∣ (sin‘𝑦) ≠ 0}    ⇒   ⊢ 𝐷 ∈ (topGen‘ran (,))
Theorem	readvcot 43241*	Real antiderivative of cotangent. (Contributed by SN, 7-Oct-2025.)
⊢ 𝐷 = {𝑦 ∈ ℝ ∣ (sin‘𝑦) ≠ 0}    ⇒   ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (log‘(abs‘(sin‘𝑥))))) = (𝑥 ∈ 𝐷 ↦ ((cos‘𝑥) / (sin‘𝑥)))
21.32.5  Independence of ax-mulcom This section mainly concerns the independence of ax-mulcom 11191, which is the only real and complex number axiom whose independence is open ( https://us.metamath.org/mpeuni/mmcomplex.html 11191). In particular, this is a combination of attempts to prove more and more properties of real and complex numbers without ax-mulcom 11191. Completing this direction would show that ax-mulcom 11191 is not independent. Alternatively, one could search for a model satisfying all axioms except ax-mulcom 11191, 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 11191. I conjecture that if it is possible to prove ax-mulcom 11191 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) 11191 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 11184, ax-icn 11186, ax-i2m1 11195, and most crucially ax-cnre 11200. 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 43242	Real number subtraction.
class −ℝ
Definition	df-resub 43243*	Define subtraction between real numbers. This operator saves a few axioms over df-sub 11470 in certain situations. Theorem resubval 43244 shows its value, resubadd 43256 relates it to addition, and rersubcl 43255 proves its closure. It is the restriction of df-sub 11470 to the reals: subresre 43308. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ −ℝ = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (℩𝑧 ∈ ℝ (𝑦 + 𝑧) = 𝑥))
Theorem	resubval 43244*	Value of real subtraction, which is the (unique) real 𝑥 such that 𝐵 + 𝑥 = 𝐴. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (℩𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴))
Theorem	renegeulemv 43245*	Lemma for renegeu 43247 and similar. Derive existential uniqueness from existence. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴)
Theorem	renegeulem 43246*	Lemma for renegeu 43247 and similar. Remove a change in bound variables from renegeulemv 43245. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴)    ⇒   ⊢ (𝜑 → ∃!𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴)
Theorem	renegeu 43247*	Existential uniqueness of real negatives. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
Theorem	rernegcl 43248	Closure law for negative reals. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ (𝐴 ∈ ℝ → (0 −ℝ 𝐴) ∈ ℝ)
Theorem	renegadd 43249	Relationship between real negation and addition. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 −ℝ 𝐴) = 𝐵 ↔ (𝐴 + 𝐵) = 0))
Theorem	renegid 43250	Addition of a real number and its negative. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ (𝐴 ∈ ℝ → (𝐴 + (0 −ℝ 𝐴)) = 0)
Theorem	reneg0addlid 43251	Negative zero is a left additive identity. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ (𝐴 ∈ ℝ → ((0 −ℝ 0) + 𝐴) = 𝐴)
Theorem	resubeulem1 43252	Lemma for resubeu 43254. 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 43253	Lemma for resubeu 43254. A value which when added to 𝐴, results in 𝐵. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + ((0 −ℝ 𝐴) + ((0 −ℝ (0 + 0)) + 𝐵))) = 𝐵)
Theorem	resubeu 43254*	Existential uniqueness of real differences. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 𝐵)
Theorem	rersubcl 43255	Closure for real subtraction. Based on subcl 11483. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) ∈ ℝ)
Theorem	resubadd 43256	Relation between real subtraction and addition. Based on subadd 11487. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴))
Theorem	resubaddd 43257	Relationship between subtraction and addition. Based on subaddd 11614. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴))
Theorem	resubf 43258	Real subtraction is an operation on the real numbers. Based on subf 11486. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ −ℝ :(ℝ × ℝ)⟶ℝ
Theorem	repncan2 43259	Addition and subtraction of equals. Compare pncan2 11491. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐴) = 𝐵)
Theorem	repncan3 43260	Addition and subtraction of equals. Based on pncan3 11492. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + (𝐵 −ℝ 𝐴)) = 𝐵)
Theorem	readdsub 43261	Law for addition and subtraction. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐶) = ((𝐴 −ℝ 𝐶) + 𝐵))
Theorem	reladdrsub 43262	Move LHS of a sum into RHS of a (real) difference. Version of mvlladdd 11652 with real subtraction. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 = (𝐶 −ℝ 𝐴))
Theorem	reltsub1 43263	Subtraction from both sides of 'less than'. Compare ltsub1 11737. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 −ℝ 𝐶) < (𝐵 −ℝ 𝐶)))
Theorem	reltsubadd2 43264	'Less than' relationship between addition and subtraction. Compare ltsubadd2 11712. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶)))
Theorem	resubcan2 43265	Cancellation law for real subtraction. Compare subcan2 11510. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) = (𝐵 −ℝ 𝐶) ↔ 𝐴 = 𝐵))
Theorem	resubsub4 43266	Law for double subtraction. Compare subsub4 11518. (Contributed by Steven Nguyen, 14-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) −ℝ 𝐶) = (𝐴 −ℝ (𝐵 + 𝐶)))
Theorem	rennncan2 43267	Cancellation law for real subtraction. Compare nnncan2 11522. (Contributed by Steven Nguyen, 14-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) −ℝ (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐵))
Theorem	renpncan3 43268	Cancellation law for real subtraction. Compare npncan3 11523. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) + (𝐶 −ℝ 𝐴)) = (𝐶 −ℝ 𝐵))
Theorem	repnpcan 43269	Cancellation law for addition and real subtraction. Compare pnpcan 11524. (Contributed by Steven Nguyen, 19-May-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ (𝐴 + 𝐶)) = (𝐵 −ℝ 𝐶))
Theorem	reppncan 43270	Cancellation law for mixed addition and real subtraction. Compare ppncan 11527. (Contributed by SN, 3-Sep-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) + (𝐵 −ℝ 𝐶)) = (𝐴 + 𝐵))
Theorem	resubidaddlidlem 43271	Lemma for resubidaddlid 43272. A special case of npncan 11506. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 −ℝ 𝐵) = (𝐵 −ℝ 𝐶))    ⇒   ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) + (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐶))
Theorem	resubidaddlid 43272	Any real number subtracted from itself forms a left additive identity. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 −ℝ 𝐴) + 𝐵) = 𝐵)
Theorem	resubdi 43273	Distribution of multiplication over real subtraction. (Contributed by Steven Nguyen, 3-Jun-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐵 −ℝ 𝐶)) = ((𝐴 · 𝐵) −ℝ (𝐴 · 𝐶)))
Theorem	re1m1e0m0 43274	Equality of two left-additive identities. See resubidaddlid 43272. Uses ax-i2m1 11195. (Contributed by SN, 25-Dec-2023.)
⊢ (1 −ℝ 1) = (0 −ℝ 0)
Theorem	sn-00idlem1 43275	Lemma for sn-00id 43278. (Contributed by SN, 25-Dec-2023.)
⊢ (𝐴 ∈ ℝ → (𝐴 · (0 −ℝ 0)) = (𝐴 −ℝ 𝐴))
Theorem	sn-00idlem2 43276	Lemma for sn-00id 43278. (Contributed by SN, 25-Dec-2023.)
⊢ ((0 −ℝ 0) ≠ 0 → (0 −ℝ 0) = 1)
Theorem	sn-00idlem3 43277	Lemma for sn-00id 43278. (Contributed by SN, 25-Dec-2023.)
⊢ ((0 −ℝ 0) = 1 → (0 + 0) = 0)
Theorem	sn-00id 43278	00id 11412 proven without ax-mulcom 11191 but using ax-1ne0 11196. (Though note that the current version of 00id 11412 can be changed to avoid ax-icn 11186, ax-addcl 11187, ax-mulcl 11189, ax-i2m1 11195, ax-cnre 11200. Most of this is by using 0cnALT3 43122 instead of 0cn 11225). (Contributed by SN, 25-Dec-2023.) (Proof modification is discouraged.)
⊢ (0 + 0) = 0
Theorem	re0m0e0 43279	Real number version of 0m0e0 12386 proven without ax-mulcom 11191. (Contributed by SN, 23-Jan-2024.)
⊢ (0 −ℝ 0) = 0
Theorem	readdlid 43280	Real number version of addlid 11420. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (0 + 𝐴) = 𝐴)
Theorem	sn-addlid 43281	addlid 11420 without ax-mulcom 11191. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
Theorem	remul02 43282	Real number version of mul02 11415 proven without ax-mulcom 11191. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (0 · 𝐴) = 0)
Theorem	sn-0ne2 43283	0ne2 12477 without ax-mulcom 11191. (Contributed by SN, 23-Jan-2024.)
⊢ 0 ≠ 2
Theorem	remul01 43284	Real number version of mul01 11416 proven without ax-mulcom 11191. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 · 0) = 0)
Theorem	sn-remul0ord 43285	A product is zero iff one of its factors are zero. (Contributed by SN, 24-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) = 0 ↔ (𝐴 = 0 ∨ 𝐵 = 0)))
Theorem	resubid 43286	Subtraction of a real number from itself (compare subid 11504). (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 𝐴) = 0)
Theorem	readdrid 43287	Real number version of addrid 11417 without ax-mulcom 11191. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 + 0) = 𝐴)
Theorem	resubid1 43288	Real number version of subid1 11505 without ax-mulcom 11191. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 0) = 𝐴)
Theorem	renegneg 43289	A real number is equal to the negative of its negative. Compare negneg 11535. (Contributed by SN, 13-Feb-2024.)
⊢ (𝐴 ∈ ℝ → (0 −ℝ (0 −ℝ 𝐴)) = 𝐴)
Theorem	readdcan2 43290	Commuted version of readdcan 11411 without ax-mulcom 11191. (Contributed by SN, 21-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵))
Theorem	renegid2 43291	Commuted version of renegid 43250. (Contributed by SN, 4-May-2024.)
⊢ (𝐴 ∈ ℝ → ((0 −ℝ 𝐴) + 𝐴) = 0)
Theorem	remulneg2d 43292	Product with negative is negative of product. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 · (0 −ℝ 𝐵)) = (0 −ℝ (𝐴 · 𝐵)))
Theorem	sn-it0e0 43293	Proof of it0e0 12494 without ax-mulcom 11191. Informally, a real number times 0 is 0, and ∃𝑟 ∈ ℝ𝑟 = i · 𝑠 by ax-cnre 11200 and renegid2 43291. (Contributed by SN, 30-Apr-2024.)
⊢ (i · 0) = 0
Theorem	sn-negex12 43294*	A combination of cnegex 11418 and cnegex2 11419, this proof takes cnre 11232 𝐴 = 𝑟 + 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 43295*	Proof of cnegex 11418 without ax-mulcom 11191. (Contributed by SN, 30-Apr-2024.)
⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝐴 + 𝑏) = 0)
Theorem	sn-negex2 43296*	Proof of cnegex2 11419 without ax-mulcom 11191. (Contributed by SN, 5-May-2024.)
⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝑏 + 𝐴) = 0)
Theorem	sn-addcand 43297	addcand 11440 without ax-mulcom 11191. Note how the proof is almost identical to addcan 11421. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶))
Theorem	sn-addrid 43298	addrid 11417 without ax-mulcom 11191. (Contributed by SN, 5-May-2024.)
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
Theorem	sn-addcan2d 43299	addcan2d 11441 without ax-mulcom 11191. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵))
Theorem	reixi 43300	ixi 11870 without ax-mulcom 11191. (Contributed by SN, 5-May-2024.)
⊢ (i · i) = (0 −ℝ 1)