P. 436 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43501-43600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	flt4lem2 43501	If 𝐴 is even, 𝐵 is odd. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ¬ 2 ∥ 𝐵)
Theorem	flt4lem3 43502	Equivalent to pythagtriplem4 16917. Show that 𝐶 + 𝐴 and 𝐶 − 𝐴 are coprime. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ((𝐶 + 𝐴) gcd (𝐶 − 𝐴)) = 1)
Theorem	flt4lem4 43503	If the product of two coprime factors is a perfect square, the factors are perfect squares. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    &   ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐶↑2))    ⇒   ⊢ (𝜑 → (𝐴 = ((𝐴 gcd 𝐶)↑2) ∧ 𝐵 = ((𝐵 gcd 𝐶)↑2)))
Theorem	flt4lem5 43504	In the context of the lemmas of pythagtrip 16932, 𝑀 and 𝑁 are coprime. (Contributed by SN, 23-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)    ⇒   ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑀 gcd 𝑁) = 1)
Theorem	flt4lem5elem 43505	Version of fltaccoprm 43494 and fltbccoprm 43495 where 𝑀 is not squared. This can be proved in general for any polynomial in three variables: using prmdvdsncoprmbd 16824, dvds2addd 16388, and prmdvdsexp 16812, we can show that if two variables are coprime, the third is also coprime to the two. (Contributed by SN, 24-Aug-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 = ((𝑅↑2) + (𝑆↑2)))    &   ⊢ (𝜑 → (𝑅 gcd 𝑆) = 1)    ⇒   ⊢ (𝜑 → ((𝑅 gcd 𝑀) = 1 ∧ (𝑆 gcd 𝑀) = 1))
Theorem	flt4lem5a 43506	Part 1 of Equation 1 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. (Contributed by SN, 22-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑅 = (((√‘(𝑀 + 𝑁)) + (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ 𝑆 = (((√‘(𝑀 + 𝑁)) − (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ((𝐴↑2) + (𝑁↑2)) = (𝑀↑2))
Theorem	flt4lem5b 43507	Part 2 of Equation 1 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. (Contributed by SN, 22-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑅 = (((√‘(𝑀 + 𝑁)) + (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ 𝑆 = (((√‘(𝑀 + 𝑁)) − (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → (2 · (𝑀 · 𝑁)) = (𝐵↑2))
Theorem	flt4lem5c 43508	Part 2 of Equation 2 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. (Contributed by SN, 22-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑅 = (((√‘(𝑀 + 𝑁)) + (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ 𝑆 = (((√‘(𝑀 + 𝑁)) − (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → 𝑁 = (2 · (𝑅 · 𝑆)))
Theorem	flt4lem5d 43509	Part 3 of Equation 2 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. (Contributed by SN, 23-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑅 = (((√‘(𝑀 + 𝑁)) + (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ 𝑆 = (((√‘(𝑀 + 𝑁)) − (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → 𝑀 = ((𝑅↑2) + (𝑆↑2)))
Theorem	flt4lem5e 43510	Satisfy the hypotheses of flt4lem4 43503. (Contributed by SN, 23-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑅 = (((√‘(𝑀 + 𝑁)) + (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ 𝑆 = (((√‘(𝑀 + 𝑁)) − (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → (((𝑅 gcd 𝑆) = 1 ∧ (𝑅 gcd 𝑀) = 1 ∧ (𝑆 gcd 𝑀) = 1) ∧ (𝑅 ∈ ℕ ∧ 𝑆 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ ((𝑀 · (𝑅 · 𝑆)) = ((𝐵 / 2)↑2) ∧ (𝐵 / 2) ∈ ℕ)))
Theorem	flt4lem5f 43511	Final equation of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. Given 𝐴↑4 + 𝐵↑4 = 𝐶↑2, provide a smaller solution. This satisfies the infinite descent condition. (Contributed by SN, 24-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑅 = (((√‘(𝑀 + 𝑁)) + (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ 𝑆 = (((√‘(𝑀 + 𝑁)) − (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ((𝑀 gcd (𝐵 / 2))↑2) = (((𝑅 gcd (𝐵 / 2))↑4) + ((𝑆 gcd (𝐵 / 2))↑4)))
Theorem	flt4lem6 43512	Remove shared factors in a solution to 𝐴↑4 + 𝐵↑4 = 𝐶↑2. (Contributed by SN, 24-Jul-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → (((𝐴 / (𝐴 gcd 𝐵)) ∈ ℕ ∧ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ ∧ (𝐶 / ((𝐴 gcd 𝐵)↑2)) ∈ ℕ) ∧ (((𝐴 / (𝐴 gcd 𝐵))↑4) + ((𝐵 / (𝐴 gcd 𝐵))↑4)) = ((𝐶 / ((𝐴 gcd 𝐵)↑2))↑2)))
Theorem	flt4lem7 43513*	Convert flt4lem5f 43511 into a convenient form for nna4b4nsq 43514. TODO-SN: The change to (𝐴 gcd 𝐵) = 1 points at some inefficiency in the lemmas. (Contributed by SN, 25-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))
Theorem	nna4b4nsq 43514	Strengthening of Fermat's last theorem for exponent 4, where the sum is only assumed to be a square. (Contributed by SN, 23-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) ≠ (𝐶↑2))
Theorem	fltltc 43515	(𝐶↑𝑁) is the largest term and therefore 𝐵 < 𝐶. (Contributed by Steven Nguyen, 22-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → 𝐵 < 𝐶)
Theorem	fltnltalem 43516	Lemma for fltnlta 43517. A lower bound for 𝐴 based on pwdif 15961. (Contributed by Steven Nguyen, 22-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → ((𝐶 − 𝐵) · ((𝐶↑(𝑁 − 1)) + ((𝑁 − 1) · (𝐵↑(𝑁 − 1))))) < (𝐴↑𝑁))
Theorem	fltnlta 43517	In a Fermat counterexample, the exponent 𝑁 is less than all three numbers (𝐴, 𝐵, and 𝐶). Note that 𝐴 < 𝐵 (hypothesis) and 𝐵 < 𝐶 (fltltc 43515). See https://youtu.be/EymVXkPWxyc 43515 for an outline. (Contributed by SN, 24-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝑁 < 𝐴)
21.32.9  Exemplar theorems These theorems were added for illustration or pedagogical purposes without the intention of being used, but some may still be moved to main and used, of course.
Theorem	iddii 43518	Version of a1ii 2 with the hypotheses switched. The first hypothesis is redundant so this theorem should not normally appear in a proof. Inference associated with idd 25. (Contributed by SN, 1-Apr-2025.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ 𝜓
Theorem	bicomdALT 43519	Alternate proof of bicomd 226 which is shorter after expanding all parent theorems (as of 8-Aug-2024, bicom 225 depends on bicom1 224 and sylib 221 depends on syl 18). Additionally, the labels bicom1 224 and syl 18 happen to contain fewer characters than bicom 225 and sylib 221. However, neither of these conditions count as a shortening according to conventions 30888. In the first case, the criteria could easily be broken by upstream changes, and in many cases the upstream dependency tree is nontrivial (see orass 935 and pm2.31 936). For the latter case, theorem labels are up to revision, so they are not counted in the size of a proof. (Contributed by SN, 21-May-2022.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 ↔ 𝜓))
Theorem	alan 43520	Alias for 19.26 1903 for easier lookup. (Contributed by SN, 12-Aug-2025.) (New usage is discouraged.)
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
Theorem	exor 43521	Alias for 19.43 1915 for easier lookup. (Contributed by SN, 5-Jul-2025.) (New usage is discouraged.)
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))
Theorem	rexor 43522	Alias for r19.43 3132 for easier lookup. (Contributed by SN, 5-Jul-2025.) (New usage is discouraged.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))
Theorem	ruvALT 43523	Alternate proof of ruv 9584 with one fewer syntax step thanks to using elirrv 9573 instead of elirr 9576. However, it does not change the compressed proof size or the number of symbols in the generated display, so it is not considered a shortening according to conventions 30888. (Contributed by SN, 1-Sep-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V
Theorem	sn-wcdeq 43524	Alternative to wcdeq 3724 and df-cdeq 3725. This flattens the syntax representation ( wi ( weq vx vy ) wph ) to ( sn-wcdeq vx vy wph ), illustrating the comment of df-cdeq 3725. (Contributed by SN, 26-Sep-2024.) (New usage is discouraged.)
wff (𝑥 = 𝑦 → 𝜑)
Theorem	sq45 43525	45 squared is 2025. (Contributed by SN, 30-Mar-2025.)
⊢ (;45↑2) = ;;;2025
Theorem	sum9cubes 43526	The sum of the first nine perfect cubes is 2025. (Contributed by SN, 30-Mar-2025.)
⊢ Σ𝑘 ∈ (1...9)(𝑘↑3) = ;;;2025
Theorem	sn-isghm 43527*	Longer proof of isghm 19349, unsuccessfully attempting to simplify isghm 19349 using elovmpo 7663 according to an editorial note (now removed). (Contributed by SN, 7-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣)))))
Theorem	aprilfools2025 43528	An abuse of notation. (Contributed by Prof. Loof Lirpa, 1-Apr-2025.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ {⟨“𝐴𝑝𝑟𝑖𝑙”⟩, ⟨“𝑓𝑜𝑜𝑙𝑠!”⟩} ∈ V
21.32.9.1  Standard replacements of ax-10 , ax-11 , ax-12 It is known that ax-10 2178, ax-11 2194, and ax-12 2215 are logically redundant in a weak sense. Practically, they can be replaced with hbn1w 2081, alcomimw 2076, and ax12wlem 2169 as long as you can fully substitute 𝑦 for 𝑥 in the relevant wff (that is, 𝑥 cannot appear in the wff after substituting). This strategy (which I will call a "standard replacement" of axioms) has a lot of potential, for example it works with df-fv 6545 and df-mpt 5191, two very common constructions. But doing a standard replacement of ax-10 2178, ax-11 2194, and ax-12 2215 takes unsatisfyingly long. Usually, if another approach is found, that approach is shorter and better.
Theorem	nfa1w 43529*	Replace ax-10 2178 in nfa1 2188 with a substitution hypothesis. (Contributed by SN, 2-Sep-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ Ⅎ𝑥∀𝑥𝜑
Theorem	eu6w 43530*	Replace ax-10 2178, ax-12 2215 in eu6 2601 with substitution hypotheses. (Contributed by SN, 27-May-2025.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜃))    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
Theorem	abbibw 43531*	Replace ax-10 2178, ax-11 2194, ax-12 2215 in abbib 2831 with substitution hypotheses. (Contributed by SN, 27-May-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ({𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓} ↔ ∀𝑥(𝜑 ↔ 𝜓))
Theorem	absnw 43532*	Replace ax-10 2178, ax-11 2194, ax-12 2215 in absn 4607 with a substitution hypothesis. (Contributed by SN, 27-May-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ({𝑥 ∣ 𝜑} = {𝑌} ↔ ∀𝑥(𝜑 ↔ 𝑥 = 𝑌))
Theorem	euabsn2w 43533*	Replace ax-10 2178, ax-11 2194, ax-12 2215 in euabsn2 4689 with substitution hypotheses. (Contributed by SN, 27-May-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜃))    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦})
21.33  Mathbox for Igor Ieskov
Theorem	cu3addd 43534	Cube of sum of three numbers. (Contributed by Igor Ieskov, 14-Dec-2023.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐶)↑3) = (((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) + (((3 · ((𝐴↑2) · 𝐶)) + (((3 · 2) · (𝐴 · 𝐵)) · 𝐶)) + (3 · ((𝐵↑2) · 𝐶)))) + (((3 · (𝐴 · (𝐶↑2))) + (3 · (𝐵 · (𝐶↑2)))) + (𝐶↑3))))
Theorem	negexpidd 43535	The sum of a real number to the power of N and the negative of the number to the power of N equals zero if N is a nonnegative odd integer. (Contributed by Igor Ieskov, 21-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝑁)    ⇒   ⊢ (𝜑 → ((𝐴↑𝑁) + (-𝐴↑𝑁)) = 0)
Theorem	rexlimdv3d 43536*	An extended version of rexlimdvv 3220 to include three set variables. (Contributed by Igor Ieskov, 21-Jan-2024.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜓 → 𝜒))
Theorem	3cubeslem1 43537	Lemma for 3cubes 43543. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → 0 < (((𝐴 + 1)↑2) − 𝐴))
Theorem	3cubeslem2 43538	Lemma for 3cubes 43543. Used to show that the denominators in 3cubeslem4 43542 are nonzero. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → ¬ ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3) = 0)
Theorem	3cubeslem3l 43539	Lemma for 3cubes 43543. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → (𝐴 · (((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)↑3)) = (((𝐴↑7) · (3↑9)) + (((𝐴↑6) · (3↑9)) + (((𝐴↑5) · ((3↑8) + (3↑8))) + (((𝐴↑4) · (((3↑7) · 2) + (3↑6))) + (((𝐴↑3) · ((3↑6) + (3↑6))) + (((𝐴↑2) · (3↑5)) + (𝐴 · (3↑3)))))))))
Theorem	3cubeslem3r 43540	Lemma for 3cubes 43543. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → ((((((3↑3) · (𝐴↑3)) − 1)↑3) + (((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3)) + ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴))↑3)) = (((𝐴↑7) · (3↑9)) + (((𝐴↑6) · (3↑9)) + (((𝐴↑5) · ((3↑8) + (3↑8))) + (((𝐴↑4) · (((3↑7) · 2) + (3↑6))) + (((𝐴↑3) · ((3↑6) + (3↑6))) + (((𝐴↑2) · (3↑5)) + (𝐴 · (3↑3)))))))))
Theorem	3cubeslem3 43541	Lemma for 3cubes 43543. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → (𝐴 · (((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3)↑3)) = ((((((3↑3) · (𝐴↑3)) − 1)↑3) + (((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1)↑3)) + ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴))↑3)))
Theorem	3cubeslem4 43542	Lemma for 3cubes 43543. This is Ryley's explicit formula for decomposing a rational 𝐴 into a sum of three rational cubes. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → 𝐴 = (((((((3↑3) · (𝐴↑3)) − 1) / ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3))↑3) + ((((-((3↑3) · (𝐴↑3)) + ((3↑2) · 𝐴)) + 1) / ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3))↑3)) + (((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) / ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3))↑3)))
Theorem	3cubes 43543*	Every rational number is a sum of three rational cubes. See S. Ryley, The Ladies' Diary 122 (1825), 35. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝐴 ∈ ℚ ↔ ∃𝑎 ∈ ℚ ∃𝑏 ∈ ℚ ∃𝑐 ∈ ℚ 𝐴 = (((𝑎↑3) + (𝑏↑3)) + (𝑐↑3)))
21.34  Mathbox for OpenAI
Theorem	rntrclfvOAI 43544	The range of the transitive closure is equal to the range of the relation. (Contributed by OpenAI, 7-Jul-2020.)
⊢ (𝑅 ∈ 𝑉 → ran (t+‘𝑅) = ran 𝑅)
21.35  Mathbox for Stefan O'Rear
21.35.1  Additional elementary logic and set theory
Theorem	moxfr 43545*	Transfer at-most-one between related expressions. (Contributed by Stefan O'Rear, 12-Feb-2015.)
⊢ 𝐴 ∈ V    &   ⊢ ∃!𝑦 𝑥 = 𝐴    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓)
21.35.2  Additional theory of functions
Theorem	imaiinfv 43546*	Indexed intersection of an image. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → ∩ 𝑥 ∈ 𝐵 (𝐹‘𝑥) = ∩ (𝐹 “ 𝐵))
21.35.3  Additional topology
Theorem	elrfi 43547*	Elementhood in a set of relative finite intersections. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ 𝐶)) ↔ ∃𝑣 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑣)))
Theorem	elrfirn 43548*	Elementhood in a set of relative finite intersections of an indexed family of sets. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ ran 𝐹)) ↔ ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑦 ∈ 𝑣 (𝐹‘𝑦))))
Theorem	elrfirn2 43549*	Elementhood in a set of relative finite intersections of an indexed family of sets (implicit). (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ ran (𝑦 ∈ 𝐼 ↦ 𝐶))) ↔ ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑦 ∈ 𝑣 𝐶)))
Theorem	cmpfiiin 43550*	In a compact topology, a system of closed sets with nonempty finite intersections has a nonempty intersection. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝑆 ∈ (Clsd‘𝐽))    &   ⊢ ((𝜑 ∧ (𝑙 ⊆ 𝐼 ∧ 𝑙 ∈ Fin)) → (𝑋 ∩ ∩ 𝑘 ∈ 𝑙 𝑆) ≠ ∅)    ⇒   ⊢ (𝜑 → (𝑋 ∩ ∩ 𝑘 ∈ 𝐼 𝑆) ≠ ∅)
21.35.4  Characterization of closure operators. Kuratowski closure axioms
Theorem	ismrcd1 43551*	Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 17711), isotone (satisfies mrcss 17710), and idempotent (satisfies mrcidm 17713) has a collection of fixed points which is a Moore collection, and itself is the closure operator for that collection. This can be taken as an alternate definition for the closure operators. This is the first half, ismrcd2 43552 is the second. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵))
Theorem	ismrcd2 43552*	Second half of ismrcd1 43551. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → 𝐹 = (mrCls‘dom (𝐹 ∩ I )))
Theorem	istopclsd 43553*	A closure function which satisfies sscls 23287, clsidm 23298, cls0 23311, and clsun 36955 defines a (unique) topology which it is the closure function on. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥))    &   ⊢ (𝜑 → (𝐹‘∅) = ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝐵) → (𝐹‘(𝑥 ∪ 𝑦)) = ((𝐹‘𝑥) ∪ (𝐹‘𝑦)))    &   ⊢ 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐹‘(𝐵 ∖ 𝑧)) = (𝐵 ∖ 𝑧)}    ⇒   ⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ (cls‘𝐽) = 𝐹))
Theorem	ismrc 43554*	A function is a Moore closure operator iff it satisfies mrcssid 17711, mrcss 17710, and mrcidm 17713. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐹 ∈ (mrCls “ (Moore‘𝐵)) ↔ (𝐵 ∈ V ∧ 𝐹:𝒫 𝐵⟶𝒫 𝐵 ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝑥 ⊆ (𝐹‘𝑥) ∧ (𝐹‘𝑦) ⊆ (𝐹‘𝑥) ∧ (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)))))
21.35.5  Algebraic closure systems
Syntax	cnacs 43555	Class of Noetherian closure systems.
class NoeACS
Definition	df-nacs 43556*	Define a closure system of Noetherian type (not standard terminology) as an algebraic system where all closed sets are finitely generated. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ NoeACS = (𝑥 ∈ V ↦ {𝑐 ∈ (ACS‘𝑥) ∣ ∀𝑠 ∈ 𝑐 ∃𝑔 ∈ (𝒫 𝑥 ∩ Fin)𝑠 = ((mrCls‘𝑐)‘𝑔)})
Theorem	isnacs 43557*	Expand definition of Noetherian-type closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ ∀𝑠 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑠 = (𝐹‘𝑔)))
Theorem	nacsfg 43558*	In a Noetherian-type closure system, all closed sets are finitely generated. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑆 ∈ 𝐶) → ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑆 = (𝐹‘𝑔))
Theorem	isnacs2 43559	Express Noetherian-type closure system with fewer quantifiers. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ (𝐹 “ (𝒫 𝑋 ∩ Fin)) = 𝐶))
Theorem	mrefg2 43560*	Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑆 = (𝐹‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑆 ∩ Fin)𝑆 = (𝐹‘𝑔)))
Theorem	mrefg3 43561*	Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ∈ 𝐶) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑆 = (𝐹‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑆 ∩ Fin)𝑆 ⊆ (𝐹‘𝑔)))
Theorem	nacsacs 43562	A closure system of Noetherian type is algebraic. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ (𝐶 ∈ (NoeACS‘𝑋) → 𝐶 ∈ (ACS‘𝑋))
Theorem	isnacs3 43563*	A choice-free order equivalent to the Noetherian condition on a closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠 ∈ 𝑠)))
Theorem	incssnn0 43564*	Transitivity induction of subsets, lemma for nacsfix 43565. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ ((∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵))
Theorem	nacsfix 43565*	An increasing sequence of closed sets in a Noetherian-type closure system eventually fixates. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝐹:ℕ0⟶𝐶 ∧ ∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → ∃𝑦 ∈ ℕ0 ∀𝑧 ∈ (ℤ≥‘𝑦)(𝐹‘𝑧) = (𝐹‘𝑦))
21.35.6  Miscellanea 1. Map utilities
Theorem	constmap 43566	A constant (represented without dummy variables) is an element of a function set. Note: In the following development, we will be quite often quantifying over functions and points in N-dimensional space (which are equivalent to functions from an "index set"). Many of the following theorems exist to transfer standard facts about functions to elements of function sets. (Contributed by Stefan O'Rear, 30-Aug-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}) ∈ (𝐶 ↑m 𝐴))
Theorem	mapco2g 43567	Renaming indices in a tuple, with sethood as antecedents. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.)
⊢ ((𝐸 ∈ V ∧ 𝐴 ∈ (𝐵 ↑m 𝐶) ∧ 𝐷:𝐸⟶𝐶) → (𝐴 ∘ 𝐷) ∈ (𝐵 ↑m 𝐸))
Theorem	mapco2 43568	Post-composition (renaming indices) of a mapping viewed as a point. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
⊢ 𝐸 ∈ V    ⇒   ⊢ ((𝐴 ∈ (𝐵 ↑m 𝐶) ∧ 𝐷:𝐸⟶𝐶) → (𝐴 ∘ 𝐷) ∈ (𝐵 ↑m 𝐸))
Theorem	mapfzcons 43569	Extending a one-based mapping by adding a tuple at the end results in another mapping. (Contributed by Stefan O'Rear, 10-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
⊢ 𝑀 = (𝑁 + 1)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → (𝐴 ∪ {⟨𝑀, 𝐶⟩}) ∈ (𝐵 ↑m (1...𝑀)))
Theorem	mapfzcons1 43570	Recover prefix mapping from an extended mapping. (Contributed by Stefan O'Rear, 10-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
⊢ 𝑀 = (𝑁 + 1)    ⇒   ⊢ (𝐴 ∈ (𝐵 ↑m (1...𝑁)) → ((𝐴 ∪ {⟨𝑀, 𝐶⟩}) ↾ (1...𝑁)) = 𝐴)
Theorem	mapfzcons1cl 43571	A nonempty mapping has a prefix. (Contributed by Stefan O'Rear, 10-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
⊢ 𝑀 = (𝑁 + 1)    ⇒   ⊢ (𝐴 ∈ (𝐵 ↑m (1...𝑀)) → (𝐴 ↾ (1...𝑁)) ∈ (𝐵 ↑m (1...𝑁)))
Theorem	mapfzcons2 43572	Recover added element from an extended mapping. (Contributed by Stefan O'Rear, 10-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
⊢ 𝑀 = (𝑁 + 1)    ⇒   ⊢ ((𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → ((𝐴 ∪ {⟨𝑀, 𝐶⟩})‘𝑀) = 𝐶)
21.35.7  Miscellanea for polynomials
Theorem	mptfcl 43573*	Interpret range of a maps-to notation as a constraint on the definition. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ ((𝑡 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶 → (𝑡 ∈ 𝐴 → 𝐵 ∈ 𝐶))
21.35.8  Multivariate polynomials over the integers
Syntax	cmzpcl 43574	Extend class notation to include pre-polynomial rings.
class mzPolyCld
Syntax	cmzp 43575	Extend class notation to include polynomial rings.
class mzPoly
Definition	df-mzpcl 43576*	Define the polynomially closed function rings over an arbitrary index set 𝑣. The set (mzPolyCld‘𝑣) contains all sets of functions from (ℤ ↑m 𝑣) to ℤ which include all constants and projections and are closed under addition and multiplication. This is a "temporary" set used to define the polynomial function ring itself (mzPoly‘𝑣); see df-mzp 43577. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ mzPolyCld = (𝑣 ∈ V ↦ {𝑝 ∈ 𝒫 (ℤ ↑m (ℤ ↑m 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))})
Definition	df-mzp 43577	Polynomials over ℤ with an arbitrary index set, that is, the smallest ring of functions containing all constant functions and all projections. This is almost the most general reasonable definition; to reach full generality, we would need to be able to replace ZZ with an arbitrary (semi)ring (and a coordinate subring), but rings have not been defined yet. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ mzPoly = (𝑣 ∈ V ↦ ∩ (mzPolyCld‘𝑣))
Theorem	mzpclval 43578*	Substitution lemma for mzPolyCld. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (𝑉 ∈ V → (mzPolyCld‘𝑉) = {𝑝 ∈ 𝒫 (ℤ ↑m (ℤ ↑m 𝑉)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑉) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))})
Theorem	elmzpcl 43579*	Double substitution lemma for mzPolyCld. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (𝑉 ∈ V → (𝑃 ∈ (mzPolyCld‘𝑉) ↔ (𝑃 ⊆ (ℤ ↑m (ℤ ↑m 𝑉)) ∧ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑉) × {𝑖}) ∈ 𝑃 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑃) ∧ ∀𝑓 ∈ 𝑃 ∀𝑔 ∈ 𝑃 ((𝑓 ∘f + 𝑔) ∈ 𝑃 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑃)))))
Theorem	mzpclall 43580	The set of all functions with the signature of a polynomial is a polynomially closed set. This is a lemma to show that the intersection in df-mzp 43577 is well-defined. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (𝑉 ∈ V → (ℤ ↑m (ℤ ↑m 𝑉)) ∈ (mzPolyCld‘𝑉))
Theorem	mzpcln0 43581	Corollary of mzpclall 43580: polynomially closed function sets are not empty. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (𝑉 ∈ V → (mzPolyCld‘𝑉) ≠ ∅)
Theorem	mzpcl1 43582	Defining property 1 of a polynomially closed function set 𝑃: it contains all constant functions. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝑃 ∈ (mzPolyCld‘𝑉) ∧ 𝐹 ∈ ℤ) → ((ℤ ↑m 𝑉) × {𝐹}) ∈ 𝑃)
Theorem	mzpcl2 43583*	Defining property 2 of a polynomially closed function set 𝑃: it contains all projections. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝑃 ∈ (mzPolyCld‘𝑉) ∧ 𝐹 ∈ 𝑉) → (𝑔 ∈ (ℤ ↑m 𝑉) ↦ (𝑔‘𝐹)) ∈ 𝑃)
Theorem	mzpcl34 43584	Defining properties 3 and 4 of a polynomially closed function set 𝑃: it is closed under pointwise addition and multiplication. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝑃 ∈ (mzPolyCld‘𝑉) ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃) → ((𝐹 ∘f + 𝐺) ∈ 𝑃 ∧ (𝐹 ∘f · 𝐺) ∈ 𝑃))
Theorem	mzpval 43585	Value of the mzPoly function. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (𝑉 ∈ V → (mzPoly‘𝑉) = ∩ (mzPolyCld‘𝑉))
Theorem	dmmzp 43586	mzPoly is defined for all index sets which are sets. This is used with elfvdm 6916 to eliminate sethood antecedents. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ dom mzPoly = V
Theorem	mzpincl 43587	Polynomial closedness is a universal first-order property and passes to intersections. This is where the closure properties of the polynomial ring itself are proved. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (𝑉 ∈ V → (mzPoly‘𝑉) ∈ (mzPolyCld‘𝑉))
Theorem	mzpconst 43588	Constant functions are polynomial. See also mzpconstmpt 43593. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝑉 ∈ V ∧ 𝐶 ∈ ℤ) → ((ℤ ↑m 𝑉) × {𝐶}) ∈ (mzPoly‘𝑉))
Theorem	mzpf 43589	A polynomial function is a function from the coordinate space to the integers. (Contributed by Stefan O'Rear, 5-Oct-2014.)
⊢ (𝐹 ∈ (mzPoly‘𝑉) → 𝐹:(ℤ ↑m 𝑉)⟶ℤ)
Theorem	mzpproj 43590*	A projection function is polynomial. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝑉 ∈ V ∧ 𝑋 ∈ 𝑉) → (𝑔 ∈ (ℤ ↑m 𝑉) ↦ (𝑔‘𝑋)) ∈ (mzPoly‘𝑉))
Theorem	mzpadd 43591	The pointwise sum of two polynomial functions is a polynomial function. See also mzpaddmpt 43594. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝐴 ∈ (mzPoly‘𝑉) ∧ 𝐵 ∈ (mzPoly‘𝑉)) → (𝐴 ∘f + 𝐵) ∈ (mzPoly‘𝑉))
Theorem	mzpmul 43592	The pointwise product of two polynomial functions is a polynomial function. See also mzpmulmpt 43595. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝐴 ∈ (mzPoly‘𝑉) ∧ 𝐵 ∈ (mzPoly‘𝑉)) → (𝐴 ∘f · 𝐵) ∈ (mzPoly‘𝑉))
Theorem	mzpconstmpt 43593*	A constant function expressed in maps-to notation is polynomial. This theorem and the several that follow (mzpaddmpt 43594, mzpmulmpt 43595, mzpnegmpt 43597, mzpsubmpt 43596, mzpexpmpt 43598) can be used to build proofs that functions which are "manifestly polynomial", in the sense of being a maps-to containing constants, projections, and simple arithmetic operations, are actually polynomial functions. There is no mzpprojmpt because mzpproj 43590 is already expressed using maps-to notation. (Contributed by Stefan O'Rear, 5-Oct-2014.)
⊢ ((𝑉 ∈ V ∧ 𝐶 ∈ ℤ) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐶) ∈ (mzPoly‘𝑉))
Theorem	mzpaddmpt 43594*	Sum of polynomial functions is polynomial. Maps-to version of mzpadd 43591. (Contributed by Stefan O'Rear, 5-Oct-2014.)
⊢ (((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴 + 𝐵)) ∈ (mzPoly‘𝑉))
Theorem	mzpmulmpt 43595*	Product of polynomial functions is polynomial. Maps-to version of mzpmulmpt 43595. (Contributed by Stefan O'Rear, 5-Oct-2014.)
⊢ (((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴 · 𝐵)) ∈ (mzPoly‘𝑉))
Theorem	mzpsubmpt 43596*	The difference of two polynomial functions is polynomial. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴 − 𝐵)) ∈ (mzPoly‘𝑉))
Theorem	mzpnegmpt 43597*	Negation of a polynomial function. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ ((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ -𝐴) ∈ (mzPoly‘𝑉))
Theorem	mzpexpmpt 43598*	Raise a polynomial function to a (fixed) exponent. (Contributed by Stefan O'Rear, 5-Oct-2014.)
⊢ (((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ 𝐷 ∈ ℕ0) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝐷)) ∈ (mzPoly‘𝑉))
Theorem	mzpindd 43599*	"Structural" induction to prove properties of all polynomial functions. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝜑 ∧ 𝑓 ∈ ℤ) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑉) → 𝜃)    &   ⊢ ((𝜑 ∧ (𝑓:(ℤ ↑m 𝑉)⟶ℤ ∧ 𝜏) ∧ (𝑔:(ℤ ↑m 𝑉)⟶ℤ ∧ 𝜂)) → 𝜁)    &   ⊢ ((𝜑 ∧ (𝑓:(ℤ ↑m 𝑉)⟶ℤ ∧ 𝜏) ∧ (𝑔:(ℤ ↑m 𝑉)⟶ℤ ∧ 𝜂)) → 𝜎)    &   ⊢ (𝑥 = ((ℤ ↑m 𝑉) × {𝑓}) → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑔 ∈ (ℤ ↑m 𝑉) ↦ (𝑔‘𝑓)) → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = 𝑓 → (𝜓 ↔ 𝜏))    &   ⊢ (𝑥 = 𝑔 → (𝜓 ↔ 𝜂))    &   ⊢ (𝑥 = (𝑓 ∘f + 𝑔) → (𝜓 ↔ 𝜁))    &   ⊢ (𝑥 = (𝑓 ∘f · 𝑔) → (𝜓 ↔ 𝜎))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜌))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ (mzPoly‘𝑉)) → 𝜌)
Theorem	mzpmfp 43600	Relationship between multivariate Z-polynomials and general multivariate polynomial functions. (Contributed by Stefan O'Rear, 20-Mar-2015.) (Revised by AV, 13-Jun-2019.)
⊢ (mzPoly‘𝐼) = ran (𝐼 eval ℤring)