Detailed syntax breakdown of Definition df-pell1qr
Step | Hyp | Ref
| Expression |
1 | | cpell1qr 40362 |
. 2
class
Pell1QR |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cn 11830 |
. . . 4
class
ℕ |
4 | | csquarenn 40361 |
. . . 4
class
◻NN |
5 | 3, 4 | cdif 3863 |
. . 3
class (ℕ
∖ ◻NN) |
6 | | vy |
. . . . . . . . 9
setvar 𝑦 |
7 | 6 | cv 1542 |
. . . . . . . 8
class 𝑦 |
8 | | vz |
. . . . . . . . . 10
setvar 𝑧 |
9 | 8 | cv 1542 |
. . . . . . . . 9
class 𝑧 |
10 | 2 | cv 1542 |
. . . . . . . . . . 11
class 𝑥 |
11 | | csqrt 14796 |
. . . . . . . . . . 11
class
√ |
12 | 10, 11 | cfv 6380 |
. . . . . . . . . 10
class
(√‘𝑥) |
13 | | vw |
. . . . . . . . . . 11
setvar 𝑤 |
14 | 13 | cv 1542 |
. . . . . . . . . 10
class 𝑤 |
15 | | cmul 10734 |
. . . . . . . . . 10
class
· |
16 | 12, 14, 15 | co 7213 |
. . . . . . . . 9
class
((√‘𝑥)
· 𝑤) |
17 | | caddc 10732 |
. . . . . . . . 9
class
+ |
18 | 9, 16, 17 | co 7213 |
. . . . . . . 8
class (𝑧 + ((√‘𝑥) · 𝑤)) |
19 | 7, 18 | wceq 1543 |
. . . . . . 7
wff 𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) |
20 | | c2 11885 |
. . . . . . . . . 10
class
2 |
21 | | cexp 13635 |
. . . . . . . . . 10
class
↑ |
22 | 9, 20, 21 | co 7213 |
. . . . . . . . 9
class (𝑧↑2) |
23 | 14, 20, 21 | co 7213 |
. . . . . . . . . 10
class (𝑤↑2) |
24 | 10, 23, 15 | co 7213 |
. . . . . . . . 9
class (𝑥 · (𝑤↑2)) |
25 | | cmin 11062 |
. . . . . . . . 9
class
− |
26 | 22, 24, 25 | co 7213 |
. . . . . . . 8
class ((𝑧↑2) − (𝑥 · (𝑤↑2))) |
27 | | c1 10730 |
. . . . . . . 8
class
1 |
28 | 26, 27 | wceq 1543 |
. . . . . . 7
wff ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1 |
29 | 19, 28 | wa 399 |
. . . . . 6
wff (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1) |
30 | | cn0 12090 |
. . . . . 6
class
ℕ0 |
31 | 29, 13, 30 | wrex 3062 |
. . . . 5
wff
∃𝑤 ∈
ℕ0 (𝑦 =
(𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1) |
32 | 31, 8, 30 | wrex 3062 |
. . . 4
wff
∃𝑧 ∈
ℕ0 ∃𝑤 ∈ ℕ0 (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1) |
33 | | cr 10728 |
. . . 4
class
ℝ |
34 | 32, 6, 33 | crab 3065 |
. . 3
class {𝑦 ∈ ℝ ∣
∃𝑧 ∈
ℕ0 ∃𝑤 ∈ ℕ0 (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)} |
35 | 2, 5, 34 | cmpt 5135 |
. 2
class (𝑥 ∈ (ℕ ∖
◻NN) ↦ {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0
∃𝑤 ∈
ℕ0 (𝑦 =
(𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)}) |
36 | 1, 35 | wceq 1543 |
1
wff Pell1QR =
(𝑥 ∈ (ℕ ∖
◻NN) ↦ {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0
∃𝑤 ∈
ℕ0 (𝑦 =
(𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)}) |