Metamath Proof Explorer

Theorem pell14qrgap

Description: Positive Pell solutions are bounded away from 1. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pell14qrgap ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → D + 1 + D ≤ A

Proof

Step Hyp Ref Expression
1 simp2 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → A ∈ Pell14QR ⁡ D
2 1re ⊢ 1 ∈ ℝ
3 pell14qrre ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → A ∈ ℝ
4 ltle ⊢ 1 ∈ ℝ ∧ A ∈ ℝ → 1 < A → 1 ≤ A
5 2 3 4 sylancr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D → 1 < A → 1 ≤ A
6 5 3impia ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → 1 ≤ A
7 elpell1qr2 ⊢ D ∈ ℕ ∖ ◻ ℕ → A ∈ Pell1QR ⁡ D ↔ A ∈ Pell14QR ⁡ D ∧ 1 ≤ A
8 7 3ad2ant1 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → A ∈ Pell1QR ⁡ D ↔ A ∈ Pell14QR ⁡ D ∧ 1 ≤ A
9 1 6 8 mpbir2and ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → A ∈ Pell1QR ⁡ D
10 pell1qrgap ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell1QR ⁡ D ∧ 1 < A → D + 1 + D ≤ A
11 9 10 syld3an2 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → D + 1 + D ≤ A