P. 427 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42601-42700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	prjcrvfval 42601*	Value of the projective curve function. (Contributed by SN, 23-Nov-2024.)
⊢ 𝐻 = ((0...𝑁) mHomP 𝐾)    &   ⊢ 𝐸 = ((0...𝑁) eval 𝐾)    &   ⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾)    &   ⊢ 0 = (0g‘𝐾)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ Field)    ⇒   ⊢ (𝜑 → (𝑁ℙ𝕣𝕠𝕛Crv𝐾) = (𝑓 ∈ ∪ ran 𝐻 ↦ {𝑝 ∈ 𝑃 ∣ ((𝐸‘𝑓) “ 𝑝) = { 0 }}))
Theorem	prjcrvval 42602*	Value of the projective curve function. (Contributed by SN, 23-Nov-2024.)
⊢ 𝐻 = ((0...𝑁) mHomP 𝐾)    &   ⊢ 𝐸 = ((0...𝑁) eval 𝐾)    &   ⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾)    &   ⊢ 0 = (0g‘𝐾)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ ∪ ran 𝐻)    ⇒   ⊢ (𝜑 → ((𝑁ℙ𝕣𝕠𝕛Crv𝐾)‘𝐹) = {𝑝 ∈ 𝑃 ∣ ((𝐸‘𝐹) “ 𝑝) = { 0 }})
Theorem	prjcrv0 42603	The "curve" (zero set) corresponding to the zero polynomial contains all coordinates. (Contributed by SN, 23-Nov-2024.)
⊢ 𝑌 = ((0...𝑁) mPoly 𝐾)    &   ⊢ 0 = (0g‘𝑌)    &   ⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ Field)    ⇒   ⊢ (𝜑 → ((𝑁ℙ𝕣𝕠𝕛Crv𝐾)‘ 0 ) = 𝑃)
21.30.8  Basic reductions for Fermat's Last Theorem
Theorem	dffltz 42604*	Fermat's Last Theorem (FLT) for nonzero integers is equivalent to the original scope of natural numbers. The backwards direction takes (𝑎↑𝑛) + (𝑏↑𝑛) = (𝑐↑𝑛), and adds the negative of any negative term to both sides, thus creating the corresponding equation with only positive integers. There are six combinations of negativity, so the proof is particularly long. (Contributed by Steven Nguyen, 27-Feb-2023.)
⊢ (∀𝑛 ∈ (ℤ≥‘3)∀𝑥 ∈ ℕ ∀𝑦 ∈ ℕ ∀𝑧 ∈ ℕ ((𝑥↑𝑛) + (𝑦↑𝑛)) ≠ (𝑧↑𝑛) ↔ ∀𝑛 ∈ (ℤ≥‘3)∀𝑎 ∈ (ℤ ∖ {0})∀𝑏 ∈ (ℤ ∖ {0})∀𝑐 ∈ (ℤ ∖ {0})((𝑎↑𝑛) + (𝑏↑𝑛)) ≠ (𝑐↑𝑛))
Theorem	fltmul 42605	A counterexample to FLT stays valid when scaled. The hypotheses are more general than they need to be for convenience. (There does not seem to be a standard term for Fermat or Pythagorean triples extended to any 𝑁 ∈ ℕ0, so the label is more about the context in which this theorem is used). (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → (((𝑆 · 𝐴)↑𝑁) + ((𝑆 · 𝐵)↑𝑁)) = ((𝑆 · 𝐶)↑𝑁))
Theorem	fltdiv 42606	A counterexample to FLT stays valid when scaled. The hypotheses are more general than they need to be for convenience. (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 𝑆 ≠ 0)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → (((𝐴 / 𝑆)↑𝑁) + ((𝐵 / 𝑆)↑𝑁)) = ((𝐶 / 𝑆)↑𝑁))
Theorem	flt0 42607	A counterexample for FLT does not exist for 𝑁 = 0. (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℕ)
Theorem	fltdvdsabdvdsc 42608	Any factor of both 𝐴 and 𝐵 also divides 𝐶. This establishes the validity of fltabcoprmex 42609. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐶)
Theorem	fltabcoprmex 42609	A counterexample to FLT implies a counterexample to FLT with 𝐴, 𝐵 (assigned to 𝐴 / (𝐴 gcd 𝐵) and 𝐵 / (𝐴 gcd 𝐵)) coprime (by divgcdcoprm0 16682). (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → (((𝐴 / (𝐴 gcd 𝐵))↑𝑁) + ((𝐵 / (𝐴 gcd 𝐵))↑𝑁)) = ((𝐶 / (𝐴 gcd 𝐵))↑𝑁))
Theorem	fltaccoprm 42610	A counterexample to FLT with 𝐴, 𝐵 coprime also has 𝐴, 𝐶 coprime. (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    ⇒   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)
Theorem	fltbccoprm 42611	A counterexample to FLT with 𝐴, 𝐵 coprime also has 𝐵, 𝐶 coprime. Proven from fltaccoprm 42610 using commutativity of addition. (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    ⇒   ⊢ (𝜑 → (𝐵 gcd 𝐶) = 1)
Theorem	fltabcoprm 42612	A counterexample to FLT with 𝐴, 𝐶 coprime also has 𝐴, 𝐵 coprime. Converse of fltaccoprm 42610. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)
Theorem	infdesc 42613*	Infinite descent. The hypotheses say that 𝑆 is lower bounded, and that if 𝜓 holds for an integer in 𝑆, it holds for a smaller integer in 𝑆. By infinite descent, eventually we cannot go any smaller, therefore 𝜓 holds for no integer in 𝑆. (Contributed by SN, 20-Aug-2024.)
⊢ (𝑦 = 𝑥 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 → 𝑆 ⊆ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝜒)) → ∃𝑧 ∈ 𝑆 (𝜃 ∧ 𝑧 < 𝑥))    ⇒   ⊢ (𝜑 → {𝑦 ∈ 𝑆 ∣ 𝜓} = ∅)
Theorem	fltne 42614	If a counterexample to FLT exists, its addends are not equal. (Contributed by SN, 1-Jun-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	flt4lem 42615	Raising a number to the fourth power is equivalent to squaring it twice. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑4) = ((𝐴↑2)↑2))
Theorem	flt4lem1 42616	Satisfy the antecedent used in several pythagtrip 16852 lemmas, with 𝐴, 𝐶 coprime rather than 𝐴, 𝐵. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)))
Theorem	flt4lem2 42617	If 𝐴 is even, 𝐵 is odd. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ¬ 2 ∥ 𝐵)
Theorem	flt4lem3 42618	Equivalent to pythagtriplem4 16837. Show that 𝐶 + 𝐴 and 𝐶 − 𝐴 are coprime. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ((𝐶 + 𝐴) gcd (𝐶 − 𝐴)) = 1)
Theorem	flt4lem4 42619	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 42620	In the context of the lemmas of pythagtrip 16852, 𝑀 and 𝑁 are coprime. (Contributed by SN, 23-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)    ⇒   ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑀 gcd 𝑁) = 1)
Theorem	flt4lem5elem 42621	Version of fltaccoprm 42610 and fltbccoprm 42611 where 𝑀 is not squared. This can be proved in general for any polynomial in three variables: using prmdvdsncoprmbd 16744, dvds2addd 16309, and prmdvdsexp 16732, 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 42622	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 42623	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 42624	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 42625	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 42626	Satisfy the hypotheses of flt4lem4 42619. (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 42627	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 42628	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 42629*	Convert flt4lem5f 42627 into a convenient form for nna4b4nsq 42630. 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 42630	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 42631	(𝐶↑𝑁) is the largest term and therefore 𝐵 < 𝐶. (Contributed by Steven Nguyen, 22-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → 𝐵 < 𝐶)
Theorem	fltnltalem 42632	Lemma for fltnlta 42633. A lower bound for 𝐴 based on pwdif 15882. (Contributed by Steven Nguyen, 22-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → ((𝐶 − 𝐵) · ((𝐶↑(𝑁 − 1)) + ((𝑁 − 1) · (𝐵↑(𝑁 − 1))))) < (𝐴↑𝑁))
Theorem	fltnlta 42633	In a Fermat counterexample, the exponent 𝑁 is less than all three numbers (𝐴, 𝐵, and 𝐶). Note that 𝐴 < 𝐵 (hypothesis) and 𝐵 < 𝐶 (fltltc 42631). See https://youtu.be/EymVXkPWxyc 42631 for an outline. (Contributed by SN, 24-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝑁 < 𝐴)
21.30.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 42634	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 24. (Contributed by SN, 1-Apr-2025.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ 𝜓
Theorem	bicomdALT 42635	Alternate proof of bicomd 223 which is shorter after expanding all parent theorems (as of 8-Aug-2024, bicom 222 depends on bicom1 221 and sylib 218 depends on syl 17). Additionally, the labels bicom1 221 and syl 17 happen to contain fewer characters than bicom 222 and sylib 218. However, neither of these conditions count as a shortening according to conventions 30327. 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 921 and pm2.31 922). 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 42636	Alias for 19.26 1870 for easier lookup. (Contributed by SN, 12-Aug-2025.) (New usage is discouraged.)
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
Theorem	exor 42637	Alias for 19.43 1882 for easier lookup. (Contributed by SN, 5-Jul-2025.) (New usage is discouraged.)
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))
Theorem	rexor 42638	Alias for r19.43 3108 for easier lookup. (Contributed by SN, 5-Jul-2025.) (New usage is discouraged.)
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))
Theorem	ruvALT 42639	Alternate proof of ruv 9614 with one fewer syntax step thanks to using elirrv 9608 instead of elirr 9609. 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 30327. (Contributed by SN, 1-Sep-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V
Theorem	sn-wcdeq 42640	Alternative to wcdeq 3746 and df-cdeq 3747. This flattens the syntax representation ( wi ( weq vx vy ) wph ) to ( sn-wcdeq vx vy wph ), illustrating the comment of df-cdeq 3747. (Contributed by SN, 26-Sep-2024.) (New usage is discouraged.)
wff (𝑥 = 𝑦 → 𝜑)
Theorem	sq45 42641	45 squared is 2025. (Contributed by SN, 30-Mar-2025.)
⊢ (;45↑2) = ;;;2025
Theorem	sum9cubes 42642	The sum of the first nine perfect cubes is 2025. (Contributed by SN, 30-Mar-2025.)
⊢ Σ𝑘 ∈ (1...9)(𝑘↑3) = ;;;2025
Theorem	sn-isghm 42643*	Longer proof of isghm 19196, unsuccessfully attempting to simplify isghm 19196 using elovmpo 7650 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 42644	An abuse of notation. (Contributed by Prof. Loof Lirpa, 1-Apr-2025.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ {⟨“𝐴𝑝𝑟𝑖𝑙”⟩, ⟨“𝑓𝑜𝑜𝑙𝑠!”⟩} ∈ V
21.30.9.1  Standard replacements of ax-10 , ax-11 , ax-12 It is known that ax-10 2141, ax-11 2157, and ax-12 2177 are logically redundant in a weak sense. Practically, they can be replaced with hbn1w 2046, alcomimw 2042, and ax12wlem 2132 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 6538 and df-mpt 5202, two very common constructions. But doing a standard replacement of ax-10 2141, ax-11 2157, and ax-12 2177 takes unsatisfyingly long. Usually, if another approach is found, that approach is shorter and better.
Theorem	nfa1w 42645*	Replace ax-10 2141 in nfa1 2151 with a substitution hypothesis. (Contributed by SN, 2-Sep-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ Ⅎ𝑥∀𝑥𝜑
Theorem	eu6w 42646*	Replace ax-10 2141, ax-12 2177 in eu6 2573 with substitution hypotheses. (Contributed by SN, 27-May-2025.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜃))    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
Theorem	abbibw 42647*	Replace ax-10 2141, ax-11 2157, ax-12 2177 in abbib 2804 with substitution hypotheses. (Contributed by SN, 27-May-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ({𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓} ↔ ∀𝑥(𝜑 ↔ 𝜓))
Theorem	absnw 42648*	Replace ax-10 2141, ax-11 2157, ax-12 2177 in absn 4621 with a substitution hypothesis. (Contributed by SN, 27-May-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ({𝑥 ∣ 𝜑} = {𝑌} ↔ ∀𝑥(𝜑 ↔ 𝑥 = 𝑌))
Theorem	euabsn2w 42649*	Replace ax-10 2141, ax-11 2157, ax-12 2177 in euabsn2 4701 with substitution hypotheses. (Contributed by SN, 27-May-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜃))    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦})
Theorem	sn-tz6.12-2 42650*	tz6.12-2 6863 without ax-10 2141, ax-11 2157, ax-12 2177. Improves 118 theorems. (Contributed by SN, 27-May-2025.)
⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
21.31  Mathbox for Igor Ieskov
Theorem	cu3addd 42651	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 42652	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 42653*	An extended version of rexlimdvv 3197 to include three set variables. (Contributed by Igor Ieskov, 21-Jan-2024.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜓 → 𝜒))
Theorem	3cubeslem1 42654	Lemma for 3cubes 42660. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → 0 < (((𝐴 + 1)↑2) − 𝐴))
Theorem	3cubeslem2 42655	Lemma for 3cubes 42660. Used to show that the denominators in 3cubeslem4 42659 are nonzero. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → ¬ ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3) = 0)
Theorem	3cubeslem3l 42656	Lemma for 3cubes 42660. (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 42657	Lemma for 3cubes 42660. (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 42658	Lemma for 3cubes 42660. (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 42659	Lemma for 3cubes 42660. 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 42660*	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.32  Mathbox for OpenAI
Theorem	rntrclfvOAI 42661	The range of the transitive closure is equal to the range of the relation. (Contributed by OpenAI, 7-Jul-2020.)
⊢ (𝑅 ∈ 𝑉 → ran (t+‘𝑅) = ran 𝑅)
21.33  Mathbox for Stefan O'Rear
21.33.1  Additional elementary logic and set theory
Theorem	moxfr 42662*	Transfer at-most-one between related expressions. (Contributed by Stefan O'Rear, 12-Feb-2015.)
⊢ 𝐴 ∈ V    &   ⊢ ∃!𝑦 𝑥 = 𝐴    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓)
21.33.2  Additional theory of functions
Theorem	imaiinfv 42663*	Indexed intersection of an image. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → ∩ 𝑥 ∈ 𝐵 (𝐹‘𝑥) = ∩ (𝐹 “ 𝐵))
21.33.3  Additional topology
Theorem	elrfi 42664*	Elementhood in a set of relative finite intersections. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ 𝐶)) ↔ ∃𝑣 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑣)))
Theorem	elrfirn 42665*	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 42666*	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 42667*	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.33.4  Characterization of closure operators. Kuratowski closure axioms
Theorem	ismrcd1 42668*	Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 17627), isotone (satisfies mrcss 17626), and idempotent (satisfies mrcidm 17629) 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 42669 is the second. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵))
Theorem	ismrcd2 42669*	Second half of ismrcd1 42668. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → 𝐹 = (mrCls‘dom (𝐹 ∩ I )))
Theorem	istopclsd 42670*	A closure function which satisfies sscls 22992, clsidm 23003, cls0 23016, and clsun 36292 defines a (unique) topology which it is the closure function on. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥))    &   ⊢ (𝜑 → (𝐹‘∅) = ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝐵) → (𝐹‘(𝑥 ∪ 𝑦)) = ((𝐹‘𝑥) ∪ (𝐹‘𝑦)))    &   ⊢ 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐹‘(𝐵 ∖ 𝑧)) = (𝐵 ∖ 𝑧)}    ⇒   ⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ (cls‘𝐽) = 𝐹))
Theorem	ismrc 42671*	A function is a Moore closure operator iff it satisfies mrcssid 17627, mrcss 17626, and mrcidm 17629. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐹 ∈ (mrCls “ (Moore‘𝐵)) ↔ (𝐵 ∈ V ∧ 𝐹:𝒫 𝐵⟶𝒫 𝐵 ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝑥 ⊆ (𝐹‘𝑥) ∧ (𝐹‘𝑦) ⊆ (𝐹‘𝑥) ∧ (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)))))
21.33.5  Algebraic closure systems
Syntax	cnacs 42672	Class of Noetherian closure systems.
class NoeACS
Definition	df-nacs 42673*	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 42674*	Expand definition of Noetherian-type closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ ∀𝑠 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑠 = (𝐹‘𝑔)))
Theorem	nacsfg 42675*	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 42676	Express Noetherian-type closure system with fewer quantifiers. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ (𝐹 “ (𝒫 𝑋 ∩ Fin)) = 𝐶))
Theorem	mrefg2 42677*	Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑆 = (𝐹‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑆 ∩ Fin)𝑆 = (𝐹‘𝑔)))
Theorem	mrefg3 42678*	Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ∈ 𝐶) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑆 = (𝐹‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑆 ∩ Fin)𝑆 ⊆ (𝐹‘𝑔)))
Theorem	nacsacs 42679	A closure system of Noetherian type is algebraic. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ (𝐶 ∈ (NoeACS‘𝑋) → 𝐶 ∈ (ACS‘𝑋))
Theorem	isnacs3 42680*	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 42681*	Transitivity induction of subsets, lemma for nacsfix 42682. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ ((∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵))
Theorem	nacsfix 42682*	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.33.6  Miscellanea 1. Map utilities
Theorem	constmap 42683	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 42684	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 42685	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 42686	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 42687	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 42688	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 42689	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.33.7  Miscellanea for polynomials
Theorem	mptfcl 42690*	Interpret range of a maps-to notation as a constraint on the definition. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ ((𝑡 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶 → (𝑡 ∈ 𝐴 → 𝐵 ∈ 𝐶))
21.33.8  Multivariate polynomials over the integers
Syntax	cmzpcl 42691	Extend class notation to include pre-polynomial rings.
class mzPolyCld
Syntax	cmzp 42692	Extend class notation to include polynomial rings.
class mzPoly
Definition	df-mzpcl 42693*	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 42694. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ mzPolyCld = (𝑣 ∈ V ↦ {𝑝 ∈ 𝒫 (ℤ ↑m (ℤ ↑m 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))})
Definition	df-mzp 42694	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 42695*	Substitution lemma for mzPolyCld. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (𝑉 ∈ V → (mzPolyCld‘𝑉) = {𝑝 ∈ 𝒫 (ℤ ↑m (ℤ ↑m 𝑉)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑉) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))})
Theorem	elmzpcl 42696*	Double substitution lemma for mzPolyCld. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (𝑉 ∈ V → (𝑃 ∈ (mzPolyCld‘𝑉) ↔ (𝑃 ⊆ (ℤ ↑m (ℤ ↑m 𝑉)) ∧ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑉) × {𝑖}) ∈ 𝑃 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑃) ∧ ∀𝑓 ∈ 𝑃 ∀𝑔 ∈ 𝑃 ((𝑓 ∘f + 𝑔) ∈ 𝑃 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑃)))))
Theorem	mzpclall 42697	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 42694 is well-defined. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (𝑉 ∈ V → (ℤ ↑m (ℤ ↑m 𝑉)) ∈ (mzPolyCld‘𝑉))
Theorem	mzpcln0 42698	Corollary of mzpclall 42697: polynomially closed function sets are not empty. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (𝑉 ∈ V → (mzPolyCld‘𝑉) ≠ ∅)
Theorem	mzpcl1 42699	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 42700*	Defining property 2 of a polynomially closed function set 𝑃: it contains all projections. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝑃 ∈ (mzPolyCld‘𝑉) ∧ 𝐹 ∈ 𝑉) → (𝑔 ∈ (ℤ ↑m 𝑉) ↦ (𝑔‘𝐹)) ∈ 𝑃)