Step | Hyp | Ref
| Expression |
1 | | cpell1qr 41251 |
. 2
class
Pell1QR |
2 | | vx |
. . 3
setvar ๐ฅ |
3 | | cn 12177 |
. . . 4
class
โ |
4 | | csquarenn 41250 |
. . . 4
class
โปNN |
5 | 3, 4 | cdif 3925 |
. . 3
class (โ
โ โปNN) |
6 | | vy |
. . . . . . . . 9
setvar ๐ฆ |
7 | 6 | cv 1540 |
. . . . . . . 8
class ๐ฆ |
8 | | vz |
. . . . . . . . . 10
setvar ๐ง |
9 | 8 | cv 1540 |
. . . . . . . . 9
class ๐ง |
10 | 2 | cv 1540 |
. . . . . . . . . . 11
class ๐ฅ |
11 | | csqrt 15145 |
. . . . . . . . . . 11
class
โ |
12 | 10, 11 | cfv 6516 |
. . . . . . . . . 10
class
(โโ๐ฅ) |
13 | | vw |
. . . . . . . . . . 11
setvar ๐ค |
14 | 13 | cv 1540 |
. . . . . . . . . 10
class ๐ค |
15 | | cmul 11080 |
. . . . . . . . . 10
class
ยท |
16 | 12, 14, 15 | co 7377 |
. . . . . . . . 9
class
((โโ๐ฅ)
ยท ๐ค) |
17 | | caddc 11078 |
. . . . . . . . 9
class
+ |
18 | 9, 16, 17 | co 7377 |
. . . . . . . 8
class (๐ง + ((โโ๐ฅ) ยท ๐ค)) |
19 | 7, 18 | wceq 1541 |
. . . . . . 7
wff ๐ฆ = (๐ง + ((โโ๐ฅ) ยท ๐ค)) |
20 | | c2 12232 |
. . . . . . . . . 10
class
2 |
21 | | cexp 13992 |
. . . . . . . . . 10
class
โ |
22 | 9, 20, 21 | co 7377 |
. . . . . . . . 9
class (๐งโ2) |
23 | 14, 20, 21 | co 7377 |
. . . . . . . . . 10
class (๐คโ2) |
24 | 10, 23, 15 | co 7377 |
. . . . . . . . 9
class (๐ฅ ยท (๐คโ2)) |
25 | | cmin 11409 |
. . . . . . . . 9
class
โ |
26 | 22, 24, 25 | co 7377 |
. . . . . . . 8
class ((๐งโ2) โ (๐ฅ ยท (๐คโ2))) |
27 | | c1 11076 |
. . . . . . . 8
class
1 |
28 | 26, 27 | wceq 1541 |
. . . . . . 7
wff ((๐งโ2) โ (๐ฅ ยท (๐คโ2))) = 1 |
29 | 19, 28 | wa 396 |
. . . . . 6
wff (๐ฆ = (๐ง + ((โโ๐ฅ) ยท ๐ค)) โง ((๐งโ2) โ (๐ฅ ยท (๐คโ2))) = 1) |
30 | | cn0 12437 |
. . . . . 6
class
โ0 |
31 | 29, 13, 30 | wrex 3069 |
. . . . 5
wff
โ๐ค โ
โ0 (๐ฆ =
(๐ง + ((โโ๐ฅ) ยท ๐ค)) โง ((๐งโ2) โ (๐ฅ ยท (๐คโ2))) = 1) |
32 | 31, 8, 30 | wrex 3069 |
. . . 4
wff
โ๐ง โ
โ0 โ๐ค โ โ0 (๐ฆ = (๐ง + ((โโ๐ฅ) ยท ๐ค)) โง ((๐งโ2) โ (๐ฅ ยท (๐คโ2))) = 1) |
33 | | cr 11074 |
. . . 4
class
โ |
34 | 32, 6, 33 | crab 3418 |
. . 3
class {๐ฆ โ โ โฃ
โ๐ง โ
โ0 โ๐ค โ โ0 (๐ฆ = (๐ง + ((โโ๐ฅ) ยท ๐ค)) โง ((๐งโ2) โ (๐ฅ ยท (๐คโ2))) = 1)} |
35 | 2, 5, 34 | cmpt 5208 |
. 2
class (๐ฅ โ (โ โ
โปNN) โฆ {๐ฆ โ โ โฃ โ๐ง โ โ0
โ๐ค โ
โ0 (๐ฆ =
(๐ง + ((โโ๐ฅ) ยท ๐ค)) โง ((๐งโ2) โ (๐ฅ ยท (๐คโ2))) = 1)}) |
36 | 1, 35 | wceq 1541 |
1
wff Pell1QR =
(๐ฅ โ (โ โ
โปNN) โฆ {๐ฆ โ โ โฃ โ๐ง โ โ0
โ๐ค โ
โ0 (๐ฆ =
(๐ง + ((โโ๐ฅ) ยท ๐ค)) โง ((๐งโ2) โ (๐ฅ ยท (๐คโ2))) = 1)}) |