Step | Hyp | Ref
| Expression |
1 | | flge0nn0 13781 |
. . 3
โข ((๐ด โ โ โง 0 โค
๐ด) โ
(โโ๐ด) โ
โ0) |
2 | | logfac 26091 |
. . 3
โข
((โโ๐ด)
โ โ0 โ (logโ(!โ(โโ๐ด))) = ฮฃ๐ โ (1...(โโ๐ด))(logโ๐)) |
3 | 1, 2 | syl 17 |
. 2
โข ((๐ด โ โ โง 0 โค
๐ด) โ
(logโ(!โ(โโ๐ด))) = ฮฃ๐ โ (1...(โโ๐ด))(logโ๐)) |
4 | | fzfid 13934 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ
(1...(โโ๐ด))
โ Fin) |
5 | | fzfid 13934 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ (1...(โโ๐ด)) โ Fin) |
6 | | ssrab2 4076 |
. . . . 5
โข {๐ฅ โ
(1...(โโ๐ด))
โฃ ๐ โฅ ๐ฅ} โ
(1...(โโ๐ด)) |
7 | | ssfi 9169 |
. . . . 5
โข
(((1...(โโ๐ด)) โ Fin โง {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ} โ (1...(โโ๐ด))) โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ} โ Fin) |
8 | 5, 6, 7 | sylancl 587 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ} โ Fin) |
9 | | flcl 13756 |
. . . . . . . . 9
โข (๐ด โ โ โ
(โโ๐ด) โ
โค) |
10 | 9 | adantr 482 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 โค
๐ด) โ
(โโ๐ด) โ
โค) |
11 | | fznn 13565 |
. . . . . . . 8
โข
((โโ๐ด)
โ โค โ (๐
โ (1...(โโ๐ด)) โ (๐ โ โ โง ๐ โค (โโ๐ด)))) |
12 | 10, 11 | syl 17 |
. . . . . . 7
โข ((๐ด โ โ โง 0 โค
๐ด) โ (๐ โ
(1...(โโ๐ด))
โ (๐ โ โ
โง ๐ โค
(โโ๐ด)))) |
13 | 12 | anbi1d 631 |
. . . . . 6
โข ((๐ด โ โ โง 0 โค
๐ด) โ ((๐ โ
(1...(โโ๐ด))
โง (๐ โ
(1...(โโ๐ด))
โง ๐ โฅ ๐)) โ ((๐ โ โ โง ๐ โค (โโ๐ด)) โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐)))) |
14 | | nnre 12215 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
15 | 14 | ad2antlr 726 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ โ) โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐)) โ ๐ โ โ) |
16 | | elfznn 13526 |
. . . . . . . . . . . 12
โข (๐ โ
(1...(โโ๐ด))
โ ๐ โ
โ) |
17 | 16 | ad2antrl 727 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ โ) โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐)) โ ๐ โ โ) |
18 | 17 | nnred 12223 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ โ) โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐)) โ ๐ โ โ) |
19 | | reflcl 13757 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
20 | 19 | ad3antrrr 729 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ โ) โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐)) โ (โโ๐ด) โ โ) |
21 | | simprr 772 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ โ) โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐)) โ ๐ โฅ ๐) |
22 | | nnz 12575 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โค) |
23 | 22 | ad2antlr 726 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ โ) โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐)) โ ๐ โ โค) |
24 | | dvdsle 16249 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โ) โ (๐ โฅ ๐ โ ๐ โค ๐)) |
25 | 23, 17, 24 | syl2anc 585 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ โ) โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐)) โ (๐ โฅ ๐ โ ๐ โค ๐)) |
26 | 21, 25 | mpd 15 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ โ) โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐)) โ ๐ โค ๐) |
27 | | elfzle2 13501 |
. . . . . . . . . . 11
โข (๐ โ
(1...(โโ๐ด))
โ ๐ โค
(โโ๐ด)) |
28 | 27 | ad2antrl 727 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ โ) โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐)) โ ๐ โค (โโ๐ด)) |
29 | 15, 18, 20, 26, 28 | letrd 11367 |
. . . . . . . . 9
โข ((((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ โ) โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐)) โ ๐ โค (โโ๐ด)) |
30 | 29 | expl 459 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 โค
๐ด) โ ((๐ โ โ โง (๐ โ
(1...(โโ๐ด))
โง ๐ โฅ ๐)) โ ๐ โค (โโ๐ด))) |
31 | 30 | pm4.71rd 564 |
. . . . . . 7
โข ((๐ด โ โ โง 0 โค
๐ด) โ ((๐ โ โ โง (๐ โ
(1...(โโ๐ด))
โง ๐ โฅ ๐)) โ (๐ โค (โโ๐ด) โง (๐ โ โ โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐))))) |
32 | | an12 644 |
. . . . . . 7
โข ((๐ โ
(1...(โโ๐ด))
โง (๐ โ โ
โง ๐ โฅ ๐)) โ (๐ โ โ โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐))) |
33 | | an21 643 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โค (โโ๐ด)) โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐)) โ (๐ โค (โโ๐ด) โง (๐ โ โ โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐)))) |
34 | 31, 32, 33 | 3bitr4g 314 |
. . . . . 6
โข ((๐ด โ โ โง 0 โค
๐ด) โ ((๐ โ
(1...(โโ๐ด))
โง (๐ โ โ
โง ๐ โฅ ๐)) โ ((๐ โ โ โง ๐ โค (โโ๐ด)) โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐)))) |
35 | 13, 34 | bitr4d 282 |
. . . . 5
โข ((๐ด โ โ โง 0 โค
๐ด) โ ((๐ โ
(1...(โโ๐ด))
โง (๐ โ
(1...(โโ๐ด))
โง ๐ โฅ ๐)) โ (๐ โ (1...(โโ๐ด)) โง (๐ โ โ โง ๐ โฅ ๐)))) |
36 | | breq2 5151 |
. . . . . . 7
โข (๐ฅ = ๐ โ (๐ โฅ ๐ฅ โ ๐ โฅ ๐)) |
37 | 36 | elrab 3682 |
. . . . . 6
โข (๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ} โ (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐)) |
38 | 37 | anbi2i 624 |
. . . . 5
โข ((๐ โ
(1...(โโ๐ด))
โง ๐ โ {๐ฅ โ
(1...(โโ๐ด))
โฃ ๐ โฅ ๐ฅ}) โ (๐ โ (1...(โโ๐ด)) โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐))) |
39 | | breq1 5150 |
. . . . . . 7
โข (๐ฅ = ๐ โ (๐ฅ โฅ ๐ โ ๐ โฅ ๐)) |
40 | 39 | elrab 3682 |
. . . . . 6
โข (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ (๐ โ โ โง ๐ โฅ ๐)) |
41 | 40 | anbi2i 624 |
. . . . 5
โข ((๐ โ
(1...(โโ๐ด))
โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (๐ โ (1...(โโ๐ด)) โง (๐ โ โ โง ๐ โฅ ๐))) |
42 | 35, 38, 41 | 3bitr4g 314 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ ((๐ โ
(1...(โโ๐ด))
โง ๐ โ {๐ฅ โ
(1...(โโ๐ด))
โฃ ๐ โฅ ๐ฅ}) โ (๐ โ (1...(โโ๐ด)) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}))) |
43 | | elfznn 13526 |
. . . . . . . 8
โข (๐ โ
(1...(โโ๐ด))
โ ๐ โ
โ) |
44 | 43 | adantl 483 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ ๐ โ โ) |
45 | | vmacl 26602 |
. . . . . . 7
โข (๐ โ โ โ
(ฮโ๐) โ
โ) |
46 | 44, 45 | syl 17 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ (ฮโ๐) โ
โ) |
47 | 46 | recnd 11238 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ (ฮโ๐) โ
โ) |
48 | 47 | adantrr 716 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ โ
(1...(โโ๐ด))
โง ๐ โ {๐ฅ โ
(1...(โโ๐ด))
โฃ ๐ โฅ ๐ฅ})) โ (ฮโ๐) โ
โ) |
49 | 4, 4, 8, 42, 48 | fsumcom2 15716 |
. . 3
โข ((๐ด โ โ โง 0 โค
๐ด) โ ฮฃ๐ โ
(1...(โโ๐ด))ฮฃ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ} (ฮโ๐) = ฮฃ๐ โ (1...(โโ๐ด))ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} (ฮโ๐)) |
50 | | fsumconst 15732 |
. . . . . 6
โข (({๐ฅ โ
(1...(โโ๐ด))
โฃ ๐ โฅ ๐ฅ} โ Fin โง
(ฮโ๐) โ
โ) โ ฮฃ๐
โ {๐ฅ โ
(1...(โโ๐ด))
โฃ ๐ โฅ ๐ฅ} (ฮโ๐) = ((โฏโ{๐ฅ โ
(1...(โโ๐ด))
โฃ ๐ โฅ ๐ฅ}) ยท
(ฮโ๐))) |
51 | 8, 47, 50 | syl2anc 585 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ ฮฃ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ} (ฮโ๐) = ((โฏโ{๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) ยท (ฮโ๐))) |
52 | | fzfid 13934 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ (1...(โโ(๐ด / ๐))) โ Fin) |
53 | | simpll 766 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ ๐ด โ โ) |
54 | | eqid 2733 |
. . . . . . . . 9
โข (๐ โ
(1...(โโ(๐ด /
๐))) โฆ (๐ ยท ๐)) = (๐ โ (1...(โโ(๐ด / ๐))) โฆ (๐ ยท ๐)) |
55 | 53, 44, 54 | dvdsflf1o 26671 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ (๐ โ (1...(โโ(๐ด / ๐))) โฆ (๐ ยท ๐)):(1...(โโ(๐ด / ๐)))โ1-1-ontoโ{๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) |
56 | 52, 55 | hasheqf1od 14309 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ
(โฏโ(1...(โโ(๐ด / ๐)))) = (โฏโ{๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ})) |
57 | | simpl 484 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 โค
๐ด) โ ๐ด โ โ) |
58 | | nndivre 12249 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ด / ๐) โ โ) |
59 | 57, 43, 58 | syl2an 597 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ (๐ด / ๐) โ โ) |
60 | | nngt0 12239 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 0 <
๐) |
61 | 14, 60 | jca 513 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ โ โ โง 0 <
๐)) |
62 | 43, 61 | syl 17 |
. . . . . . . . . 10
โข (๐ โ
(1...(โโ๐ด))
โ (๐ โ โ
โง 0 < ๐)) |
63 | | divge0 12079 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ โ โ โง 0 <
๐)) โ 0 โค (๐ด / ๐)) |
64 | 62, 63 | sylan2 594 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ 0 โค (๐ด / ๐)) |
65 | | flge0nn0 13781 |
. . . . . . . . 9
โข (((๐ด / ๐) โ โ โง 0 โค (๐ด / ๐)) โ (โโ(๐ด / ๐)) โ
โ0) |
66 | 59, 64, 65 | syl2anc 585 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ (โโ(๐ด / ๐)) โ
โ0) |
67 | | hashfz1 14302 |
. . . . . . . 8
โข
((โโ(๐ด /
๐)) โ
โ0 โ (โฏโ(1...(โโ(๐ด / ๐)))) = (โโ(๐ด / ๐))) |
68 | 66, 67 | syl 17 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ
(โฏโ(1...(โโ(๐ด / ๐)))) = (โโ(๐ด / ๐))) |
69 | 56, 68 | eqtr3d 2775 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ (โฏโ{๐ฅ โ
(1...(โโ๐ด))
โฃ ๐ โฅ ๐ฅ}) = (โโ(๐ด / ๐))) |
70 | 69 | oveq1d 7419 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ ((โฏโ{๐ฅ โ
(1...(โโ๐ด))
โฃ ๐ โฅ ๐ฅ}) ยท
(ฮโ๐)) =
((โโ(๐ด / ๐)) ยท
(ฮโ๐))) |
71 | 59 | flcld 13759 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ (โโ(๐ด / ๐)) โ โค) |
72 | 71 | zcnd 12663 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ (โโ(๐ด / ๐)) โ โ) |
73 | 72, 47 | mulcomd 11231 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ ((โโ(๐ด / ๐)) ยท (ฮโ๐)) = ((ฮโ๐) ยท (โโ(๐ด / ๐)))) |
74 | 51, 70, 73 | 3eqtrd 2777 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ ฮฃ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ} (ฮโ๐) = ((ฮโ๐) ยท (โโ(๐ด / ๐)))) |
75 | 74 | sumeq2dv 15645 |
. . 3
โข ((๐ด โ โ โง 0 โค
๐ด) โ ฮฃ๐ โ
(1...(โโ๐ด))ฮฃ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ} (ฮโ๐) = ฮฃ๐ โ (1...(โโ๐ด))((ฮโ๐) ยท (โโ(๐ด / ๐)))) |
76 | 16 | adantl 483 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ ๐ โ โ) |
77 | | vmasum 26699 |
. . . . 5
โข (๐ โ โ โ
ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} (ฮโ๐) = (logโ๐)) |
78 | 76, 77 | syl 17 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ โ (1...(โโ๐ด))) โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} (ฮโ๐) = (logโ๐)) |
79 | 78 | sumeq2dv 15645 |
. . 3
โข ((๐ด โ โ โง 0 โค
๐ด) โ ฮฃ๐ โ
(1...(โโ๐ด))ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} (ฮโ๐) = ฮฃ๐ โ (1...(โโ๐ด))(logโ๐)) |
80 | 49, 75, 79 | 3eqtr3d 2781 |
. 2
โข ((๐ด โ โ โง 0 โค
๐ด) โ ฮฃ๐ โ
(1...(โโ๐ด))((ฮโ๐) ยท (โโ(๐ด / ๐))) = ฮฃ๐ โ (1...(โโ๐ด))(logโ๐)) |
81 | 3, 80 | eqtr4d 2776 |
1
โข ((๐ด โ โ โง 0 โค
๐ด) โ
(logโ(!โ(โโ๐ด))) = ฮฃ๐ โ (1...(โโ๐ด))((ฮโ๐) ยท (โโ(๐ด / ๐)))) |