Step | Hyp | Ref
| Expression |
1 | | elpell1qr 40324 |
. . 3
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (𝐴 ∈ (Pell1QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑎 ∈ ℕ0
∃𝑏 ∈
ℕ0 (𝐴 =
(𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)))) |
2 | | 1red 10817 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 1 ∈
ℝ) |
3 | | simplrl 777 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 𝑎 ∈
ℕ0) |
4 | 3 | nn0red 12134 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 𝑎 ∈
ℝ) |
5 | | eldifi 4031 |
. . . . . . . . . . . . . . 15
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → 𝐷 ∈ ℕ) |
6 | 5 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 𝐷 ∈
ℕ) |
7 | 6 | nnnn0d 12133 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 𝐷 ∈
ℕ0) |
8 | 7 | nn0red 12134 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 𝐷 ∈
ℝ) |
9 | 7 | nn0ge0d 12136 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 0 ≤
𝐷) |
10 | 8, 9 | resqrtcld 14964 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) →
(√‘𝐷) ∈
ℝ) |
11 | | simplrr 778 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 𝑏 ∈
ℕ0) |
12 | 11 | nn0red 12134 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 𝑏 ∈
ℝ) |
13 | 10, 12 | remulcld 10846 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) →
((√‘𝐷) ·
𝑏) ∈
ℝ) |
14 | 4, 13 | readdcld 10845 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → (𝑎 + ((√‘𝐷) · 𝑏)) ∈ ℝ) |
15 | | 2nn0 12090 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ0 |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 2 ∈
ℕ0) |
17 | 11, 16 | nn0expcld 13796 |
. . . . . . . . . . . . . 14
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → (𝑏↑2) ∈
ℕ0) |
18 | 7, 17 | nn0mulcld 12138 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → (𝐷 · (𝑏↑2)) ∈
ℕ0) |
19 | 18 | nn0ge0d 12136 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 0 ≤
(𝐷 · (𝑏↑2))) |
20 | 18 | nn0red 12134 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → (𝐷 · (𝑏↑2)) ∈ ℝ) |
21 | 2, 20 | addge02d 11404 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → (0 ≤
(𝐷 · (𝑏↑2)) ↔ 1 ≤ ((𝐷 · (𝑏↑2)) + 1))) |
22 | 19, 21 | mpbid 235 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 1 ≤
((𝐷 · (𝑏↑2)) + 1)) |
23 | | sq1 13747 |
. . . . . . . . . . . 12
⊢
(1↑2) = 1 |
24 | 23 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) →
(1↑2) = 1) |
25 | | nn0cn 12083 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ ℕ0
→ 𝑎 ∈
ℂ) |
26 | 25 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ 𝑎 ∈
ℂ) |
27 | 26 | sqcld 13697 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ (𝑎↑2) ∈
ℂ) |
28 | 5 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ 𝐷 ∈
ℕ) |
29 | 28 | nncnd 11829 |
. . . . . . . . . . . . . . 15
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ 𝐷 ∈
ℂ) |
30 | | nn0cn 12083 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ ℕ0
→ 𝑏 ∈
ℂ) |
31 | 30 | ad2antll 729 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ 𝑏 ∈
ℂ) |
32 | 31 | sqcld 13697 |
. . . . . . . . . . . . . . 15
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ (𝑏↑2) ∈
ℂ) |
33 | 29, 32 | mulcld 10836 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ (𝐷 · (𝑏↑2)) ∈
ℂ) |
34 | | 1cnd 10811 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ 1 ∈ ℂ) |
35 | 27, 33, 34 | subaddd 11190 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ (((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1 ↔ ((𝐷 · (𝑏↑2)) + 1) = (𝑎↑2))) |
36 | 35 | biimpa 480 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → ((𝐷 · (𝑏↑2)) + 1) = (𝑎↑2)) |
37 | 36 | eqcomd 2740 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → (𝑎↑2) = ((𝐷 · (𝑏↑2)) + 1)) |
38 | 22, 24, 37 | 3brtr4d 5075 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) →
(1↑2) ≤ (𝑎↑2)) |
39 | | 0le1 11338 |
. . . . . . . . . . . 12
⊢ 0 ≤
1 |
40 | 39 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 0 ≤
1) |
41 | 3 | nn0ge0d 12136 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 0 ≤
𝑎) |
42 | 2, 4, 40, 41 | le2sqd 13809 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → (1 ≤
𝑎 ↔ (1↑2) ≤
(𝑎↑2))) |
43 | 38, 42 | mpbird 260 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 1 ≤
𝑎) |
44 | 8, 9 | sqrtge0d 14967 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 0 ≤
(√‘𝐷)) |
45 | 11 | nn0ge0d 12136 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 0 ≤
𝑏) |
46 | 10, 12, 44, 45 | mulge0d 11392 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 0 ≤
((√‘𝐷) ·
𝑏)) |
47 | 4, 13 | addge01d 11403 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → (0 ≤
((√‘𝐷) ·
𝑏) ↔ 𝑎 ≤ (𝑎 + ((√‘𝐷) · 𝑏)))) |
48 | 46, 47 | mpbid 235 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ ((𝑎↑2) −
(𝐷 · (𝑏↑2))) = 1) → 𝑎 ≤ (𝑎 + ((√‘𝐷) · 𝑏))) |
49 | 2, 4, 14, 43, 48 | letrd 10972 |
. . . . . . . 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 5071 |
. . . . . 6
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 1 ≤ 𝐴) |
53 | 52 | ex 416 |
. . . . 5
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0))
→ ((𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 1 ≤ 𝐴)) |
54 | 53 | rexlimdvva 3206 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) → (∃𝑎 ∈ ℕ0
∃𝑏 ∈
ℕ0 (𝐴 =
(𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 1 ≤ 𝐴)) |
55 | 54 | expimpd 457 |
. . 3
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → ((𝐴 ∈ ℝ ∧ ∃𝑎 ∈ ℕ0
∃𝑏 ∈
ℕ0 (𝐴 =
(𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 1 ≤ 𝐴)) |
56 | 1, 55 | sylbid 243 |
. 2
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (𝐴 ∈ (Pell1QR‘𝐷) → 1 ≤ 𝐴)) |
57 | 56 | imp 410 |
1
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell1QR‘𝐷)) → 1 ≤ 𝐴) |