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 ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝐴 )

Proof

Step Hyp Ref Expression
1 simp2 ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) )
2 1re 1 ∈ ℝ
3 pell14qrre ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐴 ∈ ℝ )
4 ltle ( ( 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 1 < 𝐴 → 1 ≤ 𝐴 ) )
5 2 3 4 sylancr ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 1 < 𝐴 → 1 ≤ 𝐴 ) )
6 5 3impia ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 1 ≤ 𝐴 )
7 elpell1qr2 ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell1QR ‘ 𝐷 ) ↔ ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 ≤ 𝐴 ) ) )
8 7 3ad2ant1 ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( 𝐴 ∈ ( Pell1QR ‘ 𝐷 ) ↔ ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 ≤ 𝐴 ) ) )
9 1 6 8 mpbir2and ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 𝐴 ∈ ( Pell1QR ‘ 𝐷 ) )
10 pell1qrgap ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝐴 )
11 9 10 syld3an2 ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝐴 )