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=supa∈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⁡D1<a
9 ssrexv ⊢Pell1QR⁡D⊆Pell14QR⁡D→∃a∈Pell1QR⁡D1<a→∃a∈Pell14QR⁡D1<a
10 7 8 9 sylc ⊢D∈ℕ∖◻ℕ→∃a∈Pell14QR⁡D1<a
11 rabn0 ⊢a∈Pell14QR⁡D|1<a≠∅↔∃a∈Pell14QR⁡D1<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<a1≤c
22 breq1 ⊢b=1→b≤c↔1≤c
23 22 ralbidv ⊢b=1→∀c∈a∈Pell14QR⁡D|1<ab≤c↔∀c∈a∈Pell14QR⁡D|1<a1≤c
24 23 rspcev ⊢1∈ℝ∧∀c∈a∈Pell14QR⁡D|1<a1≤c→∃b∈ℝ∀c∈a∈Pell14QR⁡D|1<ab≤c
25 13 21 24 sylancr ⊢D∈ℕ∖◻ℕ→∃b∈ℝ∀c∈a∈Pell14QR⁡D|1<ab≤c
26 infrecl ⊢a∈Pell14QR⁡D|1<a⊆ℝ∧a∈Pell14QR⁡D|1<a≠∅∧∃b∈ℝ∀c∈a∈Pell14QR⁡D|1<ab≤c→supa∈Pell14QR⁡D|1<aℝ<∈ℝ
27 6 12 25 26 syl3anc ⊢D∈ℕ∖◻ℕ→supa∈Pell14QR⁡D|1<aℝ<∈ℝ
28 1 27 eqeltrd ⊢D∈ℕ∖◻ℕ→PellFund⁡D∈ℝ