P. 426 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42501-42600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	repncan3 42501	Addition and subtraction of equals. Based on pncan3 11375. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + (𝐵 −ℝ 𝐴)) = 𝐵)
Theorem	readdsub 42502	Law for addition and subtraction. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐶) = ((𝐴 −ℝ 𝐶) + 𝐵))
Theorem	reladdrsub 42503	Move LHS of a sum into RHS of a (real) difference. Version of mvlladdd 11535 with real subtraction. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 = (𝐶 −ℝ 𝐴))
Theorem	reltsub1 42504	Subtraction from both sides of 'less than'. Compare ltsub1 11620. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 −ℝ 𝐶) < (𝐵 −ℝ 𝐶)))
Theorem	reltsubadd2 42505	'Less than' relationship between addition and subtraction. Compare ltsubadd2 11595. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶)))
Theorem	resubcan2 42506	Cancellation law for real subtraction. Compare subcan2 11393. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) = (𝐵 −ℝ 𝐶) ↔ 𝐴 = 𝐵))
Theorem	resubsub4 42507	Law for double subtraction. Compare subsub4 11401. (Contributed by Steven Nguyen, 14-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) −ℝ 𝐶) = (𝐴 −ℝ (𝐵 + 𝐶)))
Theorem	rennncan2 42508	Cancellation law for real subtraction. Compare nnncan2 11405. (Contributed by Steven Nguyen, 14-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) −ℝ (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐵))
Theorem	renpncan3 42509	Cancellation law for real subtraction. Compare npncan3 11406. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) + (𝐶 −ℝ 𝐴)) = (𝐶 −ℝ 𝐵))
Theorem	repnpcan 42510	Cancellation law for addition and real subtraction. Compare pnpcan 11407. (Contributed by Steven Nguyen, 19-May-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ (𝐴 + 𝐶)) = (𝐵 −ℝ 𝐶))
Theorem	reppncan 42511	Cancellation law for mixed addition and real subtraction. Compare ppncan 11410. (Contributed by SN, 3-Sep-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) + (𝐵 −ℝ 𝐶)) = (𝐴 + 𝐵))
Theorem	resubidaddlidlem 42512	Lemma for resubidaddlid 42513. A special case of npncan 11389. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 −ℝ 𝐵) = (𝐵 −ℝ 𝐶))    ⇒   ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) + (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐶))
Theorem	resubidaddlid 42513	Any real number subtracted from itself forms a left additive identity. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 −ℝ 𝐴) + 𝐵) = 𝐵)
Theorem	resubdi 42514	Distribution of multiplication over real subtraction. (Contributed by Steven Nguyen, 3-Jun-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐵 −ℝ 𝐶)) = ((𝐴 · 𝐵) −ℝ (𝐴 · 𝐶)))
Theorem	re1m1e0m0 42515	Equality of two left-additive identities. See resubidaddlid 42513. Uses ax-i2m1 11081. (Contributed by SN, 25-Dec-2023.)
⊢ (1 −ℝ 1) = (0 −ℝ 0)
Theorem	sn-00idlem1 42516	Lemma for sn-00id 42519. (Contributed by SN, 25-Dec-2023.)
⊢ (𝐴 ∈ ℝ → (𝐴 · (0 −ℝ 0)) = (𝐴 −ℝ 𝐴))
Theorem	sn-00idlem2 42517	Lemma for sn-00id 42519. (Contributed by SN, 25-Dec-2023.)
⊢ ((0 −ℝ 0) ≠ 0 → (0 −ℝ 0) = 1)
Theorem	sn-00idlem3 42518	Lemma for sn-00id 42519. (Contributed by SN, 25-Dec-2023.)
⊢ ((0 −ℝ 0) = 1 → (0 + 0) = 0)
Theorem	sn-00id 42519	00id 11295 proven without ax-mulcom 11077 but using ax-1ne0 11082. (Though note that the current version of 00id 11295 can be changed to avoid ax-icn 11072, ax-addcl 11073, ax-mulcl 11075, ax-i2m1 11081, ax-cnre 11086. Most of this is by using 0cnALT3 42371 instead of 0cn 11111). (Contributed by SN, 25-Dec-2023.) (Proof modification is discouraged.)
⊢ (0 + 0) = 0
Theorem	re0m0e0 42520	Real number version of 0m0e0 12247 proven without ax-mulcom 11077. (Contributed by SN, 23-Jan-2024.)
⊢ (0 −ℝ 0) = 0
Theorem	readdlid 42521	Real number version of addlid 11303. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (0 + 𝐴) = 𝐴)
Theorem	sn-addlid 42522	addlid 11303 without ax-mulcom 11077. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
Theorem	remul02 42523	Real number version of mul02 11298 proven without ax-mulcom 11077. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (0 · 𝐴) = 0)
Theorem	sn-0ne2 42524	0ne2 12334 without ax-mulcom 11077. (Contributed by SN, 23-Jan-2024.)
⊢ 0 ≠ 2
Theorem	remul01 42525	Real number version of mul01 11299 proven without ax-mulcom 11077. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 · 0) = 0)
Theorem	sn-remul0ord 42526	A product is zero iff one of its factors are zero. (Contributed by SN, 24-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) = 0 ↔ (𝐴 = 0 ∨ 𝐵 = 0)))
Theorem	resubid 42527	Subtraction of a real number from itself (compare subid 11387). (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 𝐴) = 0)
Theorem	readdrid 42528	Real number version of addrid 11300 without ax-mulcom 11077. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 + 0) = 𝐴)
Theorem	resubid1 42529	Real number version of subid1 11388 without ax-mulcom 11077. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 0) = 𝐴)
Theorem	renegneg 42530	A real number is equal to the negative of its negative. Compare negneg 11418. (Contributed by SN, 13-Feb-2024.)
⊢ (𝐴 ∈ ℝ → (0 −ℝ (0 −ℝ 𝐴)) = 𝐴)
Theorem	readdcan2 42531	Commuted version of readdcan 11294 without ax-mulcom 11077. (Contributed by SN, 21-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵))
Theorem	renegid2 42532	Commuted version of renegid 42491. (Contributed by SN, 4-May-2024.)
⊢ (𝐴 ∈ ℝ → ((0 −ℝ 𝐴) + 𝐴) = 0)
Theorem	remulneg2d 42533	Product with negative is negative of product. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 · (0 −ℝ 𝐵)) = (0 −ℝ (𝐴 · 𝐵)))
Theorem	sn-it0e0 42534	Proof of it0e0 12351 without ax-mulcom 11077. Informally, a real number times 0 is 0, and ∃𝑟 ∈ ℝ𝑟 = i · 𝑠 by ax-cnre 11086 and renegid2 42532. (Contributed by SN, 30-Apr-2024.)
⊢ (i · 0) = 0
Theorem	sn-negex12 42535*	A combination of cnegex 11301 and cnegex2 11302, this proof takes cnre 11116 𝐴 = 𝑟 + 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 42536*	Proof of cnegex 11301 without ax-mulcom 11077. (Contributed by SN, 30-Apr-2024.)
⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝐴 + 𝑏) = 0)
Theorem	sn-negex2 42537*	Proof of cnegex2 11302 without ax-mulcom 11077. (Contributed by SN, 5-May-2024.)
⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝑏 + 𝐴) = 0)
Theorem	sn-addcand 42538	addcand 11323 without ax-mulcom 11077. Note how the proof is almost identical to addcan 11304. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶))
Theorem	sn-addrid 42539	addrid 11300 without ax-mulcom 11077. (Contributed by SN, 5-May-2024.)
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
Theorem	sn-addcan2d 42540	addcan2d 11324 without ax-mulcom 11077. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵))
Theorem	reixi 42541	ixi 11753 without ax-mulcom 11077. (Contributed by SN, 5-May-2024.)
⊢ (i · i) = (0 −ℝ 1)
Theorem	rei4 42542	i4 14113 without ax-mulcom 11077. (Contributed by SN, 27-May-2024.)
⊢ ((i · i) · (i · i)) = 1
Theorem	sn-addid0 42543	A number that sums to itself is zero. Compare addid0 11543, readdridaddlidd 42376. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐴) = 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	sn-mul01 42544	mul01 11299 without ax-mulcom 11077. (Contributed by SN, 5-May-2024.)
⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0)
Theorem	sn-subeu 42545*	negeu 11357 without ax-mulcom 11077 and complex number version of resubeu 42495. (Contributed by SN, 5-May-2024.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐴 + 𝑥) = 𝐵)
Theorem	sn-subcl 42546	subcl 11366 without ax-mulcom 11077. (Contributed by SN, 5-May-2024.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
Theorem	sn-subf 42547	subf 11369 without ax-mulcom 11077. (Contributed by SN, 5-May-2024.)
⊢ − :(ℂ × ℂ)⟶ℂ
Theorem	resubeqsub 42548	Equivalence between real subtraction and subtraction. (Contributed by SN, 5-May-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (𝐴 − 𝐵))
Theorem	subresre 42549	Subtraction restricted to the reals. (Contributed by SN, 5-May-2024.)
⊢ −ℝ = ( − ↾ (ℝ × ℝ))
Theorem	addinvcom 42550	A number commutes with its additive inverse. Compare remulinvcom 42551. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 0)    ⇒   ⊢ (𝜑 → (𝐵 + 𝐴) = 0)
Theorem	remulinvcom 42551	A left multiplicative inverse is a right multiplicative inverse. Proven without ax-mulcom 11077. (Contributed by SN, 5-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 · 𝐵) = 1)    ⇒   ⊢ (𝜑 → (𝐵 · 𝐴) = 1)
Theorem	remullid 42552	Commuted version of ax-1rid 11083 without ax-mulcom 11077. (Contributed by SN, 5-Feb-2024.)
⊢ (𝐴 ∈ ℝ → (1 · 𝐴) = 𝐴)
Theorem	sn-1ticom 42553	Lemma for sn-mullid 42554 and sn-it1ei 42555. (Contributed by SN, 27-May-2024.)
⊢ (1 · i) = (i · 1)
Theorem	sn-mullid 42554	mullid 11118 without ax-mulcom 11077. (Contributed by SN, 27-May-2024.)
⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
Theorem	sn-it1ei 42555	it1ei 42434 without ax-mulcom 11077. (See sn-mullid 42554 for commuted version). (Contributed by SN, 1-Jun-2024.)
⊢ (i · 1) = i
Theorem	ipiiie0 42556	The multiplicative inverse of i (per i4 14113) is also its additive inverse. (Contributed by SN, 30-Jun-2024.)
⊢ (i + (i · (i · i))) = 0
Theorem	remulcand 42557	Commuted version of remulcan2d 42375 without ax-mulcom 11077. (Contributed by SN, 21-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵))
Syntax	crediv 42558	Real number division.
class /ℝ
Definition	df-rediv 42559*	Define division between real numbers. This operator saves ax-mulcom 11077 over df-div 11782 in certain situations. (Contributed by SN, 25-Nov-2025.)
⊢ /ℝ = (𝑥 ∈ ℝ, 𝑦 ∈ (ℝ ∖ {0}) ↦ (℩𝑧 ∈ ℝ (𝑦 · 𝑧) = 𝑥))
Theorem	redivvald 42560*	Value of real division, which is the (unique) real 𝑥 such that (𝐵 · 𝑥) = 𝐴. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 /ℝ 𝐵) = (℩𝑥 ∈ ℝ (𝐵 · 𝑥) = 𝐴))
Theorem	rediveud 42561*	Existential uniqueness of real quotients. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ ℝ (𝐵 · 𝑥) = 𝐴)
Theorem	sn-redivcld 42562	Closure law for real division. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 /ℝ 𝐵) ∈ ℝ)
Theorem	redivmuld 42563	Relationship between division and multiplication. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 /ℝ 𝐶) = 𝐵 ↔ (𝐶 · 𝐵) = 𝐴))
Theorem	redivcan2d 42564	A cancellation law for division. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐵 · (𝐴 /ℝ 𝐵)) = 𝐴)
Theorem	redivcan3d 42565	A cancellation law for division. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐵 · 𝐴) /ℝ 𝐵) = 𝐴)
Theorem	sn-rereccld 42566	Closure law for reciprocal. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (1 /ℝ 𝐴) ∈ ℝ)
Theorem	rerecid 42567	Multiplication of a number and its reciprocal. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 · (1 /ℝ 𝐴)) = 1)
Theorem	rerecid2 42568	Multiplication of a number and its reciprocal. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → ((1 /ℝ 𝐴) · 𝐴) = 1)
Theorem	sn-0tie0 42569	Lemma for sn-mul02 42570. Commuted version of sn-it0e0 42534. (Contributed by SN, 30-Jun-2024.)
⊢ (0 · i) = 0
Theorem	sn-mul02 42570	mul02 11298 without ax-mulcom 11077. See https://github.com/icecream17/Stuff/blob/main/math/0A%3D0.md 11077 for an outline. (Contributed by SN, 30-Jun-2024.)
⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0)
Theorem	sn-ltaddpos 42571	ltaddpos 11614 without ax-mulcom 11077. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴)))
Theorem	sn-ltaddneg 42572	ltaddneg 11336 without ax-mulcom 11077. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ (𝐵 + 𝐴) < 𝐵))
Theorem	reposdif 42573	Comparison of two numbers whose difference is positive. Compare posdif 11617. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 −ℝ 𝐴)))
Theorem	relt0neg1 42574	Comparison of a real and its negative to zero. Compare lt0neg1 11630. (Contributed by SN, 13-Feb-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 < 0 ↔ 0 < (0 −ℝ 𝐴)))
Theorem	relt0neg2 42575	Comparison of a real and its negative to zero. Compare lt0neg2 11631. (Contributed by SN, 13-Feb-2024.)
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ (0 −ℝ 𝐴) < 0))
Theorem	sn-addlt0d 42576	The sum of negative numbers is negative. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    &   ⊢ (𝜑 → 𝐵 < 0)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) < 0)
Theorem	sn-addgt0d 42577	The sum of positive numbers is positive. Proof of addgt0d 11699 without ax-mulcom 11077. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → 0 < (𝐴 + 𝐵))
Theorem	sn-nnne0 42578	nnne0 12166 without ax-mulcom 11077. (Contributed by SN, 25-Jan-2025.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)
Theorem	reelznn0nn 42579	elznn0nn 12489 restated using df-resub 42484. (Contributed by SN, 25-Jan-2025.)
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ (0 −ℝ 𝑁) ∈ ℕ)))
Theorem	nn0addcom 42580	Addition is commutative for nonnegative integers. Proven without ax-mulcom 11077. (Contributed by SN, 1-Feb-2025.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	zaddcomlem 42581	Lemma for zaddcom 42582. (Contributed by SN, 1-Feb-2025.)
⊢ (((𝐴 ∈ ℝ ∧ (0 −ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	zaddcom 42582	Addition is commutative for integers. Proven without ax-mulcom 11077. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	renegmulnnass 42583	Move multiplication by a natural number inside and outside negation. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((0 −ℝ 𝐴) · 𝑁) = (0 −ℝ (𝐴 · 𝑁)))
Theorem	nn0mulcom 42584	Multiplication is commutative for nonnegative integers. Proven without ax-mulcom 11077. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	zmulcomlem 42585	Lemma for zmulcom 42586. (Contributed by SN, 25-Jan-2025.)
⊢ (((𝐴 ∈ ℝ ∧ (0 −ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	zmulcom 42586	Multiplication is commutative for integers. Proven without ax-mulcom 11077. From this result and grpcominv1 42626, we can show that rationals commute under multiplication without using ax-mulcom 11077. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	mulgt0con1dlem 42587	Lemma for mulgt0con1d 42588. Contraposes a positive deduction to a negative deduction. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (0 < 𝐴 → 0 < 𝐵))    &   ⊢ (𝜑 → (𝐴 = 0 → 𝐵 = 0))    ⇒   ⊢ (𝜑 → (𝐵 < 0 → 𝐴 < 0))
Theorem	mulgt0con1d 42588	Counterpart to mulgt0con2d 42589, though not a lemma. This is the first use of ax-pre-mulgt0 11090. One direction of mulgt0b2d 42596. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐵)    &   ⊢ (𝜑 → (𝐴 · 𝐵) < 0)    ⇒   ⊢ (𝜑 → 𝐴 < 0)
Theorem	mulgt0con2d 42589	Lemma for mulgt0b1d 42590 and contrapositive of mulgt0 11197. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → (𝐴 · 𝐵) < 0)    ⇒   ⊢ (𝜑 → 𝐵 < 0)
Theorem	mulgt0b1d 42590	Biconditional, deductive form of mulgt0 11197. The second factor is positive iff the product is. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → (0 < 𝐵 ↔ 0 < (𝐴 · 𝐵)))
Theorem	sn-ltmul2d 42591	ltmul2d 12978 without ax-mulcom 11077. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐶)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) < (𝐶 · 𝐵) ↔ 𝐴 < 𝐵))
Theorem	sn-ltmulgt11d 42592	ltmulgt11d 12971 without ax-mulcom 11077. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → (1 < 𝐴 ↔ 𝐵 < (𝐵 · 𝐴)))
Theorem	sn-0lt1 42593	0lt1 11646 without ax-mulcom 11077. (Contributed by SN, 13-Feb-2024.)
⊢ 0 < 1
Theorem	sn-ltp1 42594	ltp1 11968 without ax-mulcom 11077. (Contributed by SN, 13-Feb-2024.)
⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1))
Theorem	sn-recgt0d 42595	The reciprocal of a positive real is positive. (Contributed by SN, 26-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → 0 < (1 /ℝ 𝐴))
Theorem	mulgt0b2d 42596	Biconditional, deductive form of mulgt0 11197. The first factor is positive iff the product is. (Contributed by SN, 24-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → (0 < 𝐴 ↔ 0 < (𝐴 · 𝐵)))
Theorem	sn-mulgt1d 42597	mulgt1d 12065 without ax-mulcom 11077. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 1 < 𝐴)    &   ⊢ (𝜑 → 1 < 𝐵)    ⇒   ⊢ (𝜑 → 1 < (𝐴 · 𝐵))
Theorem	reneg1lt0 42598	Negative one is a negative number. (Contributed by SN, 1-Jun-2024.)
⊢ (0 −ℝ 1) < 0
Theorem	sn-reclt0d 42599	The reciprocal of a negative real is negative. (Contributed by SN, 26-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    ⇒   ⊢ (𝜑 → (1 /ℝ 𝐴) < 0)
Theorem	mulltgt0d 42600	Negative times positive is negative. (Contributed by SN, 26-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) < 0)