Step | Hyp | Ref
| Expression |
1 | | fzfid 13934 |
. 2
โข (๐ โ (1...๐) โ Fin) |
2 | | 0zd 12566 |
. . 3
โข (((๐ โง ๐ โ (1...๐)) โง ๐ < (๐ถโ๐)) โ 0 โ โค) |
3 | | 0zd 12566 |
. . . . . . 7
โข (((๐ โง ๐ โ (1...๐)) โง ยฌ ๐ < (๐ถโ๐)) โ 0 โ โค) |
4 | | etransclem7.n |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
5 | 4 | nnzd 12581 |
. . . . . . . 8
โข (๐ โ ๐ โ โค) |
6 | 5 | ad2antrr 724 |
. . . . . . 7
โข (((๐ โง ๐ โ (1...๐)) โง ยฌ ๐ < (๐ถโ๐)) โ ๐ โ โค) |
7 | 5 | adantr 481 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (1...๐)) โ ๐ โ โค) |
8 | | etransclem7.c |
. . . . . . . . . . . 12
โข (๐ โ ๐ถ:(0...๐)โถ(0...๐)) |
9 | 8 | adantr 481 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (1...๐)) โ ๐ถ:(0...๐)โถ(0...๐)) |
10 | | 0zd 12566 |
. . . . . . . . . . . . . 14
โข (๐ โ (1...๐) โ 0 โ โค) |
11 | | fzp1ss 13548 |
. . . . . . . . . . . . . 14
โข (0 โ
โค โ ((0 + 1)...๐) โ (0...๐)) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ ((0 + 1)...๐) โ (0...๐)) |
13 | | id 22 |
. . . . . . . . . . . . . 14
โข (๐ โ (1...๐) โ ๐ โ (1...๐)) |
14 | | 1e0p1 12715 |
. . . . . . . . . . . . . . 15
โข 1 = (0 +
1) |
15 | 14 | oveq1i 7415 |
. . . . . . . . . . . . . 14
โข
(1...๐) = ((0 +
1)...๐) |
16 | 13, 15 | eleqtrdi 2843 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ ๐ โ ((0 + 1)...๐)) |
17 | 12, 16 | sseldd 3982 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐) โ ๐ โ (0...๐)) |
18 | 17 | adantl 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (1...๐)) โ ๐ โ (0...๐)) |
19 | 9, 18 | ffvelcdmd 7084 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (1...๐)) โ (๐ถโ๐) โ (0...๐)) |
20 | 19 | elfzelzd 13498 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (1...๐)) โ (๐ถโ๐) โ โค) |
21 | 7, 20 | zsubcld 12667 |
. . . . . . . 8
โข ((๐ โง ๐ โ (1...๐)) โ (๐ โ (๐ถโ๐)) โ โค) |
22 | 21 | adantr 481 |
. . . . . . 7
โข (((๐ โง ๐ โ (1...๐)) โง ยฌ ๐ < (๐ถโ๐)) โ (๐ โ (๐ถโ๐)) โ โค) |
23 | 20 | zred 12662 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (1...๐)) โ (๐ถโ๐) โ โ) |
24 | 23 | adantr 481 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (1...๐)) โง ยฌ ๐ < (๐ถโ๐)) โ (๐ถโ๐) โ โ) |
25 | 6 | zred 12662 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (1...๐)) โง ยฌ ๐ < (๐ถโ๐)) โ ๐ โ โ) |
26 | | simpr 485 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (1...๐)) โง ยฌ ๐ < (๐ถโ๐)) โ ยฌ ๐ < (๐ถโ๐)) |
27 | 24, 25, 26 | nltled 11360 |
. . . . . . . 8
โข (((๐ โง ๐ โ (1...๐)) โง ยฌ ๐ < (๐ถโ๐)) โ (๐ถโ๐) โค ๐) |
28 | 25, 24 | subge0d 11800 |
. . . . . . . 8
โข (((๐ โง ๐ โ (1...๐)) โง ยฌ ๐ < (๐ถโ๐)) โ (0 โค (๐ โ (๐ถโ๐)) โ (๐ถโ๐) โค ๐)) |
29 | 27, 28 | mpbird 256 |
. . . . . . 7
โข (((๐ โง ๐ โ (1...๐)) โง ยฌ ๐ < (๐ถโ๐)) โ 0 โค (๐ โ (๐ถโ๐))) |
30 | | elfzle1 13500 |
. . . . . . . . . 10
โข ((๐ถโ๐) โ (0...๐) โ 0 โค (๐ถโ๐)) |
31 | 19, 30 | syl 17 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (1...๐)) โ 0 โค (๐ถโ๐)) |
32 | 31 | adantr 481 |
. . . . . . . 8
โข (((๐ โง ๐ โ (1...๐)) โง ยฌ ๐ < (๐ถโ๐)) โ 0 โค (๐ถโ๐)) |
33 | 25, 24 | subge02d 11802 |
. . . . . . . 8
โข (((๐ โง ๐ โ (1...๐)) โง ยฌ ๐ < (๐ถโ๐)) โ (0 โค (๐ถโ๐) โ (๐ โ (๐ถโ๐)) โค ๐)) |
34 | 32, 33 | mpbid 231 |
. . . . . . 7
โข (((๐ โง ๐ โ (1...๐)) โง ยฌ ๐ < (๐ถโ๐)) โ (๐ โ (๐ถโ๐)) โค ๐) |
35 | 3, 6, 22, 29, 34 | elfzd 13488 |
. . . . . 6
โข (((๐ โง ๐ โ (1...๐)) โง ยฌ ๐ < (๐ถโ๐)) โ (๐ โ (๐ถโ๐)) โ (0...๐)) |
36 | | permnn 14282 |
. . . . . 6
โข ((๐ โ (๐ถโ๐)) โ (0...๐) โ ((!โ๐) / (!โ(๐ โ (๐ถโ๐)))) โ โ) |
37 | 35, 36 | syl 17 |
. . . . 5
โข (((๐ โง ๐ โ (1...๐)) โง ยฌ ๐ < (๐ถโ๐)) โ ((!โ๐) / (!โ(๐ โ (๐ถโ๐)))) โ โ) |
38 | 37 | nnzd 12581 |
. . . 4
โข (((๐ โง ๐ โ (1...๐)) โง ยฌ ๐ < (๐ถโ๐)) โ ((!โ๐) / (!โ(๐ โ (๐ถโ๐)))) โ โค) |
39 | | etransclem7.j |
. . . . . . . . 9
โข (๐ โ ๐ฝ โ (0...๐)) |
40 | 39 | elfzelzd 13498 |
. . . . . . . 8
โข (๐ โ ๐ฝ โ โค) |
41 | 40 | adantr 481 |
. . . . . . 7
โข ((๐ โง ๐ โ (1...๐)) โ ๐ฝ โ โค) |
42 | | elfzelz 13497 |
. . . . . . . 8
โข (๐ โ (1...๐) โ ๐ โ โค) |
43 | 42 | adantl 482 |
. . . . . . 7
โข ((๐ โง ๐ โ (1...๐)) โ ๐ โ โค) |
44 | 41, 43 | zsubcld 12667 |
. . . . . 6
โข ((๐ โง ๐ โ (1...๐)) โ (๐ฝ โ ๐) โ โค) |
45 | 44 | adantr 481 |
. . . . 5
โข (((๐ โง ๐ โ (1...๐)) โง ยฌ ๐ < (๐ถโ๐)) โ (๐ฝ โ ๐) โ โค) |
46 | | elnn0z 12567 |
. . . . . 6
โข ((๐ โ (๐ถโ๐)) โ โ0 โ ((๐ โ (๐ถโ๐)) โ โค โง 0 โค (๐ โ (๐ถโ๐)))) |
47 | 22, 29, 46 | sylanbrc 583 |
. . . . 5
โข (((๐ โง ๐ โ (1...๐)) โง ยฌ ๐ < (๐ถโ๐)) โ (๐ โ (๐ถโ๐)) โ
โ0) |
48 | | zexpcl 14038 |
. . . . 5
โข (((๐ฝ โ ๐) โ โค โง (๐ โ (๐ถโ๐)) โ โ0) โ ((๐ฝ โ ๐)โ(๐ โ (๐ถโ๐))) โ โค) |
49 | 45, 47, 48 | syl2anc 584 |
. . . 4
โข (((๐ โง ๐ โ (1...๐)) โง ยฌ ๐ < (๐ถโ๐)) โ ((๐ฝ โ ๐)โ(๐ โ (๐ถโ๐))) โ โค) |
50 | 38, 49 | zmulcld 12668 |
. . 3
โข (((๐ โง ๐ โ (1...๐)) โง ยฌ ๐ < (๐ถโ๐)) โ (((!โ๐) / (!โ(๐ โ (๐ถโ๐)))) ยท ((๐ฝ โ ๐)โ(๐ โ (๐ถโ๐)))) โ โค) |
51 | 2, 50 | ifclda 4562 |
. 2
โข ((๐ โง ๐ โ (1...๐)) โ if(๐ < (๐ถโ๐), 0, (((!โ๐) / (!โ(๐ โ (๐ถโ๐)))) ยท ((๐ฝ โ ๐)โ(๐ โ (๐ถโ๐))))) โ โค) |
52 | 1, 51 | fprodzcl 15894 |
1
โข (๐ โ โ๐ โ (1...๐)if(๐ < (๐ถโ๐), 0, (((!โ๐) / (!โ(๐ โ (๐ถโ๐)))) ยท ((๐ฝ โ ๐)โ(๐ โ (๐ถโ๐))))) โ โค) |