Detailed syntax breakdown of Definition df-pell1234qr
Step | Hyp | Ref
| Expression |
1 | | cpell1234qr 40657 |
. 2
class
Pell1234QR |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cn 11973 |
. . . 4
class
ℕ |
4 | | csquarenn 40655 |
. . . 4
class
◻NN |
5 | 3, 4 | cdif 3889 |
. . 3
class (ℕ
∖ ◻NN) |
6 | | vy |
. . . . . . . . 9
setvar 𝑦 |
7 | 6 | cv 1541 |
. . . . . . . 8
class 𝑦 |
8 | | vz |
. . . . . . . . . 10
setvar 𝑧 |
9 | 8 | cv 1541 |
. . . . . . . . 9
class 𝑧 |
10 | 2 | cv 1541 |
. . . . . . . . . . 11
class 𝑥 |
11 | | csqrt 14942 |
. . . . . . . . . . 11
class
√ |
12 | 10, 11 | cfv 6432 |
. . . . . . . . . 10
class
(√‘𝑥) |
13 | | vw |
. . . . . . . . . . 11
setvar 𝑤 |
14 | 13 | cv 1541 |
. . . . . . . . . 10
class 𝑤 |
15 | | cmul 10877 |
. . . . . . . . . 10
class
· |
16 | 12, 14, 15 | co 7271 |
. . . . . . . . 9
class
((√‘𝑥)
· 𝑤) |
17 | | caddc 10875 |
. . . . . . . . 9
class
+ |
18 | 9, 16, 17 | co 7271 |
. . . . . . . 8
class (𝑧 + ((√‘𝑥) · 𝑤)) |
19 | 7, 18 | wceq 1542 |
. . . . . . 7
wff 𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) |
20 | | c2 12028 |
. . . . . . . . . 10
class
2 |
21 | | cexp 13780 |
. . . . . . . . . 10
class
↑ |
22 | 9, 20, 21 | co 7271 |
. . . . . . . . 9
class (𝑧↑2) |
23 | 14, 20, 21 | co 7271 |
. . . . . . . . . 10
class (𝑤↑2) |
24 | 10, 23, 15 | co 7271 |
. . . . . . . . 9
class (𝑥 · (𝑤↑2)) |
25 | | cmin 11205 |
. . . . . . . . 9
class
− |
26 | 22, 24, 25 | co 7271 |
. . . . . . . 8
class ((𝑧↑2) − (𝑥 · (𝑤↑2))) |
27 | | c1 10873 |
. . . . . . . 8
class
1 |
28 | 26, 27 | wceq 1542 |
. . . . . . 7
wff ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1 |
29 | 19, 28 | wa 396 |
. . . . . 6
wff (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1) |
30 | | cz 12319 |
. . . . . 6
class
ℤ |
31 | 29, 13, 30 | wrex 3067 |
. . . . 5
wff
∃𝑤 ∈
ℤ (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1) |
32 | 31, 8, 30 | wrex 3067 |
. . . 4
wff
∃𝑧 ∈
ℤ ∃𝑤 ∈
ℤ (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1) |
33 | | cr 10871 |
. . . 4
class
ℝ |
34 | 32, 6, 33 | crab 3070 |
. . 3
class {𝑦 ∈ ℝ ∣
∃𝑧 ∈ ℤ
∃𝑤 ∈ ℤ
(𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)} |
35 | 2, 5, 34 | cmpt 5162 |
. 2
class (𝑥 ∈ (ℕ ∖
◻NN) ↦ {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)}) |
36 | 1, 35 | wceq 1542 |
1
wff Pell1234QR
= (𝑥 ∈ (ℕ
∖ ◻NN) ↦ {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)}) |