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