Step | Hyp | Ref
| Expression |
1 | | cpell1234qr 41208 |
. 2
class
Pell1234QR |
2 | | vx |
. . 3
setvar ๐ฅ |
3 | | cn 12161 |
. . . 4
class
โ |
4 | | csquarenn 41206 |
. . . 4
class
โปNN |
5 | 3, 4 | cdif 3911 |
. . 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 15127 |
. . . . . . . . . . 11
class
โ |
12 | 10, 11 | cfv 6500 |
. . . . . . . . . 10
class
(โโ๐ฅ) |
13 | | vw |
. . . . . . . . . . 11
setvar ๐ค |
14 | 13 | cv 1541 |
. . . . . . . . . 10
class ๐ค |
15 | | cmul 11064 |
. . . . . . . . . 10
class
ยท |
16 | 12, 14, 15 | co 7361 |
. . . . . . . . 9
class
((โโ๐ฅ)
ยท ๐ค) |
17 | | caddc 11062 |
. . . . . . . . 9
class
+ |
18 | 9, 16, 17 | co 7361 |
. . . . . . . 8
class (๐ง + ((โโ๐ฅ) ยท ๐ค)) |
19 | 7, 18 | wceq 1542 |
. . . . . . 7
wff ๐ฆ = (๐ง + ((โโ๐ฅ) ยท ๐ค)) |
20 | | c2 12216 |
. . . . . . . . . 10
class
2 |
21 | | cexp 13976 |
. . . . . . . . . 10
class
โ |
22 | 9, 20, 21 | co 7361 |
. . . . . . . . 9
class (๐งโ2) |
23 | 14, 20, 21 | co 7361 |
. . . . . . . . . 10
class (๐คโ2) |
24 | 10, 23, 15 | co 7361 |
. . . . . . . . 9
class (๐ฅ ยท (๐คโ2)) |
25 | | cmin 11393 |
. . . . . . . . 9
class
โ |
26 | 22, 24, 25 | co 7361 |
. . . . . . . 8
class ((๐งโ2) โ (๐ฅ ยท (๐คโ2))) |
27 | | c1 11060 |
. . . . . . . 8
class
1 |
28 | 26, 27 | wceq 1542 |
. . . . . . 7
wff ((๐งโ2) โ (๐ฅ ยท (๐คโ2))) = 1 |
29 | 19, 28 | wa 397 |
. . . . . 6
wff (๐ฆ = (๐ง + ((โโ๐ฅ) ยท ๐ค)) โง ((๐งโ2) โ (๐ฅ ยท (๐คโ2))) = 1) |
30 | | cz 12507 |
. . . . . 6
class
โค |
31 | 29, 13, 30 | wrex 3070 |
. . . . 5
wff
โ๐ค โ
โค (๐ฆ = (๐ง + ((โโ๐ฅ) ยท ๐ค)) โง ((๐งโ2) โ (๐ฅ ยท (๐คโ2))) = 1) |
32 | 31, 8, 30 | wrex 3070 |
. . . 4
wff
โ๐ง โ
โค โ๐ค โ
โค (๐ฆ = (๐ง + ((โโ๐ฅ) ยท ๐ค)) โง ((๐งโ2) โ (๐ฅ ยท (๐คโ2))) = 1) |
33 | | cr 11058 |
. . . 4
class
โ |
34 | 32, 6, 33 | crab 3406 |
. . 3
class {๐ฆ โ โ โฃ
โ๐ง โ โค
โ๐ค โ โค
(๐ฆ = (๐ง + ((โโ๐ฅ) ยท ๐ค)) โง ((๐งโ2) โ (๐ฅ ยท (๐คโ2))) = 1)} |
35 | 2, 5, 34 | cmpt 5192 |
. 2
class (๐ฅ โ (โ โ
โปNN) โฆ {๐ฆ โ โ โฃ โ๐ง โ โค โ๐ค โ โค (๐ฆ = (๐ง + ((โโ๐ฅ) ยท ๐ค)) โง ((๐งโ2) โ (๐ฅ ยท (๐คโ2))) = 1)}) |
36 | 1, 35 | wceq 1542 |
1
wff Pell1234QR
= (๐ฅ โ (โ
โ โปNN) โฆ {๐ฆ โ โ โฃ โ๐ง โ โค โ๐ค โ โค (๐ฆ = (๐ง + ((โโ๐ฅ) ยท ๐ค)) โง ((๐งโ2) โ (๐ฅ ยท (๐คโ2))) = 1)}) |