Step | Hyp | Ref
| Expression |
1 | | cfwddifn 34798 |
. 2
class
โณn |
2 | | vn |
. . 3
setvar ๐ |
3 | | vf |
. . 3
setvar ๐ |
4 | | cn0 12421 |
. . 3
class
โ0 |
5 | | cc 11057 |
. . . 4
class
โ |
6 | | cpm 8772 |
. . . 4
class
โpm |
7 | 5, 5, 6 | co 7361 |
. . 3
class (โ
โpm โ) |
8 | | vx |
. . . 4
setvar ๐ฅ |
9 | | vy |
. . . . . . . . 9
setvar ๐ฆ |
10 | 9 | cv 1541 |
. . . . . . . 8
class ๐ฆ |
11 | | vk |
. . . . . . . . 9
setvar ๐ |
12 | 11 | cv 1541 |
. . . . . . . 8
class ๐ |
13 | | caddc 11062 |
. . . . . . . 8
class
+ |
14 | 10, 12, 13 | co 7361 |
. . . . . . 7
class (๐ฆ + ๐) |
15 | 3 | cv 1541 |
. . . . . . . 8
class ๐ |
16 | 15 | cdm 5637 |
. . . . . . 7
class dom ๐ |
17 | 14, 16 | wcel 2107 |
. . . . . 6
wff (๐ฆ + ๐) โ dom ๐ |
18 | | cc0 11059 |
. . . . . . 7
class
0 |
19 | 2 | cv 1541 |
. . . . . . 7
class ๐ |
20 | | cfz 13433 |
. . . . . . 7
class
... |
21 | 18, 19, 20 | co 7361 |
. . . . . 6
class
(0...๐) |
22 | 17, 11, 21 | wral 3061 |
. . . . 5
wff
โ๐ โ
(0...๐)(๐ฆ + ๐) โ dom ๐ |
23 | 22, 9, 5 | crab 3406 |
. . . 4
class {๐ฆ โ โ โฃ
โ๐ โ (0...๐)(๐ฆ + ๐) โ dom ๐} |
24 | | cbc 14211 |
. . . . . . 7
class
C |
25 | 19, 12, 24 | co 7361 |
. . . . . 6
class (๐C๐) |
26 | | c1 11060 |
. . . . . . . . 9
class
1 |
27 | 26 | cneg 11394 |
. . . . . . . 8
class
-1 |
28 | | cmin 11393 |
. . . . . . . . 9
class
โ |
29 | 19, 12, 28 | co 7361 |
. . . . . . . 8
class (๐ โ ๐) |
30 | | cexp 13976 |
. . . . . . . 8
class
โ |
31 | 27, 29, 30 | co 7361 |
. . . . . . 7
class
(-1โ(๐ โ
๐)) |
32 | 8 | cv 1541 |
. . . . . . . . 9
class ๐ฅ |
33 | 32, 12, 13 | co 7361 |
. . . . . . . 8
class (๐ฅ + ๐) |
34 | 33, 15 | cfv 6500 |
. . . . . . 7
class (๐โ(๐ฅ + ๐)) |
35 | | cmul 11064 |
. . . . . . 7
class
ยท |
36 | 31, 34, 35 | co 7361 |
. . . . . 6
class
((-1โ(๐ โ
๐)) ยท (๐โ(๐ฅ + ๐))) |
37 | 25, 36, 35 | co 7361 |
. . . . 5
class ((๐C๐) ยท ((-1โ(๐ โ ๐)) ยท (๐โ(๐ฅ + ๐)))) |
38 | 21, 37, 11 | csu 15579 |
. . . 4
class
ฮฃ๐ โ
(0...๐)((๐C๐) ยท ((-1โ(๐ โ ๐)) ยท (๐โ(๐ฅ + ๐)))) |
39 | 8, 23, 38 | cmpt 5192 |
. . 3
class (๐ฅ โ {๐ฆ โ โ โฃ โ๐ โ (0...๐)(๐ฆ + ๐) โ dom ๐} โฆ ฮฃ๐ โ (0...๐)((๐C๐) ยท ((-1โ(๐ โ ๐)) ยท (๐โ(๐ฅ + ๐))))) |
40 | 2, 3, 4, 7, 39 | cmpo 7363 |
. 2
class (๐ โ โ0,
๐ โ (โ
โpm โ) โฆ (๐ฅ โ {๐ฆ โ โ โฃ โ๐ โ (0...๐)(๐ฆ + ๐) โ dom ๐} โฆ ฮฃ๐ โ (0...๐)((๐C๐) ยท ((-1โ(๐ โ ๐)) ยท (๐โ(๐ฅ + ๐)))))) |
41 | 1, 40 | wceq 1542 |
1
wff
โณn = (๐ โ โ0, ๐ โ (โ
โpm โ) โฆ (๐ฅ โ {๐ฆ โ โ โฃ โ๐ โ (0...๐)(๐ฆ + ๐) โ dom ๐} โฆ ฮฃ๐ โ (0...๐)((๐C๐) ยท ((-1โ(๐ โ ๐)) ยท (๐โ(๐ฅ + ๐)))))) |