P. 423 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42201-42300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	factwoffsmonot 42201	A factorial with offset is monotonely increasing. (Contributed by metakunt, 20-Apr-2024.)
⊢ (((𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℕ0 ∧ 𝑋 ≤ 𝑌) ∧ 𝑁 ∈ ℕ0) → (!‘(𝑋 + 𝑁)) ≤ (!‘(𝑌 + 𝑁)))
21.30  Mathbox for Steven Nguyen
21.30.1  Utility theorems
Theorem	jarrii 42202	Inference associated with jarri 107. A consequence of ax-mp 5 and ax-1 6. (Contributed by SN, 14-Oct-2025.)
⊢ 𝜓    &   ⊢ ((𝜑 → 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	intnanrt 42203	Introduction of conjunct inside of a contradiction. Would be used in elfvov1 7445. (Contributed by SN, 18-May-2025.)
⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓))
Theorem	ioin9i8 42204	Miscellaneous inference creating a biconditional from an implied converse implication. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ (𝜑 → (𝜓 ∨ 𝜒))    &   ⊢ (𝜒 → ¬ 𝜃)    &   ⊢ (𝜓 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜃))
Theorem	jaodd 42205	Double deduction form of jaoi 857. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜏) → 𝜃)))
Theorem	syl3an12 42206	A double syllogism inference. (Contributed by SN, 15-Sep-2024.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
Theorem	exbiii 42207	Inference associated with exbii 1848. Weaker version of eximii 1837. (Contributed by SN, 14-Oct-2025.)
⊢ ∃𝑥𝜑    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ∃𝑥𝜓
Theorem	sbtd 42208*	A true statement is true upon substitution (deduction). A similar proof is possible for icht 47414. (Contributed by SN, 4-May-2024.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → [𝑡 / 𝑥]𝜓)
Theorem	sbor2 42209	One direction of sbor 2307, using fewer axioms. Compare 19.33 1884. (Contributed by Steven Nguyen, 18-Aug-2023.)
⊢ (([𝑡 / 𝑥]𝜑 ∨ [𝑡 / 𝑥]𝜓) → [𝑡 / 𝑥](𝜑 ∨ 𝜓))
Theorem	sbalexi 42210*	Inference form of sbalex 2242, avoiding ax-10 2141 by using ax-gen 1795. (Contributed by SN, 12-Aug-2025.)
⊢ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)    ⇒   ⊢ ∀𝑥(𝑥 = 𝑦 → 𝜑)
Theorem	19.9dev 42211*	19.9d 2203 in the case of an existential quantifier, avoiding the ax-10 2141 from nfex 2324 that would be used for the hypothesis of 19.9d 2203, at the cost of an additional DV condition on 𝑦, 𝜑. (Contributed by SN, 26-May-2024.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑦𝜓))
Theorem	3rspcedvd 42212*	Triple application of rspcedvd 3603. (Contributed by Steven Nguyen, 27-Feb-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → (𝜒 ↔ 𝜃))    &   ⊢ ((𝜑 ∧ 𝑧 = 𝐶) → (𝜃 ↔ 𝜏))    &   ⊢ (𝜑 → 𝜏)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 ∃𝑧 ∈ 𝐷 𝜓)
Theorem	sn-axrep5v 42213*	A condensed form of axrep5 5257. (Contributed by SN, 21-Sep-2023.)
⊢ (∀𝑤 ∈ 𝑥 ∃*𝑧𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 𝜑))
Theorem	sn-axprlem3 42214*	axprlem3 5395 using only Tarski's FOL axiom schemes and ax-rep 5249. (Contributed by SN, 22-Sep-2023.)
⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 if-(𝜑, 𝑧 = 𝑎, 𝑧 = 𝑏))
Theorem	sn-exelALT 42215*	Alternate proof of exel 5408, avoiding ax-pr 5402 but requiring ax-5 1910, ax-9 2118, and ax-pow 5335. This is similar to how elALT2 5339 uses ax-pow 5335 instead of ax-pr 5402 compared to el 5412. (Contributed by SN, 18-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦
Theorem	ss2ab1 42216	Class abstractions in a subclass relationship, closed form. One direction of ss2ab 4037 using fewer axioms. (Contributed by SN, 22-Dec-2024.)
⊢ (∀𝑥(𝜑 → 𝜓) → {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜓})
Theorem	ssabdv 42217*	Deduction of abstraction subclass from implication. (Contributed by SN, 22-Dec-2024.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ {𝑥 ∣ 𝜓})
Theorem	sn-iotalem 42218*	An unused lemma showing that many equivalences involving df-iota 6483 are potentially provable without ax-10 2141, ax-11 2157, ax-12 2177. (Contributed by SN, 6-Nov-2024.)
⊢ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑧 ∣ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑧}}
Theorem	sn-iotalemcor 42219*	Corollary of sn-iotalem 42218. Compare sb8iota 6494. (Contributed by SN, 6-Nov-2024.)
⊢ (℩𝑥𝜑) = (℩𝑦{𝑥 ∣ 𝜑} = {𝑦})
Theorem	abbi1sn 42220*	Originally part of uniabio 6497. Convert a theorem about df-iota 6483 to one about dfiota2 6484, without ax-10 2141, ax-11 2157, ax-12 2177. Although, eu6 2573 uses ax-10 2141 and ax-12 2177. (Contributed by SN, 23-Nov-2024.)
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → {𝑥 ∣ 𝜑} = {𝑦})
Theorem	brif2 42221	Move a relation inside and outside the conditional operator. (Contributed by SN, 14-Aug-2024.)
⊢ (𝐶𝑅if(𝜑, 𝐴, 𝐵) ↔ if-(𝜑, 𝐶𝑅𝐴, 𝐶𝑅𝐵))
Theorem	brif12 42222	Move a relation inside and outside the conditional operator. (Contributed by SN, 14-Aug-2024.)
⊢ (if(𝜑, 𝐴, 𝐵)𝑅if(𝜑, 𝐶, 𝐷) ↔ if-(𝜑, 𝐴𝑅𝐶, 𝐵𝑅𝐷))
Theorem	pssexg 42223	The proper subset of a set is also a set. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
Theorem	pssn0 42224	A proper superset is nonempty. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ (𝐴 ⊊ 𝐵 → 𝐵 ≠ ∅)
Theorem	psspwb 42225	Classes are proper subclasses if and only if their power classes are proper subclasses. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ (𝐴 ⊊ 𝐵 ↔ 𝒫 𝐴 ⊊ 𝒫 𝐵)
Theorem	xppss12 42226	Proper subset theorem for Cartesian product. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐶 ⊊ 𝐷) → (𝐴 × 𝐶) ⊊ (𝐵 × 𝐷))
Theorem	elpwbi 42227	Membership in a power set, biconditional. (Contributed by Steven Nguyen, 17-Jul-2022.) (Proof shortened by Steven Nguyen, 16-Sep-2022.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ 𝒫 𝐵)
Theorem	imaopab 42228*	The image of a class of ordered pairs. (Contributed by Steven Nguyen, 6-Jun-2023.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} “ 𝐴) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑}
Theorem	fnimasnd 42229	The image of a function by a singleton whose element is in the domain of the function. (Contributed by Steven Nguyen, 7-Jun-2023.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹 “ {𝑆}) = {(𝐹‘𝑆)})
Theorem	eqresfnbd 42230	Property of being the restriction of a function. Note that this is closer to funssres 6579 than fnssres 6660. (Contributed by SN, 11-Mar-2025.)
⊢ (𝜑 → 𝐹 Fn 𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑅 = (𝐹 ↾ 𝐴) ↔ (𝑅 Fn 𝐴 ∧ 𝑅 ⊆ 𝐹)))
Theorem	f1o2d2 42231*	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 42232*	Composition of two functions. Variation of fmpoco 8092 with more context in the substitution hypothesis for 𝑇. (Contributed by SN, 14-Mar-2025.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅))    &   ⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐶 ↦ 𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ⦋𝑅 / 𝑧⦌𝑆 = 𝑇)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇))
Theorem	ovmpogad 42233*	Value of an operation given by a maps-to rule. Deduction form of ovmpoga 7559. (Contributed by SN, 14-Mar-2025.)
⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Theorem	ofun 42234	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 42235*	Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.)
⊢ (𝐴 / 𝑅) = ran (𝑥 ∈ 𝐴 ↦ [𝑥]𝑅)
Theorem	dfqs3 42236*	Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.)
⊢ (𝐴 / 𝑅) = ∪ 𝑥 ∈ 𝐴 {[𝑥]𝑅}
Theorem	qseq12d 42237	Equality theorem for quotient set, deduction form. (Contributed by Steven Nguyen, 30-Apr-2023.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐷))
Theorem	qsalrel 42238*	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 42239	A restricted mapping is a mapping. EDITORIAL: Could be used to shorten elpm2r 8857 with some reordering involving mapsspm 8888. (Contributed by SN, 11-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m 𝐶))    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ↾ 𝐷) ∈ (𝐵 ↑m 𝐷))
Theorem	supinf 42240*	The supremum is the infimum of the upper bounds. (Contributed by SN, 29-Jun-2025.)
⊢ (𝜑 → < Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐵 𝑦 < 𝑧)))    ⇒   ⊢ (𝜑 → sup(𝐵, 𝐴, < ) = inf({𝑥 ∈ 𝐴 ∣ ∀𝑤 ∈ 𝐵 ¬ 𝑥 < 𝑤}, 𝐴, < ))
Theorem	mapcod 42241	Compose two mappings. (Contributed by SN, 11-Mar-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐴 ↑m 𝐵))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐵 ↑m 𝐶))    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ (𝐴 ↑m 𝐶))
Theorem	fisdomnn 42242	A finite set is dominated by the set of natural numbers. (Contributed by SN, 6-Jul-2025.)
⊢ (𝐴 ∈ Fin → 𝐴 ≺ ℕ)
Theorem	ltex 42243	The less-than relation is a set. (Contributed by SN, 5-Jun-2025.)
⊢ < ∈ V
Theorem	leex 42244	The less-than-or-equal-to relation is a set. (Contributed by SN, 5-Jun-2025.)
⊢ ≤ ∈ V
Theorem	subex 42245	The subtraction operation is a set. (Contributed by SN, 5-Jun-2025.)
⊢ − ∈ V
Theorem	absex 42246	The absolute value function is a set. (Contributed by SN, 5-Jun-2025.)
⊢ abs ∈ V
Theorem	cjex 42247	The conjugate function is a set. (Contributed by SN, 5-Jun-2025.)
⊢ ∗ ∈ V
Theorem	fzosumm1 42248*	Separate out the last term in a finite sum. (Contributed by Steven Nguyen, 22-Aug-2023.)
⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝑘 = (𝑁 − 1) → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝐴 = (Σ𝑘 ∈ (𝑀..^(𝑁 − 1))𝐴 + 𝐵))
Theorem	ccatcan2d 42249	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 11197 is used in mulrid 11231 related theorems, so one could trade off the extra axioms in mulrid 11231 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 11184; in the other direction, real number closure laws can be avoided by using ax-resscn 11184 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 11192, ax-1cn 11185, and ax-addcl 11187. (And in practice, the expression isn't fully expanded into ones.) Multiplication by 1 requires either mullidi 11238 or (ax-1rid 11197 and 1re 11233) as seen in 1t1e1 12400 and 1t1e1ALT 42253. Multiplying with greater natural numbers uses ax-distr 11194. 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 11191 (see readdrid 42399 and readdlid 42393).
Theorem	c0exALT 42250	Alternate proof of c0ex 11227 using more set theory axioms but fewer complex number axioms (add ax-10 2141, ax-11 2157, ax-13 2376, ax-nul 5276, and remove ax-1cn 11185, ax-icn 11186, ax-addcl 11187, and ax-mulcl 11189). (Contributed by Steven Nguyen, 4-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 ∈ V
Theorem	0cnALT3 42251	Alternate proof of 0cn 11225 using ax-resscn 11184, ax-addrcl 11188, ax-rnegex 11198, ax-cnre 11200 instead of ax-icn 11186, ax-addcl 11187, ax-mulcl 11189, ax-i2m1 11195. Version of 0cnALT 11468 using ax-1cn 11185 instead of ax-icn 11186. (Contributed by Steven Nguyen, 7-Jan-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 ∈ ℂ
Theorem	elre0re 42252	Specialized version of 0red 11236 without using ax-1cn 11185 and ax-cnre 11200. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ (𝐴 ∈ ℝ → 0 ∈ ℝ)
Theorem	1t1e1ALT 42253	Alternate proof of 1t1e1 12400 using a different set of axioms (add ax-mulrcl 11190, ax-i2m1 11195, ax-1ne0 11196, ax-rrecex 11199 and remove ax-resscn 11184, ax-mulcom 11191, ax-mulass 11193, ax-distr 11194). (Contributed by Steven Nguyen, 20-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (1 · 1) = 1
Theorem	lttrii 42254	'Less than' is transitive. (Contributed by SN, 26-Aug-2025.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 𝐴 < 𝐵    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ 𝐴 < 𝐶
Theorem	remulcan2d 42255	mulcan2d 11869 for real numbers using fewer axioms. (Contributed by Steven Nguyen, 15-Apr-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵))
Theorem	readdridaddlidd 42256	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 11407, 𝐴 is the right additive identity. (Contributed by Steven Nguyen, 14-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐵 + 𝐴) = 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ ℝ) → (𝐴 + 𝐶) = 𝐶)
Theorem	5ne0 42257	The number 5 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 5 ≠ 0
Theorem	6ne0 42258	The number 6 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 6 ≠ 0
Theorem	7ne0 42259	The number 7 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 7 ≠ 0
Theorem	8ne0 42260	The number 8 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 8 ≠ 0
Theorem	9ne0 42261	The number 9 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 9 ≠ 0
Theorem	sn-1ne2 42262	A proof of 1ne2 12446 without using ax-mulcom 11191, ax-mulass 11193, ax-pre-mulgt0 11204. Based on mul02lem2 11410. (Contributed by SN, 13-Dec-2023.)
⊢ 1 ≠ 2
Theorem	nnn1suc 42263*	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 42264	Addition with 1 is commutative for natural numbers. (Contributed by Steven Nguyen, 9-Dec-2022.)
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) = (1 + 𝐴))
Theorem	nnaddcom 42265	Addition is commutative for natural numbers. Uses fewer axioms than addcom 11419. (Contributed by Steven Nguyen, 9-Dec-2022.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	nnaddcomli 42266	Version of addcomli 11425 for natural numbers. (Contributed by Steven Nguyen, 1-Aug-2023.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ (𝐴 + 𝐵) = 𝐶    ⇒   ⊢ (𝐵 + 𝐴) = 𝐶
Theorem	nnadddir 42267	Right-distributivity for natural numbers without ax-mulcom 11191. (Contributed by SN, 5-Feb-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	nnmul1com 42268	Multiplication with 1 is commutative for natural numbers, without ax-mulcom 11191. Since (𝐴 · 1) is 𝐴 by ax-1rid 11197, this is equivalent to remullid 42423 for natural numbers, but using fewer axioms (avoiding ax-resscn 11184, ax-addass 11192, ax-mulass 11193, ax-rnegex 11198, ax-pre-lttri 11201, ax-pre-lttrn 11202, ax-pre-ltadd 11203). (Contributed by SN, 5-Feb-2024.)
⊢ (𝐴 ∈ ℕ → (1 · 𝐴) = (𝐴 · 1))
Theorem	nnmulcom 42269	Multiplication is commutative for natural numbers. (Contributed by SN, 5-Feb-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	readdrcl2d 42270	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 42271	Move a subtraction in the RHS to a right-addition in the LHS. Converse of mvlraddd 11645. EDITORIAL: Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = (𝐵 − 𝐶))    ⇒   ⊢ (𝜑 → (𝐴 + 𝐶) = 𝐵)
Theorem	laddrotrd 42272	Rotate the variables right in an equation with addition on the left, converting it into a subtraction. Version of mvlladdd 11646 with a commuted consequent, and of mvrladdd 11648 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 33541. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → (𝐶 − 𝐴) = 𝐵)
Theorem	raddswap12d 42273	Swap the first two variables in an equation with addition on the right, converting it into a subtraction. Version of mvrraddd 11647 with a commuted consequent, and of mvlraddd 11645 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 42274	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 42275	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 42276	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 42277	Relation between sums and differences. (Contributed by Steven Nguyen, 5-Jan-2023.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐴 − 𝐶) = (𝐷 − 𝐵)))
Theorem	sqsumi 42278	A sum squared. (Contributed by Steven Nguyen, 16-Sep-2022.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) · (𝐴 + 𝐵)) = (((𝐴 · 𝐴) + (𝐵 · 𝐵)) + (2 · (𝐴 · 𝐵)))
Theorem	negn0nposznnd 42279	Lemma for dffltz 42604. (Contributed by Steven Nguyen, 27-Feb-2023.)
⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → ¬ 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → -𝐴 ∈ ℕ)
Theorem	sqmid3api 42280	Value of the square of the middle term of a 3-term arithmetic progression. (Contributed by Steven Nguyen, 20-Sep-2022.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝑁 ∈ ℂ    &   ⊢ (𝐴 + 𝑁) = 𝐵    &   ⊢ (𝐵 + 𝑁) = 𝐶    ⇒   ⊢ (𝐵 · 𝐵) = ((𝐴 · 𝐶) + (𝑁 · 𝑁))
Theorem	decaddcom 42281	Commute ones place in addition. (Contributed by Steven Nguyen, 29-Jan-2023.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    ⇒   ⊢ (;𝐴𝐵 + 𝐶) = (;𝐴𝐶 + 𝐵)
Theorem	sqn5i 42282	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 42283	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 42284	Partial products algorithm for two digit multiplication, no carry. Compare muladdi 11686. (Contributed by Steven Nguyen, 9-Dec-2022.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝐸    &   ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹    &   ⊢ (𝐵 · 𝐷) = 𝐺    ⇒   ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;;𝐸𝐹𝐺
Theorem	decpmul 42285	Partial products algorithm for two digit multiplication. (Contributed by Steven Nguyen, 10-Dec-2022.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝐸    &   ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹    &   ⊢ (𝐵 · 𝐷) = ;𝐺𝐻    &   ⊢ (;𝐸𝐺 + 𝐹) = 𝐼    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐻 ∈ ℕ0    ⇒   ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;𝐼𝐻
Theorem	sqdeccom12 42286	The square of a number in terms of its digits switched. (Contributed by Steven Nguyen, 3-Jan-2023.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    ⇒   ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
Theorem	sq3deccom12 42287	Variant of sqdeccom12 42286 with a three digit square. (Contributed by Steven Nguyen, 3-Jan-2023.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ (𝐴 + 𝐶) = 𝐷    ⇒   ⊢ ((;;𝐴𝐵𝐶 · ;;𝐴𝐵𝐶) − (;𝐷𝐵 · ;𝐷𝐵)) = (;99 · ((;𝐴𝐵 · ;𝐴𝐵) − (𝐶 · 𝐶)))
Theorem	4t5e20 42288	4 times 5 equals 20. (Contributed by SN, 30-Mar-2025.)
⊢ (4 · 5) = ;20
Theorem	sq4 42289	The square of 4 is 16. (Contributed by SN, 26-Aug-2025.)
⊢ (4↑2) = ;16
Theorem	sq5 42290	The square of 5 is 25. (Contributed by SN, 26-Aug-2025.)
⊢ (5↑2) = ;25
Theorem	sq6 42291	The square of 6 is 36. (Contributed by SN, 26-Aug-2025.)
⊢ (6↑2) = ;36
Theorem	sq7 42292	The square of 7 is 49. (Contributed by SN, 26-Aug-2025.)
⊢ (7↑2) = ;49
Theorem	sq8 42293	The square of 8 is 64. (Contributed by SN, 26-Aug-2025.)
⊢ (8↑2) = ;64
Theorem	sq9 42294	The square of 9 is 81. (Contributed by SN, 30-Mar-2025.)
⊢ (9↑2) = ;81
Theorem	rpsscn 42295	The positive reals are a subset of the complex numbers. (Contributed by SN, 1-Oct-2025.)
⊢ ℝ+ ⊆ ℂ
Theorem	4rp 42296	4 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 4 ∈ ℝ+
Theorem	6rp 42297	6 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 6 ∈ ℝ+
Theorem	7rp 42298	7 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 7 ∈ ℝ+
Theorem	8rp 42299	8 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 8 ∈ ℝ+
Theorem	9rp 42300	9 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 9 ∈ ℝ+