Step | Hyp | Ref
| Expression |
1 | | fsumvma2.1 |
. 2
โข (๐ฅ = (๐โ๐) โ ๐ต = ๐ถ) |
2 | | fzfid 13938 |
. 2
โข (๐ โ (1...(โโ๐ด)) โ Fin) |
3 | | fz1ssnn 13532 |
. . 3
โข
(1...(โโ๐ด)) โ โ |
4 | 3 | a1i 11 |
. 2
โข (๐ โ (1...(โโ๐ด)) โ
โ) |
5 | | fsumvma2.2 |
. . 3
โข (๐ โ ๐ด โ โ) |
6 | | ppifi 26610 |
. . 3
โข (๐ด โ โ โ
((0[,]๐ด) โฉ โ)
โ Fin) |
7 | 5, 6 | syl 17 |
. 2
โข (๐ โ ((0[,]๐ด) โฉ โ) โ
Fin) |
8 | | elinel2 4197 |
. . . . 5
โข (๐ โ ((0[,]๐ด) โฉ โ) โ ๐ โ โ) |
9 | | elfznn 13530 |
. . . . 5
โข (๐ โ
(1...(โโ((logโ๐ด) / (logโ๐)))) โ ๐ โ โ) |
10 | 8, 9 | anim12i 614 |
. . . 4
โข ((๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐))))) โ (๐ โ โ โง ๐ โ โ)) |
11 | 10 | pm4.71ri 562 |
. . 3
โข ((๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐))))) โ ((๐ โ โ โง ๐ โ โ) โง (๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐))))))) |
12 | 5 | adantr 482 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ๐ด โ โ) |
13 | | prmnn 16611 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
14 | 13 | ad2antrl 727 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โ) |
15 | | nnnn0 12479 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ0) |
16 | 15 | ad2antll 728 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โ0) |
17 | 14, 16 | nnexpcld 14208 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (๐โ๐) โ โ) |
18 | 17 | nnzd 12585 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (๐โ๐) โ โค) |
19 | | flge 13770 |
. . . . . 6
โข ((๐ด โ โ โง (๐โ๐) โ โค) โ ((๐โ๐) โค ๐ด โ (๐โ๐) โค (โโ๐ด))) |
20 | 12, 18, 19 | syl2anc 585 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((๐โ๐) โค ๐ด โ (๐โ๐) โค (โโ๐ด))) |
21 | | simplrl 776 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ ๐ โ โ) |
22 | 21, 13 | syl 17 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ ๐ โ โ) |
23 | 22 | nnrpd 13014 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ ๐ โ โ+) |
24 | | simplrr 777 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ ๐ โ โ) |
25 | 24 | nnzd 12585 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ ๐ โ โค) |
26 | | relogexp 26104 |
. . . . . . . . . . 11
โข ((๐ โ โ+
โง ๐ โ โค)
โ (logโ(๐โ๐)) = (๐ ยท (logโ๐))) |
27 | 23, 25, 26 | syl2anc 585 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ (logโ(๐โ๐)) = (๐ ยท (logโ๐))) |
28 | 27 | breq1d 5159 |
. . . . . . . . 9
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ ((logโ(๐โ๐)) โค (logโ๐ด) โ (๐ ยท (logโ๐)) โค (logโ๐ด))) |
29 | 24 | nnred 12227 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ ๐ โ โ) |
30 | 12 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ ๐ด โ โ) |
31 | | 0red 11217 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ 0 โ โ) |
32 | 14 | nnred 12227 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โ) |
33 | 32 | adantr 482 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ ๐ โ โ) |
34 | 22 | nngt0d 12261 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ 0 < ๐) |
35 | | 0red 11217 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ 0 โ
โ) |
36 | 14 | nnnn0d 12532 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โ0) |
37 | 36 | nn0ge0d 12535 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ 0 โค ๐) |
38 | | elicc2 13389 |
. . . . . . . . . . . . . . . . 17
โข ((0
โ โ โง ๐ด
โ โ) โ (๐
โ (0[,]๐ด) โ
(๐ โ โ โง 0
โค ๐ โง ๐ โค ๐ด))) |
39 | | df-3an 1090 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง 0 โค
๐ โง ๐ โค ๐ด) โ ((๐ โ โ โง 0 โค ๐) โง ๐ โค ๐ด)) |
40 | 38, 39 | bitrdi 287 |
. . . . . . . . . . . . . . . 16
โข ((0
โ โ โง ๐ด
โ โ) โ (๐
โ (0[,]๐ด) โ
((๐ โ โ โง 0
โค ๐) โง ๐ โค ๐ด))) |
41 | 40 | baibd 541 |
. . . . . . . . . . . . . . 15
โข (((0
โ โ โง ๐ด
โ โ) โง (๐
โ โ โง 0 โค ๐)) โ (๐ โ (0[,]๐ด) โ ๐ โค ๐ด)) |
42 | 35, 12, 32, 37, 41 | syl22anc 838 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (๐ โ (0[,]๐ด) โ ๐ โค ๐ด)) |
43 | 42 | biimpa 478 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ ๐ โค ๐ด) |
44 | 31, 33, 30, 34, 43 | ltletrd 11374 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ 0 < ๐ด) |
45 | 30, 44 | elrpd 13013 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ ๐ด โ
โ+) |
46 | 45 | relogcld 26131 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ (logโ๐ด) โ โ) |
47 | | prmuz2 16633 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
48 | | eluzelre 12833 |
. . . . . . . . . . . 12
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
49 | | eluz2gt1 12904 |
. . . . . . . . . . . 12
โข (๐ โ
(โคโฅโ2) โ 1 < ๐) |
50 | 48, 49 | rplogcld 26137 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ2) โ (logโ๐) โ
โ+) |
51 | 21, 47, 50 | 3syl 18 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ (logโ๐) โ
โ+) |
52 | 29, 46, 51 | lemuldivd 13065 |
. . . . . . . . 9
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ ((๐ ยท (logโ๐)) โค (logโ๐ด) โ ๐ โค ((logโ๐ด) / (logโ๐)))) |
53 | 46, 51 | rerpdivcld 13047 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ ((logโ๐ด) / (logโ๐)) โ โ) |
54 | | flge 13770 |
. . . . . . . . . 10
โข
((((logโ๐ด) /
(logโ๐)) โ
โ โง ๐ โ
โค) โ (๐ โค
((logโ๐ด) /
(logโ๐)) โ ๐ โค
(โโ((logโ๐ด) / (logโ๐))))) |
55 | 53, 25, 54 | syl2anc 585 |
. . . . . . . . 9
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ (๐ โค ((logโ๐ด) / (logโ๐)) โ ๐ โค (โโ((logโ๐ด) / (logโ๐))))) |
56 | 28, 52, 55 | 3bitrd 305 |
. . . . . . . 8
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ ((logโ(๐โ๐)) โค (logโ๐ด) โ ๐ โค (โโ((logโ๐ด) / (logโ๐))))) |
57 | 17 | adantr 482 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ (๐โ๐) โ โ) |
58 | 57 | nnrpd 13014 |
. . . . . . . . 9
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ (๐โ๐) โ
โ+) |
59 | 58, 45 | logled 26135 |
. . . . . . . 8
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ ((๐โ๐) โค ๐ด โ (logโ(๐โ๐)) โค (logโ๐ด))) |
60 | | simprr 772 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โ) |
61 | | nnuz 12865 |
. . . . . . . . . . 11
โข โ =
(โคโฅโ1) |
62 | 60, 61 | eleqtrdi 2844 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ
(โคโฅโ1)) |
63 | 62 | adantr 482 |
. . . . . . . . 9
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ ๐ โ
(โคโฅโ1)) |
64 | 53 | flcld 13763 |
. . . . . . . . 9
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ (โโ((logโ๐ด) / (logโ๐))) โ
โค) |
65 | | elfz5 13493 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ1) โง (โโ((logโ๐ด) / (logโ๐))) โ โค) โ
(๐ โ
(1...(โโ((logโ๐ด) / (logโ๐)))) โ ๐ โค (โโ((logโ๐ด) / (logโ๐))))) |
66 | 63, 64, 65 | syl2anc 585 |
. . . . . . . 8
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ (๐ โ (1...(โโ((logโ๐ด) / (logโ๐)))) โ ๐ โค (โโ((logโ๐ด) / (logโ๐))))) |
67 | 56, 59, 66 | 3bitr4d 311 |
. . . . . . 7
โข (((๐ โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ (0[,]๐ด)) โ ((๐โ๐) โค ๐ด โ ๐ โ (1...(โโ((logโ๐ด) / (logโ๐)))))) |
68 | 67 | pm5.32da 580 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((๐ โ (0[,]๐ด) โง (๐โ๐) โค ๐ด) โ (๐ โ (0[,]๐ด) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐))))))) |
69 | 14 | nncnd 12228 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โ) |
70 | 69 | exp1d 14106 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (๐โ1) = ๐) |
71 | 14 | nnge1d 12260 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ 1 โค ๐) |
72 | 32, 71, 62 | leexp2ad 14217 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (๐โ1) โค (๐โ๐)) |
73 | 70, 72 | eqbrtrrd 5173 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ๐ โค (๐โ๐)) |
74 | 17 | nnred 12227 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (๐โ๐) โ โ) |
75 | | letr 11308 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐โ๐) โ โ โง ๐ด โ โ) โ ((๐ โค (๐โ๐) โง (๐โ๐) โค ๐ด) โ ๐ โค ๐ด)) |
76 | 32, 74, 12, 75 | syl3anc 1372 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((๐ โค (๐โ๐) โง (๐โ๐) โค ๐ด) โ ๐ โค ๐ด)) |
77 | 73, 76 | mpand 694 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((๐โ๐) โค ๐ด โ ๐ โค ๐ด)) |
78 | 77, 42 | sylibrd 259 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((๐โ๐) โค ๐ด โ ๐ โ (0[,]๐ด))) |
79 | 78 | pm4.71rd 564 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((๐โ๐) โค ๐ด โ (๐ โ (0[,]๐ด) โง (๐โ๐) โค ๐ด))) |
80 | | elin 3965 |
. . . . . . . . 9
โข (๐ โ ((0[,]๐ด) โฉ โ) โ (๐ โ (0[,]๐ด) โง ๐ โ โ)) |
81 | 80 | rbaib 540 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โ ((0[,]๐ด) โฉ โ) โ ๐ โ (0[,]๐ด))) |
82 | 81 | ad2antrl 727 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (๐ โ ((0[,]๐ด) โฉ โ) โ ๐ โ (0[,]๐ด))) |
83 | 82 | anbi1d 631 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐))))) โ (๐ โ (0[,]๐ด) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐))))))) |
84 | 68, 79, 83 | 3bitr4rd 312 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐))))) โ (๐โ๐) โค ๐ด)) |
85 | 17, 61 | eleqtrdi 2844 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (๐โ๐) โ
(โคโฅโ1)) |
86 | 12 | flcld 13763 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (โโ๐ด) โ
โค) |
87 | | elfz5 13493 |
. . . . . 6
โข (((๐โ๐) โ (โคโฅโ1)
โง (โโ๐ด)
โ โค) โ ((๐โ๐) โ (1...(โโ๐ด)) โ (๐โ๐) โค (โโ๐ด))) |
88 | 85, 86, 87 | syl2anc 585 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((๐โ๐) โ (1...(โโ๐ด)) โ (๐โ๐) โค (โโ๐ด))) |
89 | 20, 84, 88 | 3bitr4d 311 |
. . . 4
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐))))) โ (๐โ๐) โ (1...(โโ๐ด)))) |
90 | 89 | pm5.32da 580 |
. . 3
โข (๐ โ (((๐ โ โ โง ๐ โ โ) โง (๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐)))))) โ ((๐ โ โ โง ๐ โ โ) โง (๐โ๐) โ (1...(โโ๐ด))))) |
91 | 11, 90 | bitrid 283 |
. 2
โข (๐ โ ((๐ โ ((0[,]๐ด) โฉ โ) โง ๐ โ (1...(โโ((logโ๐ด) / (logโ๐))))) โ ((๐ โ โ โง ๐ โ โ) โง (๐โ๐) โ (1...(โโ๐ด))))) |
92 | | fsumvma2.3 |
. 2
โข ((๐ โง ๐ฅ โ (1...(โโ๐ด))) โ ๐ต โ โ) |
93 | | fsumvma2.4 |
. 2
โข ((๐ โง (๐ฅ โ (1...(โโ๐ด)) โง (ฮโ๐ฅ) = 0)) โ ๐ต = 0) |
94 | 1, 2, 4, 7, 91, 92, 93 | fsumvma 26716 |
1
โข (๐ โ ฮฃ๐ฅ โ (1...(โโ๐ด))๐ต = ฮฃ๐ โ ((0[,]๐ด) โฉ โ)ฮฃ๐ โ (1...(โโ((logโ๐ด) / (logโ๐))))๐ถ) |