Step | Hyp | Ref
| Expression |
1 | | 0zd 12575 |
. 2
โข ((๐ โง (๐ โ 1) < (๐ถโ0)) โ 0 โ
โค) |
2 | | 0zd 12575 |
. . . . . . . . 9
โข (๐ โ 0 โ
โค) |
3 | | etransclem10.n |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
4 | | nnm1nn0 12518 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
5 | 3, 4 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (๐ โ 1) โ
โ0) |
6 | 5 | nn0zd 12589 |
. . . . . . . . 9
โข (๐ โ (๐ โ 1) โ โค) |
7 | | etransclem10.c |
. . . . . . . . . . . 12
โข (๐ โ ๐ถ:(0...๐)โถ(0...๐)) |
8 | | etransclem10.m |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ
โ0) |
9 | | nn0uz 12869 |
. . . . . . . . . . . . . 14
โข
โ0 = (โคโฅโ0) |
10 | 8, 9 | eleqtrdi 2842 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ
(โคโฅโ0)) |
11 | | eluzfz1 13513 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ0) โ 0 โ (0...๐)) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ 0 โ (0...๐)) |
13 | 7, 12 | ffvelcdmd 7088 |
. . . . . . . . . . 11
โข (๐ โ (๐ถโ0) โ (0...๐)) |
14 | 13 | elfzelzd 13507 |
. . . . . . . . . 10
โข (๐ โ (๐ถโ0) โ โค) |
15 | 6, 14 | zsubcld 12676 |
. . . . . . . . 9
โข (๐ โ ((๐ โ 1) โ (๐ถโ0)) โ โค) |
16 | 2, 6, 15 | 3jca 1127 |
. . . . . . . 8
โข (๐ โ (0 โ โค โง
(๐ โ 1) โ
โค โง ((๐ โ
1) โ (๐ถโ0))
โ โค)) |
17 | 16 | adantr 480 |
. . . . . . 7
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ (0 โ โค โง
(๐ โ 1) โ
โค โง ((๐ โ
1) โ (๐ถโ0))
โ โค)) |
18 | 14 | zred 12671 |
. . . . . . . . . 10
โข (๐ โ (๐ถโ0) โ โ) |
19 | 18 | adantr 480 |
. . . . . . . . 9
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ (๐ถโ0) โ โ) |
20 | 5 | nn0red 12538 |
. . . . . . . . . 10
โข (๐ โ (๐ โ 1) โ โ) |
21 | 20 | adantr 480 |
. . . . . . . . 9
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ (๐ โ 1) โ โ) |
22 | | simpr 484 |
. . . . . . . . 9
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ ยฌ (๐ โ 1) < (๐ถโ0)) |
23 | 19, 21, 22 | nltled 11369 |
. . . . . . . 8
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ (๐ถโ0) โค (๐ โ 1)) |
24 | 21, 19 | subge0d 11809 |
. . . . . . . 8
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ (0 โค ((๐ โ 1) โ (๐ถโ0)) โ (๐ถโ0) โค (๐ โ 1))) |
25 | 23, 24 | mpbird 256 |
. . . . . . 7
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ 0 โค ((๐ โ 1) โ (๐ถโ0))) |
26 | | elfzle1 13509 |
. . . . . . . . . 10
โข ((๐ถโ0) โ (0...๐) โ 0 โค (๐ถโ0)) |
27 | 13, 26 | syl 17 |
. . . . . . . . 9
โข (๐ โ 0 โค (๐ถโ0)) |
28 | 27 | adantr 480 |
. . . . . . . 8
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ 0 โค (๐ถโ0)) |
29 | 21, 19 | subge02d 11811 |
. . . . . . . 8
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ (0 โค (๐ถโ0) โ ((๐ โ 1) โ (๐ถโ0)) โค (๐ โ 1))) |
30 | 28, 29 | mpbid 231 |
. . . . . . 7
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ ((๐ โ 1) โ (๐ถโ0)) โค (๐ โ 1)) |
31 | 17, 25, 30 | jca32 515 |
. . . . . 6
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ ((0 โ โค โง
(๐ โ 1) โ
โค โง ((๐ โ
1) โ (๐ถโ0))
โ โค) โง (0 โค ((๐ โ 1) โ (๐ถโ0)) โง ((๐ โ 1) โ (๐ถโ0)) โค (๐ โ 1)))) |
32 | | elfz2 13496 |
. . . . . 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 14291 |
. . . . 5
โข (((๐ โ 1) โ (๐ถโ0)) โ (0...(๐ โ 1)) โ
((!โ(๐ โ 1)) /
(!โ((๐ โ 1)
โ (๐ถโ0))))
โ โ) |
35 | 33, 34 | syl 17 |
. . . 4
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ ((!โ(๐ โ 1)) / (!โ((๐ โ 1) โ (๐ถโ0)))) โ
โ) |
36 | 35 | nnzd 12590 |
. . 3
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ ((!โ(๐ โ 1)) / (!โ((๐ โ 1) โ (๐ถโ0)))) โ
โค) |
37 | | etransclem10.j |
. . . . 5
โข (๐ โ ๐ฝ โ โค) |
38 | 37 | adantr 480 |
. . . 4
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ ๐ฝ โ โค) |
39 | 15 | adantr 480 |
. . . . 5
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ ((๐ โ 1) โ (๐ถโ0)) โ โค) |
40 | | elnn0z 12576 |
. . . . 5
โข (((๐ โ 1) โ (๐ถโ0)) โ
โ0 โ (((๐ โ 1) โ (๐ถโ0)) โ โค โง 0 โค
((๐ โ 1) โ
(๐ถโ0)))) |
41 | 39, 25, 40 | sylanbrc 582 |
. . . 4
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ ((๐ โ 1) โ (๐ถโ0)) โ
โ0) |
42 | | zexpcl 14047 |
. . . 4
โข ((๐ฝ โ โค โง ((๐ โ 1) โ (๐ถโ0)) โ
โ0) โ (๐ฝโ((๐ โ 1) โ (๐ถโ0))) โ โค) |
43 | 38, 41, 42 | syl2anc 583 |
. . 3
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ (๐ฝโ((๐ โ 1) โ (๐ถโ0))) โ โค) |
44 | 36, 43 | zmulcld 12677 |
. 2
โข ((๐ โง ยฌ (๐ โ 1) < (๐ถโ0)) โ (((!โ(๐ โ 1)) / (!โ((๐ โ 1) โ (๐ถโ0)))) ยท (๐ฝโ((๐ โ 1) โ (๐ถโ0)))) โ
โค) |
45 | 1, 44 | ifclda 4564 |
1
โข (๐ โ if((๐ โ 1) < (๐ถโ0), 0, (((!โ(๐ โ 1)) / (!โ((๐ โ 1) โ (๐ถโ0)))) ยท (๐ฝโ((๐ โ 1) โ (๐ถโ0))))) โ
โค) |