P. 432 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43101-43200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	readvrec 43101*	For real numbers, the antiderivative of 1/x is ln|x|. (Contributed by SN, 30-Sep-2025.)
⊢ 𝐷 = (ℝ ∖ {0})    ⇒   ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (log‘(abs‘𝑥)))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥))
Theorem	resuppsinopn 43102	The support of sin (df-supp 8158) restricted to the reals is an open set. (Contributed by SN, 7-Oct-2025.)
⊢ 𝐷 = {𝑦 ∈ ℝ ∣ (sin‘𝑦) ≠ 0}    ⇒   ⊢ 𝐷 ∈ (topGen‘ran (,))
Theorem	readvcot 43103*	Real antiderivative of cotangent. (Contributed by SN, 7-Oct-2025.)
⊢ 𝐷 = {𝑦 ∈ ℝ ∣ (sin‘𝑦) ≠ 0}    ⇒   ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (log‘(abs‘(sin‘𝑥))))) = (𝑥 ∈ 𝐷 ↦ ((cos‘𝑥) / (sin‘𝑥)))
21.31.5  Independence of ax-mulcom This section mainly concerns the independence of ax-mulcom 11165, which is the only real and complex number axiom whose independence is open ( https://us.metamath.org/mpeuni/mmcomplex.html 11165). In particular, this is a combination of attempts to prove more and more properties of real and complex numbers without ax-mulcom 11165. Completing this direction would show that ax-mulcom 11165 is not independent. Alternatively, one could search for a model satisfying all axioms except ax-mulcom 11165, 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 11165. I conjecture that if it is possible to prove ax-mulcom 11165 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) 11165 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 11158, ax-icn 11160, ax-i2m1 11169, and most crucially ax-cnre 11174. 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 43104	Real number subtraction.
class −ℝ
Definition	df-resub 43105*	Define subtraction between real numbers. This operator saves a few axioms over df-sub 11444 in certain situations. Theorem resubval 43106 shows its value, resubadd 43118 relates it to addition, and rersubcl 43117 proves its closure. It is the restriction of df-sub 11444 to the reals: subresre 43170. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ −ℝ = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (℩𝑧 ∈ ℝ (𝑦 + 𝑧) = 𝑥))
Theorem	resubval 43106*	Value of real subtraction, which is the (unique) real 𝑥 such that 𝐵 + 𝑥 = 𝐴. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (℩𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴))
Theorem	renegeulemv 43107*	Lemma for renegeu 43109 and similar. Derive existential uniqueness from existence. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴)
Theorem	renegeulem 43108*	Lemma for renegeu 43109 and similar. Remove a change in bound variables from renegeulemv 43107. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴)    ⇒   ⊢ (𝜑 → ∃!𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴)
Theorem	renegeu 43109*	Existential uniqueness of real negatives. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
Theorem	rernegcl 43110	Closure law for negative reals. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ (𝐴 ∈ ℝ → (0 −ℝ 𝐴) ∈ ℝ)
Theorem	renegadd 43111	Relationship between real negation and addition. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 −ℝ 𝐴) = 𝐵 ↔ (𝐴 + 𝐵) = 0))
Theorem	renegid 43112	Addition of a real number and its negative. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ (𝐴 ∈ ℝ → (𝐴 + (0 −ℝ 𝐴)) = 0)
Theorem	reneg0addlid 43113	Negative zero is a left additive identity. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ (𝐴 ∈ ℝ → ((0 −ℝ 0) + 𝐴) = 𝐴)
Theorem	resubeulem1 43114	Lemma for resubeu 43116. 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 43115	Lemma for resubeu 43116. A value which when added to 𝐴, results in 𝐵. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + ((0 −ℝ 𝐴) + ((0 −ℝ (0 + 0)) + 𝐵))) = 𝐵)
Theorem	resubeu 43116*	Existential uniqueness of real differences. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 𝐵)
Theorem	rersubcl 43117	Closure for real subtraction. Based on subcl 11457. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) ∈ ℝ)
Theorem	resubadd 43118	Relation between real subtraction and addition. Based on subadd 11461. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴))
Theorem	resubaddd 43119	Relationship between subtraction and addition. Based on subaddd 11588. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴))
Theorem	resubf 43120	Real subtraction is an operation on the real numbers. Based on subf 11460. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ −ℝ :(ℝ × ℝ)⟶ℝ
Theorem	repncan2 43121	Addition and subtraction of equals. Compare pncan2 11465. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐴) = 𝐵)
Theorem	repncan3 43122	Addition and subtraction of equals. Based on pncan3 11466. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + (𝐵 −ℝ 𝐴)) = 𝐵)
Theorem	readdsub 43123	Law for addition and subtraction. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐶) = ((𝐴 −ℝ 𝐶) + 𝐵))
Theorem	reladdrsub 43124	Move LHS of a sum into RHS of a (real) difference. Version of mvlladdd 11626 with real subtraction. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 = (𝐶 −ℝ 𝐴))
Theorem	reltsub1 43125	Subtraction from both sides of 'less than'. Compare ltsub1 11711. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 −ℝ 𝐶) < (𝐵 −ℝ 𝐶)))
Theorem	reltsubadd2 43126	'Less than' relationship between addition and subtraction. Compare ltsubadd2 11686. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶)))
Theorem	resubcan2 43127	Cancellation law for real subtraction. Compare subcan2 11484. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) = (𝐵 −ℝ 𝐶) ↔ 𝐴 = 𝐵))
Theorem	resubsub4 43128	Law for double subtraction. Compare subsub4 11492. (Contributed by Steven Nguyen, 14-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) −ℝ 𝐶) = (𝐴 −ℝ (𝐵 + 𝐶)))
Theorem	rennncan2 43129	Cancellation law for real subtraction. Compare nnncan2 11496. (Contributed by Steven Nguyen, 14-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) −ℝ (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐵))
Theorem	renpncan3 43130	Cancellation law for real subtraction. Compare npncan3 11497. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) + (𝐶 −ℝ 𝐴)) = (𝐶 −ℝ 𝐵))
Theorem	repnpcan 43131	Cancellation law for addition and real subtraction. Compare pnpcan 11498. (Contributed by Steven Nguyen, 19-May-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ (𝐴 + 𝐶)) = (𝐵 −ℝ 𝐶))
Theorem	reppncan 43132	Cancellation law for mixed addition and real subtraction. Compare ppncan 11501. (Contributed by SN, 3-Sep-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) + (𝐵 −ℝ 𝐶)) = (𝐴 + 𝐵))
Theorem	resubidaddlidlem 43133	Lemma for resubidaddlid 43134. A special case of npncan 11480. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 −ℝ 𝐵) = (𝐵 −ℝ 𝐶))    ⇒   ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) + (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐶))
Theorem	resubidaddlid 43134	Any real number subtracted from itself forms a left additive identity. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 −ℝ 𝐴) + 𝐵) = 𝐵)
Theorem	resubdi 43135	Distribution of multiplication over real subtraction. (Contributed by Steven Nguyen, 3-Jun-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐵 −ℝ 𝐶)) = ((𝐴 · 𝐵) −ℝ (𝐴 · 𝐶)))
Theorem	re1m1e0m0 43136	Equality of two left-additive identities. See resubidaddlid 43134. Uses ax-i2m1 11169. (Contributed by SN, 25-Dec-2023.)
⊢ (1 −ℝ 1) = (0 −ℝ 0)
Theorem	sn-00idlem1 43137	Lemma for sn-00id 43140. (Contributed by SN, 25-Dec-2023.)
⊢ (𝐴 ∈ ℝ → (𝐴 · (0 −ℝ 0)) = (𝐴 −ℝ 𝐴))
Theorem	sn-00idlem2 43138	Lemma for sn-00id 43140. (Contributed by SN, 25-Dec-2023.)
⊢ ((0 −ℝ 0) ≠ 0 → (0 −ℝ 0) = 1)
Theorem	sn-00idlem3 43139	Lemma for sn-00id 43140. (Contributed by SN, 25-Dec-2023.)
⊢ ((0 −ℝ 0) = 1 → (0 + 0) = 0)
Theorem	sn-00id 43140	00id 11386 proven without ax-mulcom 11165 but using ax-1ne0 11170. (Though note that the current version of 00id 11386 can be changed to avoid ax-icn 11160, ax-addcl 11161, ax-mulcl 11163, ax-i2m1 11169, ax-cnre 11174. Most of this is by using 0cnALT3 42999 instead of 0cn 11199). (Contributed by SN, 25-Dec-2023.) (Proof modification is discouraged.)
⊢ (0 + 0) = 0
Theorem	re0m0e0 43141	Real number version of 0m0e0 12360 proven without ax-mulcom 11165. (Contributed by SN, 23-Jan-2024.)
⊢ (0 −ℝ 0) = 0
Theorem	readdlid 43142	Real number version of addlid 11394. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (0 + 𝐴) = 𝐴)
Theorem	sn-addlid 43143	addlid 11394 without ax-mulcom 11165. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
Theorem	remul02 43144	Real number version of mul02 11389 proven without ax-mulcom 11165. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (0 · 𝐴) = 0)
Theorem	sn-0ne2 43145	0ne2 12451 without ax-mulcom 11165. (Contributed by SN, 23-Jan-2024.)
⊢ 0 ≠ 2
Theorem	remul01 43146	Real number version of mul01 11390 proven without ax-mulcom 11165. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 · 0) = 0)
Theorem	sn-remul0ord 43147	A product is zero iff one of its factors are zero. (Contributed by SN, 24-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) = 0 ↔ (𝐴 = 0 ∨ 𝐵 = 0)))
Theorem	resubid 43148	Subtraction of a real number from itself (compare subid 11478). (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 𝐴) = 0)
Theorem	readdrid 43149	Real number version of addrid 11391 without ax-mulcom 11165. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 + 0) = 𝐴)
Theorem	resubid1 43150	Real number version of subid1 11479 without ax-mulcom 11165. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 0) = 𝐴)
Theorem	renegneg 43151	A real number is equal to the negative of its negative. Compare negneg 11509. (Contributed by SN, 13-Feb-2024.)
⊢ (𝐴 ∈ ℝ → (0 −ℝ (0 −ℝ 𝐴)) = 𝐴)
Theorem	readdcan2 43152	Commuted version of readdcan 11385 without ax-mulcom 11165. (Contributed by SN, 21-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵))
Theorem	renegid2 43153	Commuted version of renegid 43112. (Contributed by SN, 4-May-2024.)
⊢ (𝐴 ∈ ℝ → ((0 −ℝ 𝐴) + 𝐴) = 0)
Theorem	remulneg2d 43154	Product with negative is negative of product. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 · (0 −ℝ 𝐵)) = (0 −ℝ (𝐴 · 𝐵)))
Theorem	sn-it0e0 43155	Proof of it0e0 12468 without ax-mulcom 11165. Informally, a real number times 0 is 0, and ∃𝑟 ∈ ℝ𝑟 = i · 𝑠 by ax-cnre 11174 and renegid2 43153. (Contributed by SN, 30-Apr-2024.)
⊢ (i · 0) = 0
Theorem	sn-negex12 43156*	A combination of cnegex 11392 and cnegex2 11393, this proof takes cnre 11206 𝐴 = 𝑟 + 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 43157*	Proof of cnegex 11392 without ax-mulcom 11165. (Contributed by SN, 30-Apr-2024.)
⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝐴 + 𝑏) = 0)
Theorem	sn-negex2 43158*	Proof of cnegex2 11393 without ax-mulcom 11165. (Contributed by SN, 5-May-2024.)
⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝑏 + 𝐴) = 0)
Theorem	sn-addcand 43159	addcand 11414 without ax-mulcom 11165. Note how the proof is almost identical to addcan 11395. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶))
Theorem	sn-addrid 43160	addrid 11391 without ax-mulcom 11165. (Contributed by SN, 5-May-2024.)
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
Theorem	sn-addcan2d 43161	addcan2d 11415 without ax-mulcom 11165. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵))
Theorem	reixi 43162	ixi 11844 without ax-mulcom 11165. (Contributed by SN, 5-May-2024.)
⊢ (i · i) = (0 −ℝ 1)
Theorem	rei4 43163	i4 14242 without ax-mulcom 11165. (Contributed by SN, 27-May-2024.)
⊢ ((i · i) · (i · i)) = 1
Theorem	sn-addid0 43164	A number that sums to itself is zero. Compare addid0 11634, readdridaddlidd 43003. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐴) = 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	sn-mul01 43165	mul01 11390 without ax-mulcom 11165. (Contributed by SN, 5-May-2024.)
⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0)
Theorem	sn-subeu 43166*	negeu 11448 without ax-mulcom 11165 and complex number version of resubeu 43116. (Contributed by SN, 5-May-2024.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐴 + 𝑥) = 𝐵)
Theorem	sn-subcl 43167	subcl 11457 without ax-mulcom 11165. (Contributed by SN, 5-May-2024.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
Theorem	sn-subf 43168	subf 11460 without ax-mulcom 11165. (Contributed by SN, 5-May-2024.)
⊢ − :(ℂ × ℂ)⟶ℂ
Theorem	resubeqsub 43169	Equivalence between real subtraction and subtraction. (Contributed by SN, 5-May-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (𝐴 − 𝐵))
Theorem	subresre 43170	Subtraction restricted to the reals. (Contributed by SN, 5-May-2024.)
⊢ −ℝ = ( − ↾ (ℝ × ℝ))
Theorem	addinvcom 43171	A number commutes with its additive inverse. Compare remulinvcom 43172. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 0)    ⇒   ⊢ (𝜑 → (𝐵 + 𝐴) = 0)
Theorem	remulinvcom 43172	A left multiplicative inverse is a right multiplicative inverse. Proven without ax-mulcom 11165. (Contributed by SN, 5-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 · 𝐵) = 1)    ⇒   ⊢ (𝜑 → (𝐵 · 𝐴) = 1)
Theorem	remullid 43173	Commuted version of ax-1rid 11171 without ax-mulcom 11165. (Contributed by SN, 5-Feb-2024.)
⊢ (𝐴 ∈ ℝ → (1 · 𝐴) = 𝐴)
Theorem	sn-1ticom 43174	Lemma for sn-mullid 43175 and sn-it1ei 43176. (Contributed by SN, 27-May-2024.)
⊢ (1 · i) = (i · 1)
Theorem	sn-mullid 43175	mullid 11208 without ax-mulcom 11165. (Contributed by SN, 27-May-2024.)
⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
Theorem	sn-it1ei 43176	it1ei 43055 without ax-mulcom 11165. (See sn-mullid 43175 for commuted version). (Contributed by SN, 1-Jun-2024.)
⊢ (i · 1) = i
Theorem	ipiiie0 43177	The multiplicative inverse of i (per i4 14242) is also its additive inverse. (Contributed by SN, 30-Jun-2024.)
⊢ (i + (i · (i · i))) = 0
Theorem	remulcand 43178	Commuted version of remulcan2d 43002 without ax-mulcom 11165. (Contributed by SN, 21-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵))
Syntax	crediv 43179	Real number division.
class /ℝ
Definition	df-rediv 43180*	Define division between real numbers. This operator saves ax-mulcom 11165 over df-div 11873 in certain situations. (Contributed by SN, 25-Nov-2025.)
⊢ /ℝ = (𝑥 ∈ ℝ, 𝑦 ∈ (ℝ ∖ {0}) ↦ (℩𝑧 ∈ ℝ (𝑦 · 𝑧) = 𝑥))
Theorem	redivvald 43181*	Value of real division, which is the (unique) real 𝑥 such that (𝐵 · 𝑥) = 𝐴. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 /ℝ 𝐵) = (℩𝑥 ∈ ℝ (𝐵 · 𝑥) = 𝐴))
Theorem	rediveud 43182*	Existential uniqueness of real quotients. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ ℝ (𝐵 · 𝑥) = 𝐴)
Theorem	sn-redivcld 43183	Closure law for real division. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 /ℝ 𝐵) ∈ ℝ)
Theorem	redivmuld 43184	Relationship between division and multiplication. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 /ℝ 𝐶) = 𝐵 ↔ (𝐶 · 𝐵) = 𝐴))
Theorem	redivmul2d 43185	Relationship between division and multiplication. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 /ℝ 𝐶) = 𝐵 ↔ 𝐴 = (𝐶 · 𝐵)))
Theorem	redivcan2d 43186	A cancellation law for division. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐵 · (𝐴 /ℝ 𝐵)) = 𝐴)
Theorem	redivcan3d 43187	A cancellation law for division. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐵 · 𝐴) /ℝ 𝐵) = 𝐴)
Theorem	rediveq0d 43188	A ratio is zero iff the numerator is zero. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 /ℝ 𝐵) = 0 ↔ 𝐴 = 0))
Theorem	redivne0bd 43189	The ratio of nonzero numbers is nonzero. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 0 ↔ (𝐴 /ℝ 𝐵) ≠ 0))
Theorem	rediveq1d 43190	Equality in terms of unit ratio. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 /ℝ 𝐵) = 1 ↔ 𝐴 = 𝐵))
Theorem	sn-rediv1d 43191	A number divided by 1 is itself. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 /ℝ 1) = 𝐴)
Theorem	sn-rediv0d 43192	Division into zero is zero. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (0 /ℝ 𝐴) = 0)
Theorem	sn-redividd 43193	A number divided by itself is 1. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 /ℝ 𝐴) = 1)
Theorem	sn-rereccld 43194	Closure law for reciprocal. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (1 /ℝ 𝐴) ∈ ℝ)
Theorem	rerecne0d 43195	The reciprocal of a nonzero number is nonzero. (Contributed by SN, 4-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (1 /ℝ 𝐴) ≠ 0)
Theorem	rerecidd 43196	Multiplication of a number and its reciprocal. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 · (1 /ℝ 𝐴)) = 1)
Theorem	rerecid2d 43197	Multiplication of a number and its reciprocal. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → ((1 /ℝ 𝐴) · 𝐴) = 1)
Theorem	rerecrecd 43198	A number is equal to the reciprocal of its reciprocal. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (1 /ℝ (1 /ℝ 𝐴)) = 𝐴)
Theorem	redivrec2d 43199	Relationship between division and reciprocal. (Contributed by SN, 9-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 /ℝ 𝐵) = ((1 /ℝ 𝐵) · 𝐴))
Theorem	rediv23d 43200	A "commutative"/associative law for division. (Contributed by SN, 9-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) /ℝ 𝐶) = ((𝐴 /ℝ 𝐶) · 𝐵))