Step | Hyp | Ref
| Expression |
1 | | etransclem41.mp |
. . . . . . 7
โข (๐ โ (!โ๐) < ๐) |
2 | | etransclem41.m |
. . . . . . . . . 10
โข (๐ โ ๐ โ
โ0) |
3 | 2 | faccld 14241 |
. . . . . . . . 9
โข (๐ โ (!โ๐) โ โ) |
4 | 3 | nnred 12224 |
. . . . . . . 8
โข (๐ โ (!โ๐) โ โ) |
5 | | etransclem41.p |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
6 | | prmnn 16608 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
8 | 7 | nnred 12224 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
9 | 4, 8 | ltnled 11358 |
. . . . . . 7
โข (๐ โ ((!โ๐) < ๐ โ ยฌ ๐ โค (!โ๐))) |
10 | 1, 9 | mpbid 231 |
. . . . . 6
โข (๐ โ ยฌ ๐ โค (!โ๐)) |
11 | 7 | nnzd 12582 |
. . . . . . . . 9
โข (๐ โ ๐ โ โค) |
12 | 11, 3 | jca 511 |
. . . . . . . 8
โข (๐ โ (๐ โ โค โง (!โ๐) โ
โ)) |
13 | 12 | adantr 480 |
. . . . . . 7
โข ((๐ โง ๐ โฅ (!โ๐)) โ (๐ โ โค โง (!โ๐) โ
โ)) |
14 | | simpr 484 |
. . . . . . 7
โข ((๐ โง ๐ โฅ (!โ๐)) โ ๐ โฅ (!โ๐)) |
15 | | dvdsle 16250 |
. . . . . . 7
โข ((๐ โ โค โง
(!โ๐) โ โ)
โ (๐ โฅ
(!โ๐) โ ๐ โค (!โ๐))) |
16 | 13, 14, 15 | sylc 65 |
. . . . . 6
โข ((๐ โง ๐ โฅ (!โ๐)) โ ๐ โค (!โ๐)) |
17 | 10, 16 | mtand 813 |
. . . . 5
โข (๐ โ ยฌ ๐ โฅ (!โ๐)) |
18 | | fzfid 13935 |
. . . . . . . . . 10
โข (โค
โ (1...๐) โ
Fin) |
19 | | elfzelz 13498 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ ๐ โ โค) |
20 | 19 | znegcld 12665 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐) โ -๐ โ โค) |
21 | 20 | zcnd 12664 |
. . . . . . . . . . 11
โข (๐ โ (1...๐) โ -๐ โ โ) |
22 | 21 | adantl 481 |
. . . . . . . . . 10
โข
((โค โง ๐
โ (1...๐)) โ
-๐ โ
โ) |
23 | 18, 22 | fprodabs2 44796 |
. . . . . . . . 9
โข (โค
โ (absโโ๐
โ (1...๐)-๐) = โ๐ โ (1...๐)(absโ-๐)) |
24 | 23 | mptru 1540 |
. . . . . . . 8
โข
(absโโ๐
โ (1...๐)-๐) = โ๐ โ (1...๐)(absโ-๐) |
25 | 19 | zcnd 12664 |
. . . . . . . . . . 11
โข (๐ โ (1...๐) โ ๐ โ โ) |
26 | 25 | absnegd 15393 |
. . . . . . . . . 10
โข (๐ โ (1...๐) โ (absโ-๐) = (absโ๐)) |
27 | 19 | zred 12663 |
. . . . . . . . . . 11
โข (๐ โ (1...๐) โ ๐ โ โ) |
28 | | 0red 11214 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐) โ 0 โ โ) |
29 | | 1red 11212 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ 1 โ โ) |
30 | | 0lt1 11733 |
. . . . . . . . . . . . . 14
โข 0 <
1 |
31 | 30 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ 0 < 1) |
32 | | elfzle1 13501 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ 1 โค ๐) |
33 | 28, 29, 27, 31, 32 | ltletrd 11371 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐) โ 0 < ๐) |
34 | 28, 27, 33 | ltled 11359 |
. . . . . . . . . . 11
โข (๐ โ (1...๐) โ 0 โค ๐) |
35 | 27, 34 | absidd 15366 |
. . . . . . . . . 10
โข (๐ โ (1...๐) โ (absโ๐) = ๐) |
36 | 26, 35 | eqtrd 2764 |
. . . . . . . . 9
โข (๐ โ (1...๐) โ (absโ-๐) = ๐) |
37 | 36 | prodeq2i 15860 |
. . . . . . . 8
โข
โ๐ โ
(1...๐)(absโ-๐) = โ๐ โ (1...๐)๐ |
38 | 24, 37 | eqtri 2752 |
. . . . . . 7
โข
(absโโ๐
โ (1...๐)-๐) = โ๐ โ (1...๐)๐ |
39 | | fprodfac 15914 |
. . . . . . . 8
โข (๐ โ โ0
โ (!โ๐) =
โ๐ โ (1...๐)๐) |
40 | 2, 39 | syl 17 |
. . . . . . 7
โข (๐ โ (!โ๐) = โ๐ โ (1...๐)๐) |
41 | 38, 40 | eqtr4id 2783 |
. . . . . 6
โข (๐ โ (absโโ๐ โ (1...๐)-๐) = (!โ๐)) |
42 | 41 | breq2d 5150 |
. . . . 5
โข (๐ โ (๐ โฅ (absโโ๐ โ (1...๐)-๐) โ ๐ โฅ (!โ๐))) |
43 | 17, 42 | mtbird 325 |
. . . 4
โข (๐ โ ยฌ ๐ โฅ (absโโ๐ โ (1...๐)-๐)) |
44 | | fzfid 13935 |
. . . . . 6
โข (๐ โ (1...๐) โ Fin) |
45 | 20 | adantl 481 |
. . . . . 6
โข ((๐ โง ๐ โ (1...๐)) โ -๐ โ โค) |
46 | 44, 45 | fprodzcl 15895 |
. . . . 5
โข (๐ โ โ๐ โ (1...๐)-๐ โ โค) |
47 | | dvdsabsb 16216 |
. . . . 5
โข ((๐ โ โค โง
โ๐ โ (1...๐)-๐ โ โค) โ (๐ โฅ โ๐ โ (1...๐)-๐ โ ๐ โฅ (absโโ๐ โ (1...๐)-๐))) |
48 | 11, 46, 47 | syl2anc 583 |
. . . 4
โข (๐ โ (๐ โฅ โ๐ โ (1...๐)-๐ โ ๐ โฅ (absโโ๐ โ (1...๐)-๐))) |
49 | 43, 48 | mtbird 325 |
. . 3
โข (๐ โ ยฌ ๐ โฅ โ๐ โ (1...๐)-๐) |
50 | | prmdvdsexp 16649 |
. . . 4
โข ((๐ โ โ โง
โ๐ โ (1...๐)-๐ โ โค โง ๐ โ โ) โ (๐ โฅ (โ๐ โ (1...๐)-๐โ๐) โ ๐ โฅ โ๐ โ (1...๐)-๐)) |
51 | 5, 46, 7, 50 | syl3anc 1368 |
. . 3
โข (๐ โ (๐ โฅ (โ๐ โ (1...๐)-๐โ๐) โ ๐ โฅ โ๐ โ (1...๐)-๐)) |
52 | 49, 51 | mtbird 325 |
. 2
โข (๐ โ ยฌ ๐ โฅ (โ๐ โ (1...๐)-๐โ๐)) |
53 | | etransclem41.f |
. . . . . 6
โข ๐น = (๐ฅ โ โ โฆ ((๐ฅโ(๐ โ 1)) ยท โ๐ โ (1...๐)((๐ฅ โ ๐)โ๐))) |
54 | | etransclem11 45446 |
. . . . . 6
โข (๐ โ โ0
โฆ {๐ โ
((0...๐) โm
(0...๐)) โฃ
ฮฃ๐ โ (0...๐)(๐โ๐) = ๐}) = (๐ โ โ0 โฆ {๐ โ ((0...๐) โm (0...๐)) โฃ ฮฃ๐ โ (0...๐)(๐โ๐) = ๐}) |
55 | | eqeq1 2728 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ = 0 โ ๐ = 0)) |
56 | 55 | ifbid 4543 |
. . . . . . 7
โข (๐ = ๐ โ if(๐ = 0, (๐ โ 1), 0) = if(๐ = 0, (๐ โ 1), 0)) |
57 | 56 | cbvmptv 5251 |
. . . . . 6
โข (๐ โ (0...๐) โฆ if(๐ = 0, (๐ โ 1), 0)) = (๐ โ (0...๐) โฆ if(๐ = 0, (๐ โ 1), 0)) |
58 | 7, 2, 53, 54, 57 | etransclem35 45470 |
. . . . 5
โข (๐ โ (((โ
D๐ ๐น)โ(๐ โ 1))โ0) = ((!โ(๐ โ 1)) ยท
(โ๐ โ (1...๐)-๐โ๐))) |
59 | 58 | oveq1d 7416 |
. . . 4
โข (๐ โ ((((โ
D๐ ๐น)โ(๐ โ 1))โ0) / (!โ(๐ โ 1))) =
(((!โ(๐ โ 1))
ยท (โ๐ โ
(1...๐)-๐โ๐)) / (!โ(๐ โ 1)))) |
60 | 21 | adantl 481 |
. . . . . . 7
โข ((๐ โง ๐ โ (1...๐)) โ -๐ โ โ) |
61 | 44, 60 | fprodcl 15893 |
. . . . . 6
โข (๐ โ โ๐ โ (1...๐)-๐ โ โ) |
62 | 7 | nnnn0d 12529 |
. . . . . 6
โข (๐ โ ๐ โ
โ0) |
63 | 61, 62 | expcld 14108 |
. . . . 5
โข (๐ โ (โ๐ โ (1...๐)-๐โ๐) โ โ) |
64 | | nnm1nn0 12510 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
65 | 7, 64 | syl 17 |
. . . . . . 7
โข (๐ โ (๐ โ 1) โ
โ0) |
66 | 65 | faccld 14241 |
. . . . . 6
โข (๐ โ (!โ(๐ โ 1)) โ
โ) |
67 | 66 | nncnd 12225 |
. . . . 5
โข (๐ โ (!โ(๐ โ 1)) โ
โ) |
68 | 66 | nnne0d 12259 |
. . . . 5
โข (๐ โ (!โ(๐ โ 1)) โ
0) |
69 | 63, 67, 68 | divcan3d 11992 |
. . . 4
โข (๐ โ (((!โ(๐ โ 1)) ยท
(โ๐ โ (1...๐)-๐โ๐)) / (!โ(๐ โ 1))) = (โ๐ โ (1...๐)-๐โ๐)) |
70 | 59, 69 | eqtrd 2764 |
. . 3
โข (๐ โ ((((โ
D๐ ๐น)โ(๐ โ 1))โ0) / (!โ(๐ โ 1))) = (โ๐ โ (1...๐)-๐โ๐)) |
71 | 70 | breq2d 5150 |
. 2
โข (๐ โ (๐ โฅ ((((โ D๐
๐น)โ(๐ โ 1))โ0) / (!โ(๐ โ 1))) โ ๐ โฅ (โ๐ โ (1...๐)-๐โ๐))) |
72 | 52, 71 | mtbird 325 |
1
โข (๐ โ ยฌ ๐ โฅ ((((โ D๐
๐น)โ(๐ โ 1))โ0) / (!โ(๐ โ 1)))) |