Metamath Proof Explorer

Theorem pellfundlb

Description: 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)

Ref Expression
Assertion pellfundlb ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( PellFund ‘ 𝐷 ) ≤ 𝐴 )

Proof

Step Hyp Ref Expression
1 pellfundval ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) = inf ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } , ℝ , < ) )
2 1 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( PellFund ‘ 𝐷 ) = inf ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } , ℝ , < ) )
3 ssrab2 ⊢ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ⊆ ( Pell14QR ‘ 𝐷 )
4 pell14qrre ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑑 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝑑 ∈ ℝ )
5 4 ex ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝑑 ∈ ( Pell14QR ‘ 𝐷 ) → 𝑑 ∈ ℝ ) )
6 5 ssrdv ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( Pell14QR ‘ 𝐷 ) ⊆ ℝ )
7 3 6 sstrid ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ⊆ ℝ )
8 7 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ⊆ ℝ )
9 1re ⊢ 1 ∈ ℝ
10 breq2 ⊢ ( 𝑎 = 𝑐 → ( 1 < 𝑎 ↔ 1 < 𝑐 ) )
11 10 elrab ⊢ ( 𝑐 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ↔ ( 𝑐 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝑐 ) )
12 pell14qrre ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑐 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝑐 ∈ ℝ )
13 ltle ⊢ ( ( 1 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ( 1 < 𝑐 → 1 ≤ 𝑐 ) )
14 9 12 13 sylancr ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑐 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 1 < 𝑐 → 1 ≤ 𝑐 ) )
15 14 expimpd ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 𝑐 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝑐 ) → 1 ≤ 𝑐 ) )
16 11 15 syl5bi ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝑐 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } → 1 ≤ 𝑐 ) )
17 16 ralrimiv ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ∀ 𝑐 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } 1 ≤ 𝑐 )
18 17 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ∀ 𝑐 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } 1 ≤ 𝑐 )
19 breq1 ⊢ ( 𝑏 = 1 → ( 𝑏 ≤ 𝑐 ↔ 1 ≤ 𝑐 ) )
20 19 ralbidv ⊢ ( 𝑏 = 1 → ( ∀ 𝑐 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } 𝑏 ≤ 𝑐 ↔ ∀ 𝑐 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } 1 ≤ 𝑐 ) )
21 20 rspcev ⊢ ( ( 1 ∈ ℝ ∧ ∀ 𝑐 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } 1 ≤ 𝑐 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑐 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } 𝑏 ≤ 𝑐 )
22 9 18 21 sylancr ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑐 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } 𝑏 ≤ 𝑐 )
23 simp2 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) )
24 simp3 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 1 < 𝐴 )
25 breq2 ⊢ ( 𝑎 = 𝐴 → ( 1 < 𝑎 ↔ 1 < 𝐴 ) )
26 25 elrab ⊢ ( 𝐴 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ↔ ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) )
27 23 24 26 sylanbrc ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 𝐴 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } )
28 infrelb ⊢ ( ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ⊆ ℝ ∧ ∃ 𝑏 ∈ ℝ ∀ 𝑐 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } 𝑏 ≤ 𝑐 ∧ 𝐴 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ) → inf ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } , ℝ , < ) ≤ 𝐴 )
29 8 22 27 28 syl3anc ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → inf ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } , ℝ , < ) ≤ 𝐴 )
30 2 29 eqbrtrd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( PellFund ‘ 𝐷 ) ≤ 𝐴 )