P. 438 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43701-43800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mzpcompact2 43701*	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 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎)))))
21.35.9  Miscellanea for Diophantine sets 1
Theorem	coeq0i 43702	coeq0 6246 but without explicitly introducing domain and range symbols. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ ((𝐴:𝐶⟶𝐷 ∧ 𝐵:𝐸⟶𝐹 ∧ (𝐶 ∩ 𝐹) = ∅) → (𝐴 ∘ 𝐵) = ∅)
Theorem	fzsplit1nn0 43703	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)...𝐵)))
21.35.10  Diophantine sets 1: definitions
Syntax	cdioph 43704	Extend class notation to include the family of Diophantine sets.
class Dioph
Definition	df-dioph 43705*	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 17104 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 43712. (Contributed by Stefan O'Rear, 5-Oct-2014.)
⊢ Dioph = (𝑛 ∈ ℕ0 ↦ ran (𝑘 ∈ (ℤ≥‘𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)}))
Theorem	eldiophb 43706*	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 43707*	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 43708*	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 43709*	Lemma for eldioph2 43711. 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 43710*	Lemma for eldioph2 43711. 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 43711*	Construct a Diophantine set from a polynomial with witness variables drawn from any set whatsoever, via mzpcompact2 43701. (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 43712*	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 43721 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 43713	Remove antecedent on 𝐵 from Diophantine set constructors. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (𝐴 ∈ (Dioph‘𝐵) → 𝐵 ∈ ℕ0)
Theorem	eldioph3b 43714*	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 43706 in most cases. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (𝐴 ∈ (Dioph‘𝑁) ↔ (𝑁 ∈ ℕ0 ∧ ∃𝑝 ∈ (mzPoly‘ℕ)𝐴 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑m ℕ)(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}))
Theorem	eldioph3 43715*	Inference version of eldioph3b 43714 with quantifier expanded. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑃 ∈ (mzPoly‘ℕ)) → {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑m ℕ)(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑃‘𝑢) = 0)} ∈ (Dioph‘𝑁))
21.35.11  Diophantine sets 2 miscellanea
Theorem	ellz1 43716	Membership in a lower set of integers. (Contributed by Stefan O'Rear, 9-Oct-2014.)
⊢ (𝐵 ∈ ℤ → (𝐴 ∈ (ℤ ∖ (ℤ≥‘(𝐵 + 1))) ↔ (𝐴 ∈ ℤ ∧ 𝐴 ≤ 𝐵)))
Theorem	lzunuz 43717	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 43718	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 43719	Lower integers are countably infinite. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (𝑁 ∈ ℤ → (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ≈ ω)
Theorem	elmapresaunres2 43720	fresaunres2 6742 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014.)
⊢ ((𝐹 ∈ (𝐶 ↑m 𝐴) ∧ 𝐺 ∈ (𝐶 ↑m 𝐵) ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ∪ 𝐺) ↾ 𝐵) = 𝐺)
21.35.12  Diophantine sets 2: union and intersection. Monotone Boolean algebra
Theorem	diophin 43721	If two sets are Diophantine, so is their intersection. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁))
Theorem	diophun 43722	If two sets are Diophantine, so is their union. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∪ 𝐵) ∈ (Dioph‘𝑁))
Theorem	eldiophss 43723	Diophantine sets are sets of tuples of nonnegative integers. (Contributed by Stefan O'Rear, 10-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ (𝐴 ∈ (Dioph‘𝐵) → 𝐴 ⊆ (ℕ0 ↑m (1...𝐵)))
21.35.13  Diophantine sets 3: construction
Theorem	diophrex 43724*	Projecting a Diophantine set by removing a coordinate results in a Diophantine set. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) → {𝑡 ∣ ∃𝑢 ∈ 𝑆 𝑡 = (𝑢 ↾ (1...𝑁))} ∈ (Dioph‘𝑁))
Theorem	eq0rabdioph 43725*	This is the first of a number of theorems which allow sets to be proven Diophantine by syntactic induction, and models the correspondence between Diophantine sets and monotone existential first-order logic. This first theorem shows that the zero set of an implicit polynomial is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑m (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝐴 = 0} ∈ (Dioph‘𝑁))
Theorem	eqrabdioph 43726*	Diophantine set builder for equality of polynomial expressions. Note that the two expressions need not be nonnegative; only variables are so constrained. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑m (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑m (1...𝑁)) ↦ 𝐵) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝐴 = 𝐵} ∈ (Dioph‘𝑁))
Theorem	0dioph 43727	The empty set is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (𝐴 ∈ ℕ0 → ∅ ∈ (Dioph‘𝐴))
Theorem	vdioph 43728	The "universal" set (as large as possible given eldiophss 43723) is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (𝐴 ∈ ℕ0 → (ℕ0 ↑m (1...𝐴)) ∈ (Dioph‘𝐴))
Theorem	anrabdioph 43729*	Diophantine set builder for conjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (({𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝜑} ∈ (Dioph‘𝑁) ∧ {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝜓} ∈ (Dioph‘𝑁)) → {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ (𝜑 ∧ 𝜓)} ∈ (Dioph‘𝑁))
Theorem	orrabdioph 43730*	Diophantine set builder for disjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (({𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝜑} ∈ (Dioph‘𝑁) ∧ {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝜓} ∈ (Dioph‘𝑁)) → {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ (𝜑 ∨ 𝜓)} ∈ (Dioph‘𝑁))
Theorem	3anrabdioph 43731*	Diophantine set builder for ternary conjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (({𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝜑} ∈ (Dioph‘𝑁) ∧ {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝜓} ∈ (Dioph‘𝑁) ∧ {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝜒} ∈ (Dioph‘𝑁)) → {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ (𝜑 ∧ 𝜓 ∧ 𝜒)} ∈ (Dioph‘𝑁))
Theorem	3orrabdioph 43732*	Diophantine set builder for ternary disjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (({𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝜑} ∈ (Dioph‘𝑁) ∧ {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝜓} ∈ (Dioph‘𝑁) ∧ {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝜒} ∈ (Dioph‘𝑁)) → {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ (𝜑 ∨ 𝜓 ∨ 𝜒)} ∈ (Dioph‘𝑁))
21.35.14  Diophantine sets 4 miscellanea
Theorem	2sbcrex 43733*	Exchange an existential quantifier with two substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by NM, 24-Aug-2018.)
⊢ ([𝐴 / 𝑎][𝐵 / 𝑏]∃𝑐 ∈ 𝐶 𝜑 ↔ ∃𝑐 ∈ 𝐶 [𝐴 / 𝑎][𝐵 / 𝑏]𝜑)
Theorem	sbc2rex 43734*	Exchange a substitution with two existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by NM, 24-Aug-2018.)
⊢ ([𝐴 / 𝑎]∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝜑 ↔ ∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 [𝐴 / 𝑎]𝜑)
Theorem	sbc4rex 43735*	Exchange a substitution with four existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by NM, 24-Aug-2018.)
⊢ ([𝐴 / 𝑎]∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 ∃𝑒 ∈ 𝐸 𝜑 ↔ ∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 ∃𝑒 ∈ 𝐸 [𝐴 / 𝑎]𝜑)
Theorem	sbcrot3 43736*	Rotate a sequence of three explicit substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ ([𝐴 / 𝑎][𝐵 / 𝑏][𝐶 / 𝑐]𝜑 ↔ [𝐵 / 𝑏][𝐶 / 𝑐][𝐴 / 𝑎]𝜑)
Theorem	sbcrot5 43737*	Rotate a sequence of five explicit substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ ([𝐴 / 𝑎][𝐵 / 𝑏][𝐶 / 𝑐][𝐷 / 𝑑][𝐸 / 𝑒]𝜑 ↔ [𝐵 / 𝑏][𝐶 / 𝑐][𝐷 / 𝑑][𝐸 / 𝑒][𝐴 / 𝑎]𝜑)
Theorem	sbccomieg 43738*	Commute two explicit substitutions, using an implicit substitution to rewrite the exiting substitution. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ (𝑎 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ([𝐴 / 𝑎][𝐵 / 𝑏]𝜑 ↔ [𝐶 / 𝑏][𝐴 / 𝑎]𝜑)
21.35.15  Diophantine sets 4: Quantification
Theorem	rexrabdioph 43739*	Diophantine set builder for existential quantification. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ 𝑀 = (𝑁 + 1)    &   ⊢ (𝑣 = (𝑡‘𝑀) → (𝜓 ↔ 𝜒))    &   ⊢ (𝑢 = (𝑡 ↾ (1...𝑁)) → (𝜒 ↔ 𝜑))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ {𝑡 ∈ (ℕ0 ↑m (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → {𝑢 ∈ (ℕ0 ↑m (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 𝜓} ∈ (Dioph‘𝑁))
Theorem	rexfrabdioph 43740*	Diophantine set builder for existential quantifier, explicit substitution. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ 𝑀 = (𝑁 + 1)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ {𝑡 ∈ (ℕ0 ↑m (1...𝑀)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣]𝜑} ∈ (Dioph‘𝑀)) → {𝑢 ∈ (ℕ0 ↑m (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 𝜑} ∈ (Dioph‘𝑁))
Theorem	2rexfrabdioph 43741*	Diophantine set builder for existential quantifier, explicit substitution, two variables. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ 𝑀 = (𝑁 + 1)    &   ⊢ 𝐿 = (𝑀 + 1)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ {𝑡 ∈ (ℕ0 ↑m (1...𝐿)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑} ∈ (Dioph‘𝐿)) → {𝑢 ∈ (ℕ0 ↑m (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 ∃𝑤 ∈ ℕ0 𝜑} ∈ (Dioph‘𝑁))
Theorem	3rexfrabdioph 43742*	Diophantine set builder for existential quantifier, explicit substitution, two variables. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ 𝑀 = (𝑁 + 1)    &   ⊢ 𝐿 = (𝑀 + 1)    &   ⊢ 𝐾 = (𝐿 + 1)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ {𝑡 ∈ (ℕ0 ↑m (1...𝐾)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤][(𝑡‘𝐾) / 𝑥]𝜑} ∈ (Dioph‘𝐾)) → {𝑢 ∈ (ℕ0 ↑m (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 ∃𝑤 ∈ ℕ0 ∃𝑥 ∈ ℕ0 𝜑} ∈ (Dioph‘𝑁))
Theorem	4rexfrabdioph 43743*	Diophantine set builder for existential quantifier, explicit substitution, four variables. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ 𝑀 = (𝑁 + 1)    &   ⊢ 𝐿 = (𝑀 + 1)    &   ⊢ 𝐾 = (𝐿 + 1)    &   ⊢ 𝐽 = (𝐾 + 1)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ {𝑡 ∈ (ℕ0 ↑m (1...𝐽)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤][(𝑡‘𝐾) / 𝑥][(𝑡‘𝐽) / 𝑦]𝜑} ∈ (Dioph‘𝐽)) → {𝑢 ∈ (ℕ0 ↑m (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 ∃𝑤 ∈ ℕ0 ∃𝑥 ∈ ℕ0 ∃𝑦 ∈ ℕ0 𝜑} ∈ (Dioph‘𝑁))
Theorem	6rexfrabdioph 43744*	Diophantine set builder for existential quantifier, explicit substitution, six variables. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ 𝑀 = (𝑁 + 1)    &   ⊢ 𝐿 = (𝑀 + 1)    &   ⊢ 𝐾 = (𝐿 + 1)    &   ⊢ 𝐽 = (𝐾 + 1)    &   ⊢ 𝐼 = (𝐽 + 1)    &   ⊢ 𝐻 = (𝐼 + 1)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ {𝑡 ∈ (ℕ0 ↑m (1...𝐻)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤][(𝑡‘𝐾) / 𝑥][(𝑡‘𝐽) / 𝑦][(𝑡‘𝐼) / 𝑧][(𝑡‘𝐻) / 𝑝]𝜑} ∈ (Dioph‘𝐻)) → {𝑢 ∈ (ℕ0 ↑m (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 ∃𝑤 ∈ ℕ0 ∃𝑥 ∈ ℕ0 ∃𝑦 ∈ ℕ0 ∃𝑧 ∈ ℕ0 ∃𝑝 ∈ ℕ0 𝜑} ∈ (Dioph‘𝑁))
Theorem	7rexfrabdioph 43745*	Diophantine set builder for existential quantifier, explicit substitution, seven variables. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ 𝑀 = (𝑁 + 1)    &   ⊢ 𝐿 = (𝑀 + 1)    &   ⊢ 𝐾 = (𝐿 + 1)    &   ⊢ 𝐽 = (𝐾 + 1)    &   ⊢ 𝐼 = (𝐽 + 1)    &   ⊢ 𝐻 = (𝐼 + 1)    &   ⊢ 𝐺 = (𝐻 + 1)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ {𝑡 ∈ (ℕ0 ↑m (1...𝐺)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤][(𝑡‘𝐾) / 𝑥][(𝑡‘𝐽) / 𝑦][(𝑡‘𝐼) / 𝑧][(𝑡‘𝐻) / 𝑝][(𝑡‘𝐺) / 𝑞]𝜑} ∈ (Dioph‘𝐺)) → {𝑢 ∈ (ℕ0 ↑m (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 ∃𝑤 ∈ ℕ0 ∃𝑥 ∈ ℕ0 ∃𝑦 ∈ ℕ0 ∃𝑧 ∈ ℕ0 ∃𝑝 ∈ ℕ0 ∃𝑞 ∈ ℕ0 𝜑} ∈ (Dioph‘𝑁))
21.35.16  Diophantine sets 5: Arithmetic sets
Theorem	rabdiophlem1 43746*	Lemma for arithmetic diophantine sets. Convert polynomial-ness of an expression into a constraint suitable for ralimi 3099. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ ((𝑡 ∈ (ℤ ↑m (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) → ∀𝑡 ∈ (ℕ0 ↑m (1...𝑁))𝐴 ∈ ℤ)
Theorem	rabdiophlem2 43747*	Lemma for arithmetic diophantine sets. Reuse a polynomial expression under a new quantifier. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ 𝑀 = (𝑁 + 1)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑢 ∈ (ℤ ↑m (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑡 ∈ (ℤ ↑m (1...𝑀)) ↦ ⦋(𝑡 ↾ (1...𝑁)) / 𝑢⦌𝐴) ∈ (mzPoly‘(1...𝑀)))
Theorem	elnn0rabdioph 43748*	Diophantine set builder for nonnegativity constraints. The first builder which uses a witness variable internally; an expression is nonnegative if there is a nonnegative integer equal to it. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑m (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝐴 ∈ ℕ0} ∈ (Dioph‘𝑁))
Theorem	rexzrexnn0 43749*	Rewrite an existential quantification restricted to integers into an existential quantification restricted to naturals. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = -𝑦 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (∃𝑥 ∈ ℤ 𝜑 ↔ ∃𝑦 ∈ ℕ0 (𝜓 ∨ 𝜒))
Theorem	lerabdioph 43750*	Diophantine set builder for the "less than or equal to" relation. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑m (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑m (1...𝑁)) ↦ 𝐵) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝐴 ≤ 𝐵} ∈ (Dioph‘𝑁))
Theorem	eluzrabdioph 43751*	Diophantine set builder for membership in a fixed upper set of integers. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ (𝑡 ∈ (ℤ ↑m (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝐴 ∈ (ℤ≥‘𝑀)} ∈ (Dioph‘𝑁))
Theorem	elnnrabdioph 43752*	Diophantine set builder for positivity. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑m (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝐴 ∈ ℕ} ∈ (Dioph‘𝑁))
Theorem	ltrabdioph 43753*	Diophantine set builder for the strict less than relation. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑m (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑m (1...𝑁)) ↦ 𝐵) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝐴 < 𝐵} ∈ (Dioph‘𝑁))
Theorem	nerabdioph 43754*	Diophantine set builder for inequality. This not quite trivial theorem touches on something important; Diophantine sets are not closed under negation, but they contain an important subclass that is, namely the recursive sets. With this theorem and De Morgan's laws, all quantifier-free formulas can be negated. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑m (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑m (1...𝑁)) ↦ 𝐵) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝐴 ≠ 𝐵} ∈ (Dioph‘𝑁))
Theorem	dvdsrabdioph 43755*	Divisibility is a Diophantine relation. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑m (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑m (1...𝑁)) ↦ 𝐵) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝐴 ∥ 𝐵} ∈ (Dioph‘𝑁))
21.35.17  Diophantine sets 6: reusability. renumbering of variables
Theorem	eldioph4b 43756*	Membership in Dioph expressed using a quantified union to add witness variables instead of a restriction to remove them. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ 𝑊 ∈ V    &   ⊢ ¬ 𝑊 ∈ Fin    &   ⊢ (𝑊 ∩ ℕ) = ∅    ⇒   ⊢ (𝑆 ∈ (Dioph‘𝑁) ↔ (𝑁 ∈ ℕ0 ∧ ∃𝑝 ∈ (mzPoly‘(𝑊 ∪ (1...𝑁)))𝑆 = {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ ∃𝑤 ∈ (ℕ0 ↑m 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0}))
Theorem	eldioph4i 43757*	Forward-only version of eldioph4b 43756. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ 𝑊 ∈ V    &   ⊢ ¬ 𝑊 ∈ Fin    &   ⊢ (𝑊 ∩ ℕ) = ∅    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑃 ∈ (mzPoly‘(𝑊 ∪ (1...𝑁)))) → {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ ∃𝑤 ∈ (ℕ0 ↑m 𝑊)(𝑃‘(𝑡 ∪ 𝑤)) = 0} ∈ (Dioph‘𝑁))
Theorem	diophren 43758*	Change variables in a Diophantine set, using class notation. This allows already proved Diophantine sets to be reused in contexts with more variables. (Contributed by Stefan O'Rear, 16-Oct-2014.) (Revised by Stefan O'Rear, 5-Jun-2015.)
⊢ ((𝑆 ∈ (Dioph‘𝑁) ∧ 𝑀 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶(1...𝑀)) → {𝑎 ∈ (ℕ0 ↑m (1...𝑀)) ∣ (𝑎 ∘ 𝐹) ∈ 𝑆} ∈ (Dioph‘𝑀))
Theorem	rabrenfdioph 43759*	Change variable numbers in a Diophantine class abstraction using explicit substitution. (Contributed by Stefan O'Rear, 17-Oct-2014.)
⊢ ((𝐵 ∈ ℕ0 ∧ 𝐹:(1...𝐴)⟶(1...𝐵) ∧ {𝑎 ∈ (ℕ0 ↑m (1...𝐴)) ∣ 𝜑} ∈ (Dioph‘𝐴)) → {𝑏 ∈ (ℕ0 ↑m (1...𝐵)) ∣ [(𝑏 ∘ 𝐹) / 𝑎]𝜑} ∈ (Dioph‘𝐵))
Theorem	rabren3dioph 43760*	Change variable numbers in a 3-variable Diophantine class abstraction. (Contributed by Stefan O'Rear, 17-Oct-2014.)
⊢ (((𝑎‘1) = (𝑏‘𝑋) ∧ (𝑎‘2) = (𝑏‘𝑌) ∧ (𝑎‘3) = (𝑏‘𝑍)) → (𝜑 ↔ 𝜓))    &   ⊢ 𝑋 ∈ (1...𝑁)    &   ⊢ 𝑌 ∈ (1...𝑁)    &   ⊢ 𝑍 ∈ (1...𝑁)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ 𝜑} ∈ (Dioph‘3)) → {𝑏 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝜓} ∈ (Dioph‘𝑁))
21.35.18  Pigeonhole Principle and cardinality helpers
Theorem	fphpd 43761*	Pigeonhole principle expressed with implicit substitution. If the range is smaller than the domain, two inputs must be mapped to the same output. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ (𝜑 → 𝐵 ≺ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)    &   ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 ∧ 𝐶 = 𝐷))
Theorem	fphpdo 43762*	Pigeonhole principle for sets of real numbers with implicit output reordering. (Contributed by Stefan O'Rear, 12-Sep-2014.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐵 ≺ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐶 ∈ 𝐵)    &   ⊢ (𝑧 = 𝑥 → 𝐶 = 𝐷)    &   ⊢ (𝑧 = 𝑦 → 𝐶 = 𝐸)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ 𝐷 = 𝐸))
Theorem	ctbnfien 43763	An infinite subset of a countable set is countable, without using choice. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ (((𝑋 ≈ ω ∧ 𝑌 ≈ ω) ∧ (𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin)) → 𝐴 ≈ 𝑌)
Theorem	fiphp3d 43764*	Infinite pigeonhole principle for partitioning an infinite set between finitely many buckets. (Contributed by Stefan O'Rear, 18-Oct-2014.)
⊢ (𝜑 → 𝐴 ≈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ 𝐵 {𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦} ≈ ℕ)
21.35.19  A non-closed set of reals is infinite
Theorem	rencldnfilem 43765*	Lemma for rencldnfi 43766. (Contributed by Stefan O'Rear, 18-Oct-2014.)
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥) → ¬ 𝐴 ∈ Fin)
Theorem	rencldnfi 43766*	A set of real numbers which comes arbitrarily close to some target yet excludes it is infinite. The work is done in rencldnfilem 43765 using infima; this theorem removes the requirement that A be nonempty. (Contributed by Stefan O'Rear, 19-Oct-2014.)
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ 𝐵 ∈ 𝐴) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥) → ¬ 𝐴 ∈ Fin)
21.35.20  Lagrange's rational approximation theorem
Theorem	irrapxlem1 43767*	Lemma for irrapx1 43773. Divides the unit interval into 𝐵 half-open sections and using the pigeonhole principle fphpdo 43762 finds two multiples of 𝐴 in the same section mod 1. (Contributed by Stefan O'Rear, 12-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ (0...𝐵)∃𝑦 ∈ (0...𝐵)(𝑥 < 𝑦 ∧ (⌊‘(𝐵 · ((𝐴 · 𝑥) mod 1))) = (⌊‘(𝐵 · ((𝐴 · 𝑦) mod 1)))))
Theorem	irrapxlem2 43768*	Lemma for irrapx1 43773. Two multiples in the same bucket means they are very close mod 1. (Contributed by Stefan O'Rear, 12-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ (0...𝐵)∃𝑦 ∈ (0...𝐵)(𝑥 < 𝑦 ∧ (abs‘(((𝐴 · 𝑥) mod 1) − ((𝐴 · 𝑦) mod 1))) < (1 / 𝐵)))
Theorem	irrapxlem3 43769*	Lemma for irrapx1 43773. By subtraction, there is a multiple very close to an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ (1...𝐵)∃𝑦 ∈ ℕ0 (abs‘((𝐴 · 𝑥) − 𝑦)) < (1 / 𝐵))
Theorem	irrapxlem4 43770*	Lemma for irrapx1 43773. Eliminate ranges, use positivity of the input to force positivity of the output by increasing 𝐵 as needed. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ (abs‘((𝐴 · 𝑥) − 𝑦)) < (1 / if(𝑥 ≤ 𝐵, 𝐵, 𝑥)))
Theorem	irrapxlem5 43771*	Lemma for irrapx1 43773. Switching to real intervals and fraction syntax. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ ℚ (0 < 𝑥 ∧ (abs‘(𝑥 − 𝐴)) < 𝐵 ∧ (abs‘(𝑥 − 𝐴)) < ((denom‘𝑥)↑-2)))
Theorem	irrapxlem6 43772*	Lemma for irrapx1 43773. Explicit description of a non-closed set. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ {𝑦 ∈ ℚ ∣ (0 < 𝑦 ∧ (abs‘(𝑦 − 𝐴)) < ((denom‘𝑦)↑-2))} (abs‘(𝑥 − 𝐴)) < 𝐵)
Theorem	irrapx1 43773*	Dirichlet's approximation theorem. Every positive irrational number has infinitely many rational approximations which are closer than the inverse squares of their reduced denominators. Lemma 61 in [vandenDries] p. 42. (Contributed by Stefan O'Rear, 14-Sep-2014.)
⊢ (𝐴 ∈ (ℝ+ ∖ ℚ) → {𝑦 ∈ ℚ ∣ (0 < 𝑦 ∧ (abs‘(𝑦 − 𝐴)) < ((denom‘𝑦)↑-2))} ≈ ℕ)
21.35.21  Pell equations 1: A nontrivial solution always exists
Theorem	pellexlem1 43774	Lemma for pellex 43780. Arithmetical core of pellexlem3, norm lower bound. This begins Dirichlet's proof of the Pell equation solution existence; the proof here follows theorem 62 of [vandenDries] p. 43. (Contributed by Stefan O'Rear, 14-Sep-2014.)
⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ ¬ (√‘𝐷) ∈ ℚ) → ((𝐴↑2) − (𝐷 · (𝐵↑2))) ≠ 0)
Theorem	pellexlem2 43775	Lemma for pellex 43780. Arithmetical core of pellexlem3, norm upper bound. (Contributed by Stefan O'Rear, 14-Sep-2014.)
⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) < (1 + (2 · (√‘𝐷))))
Theorem	pellexlem3 43776*	Lemma for pellex 43780. To each good rational approximation of (√‘𝐷), there exists a near-solution. (Contributed by Stefan O'Rear, 14-Sep-2014.)
⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → {𝑥 ∈ ℚ ∣ (0 < 𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))} ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))})
Theorem	pellexlem4 43777*	Lemma for pellex 43780. Invoking irrapx1 43773, we have infinitely many near-solutions. (Contributed by Stefan O'Rear, 14-Sep-2014.)
⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ≈ ℕ)
Theorem	pellexlem5 43778*	Lemma for pellex 43780. Invoking fiphp3d 43764, we have infinitely many near-solutions for some specific norm. (Contributed by Stefan O'Rear, 19-Oct-2014.)
⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ∃𝑥 ∈ ℤ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ))
Theorem	pellexlem6 43779*	Lemma for pellex 43780. Doing a field division between near solutions get us to norm 1, and the modularity constraint ensures we still have an integer. Returning NN guarantees that we are not returning the trivial solution (1,0). We are not explicitly defining the Pell-field, Pell-ring, and Pell-norm explicitly because after this construction is done we will never use them. This is mostly basic algebraic number theory and could be simplified if a generic framework for that were in place. (Contributed by Stefan O'Rear, 19-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ)    &   ⊢ (𝜑 → ¬ (√‘𝐷) ∈ ℚ)    &   ⊢ (𝜑 → 𝐸 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹 ∈ ℕ)    &   ⊢ (𝜑 → ¬ (𝐴 = 𝐸 ∧ 𝐵 = 𝐹))    &   ⊢ (𝜑 → 𝐶 ≠ 0)    &   ⊢ (𝜑 → ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 𝐶)    &   ⊢ (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶)    &   ⊢ (𝜑 → (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶)))    &   ⊢ (𝜑 → (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶)))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
Theorem	pellex 43780*	Every Pell equation has a nontrivial solution. Theorem 62 in [vandenDries] p. 43. (Contributed by Stefan O'Rear, 19-Oct-2014.)
⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ ((𝑥↑2) − (𝐷 · (𝑦↑2))) = 1)
21.35.22  Pell equations 2: Algebraic number theory of the solution set
Syntax	csquarenn 43781	Extend class notation to include the set of square positive integers.
class ◻NN
Syntax	cpell1qr 43782	Extend class notation to include the class of quadrant-1 Pell solutions.
class Pell1QR
Syntax	cpell1234qr 43783	Extend class notation to include the class of any-quadrant Pell solutions.
class Pell1234QR
Syntax	cpell14qr 43784	Extend class notation to include the class of positive Pell solutions.
class Pell14QR
Syntax	cpellfund 43785	Extend class notation to include the Pell-equation fundamental solution function.
class PellFund
Definition	df-squarenn 43786	Define the set of square positive integers. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ◻NN = {𝑥 ∈ ℕ ∣ (√‘𝑥) ∈ ℚ}
Definition	df-pell1qr 43787*	Define the solutions of a Pell equation in the first quadrant. To avoid pair pain, we represent this via the canonical embedding into the reals. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ Pell1QR = (𝑥 ∈ (ℕ ∖ ◻NN) ↦ {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℕ0 (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)})
Definition	df-pell14qr 43788*	Define the positive solutions of a Pell equation. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ Pell14QR = (𝑥 ∈ (ℕ ∖ ◻NN) ↦ {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)})
Definition	df-pell1234qr 43789*	Define the general solutions of a Pell equation. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ Pell1234QR = (𝑥 ∈ (ℕ ∖ ◻NN) ↦ {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)})
Definition	df-pellfund 43790*	A function mapping Pell discriminants to the corresponding fundamental solution. (Contributed by Stefan O'Rear, 18-Sep-2014.) (Revised by AV, 17-Sep-2020.)
⊢ PellFund = (𝑥 ∈ (ℕ ∖ ◻NN) ↦ inf({𝑧 ∈ (Pell14QR‘𝑥) ∣ 1 < 𝑧}, ℝ, < ))
Theorem	pell1qrval 43791*	Value of the set of first-quadrant Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell1QR‘𝐷) = {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℕ0 (𝑦 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)})
Theorem	elpell1qr 43792*	Membership in a first-quadrant Pell solution set. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell1QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℕ0 (𝐴 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1))))
Theorem	pell14qrval 43793*	Value of the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell14QR‘𝐷) = {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)})
Theorem	elpell14qr 43794*	Membership in the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℤ (𝐴 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1))))
Theorem	pell1234qrval 43795*	Value of the set of general Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell1234QR‘𝐷) = {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)})
Theorem	elpell1234qr 43796*	Membership in the set of general Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell1234QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ (𝐴 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1))))
Theorem	pell1234qrre 43797	General Pell solutions are (coded as) real numbers. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → 𝐴 ∈ ℝ)
Theorem	pell1234qrne0 43798	No solution to a Pell equation is zero. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → 𝐴 ≠ 0)
Theorem	pell1234qrreccl 43799	General solutions of the Pell equation are closed under reciprocals. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → (1 / 𝐴) ∈ (Pell1234QR‘𝐷))
Theorem	pell1234qrmulcl 43800	General solutions of the Pell equation are closed under multiplication. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷) ∧ 𝐵 ∈ (Pell1234QR‘𝐷)) → (𝐴 · 𝐵) ∈ (Pell1234QR‘𝐷))