Proof of Theorem pell14qrgapw
| Step | Hyp | Ref
| Expression |
| 1 | | 2re 12340 |
. . 3
⊢ 2 ∈
ℝ |
| 2 | 1 | a1i 11 |
. 2
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 2 ∈ ℝ) |
| 3 | | eldifi 4131 |
. . . . . . . 8
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → 𝐷 ∈ ℕ) |
| 4 | 3 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 𝐷 ∈ ℕ) |
| 5 | 4 | nnrpd 13075 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 𝐷 ∈
ℝ+) |
| 6 | | 1rp 13038 |
. . . . . . 7
⊢ 1 ∈
ℝ+ |
| 7 | 6 | a1i 11 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 1 ∈
ℝ+) |
| 8 | 5, 7 | rpaddcld 13092 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (𝐷 + 1) ∈
ℝ+) |
| 9 | 8 | rpsqrtcld 15450 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (√‘(𝐷 + 1)) ∈
ℝ+) |
| 10 | 9 | rpred 13077 |
. . 3
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (√‘(𝐷 + 1)) ∈ ℝ) |
| 11 | 5 | rpsqrtcld 15450 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (√‘𝐷) ∈
ℝ+) |
| 12 | 11 | rpred 13077 |
. . 3
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (√‘𝐷) ∈ ℝ) |
| 13 | 10, 12 | readdcld 11290 |
. 2
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ∈ ℝ) |
| 14 | | pell14qrre 42868 |
. . 3
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ∈ ℝ) |
| 15 | 14 | 3adant3 1133 |
. 2
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 𝐴 ∈ ℝ) |
| 16 | | df-2 12329 |
. . 3
⊢ 2 = (1 +
1) |
| 17 | | 1red 11262 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 1 ∈ ℝ) |
| 18 | 4 | nnred 12281 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 𝐷 ∈ ℝ) |
| 19 | | peano2re 11434 |
. . . . . . . 8
⊢ (𝐷 ∈ ℝ → (𝐷 + 1) ∈
ℝ) |
| 20 | 18, 19 | syl 17 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (𝐷 + 1) ∈ ℝ) |
| 21 | 4 | nnge1d 12314 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 1 ≤ 𝐷) |
| 22 | 18 | ltp1d 12198 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 𝐷 < (𝐷 + 1)) |
| 23 | 17, 18, 20, 21, 22 | lelttrd 11419 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 1 < (𝐷 + 1)) |
| 24 | | sq1 14234 |
. . . . . . 7
⊢
(1↑2) = 1 |
| 25 | 24 | a1i 11 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (1↑2) = 1) |
| 26 | 4 | nncnd 12282 |
. . . . . . . 8
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 𝐷 ∈ ℂ) |
| 27 | | peano2cn 11433 |
. . . . . . . 8
⊢ (𝐷 ∈ ℂ → (𝐷 + 1) ∈
ℂ) |
| 28 | 26, 27 | syl 17 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (𝐷 + 1) ∈ ℂ) |
| 29 | 28 | sqsqrtd 15478 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → ((√‘(𝐷 + 1))↑2) = (𝐷 + 1)) |
| 30 | 23, 25, 29 | 3brtr4d 5175 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (1↑2) <
((√‘(𝐷 +
1))↑2)) |
| 31 | | 0le1 11786 |
. . . . . . 7
⊢ 0 ≤
1 |
| 32 | 31 | a1i 11 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 0 ≤ 1) |
| 33 | 9 | rpge0d 13081 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 0 ≤ (√‘(𝐷 + 1))) |
| 34 | 17, 10, 32, 33 | lt2sqd 14295 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (1 < (√‘(𝐷 + 1)) ↔ (1↑2) <
((√‘(𝐷 +
1))↑2))) |
| 35 | 30, 34 | mpbird 257 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 1 < (√‘(𝐷 + 1))) |
| 36 | 26 | sqsqrtd 15478 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → ((√‘𝐷)↑2) = 𝐷) |
| 37 | 21, 25, 36 | 3brtr4d 5175 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (1↑2) ≤
((√‘𝐷)↑2)) |
| 38 | 11 | rpge0d 13081 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 0 ≤ (√‘𝐷)) |
| 39 | 17, 12, 32, 38 | le2sqd 14296 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (1 ≤ (√‘𝐷) ↔ (1↑2) ≤
((√‘𝐷)↑2))) |
| 40 | 37, 39 | mpbird 257 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 1 ≤ (√‘𝐷)) |
| 41 | 17, 17, 10, 12, 35, 40 | ltleaddd 11884 |
. . 3
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (1 + 1) < ((√‘(𝐷 + 1)) + (√‘𝐷))) |
| 42 | 16, 41 | eqbrtrid 5178 |
. 2
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 2 < ((√‘(𝐷 + 1)) + (√‘𝐷))) |
| 43 | | pell14qrgap 42886 |
. 2
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ 𝐴) |
| 44 | 2, 13, 15, 42, 43 | ltletrd 11421 |
1
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 2 < 𝐴) |