P. 431 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43001-43100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	resubaddd 43001	Relationship between subtraction and addition. Based on subaddd 11575. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴))
Theorem	resubf 43002	Real subtraction is an operation on the real numbers. Based on subf 11447. (Contributed by Steven Nguyen, 7-Jan-2023.)
⊢ −ℝ :(ℝ × ℝ)⟶ℝ
Theorem	repncan2 43003	Addition and subtraction of equals. Compare pncan2 11452. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐴) = 𝐵)
Theorem	repncan3 43004	Addition and subtraction of equals. Based on pncan3 11453. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + (𝐵 −ℝ 𝐴)) = 𝐵)
Theorem	readdsub 43005	Law for addition and subtraction. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐶) = ((𝐴 −ℝ 𝐶) + 𝐵))
Theorem	reladdrsub 43006	Move LHS of a sum into RHS of a (real) difference. Version of mvlladdd 11613 with real subtraction. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 = (𝐶 −ℝ 𝐴))
Theorem	reltsub1 43007	Subtraction from both sides of 'less than'. Compare ltsub1 11698. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 −ℝ 𝐶) < (𝐵 −ℝ 𝐶)))
Theorem	reltsubadd2 43008	'Less than' relationship between addition and subtraction. Compare ltsubadd2 11673. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶)))
Theorem	resubcan2 43009	Cancellation law for real subtraction. Compare subcan2 11471. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) = (𝐵 −ℝ 𝐶) ↔ 𝐴 = 𝐵))
Theorem	resubsub4 43010	Law for double subtraction. Compare subsub4 11479. (Contributed by Steven Nguyen, 14-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) −ℝ 𝐶) = (𝐴 −ℝ (𝐵 + 𝐶)))
Theorem	rennncan2 43011	Cancellation law for real subtraction. Compare nnncan2 11483. (Contributed by Steven Nguyen, 14-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) −ℝ (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐵))
Theorem	renpncan3 43012	Cancellation law for real subtraction. Compare npncan3 11484. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) + (𝐶 −ℝ 𝐴)) = (𝐶 −ℝ 𝐵))
Theorem	repnpcan 43013	Cancellation law for addition and real subtraction. Compare pnpcan 11485. (Contributed by Steven Nguyen, 19-May-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ (𝐴 + 𝐶)) = (𝐵 −ℝ 𝐶))
Theorem	reppncan 43014	Cancellation law for mixed addition and real subtraction. Compare ppncan 11488. (Contributed by SN, 3-Sep-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) + (𝐵 −ℝ 𝐶)) = (𝐴 + 𝐵))
Theorem	resubidaddlidlem 43015	Lemma for resubidaddlid 43016. A special case of npncan 11467. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 −ℝ 𝐵) = (𝐵 −ℝ 𝐶))    ⇒   ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) + (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐶))
Theorem	resubidaddlid 43016	Any real number subtracted from itself forms a left additive identity. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 −ℝ 𝐴) + 𝐵) = 𝐵)
Theorem	resubdi 43017	Distribution of multiplication over real subtraction. (Contributed by Steven Nguyen, 3-Jun-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐵 −ℝ 𝐶)) = ((𝐴 · 𝐵) −ℝ (𝐴 · 𝐶)))
Theorem	re1m1e0m0 43018	Equality of two left-additive identities. See resubidaddlid 43016. Uses ax-i2m1 11156. (Contributed by SN, 25-Dec-2023.)
⊢ (1 −ℝ 1) = (0 −ℝ 0)
Theorem	sn-00idlem1 43019	Lemma for sn-00id 43022. (Contributed by SN, 25-Dec-2023.)
⊢ (𝐴 ∈ ℝ → (𝐴 · (0 −ℝ 0)) = (𝐴 −ℝ 𝐴))
Theorem	sn-00idlem2 43020	Lemma for sn-00id 43022. (Contributed by SN, 25-Dec-2023.)
⊢ ((0 −ℝ 0) ≠ 0 → (0 −ℝ 0) = 1)
Theorem	sn-00idlem3 43021	Lemma for sn-00id 43022. (Contributed by SN, 25-Dec-2023.)
⊢ ((0 −ℝ 0) = 1 → (0 + 0) = 0)
Theorem	sn-00id 43022	00id 11373 proven without ax-mulcom 11152 but using ax-1ne0 11157. (Though note that the current version of 00id 11373 can be changed to avoid ax-icn 11147, ax-addcl 11148, ax-mulcl 11150, ax-i2m1 11156, ax-cnre 11161. Most of this is by using 0cnALT3 42881 instead of 0cn 11186). (Contributed by SN, 25-Dec-2023.) (Proof modification is discouraged.)
⊢ (0 + 0) = 0
Theorem	re0m0e0 43023	Real number version of 0m0e0 12350 proven without ax-mulcom 11152. (Contributed by SN, 23-Jan-2024.)
⊢ (0 −ℝ 0) = 0
Theorem	readdlid 43024	Real number version of addlid 11381. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (0 + 𝐴) = 𝐴)
Theorem	sn-addlid 43025	addlid 11381 without ax-mulcom 11152. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
Theorem	remul02 43026	Real number version of mul02 11376 proven without ax-mulcom 11152. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (0 · 𝐴) = 0)
Theorem	sn-0ne2 43027	0ne2 12441 without ax-mulcom 11152. (Contributed by SN, 23-Jan-2024.)
⊢ 0 ≠ 2
Theorem	remul01 43028	Real number version of mul01 11377 proven without ax-mulcom 11152. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 · 0) = 0)
Theorem	sn-remul0ord 43029	A product is zero iff one of its factors are zero. (Contributed by SN, 24-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) = 0 ↔ (𝐴 = 0 ∨ 𝐵 = 0)))
Theorem	resubid 43030	Subtraction of a real number from itself (compare subid 11465). (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 𝐴) = 0)
Theorem	readdrid 43031	Real number version of addrid 11378 without ax-mulcom 11152. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 + 0) = 𝐴)
Theorem	resubid1 43032	Real number version of subid1 11466 without ax-mulcom 11152. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 0) = 𝐴)
Theorem	renegneg 43033	A real number is equal to the negative of its negative. Compare negneg 11496. (Contributed by SN, 13-Feb-2024.)
⊢ (𝐴 ∈ ℝ → (0 −ℝ (0 −ℝ 𝐴)) = 𝐴)
Theorem	readdcan2 43034	Commuted version of readdcan 11372 without ax-mulcom 11152. (Contributed by SN, 21-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵))
Theorem	renegid2 43035	Commuted version of renegid 42994. (Contributed by SN, 4-May-2024.)
⊢ (𝐴 ∈ ℝ → ((0 −ℝ 𝐴) + 𝐴) = 0)
Theorem	remulneg2d 43036	Product with negative is negative of product. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 · (0 −ℝ 𝐵)) = (0 −ℝ (𝐴 · 𝐵)))
Theorem	sn-it0e0 43037	Proof of it0e0 12458 without ax-mulcom 11152. Informally, a real number times 0 is 0, and ∃𝑟 ∈ ℝ𝑟 = i · 𝑠 by ax-cnre 11161 and renegid2 43035. (Contributed by SN, 30-Apr-2024.)
⊢ (i · 0) = 0
Theorem	sn-negex12 43038*	A combination of cnegex 11379 and cnegex2 11380, this proof takes cnre 11193 𝐴 = 𝑟 + 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 43039*	Proof of cnegex 11379 without ax-mulcom 11152. (Contributed by SN, 30-Apr-2024.)
⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝐴 + 𝑏) = 0)
Theorem	sn-negex2 43040*	Proof of cnegex2 11380 without ax-mulcom 11152. (Contributed by SN, 5-May-2024.)
⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝑏 + 𝐴) = 0)
Theorem	sn-addcand 43041	addcand 11401 without ax-mulcom 11152. Note how the proof is almost identical to addcan 11382. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶))
Theorem	sn-addrid 43042	addrid 11378 without ax-mulcom 11152. (Contributed by SN, 5-May-2024.)
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
Theorem	sn-addcan2d 43043	addcan2d 11402 without ax-mulcom 11152. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵))
Theorem	reixi 43044	ixi 11831 without ax-mulcom 11152. (Contributed by SN, 5-May-2024.)
⊢ (i · i) = (0 −ℝ 1)
Theorem	rei4 43045	i4 14231 without ax-mulcom 11152. (Contributed by SN, 27-May-2024.)
⊢ ((i · i) · (i · i)) = 1
Theorem	sn-addid0 43046	A number that sums to itself is zero. Compare addid0 11621, readdridaddlidd 42885. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐴) = 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	sn-mul01 43047	mul01 11377 without ax-mulcom 11152. (Contributed by SN, 5-May-2024.)
⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0)
Theorem	sn-subeu 43048*	negeu 11435 without ax-mulcom 11152 and complex number version of resubeu 42998. (Contributed by SN, 5-May-2024.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐴 + 𝑥) = 𝐵)
Theorem	sn-subcl 43049	subcl 11444 without ax-mulcom 11152. (Contributed by SN, 5-May-2024.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
Theorem	sn-subf 43050	subf 11447 without ax-mulcom 11152. (Contributed by SN, 5-May-2024.)
⊢ − :(ℂ × ℂ)⟶ℂ
Theorem	resubeqsub 43051	Equivalence between real subtraction and subtraction. (Contributed by SN, 5-May-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (𝐴 − 𝐵))
Theorem	subresre 43052	Subtraction restricted to the reals. (Contributed by SN, 5-May-2024.)
⊢ −ℝ = ( − ↾ (ℝ × ℝ))
Theorem	addinvcom 43053	A number commutes with its additive inverse. Compare remulinvcom 43054. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 0)    ⇒   ⊢ (𝜑 → (𝐵 + 𝐴) = 0)
Theorem	remulinvcom 43054	A left multiplicative inverse is a right multiplicative inverse. Proven without ax-mulcom 11152. (Contributed by SN, 5-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 · 𝐵) = 1)    ⇒   ⊢ (𝜑 → (𝐵 · 𝐴) = 1)
Theorem	remullid 43055	Commuted version of ax-1rid 11158 without ax-mulcom 11152. (Contributed by SN, 5-Feb-2024.)
⊢ (𝐴 ∈ ℝ → (1 · 𝐴) = 𝐴)
Theorem	sn-1ticom 43056	Lemma for sn-mullid 43057 and sn-it1ei 43058. (Contributed by SN, 27-May-2024.)
⊢ (1 · i) = (i · 1)
Theorem	sn-mullid 43057	mullid 11195 without ax-mulcom 11152. (Contributed by SN, 27-May-2024.)
⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
Theorem	sn-it1ei 43058	it1ei 42937 without ax-mulcom 11152. (See sn-mullid 43057 for commuted version). (Contributed by SN, 1-Jun-2024.)
⊢ (i · 1) = i
Theorem	ipiiie0 43059	The multiplicative inverse of i (per i4 14231) is also its additive inverse. (Contributed by SN, 30-Jun-2024.)
⊢ (i + (i · (i · i))) = 0
Theorem	remulcand 43060	Commuted version of remulcan2d 42884 without ax-mulcom 11152. (Contributed by SN, 21-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵))
Syntax	crediv 43061	Real number division.
class /ℝ
Definition	df-rediv 43062*	Define division between real numbers. This operator saves ax-mulcom 11152 over df-div 11860 in certain situations. (Contributed by SN, 25-Nov-2025.)
⊢ /ℝ = (𝑥 ∈ ℝ, 𝑦 ∈ (ℝ ∖ {0}) ↦ (℩𝑧 ∈ ℝ (𝑦 · 𝑧) = 𝑥))
Theorem	redivvald 43063*	Value of real division, which is the (unique) real 𝑥 such that (𝐵 · 𝑥) = 𝐴. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 /ℝ 𝐵) = (℩𝑥 ∈ ℝ (𝐵 · 𝑥) = 𝐴))
Theorem	rediveud 43064*	Existential uniqueness of real quotients. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ ℝ (𝐵 · 𝑥) = 𝐴)
Theorem	sn-redivcld 43065	Closure law for real division. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 /ℝ 𝐵) ∈ ℝ)
Theorem	redivmuld 43066	Relationship between division and multiplication. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 /ℝ 𝐶) = 𝐵 ↔ (𝐶 · 𝐵) = 𝐴))
Theorem	redivmul2d 43067	Relationship between division and multiplication. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 /ℝ 𝐶) = 𝐵 ↔ 𝐴 = (𝐶 · 𝐵)))
Theorem	redivcan2d 43068	A cancellation law for division. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐵 · (𝐴 /ℝ 𝐵)) = 𝐴)
Theorem	redivcan3d 43069	A cancellation law for division. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐵 · 𝐴) /ℝ 𝐵) = 𝐴)
Theorem	rediveq0d 43070	A ratio is zero iff the numerator is zero. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 /ℝ 𝐵) = 0 ↔ 𝐴 = 0))
Theorem	redivne0bd 43071	The ratio of nonzero numbers is nonzero. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 0 ↔ (𝐴 /ℝ 𝐵) ≠ 0))
Theorem	rediveq1d 43072	Equality in terms of unit ratio. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 /ℝ 𝐵) = 1 ↔ 𝐴 = 𝐵))
Theorem	sn-rediv1d 43073	A number divided by 1 is itself. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 /ℝ 1) = 𝐴)
Theorem	sn-rediv0d 43074	Division into zero is zero. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (0 /ℝ 𝐴) = 0)
Theorem	sn-redividd 43075	A number divided by itself is 1. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 /ℝ 𝐴) = 1)
Theorem	sn-rereccld 43076	Closure law for reciprocal. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (1 /ℝ 𝐴) ∈ ℝ)
Theorem	rerecne0d 43077	The reciprocal of a nonzero number is nonzero. (Contributed by SN, 4-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (1 /ℝ 𝐴) ≠ 0)
Theorem	rerecidd 43078	Multiplication of a number and its reciprocal. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 · (1 /ℝ 𝐴)) = 1)
Theorem	rerecid2d 43079	Multiplication of a number and its reciprocal. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → ((1 /ℝ 𝐴) · 𝐴) = 1)
Theorem	rerecrecd 43080	A number is equal to the reciprocal of its reciprocal. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (1 /ℝ (1 /ℝ 𝐴)) = 𝐴)
Theorem	redivrec2d 43081	Relationship between division and reciprocal. (Contributed by SN, 9-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 /ℝ 𝐵) = ((1 /ℝ 𝐵) · 𝐴))
Theorem	rediv23d 43082	A "commutative"/associative law for division. (Contributed by SN, 9-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) /ℝ 𝐶) = ((𝐴 /ℝ 𝐶) · 𝐵))
Theorem	redivdird 43083	Distribution of division over addition. (Contributed by SN, 9-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) /ℝ 𝐶) = ((𝐴 /ℝ 𝐶) + (𝐵 /ℝ 𝐶)))
Theorem	rediv11d 43084	One-to-one relationship for division. (Contributed by SN, 9-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 /ℝ 𝐶) = (𝐵 /ℝ 𝐶) ↔ 𝐴 = 𝐵))
Theorem	sn-0tie0 43085	Lemma for sn-mul02 43086. Commuted version of sn-it0e0 43037. (Contributed by SN, 30-Jun-2024.)
⊢ (0 · i) = 0
Theorem	sn-mul02 43086	mul02 11376 without ax-mulcom 11152. See https://github.com/icecream17/Stuff/blob/main/math/0A%3D0.md 11152 for an outline. (Contributed by SN, 30-Jun-2024.)
⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0)
Theorem	sn-ltaddpos 43087	ltaddpos 11692 without ax-mulcom 11152. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴)))
Theorem	sn-ltaddneg 43088	ltaddneg 11414 without ax-mulcom 11152. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ (𝐵 + 𝐴) < 𝐵))
Theorem	reposdif 43089	Comparison of two numbers whose difference is positive. Compare posdif 11695. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 −ℝ 𝐴)))
Theorem	relt0neg1 43090	Comparison of a real and its negative to zero. Compare lt0neg1 11708. (Contributed by SN, 13-Feb-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 < 0 ↔ 0 < (0 −ℝ 𝐴)))
Theorem	relt0neg2 43091	Comparison of a real and its negative to zero. Compare lt0neg2 11709. (Contributed by SN, 13-Feb-2024.)
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ (0 −ℝ 𝐴) < 0))
Theorem	sn-addlt0d 43092	The sum of negative numbers is negative. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    &   ⊢ (𝜑 → 𝐵 < 0)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) < 0)
Theorem	sn-addgt0d 43093	The sum of positive numbers is positive. Proof of addgt0d 11777 without ax-mulcom 11152. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → 0 < (𝐴 + 𝐵))
Theorem	sn-nnne0 43094	nnne0 12261 without ax-mulcom 11152. (Contributed by SN, 25-Jan-2025.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)
Theorem	reelznn0nn 43095	elznn0nn 12596 restated using df-resub 42987. (Contributed by SN, 25-Jan-2025.)
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ (0 −ℝ 𝑁) ∈ ℕ)))
Theorem	nn0addcom 43096	Addition is commutative for nonnegative integers. Proven without ax-mulcom 11152. (Contributed by SN, 1-Feb-2025.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	zaddcomlem 43097	Lemma for zaddcom 43098. (Contributed by SN, 1-Feb-2025.)
⊢ (((𝐴 ∈ ℝ ∧ (0 −ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	zaddcom 43098	Addition is commutative for integers. Proven without ax-mulcom 11152. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	renegmulnnass 43099	Move multiplication by a natural number inside and outside negation. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((0 −ℝ 𝐴) · 𝑁) = (0 −ℝ (𝐴 · 𝑁)))
Theorem	nn0mulcom 43100	Multiplication is commutative for nonnegative integers. Proven without ax-mulcom 11152. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = (𝐵 · 𝐴))