Proof of Theorem pell14qrgapw
Step | Hyp | Ref
| Expression |
1 | | 2re 12047 |
. . 3
⊢ 2 ∈
ℝ |
2 | 1 | a1i 11 |
. 2
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 2 ∈ ℝ) |
3 | | eldifi 4061 |
. . . . . . . 8
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → 𝐷 ∈ ℕ) |
4 | 3 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 𝐷 ∈ ℕ) |
5 | 4 | nnrpd 12770 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 𝐷 ∈
ℝ+) |
6 | | 1rp 12734 |
. . . . . . 7
⊢ 1 ∈
ℝ+ |
7 | 6 | a1i 11 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 1 ∈
ℝ+) |
8 | 5, 7 | rpaddcld 12787 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (𝐷 + 1) ∈
ℝ+) |
9 | 8 | rpsqrtcld 15123 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (√‘(𝐷 + 1)) ∈
ℝ+) |
10 | 9 | rpred 12772 |
. . 3
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (√‘(𝐷 + 1)) ∈ ℝ) |
11 | 5 | rpsqrtcld 15123 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (√‘𝐷) ∈
ℝ+) |
12 | 11 | rpred 12772 |
. . 3
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (√‘𝐷) ∈ ℝ) |
13 | 10, 12 | readdcld 11004 |
. 2
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ∈ ℝ) |
14 | | pell14qrre 40679 |
. . 3
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ∈ ℝ) |
15 | 14 | 3adant3 1131 |
. 2
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 𝐴 ∈ ℝ) |
16 | | df-2 12036 |
. . 3
⊢ 2 = (1 +
1) |
17 | | 1red 10976 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 1 ∈ ℝ) |
18 | 4 | nnred 11988 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 𝐷 ∈ ℝ) |
19 | | peano2re 11148 |
. . . . . . . 8
⊢ (𝐷 ∈ ℝ → (𝐷 + 1) ∈
ℝ) |
20 | 18, 19 | syl 17 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (𝐷 + 1) ∈ ℝ) |
21 | 4 | nnge1d 12021 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 1 ≤ 𝐷) |
22 | 18 | ltp1d 11905 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 𝐷 < (𝐷 + 1)) |
23 | 17, 18, 20, 21, 22 | lelttrd 11133 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 1 < (𝐷 + 1)) |
24 | | sq1 13912 |
. . . . . . 7
⊢
(1↑2) = 1 |
25 | 24 | a1i 11 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (1↑2) = 1) |
26 | 4 | nncnd 11989 |
. . . . . . . 8
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 𝐷 ∈ ℂ) |
27 | | peano2cn 11147 |
. . . . . . . 8
⊢ (𝐷 ∈ ℂ → (𝐷 + 1) ∈
ℂ) |
28 | 26, 27 | syl 17 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (𝐷 + 1) ∈ ℂ) |
29 | 28 | sqsqrtd 15151 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → ((√‘(𝐷 + 1))↑2) = (𝐷 + 1)) |
30 | 23, 25, 29 | 3brtr4d 5106 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (1↑2) <
((√‘(𝐷 +
1))↑2)) |
31 | | 0le1 11498 |
. . . . . . 7
⊢ 0 ≤
1 |
32 | 31 | a1i 11 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 0 ≤ 1) |
33 | 9 | rpge0d 12776 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 0 ≤ (√‘(𝐷 + 1))) |
34 | 17, 10, 32, 33 | lt2sqd 13973 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (1 < (√‘(𝐷 + 1)) ↔ (1↑2) <
((√‘(𝐷 +
1))↑2))) |
35 | 30, 34 | mpbird 256 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 1 < (√‘(𝐷 + 1))) |
36 | 26 | sqsqrtd 15151 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → ((√‘𝐷)↑2) = 𝐷) |
37 | 21, 25, 36 | 3brtr4d 5106 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (1↑2) ≤
((√‘𝐷)↑2)) |
38 | 11 | rpge0d 12776 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 0 ≤ (√‘𝐷)) |
39 | 17, 12, 32, 38 | le2sqd 13974 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (1 ≤ (√‘𝐷) ↔ (1↑2) ≤
((√‘𝐷)↑2))) |
40 | 37, 39 | mpbird 256 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 1 ≤ (√‘𝐷)) |
41 | 17, 17, 10, 12, 35, 40 | ltleaddd 11596 |
. . 3
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (1 + 1) < ((√‘(𝐷 + 1)) + (√‘𝐷))) |
42 | 16, 41 | eqbrtrid 5109 |
. 2
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 2 < ((√‘(𝐷 + 1)) + (√‘𝐷))) |
43 | | pell14qrgap 40697 |
. 2
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ 𝐴) |
44 | 2, 13, 15, 42, 43 | ltletrd 11135 |
1
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 2 < 𝐴) |