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 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → PellFund ⁡ D ≤ A

Proof

Step Hyp Ref Expression
1 pellfundval ⊢ D ∈ ℕ ∖ ◻ ℕ → PellFund ⁡ D = inf a ∈ Pell14QR ⁡ D | 1 < a ℝ <
2 1 3ad2ant1 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → PellFund ⁡ D = inf a ∈ Pell14QR ⁡ D | 1 < a ℝ <
3 ssrab2 ⊢ a ∈ Pell14QR ⁡ D | 1 < a ⊆ Pell14QR ⁡ D
4 pell14qrre ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ d ∈ Pell14QR ⁡ D → d ∈ ℝ
5 4 ex ⊢ D ∈ ℕ ∖ ◻ ℕ → d ∈ Pell14QR ⁡ D → d ∈ ℝ
6 5 ssrdv ⊢ D ∈ ℕ ∖ ◻ ℕ → Pell14QR ⁡ D ⊆ ℝ
7 3 6 sstrid ⊢ D ∈ ℕ ∖ ◻ ℕ → a ∈ Pell14QR ⁡ D | 1 < a ⊆ ℝ
8 7 3ad2ant1 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → a ∈ Pell14QR ⁡ D | 1 < a ⊆ ℝ
9 1re ⊢ 1 ∈ ℝ
10 breq2 ⊢ a = c → 1 < a ↔ 1 < c
11 10 elrab ⊢ c ∈ a ∈ Pell14QR ⁡ D | 1 < a ↔ c ∈ Pell14QR ⁡ D ∧ 1 < c
12 pell14qrre ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ c ∈ Pell14QR ⁡ D → c ∈ ℝ
13 ltle ⊢ 1 ∈ ℝ ∧ c ∈ ℝ → 1 < c → 1 ≤ c
14 9 12 13 sylancr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ c ∈ Pell14QR ⁡ D → 1 < c → 1 ≤ c
15 14 expimpd ⊢ D ∈ ℕ ∖ ◻ ℕ → c ∈ Pell14QR ⁡ D ∧ 1 < c → 1 ≤ c
16 11 15 biimtrid ⊢ D ∈ ℕ ∖ ◻ ℕ → c ∈ a ∈ Pell14QR ⁡ D | 1 < a → 1 ≤ c
17 16 ralrimiv ⊢ D ∈ ℕ ∖ ◻ ℕ → ∀ c ∈ a ∈ Pell14QR ⁡ D | 1 < a 1 ≤ c
18 17 3ad2ant1 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → ∀ c ∈ a ∈ Pell14QR ⁡ D | 1 < a 1 ≤ c
19 breq1 ⊢ b = 1 → b ≤ c ↔ 1 ≤ c
20 19 ralbidv ⊢ b = 1 → ∀ c ∈ a ∈ Pell14QR ⁡ D | 1 < a b ≤ c ↔ ∀ c ∈ a ∈ Pell14QR ⁡ D | 1 < a 1 ≤ c
21 20 rspcev ⊢ 1 ∈ ℝ ∧ ∀ c ∈ a ∈ Pell14QR ⁡ D | 1 < a 1 ≤ c → ∃ b ∈ ℝ ∀ c ∈ a ∈ Pell14QR ⁡ D | 1 < a b ≤ c
22 9 18 21 sylancr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → ∃ b ∈ ℝ ∀ c ∈ a ∈ Pell14QR ⁡ D | 1 < a b ≤ c
23 simp2 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → A ∈ Pell14QR ⁡ D
24 simp3 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → 1 < A
25 breq2 ⊢ a = A → 1 < a ↔ 1 < A
26 25 elrab ⊢ A ∈ a ∈ Pell14QR ⁡ D | 1 < a ↔ A ∈ Pell14QR ⁡ D ∧ 1 < A
27 23 24 26 sylanbrc ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → A ∈ a ∈ Pell14QR ⁡ D | 1 < a
28 infrelb ⊢ a ∈ Pell14QR ⁡ D | 1 < a ⊆ ℝ ∧ ∃ b ∈ ℝ ∀ c ∈ a ∈ Pell14QR ⁡ D | 1 < a b ≤ c ∧ A ∈ a ∈ Pell14QR ⁡ D | 1 < a → inf a ∈ Pell14QR ⁡ D | 1 < a ℝ < ≤ A
29 8 22 27 28 syl3anc ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → inf a ∈ Pell14QR ⁡ D | 1 < a ℝ < ≤ A
30 2 29 eqbrtrd ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → PellFund ⁡ D ≤ A