Step | Hyp | Ref
| Expression |
1 | | 0zd 12572 |
. 2
โข ((๐ โง (๐ โ 1) < (๐ถโ0)) โ 0 โ
โค) |
2 | | 0zd 12572 |
. . . . . . . . 9
โข (๐ โ 0 โ
โค) |
3 | | etransclem10.n |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
4 | | nnm1nn0 12515 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
5 | 3, 4 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (๐ โ 1) โ
โ0) |
6 | 5 | nn0zd 12586 |
. . . . . . . . 9
โข (๐ โ (๐ โ 1) โ โค) |
7 | | etransclem10.c |
. . . . . . . . . . . 12
โข (๐ โ ๐ถ:(0...๐)โถ(0...๐)) |
8 | | etransclem10.m |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ
โ0) |
9 | | nn0uz 12866 |
. . . . . . . . . . . . . 14
โข
โ0 = (โคโฅโ0) |
10 | 8, 9 | eleqtrdi 2843 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ
(โคโฅโ0)) |
11 | | eluzfz1 13510 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ0) โ 0 โ (0...๐)) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ 0 โ (0...๐)) |
13 | 7, 12 | ffvelcdmd 7087 |
. . . . . . . . . . 11
โข (๐ โ (๐ถโ0) โ (0...๐)) |
14 | 13 | elfzelzd 13504 |
. . . . . . . . . 10
โข (๐ โ (๐ถโ0) โ โค) |
15 | 6, 14 | zsubcld 12673 |
. . . . . . . . 9
โข (๐ โ ((๐ โ 1) โ (๐ถโ0)) โ โค) |
16 | 2, 6, 15 | 3jca 1128 |
. . . . . . . 8
โข (๐ โ (0 โ โค โง
(๐ โ 1) โ
โค โง ((๐ โ
1) โ (๐ถโ0))
โ โค)) |
17 | 16 | adantr 481 |
. . . . . . 7
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ (0 โ โค โง
(๐ โ 1) โ
โค โง ((๐ โ
1) โ (๐ถโ0))
โ โค)) |
18 | 14 | zred 12668 |
. . . . . . . . . 10
โข (๐ โ (๐ถโ0) โ โ) |
19 | 18 | adantr 481 |
. . . . . . . . 9
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ (๐ถโ0) โ โ) |
20 | 5 | nn0red 12535 |
. . . . . . . . . 10
โข (๐ โ (๐ โ 1) โ โ) |
21 | 20 | adantr 481 |
. . . . . . . . 9
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ (๐ โ 1) โ โ) |
22 | | simpr 485 |
. . . . . . . . 9
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ ยฌ (๐ โ 1) < (๐ถโ0)) |
23 | 19, 21, 22 | nltled 11366 |
. . . . . . . 8
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ (๐ถโ0) โค (๐ โ 1)) |
24 | 21, 19 | subge0d 11806 |
. . . . . . . 8
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ (0 โค ((๐ โ 1) โ (๐ถโ0)) โ (๐ถโ0) โค (๐ โ 1))) |
25 | 23, 24 | mpbird 256 |
. . . . . . 7
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ 0 โค ((๐ โ 1) โ (๐ถโ0))) |
26 | | elfzle1 13506 |
. . . . . . . . . 10
โข ((๐ถโ0) โ (0...๐) โ 0 โค (๐ถโ0)) |
27 | 13, 26 | syl 17 |
. . . . . . . . 9
โข (๐ โ 0 โค (๐ถโ0)) |
28 | 27 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ 0 โค (๐ถโ0)) |
29 | 21, 19 | subge02d 11808 |
. . . . . . . 8
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ (0 โค (๐ถโ0) โ ((๐ โ 1) โ (๐ถโ0)) โค (๐ โ 1))) |
30 | 28, 29 | mpbid 231 |
. . . . . . 7
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ ((๐ โ 1) โ (๐ถโ0)) โค (๐ โ 1)) |
31 | 17, 25, 30 | jca32 516 |
. . . . . 6
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ ((0 โ โค โง
(๐ โ 1) โ
โค โง ((๐ โ
1) โ (๐ถโ0))
โ โค) โง (0 โค ((๐ โ 1) โ (๐ถโ0)) โง ((๐ โ 1) โ (๐ถโ0)) โค (๐ โ 1)))) |
32 | | elfz2 13493 |
. . . . . 6
โข (((๐ โ 1) โ (๐ถโ0)) โ (0...(๐ โ 1)) โ ((0 โ
โค โง (๐ โ 1)
โ โค โง ((๐
โ 1) โ (๐ถโ0)) โ โค) โง (0 โค
((๐ โ 1) โ
(๐ถโ0)) โง ((๐ โ 1) โ (๐ถโ0)) โค (๐ โ 1)))) |
33 | 31, 32 | sylibr 233 |
. . . . 5
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ ((๐ โ 1) โ (๐ถโ0)) โ (0...(๐ โ 1))) |
34 | | permnn 14288 |
. . . . 5
โข (((๐ โ 1) โ (๐ถโ0)) โ (0...(๐ โ 1)) โ
((!โ(๐ โ 1)) /
(!โ((๐ โ 1)
โ (๐ถโ0))))
โ โ) |
35 | 33, 34 | syl 17 |
. . . 4
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ ((!โ(๐ โ 1)) / (!โ((๐ โ 1) โ (๐ถโ0)))) โ
โ) |
36 | 35 | nnzd 12587 |
. . 3
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ ((!โ(๐ โ 1)) / (!โ((๐ โ 1) โ (๐ถโ0)))) โ
โค) |
37 | | etransclem10.j |
. . . . 5
โข (๐ โ ๐ฝ โ โค) |
38 | 37 | adantr 481 |
. . . 4
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ ๐ฝ โ โค) |
39 | 15 | adantr 481 |
. . . . 5
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ ((๐ โ 1) โ (๐ถโ0)) โ โค) |
40 | | elnn0z 12573 |
. . . . 5
โข (((๐ โ 1) โ (๐ถโ0)) โ
โ0 โ (((๐ โ 1) โ (๐ถโ0)) โ โค โง 0 โค
((๐ โ 1) โ
(๐ถโ0)))) |
41 | 39, 25, 40 | sylanbrc 583 |
. . . 4
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ ((๐ โ 1) โ (๐ถโ0)) โ
โ0) |
42 | | zexpcl 14044 |
. . . 4
โข ((๐ฝ โ โค โง ((๐ โ 1) โ (๐ถโ0)) โ
โ0) โ (๐ฝโ((๐ โ 1) โ (๐ถโ0))) โ โค) |
43 | 38, 41, 42 | syl2anc 584 |
. . 3
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ (๐ฝโ((๐ โ 1) โ (๐ถโ0))) โ โค) |
44 | 36, 43 | zmulcld 12674 |
. 2
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ (((!โ(๐ โ 1)) / (!โ((๐ โ 1) โ (๐ถโ0)))) ยท (๐ฝโ((๐ โ 1) โ (๐ถโ0)))) โ
โค) |
45 | 1, 44 | ifclda 4563 |
1
โข (๐ โ if((๐ โ 1) < (๐ถโ0), 0, (((!โ(๐ โ 1)) / (!โ((๐ โ 1) โ (๐ถโ0)))) ยท (๐ฝโ((๐ โ 1) โ (๐ถโ0))))) โ
โค) |