Metamath Proof Explorer

Theorem pellfundre

Description: The fundamental solution of a Pell equation exists as a real number. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pellfundre ⊢ D ∈ ℕ ∖ ◻ ℕ → PellFund ⁡ D ∈ ℝ

Proof

Step Hyp Ref Expression
1 pellfundval ⊢ D ∈ ℕ ∖ ◻ ℕ → PellFund ⁡ D = inf a ∈ Pell14QR ⁡ D | 1 < a ℝ <
2 ssrab2 ⊢ a ∈ Pell14QR ⁡ D | 1 < a ⊆ Pell14QR ⁡ D
3 pell14qrre ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ a ∈ Pell14QR ⁡ D → a ∈ ℝ
4 3 ex ⊢ D ∈ ℕ ∖ ◻ ℕ → a ∈ Pell14QR ⁡ D → a ∈ ℝ
5 4 ssrdv ⊢ D ∈ ℕ ∖ ◻ ℕ → Pell14QR ⁡ D ⊆ ℝ
6 2 5 sstrid ⊢ D ∈ ℕ ∖ ◻ ℕ → a ∈ Pell14QR ⁡ D | 1 < a ⊆ ℝ
7 pell1qrss14 ⊢ D ∈ ℕ ∖ ◻ ℕ → Pell1QR ⁡ D ⊆ Pell14QR ⁡ D
8 pellqrex ⊢ D ∈ ℕ ∖ ◻ ℕ → ∃ a ∈ Pell1QR ⁡ D 1 < a
9 ssrexv ⊢ Pell1QR ⁡ D ⊆ Pell14QR ⁡ D → ∃ a ∈ Pell1QR ⁡ D 1 < a → ∃ a ∈ Pell14QR ⁡ D 1 < a
10 7 8 9 sylc ⊢ D ∈ ℕ ∖ ◻ ℕ → ∃ a ∈ Pell14QR ⁡ D 1 < a
11 rabn0 ⊢ a ∈ Pell14QR ⁡ D | 1 < a ≠ ∅ ↔ ∃ a ∈ Pell14QR ⁡ D 1 < a
12 10 11 sylibr ⊢ D ∈ ℕ ∖ ◻ ℕ → a ∈ Pell14QR ⁡ D | 1 < a ≠ ∅
13 1re ⊢ 1 ∈ ℝ
14 breq2 ⊢ a = c → 1 < a ↔ 1 < c
15 14 elrab ⊢ c ∈ a ∈ Pell14QR ⁡ D | 1 < a ↔ c ∈ Pell14QR ⁡ D ∧ 1 < c
16 pell14qrre ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ c ∈ Pell14QR ⁡ D → c ∈ ℝ
17 ltle ⊢ 1 ∈ ℝ ∧ c ∈ ℝ → 1 < c → 1 ≤ c
18 13 16 17 sylancr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ c ∈ Pell14QR ⁡ D → 1 < c → 1 ≤ c
19 18 expimpd ⊢ D ∈ ℕ ∖ ◻ ℕ → c ∈ Pell14QR ⁡ D ∧ 1 < c → 1 ≤ c
20 15 19 biimtrid ⊢ D ∈ ℕ ∖ ◻ ℕ → c ∈ a ∈ Pell14QR ⁡ D | 1 < a → 1 ≤ c
21 20 ralrimiv ⊢ D ∈ ℕ ∖ ◻ ℕ → ∀ c ∈ a ∈ Pell14QR ⁡ D | 1 < a 1 ≤ c
22 breq1 ⊢ b = 1 → b ≤ c ↔ 1 ≤ c
23 22 ralbidv ⊢ b = 1 → ∀ c ∈ a ∈ Pell14QR ⁡ D | 1 < a b ≤ c ↔ ∀ c ∈ a ∈ Pell14QR ⁡ D | 1 < a 1 ≤ c
24 23 rspcev ⊢ 1 ∈ ℝ ∧ ∀ c ∈ a ∈ Pell14QR ⁡ D | 1 < a 1 ≤ c → ∃ b ∈ ℝ ∀ c ∈ a ∈ Pell14QR ⁡ D | 1 < a b ≤ c
25 13 21 24 sylancr ⊢ D ∈ ℕ ∖ ◻ ℕ → ∃ b ∈ ℝ ∀ c ∈ a ∈ Pell14QR ⁡ D | 1 < a b ≤ c
26 infrecl ⊢ a ∈ Pell14QR ⁡ D | 1 < a ⊆ ℝ ∧ a ∈ Pell14QR ⁡ D | 1 < a ≠ ∅ ∧ ∃ b ∈ ℝ ∀ c ∈ a ∈ Pell14QR ⁡ D | 1 < a b ≤ c → inf a ∈ Pell14QR ⁡ D | 1 < a ℝ < ∈ ℝ
27 6 12 25 26 syl3anc ⊢ D ∈ ℕ ∖ ◻ ℕ → inf a ∈ Pell14QR ⁡ D | 1 < a ℝ < ∈ ℝ
28 1 27 eqeltrd ⊢ D ∈ ℕ ∖ ◻ ℕ → PellFund ⁡ D ∈ ℝ