Metamath Proof Explorer

Theorem pell14qrgapw

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

Ref Expression
Assertion pell14qrgapw ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 2 < 𝐴 )

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 1 a1i ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 2 ∈ ℝ )
3 eldifi ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 𝐷 ∈ ℕ )
4 3 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 𝐷 ∈ ℕ )
5 4 nnrpd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 𝐷 ∈ ℝ+ )
6 1rp ⊢ 1 ∈ ℝ+
7 6 a1i ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 1 ∈ ℝ+ )
8 5 7 rpaddcld ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( 𝐷 + 1 ) ∈ ℝ+ )
9 8 rpsqrtcld ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( √ ‘ ( 𝐷 + 1 ) ) ∈ ℝ+ )
10 9 rpred ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( √ ‘ ( 𝐷 + 1 ) ) ∈ ℝ )
11 5 rpsqrtcld ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( √ ‘ 𝐷 ) ∈ ℝ+ )
12 11 rpred ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( √ ‘ 𝐷 ) ∈ ℝ )
13 10 12 readdcld ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ∈ ℝ )
14 pell14qrre ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐴 ∈ ℝ )
15 14 3adant3 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ )
16 df-2 ⊢ 2 = ( 1 + 1 )
17 1red ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 1 ∈ ℝ )
18 4 nnred ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 𝐷 ∈ ℝ )
19 peano2re ⊢ ( 𝐷 ∈ ℝ → ( 𝐷 + 1 ) ∈ ℝ )
20 18 19 syl ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( 𝐷 + 1 ) ∈ ℝ )
21 4 nnge1d ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 1 ≤ 𝐷 )
22 18 ltp1d ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 𝐷 < ( 𝐷 + 1 ) )
23 17 18 20 21 22 lelttrd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 1 < ( 𝐷 + 1 ) )
24 sq1 ⊢ ( 1 ↑ 2 ) = 1
25 24 a1i ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( 1 ↑ 2 ) = 1 )
26 4 nncnd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 𝐷 ∈ ℂ )
27 peano2cn ⊢ ( 𝐷 ∈ ℂ → ( 𝐷 + 1 ) ∈ ℂ )
28 26 27 syl ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( 𝐷 + 1 ) ∈ ℂ )
29 28 sqsqrtd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( ( √ ‘ ( 𝐷 + 1 ) ) ↑ 2 ) = ( 𝐷 + 1 ) )
30 23 25 29 3brtr4d ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( 1 ↑ 2 ) < ( ( √ ‘ ( 𝐷 + 1 ) ) ↑ 2 ) )
31 0le1 ⊢ 0 ≤ 1
32 31 a1i ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 0 ≤ 1 )
33 9 rpge0d ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 0 ≤ ( √ ‘ ( 𝐷 + 1 ) ) )
34 17 10 32 33 lt2sqd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( 1 < ( √ ‘ ( 𝐷 + 1 ) ) ↔ ( 1 ↑ 2 ) < ( ( √ ‘ ( 𝐷 + 1 ) ) ↑ 2 ) ) )
35 30 34 mpbird ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 1 < ( √ ‘ ( 𝐷 + 1 ) ) )
36 26 sqsqrtd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( ( √ ‘ 𝐷 ) ↑ 2 ) = 𝐷 )
37 21 25 36 3brtr4d ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( 1 ↑ 2 ) ≤ ( ( √ ‘ 𝐷 ) ↑ 2 ) )
38 11 rpge0d ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 0 ≤ ( √ ‘ 𝐷 ) )
39 17 12 32 38 le2sqd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( 1 ≤ ( √ ‘ 𝐷 ) ↔ ( 1 ↑ 2 ) ≤ ( ( √ ‘ 𝐷 ) ↑ 2 ) ) )
40 37 39 mpbird ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 1 ≤ ( √ ‘ 𝐷 ) )
41 17 17 10 12 35 40 ltleaddd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( 1 + 1 ) < ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) )
42 16 41 eqbrtrid ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 2 < ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) )
43 pell14qrgap ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → ( ( √ ‘ ( 𝐷 + 1 ) ) + ( √ ‘ 𝐷 ) ) ≤ 𝐴 )
44 2 13 15 42 43 ltletrd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝐴 ) → 2 < 𝐴 )