Step | Hyp | Ref
| Expression |
1 | | etransclem26.d |
. . . . . . . . . 10
โข (๐ โ ๐ท โ (๐ถโ๐)) |
2 | | etransclem26.c |
. . . . . . . . . . 11
โข ๐ถ = (๐ โ โ0 โฆ {๐ โ ((0...๐) โm (0...๐)) โฃ ฮฃ๐ โ (0...๐)(๐โ๐) = ๐}) |
3 | | etransclem26.n |
. . . . . . . . . . 11
โข (๐ โ ๐ โ
โ0) |
4 | 2, 3 | etransclem12 45261 |
. . . . . . . . . 10
โข (๐ โ (๐ถโ๐) = {๐ โ ((0...๐) โm (0...๐)) โฃ ฮฃ๐ โ (0...๐)(๐โ๐) = ๐}) |
5 | 1, 4 | eleqtrd 2834 |
. . . . . . . . 9
โข (๐ โ ๐ท โ {๐ โ ((0...๐) โm (0...๐)) โฃ ฮฃ๐ โ (0...๐)(๐โ๐) = ๐}) |
6 | | fveq1 6890 |
. . . . . . . . . . . 12
โข (๐ = ๐ท โ (๐โ๐) = (๐ทโ๐)) |
7 | 6 | sumeq2sdv 15655 |
. . . . . . . . . . 11
โข (๐ = ๐ท โ ฮฃ๐ โ (0...๐)(๐โ๐) = ฮฃ๐ โ (0...๐)(๐ทโ๐)) |
8 | 7 | eqeq1d 2733 |
. . . . . . . . . 10
โข (๐ = ๐ท โ (ฮฃ๐ โ (0...๐)(๐โ๐) = ๐ โ ฮฃ๐ โ (0...๐)(๐ทโ๐) = ๐)) |
9 | 8 | elrab 3683 |
. . . . . . . . 9
โข (๐ท โ {๐ โ ((0...๐) โm (0...๐)) โฃ ฮฃ๐ โ (0...๐)(๐โ๐) = ๐} โ (๐ท โ ((0...๐) โm (0...๐)) โง ฮฃ๐ โ (0...๐)(๐ทโ๐) = ๐)) |
10 | 5, 9 | sylib 217 |
. . . . . . . 8
โข (๐ โ (๐ท โ ((0...๐) โm (0...๐)) โง ฮฃ๐ โ (0...๐)(๐ทโ๐) = ๐)) |
11 | 10 | simprd 495 |
. . . . . . 7
โข (๐ โ ฮฃ๐ โ (0...๐)(๐ทโ๐) = ๐) |
12 | 11 | eqcomd 2737 |
. . . . . 6
โข (๐ โ ๐ = ฮฃ๐ โ (0...๐)(๐ทโ๐)) |
13 | 12 | fveq2d 6895 |
. . . . 5
โข (๐ โ (!โ๐) = (!โฮฃ๐ โ (0...๐)(๐ทโ๐))) |
14 | 13 | oveq1d 7427 |
. . . 4
โข (๐ โ ((!โ๐) / โ๐ โ (0...๐)(!โ(๐ทโ๐))) = ((!โฮฃ๐ โ (0...๐)(๐ทโ๐)) / โ๐ โ (0...๐)(!โ(๐ทโ๐)))) |
15 | | nfcv 2902 |
. . . . 5
โข
โฒ๐๐ท |
16 | | fzfid 13943 |
. . . . 5
โข (๐ โ (0...๐) โ Fin) |
17 | | nn0ex 12483 |
. . . . . . 7
โข
โ0 โ V |
18 | | fzssnn0 44326 |
. . . . . . 7
โข
(0...๐) โ
โ0 |
19 | | mapss 8887 |
. . . . . . 7
โข
((โ0 โ V โง (0...๐) โ โ0) โ
((0...๐) โm
(0...๐)) โ
(โ0 โm (0...๐))) |
20 | 17, 18, 19 | mp2an 689 |
. . . . . 6
โข
((0...๐)
โm (0...๐))
โ (โ0 โm (0...๐)) |
21 | 10 | simpld 494 |
. . . . . 6
โข (๐ โ ๐ท โ ((0...๐) โm (0...๐))) |
22 | 20, 21 | sselid 3980 |
. . . . 5
โข (๐ โ ๐ท โ (โ0
โm (0...๐))) |
23 | 15, 16, 22 | mccl 44613 |
. . . 4
โข (๐ โ ((!โฮฃ๐ โ (0...๐)(๐ทโ๐)) / โ๐ โ (0...๐)(!โ(๐ทโ๐))) โ โ) |
24 | 14, 23 | eqeltrd 2832 |
. . 3
โข (๐ โ ((!โ๐) / โ๐ โ (0...๐)(!โ(๐ทโ๐))) โ โ) |
25 | 24 | nnzd 12590 |
. 2
โข (๐ โ ((!โ๐) / โ๐ โ (0...๐)(!โ(๐ทโ๐))) โ โค) |
26 | | etransclem26.p |
. . . 4
โข (๐ โ ๐ โ โ) |
27 | | etransclem26.m |
. . . 4
โข (๐ โ ๐ โ
โ0) |
28 | | elmapi 8847 |
. . . . 5
โข (๐ท โ ((0...๐) โm (0...๐)) โ ๐ท:(0...๐)โถ(0...๐)) |
29 | 21, 28 | syl 17 |
. . . 4
โข (๐ โ ๐ท:(0...๐)โถ(0...๐)) |
30 | | etransclem26.jz |
. . . 4
โข (๐ โ ๐ฝ โ โค) |
31 | 26, 27, 29, 30 | etransclem10 45259 |
. . 3
โข (๐ โ if((๐ โ 1) < (๐ทโ0), 0, (((!โ(๐ โ 1)) / (!โ((๐ โ 1) โ (๐ทโ0)))) ยท (๐ฝโ((๐ โ 1) โ (๐ทโ0))))) โ
โค) |
32 | | fzfid 13943 |
. . . 4
โข (๐ โ (1...๐) โ Fin) |
33 | 26 | adantr 480 |
. . . . 5
โข ((๐ โง ๐ โ (1...๐)) โ ๐ โ โ) |
34 | 29 | adantr 480 |
. . . . 5
โข ((๐ โง ๐ โ (1...๐)) โ ๐ท:(0...๐)โถ(0...๐)) |
35 | | 0z 12574 |
. . . . . . . 8
โข 0 โ
โค |
36 | | fzp1ss 13557 |
. . . . . . . 8
โข (0 โ
โค โ ((0 + 1)...๐) โ (0...๐)) |
37 | 35, 36 | ax-mp 5 |
. . . . . . 7
โข ((0 +
1)...๐) โ (0...๐) |
38 | | 1e0p1 12724 |
. . . . . . . . . 10
โข 1 = (0 +
1) |
39 | 38 | oveq1i 7422 |
. . . . . . . . 9
โข
(1...๐) = ((0 +
1)...๐) |
40 | 39 | eleq2i 2824 |
. . . . . . . 8
โข (๐ โ (1...๐) โ ๐ โ ((0 + 1)...๐)) |
41 | 40 | biimpi 215 |
. . . . . . 7
โข (๐ โ (1...๐) โ ๐ โ ((0 + 1)...๐)) |
42 | 37, 41 | sselid 3980 |
. . . . . 6
โข (๐ โ (1...๐) โ ๐ โ (0...๐)) |
43 | 42 | adantl 481 |
. . . . 5
โข ((๐ โง ๐ โ (1...๐)) โ ๐ โ (0...๐)) |
44 | 30 | adantr 480 |
. . . . 5
โข ((๐ โง ๐ โ (1...๐)) โ ๐ฝ โ โค) |
45 | 33, 34, 43, 44 | etransclem3 45252 |
. . . 4
โข ((๐ โง ๐ โ (1...๐)) โ if(๐ < (๐ทโ๐), 0, (((!โ๐) / (!โ(๐ โ (๐ทโ๐)))) ยท ((๐ฝ โ ๐)โ(๐ โ (๐ทโ๐))))) โ โค) |
46 | 32, 45 | fprodzcl 15903 |
. . 3
โข (๐ โ โ๐ โ (1...๐)if(๐ < (๐ทโ๐), 0, (((!โ๐) / (!โ(๐ โ (๐ทโ๐)))) ยท ((๐ฝ โ ๐)โ(๐ โ (๐ทโ๐))))) โ โค) |
47 | 31, 46 | zmulcld 12677 |
. 2
โข (๐ โ (if((๐ โ 1) < (๐ทโ0), 0, (((!โ(๐ โ 1)) / (!โ((๐ โ 1) โ (๐ทโ0)))) ยท (๐ฝโ((๐ โ 1) โ (๐ทโ0))))) ยท โ๐ โ (1...๐)if(๐ < (๐ทโ๐), 0, (((!โ๐) / (!โ(๐ โ (๐ทโ๐)))) ยท ((๐ฝ โ ๐)โ(๐ โ (๐ทโ๐)))))) โ โค) |
48 | 25, 47 | zmulcld 12677 |
1
โข (๐ โ (((!โ๐) / โ๐ โ (0...๐)(!โ(๐ทโ๐))) ยท (if((๐ โ 1) < (๐ทโ0), 0, (((!โ(๐ โ 1)) / (!โ((๐ โ 1) โ (๐ทโ0)))) ยท (๐ฝโ((๐ โ 1) โ (๐ทโ0))))) ยท โ๐ โ (1...๐)if(๐ < (๐ทโ๐), 0, (((!โ๐) / (!โ(๐ โ (๐ทโ๐)))) ยท ((๐ฝ โ ๐)โ(๐ โ (๐ทโ๐))))))) โ โค) |