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 ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) ∈ ℝ )

Proof

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