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 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝐴 )