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 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ Pell14QR ⁡ D ∧ 1 < A → 2 < A

Proof

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