P. 432 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43101-43200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	abbi1sn 43101*	Originally part of uniabio 6507. Convert a theorem about df-iota 6493 to one about dfiota2 6494, without ax-10 2178, ax-11 2194, ax-12 2215. Although, eu6 2601 uses ax-10 2178 and ax-12 2215. (Contributed by SN, 23-Nov-2024.)
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → {𝑥 ∣ 𝜑} = {𝑦})
Theorem	brif2 43102	Move a relation inside and outside the conditional operator. (Contributed by SN, 14-Aug-2024.)
⊢ (𝐶𝑅if(𝜑, 𝐴, 𝐵) ↔ if-(𝜑, 𝐶𝑅𝐴, 𝐶𝑅𝐵))
Theorem	brif12 43103	Move a relation inside and outside the conditional operator. (Contributed by SN, 14-Aug-2024.)
⊢ (if(𝜑, 𝐴, 𝐵)𝑅if(𝜑, 𝐶, 𝐷) ↔ if-(𝜑, 𝐴𝑅𝐶, 𝐵𝑅𝐷))
Theorem	pssexg 43104	The proper subset of a set is also a set. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
Theorem	pssn0 43105	A proper superset is nonempty. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ (𝐴 ⊊ 𝐵 → 𝐵 ≠ ∅)
Theorem	psspwb 43106	Classes are proper subclasses if and only if their power classes are proper subclasses. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ (𝐴 ⊊ 𝐵 ↔ 𝒫 𝐴 ⊊ 𝒫 𝐵)
Theorem	xppss12 43107	Proper subset theorem for Cartesian product. (Contributed by Steven Nguyen, 17-Jul-2022.)
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐶 ⊊ 𝐷) → (𝐴 × 𝐶) ⊊ (𝐵 × 𝐷))
Theorem	elpwbi 43108	Membership in a power set, biconditional. (Contributed by Steven Nguyen, 17-Jul-2022.) (Proof shortened by Steven Nguyen, 16-Sep-2022.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ 𝒫 𝐵)
Theorem	imaopab 43109*	The image of a class of ordered pairs. (Contributed by Steven Nguyen, 6-Jun-2023.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} “ 𝐴) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑}
Theorem	eqresfnbd 43110	Property of being the restriction of a function. Note that this is closer to funssres 6581 than fnssres 6659. (Contributed by SN, 11-Mar-2025.)
⊢ (𝜑 → 𝐹 Fn 𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑅 = (𝐹 ↾ 𝐴) ↔ (𝑅 Fn 𝐴 ∧ 𝑅 ⊆ 𝐹)))
Theorem	fmpocos 43111*	Composition of two functions. Variation of fmpoco 8096 with more context in the substitution hypothesis for 𝑇. (Contributed by SN, 14-Mar-2025.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅))    &   ⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐶 ↦ 𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ⦋𝑅 / 𝑧⦌𝑆 = 𝑇)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇))
Theorem	ovmpogad 43112*	Value of an operation given by a maps-to rule. Deduction form of ovmpoga 7571. (Contributed by SN, 14-Mar-2025.)
⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Theorem	ofun 43113	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	dfqs3 43114*	Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.)
⊢ (𝐴 / 𝑅) = ∪ 𝑥 ∈ 𝐴 {[𝑥]𝑅}
Theorem	qseq12d 43115	Equality theorem for quotient set, deduction form. (Contributed by Steven Nguyen, 30-Apr-2023.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐷))
Theorem	qsalrel 43116*	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	supinf 43117*	The supremum is the infimum of the upper bounds. (Contributed by SN, 29-Jun-2025.)
⊢ (𝜑 → < Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐵 𝑦 < 𝑧)))    ⇒   ⊢ (𝜑 → sup(𝐵, 𝐴, < ) = inf({𝑥 ∈ 𝐴 ∣ ∀𝑤 ∈ 𝐵 ¬ 𝑥 < 𝑤}, 𝐴, < ))
Theorem	mapcod 43118	Compose two mappings. (Contributed by SN, 11-Mar-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝐴 ↑m 𝐵))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐵 ↑m 𝐶))    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ (𝐴 ↑m 𝐶))
Theorem	fisdomnn 43119	A finite set is dominated by the set of natural numbers. (Contributed by SN, 6-Jul-2025.)
⊢ (𝐴 ∈ Fin → 𝐴 ≺ ℕ)
Theorem	ltex 43120	The less-than relation is a set. (Contributed by SN, 5-Jun-2025.)
⊢ < ∈ V
Theorem	leex 43121	The less-than-or-equal-to relation is a set. (Contributed by SN, 5-Jun-2025.)
⊢ ≤ ∈ V
Theorem	subex 43122	The subtraction operation is a set. (Contributed by SN, 5-Jun-2025.)
⊢ − ∈ V
Theorem	absex 43123	The absolute value function is a set. (Contributed by SN, 5-Jun-2025.)
⊢ abs ∈ V
Theorem	cjex 43124	The conjugate function is a set. (Contributed by SN, 5-Jun-2025.)
⊢ ∗ ∈ V
Theorem	fzosumm1 43125*	Separate out the last term in a finite sum. (Contributed by Steven Nguyen, 22-Aug-2023.)
⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝑘 = (𝑁 − 1) → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝐴 = (Σ𝑘 ∈ (𝑀..^(𝑁 − 1))𝐴 + 𝐵))
Theorem	ccatcan2d 43126	Cancellation law for concatenation. (Contributed by SN, 6-Sep-2023.)
⊢ (𝜑 → 𝐴 ∈ Word 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ Word 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ Word 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 ++ 𝐶) = (𝐵 ++ 𝐶) ↔ 𝐴 = 𝐵))
21.32.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 11198 is used in mulrid 11234 related theorems, so one could trade off the extra axioms in mulrid 11234 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 11185; in the other direction, real number closure laws can be avoided by using ax-resscn 11185 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 11193, ax-1cn 11186, and ax-addcl 11188. (And in practice, the expression isn't fully expanded into ones.) Multiplication by 1 requires either mullidi 11242 or (ax-1rid 11198 and 1re 11236) as seen in 1t1e1 12430 and 1t1e1ALT 12319. Multiplying with greater natural numbers uses ax-distr 11195. 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 11192 (see readdrid 43293 and readdlid 43286).
Theorem	c0exALT 43127	Alternate proof of c0ex 11228 using more set theory axioms but fewer complex number axioms (add ax-10 2178, ax-11 2194, ax-13 2403, ax-nul 5267, and remove ax-1cn 11186, ax-icn 11187, ax-addcl 11188, and ax-mulcl 11190). (Contributed by Steven Nguyen, 4-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 ∈ V
Theorem	0cnALT3 43128	Alternate proof of 0cn 11226 using ax-resscn 11185, ax-addrcl 11189, ax-rnegex 11199, ax-cnre 11201 instead of ax-icn 11187, ax-addcl 11188, ax-mulcl 11190, ax-i2m1 11196. Version of 0cnALT 11473 using ax-1cn 11186 instead of ax-icn 11187. (Contributed by Steven Nguyen, 7-Jan-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 ∈ ℂ
Theorem	elre0re 43129	Specialized version of 0red 11239 without using ax-1cn 11186 and ax-cnre 11201. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ (𝐴 ∈ ℝ → 0 ∈ ℝ)
Theorem	lttrii 43130	'Less than' is transitive. (Contributed by SN, 26-Aug-2025.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 𝐴 < 𝐵    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ 𝐴 < 𝐶
Theorem	remulcan2d 43131	mulcan2d 11876 for real numbers using fewer axioms. (Contributed by Steven Nguyen, 15-Apr-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵))
Theorem	readdridaddlidd 43132	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 11412, 𝐴 is the right additive identity. (Contributed by Steven Nguyen, 14-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐵 + 𝐴) = 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ ℝ) → (𝐴 + 𝐶) = 𝐶)
Theorem	4p4e8ALT 43133	A shorter proof of 4p4e8 12423 if 6p2e8 12427 was moved up. The most clean way to do this would be to start with 7p2e9 12429, then go 6p2e8 12427, 6p3e9 12428, etc., which is still inelegant. The idea here is that using 4 = 2 + 2 and 2cn 12344 is shorter than using 4 = 3 + 1, 3cn 12350, and ax-1cn 11186. This also works with 5p4e9 12426. (Contributed by SN, 24-Aug-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (4 + 4) = 8
Theorem	1p3e4 43134	1 + 3 = 4. (Contributed by SN, 19-Nov-2025.)
⊢ (1 + 3) = 4
Theorem	1p4e5 43135	1 + 4 = 5. (Contributed by SN, 24-Aug-2026.)
⊢ (1 + 4) = 5
Theorem	1p5e6 43136	1 + 5 = 6. (Contributed by SN, 24-Aug-2026.)
⊢ (1 + 5) = 6
Theorem	1p6e7 43137	1 + 6 = 7. (Contributed by SN, 24-Aug-2026.)
⊢ (1 + 6) = 7
Theorem	1p7e8 43138	1 + 7 = 8. (Contributed by SN, 24-Aug-2026.)
⊢ (1 + 7) = 8
Theorem	1p8e9 43139	1 + 8 = 9. (Contributed by SN, 24-Aug-2026.)
⊢ (1 + 8) = 9
Theorem	2p3e5 43140	2 + 3 = 5. (Contributed by SN, 24-Aug-2026.)
⊢ (2 + 3) = 5
Theorem	2p4e6 43141	2 + 4 = 6. (Contributed by SN, 24-Aug-2026.)
⊢ (2 + 4) = 6
Theorem	2p5e7 43142	2 + 5 = 7. (Contributed by SN, 24-Aug-2026.)
⊢ (2 + 5) = 7
Theorem	2p6e8 43143	2 + 6 = 8. (Contributed by SN, 24-Aug-2026.)
⊢ (2 + 6) = 8
Theorem	2p7e9 43144	2 + 7 = 9. (Contributed by SN, 24-Aug-2026.)
⊢ (2 + 7) = 9
Theorem	3p4e7 43145	3 + 4 = 7. (Contributed by SN, 24-Aug-2026.)
⊢ (3 + 4) = 7
Theorem	3p5e8 43146	3 + 5 = 8. (Contributed by SN, 24-Aug-2026.)
⊢ (3 + 5) = 8
Theorem	3p6e9 43147	3 + 6 = 9. (Contributed by SN, 24-Aug-2026.)
⊢ (3 + 6) = 9
Theorem	4p5e9 43148	4 + 5 = 9. (Contributed by SN, 24-Aug-2026.)
⊢ (4 + 5) = 9
Theorem	5ne0 43149	The number 5 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 5 ≠ 0
Theorem	6ne0 43150	The number 6 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 6 ≠ 0
Theorem	7ne0 43151	The number 7 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 7 ≠ 0
Theorem	8ne0 43152	The number 8 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 8 ≠ 0
Theorem	9ne0 43153	The number 9 is nonzero. (Contributed by SN, 22-Oct-2025.)
⊢ 9 ≠ 0
Theorem	sn-1ne2 43154	A proof of 1ne2 12479 without using ax-mulcom 11192, ax-mulass 11194, ax-pre-mulgt0 11205. Based on mul02lem2 11415. (Contributed by SN, 13-Dec-2023.)
⊢ 1 ≠ 2
Theorem	nnn1suc 43155*	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	readdrcl2d 43156	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 43157	Move a subtraction in the RHS to a right-addition in the LHS. Converse of mvlraddd 11652. EDITORIAL: Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = (𝐵 − 𝐶))    ⇒   ⊢ (𝜑 → (𝐴 + 𝐶) = 𝐵)
Theorem	laddrotrd 43158	Rotate the variables right in an equation with addition on the left, converting it into a subtraction. Version of mvlladdd 11653 with a commuted consequent, and of mvrladdd 11655 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 34002. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → (𝐶 − 𝐴) = 𝐵)
Theorem	raddswap12d 43159	Swap the first two variables in an equation with addition on the right, converting it into a subtraction. Version of mvrraddd 11654 with a commuted consequent, and of mvlraddd 11652 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 43160	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 43161	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 43162	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 43163	Relation between sums and differences. (Contributed by Steven Nguyen, 5-Jan-2023.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐴 − 𝐶) = (𝐷 − 𝐵)))
Theorem	sqsumi 43164	A sum squared. (Contributed by Steven Nguyen, 16-Sep-2022.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) · (𝐴 + 𝐵)) = (((𝐴 · 𝐴) + (𝐵 · 𝐵)) + (2 · (𝐴 · 𝐵)))
Theorem	negn0nposznnd 43165	Lemma for dffltz 43488. (Contributed by Steven Nguyen, 27-Feb-2023.)
⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → ¬ 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → -𝐴 ∈ ℕ)
Theorem	sqmid3api 43166	Value of the square of the middle term of a 3-term arithmetic progression. (Contributed by Steven Nguyen, 20-Sep-2022.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝑁 ∈ ℂ    &   ⊢ (𝐴 + 𝑁) = 𝐵    &   ⊢ (𝐵 + 𝑁) = 𝐶    ⇒   ⊢ (𝐵 · 𝐵) = ((𝐴 · 𝐶) + (𝑁 · 𝑁))
Theorem	decaddcom 43167	Commute ones place in addition. (Contributed by Steven Nguyen, 29-Jan-2023.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    ⇒   ⊢ (;𝐴𝐵 + 𝐶) = (;𝐴𝐶 + 𝐵)
Theorem	sqn5i 43168	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 43169	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 43170	Partial products algorithm for two digit multiplication, no carry. Compare muladdi 11693. (Contributed by Steven Nguyen, 9-Dec-2022.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝐸    &   ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹    &   ⊢ (𝐵 · 𝐷) = 𝐺    ⇒   ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;;𝐸𝐹𝐺
Theorem	decpmul 43171	Partial products algorithm for two digit multiplication. (Contributed by Steven Nguyen, 10-Dec-2022.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝐸    &   ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹    &   ⊢ (𝐵 · 𝐷) = ;𝐺𝐻    &   ⊢ (;𝐸𝐺 + 𝐹) = 𝐼    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐻 ∈ ℕ0    ⇒   ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;𝐼𝐻
Theorem	sqdeccom12 43172	The square of a number in terms of its digits switched. (Contributed by Steven Nguyen, 3-Jan-2023.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    ⇒   ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
Theorem	sq3deccom12 43173	Variant of sqdeccom12 43172 with a three digit square. (Contributed by Steven Nguyen, 3-Jan-2023.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ (𝐴 + 𝐶) = 𝐷    ⇒   ⊢ ((;;𝐴𝐵𝐶 · ;;𝐴𝐵𝐶) − (;𝐷𝐵 · ;𝐷𝐵)) = (;99 · ((;𝐴𝐵 · ;𝐴𝐵) − (𝐶 · 𝐶)))
Theorem	4t5e20 43174	4 times 5 equals 20. (Contributed by SN, 30-Mar-2025.)
⊢ (4 · 5) = ;20
Theorem	3rdpwhole 43175	A third of a number plus the number is four thirds of the number. (Contributed by SN, 19-Nov-2025.)
⊢ (𝐴 ∈ ℂ → ((𝐴 / 3) + 𝐴) = (4 · (𝐴 / 3)))
Theorem	sq4 43176	The square of 4 is 16. (Contributed by SN, 26-Aug-2025.)
⊢ (4↑2) = ;16
Theorem	sq5 43177	The square of 5 is 25. (Contributed by SN, 26-Aug-2025.)
⊢ (5↑2) = ;25
Theorem	sq6 43178	The square of 6 is 36. (Contributed by SN, 26-Aug-2025.)
⊢ (6↑2) = ;36
Theorem	sq7 43179	The square of 7 is 49. (Contributed by SN, 26-Aug-2025.)
⊢ (7↑2) = ;49
Theorem	sq8 43180	The square of 8 is 64. (Contributed by SN, 26-Aug-2025.)
⊢ (8↑2) = ;64
Theorem	sq9 43181	The square of 9 is 81. (Contributed by SN, 30-Mar-2025.)
⊢ (9↑2) = ;81
Theorem	rpsscn 43182	The positive reals are a subset of the complex numbers. (Contributed by SN, 1-Oct-2025.)
⊢ ℝ+ ⊆ ℂ
Theorem	4rp 43183	4 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 4 ∈ ℝ+
Theorem	6rp 43184	6 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 6 ∈ ℝ+
Theorem	7rp 43185	7 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 7 ∈ ℝ+
Theorem	8rp 43186	8 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 8 ∈ ℝ+
Theorem	9rp 43187	9 is a positive real. (Contributed by SN, 26-Aug-2025.)
⊢ 9 ∈ ℝ+
Theorem	235t711 43188	Calculate a product by long multiplication as a base comparison with other multiplication algorithms. Conveniently, 711 has two ones which greatly simplifies calculations like 235 · 1. There isn't a higher level mulcomli 11246 saving the lower level uses of mulcomli 11246 within 235 · 7 since mulcom2 doesn't exist, but if commuted versions of theorems like 7t2e14 12854 are added then this proof would benefit more than ex-decpmul 43189. For practicality, this proof doesn't have "e167085" at the end of its name like 2p2e4 12403 or 8t7e56 12865. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.)
⊢ (;;235 · ;;711) = ;;;;;167085
Theorem	ex-decpmul 43189	Example usage of decpmul 43171. This proof is significantly longer than 235t711 43188. There is more unnecessary carrying compared to 235t711 43188. Although saving 5 visual steps, using mulcomli 11246 early on increases the compressed proof length. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (;;235 · ;;711) = ;;;;;167085
Theorem	eluzp1 43190	Membership in a successor upper set of integers. (Contributed by SN, 5-Jul-2025.)
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) ↔ (𝑁 ∈ ℤ ∧ 𝑀 < 𝑁)))
Theorem	sn-eluzp1l 43191	Shorter proof of eluzp1l 12918. (Contributed by NM, 12-Sep-2005.) (Revised by SN, 5-Jul-2025.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑁)
Theorem	fz1sumconst 43192*	The sum of 𝑁 constant terms (𝑘 is not free in 𝐶). (Contributed by SN, 21-Mar-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (1...𝑁)𝐶 = (𝑁 · 𝐶))
Theorem	fz1sump1 43193*	Add one more term to a sum. Special case of fsump1 15846 generalized to 𝑁 ∈ ℕ0. (Contributed by SN, 22-Mar-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐴 ∈ ℂ)    &   ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (1...(𝑁 + 1))𝐴 = (Σ𝑘 ∈ (1...𝑁)𝐴 + 𝐵))
Theorem	oddnumth 43194*	The Odd Number Theorem. The sum of the first 𝑁 odd numbers is 𝑁↑2. A corollary of arisum 15953. (Contributed by SN, 21-Mar-2025.)
⊢ (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑁)((2 · 𝑘) − 1) = (𝑁↑2))
Theorem	nicomachus 43195*	Nicomachus's Theorem. The sum of the odd numbers from 𝑁↑2 − 𝑁 + 1 to 𝑁↑2 + 𝑁 − 1 is 𝑁↑3. Proof 2 from https://proofwiki.org/wiki/Nicomachus%27s_Theorem. (Contributed by SN, 21-Mar-2025.)
⊢ (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑁)(((𝑁↑2) − 𝑁) + ((2 · 𝑘) − 1)) = (𝑁↑3))
Theorem	sumcubes 43196*	The sum of the first 𝑁 perfect cubes is the sum of the first 𝑁 nonnegative integers, squared. This is the Proof by Nicomachus from https://proofwiki.org/wiki/Sum_of_Sequence_of_Cubes using induction and index shifting to collect all the odd numbers. (Contributed by SN, 22-Mar-2025.)
⊢ (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑁)(𝑘↑3) = (Σ𝑘 ∈ (1...𝑁)𝑘↑2))
Theorem	ine1 43197	i is not 1. (Contributed by SN, 25-Apr-2025.)
⊢ i ≠ 1
Theorem	0tie0 43198	0 times i equals 0. (Contributed by SN, 25-Apr-2025.)
⊢ (0 · i) = 0
Theorem	it1ei 43199	i times 1 equals i. (Contributed by SN, 25-Apr-2025.)
⊢ (i · 1) = i
Theorem	1tiei 43200	1 times i equals i. (Contributed by SN, 25-Apr-2025.)
⊢ (1 · i) = i