Home | Metamath
Proof Explorer Theorem List (p. 364 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mptfcl 36301* | Interpret range of a maps-to notation as a constraint on the definition. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ ((𝑡 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶 → (𝑡 ∈ 𝐴 → 𝐵 ∈ 𝐶)) | ||
Syntax | cmzpcl 36302 | Extend class notation to include pre-polynomial rings. |
class mzPolyCld | ||
Syntax | cmzp 36303 | Extend class notation to include polynomial rings. |
class mzPoly | ||
Definition | df-mzpcl 36304* | Define the polynomially closed function rings over an arbitrary index set 𝑣. The set (mzPolyCld‘𝑣) contains all sets of functions from (ℤ ↑𝑚 𝑣) 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 36305. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ mzPolyCld = (𝑣 ∈ V ↦ {𝑝 ∈ 𝒫 (ℤ ↑𝑚 (ℤ ↑𝑚 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑝))}) | ||
Definition | df-mzp 36305 | 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 36306* | Substitution lemma for mzPolyCld. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ (𝑉 ∈ V → (mzPolyCld‘𝑉) = {𝑝 ∈ 𝒫 (ℤ ↑𝑚 (ℤ ↑𝑚 𝑉)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑉) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑𝑚 𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑝))}) | ||
Theorem | elmzpcl 36307* | Double substitution lemma for mzPolyCld. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ (𝑉 ∈ V → (𝑃 ∈ (mzPolyCld‘𝑉) ↔ (𝑃 ⊆ (ℤ ↑𝑚 (ℤ ↑𝑚 𝑉)) ∧ ((∀𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑉) × {𝑖}) ∈ 𝑃 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑𝑚 𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑃) ∧ ∀𝑓 ∈ 𝑃 ∀𝑔 ∈ 𝑃 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑃 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑃))))) | ||
Theorem | mzpclall 36308 | 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 36305 is well-defined. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ (𝑉 ∈ V → (ℤ ↑𝑚 (ℤ ↑𝑚 𝑉)) ∈ (mzPolyCld‘𝑉)) | ||
Theorem | mzpcln0 36309 | Corrolary of mzpclall 36308: polynomially closed function sets are not empty. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ (𝑉 ∈ V → (mzPolyCld‘𝑉) ≠ ∅) | ||
Theorem | mzpcl1 36310 | Defining property 1 of a polynomially closed function set 𝑃: it contains all constant functions. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝑃 ∈ (mzPolyCld‘𝑉) ∧ 𝐹 ∈ ℤ) → ((ℤ ↑𝑚 𝑉) × {𝐹}) ∈ 𝑃) | ||
Theorem | mzpcl2 36311* | Defining property 2 of a polynomially closed function set 𝑃: it contains all projections. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝑃 ∈ (mzPolyCld‘𝑉) ∧ 𝐹 ∈ 𝑉) → (𝑔 ∈ (ℤ ↑𝑚 𝑉) ↦ (𝑔‘𝐹)) ∈ 𝑃) | ||
Theorem | mzpcl34 36312 | 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‘𝑉) ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃) → ((𝐹 ∘𝑓 + 𝐺) ∈ 𝑃 ∧ (𝐹 ∘𝑓 · 𝐺) ∈ 𝑃)) | ||
Theorem | mzpval 36313 | Value of the mzPoly function. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ (𝑉 ∈ V → (mzPoly‘𝑉) = ∩ (mzPolyCld‘𝑉)) | ||
Theorem | dmmzp 36314 | mzPoly is defined for all index sets which are sets. This is used with elfvdm 6130 to eliminate sethood antecedents. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ dom mzPoly = V | ||
Theorem | mzpincl 36315 | 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 36316 | Constant functions are polynomial. See also mzpconstmpt 36321. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝑉 ∈ V ∧ 𝐶 ∈ ℤ) → ((ℤ ↑𝑚 𝑉) × {𝐶}) ∈ (mzPoly‘𝑉)) | ||
Theorem | mzpf 36317 | A polynomial function is a function from the coordinate space to the integers. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
⊢ (𝐹 ∈ (mzPoly‘𝑉) → 𝐹:(ℤ ↑𝑚 𝑉)⟶ℤ) | ||
Theorem | mzpproj 36318* | A projection function is polynomial. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝑉 ∈ V ∧ 𝑋 ∈ 𝑉) → (𝑔 ∈ (ℤ ↑𝑚 𝑉) ↦ (𝑔‘𝑋)) ∈ (mzPoly‘𝑉)) | ||
Theorem | mzpadd 36319 | The pointwise sum of two polynomial functions is a polynomial function. See also mzpaddmpt 36322. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ (mzPoly‘𝑉) ∧ 𝐵 ∈ (mzPoly‘𝑉)) → (𝐴 ∘𝑓 + 𝐵) ∈ (mzPoly‘𝑉)) | ||
Theorem | mzpmul 36320 | The pointwise product of two polynomial functions is a polynomial function. See also mzpmulmpt 36323. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ (mzPoly‘𝑉) ∧ 𝐵 ∈ (mzPoly‘𝑉)) → (𝐴 ∘𝑓 · 𝐵) ∈ (mzPoly‘𝑉)) | ||
Theorem | mzpconstmpt 36321* | A constant function expressed in maps-to notation is polynomial. This theorem and the several that follow (mzpaddmpt 36322, mzpmulmpt 36323, mzpnegmpt 36325, mzpsubmpt 36324, mzpexpmpt 36326) 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 36318 is already expressed using maps-to notation. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
⊢ ((𝑉 ∈ V ∧ 𝐶 ∈ ℤ) → (𝑥 ∈ (ℤ ↑𝑚 𝑉) ↦ 𝐶) ∈ (mzPoly‘𝑉)) | ||
Theorem | mzpaddmpt 36322* | Sum of polynomial functions is polynomial. Maps-to version of mzpadd 36319. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
⊢ (((𝑥 ∈ (ℤ ↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑𝑚 𝑉) ↦ (𝐴 + 𝐵)) ∈ (mzPoly‘𝑉)) | ||
Theorem | mzpmulmpt 36323* | Product of polynomial functions is polynomial. Maps-to version of mzpmulmpt 36323. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
⊢ (((𝑥 ∈ (ℤ ↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑𝑚 𝑉) ↦ (𝐴 · 𝐵)) ∈ (mzPoly‘𝑉)) | ||
Theorem | mzpsubmpt 36324* | The difference of two polynomial functions is polynomial. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ (((𝑥 ∈ (ℤ ↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑𝑚 𝑉) ↦ (𝐴 − 𝐵)) ∈ (mzPoly‘𝑉)) | ||
Theorem | mzpnegmpt 36325* | Negation of a polynomial function. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ ((𝑥 ∈ (ℤ ↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚 𝑉) ↦ -𝐴) ∈ (mzPoly‘𝑉)) | ||
Theorem | mzpexpmpt 36326* | Raise a polynomial function to a (fixed) exponent. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
⊢ (((𝑥 ∈ (ℤ ↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ 𝐷 ∈ ℕ0) → (𝑥 ∈ (ℤ ↑𝑚 𝑉) ↦ (𝐴↑𝐷)) ∈ (mzPoly‘𝑉)) | ||
Theorem | mzpindd 36327* | "Structural" induction to prove properties of all polynomial functions. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝜑 ∧ 𝑓 ∈ ℤ) → 𝜒) & ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑉) → 𝜃) & ⊢ ((𝜑 ∧ (𝑓:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜏) ∧ (𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜂)) → 𝜁) & ⊢ ((𝜑 ∧ (𝑓:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜏) ∧ (𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜂)) → 𝜎) & ⊢ (𝑥 = ((ℤ ↑𝑚 𝑉) × {𝑓}) → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = (𝑔 ∈ (ℤ ↑𝑚 𝑉) ↦ (𝑔‘𝑓)) → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = 𝑓 → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝑔 → (𝜓 ↔ 𝜂)) & ⊢ (𝑥 = (𝑓 ∘𝑓 + 𝑔) → (𝜓 ↔ 𝜁)) & ⊢ (𝑥 = (𝑓 ∘𝑓 · 𝑔) → (𝜓 ↔ 𝜎)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜌)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ (mzPoly‘𝑉)) → 𝜌) | ||
Theorem | mzpmfp 36328 | 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 36329* | 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‘𝑊)) → (𝑥 ∈ (ℤ ↑𝑚 𝑊) ↦ (𝐹‘(𝑦 ∈ 𝑉 ↦ (𝐺‘𝑥)))) ∈ (mzPoly‘𝑊)) | ||
Theorem | mzprename 36330* | Simplified version of mzpsubst 36329 to simply relabel variables in a polynomial. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
⊢ ((𝑊 ∈ V ∧ 𝐹 ∈ (mzPoly‘𝑉) ∧ 𝑅:𝑉⟶𝑊) → (𝑥 ∈ (ℤ ↑𝑚 𝑊) ↦ (𝐹‘(𝑥 ∘ 𝑅))) ∈ (mzPoly‘𝑊)) | ||
Theorem | mzpresrename 36331* | 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‘𝑉)) → (𝑥 ∈ (ℤ ↑𝑚 𝑊) ↦ (𝐹‘(𝑥 ↾ 𝑉))) ∈ (mzPoly‘𝑊)) | ||
Theorem | mzpcompact2lem 36332* | Lemma for mzpcompact2 36333. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑐 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎))))) | ||
Theorem | mzpcompact2 36333* | 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‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑐 ∈ (ℤ ↑𝑚 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎))))) | ||
Theorem | coeq0i 36334 | coeq0 5561 but without explicitly introducing domain and range symbols. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ ((𝐴:𝐶⟶𝐷 ∧ 𝐵:𝐸⟶𝐹 ∧ (𝐶 ∩ 𝐹) = ∅) → (𝐴 ∘ 𝐵) = ∅) | ||
Theorem | fzsplit1nn0 36335 | 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)...𝐵))) | ||
Syntax | cdioph 36336 | Extend class notation to include the family of Diophantine sets. |
class Dioph | ||
Definition | df-dioph 36337* | 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 15506 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 36344. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
⊢ Dioph = (𝑛 ∈ ℕ0 ↦ ran (𝑘 ∈ (ℤ≥‘𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)})) | ||
Theorem | eldiophb 36338* | 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 ↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) | ||
Theorem | eldioph 36339* | Condition for a set to be Diophantine (unpacking existential quantifier). (Contributed by Stefan O'Rear, 5-Oct-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ (ℤ≥‘𝑁) ∧ 𝑃 ∈ (mzPoly‘(1...𝐾))) → {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑𝑚 (1...𝐾))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑃‘𝑢) = 0)} ∈ (Dioph‘𝑁)) | ||
Theorem | diophrw 36340* | 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 ↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)} = {𝑎 ∣ ∃𝑐 ∈ (ℕ0 ↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)}) | ||
Theorem | eldioph2lem1 36341* | Lemma for eldioph2 36343. 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 36342* | Lemma for eldioph2 36343. 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 36343* | Construct a Diophantine set from a polynomial with witness variables drawn from any set whatsoever, via mzpcompact2 36333. (Contributed by Stefan O'Rear, 8-Oct-2014.) (Revised by Stefan O'Rear, 5-Jun-2015.) |
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ V ∧ (1...𝑁) ⊆ 𝑆) ∧ 𝑃 ∈ (mzPoly‘𝑆)) → {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑𝑚 𝑆)(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑃‘𝑢) = 0)} ∈ (Dioph‘𝑁)) | ||
Theorem | eldioph2b 36344* | 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 36354 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 ↑𝑚 𝑆)(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) | ||
Theorem | eldiophelnn0 36345 | Remove antecedent on 𝐵 from Diophantine set constructors. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ (𝐴 ∈ (Dioph‘𝐵) → 𝐵 ∈ ℕ0) | ||
Theorem | eldioph3b 36346* | 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 36338 in most cases. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ (𝐴 ∈ (Dioph‘𝑁) ↔ (𝑁 ∈ ℕ0 ∧ ∃𝑝 ∈ (mzPoly‘ℕ)𝐴 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑𝑚 ℕ)(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) | ||
Theorem | eldioph3 36347* | Inference version of eldioph3b 36346 with quantifier expanded. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑃 ∈ (mzPoly‘ℕ)) → {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑𝑚 ℕ)(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑃‘𝑢) = 0)} ∈ (Dioph‘𝑁)) | ||
Theorem | ellz1 36348 | Membership in a lower set of integers. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
⊢ (𝐵 ∈ ℤ → (𝐴 ∈ (ℤ ∖ (ℤ≥‘(𝐵 + 1))) ↔ (𝐴 ∈ ℤ ∧ 𝐴 ≤ 𝐵))) | ||
Theorem | lzunuz 36349 | 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 36350 | 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 36351 | Lower integers are countably infinite. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ (𝑁 ∈ ℤ → (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ≈ ω) | ||
Theorem | elmapresaun 36352 | fresaun 5988 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
⊢ ((𝐹 ∈ (𝐶 ↑𝑚 𝐴) ∧ 𝐺 ∈ (𝐶 ↑𝑚 𝐵) ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ∪ 𝐺) ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵))) | ||
Theorem | elmapresaunres2 36353 | fresaunres2 5989 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
⊢ ((𝐹 ∈ (𝐶 ↑𝑚 𝐴) ∧ 𝐺 ∈ (𝐶 ↑𝑚 𝐵) ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ∪ 𝐺) ↾ 𝐵) = 𝐺) | ||
Theorem | diophin 36354 | 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 36355 | 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 36356 | 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 ↑𝑚 (1...𝐵))) | ||
Theorem | diophrex 36357* | 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 36358* | 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 ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 = 0} ∈ (Dioph‘𝑁)) | ||
Theorem | eqrabdioph 36359* | 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 ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐵) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 = 𝐵} ∈ (Dioph‘𝑁)) | ||
Theorem | 0dioph 36360 | The null set is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ (𝐴 ∈ ℕ0 → ∅ ∈ (Dioph‘𝐴)) | ||
Theorem | vdioph 36361 | The "universal" set (as large as possible given eldiophss 36356) is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ (𝐴 ∈ ℕ0 → (ℕ0 ↑𝑚 (1...𝐴)) ∈ (Dioph‘𝐴)) | ||
Theorem | anrabdioph 36362* | Diophantine set builder for conjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ (({𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝜑} ∈ (Dioph‘𝑁) ∧ {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝜓} ∈ (Dioph‘𝑁)) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ (𝜑 ∧ 𝜓)} ∈ (Dioph‘𝑁)) | ||
Theorem | orrabdioph 36363* | Diophantine set builder for disjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ (({𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝜑} ∈ (Dioph‘𝑁) ∧ {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝜓} ∈ (Dioph‘𝑁)) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ (𝜑 ∨ 𝜓)} ∈ (Dioph‘𝑁)) | ||
Theorem | 3anrabdioph 36364* | Diophantine set builder for ternary conjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ (({𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝜑} ∈ (Dioph‘𝑁) ∧ {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝜓} ∈ (Dioph‘𝑁) ∧ {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝜒} ∈ (Dioph‘𝑁)) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ (𝜑 ∧ 𝜓 ∧ 𝜒)} ∈ (Dioph‘𝑁)) | ||
Theorem | 3orrabdioph 36365* | Diophantine set builder for ternary disjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ (({𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝜑} ∈ (Dioph‘𝑁) ∧ {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝜓} ∈ (Dioph‘𝑁) ∧ {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝜒} ∈ (Dioph‘𝑁)) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ (𝜑 ∨ 𝜓 ∨ 𝜒)} ∈ (Dioph‘𝑁)) | ||
Theorem | 2sbcrex 36366* | Exchange an existential quantifier with two substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by NM, 24-Aug-2018.) |
⊢ ([𝐴 / 𝑎][𝐵 / 𝑏]∃𝑐 ∈ 𝐶 𝜑 ↔ ∃𝑐 ∈ 𝐶 [𝐴 / 𝑎][𝐵 / 𝑏]𝜑) | ||
Theorem | sbcrexgOLD 36367* | Interchange class substitution and restricted existential quantifier. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) Obsolete as of 18-Aug-2018. Use sbcrex 3481 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) | ||
Theorem | 2sbcrexOLD 36368* | Exchange an existential quantifier with two substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 6585 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ([𝐴 / 𝑎][𝐵 / 𝑏]∃𝑐 ∈ 𝐶 𝜑 ↔ ∃𝑐 ∈ 𝐶 [𝐴 / 𝑎][𝐵 / 𝑏]𝜑) | ||
Theorem | sbc2rex 36369* | Exchange a substitution with two existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by NM, 24-Aug-2018.) |
⊢ ([𝐴 / 𝑎]∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝜑 ↔ ∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 [𝐴 / 𝑎]𝜑) | ||
Theorem | sbc2rexgOLD 36370* | Exchange a substitution with two existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 6585 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑎]∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝜑 ↔ ∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 [𝐴 / 𝑎]𝜑)) | ||
Theorem | sbc4rex 36371* | Exchange a substitution with four existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by NM, 24-Aug-2018.) |
⊢ ([𝐴 / 𝑎]∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 ∃𝑒 ∈ 𝐸 𝜑 ↔ ∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 ∃𝑒 ∈ 𝐸 [𝐴 / 𝑎]𝜑) | ||
Theorem | sbc4rexgOLD 36372* | Exchange a substitution with four existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 6585 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑎]∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 ∃𝑒 ∈ 𝐸 𝜑 ↔ ∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 ∃𝑒 ∈ 𝐸 [𝐴 / 𝑎]𝜑)) | ||
Theorem | sbcrot3 36373* | Rotate a sequence of three explicit substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ ([𝐴 / 𝑎][𝐵 / 𝑏][𝐶 / 𝑐]𝜑 ↔ [𝐵 / 𝑏][𝐶 / 𝑐][𝐴 / 𝑎]𝜑) | ||
Theorem | sbcrot5 36374* | Rotate a sequence of five explicit substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ ([𝐴 / 𝑎][𝐵 / 𝑏][𝐶 / 𝑐][𝐷 / 𝑑][𝐸 / 𝑒]𝜑 ↔ [𝐵 / 𝑏][𝐶 / 𝑐][𝐷 / 𝑑][𝐸 / 𝑒][𝐴 / 𝑎]𝜑) | ||
Theorem | sbccomieg 36375* | 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.) |
⊢ (𝑎 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ([𝐴 / 𝑎][𝐵 / 𝑏]𝜑 ↔ [𝐶 / 𝑏][𝐴 / 𝑎]𝜑) | ||
Theorem | rexrabdioph 36376* | Diophantine set builder for existential quantification. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ 𝑀 = (𝑁 + 1) & ⊢ (𝑣 = (𝑡‘𝑀) → (𝜓 ↔ 𝜒)) & ⊢ (𝑢 = (𝑡 ↾ (1...𝑁)) → (𝜒 ↔ 𝜑)) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → {𝑢 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 𝜓} ∈ (Dioph‘𝑁)) | ||
Theorem | rexfrabdioph 36377* | 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 ↑𝑚 (1...𝑀)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣]𝜑} ∈ (Dioph‘𝑀)) → {𝑢 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 𝜑} ∈ (Dioph‘𝑁)) | ||
Theorem | 2rexfrabdioph 36378* | 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 ↑𝑚 (1...𝐿)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑} ∈ (Dioph‘𝐿)) → {𝑢 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 ∃𝑤 ∈ ℕ0 𝜑} ∈ (Dioph‘𝑁)) | ||
Theorem | 3rexfrabdioph 36379* | 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 ↑𝑚 (1...𝐾)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤][(𝑡‘𝐾) / 𝑥]𝜑} ∈ (Dioph‘𝐾)) → {𝑢 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 ∃𝑤 ∈ ℕ0 ∃𝑥 ∈ ℕ0 𝜑} ∈ (Dioph‘𝑁)) | ||
Theorem | 4rexfrabdioph 36380* | 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 ↑𝑚 (1...𝐽)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤][(𝑡‘𝐾) / 𝑥][(𝑡‘𝐽) / 𝑦]𝜑} ∈ (Dioph‘𝐽)) → {𝑢 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 ∃𝑤 ∈ ℕ0 ∃𝑥 ∈ ℕ0 ∃𝑦 ∈ ℕ0 𝜑} ∈ (Dioph‘𝑁)) | ||
Theorem | 6rexfrabdioph 36381* | 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 ↑𝑚 (1...𝐻)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤][(𝑡‘𝐾) / 𝑥][(𝑡‘𝐽) / 𝑦][(𝑡‘𝐼) / 𝑧][(𝑡‘𝐻) / 𝑝]𝜑} ∈ (Dioph‘𝐻)) → {𝑢 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 ∃𝑤 ∈ ℕ0 ∃𝑥 ∈ ℕ0 ∃𝑦 ∈ ℕ0 ∃𝑧 ∈ ℕ0 ∃𝑝 ∈ ℕ0 𝜑} ∈ (Dioph‘𝑁)) | ||
Theorem | 7rexfrabdioph 36382* | 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 ↑𝑚 (1...𝐺)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤][(𝑡‘𝐾) / 𝑥][(𝑡‘𝐽) / 𝑦][(𝑡‘𝐼) / 𝑧][(𝑡‘𝐻) / 𝑝][(𝑡‘𝐺) / 𝑞]𝜑} ∈ (Dioph‘𝐺)) → {𝑢 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 ∃𝑤 ∈ ℕ0 ∃𝑥 ∈ ℕ0 ∃𝑦 ∈ ℕ0 ∃𝑧 ∈ ℕ0 ∃𝑝 ∈ ℕ0 ∃𝑞 ∈ ℕ0 𝜑} ∈ (Dioph‘𝑁)) | ||
Theorem | rabdiophlem1 36383* | Lemma for arithmetic diophantine sets. Convert polynomial-ness of an expression into a constraint suitable for ralimi 2936. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ ((𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) → ∀𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁))𝐴 ∈ ℤ) | ||
Theorem | rabdiophlem2 36384* | Lemma for arithmetic diophantine sets. Reuse a polynomial expression under a new quantifier. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ 𝑀 = (𝑁 + 1) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑡 ∈ (ℤ ↑𝑚 (1...𝑀)) ↦ ⦋(𝑡 ↾ (1...𝑁)) / 𝑢⦌𝐴) ∈ (mzPoly‘(1...𝑀))) | ||
Theorem | elnn0rabdioph 36385* | 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 ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 ∈ ℕ0} ∈ (Dioph‘𝑁)) | ||
Theorem | rexzrexnn0 36386* | Rewrite a quantification over integers into a quantification over naturals. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = -𝑦 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (∃𝑥 ∈ ℤ 𝜑 ↔ ∃𝑦 ∈ ℕ0 (𝜓 ∨ 𝜒)) | ||
Theorem | lerabdioph 36387* | Diophantine set builder for the less or equals relation. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐵) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 ≤ 𝐵} ∈ (Dioph‘𝑁)) | ||
Theorem | eluzrabdioph 36388* | Diophantine set builder for membership in a fixed upper set of integers. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 ∈ (ℤ≥‘𝑀)} ∈ (Dioph‘𝑁)) | ||
Theorem | elnnrabdioph 36389* | Diophantine set builder for positivity. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 ∈ ℕ} ∈ (Dioph‘𝑁)) | ||
Theorem | ltrabdioph 36390* | Diophantine set builder for the strict less than relation. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐵) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 < 𝐵} ∈ (Dioph‘𝑁)) | ||
Theorem | nerabdioph 36391* | 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 formulae can be negated. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐵) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 ≠ 𝐵} ∈ (Dioph‘𝑁)) | ||
Theorem | dvdsrabdioph 36392* | Divisibility is a Diophantine relation. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐵) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 ∥ 𝐵} ∈ (Dioph‘𝑁)) | ||
Theorem | eldioph4b 36393* | 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 ↑𝑚 (1...𝑁)) ∣ ∃𝑤 ∈ (ℕ0 ↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0})) | ||
Theorem | eldioph4i 36394* | Forward-only version of eldioph4b 36393. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ 𝑊 ∈ V & ⊢ ¬ 𝑊 ∈ Fin & ⊢ (𝑊 ∩ ℕ) = ∅ ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑃 ∈ (mzPoly‘(𝑊 ∪ (1...𝑁)))) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ ∃𝑤 ∈ (ℕ0 ↑𝑚 𝑊)(𝑃‘(𝑡 ∪ 𝑤)) = 0} ∈ (Dioph‘𝑁)) | ||
Theorem | diophren 36395* | 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 ↑𝑚 (1...𝑀)) ∣ (𝑎 ∘ 𝐹) ∈ 𝑆} ∈ (Dioph‘𝑀)) | ||
Theorem | rabrenfdioph 36396* | Change variable numbers in a Diophantine class abstraction using explicit substitution. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
⊢ ((𝐵 ∈ ℕ0 ∧ 𝐹:(1...𝐴)⟶(1...𝐵) ∧ {𝑎 ∈ (ℕ0 ↑𝑚 (1...𝐴)) ∣ 𝜑} ∈ (Dioph‘𝐴)) → {𝑏 ∈ (ℕ0 ↑𝑚 (1...𝐵)) ∣ [(𝑏 ∘ 𝐹) / 𝑎]𝜑} ∈ (Dioph‘𝐵)) | ||
Theorem | rabren3dioph 36397* | 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 ↑𝑚 (1...3)) ∣ 𝜑} ∈ (Dioph‘3)) → {𝑏 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝜓} ∈ (Dioph‘𝑁)) | ||
Theorem | fphpd 36398* | 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 36399* | Pigeonhole principle for sets of real numbers with implicit output reordering. (Contributed by Stefan O'Rear, 12-Sep-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐵 ≺ 𝐴) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐶 ∈ 𝐵) & ⊢ (𝑧 = 𝑥 → 𝐶 = 𝐷) & ⊢ (𝑧 = 𝑦 → 𝐶 = 𝐸) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ 𝐷 = 𝐸)) | ||
Theorem | ctbnfien 36400 | 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)) → 𝐴 ≈ 𝑌) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |