| Metamath
Proof Explorer Theorem List (p. 429 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 | sbc4rexgOLD 42801* | Exchange a substitution with four 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 | sbcrot3 42802* | Rotate a sequence of three explicit substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Mario Carneiro, 11-Dec-2016.) |
| ⊢ ([𝐴 / 𝑎][𝐵 / 𝑏][𝐶 / 𝑐]𝜑 ↔ [𝐵 / 𝑏][𝐶 / 𝑐][𝐴 / 𝑎]𝜑) | ||
| Theorem | sbcrot5 42803* | Rotate a sequence of five explicit substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Mario Carneiro, 11-Dec-2016.) |
| ⊢ ([𝐴 / 𝑎][𝐵 / 𝑏][𝐶 / 𝑐][𝐷 / 𝑑][𝐸 / 𝑒]𝜑 ↔ [𝐵 / 𝑏][𝐶 / 𝑐][𝐷 / 𝑑][𝐸 / 𝑒][𝐴 / 𝑎]𝜑) | ||
| Theorem | sbccomieg 42804* | 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 42805* | 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 42806* | 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 42807* | 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 42808* | 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 42809* | 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 42810* | 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 42811* | 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‘𝑁)) | ||
| Theorem | rabdiophlem1 42812* | Lemma for arithmetic diophantine sets. Convert polynomial-ness of an expression into a constraint suitable for ralimi 3083. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
| ⊢ ((𝑡 ∈ (ℤ ↑m (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) → ∀𝑡 ∈ (ℕ0 ↑m (1...𝑁))𝐴 ∈ ℤ) | ||
| Theorem | rabdiophlem2 42813* | 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 42814* | 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 42815* | 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 42816* | 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 42817* | 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 42818* | Diophantine set builder for positivity. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑m (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ 𝐴 ∈ ℕ} ∈ (Dioph‘𝑁)) | ||
| Theorem | ltrabdioph 42819* | 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 42820* | 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 42821* | 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‘𝑁)) | ||
| Theorem | eldioph4b 42822* | 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 42823* | Forward-only version of eldioph4b 42822. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
| ⊢ 𝑊 ∈ V & ⊢ ¬ 𝑊 ∈ Fin & ⊢ (𝑊 ∩ ℕ) = ∅ ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑃 ∈ (mzPoly‘(𝑊 ∪ (1...𝑁)))) → {𝑡 ∈ (ℕ0 ↑m (1...𝑁)) ∣ ∃𝑤 ∈ (ℕ0 ↑m 𝑊)(𝑃‘(𝑡 ∪ 𝑤)) = 0} ∈ (Dioph‘𝑁)) | ||
| Theorem | diophren 42824* | 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 42825* | 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 42826* | 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‘𝑁)) | ||
| Theorem | fphpd 42827* | 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 42828* | Pigeonhole principle for sets of real numbers with implicit output reordering. (Contributed by Stefan O'Rear, 12-Sep-2014.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐵 ≺ 𝐴) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐶 ∈ 𝐵) & ⊢ (𝑧 = 𝑥 → 𝐶 = 𝐷) & ⊢ (𝑧 = 𝑦 → 𝐶 = 𝐸) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ 𝐷 = 𝐸)) | ||
| Theorem | ctbnfien 42829 | 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 42830* | Infinite pigeonhole principle for partitioning an infinite set between finitely many buckets. (Contributed by Stefan O'Rear, 18-Oct-2014.) |
| ⊢ (𝜑 → 𝐴 ≈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ 𝐵 {𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦} ≈ ℕ) | ||
| Theorem | rencldnfilem 42831* | Lemma for rencldnfi 42832. (Contributed by Stefan O'Rear, 18-Oct-2014.) |
| ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥) → ¬ 𝐴 ∈ Fin) | ||
| Theorem | rencldnfi 42832* | A set of real numbers which comes arbitrarily close to some target yet excludes it is infinite. The work is done in rencldnfilem 42831 using infima; this theorem removes the requirement that A be nonempty. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
| ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ 𝐵 ∈ 𝐴) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥) → ¬ 𝐴 ∈ Fin) | ||
| Theorem | irrapxlem1 42833* | Lemma for irrapx1 42839. Divides the unit interval into 𝐵 half-open sections and using the pigeonhole principle fphpdo 42828 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 42834* | Lemma for irrapx1 42839. 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 42835* | Lemma for irrapx1 42839. 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 42836* | Lemma for irrapx1 42839. 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 42837* | Lemma for irrapx1 42839. Switching to real intervals and fraction syntax. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ ℚ (0 < 𝑥 ∧ (abs‘(𝑥 − 𝐴)) < 𝐵 ∧ (abs‘(𝑥 − 𝐴)) < ((denom‘𝑥)↑-2))) | ||
| Theorem | irrapxlem6 42838* | Lemma for irrapx1 42839. Explicit description of a non-closed set. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ {𝑦 ∈ ℚ ∣ (0 < 𝑦 ∧ (abs‘(𝑦 − 𝐴)) < ((denom‘𝑦)↑-2))} (abs‘(𝑥 − 𝐴)) < 𝐵) | ||
| Theorem | irrapx1 42839* | 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))} ≈ ℕ) | ||
| Theorem | pellexlem1 42840 | Lemma for pellex 42846. 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 42841 | Lemma for pellex 42846. Arithmetical core of pellexlem3, norm upper bound. (Contributed by Stefan O'Rear, 14-Sep-2014.) |
| ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) < (1 + (2 · (√‘𝐷)))) | ||
| Theorem | pellexlem3 42842* | Lemma for pellex 42846. 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 42843* | Lemma for pellex 42846. Invoking irrapx1 42839, we have infinitely many near-solutions. (Contributed by Stefan O'Rear, 14-Sep-2014.) |
| ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ≈ ℕ) | ||
| Theorem | pellexlem5 42844* | Lemma for pellex 42846. Invoking fiphp3d 42830, we have infinitely many near-solutions for some specific norm. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
| ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ∃𝑥 ∈ ℤ (𝑥 ≠ 0 ∧ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)) | ||
| Theorem | pellexlem6 42845* | Lemma for pellex 42846. 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 42846* | Every Pell equation has a nontrivial solution. Theorem 62 in [vandenDries] p. 43. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
| ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ ((𝑥↑2) − (𝐷 · (𝑦↑2))) = 1) | ||
| Syntax | csquarenn 42847 | Extend class notation to include the set of square positive integers. |
| class ◻NN | ||
| Syntax | cpell1qr 42848 | Extend class notation to include the class of quadrant-1 Pell solutions. |
| class Pell1QR | ||
| Syntax | cpell1234qr 42849 | Extend class notation to include the class of any-quadrant Pell solutions. |
| class Pell1234QR | ||
| Syntax | cpell14qr 42850 | Extend class notation to include the class of positive Pell solutions. |
| class Pell14QR | ||
| Syntax | cpellfund 42851 | Extend class notation to include the Pell-equation fundamental solution function. |
| class PellFund | ||
| Definition | df-squarenn 42852 | Define the set of square positive integers. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ◻NN = {𝑥 ∈ ℕ ∣ (√‘𝑥) ∈ ℚ} | ||
| Definition | df-pell1qr 42853* | 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 42854* | 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 42855* | Define the general solutions of a Pell equation. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ Pell1234QR = (𝑥 ∈ (ℕ ∖ ◻NN) ↦ {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)}) | ||
| Definition | df-pellfund 42856* | 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 42857* | 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 42858* | 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 42859* | Value of the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell14QR‘𝐷) = {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)}) | ||
| Theorem | elpell14qr 42860* | Membership in the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℤ (𝐴 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)))) | ||
| Theorem | pell1234qrval 42861* | Value of the set of general Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell1234QR‘𝐷) = {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)}) | ||
| Theorem | elpell1234qr 42862* | Membership in the set of general Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell1234QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ (𝐴 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)))) | ||
| Theorem | pell1234qrre 42863 | General Pell solutions are (coded as) real numbers. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → 𝐴 ∈ ℝ) | ||
| Theorem | pell1234qrne0 42864 | No solution to a Pell equation is zero. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → 𝐴 ≠ 0) | ||
| Theorem | pell1234qrreccl 42865 | General solutions of the Pell equation are closed under reciprocals. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → (1 / 𝐴) ∈ (Pell1234QR‘𝐷)) | ||
| Theorem | pell1234qrmulcl 42866 | General solutions of the Pell equation are closed under multiplication. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷) ∧ 𝐵 ∈ (Pell1234QR‘𝐷)) → (𝐴 · 𝐵) ∈ (Pell1234QR‘𝐷)) | ||
| Theorem | pell14qrss1234 42867 | A positive Pell solution is a general Pell solution. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell14QR‘𝐷) ⊆ (Pell1234QR‘𝐷)) | ||
| Theorem | pell14qrre 42868 | A positive Pell solution is a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ∈ ℝ) | ||
| Theorem | pell14qrne0 42869 | A positive Pell solution is a nonzero number. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ≠ 0) | ||
| Theorem | pell14qrgt0 42870 | A positive Pell solution is a positive number. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 0 < 𝐴) | ||
| Theorem | pell14qrrp 42871 | A positive Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ∈ ℝ+) | ||
| Theorem | pell1234qrdich 42872 | A general Pell solution is either a positive solution, or its negation is. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷))) | ||
| Theorem | elpell14qr2 42873 | A number is a positive Pell solution iff it is positive and a Pell solution, justifying our name choice. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ (𝐴 ∈ (Pell1234QR‘𝐷) ∧ 0 < 𝐴))) | ||
| Theorem | pell14qrmulcl 42874 | Positive Pell solutions are closed under multiplication. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ (Pell14QR‘𝐷)) → (𝐴 · 𝐵) ∈ (Pell14QR‘𝐷)) | ||
| Theorem | pell14qrreccl 42875 | Positive Pell solutions are closed under reciprocal. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → (1 / 𝐴) ∈ (Pell14QR‘𝐷)) | ||
| Theorem | pell14qrdivcl 42876 | Positive Pell solutions are closed under division. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ (Pell14QR‘𝐷)) → (𝐴 / 𝐵) ∈ (Pell14QR‘𝐷)) | ||
| Theorem | pell14qrexpclnn0 42877 | Lemma for pell14qrexpcl 42878. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝐵) ∈ (Pell14QR‘𝐷)) | ||
| Theorem | pell14qrexpcl 42878 | Positive Pell solutions are closed under integer powers. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ ℤ) → (𝐴↑𝐵) ∈ (Pell14QR‘𝐷)) | ||
| Theorem | pell1qrss14 42879 | First-quadrant Pell solutions are a subset of the positive solutions. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷)) | ||
| Theorem | pell14qrdich 42880 | A positive Pell solution is either in the first quadrant, or its reciprocal is. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → (𝐴 ∈ (Pell1QR‘𝐷) ∨ (1 / 𝐴) ∈ (Pell1QR‘𝐷))) | ||
| Theorem | pell1qrge1 42881 | A Pell solution in the first quadrant is at least 1. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1QR‘𝐷)) → 1 ≤ 𝐴) | ||
| Theorem | pell1qr1 42882 | 1 is a Pell solution and in the first quadrant as one. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → 1 ∈ (Pell1QR‘𝐷)) | ||
| Theorem | elpell1qr2 42883 | The first quadrant solutions are precisely the positive Pell solutions which are at least one. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell1QR‘𝐷) ↔ (𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 ≤ 𝐴))) | ||
| Theorem | pell1qrgaplem 42884 | Lemma for pell1qrgap 42885. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ (𝐴 + ((√‘𝐷) · 𝐵))) | ||
| Theorem | pell1qrgap 42885 | First-quadrant Pell solutions are bounded away from 1. (This particular bound allows to prove exact values for the fundamental solution later.) (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1QR‘𝐷) ∧ 1 < 𝐴) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ 𝐴) | ||
| Theorem | pell14qrgap 42886 | Positive Pell solutions are bounded away from 1. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ 𝐴) | ||
| Theorem | pell14qrgapw 42887 | Positive Pell solutions are bounded away from 1, with a friendlier bound. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 2 < 𝐴) | ||
| Theorem | pellqrexplicit 42888 | Condition for a calculated real to be a Pell solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1) → (𝐴 + ((√‘𝐷) · 𝐵)) ∈ (Pell1QR‘𝐷)) | ||
| Theorem | infmrgelbi 42889* | Any lower bound of a nonempty set of real numbers is less than or equal to its infimum, one-direction version. (Contributed by Stefan O'Rear, 1-Sep-2013.) (Revised by AV, 17-Sep-2020.) |
| ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ 𝐵 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑥) → 𝐵 ≤ inf(𝐴, ℝ, < )) | ||
| Theorem | pellqrex 42890* | There is a nontrivial solution of a Pell equation in the first quadrant. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → ∃𝑥 ∈ (Pell1QR‘𝐷)1 < 𝑥) | ||
| Theorem | pellfundval 42891* | Value of the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 18-Sep-2014.) (Revised by AV, 17-Sep-2020.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) = inf({𝑥 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑥}, ℝ, < )) | ||
| Theorem | pellfundre 42892 | The fundamental solution of a Pell equation exists as a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℝ) | ||
| Theorem | pellfundge 42893 | Lower bound on the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ (PellFund‘𝐷)) | ||
| Theorem | pellfundgt1 42894 | Weak lower bound on the Pell fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → 1 < (PellFund‘𝐷)) | ||
| Theorem | pellfundlb 42895 | A nontrivial first quadrant solution is at least as large as the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Proof shortened by AV, 15-Sep-2020.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (PellFund‘𝐷) ≤ 𝐴) | ||
| Theorem | pellfundglb 42896* | If a real is larger than the fundamental solution, there is a nontrivial solution less than it. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → ∃𝑥 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑥 ∧ 𝑥 < 𝐴)) | ||
| Theorem | pellfundex 42897 |
The fundamental solution as an infimum is itself a solution, showing
that the solution set is discrete.
Since the fundamental solution is an infimum, there must be an element ge to Fund and lt 2*Fund. If this element is equal to the fundamental solution we're done, otherwise use the infimum again to find another element which must be ge Fund and lt the first element; their ratio is a group element in (1,2), contradicting pell14qrgapw 42887. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)) | ||
| Theorem | pellfund14gap 42898 | There are no solutions between 1 and the fundamental solution. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ (1 ≤ 𝐴 ∧ 𝐴 < (PellFund‘𝐷))) → 𝐴 = 1) | ||
| Theorem | pellfundrp 42899 | The fundamental Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℝ+) | ||
| Theorem | pellfundne1 42900 | The fundamental Pell solution is never 1. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ≠ 1) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |