| Step | Hyp | Ref
| Expression |
| 1 | | elpell1qr 42858 |
. . 3
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (𝐴 ∈ (Pell1QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑎 ∈ ℕ0
∃𝑏 ∈
ℕ0 (𝐴 =
(𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)))) |
| 2 | | 1red 11262 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 1 ∈
ℝ) |
| 3 | | simplrl 777 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 𝑎 ∈
ℕ0) |
| 4 | 3 | nn0red 12588 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 𝑎 ∈
ℝ) |
| 5 | | eldifi 4131 |
. . . . . . . . . . . . . . 15
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → 𝐷 ∈ ℕ) |
| 6 | 5 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 𝐷 ∈
ℕ) |
| 7 | 6 | nnnn0d 12587 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 𝐷 ∈
ℕ0) |
| 8 | 7 | nn0red 12588 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 𝐷 ∈
ℝ) |
| 9 | 7 | nn0ge0d 12590 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 0 ≤
𝐷) |
| 10 | 8, 9 | resqrtcld 15456 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) →
(√‘𝐷) ∈
ℝ) |
| 11 | | simplrr 778 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 𝑏 ∈
ℕ0) |
| 12 | 11 | nn0red 12588 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 𝑏 ∈
ℝ) |
| 13 | 10, 12 | remulcld 11291 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) →
((√‘𝐷) ·
𝑏) ∈
ℝ) |
| 14 | 4, 13 | readdcld 11290 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → (𝑎 + ((√‘𝐷) · 𝑏)) ∈ ℝ) |
| 15 | | 2nn0 12543 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ0 |
| 16 | 15 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 2 ∈
ℕ0) |
| 17 | 11, 16 | nn0expcld 14285 |
. . . . . . . . . . . . . 14
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → (𝑏↑2) ∈
ℕ0) |
| 18 | 7, 17 | nn0mulcld 12592 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → (𝐷 · (𝑏↑2)) ∈
ℕ0) |
| 19 | 18 | nn0ge0d 12590 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 0 ≤
(𝐷 · (𝑏↑2))) |
| 20 | 18 | nn0red 12588 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → (𝐷 · (𝑏↑2)) ∈ ℝ) |
| 21 | 2, 20 | addge02d 11852 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → (0 ≤
(𝐷 · (𝑏↑2)) ↔ 1 ≤ ((𝐷 · (𝑏↑2)) + 1))) |
| 22 | 19, 21 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 1 ≤
((𝐷 · (𝑏↑2)) + 1)) |
| 23 | | sq1 14234 |
. . . . . . . . . . . 12
⊢
(1↑2) = 1 |
| 24 | 23 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) →
(1↑2) = 1) |
| 25 | | nn0cn 12536 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ ℕ0
→ 𝑎 ∈
ℂ) |
| 26 | 25 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ 𝑎 ∈
ℂ) |
| 27 | 26 | sqcld 14184 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ (𝑎↑2) ∈
ℂ) |
| 28 | 5 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ 𝐷 ∈
ℕ) |
| 29 | 28 | nncnd 12282 |
. . . . . . . . . . . . . . 15
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ 𝐷 ∈
ℂ) |
| 30 | | nn0cn 12536 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ ℕ0
→ 𝑏 ∈
ℂ) |
| 31 | 30 | ad2antll 729 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ 𝑏 ∈
ℂ) |
| 32 | 31 | sqcld 14184 |
. . . . . . . . . . . . . . 15
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ (𝑏↑2) ∈
ℂ) |
| 33 | 29, 32 | mulcld 11281 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ (𝐷 · (𝑏↑2)) ∈
ℂ) |
| 34 | | 1cnd 11256 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ 1 ∈ ℂ) |
| 35 | 27, 33, 34 | subaddd 11638 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ (((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1 ↔ ((𝐷 · (𝑏↑2)) + 1) = (𝑎↑2))) |
| 36 | 35 | biimpa 476 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → ((𝐷 · (𝑏↑2)) + 1) = (𝑎↑2)) |
| 37 | 36 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → (𝑎↑2) = ((𝐷 · (𝑏↑2)) + 1)) |
| 38 | 22, 24, 37 | 3brtr4d 5175 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) →
(1↑2) ≤ (𝑎↑2)) |
| 39 | | 0le1 11786 |
. . . . . . . . . . . 12
⊢ 0 ≤
1 |
| 40 | 39 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 0 ≤
1) |
| 41 | 3 | nn0ge0d 12590 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 0 ≤
𝑎) |
| 42 | 2, 4, 40, 41 | le2sqd 14296 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → (1 ≤
𝑎 ↔ (1↑2) ≤
(𝑎↑2))) |
| 43 | 38, 42 | mpbird 257 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 1 ≤
𝑎) |
| 44 | 8, 9 | sqrtge0d 15459 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 0 ≤
(√‘𝐷)) |
| 45 | 11 | nn0ge0d 12590 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 0 ≤
𝑏) |
| 46 | 10, 12, 44, 45 | mulge0d 11840 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 0 ≤
((√‘𝐷) ·
𝑏)) |
| 47 | 4, 13 | addge01d 11851 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → (0 ≤
((√‘𝐷) ·
𝑏) ↔ 𝑎 ≤ (𝑎 + ((√‘𝐷) · 𝑏)))) |
| 48 | 46, 47 | mpbid 232 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 𝑎 ≤ (𝑎 + ((√‘𝐷) · 𝑏))) |
| 49 | 2, 4, 14, 43, 48 | letrd 11418 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 1 ≤
(𝑎 + ((√‘𝐷) · 𝑏))) |
| 50 | 49 | adantrl 716 |
. . . . . . 7
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 1 ≤ (𝑎 + ((√‘𝐷) · 𝑏))) |
| 51 | | simprl 771 |
. . . . . . 7
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝐴 = (𝑎 + ((√‘𝐷) · 𝑏))) |
| 52 | 50, 51 | breqtrrd 5171 |
. . . . . 6
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 1 ≤ 𝐴) |
| 53 | 52 | ex 412 |
. . . . 5
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ ((𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 1 ≤ 𝐴)) |
| 54 | 53 | rexlimdvva 3213 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) → (∃𝑎 ∈ ℕ0
∃𝑏 ∈
ℕ0 (𝐴 =
(𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 1 ≤ 𝐴)) |
| 55 | 54 | expimpd 453 |
. . 3
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → ((𝐴 ∈ ℝ ∧ ∃𝑎 ∈ ℕ0
∃𝑏 ∈
ℕ0 (𝐴 =
(𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 1 ≤ 𝐴)) |
| 56 | 1, 55 | sylbid 240 |
. 2
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (𝐴 ∈ (Pell1QR‘𝐷) → 1 ≤ 𝐴)) |
| 57 | 56 | imp 406 |
1
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell1QR‘𝐷)) → 1 ≤ 𝐴) |