Step | Hyp | Ref
| Expression |
1 | | ctayl 25728 |
. 2
class
Tayl |
2 | | vs |
. . 3
setvar ๐ |
3 | | vf |
. . 3
setvar ๐ |
4 | | cr 11057 |
. . . 4
class
โ |
5 | | cc 11056 |
. . . 4
class
โ |
6 | 4, 5 | cpr 4593 |
. . 3
class {โ,
โ} |
7 | 2 | cv 1541 |
. . . 4
class ๐ |
8 | | cpm 8773 |
. . . 4
class
โpm |
9 | 5, 7, 8 | co 7362 |
. . 3
class (โ
โpm ๐ ) |
10 | | vn |
. . . 4
setvar ๐ |
11 | | va |
. . . 4
setvar ๐ |
12 | | cn0 12420 |
. . . . 5
class
โ0 |
13 | | cpnf 11193 |
. . . . . 6
class
+โ |
14 | 13 | csn 4591 |
. . . . 5
class
{+โ} |
15 | 12, 14 | cun 3913 |
. . . 4
class
(โ0 โช {+โ}) |
16 | | vk |
. . . . 5
setvar ๐ |
17 | | cc0 11058 |
. . . . . . 7
class
0 |
18 | 10 | cv 1541 |
. . . . . . 7
class ๐ |
19 | | cicc 13274 |
. . . . . . 7
class
[,] |
20 | 17, 18, 19 | co 7362 |
. . . . . 6
class
(0[,]๐) |
21 | | cz 12506 |
. . . . . 6
class
โค |
22 | 20, 21 | cin 3914 |
. . . . 5
class
((0[,]๐) โฉ
โค) |
23 | 16 | cv 1541 |
. . . . . . 7
class ๐ |
24 | 3 | cv 1541 |
. . . . . . . 8
class ๐ |
25 | | cdvn 25244 |
. . . . . . . 8
class
D๐ |
26 | 7, 24, 25 | co 7362 |
. . . . . . 7
class (๐ D๐ ๐) |
27 | 23, 26 | cfv 6501 |
. . . . . 6
class ((๐ D๐ ๐)โ๐) |
28 | 27 | cdm 5638 |
. . . . 5
class dom
((๐ D๐
๐)โ๐) |
29 | 16, 22, 28 | ciin 4960 |
. . . 4
class โฉ ๐ โ ((0[,]๐) โฉ โค)dom ((๐ D๐ ๐)โ๐) |
30 | | vx |
. . . . 5
setvar ๐ฅ |
31 | 30 | cv 1541 |
. . . . . . 7
class ๐ฅ |
32 | 31 | csn 4591 |
. . . . . 6
class {๐ฅ} |
33 | | ccnfld 20812 |
. . . . . . 7
class
โfld |
34 | 11 | cv 1541 |
. . . . . . . . . . 11
class ๐ |
35 | 34, 27 | cfv 6501 |
. . . . . . . . . 10
class (((๐ D๐ ๐)โ๐)โ๐) |
36 | | cfa 14180 |
. . . . . . . . . . 11
class
! |
37 | 23, 36 | cfv 6501 |
. . . . . . . . . 10
class
(!โ๐) |
38 | | cdiv 11819 |
. . . . . . . . . 10
class
/ |
39 | 35, 37, 38 | co 7362 |
. . . . . . . . 9
class ((((๐ D๐ ๐)โ๐)โ๐) / (!โ๐)) |
40 | | cmin 11392 |
. . . . . . . . . . 11
class
โ |
41 | 31, 34, 40 | co 7362 |
. . . . . . . . . 10
class (๐ฅ โ ๐) |
42 | | cexp 13974 |
. . . . . . . . . 10
class
โ |
43 | 41, 23, 42 | co 7362 |
. . . . . . . . 9
class ((๐ฅ โ ๐)โ๐) |
44 | | cmul 11063 |
. . . . . . . . 9
class
ยท |
45 | 39, 43, 44 | co 7362 |
. . . . . . . 8
class
(((((๐
D๐ ๐)โ๐)โ๐) / (!โ๐)) ยท ((๐ฅ โ ๐)โ๐)) |
46 | 16, 22, 45 | cmpt 5193 |
. . . . . . 7
class (๐ โ ((0[,]๐) โฉ โค) โฆ (((((๐ D๐ ๐)โ๐)โ๐) / (!โ๐)) ยท ((๐ฅ โ ๐)โ๐))) |
47 | | ctsu 23493 |
. . . . . . 7
class
tsums |
48 | 33, 46, 47 | co 7362 |
. . . . . 6
class
(โfld tsums (๐ โ ((0[,]๐) โฉ โค) โฆ (((((๐ D๐ ๐)โ๐)โ๐) / (!โ๐)) ยท ((๐ฅ โ ๐)โ๐)))) |
49 | 32, 48 | cxp 5636 |
. . . . 5
class ({๐ฅ} ร (โfld
tsums (๐ โ ((0[,]๐) โฉ โค) โฆ
(((((๐
D๐ ๐)โ๐)โ๐) / (!โ๐)) ยท ((๐ฅ โ ๐)โ๐))))) |
50 | 30, 5, 49 | ciun 4959 |
. . . 4
class โช ๐ฅ โ โ ({๐ฅ} ร (โfld tsums (๐ โ ((0[,]๐) โฉ โค) โฆ (((((๐ D๐ ๐)โ๐)โ๐) / (!โ๐)) ยท ((๐ฅ โ ๐)โ๐))))) |
51 | 10, 11, 15, 29, 50 | cmpo 7364 |
. . 3
class (๐ โ (โ0
โช {+โ}), ๐ โ
โฉ ๐ โ ((0[,]๐) โฉ โค)dom ((๐ D๐ ๐)โ๐) โฆ โช
๐ฅ โ โ ({๐ฅ} ร (โfld
tsums (๐ โ ((0[,]๐) โฉ โค) โฆ
(((((๐
D๐ ๐)โ๐)โ๐) / (!โ๐)) ยท ((๐ฅ โ ๐)โ๐)))))) |
52 | 2, 3, 6, 9, 51 | cmpo 7364 |
. 2
class (๐ โ {โ, โ},
๐ โ (โ
โpm ๐ )
โฆ (๐ โ
(โ0 โช {+โ}), ๐ โ โฉ
๐ โ ((0[,]๐) โฉ โค)dom ((๐ D๐ ๐)โ๐) โฆ โช
๐ฅ โ โ ({๐ฅ} ร (โfld
tsums (๐ โ ((0[,]๐) โฉ โค) โฆ
(((((๐
D๐ ๐)โ๐)โ๐) / (!โ๐)) ยท ((๐ฅ โ ๐)โ๐))))))) |
53 | 1, 52 | wceq 1542 |
1
wff Tayl =
(๐ โ {โ,
โ}, ๐ โ (โ
โpm ๐ )
โฆ (๐ โ
(โ0 โช {+โ}), ๐ โ โฉ
๐ โ ((0[,]๐) โฉ โค)dom ((๐ D๐ ๐)โ๐) โฆ โช
๐ฅ โ โ ({๐ฅ} ร (โfld
tsums (๐ โ ((0[,]๐) โฉ โค) โฆ
(((((๐
D๐ ๐)โ๐)โ๐) / (!โ๐)) ยท ((๐ฅ โ ๐)โ๐))))))) |