P. 425 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42401-42500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	resubidaddlid 42401	Any real number subtracted from itself forms a left additive identity. (Contributed by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 −ℝ 𝐴) + 𝐵) = 𝐵)
Theorem	resubdi 42402	Distribution of multiplication over real subtraction. (Contributed by Steven Nguyen, 3-Jun-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐵 −ℝ 𝐶)) = ((𝐴 · 𝐵) −ℝ (𝐴 · 𝐶)))
Theorem	re1m1e0m0 42403	Equality of two left-additive identities. See resubidaddlid 42401. Uses ax-i2m1 11220. (Contributed by SN, 25-Dec-2023.)
⊢ (1 −ℝ 1) = (0 −ℝ 0)
Theorem	sn-00idlem1 42404	Lemma for sn-00id 42407. (Contributed by SN, 25-Dec-2023.)
⊢ (𝐴 ∈ ℝ → (𝐴 · (0 −ℝ 0)) = (𝐴 −ℝ 𝐴))
Theorem	sn-00idlem2 42405	Lemma for sn-00id 42407. (Contributed by SN, 25-Dec-2023.)
⊢ ((0 −ℝ 0) ≠ 0 → (0 −ℝ 0) = 1)
Theorem	sn-00idlem3 42406	Lemma for sn-00id 42407. (Contributed by SN, 25-Dec-2023.)
⊢ ((0 −ℝ 0) = 1 → (0 + 0) = 0)
Theorem	sn-00id 42407	00id 11433 proven without ax-mulcom 11216 but using ax-1ne0 11221. (Though note that the current version of 00id 11433 can be changed to avoid ax-icn 11211, ax-addcl 11212, ax-mulcl 11214, ax-i2m1 11220, ax-cnre 11225. Most of this is by using 0cnALT3 42272 instead of 0cn 11250). (Contributed by SN, 25-Dec-2023.) (Proof modification is discouraged.)
⊢ (0 + 0) = 0
Theorem	re0m0e0 42408	Real number version of 0m0e0 12383 proven without ax-mulcom 11216. (Contributed by SN, 23-Jan-2024.)
⊢ (0 −ℝ 0) = 0
Theorem	readdlid 42409	Real number version of addlid 11441. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (0 + 𝐴) = 𝐴)
Theorem	sn-addlid 42410	addlid 11441 without ax-mulcom 11216. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
Theorem	remul02 42411	Real number version of mul02 11436 proven without ax-mulcom 11216. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (0 · 𝐴) = 0)
Theorem	sn-0ne2 42412	0ne2 12470 without ax-mulcom 11216. (Contributed by SN, 23-Jan-2024.)
⊢ 0 ≠ 2
Theorem	remul01 42413	Real number version of mul01 11437 proven without ax-mulcom 11216. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 · 0) = 0)
Theorem	resubid 42414	Subtraction of a real number from itself (compare subid 11525). (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 𝐴) = 0)
Theorem	readdrid 42415	Real number version of addrid 11438 without ax-mulcom 11216. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 + 0) = 𝐴)
Theorem	resubid1 42416	Real number version of subid1 11526 without ax-mulcom 11216. (Contributed by SN, 23-Jan-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 −ℝ 0) = 𝐴)
Theorem	renegneg 42417	A real number is equal to the negative of its negative. Compare negneg 11556. (Contributed by SN, 13-Feb-2024.)
⊢ (𝐴 ∈ ℝ → (0 −ℝ (0 −ℝ 𝐴)) = 𝐴)
Theorem	readdcan2 42418	Commuted version of readdcan 11432 without ax-mulcom 11216. (Contributed by SN, 21-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵))
Theorem	renegid2 42419	Commuted version of renegid 42379. (Contributed by SN, 4-May-2024.)
⊢ (𝐴 ∈ ℝ → ((0 −ℝ 𝐴) + 𝐴) = 0)
Theorem	remulneg2d 42420	Product with negative is negative of product. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 · (0 −ℝ 𝐵)) = (0 −ℝ (𝐴 · 𝐵)))
Theorem	sn-it0e0 42421	Proof of it0e0 12485 without ax-mulcom 11216. Informally, a real number times 0 is 0, and ∃𝑟 ∈ ℝ𝑟 = i · 𝑠 by ax-cnre 11225 and renegid2 42419. (Contributed by SN, 30-Apr-2024.)
⊢ (i · 0) = 0
Theorem	sn-negex12 42422*	A combination of cnegex 11439 and cnegex2 11440, this proof takes cnre 11255 𝐴 = 𝑟 + 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 42423*	Proof of cnegex 11439 without ax-mulcom 11216. (Contributed by SN, 30-Apr-2024.)
⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝐴 + 𝑏) = 0)
Theorem	sn-negex2 42424*	Proof of cnegex2 11440 without ax-mulcom 11216. (Contributed by SN, 5-May-2024.)
⊢ (𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝑏 + 𝐴) = 0)
Theorem	sn-addcand 42425	addcand 11461 without ax-mulcom 11216. Note how the proof is almost identical to addcan 11442. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶))
Theorem	sn-addrid 42426	addrid 11438 without ax-mulcom 11216. (Contributed by SN, 5-May-2024.)
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
Theorem	sn-addcan2d 42427	addcan2d 11462 without ax-mulcom 11216. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵))
Theorem	reixi 42428	ixi 11889 without ax-mulcom 11216. (Contributed by SN, 5-May-2024.)
⊢ (i · i) = (0 −ℝ 1)
Theorem	rei4 42429	i4 14239 without ax-mulcom 11216. (Contributed by SN, 27-May-2024.)
⊢ ((i · i) · (i · i)) = 1
Theorem	sn-addid0 42430	A number that sums to itself is zero. Compare addid0 11679, readdridaddlidd 42277. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐴) = 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	sn-mul01 42431	mul01 11437 without ax-mulcom 11216. (Contributed by SN, 5-May-2024.)
⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0)
Theorem	sn-subeu 42432*	negeu 11495 without ax-mulcom 11216 and complex number version of resubeu 42383. (Contributed by SN, 5-May-2024.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐴 + 𝑥) = 𝐵)
Theorem	sn-subcl 42433	subcl 11504 without ax-mulcom 11216. (Contributed by SN, 5-May-2024.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
Theorem	sn-subf 42434	subf 11507 without ax-mulcom 11216. (Contributed by SN, 5-May-2024.)
⊢ − :(ℂ × ℂ)⟶ℂ
Theorem	resubeqsub 42435	Equivalence between real subtraction and subtraction. (Contributed by SN, 5-May-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (𝐴 − 𝐵))
Theorem	subresre 42436	Subtraction restricted to the reals. (Contributed by SN, 5-May-2024.)
⊢ −ℝ = ( − ↾ (ℝ × ℝ))
Theorem	addinvcom 42437	A number commutes with its additive inverse. Compare remulinvcom 42438. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 0)    ⇒   ⊢ (𝜑 → (𝐵 + 𝐴) = 0)
Theorem	remulinvcom 42438	A left multiplicative inverse is a right multiplicative inverse. Proven without ax-mulcom 11216. (Contributed by SN, 5-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 · 𝐵) = 1)    ⇒   ⊢ (𝜑 → (𝐵 · 𝐴) = 1)
Theorem	remullid 42439	Commuted version of ax-1rid 11222 without ax-mulcom 11216. (Contributed by SN, 5-Feb-2024.)
⊢ (𝐴 ∈ ℝ → (1 · 𝐴) = 𝐴)
Theorem	sn-1ticom 42440	Lemma for sn-mullid 42441 and sn-it1ei 42442. (Contributed by SN, 27-May-2024.)
⊢ (1 · i) = (i · 1)
Theorem	sn-mullid 42441	mullid 11257 without ax-mulcom 11216. (Contributed by SN, 27-May-2024.)
⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
Theorem	sn-it1ei 42442	it1ei 42329 without ax-mulcom 11216. (See sn-mullid 42441 for commuted version). (Contributed by SN, 1-Jun-2024.)
⊢ (i · 1) = i
Theorem	ipiiie0 42443	The multiplicative inverse of i (per i4 14239) is also its additive inverse. (Contributed by SN, 30-Jun-2024.)
⊢ (i + (i · (i · i))) = 0
Theorem	remulcand 42444	Commuted version of remulcan2d 42276 without ax-mulcom 11216. (Contributed by SN, 21-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵))
Theorem	sn-0tie0 42445	Lemma for sn-mul02 42446. Commuted version of sn-it0e0 42421. (Contributed by SN, 30-Jun-2024.)
⊢ (0 · i) = 0
Theorem	sn-mul02 42446	mul02 11436 without ax-mulcom 11216. See https://github.com/icecream17/Stuff/blob/main/math/0A%3D0.md 11216 for an outline. (Contributed by SN, 30-Jun-2024.)
⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0)
Theorem	sn-ltaddpos 42447	ltaddpos 11750 without ax-mulcom 11216. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴)))
Theorem	sn-ltaddneg 42448	ltaddneg 11474 without ax-mulcom 11216. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ (𝐵 + 𝐴) < 𝐵))
Theorem	reposdif 42449	Comparison of two numbers whose difference is positive. Compare posdif 11753. (Contributed by SN, 13-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 −ℝ 𝐴)))
Theorem	relt0neg1 42450	Comparison of a real and its negative to zero. Compare lt0neg1 11766. (Contributed by SN, 13-Feb-2024.)
⊢ (𝐴 ∈ ℝ → (𝐴 < 0 ↔ 0 < (0 −ℝ 𝐴)))
Theorem	relt0neg2 42451	Comparison of a real and its negative to zero. Compare lt0neg2 11767. (Contributed by SN, 13-Feb-2024.)
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ (0 −ℝ 𝐴) < 0))
Theorem	sn-addlt0d 42452	The sum of negative numbers is negative. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    &   ⊢ (𝜑 → 𝐵 < 0)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) < 0)
Theorem	sn-addgt0d 42453	The sum of positive numbers is positive. Proof of addgt0d 11835 without ax-mulcom 11216. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → 0 < (𝐴 + 𝐵))
Theorem	sn-nnne0 42454	nnne0 12297 without ax-mulcom 11216. (Contributed by SN, 25-Jan-2025.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)
Theorem	reelznn0nn 42455	elznn0nn 12624 restated using df-resub 42372. (Contributed by SN, 25-Jan-2025.)
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ (0 −ℝ 𝑁) ∈ ℕ)))
Theorem	nn0addcom 42456	Addition is commutative for nonnegative integers. Proven without ax-mulcom 11216. (Contributed by SN, 1-Feb-2025.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	zaddcomlem 42457	Lemma for zaddcom 42458. (Contributed by SN, 1-Feb-2025.)
⊢ (((𝐴 ∈ ℝ ∧ (0 −ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	zaddcom 42458	Addition is commutative for integers. Proven without ax-mulcom 11216. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	renegmulnnass 42459	Move multiplication by a natural number inside and outside negation. (Contributed by SN, 25-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((0 −ℝ 𝐴) · 𝑁) = (0 −ℝ (𝐴 · 𝑁)))
Theorem	nn0mulcom 42460	Multiplication is commutative for nonnegative integers. Proven without ax-mulcom 11216. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	zmulcomlem 42461	Lemma for zmulcom 42462. (Contributed by SN, 25-Jan-2025.)
⊢ (((𝐴 ∈ ℝ ∧ (0 −ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	zmulcom 42462	Multiplication is commutative for integers. Proven without ax-mulcom 11216. From this result and grpcominv1 42494, we can show that rationals commute under multiplication without using ax-mulcom 11216. (Contributed by SN, 25-Jan-2025.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	mulgt0con1dlem 42463	Lemma for mulgt0con1d 42464. Contraposes a positive deduction to a negative deduction. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (0 < 𝐴 → 0 < 𝐵))    &   ⊢ (𝜑 → (𝐴 = 0 → 𝐵 = 0))    ⇒   ⊢ (𝜑 → (𝐵 < 0 → 𝐴 < 0))
Theorem	mulgt0con1d 42464	Counterpart to mulgt0con2d 42465, though not a lemma of anything. This is the first use of ax-pre-mulgt0 11229. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐵)    &   ⊢ (𝜑 → (𝐴 · 𝐵) < 0)    ⇒   ⊢ (𝜑 → 𝐴 < 0)
Theorem	mulgt0con2d 42465	Lemma for mulgt0b2d 42466 and contrapositive of mulgt0 11335. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → (𝐴 · 𝐵) < 0)    ⇒   ⊢ (𝜑 → 𝐵 < 0)
Theorem	mulgt0b2d 42466	Biconditional, deductive form of mulgt0 11335. The second factor is positive iff the product is. Note that the commuted form cannot be proven since resubdi 42402 does not have a commuted form. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → (0 < 𝐵 ↔ 0 < (𝐴 · 𝐵)))
Theorem	sn-ltmul2d 42467	ltmul2d 13116 without ax-mulcom 11216. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐶)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) < (𝐶 · 𝐵) ↔ 𝐴 < 𝐵))
Theorem	sn-ltmulgt11d 42468	ltmulgt11d 13109 without ax-mulcom 11216. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → (1 < 𝐴 ↔ 𝐵 < (𝐵 · 𝐴)))
Theorem	sn-0lt1 42469	0lt1 11782 without ax-mulcom 11216. (Contributed by SN, 13-Feb-2024.)
⊢ 0 < 1
Theorem	sn-ltp1 42470	ltp1 12104 without ax-mulcom 11216. (Contributed by SN, 13-Feb-2024.)
⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1))
Theorem	sn-mulgt1d 42471	mulgt1d 12201 without ax-mulcom 11216. (Contributed by SN, 26-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 1 < 𝐴)    &   ⊢ (𝜑 → 1 < 𝐵)    ⇒   ⊢ (𝜑 → 1 < (𝐴 · 𝐵))
Theorem	reneg1lt0 42472	Lemma for sn-inelr 42473. (Contributed by SN, 1-Jun-2024.)
⊢ (0 −ℝ 1) < 0
Theorem	sn-inelr 42473	inelr 12253 without ax-mulcom 11216. (Contributed by SN, 1-Jun-2024.)
⊢ ¬ i ∈ ℝ
Theorem	sn-itrere 42474	i times a real is real iff the real is zero. (Contributed by SN, 27-Jun-2024.)
⊢ (𝑅 ∈ ℝ → ((i · 𝑅) ∈ ℝ ↔ 𝑅 = 0))
Theorem	sn-retire 42475	Commuted version of sn-itrere 42474. (Contributed by SN, 27-Jun-2024.)
⊢ (𝑅 ∈ ℝ → ((𝑅 · i) ∈ ℝ ↔ 𝑅 = 0))
Theorem	cnreeu 42476	The reals in the expression given by cnre 11255 uniquely define a complex number. (Contributed by SN, 27-Jun-2024.)
⊢ (𝜑 → 𝑟 ∈ ℝ)    &   ⊢ (𝜑 → 𝑠 ∈ ℝ)    &   ⊢ (𝜑 → 𝑡 ∈ ℝ)    &   ⊢ (𝜑 → 𝑢 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑟 + (i · 𝑠)) = (𝑡 + (i · 𝑢)) ↔ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
Theorem	sn-sup2 42477*	sup2 12221 with exactly the same proof except for using sn-ltp1 42470 instead of ltp1 12104, saving ax-mulcom 11216. (Contributed by SN, 26-Jun-2024.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	sn-sup3d 42478*	sup3 12222 without ax-mulcom 11216, proven trivially from sn-sup2 42477. (Contributed by SN, 29-Jun-2025.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	sn-suprcld 42479*	suprcld 12228 without ax-mulcom 11216, proven trivially from sn-sup3d 42478. (Contributed by SN, 29-Jun-2025.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ)
Theorem	sn-suprubd 42480*	suprubd 12227 without ax-mulcom 11216, proven trivially from sn-suprcld 42479. (Contributed by SN, 29-Jun-2025.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ, < ))
21.30.6  Structures
Theorem	sn-base0 42481	Avoid axioms in base0 17249 by using the discouraged df-base 17245. 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 42482	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 42483	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 42484	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 42485	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 42486	The vectors of a finite free module are the functions from 𝐼 to 𝑁. (Contributed by SN, 31-Aug-2023.)
⊢ 𝐹 = (𝑅 freeLMod 𝐼)    &   ⊢ 𝑁 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝐹)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin) → (𝑋 ∈ 𝐵 ↔ 𝑋:𝐼⟶𝑁))
Theorem	frlmfzwrd 42487	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 42488	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 42489	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 42490	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 42491	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 42492	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 42493	An associative cancellation law for groups. (Contributed by SN, 29-Jan-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + (𝑁‘𝑌)) + 𝑌) = 𝑋)
Theorem	grpcominv1 42494	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 42495	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 42496	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 42497	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 42498	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 42499	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 42500	The image of a commutative ring homomorphism is a commutative ring. (Contributed by SN, 10-Jan-2025.)
⊢ 𝐶 = (𝑁 ↾s (𝐹 “ 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑀 RingHom 𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑀))    ⇒   ⊢ (𝜑 → 𝐶 ∈ CRing)