| Metamath
Proof Explorer Theorem List (p. 428 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | 3cubes 42701* | 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))) | ||
| Theorem | rntrclfvOAI 42702 | The range of the transitive closure is equal to the range of the relation. (Contributed by OpenAI, 7-Jul-2020.) |
| ⊢ (𝑅 ∈ 𝑉 → ran (t+‘𝑅) = ran 𝑅) | ||
| Theorem | moxfr 42703* | Transfer at-most-one between related expressions. (Contributed by Stefan O'Rear, 12-Feb-2015.) |
| ⊢ 𝐴 ∈ V & ⊢ ∃!𝑦 𝑥 = 𝐴 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓) | ||
| Theorem | imaiinfv 42704* | Indexed intersection of an image. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → ∩ 𝑥 ∈ 𝐵 (𝐹‘𝑥) = ∩ (𝐹 “ 𝐵)) | ||
| Theorem | elrfi 42705* | Elementhood in a set of relative finite intersections. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
| ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ 𝐶)) ↔ ∃𝑣 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = (𝐵 ∩ ∩ 𝑣))) | ||
| Theorem | elrfirn 42706* | 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 42707* | 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 42708* | 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)) → (𝑋 ∩ ∩ 𝑘 ∈ 𝑙 𝑆) ≠ ∅) ⇒ ⊢ (𝜑 → (𝑋 ∩ ∩ 𝑘 ∈ 𝐼 𝑆) ≠ ∅) | ||
| Theorem | ismrcd1 42709* | Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 17660), isotone (satisfies mrcss 17659), and idempotent (satisfies mrcidm 17662) 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 42710 is the second. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵)) | ||
| Theorem | ismrcd2 42710* | Second half of ismrcd1 42709. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → 𝐹 = (mrCls‘dom (𝐹 ∩ I ))) | ||
| Theorem | istopclsd 42711* | A closure function which satisfies sscls 23064, clsidm 23075, cls0 23088, and clsun 36329 defines a (unique) topology which it is the closure function on. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)) & ⊢ (𝜑 → (𝐹‘∅) = ∅) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝐵) → (𝐹‘(𝑥 ∪ 𝑦)) = ((𝐹‘𝑥) ∪ (𝐹‘𝑦))) & ⊢ 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐹‘(𝐵 ∖ 𝑧)) = (𝐵 ∖ 𝑧)} ⇒ ⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ (cls‘𝐽) = 𝐹)) | ||
| Theorem | ismrc 42712* | A function is a Moore closure operator iff it satisfies mrcssid 17660, mrcss 17659, and mrcidm 17662. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ (𝐹 ∈ (mrCls “ (Moore‘𝐵)) ↔ (𝐵 ∈ V ∧ 𝐹:𝒫 𝐵⟶𝒫 𝐵 ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝑥 ⊆ (𝐹‘𝑥) ∧ (𝐹‘𝑦) ⊆ (𝐹‘𝑥) ∧ (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥))))) | ||
| Syntax | cnacs 42713 | Class of Noetherian closure systems. |
| class NoeACS | ||
| Definition | df-nacs 42714* | 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 42715* | Expand definition of Noetherian-type closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ ∀𝑠 ∈ 𝐶 ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑠 = (𝐹‘𝑔))) | ||
| Theorem | nacsfg 42716* | 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 42717 | Express Noetherian-type closure system with fewer quantifiers. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ (𝐹 “ (𝒫 𝑋 ∩ Fin)) = 𝐶)) | ||
| Theorem | mrefg2 42718* | Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑆 = (𝐹‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑆 ∩ Fin)𝑆 = (𝐹‘𝑔))) | ||
| Theorem | mrefg3 42719* | Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ∈ 𝐶) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑆 = (𝐹‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑆 ∩ Fin)𝑆 ⊆ (𝐹‘𝑔))) | ||
| Theorem | nacsacs 42720 | A closure system of Noetherian type is algebraic. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
| ⊢ (𝐶 ∈ (NoeACS‘𝑋) → 𝐶 ∈ (ACS‘𝑋)) | ||
| Theorem | isnacs3 42721* | 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 42722* | Transitivity induction of subsets, lemma for nacsfix 42723. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
| ⊢ ((∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵)) | ||
| Theorem | nacsfix 42723* | 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 ∀𝑧 ∈ (ℤ≥‘𝑦)(𝐹‘𝑧) = (𝐹‘𝑦)) | ||
| Theorem | constmap 42724 |
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 42725 | 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 42726 | 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 42727 | 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 42728 | 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 42729 | 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 42730 | 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...𝑁)) ∧ 𝐶 ∈ 𝐵) → ((𝐴 ∪ {〈𝑀, 𝐶〉})‘𝑀) = 𝐶) | ||
| Theorem | mptfcl 42731* | Interpret range of a maps-to notation as a constraint on the definition. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
| ⊢ ((𝑡 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶 → (𝑡 ∈ 𝐴 → 𝐵 ∈ 𝐶)) | ||
| Syntax | cmzpcl 42732 | Extend class notation to include pre-polynomial rings. |
| class mzPolyCld | ||
| Syntax | cmzp 42733 | Extend class notation to include polynomial rings. |
| class mzPoly | ||
| Definition | df-mzpcl 42734* | 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 42735. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
| ⊢ mzPolyCld = (𝑣 ∈ V ↦ {𝑝 ∈ 𝒫 (ℤ ↑m (ℤ ↑m 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))}) | ||
| Definition | df-mzp 42735 | 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 42736* | Substitution lemma for mzPolyCld. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
| ⊢ (𝑉 ∈ V → (mzPolyCld‘𝑉) = {𝑝 ∈ 𝒫 (ℤ ↑m (ℤ ↑m 𝑉)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑉) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))}) | ||
| Theorem | elmzpcl 42737* | Double substitution lemma for mzPolyCld. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
| ⊢ (𝑉 ∈ V → (𝑃 ∈ (mzPolyCld‘𝑉) ↔ (𝑃 ⊆ (ℤ ↑m (ℤ ↑m 𝑉)) ∧ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑉) × {𝑖}) ∈ 𝑃 ∧ ∀𝑗 ∈ 𝑉 (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝑥‘𝑗)) ∈ 𝑃) ∧ ∀𝑓 ∈ 𝑃 ∀𝑔 ∈ 𝑃 ((𝑓 ∘f + 𝑔) ∈ 𝑃 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑃))))) | ||
| Theorem | mzpclall 42738 | 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 42735 is well-defined. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
| ⊢ (𝑉 ∈ V → (ℤ ↑m (ℤ ↑m 𝑉)) ∈ (mzPolyCld‘𝑉)) | ||
| Theorem | mzpcln0 42739 | Corollary of mzpclall 42738: polynomially closed function sets are not empty. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
| ⊢ (𝑉 ∈ V → (mzPolyCld‘𝑉) ≠ ∅) | ||
| Theorem | mzpcl1 42740 | 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 42741* | 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 42742 | 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 42743 | Value of the mzPoly function. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
| ⊢ (𝑉 ∈ V → (mzPoly‘𝑉) = ∩ (mzPolyCld‘𝑉)) | ||
| Theorem | dmmzp 42744 | mzPoly is defined for all index sets which are sets. This is used with elfvdm 6943 to eliminate sethood antecedents. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
| ⊢ dom mzPoly = V | ||
| Theorem | mzpincl 42745 | 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 42746 | Constant functions are polynomial. See also mzpconstmpt 42751. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
| ⊢ ((𝑉 ∈ V ∧ 𝐶 ∈ ℤ) → ((ℤ ↑m 𝑉) × {𝐶}) ∈ (mzPoly‘𝑉)) | ||
| Theorem | mzpf 42747 | 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 42748* | A projection function is polynomial. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
| ⊢ ((𝑉 ∈ V ∧ 𝑋 ∈ 𝑉) → (𝑔 ∈ (ℤ ↑m 𝑉) ↦ (𝑔‘𝑋)) ∈ (mzPoly‘𝑉)) | ||
| Theorem | mzpadd 42749 | The pointwise sum of two polynomial functions is a polynomial function. See also mzpaddmpt 42752. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
| ⊢ ((𝐴 ∈ (mzPoly‘𝑉) ∧ 𝐵 ∈ (mzPoly‘𝑉)) → (𝐴 ∘f + 𝐵) ∈ (mzPoly‘𝑉)) | ||
| Theorem | mzpmul 42750 | The pointwise product of two polynomial functions is a polynomial function. See also mzpmulmpt 42753. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
| ⊢ ((𝐴 ∈ (mzPoly‘𝑉) ∧ 𝐵 ∈ (mzPoly‘𝑉)) → (𝐴 ∘f · 𝐵) ∈ (mzPoly‘𝑉)) | ||
| Theorem | mzpconstmpt 42751* | A constant function expressed in maps-to notation is polynomial. This theorem and the several that follow (mzpaddmpt 42752, mzpmulmpt 42753, mzpnegmpt 42755, mzpsubmpt 42754, mzpexpmpt 42756) 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 42748 is already expressed using maps-to notation. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
| ⊢ ((𝑉 ∈ V ∧ 𝐶 ∈ ℤ) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐶) ∈ (mzPoly‘𝑉)) | ||
| Theorem | mzpaddmpt 42752* | Sum of polynomial functions is polynomial. Maps-to version of mzpadd 42749. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
| ⊢ (((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴 + 𝐵)) ∈ (mzPoly‘𝑉)) | ||
| Theorem | mzpmulmpt 42753* | Product of polynomial functions is polynomial. Maps-to version of mzpmulmpt 42753. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
| ⊢ (((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴 · 𝐵)) ∈ (mzPoly‘𝑉)) | ||
| Theorem | mzpsubmpt 42754* | The difference of two polynomial functions is polynomial. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
| ⊢ (((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐵) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴 − 𝐵)) ∈ (mzPoly‘𝑉)) | ||
| Theorem | mzpnegmpt 42755* | Negation of a polynomial function. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
| ⊢ ((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ -𝐴) ∈ (mzPoly‘𝑉)) | ||
| Theorem | mzpexpmpt 42756* | Raise a polynomial function to a (fixed) exponent. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
| ⊢ (((𝑥 ∈ (ℤ ↑m 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ 𝐷 ∈ ℕ0) → (𝑥 ∈ (ℤ ↑m 𝑉) ↦ (𝐴↑𝐷)) ∈ (mzPoly‘𝑉)) | ||
| Theorem | mzpindd 42757* | "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 42758 | 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 42759* | 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 42760* | Simplified version of mzpsubst 42759 to simply relabel variables in a polynomial. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
| ⊢ ((𝑊 ∈ V ∧ 𝐹 ∈ (mzPoly‘𝑉) ∧ 𝑅:𝑉⟶𝑊) → (𝑥 ∈ (ℤ ↑m 𝑊) ↦ (𝐹‘(𝑥 ∘ 𝑅))) ∈ (mzPoly‘𝑊)) | ||
| Theorem | mzpresrename 42761* | 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 42762* | Lemma for mzpcompact2 42763. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
| ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ (mzPoly‘𝐵) → ∃𝑎 ∈ Fin ∃𝑏 ∈ (mzPoly‘𝑎)(𝑎 ⊆ 𝐵 ∧ 𝐴 = (𝑐 ∈ (ℤ ↑m 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎))))) | ||
| Theorem | mzpcompact2 42763* | 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 𝐵) ↦ (𝑏‘(𝑐 ↾ 𝑎))))) | ||
| Theorem | coeq0i 42764 | coeq0 6275 but without explicitly introducing domain and range symbols. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
| ⊢ ((𝐴:𝐶⟶𝐷 ∧ 𝐵:𝐸⟶𝐹 ∧ (𝐶 ∩ 𝐹) = ∅) → (𝐴 ∘ 𝐵) = ∅) | ||
| Theorem | fzsplit1nn0 42765 | 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 42766 | Extend class notation to include the family of Diophantine sets. |
| class Dioph | ||
| Definition | df-dioph 42767* | 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 17002 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 42774. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
| ⊢ Dioph = (𝑛 ∈ ℕ0 ↦ ran (𝑘 ∈ (ℤ≥‘𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)})) | ||
| Theorem | eldiophb 42768* | 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 42769* | 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 42770* | 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 42771* | Lemma for eldioph2 42773. 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 42772* | Lemma for eldioph2 42773. 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 42773* | Construct a Diophantine set from a polynomial with witness variables drawn from any set whatsoever, via mzpcompact2 42763. (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 42774* | 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 42783 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 42775 | Remove antecedent on 𝐵 from Diophantine set constructors. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
| ⊢ (𝐴 ∈ (Dioph‘𝐵) → 𝐵 ∈ ℕ0) | ||
| Theorem | eldioph3b 42776* | 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 42768 in most cases. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
| ⊢ (𝐴 ∈ (Dioph‘𝑁) ↔ (𝑁 ∈ ℕ0 ∧ ∃𝑝 ∈ (mzPoly‘ℕ)𝐴 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑m ℕ)(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) | ||
| Theorem | eldioph3 42777* | Inference version of eldioph3b 42776 with quantifier expanded. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑃 ∈ (mzPoly‘ℕ)) → {𝑡 ∣ ∃𝑢 ∈ (ℕ0 ↑m ℕ)(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑃‘𝑢) = 0)} ∈ (Dioph‘𝑁)) | ||
| Theorem | ellz1 42778 | Membership in a lower set of integers. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
| ⊢ (𝐵 ∈ ℤ → (𝐴 ∈ (ℤ ∖ (ℤ≥‘(𝐵 + 1))) ↔ (𝐴 ∈ ℤ ∧ 𝐴 ≤ 𝐵))) | ||
| Theorem | lzunuz 42779 | 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 42780 | 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 42781 | Lower integers are countably infinite. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
| ⊢ (𝑁 ∈ ℤ → (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ≈ ω) | ||
| Theorem | elmapresaunres2 42782 | fresaunres2 6780 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
| ⊢ ((𝐹 ∈ (𝐶 ↑m 𝐴) ∧ 𝐺 ∈ (𝐶 ↑m 𝐵) ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ∪ 𝐺) ↾ 𝐵) = 𝐺) | ||
| Theorem | diophin 42783 | 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 42784 | 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 42785 | 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...𝐵))) | ||
| Theorem | diophrex 42786* | 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 42787* | 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 42788* | 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 42789 | The null set is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
| ⊢ (𝐴 ∈ ℕ0 → ∅ ∈ (Dioph‘𝐴)) | ||
| Theorem | vdioph 42790 | The "universal" set (as large as possible given eldiophss 42785) is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
| ⊢ (𝐴 ∈ ℕ0 → (ℕ0 ↑m (1...𝐴)) ∈ (Dioph‘𝐴)) | ||
| Theorem | anrabdioph 42791* | 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 42792* | 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 42793* | 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 42794* | 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‘𝑁)) | ||
| Theorem | 2sbcrex 42795* | Exchange an existential quantifier with two substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by NM, 24-Aug-2018.) |
| ⊢ ([𝐴 / 𝑎][𝐵 / 𝑏]∃𝑐 ∈ 𝐶 𝜑 ↔ ∃𝑐 ∈ 𝐶 [𝐴 / 𝑎][𝐵 / 𝑏]𝜑) | ||
| Theorem | sbcrexgOLD 42796* | 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 3875 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) | ||
| Theorem | 2sbcrexOLD 42797* | Exchange an existential quantifier with two substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 7475 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ([𝐴 / 𝑎][𝐵 / 𝑏]∃𝑐 ∈ 𝐶 𝜑 ↔ ∃𝑐 ∈ 𝐶 [𝐴 / 𝑎][𝐵 / 𝑏]𝜑) | ||
| Theorem | sbc2rex 42798* | Exchange a substitution with two existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by NM, 24-Aug-2018.) |
| ⊢ ([𝐴 / 𝑎]∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝜑 ↔ ∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 [𝐴 / 𝑎]𝜑) | ||
| Theorem | sbc2rexgOLD 42799* | Exchange a substitution with two existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 7475 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑎]∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝜑 ↔ ∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 [𝐴 / 𝑎]𝜑)) | ||
| Theorem | sbc4rex 42800* | Exchange a substitution with four existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by NM, 24-Aug-2018.) |
| ⊢ ([𝐴 / 𝑎]∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 ∃𝑒 ∈ 𝐸 𝜑 ↔ ∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 ∃𝑒 ∈ 𝐸 [𝐴 / 𝑎]𝜑) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |