P. 424 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42301-42400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	unitscyglem4 42301*	Lemma for unitscyg (Contributed by metakunt, 14-Jul-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ↑ = (.g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∥ (♯‘𝐵))    ⇒   ⊢ (𝜑 → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷))
Theorem	unitscyglem5 42302	Lemma for unitscyg (Contributed by metakunt, 9-Aug-2025.)
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → (Base‘𝑅) ∈ Fin)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∥ (♯‘(Base‘𝐺)))    ⇒   ⊢ (𝜑 → ((mulGrp‘𝑅) PrimRoots 𝐷) ≠ ∅)
Theorem	aks5lem7 42303*	Lemma for aks5. We clean up the hypotheses compared to aks5lem6 42295. (Contributed by metakunt, 9-Aug-2025.)
⊢ (𝜑 → (♯‘(Base‘𝐾)) ∈ ℕ)    &   ⊢ 𝑃 = (chr‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Field)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → 𝑃 ∥ 𝑁)    &   ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1)    &   ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁)))    &   ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁))    &   ⊢ (𝜑 → 𝑅 ∥ ((♯‘(Base‘𝐾)) − 1))    &   ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)[(𝑁(.g‘(mulGrp‘𝑆))(𝑋(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎)))](𝑆 ~QG 𝐿) = [((𝑁(.g‘(mulGrp‘𝑆))𝑋)(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎))](𝑆 ~QG 𝐿))    &   ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1)    &   ⊢ 𝑆 = (Poly1‘(ℤ/nℤ‘𝑁))    &   ⊢ 𝐿 = ((RSpan‘𝑆)‘{((𝑅(.g‘(mulGrp‘𝑆))𝑋)(-g‘𝑆)(1r‘𝑆))})    &   ⊢ 𝑋 = (var1‘(ℤ/nℤ‘𝑁))    ⇒   ⊢ (𝜑 → 𝑁 = (𝑃↑(𝑃 pCnt 𝑁)))
Theorem	aks5lem8 42304*	Lemma for aks5. Clean up the conclusion. (Contributed by metakunt, 9-Aug-2025.)
⊢ (𝜑 → (♯‘(Base‘𝐾)) ∈ ℕ)    &   ⊢ 𝑃 = (chr‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Field)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → 𝑃 ∥ 𝑁)    &   ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1)    &   ⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁)))    &   ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁))    &   ⊢ (𝜑 → 𝑅 ∥ ((♯‘(Base‘𝐾)) − 1))    &   ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)[(𝑁(.g‘(mulGrp‘𝑆))(𝑋(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎)))](𝑆 ~QG 𝐿) = [((𝑁(.g‘(mulGrp‘𝑆))𝑋)(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎))](𝑆 ~QG 𝐿))    &   ⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1)    &   ⊢ 𝑆 = (Poly1‘(ℤ/nℤ‘𝑁))    &   ⊢ 𝐿 = ((RSpan‘𝑆)‘{((𝑅(.g‘(mulGrp‘𝑆))𝑋)(-g‘𝑆)(1r‘𝑆))})    &   ⊢ 𝑋 = (var1‘(ℤ/nℤ‘𝑁))    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑛 ∈ ℕ 𝑁 = (𝑝↑𝑛))
Axiom	ax-exfinfld 42305*	Existence axiom for finite fields, eventually we want to construct them. (Contributed by metakunt, 13-Jul-2025.)
⊢ ∀𝑝 ∈ ℙ ∀𝑛 ∈ ℕ ∃𝑘 ∈ Field ((♯‘(Base‘𝑘)) = (𝑝↑𝑛) ∧ (chr‘𝑘) = 𝑝)
Theorem	exfinfldd 42306*	For any prime 𝑃 and any positive integer 𝑁 there exists a field 𝑘 such that 𝑘 contains 𝑃↑𝑁 elements. (Contributed by metakunt, 13-Jul-2025.)
⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ Field ((♯‘(Base‘𝑘)) = (𝑃↑𝑁) ∧ (chr‘𝑘) = 𝑃))
Theorem	aks5 42307*	The AKS Primality test, given an integer 𝑁 greater than or equal to 3, find a coprime 𝑅 such that 𝑅 is big enough. Then, if a bunch of polynomial equalities in the residue ring hold then 𝑁 is a prime power. Currently depends on the axiom ax-exfinfld 42305, since we currently do not have the existence of finite fields in the database. (Contributed by metakunt, 16-Aug-2025.)
⊢ 𝐴 = (⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁)))    &   ⊢ 𝑋 = (var1‘(ℤ/nℤ‘𝑁))    &   ⊢ 𝑆 = (Poly1‘(ℤ/nℤ‘𝑁))    &   ⊢ 𝐿 = ((RSpan‘𝑆)‘{((𝑅(.g‘(mulGrp‘𝑆))𝑋)(-g‘𝑆)(1r‘𝑆))})    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → (𝑁 gcd 𝑅) = 1)    &   ⊢ (𝜑 → ((2 logb 𝑁)↑2) < ((odℤ‘𝑅)‘𝑁))    &   ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)[(𝑁(.g‘(mulGrp‘𝑆))(𝑋(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎)))](𝑆 ~QG 𝐿) = [((𝑁(.g‘(mulGrp‘𝑆))𝑋)(+g‘𝑆)((ℤRHom‘𝑆)‘𝑎))](𝑆 ~QG 𝐿))    &   ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)(𝑎 gcd 𝑁) = 1)    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑛 ∈ ℕ 𝑁 = (𝑝↑𝑛))
21.30  Mathbox for Steven Nguyen
21.30.1  Utility theorems
Theorem	jarrii 42308	Inference associated with jarri 107. A consequence of ax-mp 5 and ax-1 6. (Contributed by SN, 14-Oct-2025.)
⊢ 𝜓    &   ⊢ ((𝜑 → 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	intnanrt 42309	Introduction of conjunct inside of a contradiction. Would be used in elfvov1 7397. (Contributed by SN, 18-May-2025.)
⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓))
Theorem	ioin9i8 42310	Miscellaneous inference creating a biconditional from an implied converse implication. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    &   ⊢ (𝜒 → ¬ 𝜃)    &   ⊢ (𝜓 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜃))
Theorem	jaodd 42311	Double deduction form of jaoi 857. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜏) → 𝜃)))
Theorem	syl3an12 42312	A double syllogism inference. (Contributed by SN, 15-Sep-2024.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
Theorem	exbiii 42313	Inference associated with exbii 1849. Weaker version of eximii 1838. (Contributed by SN, 14-Oct-2025.)
⊢ ∃𝑥𝜑    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ∃𝑥𝜓
Theorem	sbtd 42314*	A true statement is true upon substitution (deduction). A similar proof is possible for icht 47566. (Contributed by SN, 4-May-2024.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → [𝑡 / 𝑥]𝜓)
Theorem	sbor2 42315	One direction of sbor 2310, using fewer axioms. Compare 19.33 1885. (Contributed by Steven Nguyen, 18-Aug-2023.)
⊢ (([𝑡 / 𝑥]𝜑 ∨ [𝑡 / 𝑥]𝜓) → [𝑡 / 𝑥](𝜑 ∨ 𝜓))
Theorem	sbalexi 42316*	Inference form of sbalex 2247, avoiding ax-10 2146 by using ax-gen 1796. (Contributed by SN, 12-Aug-2025.)
⊢ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)    ⇒   ⊢ ∀𝑥(𝑥 = 𝑦 → 𝜑)
Theorem	nfexhe 42317	Version of nfex 2327 with the existential dual to the 'h' hypothesis, avoiding ax-12 2182. (Contributed by SN, 11-Feb-2026.)
⊢ (∃𝑥𝜑 → 𝜑)    ⇒   ⊢ Ⅎ𝑥∃𝑦𝜑
Theorem	nfalh 42318	Version of nfal 2326 with an 'h' hypothesis, avoiding ax-12 2182. (Contributed by SN, 11-Feb-2026.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ Ⅎ𝑥∀𝑦𝜑
Theorem	nfe2 42319	An inner existential quantifier's variable is bound. (Contributed by SN, 11-Feb-2026.)
⊢ Ⅎ𝑥∃𝑦∃𝑥𝜑
Theorem	nfale2 42320	An inner existential quantifier's variable is bound. (Contributed by SN, 11-Feb-2026.)
⊢ Ⅎ𝑥∀𝑦∃𝑥𝜑
Theorem	nfexa2 42321	An inner universal quantifier's variable is bound. (Contributed by SN, 11-Feb-2026.)
⊢ Ⅎ𝑥∃𝑦∀𝑥𝜑
Theorem	19.9dev 42322*	19.9d 2208 in the case of an existential quantifier, avoiding the ax-10 2146 from nfex 2327 that would be used for the hypothesis of 19.9d 2208, at the cost of an additional DV condition on 𝑦, 𝜑. (Contributed by SN, 26-May-2024.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑦𝜓))
Theorem	3rspcedvd 42323*	Triple application of rspcedvd 3576. (Contributed by Steven Nguyen, 27-Feb-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → (𝜒 ↔ 𝜃))    &   ⊢ ((𝜑 ∧ 𝑧 = 𝐶) → (𝜃 ↔ 𝜏))    &   ⊢ (𝜑 → 𝜏)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 ∃𝑧 ∈ 𝐷 𝜓)
Theorem	sn-axrep5v 42324*	A condensed form of axrep5 5229. (Contributed by SN, 21-Sep-2023.)
⊢ (∀𝑤 ∈ 𝑥 ∃*𝑧𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 𝜑))
Theorem	sn-axprlem3 42325*	axprlem3 5367 using only Tarski's FOL axiom schemes and ax-rep 5221. (Contributed by SN, 22-Sep-2023.)
⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 if-(𝜑, 𝑧 = 𝑎, 𝑧 = 𝑏))
Theorem	sn-exelALT 42326*	Alternate proof of exel 5380, avoiding ax-pr 5374 but requiring ax-5 1911, ax-9 2123, and ax-pow 5307. This is similar to how elALT2 5311 uses ax-pow 5307 instead of ax-pr 5374 compared to el 5384. (Contributed by SN, 18-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦
Theorem	ss2ab1 42327	Class abstractions in a subclass relationship, closed form. One direction of ss2ab 4011 using fewer axioms. (Contributed by SN, 22-Dec-2024.)
⊢ (∀𝑥(𝜑 → 𝜓) → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓})
Theorem	ssabdv 42328*	Deduction of abstraction subclass from implication. (Contributed by SN, 22-Dec-2024.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ {𝑥 ∣ 𝜓})
Theorem	sn-iotalem 42329*	An unused lemma showing that many equivalences involving df-iota 6445 are potentially provable without ax-10 2146, ax-11 2162, ax-12 2182. (Contributed by SN, 6-Nov-2024.)
⊢ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑧 ∣ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑧}}
Theorem	sn-iotalemcor 42330*	Corollary of sn-iotalem 42329. Compare sb8iota 6456. (Contributed by SN, 6-Nov-2024.)
⊢ (℩𝑥𝜑) = (℩𝑦{𝑥 ∣ 𝜑} = {𝑦})
Theorem	abbi1sn 42331*	Originally part of uniabio 6459. Convert a theorem about df-iota 6445 to one about dfiota2 6446, without ax-10 2146, ax-11 2162, ax-12 2182. Although, eu6 2571 uses ax-10 2146 and ax-12 2182. (Contributed by SN, 23-Nov-2024.)
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → {𝑥 ∣ 𝜑} = {𝑦})
Theorem	brif2 42332	Move a relation inside and outside the conditional operator. (Contributed by SN, 14-Aug-2024.)
⊢ (𝐶𝑅if(𝜑, 𝐴, 𝐵) ↔ if-(𝜑, 𝐶𝑅𝐴, 𝐶𝑅𝐵))
Theorem	brif12 42333	Move a relation inside and outside the conditional operator. (Contributed by SN, 14-Aug-2024.)
⊢ (if(𝜑, 𝐴, 𝐵)𝑅if(𝜑, 𝐶, 𝐷) ↔ if-(𝜑, 𝐴𝑅𝐶, 𝐵𝑅𝐷))
Theorem	pssexg 42334	The proper subset of a set is also a set. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
Theorem	pssn0 42335	A proper superset is nonempty. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ (𝐴 ⊊ 𝐵 → 𝐵 ≠ ∅)
Theorem	psspwb 42336	Classes are proper subclasses if and only if their power classes are proper subclasses. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ (𝐴 ⊊ 𝐵 ↔ 𝒫 𝐴 ⊊ 𝒫 𝐵)
Theorem	xppss12 42337	Proper subset theorem for Cartesian product. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐶 ⊊ 𝐷) → (𝐴 × 𝐶) ⊊ (𝐵 × 𝐷))
Theorem	elpwbi 42338	Membership in a power set, biconditional. (Contributed by Steven Nguyen, 17-Jul-2022.) (Proof shortened by Steven Nguyen, 16-Sep-2022.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ 𝒫 𝐵)
Theorem	imaopab 42339*	The image of a class of ordered pairs. (Contributed by Steven Nguyen, 6-Jun-2023.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} “ 𝐴) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑}
Theorem	eqresfnbd 42340	Property of being the restriction of a function. Note that this is closer to funssres 6533 than fnssres 6612. (Contributed by SN, 11-Mar-2025.)
⊢ (𝜑 → 𝐹 Fn 𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑅 = (𝐹 ↾ 𝐴) ↔ (𝑅 Fn 𝐴 ∧ 𝑅 ⊆ 𝐹)))
Theorem	f1o2d2 42341*	Sufficient condition for a binary function expressed in maps-to notation to be bijective. (Contributed by SN, 11-Mar-2025.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → 𝐼 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → 𝐽 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐷)) → ((𝑥 = 𝐼 ∧ 𝑦 = 𝐽) ↔ 𝑧 = 𝐶))    ⇒   ⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷)
Theorem	fmpocos 42342*	Composition of two functions. Variation of fmpoco 8034 with more context in the substitution hypothesis for 𝑇. (Contributed by SN, 14-Mar-2025.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅))    &   ⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐶 ↦ 𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ⦋𝑅 / 𝑧⦌𝑆 = 𝑇)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇))
Theorem	ovmpogad 42343*	Value of an operation given by a maps-to rule. Deduction form of ovmpoga 7509. (Contributed by SN, 14-Mar-2025.)
⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Theorem	ofun 42344	A function operation of unions of disjoint functions is a union of function operations. (Contributed by SN, 16-Jun-2024.)
⊢ (𝜑 → 𝐴 Fn 𝑀)    &   ⊢ (𝜑 → 𝐵 Fn 𝑀)    &   ⊢ (𝜑 → 𝐶 Fn 𝑁)    &   ⊢ (𝜑 → 𝐷 Fn 𝑁)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑀 ∩ 𝑁) = ∅)    ⇒   ⊢ (𝜑 → ((𝐴 ∪ 𝐶) ∘f 𝑅(𝐵 ∪ 𝐷)) = ((𝐴 ∘f 𝑅𝐵) ∪ (𝐶 ∘f 𝑅𝐷)))
Theorem	dfqs2 42345*	Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.)
⊢ (𝐴 / 𝑅) = ran (𝑥 ∈ 𝐴 ↦ [𝑥]𝑅)
Theorem	dfqs3 42346*	Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.)
⊢ (𝐴 / 𝑅) = ∪ 𝑥 ∈ 𝐴 {[𝑥]𝑅}
Theorem	qseq12d 42347	Equality theorem for quotient set, deduction form. (Contributed by Steven Nguyen, 30-Apr-2023.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐷))
Theorem	qsalrel 42348*	The quotient set is equal to the singleton of 𝐴 when all elements are related and 𝐴 is nonempty. (Contributed by SN, 8-Jun-2023.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∼ 𝑦)    &   ⊢ (𝜑 → ∼ Er 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐴 / ∼ ) = {𝐴})
Theorem	elmapssresd 42349	A restricted mapping is a mapping. EDITORIAL: Could be used to shorten elpm2r 8778 with some reordering involving mapsspm 8809. (Contributed by SN, 11-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m 𝐶))    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ↾ 𝐷) ∈ (𝐵 ↑m 𝐷))
Theorem	supinf 42350*	The supremum is the infimum of the upper bounds. (Contributed by SN, 29-Jun-2025.)
⊢ (𝜑 → < Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐵 𝑦 < 𝑧)))    ⇒   ⊢ (𝜑 → sup(𝐵, 𝐴, < ) = inf({𝑥 ∈ 𝐴 ∣ ∀𝑤 ∈ 𝐵 ¬ 𝑥 < 𝑤}, 𝐴, < ))
Theorem	mapcod 42351	Compose two mappings. (Contributed by SN, 11-Mar-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐴 ↑m 𝐵))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐵 ↑m 𝐶))    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ (𝐴 ↑m 𝐶))
Theorem	fisdomnn 42352	A finite set is dominated by the set of natural numbers. (Contributed by SN, 6-Jul-2025.)
⊢ (𝐴 ∈ Fin → 𝐴 ≺ ℕ)
Theorem	ltex 42353	The less-than relation is a set. (Contributed by SN, 5-Jun-2025.)
⊢ < ∈ V
Theorem	leex 42354	The less-than-or-equal-to relation is a set. (Contributed by SN, 5-Jun-2025.)
⊢ ≤ ∈ V
Theorem	subex 42355	The subtraction operation is a set. (Contributed by SN, 5-Jun-2025.)
⊢ − ∈ V
Theorem	absex 42356	The absolute value function is a set. (Contributed by SN, 5-Jun-2025.)
⊢ abs ∈ V
Theorem	cjex 42357	The conjugate function is a set. (Contributed by SN, 5-Jun-2025.)
⊢ ∗ ∈ V
Theorem	fzosumm1 42358*	Separate out the last term in a finite sum. (Contributed by Steven Nguyen, 22-Aug-2023.)
⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝑘 = (𝑁 − 1) → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝐴 = (Σ𝑘 ∈ (𝑀..^(𝑁 − 1))𝐴 + 𝐵))
Theorem	ccatcan2d 42359	Cancellation law for concatenation. (Contributed by SN, 6-Sep-2023.)
⊢ (𝜑 → 𝐴 ∈ Word 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ Word 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ Word 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 ++ 𝐶) = (𝐵 ++ 𝐶) ↔ 𝐴 = 𝐵))
21.30.2  Arithmetic theorems Towards the start of this section are several proofs regarding the different complex number axioms that could be used to prove some results. For example, ax-1rid 11086 is used in mulrid 11120 related theorems, so one could trade off the extra axioms in mulrid 11120 for the axioms needed to prove that something is a real number. Another example is avoiding complex number closure laws by using real number closure laws and then using ax-resscn 11073; in the other direction, real number closure laws can be avoided by using ax-resscn 11073 and then the complex number closure laws. (This only works if the result of (𝐴 + 𝐵) only needs to be a complex number). The natural numbers are especially amenable to axiom reductions, as the set ℕ is the recursive set {1, (1 + 1), ((1 + 1) + 1)}, etc., i.e. the set of numbers formed by only additions of 1. The digits 2 through 9 are defined so that they expand into additions of 1. This conveniently allows for adding natural numbers by rearranging parentheses, as shown below: (4 + 3) = 7 ((3 + 1) + (2 + 1)) = (6 + 1) ((((1 + 1) + 1) + 1) + ((1 + 1) + 1)) = ((((((1 + 1) + 1) + 1) + 1) + 1) + 1) This only requires ax-addass 11081, ax-1cn 11074, and ax-addcl 11076. (And in practice, the expression isn't fully expanded into ones.) Multiplication by 1 requires either mullidi 11127 or (ax-1rid 11086 and 1re 11122) as seen in 1t1e1 12292 and 1t1e1ALT 42363. Multiplying with greater natural numbers uses ax-distr 11083. Still, this takes fewer axioms than adding zero, which is often implicit in theorems such as (9 + 1) = ;10. Adding zero uses almost every complex number axiom, though notably not ax-mulcom 11080 (see readdrid 42518 and readdlid 42511).
Theorem	c0exALT 42360	Alternate proof of c0ex 11116 using more set theory axioms but fewer complex number axioms (add ax-10 2146, ax-11 2162, ax-13 2374, ax-nul 5248, and remove ax-1cn 11074, ax-icn 11075, ax-addcl 11076, and ax-mulcl 11078). (Contributed by Steven Nguyen, 4-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 ∈ V
Theorem	0cnALT3 42361	Alternate proof of 0cn 11114 using ax-resscn 11073, ax-addrcl 11077, ax-rnegex 11087, ax-cnre 11089 instead of ax-icn 11075, ax-addcl 11076, ax-mulcl 11078, ax-i2m1 11084. Version of 0cnALT 11358 using ax-1cn 11074 instead of ax-icn 11075. (Contributed by Steven Nguyen, 7-Jan-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 ∈ ℂ
Theorem	elre0re 42362	Specialized version of 0red 11125 without using ax-1cn 11074 and ax-cnre 11089. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ (𝐴 ∈ ℝ → 0 ∈ ℝ)
Theorem	1t1e1ALT 42363	Alternate proof of 1t1e1 12292 using a different set of axioms (add ax-mulrcl 11079, ax-i2m1 11084, ax-1ne0 11085, ax-rrecex 11088 and remove ax-resscn 11073, ax-mulcom 11080, ax-mulass 11082, ax-distr 11083). (Contributed by Steven Nguyen, 20-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (1 · 1) = 1
Theorem	lttrii 42364	'Less than' is transitive. (Contributed by SN, 26-Aug-2025.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 𝐴 < 𝐵    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ 𝐴 < 𝐶
Theorem	remulcan2d 42365	mulcan2d 11761 for real numbers using fewer axioms. (Contributed by Steven Nguyen, 15-Apr-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵))
Theorem	readdridaddlidd 42366	Given some real number 𝐵 where 𝐴 acts like a right additive identity, derive that 𝐴 is a left additive identity. Note that the hypothesis is weaker than proving that 𝐴 is a right additive identity (for all numbers). Although, if there is a right additive identity, then by readdcan 11297, 𝐴 is the right additive identity. (Contributed by Steven Nguyen, 14-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐵 + 𝐴) = 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ ℝ) → (𝐴 + 𝐶) = 𝐶)
Theorem	1p3e4 42367	1 + 3 = 4. (Contributed by SN, 19-Nov-2025.)
⊢ (1 + 3) = 4
Theorem	5ne0 42368	The number 5 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 5 ≠ 0
Theorem	6ne0 42369	The number 6 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 6 ≠ 0
Theorem	7ne0 42370	The number 7 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 7 ≠ 0
Theorem	8ne0 42371	The number 8 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 8 ≠ 0
Theorem	9ne0 42372	The number 9 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 9 ≠ 0
Theorem	sn-1ne2 42373	A proof of 1ne2 12338 without using ax-mulcom 11080, ax-mulass 11082, ax-pre-mulgt0 11093. Based on mul02lem2 11300. (Contributed by SN, 13-Dec-2023.)
⊢ 1 ≠ 2
Theorem	nnn1suc 42374*	A positive integer that is not 1 is a successor of some other positive integer. (Contributed by Steven Nguyen, 19-Aug-2023.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ≠ 1) → ∃𝑥 ∈ ℕ (𝑥 + 1) = 𝐴)
Theorem	nnadd1com 42375	Addition with 1 is commutative for natural numbers. (Contributed by Steven Nguyen, 9-Dec-2022.)
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) = (1 + 𝐴))
Theorem	nnaddcom 42376	Addition is commutative for natural numbers. Uses fewer axioms than addcom 11309. (Contributed by Steven Nguyen, 9-Dec-2022.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	nnaddcomli 42377	Version of addcomli 11315 for natural numbers. (Contributed by Steven Nguyen, 1-Aug-2023.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ (𝐴 + 𝐵) = 𝐶    ⇒   ⊢ (𝐵 + 𝐴) = 𝐶
Theorem	nnadddir 42378	Right-distributivity for natural numbers without ax-mulcom 11080. (Contributed by SN, 5-Feb-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	nnmul1com 42379	Multiplication with 1 is commutative for natural numbers, without ax-mulcom 11080. Since (𝐴 · 1) is 𝐴 by ax-1rid 11086, this is equivalent to remullid 42542 for natural numbers, but using fewer axioms (avoiding ax-resscn 11073, ax-addass 11081, ax-mulass 11082, ax-rnegex 11087, ax-pre-lttri 11090, ax-pre-lttrn 11091, ax-pre-ltadd 11092). (Contributed by SN, 5-Feb-2024.)
⊢ (𝐴 ∈ ℕ → (1 · 𝐴) = (𝐴 · 1))
Theorem	nnmulcom 42380	Multiplication is commutative for natural numbers. (Contributed by SN, 5-Feb-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	readdrcl2d 42381	Reverse closure for addition: the second addend is real if the first addend is real and the sum is real. (Contributed by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐵 ∈ ℝ)
Theorem	mvrrsubd 42382	Move a subtraction in the RHS to a right-addition in the LHS. Converse of mvlraddd 11537. EDITORIAL: Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = (𝐵 − 𝐶))    ⇒   ⊢ (𝜑 → (𝐴 + 𝐶) = 𝐵)
Theorem	laddrotrd 42383	Rotate the variables right in an equation with addition on the left, converting it into a subtraction. Version of mvlladdd 11538 with a commuted consequent, and of mvrladdd 11540 with a commuted hypothesis. EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: ply1dg3rt0irred 33557. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → (𝐶 − 𝐴) = 𝐵)
Theorem	raddswap12d 42384	Swap the first two variables in an equation with addition on the right, converting it into a subtraction. Version of mvrraddd 11539 with a commuted consequent, and of mvlraddd 11537 with a commuted hypothesis. EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = (𝐵 + 𝐶))    ⇒   ⊢ (𝜑 → 𝐵 = (𝐴 − 𝐶))
Theorem	lsubrotld 42385	Rotate the variables left in an equation with subtraction on the left, converting it into an addition. EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → (𝐵 + 𝐶) = 𝐴)
Theorem	rsubrotld 42386	Rotate the variables left in an equation with subtraction on the right, converting it into an addition. EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 4-Jul-2025.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = (𝐵 − 𝐶))    ⇒   ⊢ (𝜑 → 𝐵 = (𝐶 + 𝐴))
Theorem	lsubswap23d 42387	Swap the second and third variables in an equation with subtraction on the left, converting it into an addition. EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 23-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐶) = 𝐵)
Theorem	addsubeq4com 42388	Relation between sums and differences. (Contributed by Steven Nguyen, 5-Jan-2023.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐴 − 𝐶) = (𝐷 − 𝐵)))
Theorem	sqsumi 42389	A sum squared. (Contributed by Steven Nguyen, 16-Sep-2022.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) · (𝐴 + 𝐵)) = (((𝐴 · 𝐴) + (𝐵 · 𝐵)) + (2 · (𝐴 · 𝐵)))
Theorem	negn0nposznnd 42390	Lemma for dffltz 42742. (Contributed by Steven Nguyen, 27-Feb-2023.)
⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → ¬ 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → -𝐴 ∈ ℕ)
Theorem	sqmid3api 42391	Value of the square of the middle term of a 3-term arithmetic progression. (Contributed by Steven Nguyen, 20-Sep-2022.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝑁 ∈ ℂ    &   ⊢ (𝐴 + 𝑁) = 𝐵    &   ⊢ (𝐵 + 𝑁) = 𝐶    ⇒   ⊢ (𝐵 · 𝐵) = ((𝐴 · 𝐶) + (𝑁 · 𝑁))
Theorem	decaddcom 42392	Commute ones place in addition. (Contributed by Steven Nguyen, 29-Jan-2023.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    ⇒   ⊢ (;𝐴𝐵 + 𝐶) = (;𝐴𝐶 + 𝐵)
Theorem	sqn5i 42393	The square of a number ending in 5. This shortcut only works because 5 is half of 10. (Contributed by Steven Nguyen, 16-Sep-2022.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (;𝐴5 · ;𝐴5) = ;;(𝐴 · (𝐴 + 1))25
Theorem	sqn5ii 42394	The square of a number ending in 5. This shortcut only works because 5 is half of 10. (Contributed by Steven Nguyen, 16-Sep-2022.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ (𝐴 + 1) = 𝐵    &   ⊢ (𝐴 · 𝐵) = 𝐶    ⇒   ⊢ (;𝐴5 · ;𝐴5) = ;;𝐶25
Theorem	decpmulnc 42395	Partial products algorithm for two digit multiplication, no carry. Compare muladdi 11578. (Contributed by Steven Nguyen, 9-Dec-2022.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝐸    &   ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹    &   ⊢ (𝐵 · 𝐷) = 𝐺    ⇒   ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;;𝐸𝐹𝐺
Theorem	decpmul 42396	Partial products algorithm for two digit multiplication. (Contributed by Steven Nguyen, 10-Dec-2022.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝐸    &   ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹    &   ⊢ (𝐵 · 𝐷) = ;𝐺𝐻    &   ⊢ (;𝐸𝐺 + 𝐹) = 𝐼    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐻 ∈ ℕ0    ⇒   ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;𝐼𝐻
Theorem	sqdeccom12 42397	The square of a number in terms of its digits switched. (Contributed by Steven Nguyen, 3-Jan-2023.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    ⇒   ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
Theorem	sq3deccom12 42398	Variant of sqdeccom12 42397 with a three digit square. (Contributed by Steven Nguyen, 3-Jan-2023.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ (𝐴 + 𝐶) = 𝐷    ⇒   ⊢ ((;;𝐴𝐵𝐶 · ;;𝐴𝐵𝐶) − (;𝐷𝐵 · ;𝐷𝐵)) = (;99 · ((;𝐴𝐵 · ;𝐴𝐵) − (𝐶 · 𝐶)))
Theorem	4t5e20 42399	4 times 5 equals 20. (Contributed by SN, 30-Mar-2025.)
⊢ (4 · 5) = ;20
Theorem	3rdpwhole 42400	A third of a number plus the number is four thirds of the number. (Contributed by SN, 19-Nov-2025.)
⊢ (𝐴 ∈ ℂ → ((𝐴 / 3) + 𝐴) = (4 · (𝐴 / 3)))