P. 406 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40501-40600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	flt4lem5f 40501	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 40502	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 40503*	Convert flt4lem5f 40501 into a convenient form for nna4b4nsq 40504. 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 40504	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 40505	(𝐶↑𝑁) is the largest term and therefore 𝐵 < 𝐶. (Contributed by Steven Nguyen, 22-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → 𝐵 < 𝐶)
Theorem	fltnltalem 40506	Lemma for fltnlta 40507. A lower bound for 𝐴 based on pwdif 15589. (Contributed by Steven Nguyen, 22-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → ((𝐶 − 𝐵) · ((𝐶↑(𝑁 − 1)) + ((𝑁 − 1) · (𝐵↑(𝑁 − 1))))) < (𝐴↑𝑁))
Theorem	fltnlta 40507	In a Fermat counterexample, the exponent 𝑁 is less than all three numbers (𝐴, 𝐵, and 𝐶). Note that 𝐴 < 𝐵 (hypothesis) and 𝐵 < 𝐶 (fltltc 40505). See https://youtu.be/EymVXkPWxyc 40505 for an outline. (Contributed by SN, 24-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝑁 < 𝐴)
20.27  Mathbox for Igor Ieskov
Theorem	binom2d 40508	Deduction form of binom2. (Contributed by Igor Ieskov, 14-Dec-2023.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)))
Theorem	cu3addd 40509	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	sqnegd 40510	The square of the negative of a number. (Contributed by Igor Ieskov, 21-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (-𝐴↑2) = (𝐴↑2))
Theorem	negexpidd 40511	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 40512*	An extended version of rexlimdvv 3223 to include three set variables. (Contributed by Igor Ieskov, 21-Jan-2024.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜓 → 𝜒))
Theorem	3cubeslem1 40513	Lemma for 3cubes 40519. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → 0 < (((𝐴 + 1)↑2) − 𝐴))
Theorem	3cubeslem2 40514	Lemma for 3cubes 40519. Used to show that the denominators in 3cubeslem4 40518 are nonzero. (Contributed by Igor Ieskov, 22-Jan-2024.)
⊢ (𝜑 → 𝐴 ∈ ℚ)    ⇒   ⊢ (𝜑 → ¬ ((((3↑3) · (𝐴↑2)) + ((3↑2) · 𝐴)) + 3) = 0)
Theorem	3cubeslem3l 40515	Lemma for 3cubes 40519. (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 40516	Lemma for 3cubes 40519. (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 40517	Lemma for 3cubes 40519. (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 40518	Lemma for 3cubes 40519. 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 40519*	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)))
20.28  Mathbox for OpenAI
Theorem	rntrclfvOAI 40520	The range of the transitive closure is equal to the range of the relation. (Contributed by OpenAI, 7-Jul-2020.)
⊢ (𝑅 ∈ 𝑉 → ran (t+‘𝑅) = ran 𝑅)
20.29  Mathbox for Stefan O'Rear
20.29.1  Additional elementary logic and set theory
Theorem	moxfr 40521*	Transfer at-most-one between related expressions. (Contributed by Stefan O'Rear, 12-Feb-2015.)
⊢ 𝐴 ∈ V    &   ⊢ ∃!𝑦 𝑥 = 𝐴    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓)
20.29.2  Additional theory of functions
Theorem	imaiinfv 40522*	Indexed intersection of an image. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → ∩ 𝑥 ∈ 𝐵 (𝐹‘𝑥) = ∩ (𝐹 “ 𝐵))
20.29.3  Additional topology
Theorem	elrfi 40523*	Elementhood in a set of relative finite intersections. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ 𝐶)) ↔ ∃𝑣 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑣)))
Theorem	elrfirn 40524*	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 40525*	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 40526*	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)) → (𝑋 ∩ ∩ 𝑘 ∈ 𝑙 𝑆) ≠ ∅)    ⇒   ⊢ (𝜑 → (𝑋 ∩ ∩ 𝑘 ∈ 𝐼 𝑆) ≠ ∅)
20.29.4  Characterization of closure operators. Kuratowski closure axioms
Theorem	ismrcd1 40527*	Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 17335), isotone (satisfies mrcss 17334), and idempotent (satisfies mrcidm 17337) 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 40528 is the second. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵))
Theorem	ismrcd2 40528*	Second half of ismrcd1 40527. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → 𝐹 = (mrCls‘dom (𝐹 ∩ I )))
Theorem	istopclsd 40529*	A closure function which satisfies sscls 22216, clsidm 22227, cls0 22240, and clsun 34526 defines a (unique) topology which it is the closure function on. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥))    &   ⊢ (𝜑 → (𝐹‘∅) = ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝐵) → (𝐹‘(𝑥 ∪ 𝑦)) = ((𝐹‘𝑥) ∪ (𝐹‘𝑦)))    &   ⊢ 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐹‘(𝐵 ∖ 𝑧)) = (𝐵 ∖ 𝑧)}    ⇒   ⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ (cls‘𝐽) = 𝐹))
Theorem	ismrc 40530*	A function is a Moore closure operator iff it satisfies mrcssid 17335, mrcss 17334, and mrcidm 17337. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐹 ∈ (mrCls “ (Moore‘𝐵)) ↔ (𝐵 ∈ V ∧ 𝐹:𝒫 𝐵⟶𝒫 𝐵 ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝑥 ⊆ (𝐹‘𝑥) ∧ (𝐹‘𝑦) ⊆ (𝐹‘𝑥) ∧ (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)))))
20.29.5  Algebraic closure systems
Syntax	cnacs 40531	Class of Noetherian closure systems.
class NoeACS
Definition	df-nacs 40532*	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 40533*	Expand definition of Noetherian-type closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ ∀𝑠 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑠 = (𝐹‘𝑔)))
Theorem	nacsfg 40534*	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 40535	Express Noetherian-type closure system with fewer quantifiers. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ (𝐹 “ (𝒫 𝑋 ∩ Fin)) = 𝐶))
Theorem	mrefg2 40536*	Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑆 = (𝐹‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑆 ∩ Fin)𝑆 = (𝐹‘𝑔)))
Theorem	mrefg3 40537*	Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ∈ 𝐶) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑆 = (𝐹‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑆 ∩ Fin)𝑆 ⊆ (𝐹‘𝑔)))
Theorem	nacsacs 40538	A closure system of Noetherian type is algebraic. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ (𝐶 ∈ (NoeACS‘𝑋) → 𝐶 ∈ (ACS‘𝑋))
Theorem	isnacs3 40539*	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 40540*	Transitivity induction of subsets, lemma for nacsfix 40541. (Contributed by Stefan O'Rear, 4-Apr-2015.)
⊢ ((∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵))
Theorem	nacsfix 40541*	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 ∀𝑧 ∈ (ℤ≥‘𝑦)(𝐹‘𝑧) = (𝐹‘𝑦))
20.29.6  Miscellanea 1. Map utilities
Theorem	constmap 40542	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 40543	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 40544	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 40545	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 40546	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 40547	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 40548	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...𝑁)) ∧ 𝐶 ∈ 𝐵) → ((𝐴 ∪ {⟨𝑀, 𝐶⟩})‘𝑀) = 𝐶)
20.29.7  Miscellanea for polynomials
Theorem	mptfcl 40549*	Interpret range of a maps-to notation as a constraint on the definition. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ ((𝑡 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶 → (𝑡 ∈ 𝐴 → 𝐵 ∈ 𝐶))
20.29.8  Multivariate polynomials over the integers
Syntax	cmzpcl 40550	Extend class notation to include pre-polynomial rings.
class mzPolyCld
Syntax	cmzp 40551	Extend class notation to include polynomial rings.
class mzPoly
Definition	df-mzpcl 40552*	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 40553. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ mzPolyCld = (𝑣 ∈ V ↦ {𝑝 ∈ 𝒫 (ℤ ↑m (ℤ ↑m 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))})
Definition	df-mzp 40553	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 40554*	Substitution lemma for mzPolyCld. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (𝑉 ∈ V → (mzPolyCld‘𝑉) = {𝑝 ∈ 𝒫 (ℤ ↑m (ℤ ↑m 𝑉)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑉) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))})
Theorem	elmzpcl 40555*	Double substitution lemma for mzPolyCld. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (𝑉 ∈ V → (𝑃 ∈ (mzPolyCld‘𝑉) ↔ (𝑃 ⊆ (ℤ ↑m (ℤ ↑m 𝑉)) ∧ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑉) × {𝑖}) ∈ 𝑃 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑃) ∧ ∀𝑓 ∈ 𝑃 ∀𝑔 ∈ 𝑃 ((𝑓 ∘f + 𝑔) ∈ 𝑃 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑃)))))
Theorem	mzpclall 40556	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 40553 is well-defined. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (𝑉 ∈ V → (ℤ ↑m (ℤ ↑m 𝑉)) ∈ (mzPolyCld‘𝑉))
Theorem	mzpcln0 40557	Corollary of mzpclall 40556: polynomially closed function sets are not empty. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (𝑉 ∈ V → (mzPolyCld‘𝑉) ≠ ∅)
Theorem	mzpcl1 40558	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 40559*	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 40560	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 40561	Value of the mzPoly function. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (𝑉 ∈ V → (mzPoly‘𝑉) = ∩ (mzPolyCld‘𝑉))
Theorem	dmmzp 40562	mzPoly is defined for all index sets which are sets. This is used with elfvdm 6815 to eliminate sethood antecedents. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ dom mzPoly = V
Theorem	mzpincl 40563	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 40564	Constant functions are polynomial. See also mzpconstmpt 40569. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝑉 ∈ V ∧ 𝐶 ∈ ℤ) → ((ℤ ↑m 𝑉) × {𝐶}) ∈ (mzPoly‘𝑉))
Theorem	mzpf 40565	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 40566*	A projection function is polynomial. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝑉 ∈ V ∧ 𝑋 ∈ 𝑉) → (𝑔 ∈ (ℤ ↑m 𝑉) ↦ (𝑔‘𝑋)) ∈ (mzPoly‘𝑉))
Theorem	mzpadd 40567	The pointwise sum of two polynomial functions is a polynomial function. See also mzpaddmpt 40570. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝐴 ∈ (mzPoly‘𝑉) ∧ 𝐵 ∈ (mzPoly‘𝑉)) → (𝐴 ∘f + 𝐵) ∈ (mzPoly‘𝑉))
Theorem	mzpmul 40568	The pointwise product of two polynomial functions is a polynomial function. See also mzpmulmpt 40571. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝐴 ∈ (mzPoly‘𝑉) ∧ 𝐵 ∈ (mzPoly‘𝑉)) → (𝐴 ∘f · 𝐵) ∈ (mzPoly‘𝑉))
Theorem	mzpconstmpt 40569*	A constant function expressed in maps-to notation is polynomial. This theorem and the several that follow (mzpaddmpt 40570, mzpmulmpt 40571, mzpnegmpt 40573, mzpsubmpt 40572, mzpexpmpt 40574) 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 40566 is already expressed using maps-to notation. (Contributed by Stefan O'Rear, 5-Oct-2014.)
⊢ ((𝑉 ∈ V ∧ 𝐶 ∈ ℤ) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐶) ∈ (mzPoly‘𝑉))
Theorem	mzpaddmpt 40570*	Sum of polynomial functions is polynomial. Maps-to version of mzpadd 40567. (Contributed by Stefan O'Rear, 5-Oct-2014.)
⊢ (((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴 + 𝐵)) ∈ (mzPoly‘𝑉))
Theorem	mzpmulmpt 40571*	Product of polynomial functions is polynomial. Maps-to version of mzpmulmpt 40571. (Contributed by Stefan O'Rear, 5-Oct-2014.)
⊢ (((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴 · 𝐵)) ∈ (mzPoly‘𝑉))
Theorem	mzpsubmpt 40572*	The difference of two polynomial functions is polynomial. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴 − 𝐵)) ∈ (mzPoly‘𝑉))
Theorem	mzpnegmpt 40573*	Negation of a polynomial function. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ ((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ -𝐴) ∈ (mzPoly‘𝑉))
Theorem	mzpexpmpt 40574*	Raise a polynomial function to a (fixed) exponent. (Contributed by Stefan O'Rear, 5-Oct-2014.)
⊢ (((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ 𝐷 ∈ ℕ0) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝐷)) ∈ (mzPoly‘𝑉))
Theorem	mzpindd 40575*	"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 40576	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)
Theorem	mzpsubst 40577*	Substituting polynomials for the variables of a polynomial results in a polynomial. 𝐺 is expected to depend on 𝑦 and provide the polynomials which are being substituted. (Contributed by Stefan O'Rear, 5-Oct-2014.)
⊢ ((𝑊 ∈ V ∧ 𝐹 ∈ (mzPoly‘𝑉) ∧ ∀𝑦 ∈ 𝑉 𝐺 ∈ (mzPoly‘𝑊)) → (𝑥 ∈ (ℤ ↑m 𝑊) ↦ (𝐹‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊))
Theorem	mzprename 40578*	Simplified version of mzpsubst 40577 to simply relabel variables in a polynomial. (Contributed by Stefan O'Rear, 5-Oct-2014.)
⊢ ((𝑊 ∈ V ∧ 𝐹 ∈ (mzPoly‘𝑉) ∧ 𝑅:𝑉⟶𝑊) → (𝑥 ∈ (ℤ ↑m 𝑊) ↦ (𝐹‘(𝑥 ∘ 𝑅))) ∈ (mzPoly‘𝑊))
Theorem	mzpresrename 40579*	A polynomial is a polynomial over all larger index sets. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Revised by Stefan O'Rear, 5-Jun-2015.)
⊢ ((𝑊 ∈ V ∧ 𝑉 ⊆ 𝑊 ∧ 𝐹 ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑m 𝑊) ↦ (𝐹‘(𝑥 ↾ 𝑉))) ∈ (mzPoly‘𝑊))
Theorem	mzpcompact2lem 40580*	Lemma for mzpcompact2 40581. (Contributed by Stefan O'Rear, 9-Oct-2014.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑐 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))))
Theorem	mzpcompact2 40581*	Polynomials are finitary objects and can only reference a finite number of variables, even if the index set is infinite. Thus, every polynomial can be expressed as a (uniquely minimal, although we do not prove that) polynomial on a finite number of variables, which is then extended by adding an arbitrary set of ignored variables. (Contributed by Stefan O'Rear, 9-Oct-2014.)
⊢ (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑐 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))))
20.29.9  Miscellanea for Diophantine sets 1
Theorem	coeq0i 40582	coeq0 6163 but without explicitly introducing domain and range symbols. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ ((𝐴:𝐶⟶𝐷 ∧ 𝐵:𝐸⟶𝐹 ∧ (𝐶 ∩ 𝐹) = ∅) → (𝐴 ∘ 𝐵) = ∅)
Theorem	fzsplit1nn0 40583	Split a finite 1-based set of integers in the middle, allowing either end to be empty ((1...0)). (Contributed by Stefan O'Rear, 8-Oct-2014.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵) → (1...𝐵) = ((1...𝐴) ∪ ((𝐴 + 1)...𝐵)))
20.29.10  Diophantine sets 1: definitions
Syntax	cdioph 40584	Extend class notation to include the family of Diophantine sets.
class Dioph
Definition	df-dioph 40585*	A Diophantine set is a set of positive integers which is a projection of the zero set of some polynomial. This definition somewhat awkwardly mixes ℤ (via mzPoly) and ℕ0 (to define the zero sets); the former could be avoided by considering coincidence sets of ℕ0 polynomials at the cost of requiring two, and the second is driven by consistency with our mu-recursive functions and the requirements of the Davis-Putnam-Robinson-Matiyasevich proof. Both are avoidable at a complexity cost. In particular, it is a consequence of 4sq 16674 that implicitly restricting variables to ℕ0 adds no expressive power over allowing them to range over ℤ. While this definition stipulates a specific index set for the polynomials, there is actually flexibility here, see eldioph2b 40592. (Contributed by Stefan O'Rear, 5-Oct-2014.)
⊢ Dioph = (𝑛 ∈ ℕ0 ↦ ran (𝑘 ∈ (ℤ≥‘𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)}))
Theorem	eldiophb 40586*	Initial expression of Diophantine property of a set. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ (𝐷 ∈ (Dioph‘𝑁) ↔ (𝑁 ∈ ℕ0 ∧ ∃𝑘 ∈ (ℤ≥‘𝑁)∃𝑝 ∈ (mzPoly‘(1...𝑘))𝐷 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}))
Theorem	eldioph 40587*	Condition for a set to be Diophantine (unpacking existential quantifier). (Contributed by Stefan O'Rear, 5-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ (ℤ≥‘𝑁) ∧ 𝑃 ∈ (mzPoly‘(1...𝐾))) → {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑m (1...𝐾))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑃‘𝑢) = 0)} ∈ (Dioph‘𝑁))
Theorem	diophrw 40588*	Renaming and adding unused witness variables does not change the Diophantine set coded by a polynomial. (Contributed by Stefan O'Rear, 7-Oct-2014.)
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → {𝑎 ∣ ∃𝑏 ∈ (ℕ0 ↑m 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)} = {𝑎 ∣ ∃𝑐 ∈ (ℕ0 ↑m 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)})
Theorem	eldioph2lem1 40589*	Lemma for eldioph2 40591. Construct necessary renaming function for one direction. (Contributed by Stefan O'Rear, 8-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → ∃𝑑 ∈ (ℤ≥‘𝑁)∃𝑒 ∈ V (𝑒:(1...𝑑)–1-1-onto→𝐴 ∧ (𝑒 ↾ (1...𝑁)) = ( I ↾ (1...𝑁))))
Theorem	eldioph2lem2 40590*	Lemma for eldioph2 40591. Construct necessary renaming function for one direction. (Contributed by Stefan O'Rear, 8-Oct-2014.)
⊢ (((𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin) ∧ ((1...𝑁) ⊆ 𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) → ∃𝑐(𝑐:(1...𝐴)–1-1→𝑆 ∧ (𝑐 ↾ (1...𝑁)) = ( I ↾ (1...𝑁))))
Theorem	eldioph2 40591*	Construct a Diophantine set from a polynomial with witness variables drawn from any set whatsoever, via mzpcompact2 40581. (Contributed by Stefan O'Rear, 8-Oct-2014.) (Revised by Stefan O'Rear, 5-Jun-2015.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ V ∧ (1...𝑁) ⊆ 𝑆) ∧ 𝑃 ∈ (mzPoly‘𝑆)) → {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑m 𝑆)(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑃‘𝑢) = 0)} ∈ (Dioph‘𝑁))
Theorem	eldioph2b 40592*	While Diophantine sets were defined to have a finite number of witness variables consequtively following the observable variables, this is not necessary; they can equivalently be taken to use any witness set (𝑆 ∖ (1...𝑁)). For instance, in diophin 40601 we use this to take the two input sets to have disjoint witness sets. (Contributed by Stefan O'Rear, 8-Oct-2014.)
⊢ (((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V) ∧ (¬ 𝑆 ∈ Fin ∧ (1...𝑁) ⊆ 𝑆)) → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑝 ∈ (mzPoly‘𝑆)𝐴 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑m 𝑆)(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}))
Theorem	eldiophelnn0 40593	Remove antecedent on 𝐵 from Diophantine set constructors. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (𝐴 ∈ (Dioph‘𝐵) → 𝐵 ∈ ℕ0)
Theorem	eldioph3b 40594*	Define Diophantine sets in terms of polynomials with variables indexed by ℕ. This avoids a quantifier over the number of witness variables and will be easier to use than eldiophb 40586 in most cases. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (𝐴 ∈ (Dioph‘𝑁) ↔ (𝑁 ∈ ℕ0 ∧ ∃𝑝 ∈ (mzPoly‘ℕ)𝐴 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑m ℕ)(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}))
Theorem	eldioph3 40595*	Inference version of eldioph3b 40594 with quantifier expanded. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑃 ∈ (mzPoly‘ℕ)) → {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑m ℕ)(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑃‘𝑢) = 0)} ∈ (Dioph‘𝑁))
20.29.11  Diophantine sets 2 miscellanea
Theorem	ellz1 40596	Membership in a lower set of integers. (Contributed by Stefan O'Rear, 9-Oct-2014.)
⊢ (𝐵 ∈ ℤ → (𝐴 ∈ (ℤ ∖ (ℤ≥‘(𝐵 + 1))) ↔ (𝐴 ∈ ℤ ∧ 𝐴 ≤ 𝐵)))
Theorem	lzunuz 40597	The union of a lower set of integers and an upper set of integers which abut or overlap is all of the integers. (Contributed by Stefan O'Rear, 9-Oct-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≤ (𝐴 + 1)) → ((ℤ ∖ (ℤ≥‘(𝐴 + 1))) ∪ (ℤ≥‘𝐵)) = ℤ)
Theorem	fz1eqin 40598	Express a one-based finite range as the intersection of lower integers with ℕ. (Contributed by Stefan O'Rear, 9-Oct-2014.)
⊢ (𝑁 ∈ ℕ0 → (1...𝑁) = ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ))
Theorem	lzenom 40599	Lower integers are countably infinite. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (𝑁 ∈ ℤ → (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ≈ ω)
Theorem	elmapresaunres2 40600	fresaunres2 6655 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014.)
⊢ ((𝐹 ∈ (𝐶 ↑m 𝐴) ∧ 𝐺 ∈ (𝐶 ↑m 𝐵) ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ∪ 𝐺) ↾ 𝐵) = 𝐺)