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	sn-subcl 43001	subcl 11426 without ax-mulcom 11134. (Contributed by SN, 5-May-2024.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
Theorem	sn-subf 43002	subf 11429 without ax-mulcom 11134. (Contributed by SN, 5-May-2024.)
⊢ − :(ℂ × ℂ)⟶ℂ
Theorem	resubeqsub 43003	Equivalence between real subtraction and subtraction. (Contributed by SN, 5-May-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (𝐴 − 𝐵))
Theorem	subresre 43004	Subtraction restricted to the reals. (Contributed by SN, 5-May-2024.)
⊢ −ℝ = ( − ↾ (ℝ × ℝ))
Theorem	addinvcom 43005	A number commutes with its additive inverse. Compare remulinvcom 43006. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 0)    ⇒   ⊢ (𝜑 → (𝐵 + 𝐴) = 0)
Theorem	remulinvcom 43006	A left multiplicative inverse is a right multiplicative inverse. Proven without ax-mulcom 11134. (Contributed by SN, 5-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 · 𝐵) = 1)    ⇒   ⊢ (𝜑 → (𝐵 · 𝐴) = 1)
Theorem	remullid 43007	Commuted version of ax-1rid 11140 without ax-mulcom 11134. (Contributed by SN, 5-Feb-2024.)
⊢ (𝐴 ∈ ℝ → (1 · 𝐴) = 𝐴)
Theorem	sn-1ticom 43008	Lemma for sn-mullid 43009 and sn-it1ei 43010. (Contributed by SN, 27-May-2024.)
⊢ (1 · i) = (i · 1)
Theorem	sn-mullid 43009	mullid 11177 without ax-mulcom 11134. (Contributed by SN, 27-May-2024.)
⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
Theorem	sn-it1ei 43010	it1ei 42889 without ax-mulcom 11134. (See sn-mullid 43009 for commuted version). (Contributed by SN, 1-Jun-2024.)
⊢ (i · 1) = i
Theorem	ipiiie0 43011	The multiplicative inverse of i (per i4 14214) is also its additive inverse. (Contributed by SN, 30-Jun-2024.)
⊢ (i + (i · (i · i))) = 0
Theorem	remulcand 43012	Commuted version of remulcan2d 42836 without ax-mulcom 11134. (Contributed by SN, 21-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵))
Syntax	crediv 43013	Real number division.
class /ℝ
Definition	df-rediv 43014*	Define division between real numbers. This operator saves ax-mulcom 11134 over df-div 11842 in certain situations. (Contributed by SN, 25-Nov-2025.)
⊢ /ℝ = (𝑥 ∈ ℝ, 𝑦 ∈ (ℝ ∖ {0}) ↦ (℩𝑧 ∈ ℝ (𝑦 · 𝑧) = 𝑥))
Theorem	redivvald 43015*	Value of real division, which is the (unique) real 𝑥 such that (𝐵 · 𝑥) = 𝐴. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 /ℝ 𝐵) = (℩𝑥 ∈ ℝ (𝐵 · 𝑥) = 𝐴))
Theorem	rediveud 43016*	Existential uniqueness of real quotients. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ ℝ (𝐵 · 𝑥) = 𝐴)
Theorem	sn-redivcld 43017	Closure law for real division. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 /ℝ 𝐵) ∈ ℝ)
Theorem	redivmuld 43018	Relationship between division and multiplication. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 /ℝ 𝐶) = 𝐵 ↔ (𝐶 · 𝐵) = 𝐴))
Theorem	redivmul2d 43019	Relationship between division and multiplication. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 /ℝ 𝐶) = 𝐵 ↔ 𝐴 = (𝐶 · 𝐵)))
Theorem	redivcan2d 43020	A cancellation law for division. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐵 · (𝐴 /ℝ 𝐵)) = 𝐴)
Theorem	redivcan3d 43021	A cancellation law for division. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐵 · 𝐴) /ℝ 𝐵) = 𝐴)
Theorem	rediveq0d 43022	A ratio is zero iff the numerator is zero. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 /ℝ 𝐵) = 0 ↔ 𝐴 = 0))
Theorem	redivne0bd 43023	The ratio of nonzero numbers is nonzero. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 0 ↔ (𝐴 /ℝ 𝐵) ≠ 0))
Theorem	rediveq1d 43024	Equality in terms of unit ratio. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 /ℝ 𝐵) = 1 ↔ 𝐴 = 𝐵))
Theorem	sn-rediv1d 43025	A number divided by 1 is itself. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 /ℝ 1) = 𝐴)
Theorem	sn-rediv0d 43026	Division into zero is zero. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (0 /ℝ 𝐴) = 0)
Theorem	sn-redividd 43027	A number divided by itself is 1. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 /ℝ 𝐴) = 1)
Theorem	sn-rereccld 43028	Closure law for reciprocal. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (1 /ℝ 𝐴) ∈ ℝ)
Theorem	rerecne0d 43029	The reciprocal of a nonzero number is nonzero. (Contributed by SN, 4-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (1 /ℝ 𝐴) ≠ 0)
Theorem	rerecidd 43030	Multiplication of a number and its reciprocal. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 · (1 /ℝ 𝐴)) = 1)
Theorem	rerecid2d 43031	Multiplication of a number and its reciprocal. (Contributed by SN, 25-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → ((1 /ℝ 𝐴) · 𝐴) = 1)
Theorem	rerecrecd 43032	A number is equal to the reciprocal of its reciprocal. (Contributed by SN, 2-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (1 /ℝ (1 /ℝ 𝐴)) = 𝐴)
Theorem	redivrec2d 43033	Relationship between division and reciprocal. (Contributed by SN, 9-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 /ℝ 𝐵) = ((1 /ℝ 𝐵) · 𝐴))
Theorem	rediv23d 43034	A "commutative"/associative law for division. (Contributed by SN, 9-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) /ℝ 𝐶) = ((𝐴 /ℝ 𝐶) · 𝐵))
Theorem	redivdird 43035	Distribution of division over addition. (Contributed by SN, 9-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) /ℝ 𝐶) = ((𝐴 /ℝ 𝐶) + (𝐵 /ℝ 𝐶)))
Theorem	rediv11d 43036	One-to-one relationship for division. (Contributed by SN, 9-Apr-2026.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 /ℝ 𝐶) = (𝐵 /ℝ 𝐶) ↔ 𝐴 = 𝐵))
Theorem	sn-0tie0 43037	Lemma for sn-mul02 43038. Commuted version of sn-it0e0 42989. (Contributed by SN, 30-Jun-2024.)
⊢ (0 · i) = 0
Theorem	sn-mul02 43038	mul02 11358 without ax-mulcom 11134. See https://github.com/icecream17/Stuff/blob/main/math/0A%3D0.md 11134 for an outline. (Contributed by SN, 30-Jun-2024.)
⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0)
Theorem	sn-ltaddpos 43039	ltaddpos 11674 without ax-mulcom 11134. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴)))
Theorem	sn-ltaddneg 43040	ltaddneg 11396 without ax-mulcom 11134. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ (𝐵 + 𝐴) < 𝐵))
Theorem	reposdif 43041	Comparison of two numbers whose difference is positive. Compare posdif 11677. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 −ℝ 𝐴)))
Theorem	relt0neg1 43042	Comparison of a real and its negative to zero. Compare lt0neg1 11690. (Contributed by SN, 13-Feb-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 < 0 ↔ 0 < (0 −ℝ 𝐴)))
Theorem	relt0neg2 43043	Comparison of a real and its negative to zero. Compare lt0neg2 11691. (Contributed by SN, 13-Feb-2024.)
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ (0 −ℝ 𝐴) < 0))
Theorem	sn-addlt0d 43044	The sum of negative numbers is negative. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    &   ⊢ (𝜑 → 𝐵 < 0)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) < 0)
Theorem	sn-addgt0d 43045	The sum of positive numbers is positive. Proof of addgt0d 11759 without ax-mulcom 11134. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → 0 < (𝐴 + 𝐵))
Theorem	sn-nnne0 43046	nnne0 12244 without ax-mulcom 11134. (Contributed by SN, 25-Jan-2025.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)
Theorem	reelznn0nn 43047	elznn0nn 12579 restated using df-resub 42939. (Contributed by SN, 25-Jan-2025.)
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ (0 −ℝ 𝑁) ∈ ℕ)))
Theorem	nn0addcom 43048	Addition is commutative for nonnegative integers. Proven without ax-mulcom 11134. (Contributed by SN, 1-Feb-2025.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	zaddcomlem 43049	Lemma for zaddcom 43050. (Contributed by SN, 1-Feb-2025.)
⊢ (((𝐴 ∈ ℝ ∧ (0 −ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	zaddcom 43050	Addition is commutative for integers. Proven without ax-mulcom 11134. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	renegmulnnass 43051	Move multiplication by a natural number inside and outside negation. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((0 −ℝ 𝐴) · 𝑁) = (0 −ℝ (𝐴 · 𝑁)))
Theorem	nn0mulcom 43052	Multiplication is commutative for nonnegative integers. Proven without ax-mulcom 11134. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	zmulcomlem 43053	Lemma for zmulcom 43054. (Contributed by SN, 25-Jan-2025.)
⊢ (((𝐴 ∈ ℝ ∧ (0 −ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	zmulcom 43054	Multiplication is commutative for integers. Proven without ax-mulcom 11134. From this result and grpcominv1 43094, we can show that rationals commute under multiplication without using ax-mulcom 11134. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	mulgt0con1dlem 43055	Lemma for mulgt0con1d 43056. Contraposes a positive deduction to a negative deduction. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (0 < 𝐴 → 0 < 𝐵))    &   ⊢ (𝜑 → (𝐴 = 0 → 𝐵 = 0))    ⇒   ⊢ (𝜑 → (𝐵 < 0 → 𝐴 < 0))
Theorem	mulgt0con1d 43056	Counterpart to mulgt0con2d 43057, though not a lemma. This is the first use of ax-pre-mulgt0 11147. One direction of mulgt0b2d 43064. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐵)    &   ⊢ (𝜑 → (𝐴 · 𝐵) < 0)    ⇒   ⊢ (𝜑 → 𝐴 < 0)
Theorem	mulgt0con2d 43057	Lemma for mulgt0b1d 43058 and contrapositive of mulgt0 11257. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → (𝐴 · 𝐵) < 0)    ⇒   ⊢ (𝜑 → 𝐵 < 0)
Theorem	mulgt0b1d 43058	Biconditional, deductive form of mulgt0 11257. The second factor is positive iff the product is. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → (0 < 𝐵 ↔ 0 < (𝐴 · 𝐵)))
Theorem	sn-ltmul2d 43059	ltmul2d 13076 without ax-mulcom 11134. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐶)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) < (𝐶 · 𝐵) ↔ 𝐴 < 𝐵))
Theorem	sn-ltmulgt11d 43060	ltmulgt11d 13069 without ax-mulcom 11134. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → (1 < 𝐴 ↔ 𝐵 < (𝐵 · 𝐴)))
Theorem	sn-0lt1 43061	0lt1 11706 without ax-mulcom 11134. (Contributed by SN, 13-Feb-2024.)
⊢ 0 < 1
Theorem	sn-ltp1 43062	ltp1 12028 without ax-mulcom 11134. (Contributed by SN, 13-Feb-2024.)
⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1))
Theorem	sn-recgt0d 43063	The reciprocal of a positive real is positive. (Contributed by SN, 26-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → 0 < (1 /ℝ 𝐴))
Theorem	mulgt0b2d 43064	Biconditional, deductive form of mulgt0 11257. The first factor is positive iff the product is. (Contributed by SN, 24-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → (0 < 𝐴 ↔ 0 < (𝐴 · 𝐵)))
Theorem	sn-mulgt1d 43065	mulgt1d 12125 without ax-mulcom 11134. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 1 < 𝐴)    &   ⊢ (𝜑 → 1 < 𝐵)    ⇒   ⊢ (𝜑 → 1 < (𝐴 · 𝐵))
Theorem	reneg1lt0 43066	Negative one is a negative number. (Contributed by SN, 1-Jun-2024.)
⊢ (0 −ℝ 1) < 0
Theorem	sn-reclt0d 43067	The reciprocal of a negative real is negative. (Contributed by SN, 26-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    ⇒   ⊢ (𝜑 → (1 /ℝ 𝐴) < 0)
Theorem	mulltgt0d 43068	Negative times positive is negative. (Contributed by SN, 26-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) < 0)
Theorem	mullt0b1d 43069	When the first term is negative, the second term is positive iff the product is negative. (Contributed by SN, 26-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    ⇒   ⊢ (𝜑 → (0 < 𝐵 ↔ (𝐴 · 𝐵) < 0))
Theorem	mullt0b2d 43070	When the second term is negative, the first term is positive iff the product is negative. (Contributed by SN, 26-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 < 0)    ⇒   ⊢ (𝜑 → (0 < 𝐴 ↔ (𝐴 · 𝐵) < 0))
Theorem	sn-mullt0d 43071	The product of two negative numbers is positive. (Contributed by SN, 1-Dec-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    &   ⊢ (𝜑 → 𝐵 < 0)    ⇒   ⊢ (𝜑 → 0 < (𝐴 · 𝐵))
Theorem	sn-msqgt0d 43072	A nonzero square is positive. (Contributed by SN, 1-Dec-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → 0 < (𝐴 · 𝐴))
Theorem	sn-inelr 43073	inelr 12182 without ax-mulcom 11134. (Contributed by SN, 1-Jun-2024.)
⊢ ¬ i ∈ ℝ
Theorem	sn-itrere 43074	i times a real is real iff the real is zero. (Contributed by SN, 27-Jun-2024.)
⊢ (𝑅 ∈ ℝ → ((i · 𝑅) ∈ ℝ ↔ 𝑅 = 0))
Theorem	sn-retire 43075	Commuted version of sn-itrere 43074. (Contributed by SN, 27-Jun-2024.)
⊢ (𝑅 ∈ ℝ → ((𝑅 · i) ∈ ℝ ↔ 𝑅 = 0))
Theorem	cnreeu 43076	The reals in the expression given by cnre 11175 uniquely define a complex number. (Contributed by SN, 27-Jun-2024.)
⊢ (𝜑 → 𝑟 ∈ ℝ)    &   ⊢ (𝜑 → 𝑠 ∈ ℝ)    &   ⊢ (𝜑 → 𝑡 ∈ ℝ)    &   ⊢ (𝜑 → 𝑢 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑟 + (i · 𝑠)) = (𝑡 + (i · 𝑢)) ↔ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
Theorem	sn-sup2 43077*	sup2 12145 with exactly the same proof except for using sn-ltp1 43062 instead of ltp1 12028, saving ax-mulcom 11134. (Contributed by SN, 26-Jun-2024.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	sn-sup3d 43078*	sup3 12146 without ax-mulcom 11134, proven trivially from sn-sup2 43077. (Contributed by SN, 29-Jun-2025.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	sn-suprcld 43079*	suprcld 12152 without ax-mulcom 11134, proven trivially from sn-sup3d 43078. (Contributed by SN, 29-Jun-2025.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ)
Theorem	sn-suprubd 43080*	suprubd 12151 without ax-mulcom 11134, proven trivially from sn-suprcld 43079. (Contributed by SN, 29-Jun-2025.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ, < ))
21.30.6  Structures
Theorem	sn-base0 43081	Avoid axioms in base0 17233 by using the discouraged df-base 17229. This kind of axiom save is probably not worth it. (Contributed by SN, 16-Sep-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∅ = (Base‘∅)
Theorem	nelsubginvcld 43082	The inverse of a non-subgroup-member is a non-subgroup-member. (Contributed by Steven Nguyen, 15-Apr-2023.)
⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑆))    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ (𝜑 → (𝑁‘𝑋) ∈ (𝐵 ∖ 𝑆))
Theorem	nelsubgcld 43083	A non-subgroup-member plus a subgroup member is a non-subgroup-member. (Contributed by Steven Nguyen, 15-Apr-2023.)
⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑆))    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝐵 ∖ 𝑆))
Theorem	nelsubgsubcld 43084	A non-subgroup-member minus a subgroup member is a non-subgroup-member. (Contributed by Steven Nguyen, 15-Apr-2023.)
⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑆))    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ (𝜑 → (𝑋 − 𝑌) ∈ (𝐵 ∖ 𝑆))
Theorem	rnasclg 43085	The set of injected scalars is also interpretable as the span of the identity. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 1 = (1r‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) → ran 𝐴 = (𝑁‘{ 1 }))
Theorem	frlmfielbas 43086	The vectors of a finite free module are the functions from 𝐼 to 𝑁. (Contributed by SN, 31-Aug-2023.)
⊢ 𝐹 = (𝑅 freeLMod 𝐼)    &   ⊢ 𝑁 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin) → (𝑋 ∈ 𝐵 ↔ 𝑋:𝐼⟶𝑁))
Theorem	frlmfzwrd 43087	A vector of a module with indices from 0 to 𝑁 is a word over the scalars of the module. (Contributed by SN, 31-Aug-2023.)
⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑆 = (Base‘𝐾)    ⇒   ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ Word 𝑆)
Theorem	frlmfzowrd 43088	A vector of a module with indices from 0 to 𝑁 − 1 is a word over the scalars of the module. (Contributed by SN, 31-Aug-2023.)
⊢ 𝑊 = (𝐾 freeLMod (0..^𝑁))    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑆 = (Base‘𝐾)    ⇒   ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ Word 𝑆)
Theorem	frlmfzolen 43089	The dimension of a vector of a module with indices from 0 to 𝑁 − 1. (Contributed by SN, 1-Sep-2023.)
⊢ 𝑊 = (𝐾 freeLMod (0..^𝑁))    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑆 = (Base‘𝐾)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (♯‘𝑋) = 𝑁)
Theorem	frlmfzowrdb 43090	The vectors of a module with indices 0 to 𝑁 − 1 are the length- 𝑁 words over the scalars of the module. (Contributed by SN, 1-Sep-2023.)
⊢ 𝑊 = (𝐾 freeLMod (0..^𝑁))    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑆 = (Base‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑋 ∈ 𝐵 ↔ (𝑋 ∈ Word 𝑆 ∧ (♯‘𝑋) = 𝑁)))
Theorem	frlmfzoccat 43091	The concatenation of two vectors of dimension 𝑁 and 𝑀 forms a vector of dimension 𝑁 + 𝑀. (Contributed by SN, 31-Aug-2023.)
⊢ 𝑊 = (𝐾 freeLMod (0..^𝐿))    &   ⊢ 𝑋 = (𝐾 freeLMod (0..^𝑀))    &   ⊢ 𝑌 = (𝐾 freeLMod (0..^𝑁))    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐶 = (Base‘𝑋)    &   ⊢ 𝐷 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑍)    &   ⊢ (𝜑 → (𝑀 + 𝑁) = 𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑈 ++ 𝑉) ∈ 𝐵)
Theorem	frlmvscadiccat 43092	Scalar multiplication distributes over concatenation. (Contributed by SN, 6-Sep-2023.)
⊢ 𝑊 = (𝐾 freeLMod (0..^𝐿))    &   ⊢ 𝑋 = (𝐾 freeLMod (0..^𝑀))    &   ⊢ 𝑌 = (𝐾 freeLMod (0..^𝑁))    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐶 = (Base‘𝑋)    &   ⊢ 𝐷 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑍)    &   ⊢ (𝜑 → (𝑀 + 𝑁) = 𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐷)    &   ⊢ 𝑂 = ( ·𝑠 ‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝑋)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ 𝑆 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐴𝑂(𝑈 ++ 𝑉)) = ((𝐴 ∙ 𝑈) ++ (𝐴 · 𝑉)))
Theorem	grpasscan2d 43093	An associative cancellation law for groups. (Contributed by SN, 29-Jan-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + (𝑁‘𝑌)) + 𝑌) = 𝑋)
Theorem	grpcominv1 43094	If two elements commute, then they commute with each other's inverses (case of the first element commuting with the inverse of the second element). (Contributed by SN, 29-Jan-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋))    ⇒   ⊢ (𝜑 → (𝑋 + (𝑁‘𝑌)) = ((𝑁‘𝑌) + 𝑋))
Theorem	grpcominv2 43095	If two elements commute, then they commute with each other's inverses (case of the second element commuting with the inverse of the first element). (Contributed by SN, 1-Feb-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋))    ⇒   ⊢ (𝜑 → (𝑌 + (𝑁‘𝑋)) = ((𝑁‘𝑋) + 𝑌))
Theorem	finsubmsubg 43096	A submonoid of a finite group is a subgroup. This does not extend to infinite groups, as the submonoid ℕ0 of the group (ℤ, + ) shows. Note also that the union of a submonoid and its inverses need not be a submonoid, as the submonoid (ℕ0 ∖ {1}) of the group (ℤ, + ) shows: 3 is in that submonoid, -2 is the inverse of 2, but 1 is not in their union. Or simply, the subgroup generated by (ℕ0 ∖ {1}) is ℤ, not (ℤ ∖ {1, -1}). (Contributed by SN, 31-Jan-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))
Theorem	opprmndb 43097	A class is a monoid if and only if its opposite (ring) is a monoid. (Contributed by SN, 20-Jun-2025.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Mnd ↔ 𝑂 ∈ Mnd)
Theorem	opprgrpb 43098	A class is a group if and only if its opposite (ring) is a group. (Contributed by SN, 20-Jun-2025.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Grp ↔ 𝑂 ∈ Grp)
Theorem	opprablb 43099	A class is an Abelian group if and only if its opposite (ring) is an Abelian group. (Contributed by SN, 20-Jun-2025.)
⊢ 𝑂 = (oppr‘𝑅)    ⇒   ⊢ (𝑅 ∈ Abel ↔ 𝑂 ∈ Abel)
Theorem	imacrhmcl 43100	The image of a commutative ring homomorphism is a commutative ring. (Contributed by SN, 10-Jan-2025.)
⊢ 𝐶 = (𝑁 ↾s (𝐹 “ 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑀 RingHom 𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑀))    ⇒   ⊢ (𝜑 → 𝐶 ∈ CRing)