Step | Hyp | Ref
| Expression |
1 | | elin 3964 |
. . . . . 6
โข (๐ โ ((1...๐ด) โฉ โ) โ (๐ โ (1...๐ด) โง ๐ โ โ)) |
2 | 1 | baib 537 |
. . . . 5
โข (๐ โ (1...๐ด) โ (๐ โ ((1...๐ด) โฉ โ) โ ๐ โ โ)) |
3 | 2 | ifbid 4551 |
. . . 4
โข (๐ โ (1...๐ด) โ if(๐ โ ((1...๐ด) โฉ โ), (logโ(๐โ(๐ pCnt ๐ด))), 0) = if(๐ โ โ, (logโ(๐โ(๐ pCnt ๐ด))), 0)) |
4 | | fvif 6905 |
. . . . 5
โข
(logโif(๐
โ โ, (๐โ(๐ pCnt ๐ด)), 1)) = if(๐ โ โ, (logโ(๐โ(๐ pCnt ๐ด))), (logโ1)) |
5 | | log1 26086 |
. . . . . 6
โข
(logโ1) = 0 |
6 | | ifeq2 4533 |
. . . . . 6
โข
((logโ1) = 0 โ if(๐ โ โ, (logโ(๐โ(๐ pCnt ๐ด))), (logโ1)) = if(๐ โ โ, (logโ(๐โ(๐ pCnt ๐ด))), 0)) |
7 | 5, 6 | ax-mp 5 |
. . . . 5
โข if(๐ โ โ,
(logโ(๐โ(๐ pCnt ๐ด))), (logโ1)) = if(๐ โ โ, (logโ(๐โ(๐ pCnt ๐ด))), 0) |
8 | 4, 7 | eqtri 2761 |
. . . 4
โข
(logโif(๐
โ โ, (๐โ(๐ pCnt ๐ด)), 1)) = if(๐ โ โ, (logโ(๐โ(๐ pCnt ๐ด))), 0) |
9 | 3, 8 | eqtr4di 2791 |
. . 3
โข (๐ โ (1...๐ด) โ if(๐ โ ((1...๐ด) โฉ โ), (logโ(๐โ(๐ pCnt ๐ด))), 0) = (logโif(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1))) |
10 | 9 | sumeq2i 15642 |
. 2
โข
ฮฃ๐ โ
(1...๐ด)if(๐ โ ((1...๐ด) โฉ โ), (logโ(๐โ(๐ pCnt ๐ด))), 0) = ฮฃ๐ โ (1...๐ด)(logโif(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1)) |
11 | | inss1 4228 |
. . . 4
โข
((1...๐ด) โฉ
โ) โ (1...๐ด) |
12 | | simpr 486 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ ๐ โ ((1...๐ด) โฉ โ)) |
13 | 12 | elin1d 4198 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ ๐ โ (1...๐ด)) |
14 | | elfznn 13527 |
. . . . . . . . . 10
โข (๐ โ (1...๐ด) โ ๐ โ โ) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ ๐ โ โ) |
16 | 12 | elin2d 4199 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ ๐ โ โ) |
17 | | simpl 484 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ ๐ด โ โ) |
18 | 16, 17 | pccld 16780 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ (๐ pCnt ๐ด) โ
โ0) |
19 | 15, 18 | nnexpcld 14205 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ (๐โ(๐ pCnt ๐ด)) โ โ) |
20 | 19 | nnrpd 13011 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ (๐โ(๐ pCnt ๐ด)) โ
โ+) |
21 | 20 | relogcld 26123 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ (logโ(๐โ(๐ pCnt ๐ด))) โ โ) |
22 | 21 | recnd 11239 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ (logโ(๐โ(๐ pCnt ๐ด))) โ โ) |
23 | 22 | ralrimiva 3147 |
. . . 4
โข (๐ด โ โ โ
โ๐ โ
((1...๐ด) โฉ
โ)(logโ(๐โ(๐ pCnt ๐ด))) โ โ) |
24 | | fzfi 13934 |
. . . . . 6
โข
(1...๐ด) โ
Fin |
25 | 24 | olci 865 |
. . . . 5
โข
((1...๐ด) โ
(โคโฅโ1) โจ (1...๐ด) โ Fin) |
26 | | sumss2 15669 |
. . . . 5
โข
(((((1...๐ด) โฉ
โ) โ (1...๐ด)
โง โ๐ โ
((1...๐ด) โฉ
โ)(logโ(๐โ(๐ pCnt ๐ด))) โ โ) โง ((1...๐ด) โ
(โคโฅโ1) โจ (1...๐ด) โ Fin)) โ ฮฃ๐ โ ((1...๐ด) โฉ โ)(logโ(๐โ(๐ pCnt ๐ด))) = ฮฃ๐ โ (1...๐ด)if(๐ โ ((1...๐ด) โฉ โ), (logโ(๐โ(๐ pCnt ๐ด))), 0)) |
27 | 25, 26 | mpan2 690 |
. . . 4
โข
((((1...๐ด) โฉ
โ) โ (1...๐ด)
โง โ๐ โ
((1...๐ด) โฉ
โ)(logโ(๐โ(๐ pCnt ๐ด))) โ โ) โ ฮฃ๐ โ ((1...๐ด) โฉ โ)(logโ(๐โ(๐ pCnt ๐ด))) = ฮฃ๐ โ (1...๐ด)if(๐ โ ((1...๐ด) โฉ โ), (logโ(๐โ(๐ pCnt ๐ด))), 0)) |
28 | 11, 23, 27 | sylancr 588 |
. . 3
โข (๐ด โ โ โ
ฮฃ๐ โ ((1...๐ด) โฉ
โ)(logโ(๐โ(๐ pCnt ๐ด))) = ฮฃ๐ โ (1...๐ด)if(๐ โ ((1...๐ด) โฉ โ), (logโ(๐โ(๐ pCnt ๐ด))), 0)) |
29 | 15 | nnrpd 13011 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ ๐ โ โ+) |
30 | 18 | nn0zd 12581 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ (๐ pCnt ๐ด) โ โค) |
31 | | relogexp 26096 |
. . . . 5
โข ((๐ โ โ+
โง (๐ pCnt ๐ด) โ โค) โ
(logโ(๐โ(๐ pCnt ๐ด))) = ((๐ pCnt ๐ด) ยท (logโ๐))) |
32 | 29, 30, 31 | syl2anc 585 |
. . . 4
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ (logโ(๐โ(๐ pCnt ๐ด))) = ((๐ pCnt ๐ด) ยท (logโ๐))) |
33 | 32 | sumeq2dv 15646 |
. . 3
โข (๐ด โ โ โ
ฮฃ๐ โ ((1...๐ด) โฉ
โ)(logโ(๐โ(๐ pCnt ๐ด))) = ฮฃ๐ โ ((1...๐ด) โฉ โ)((๐ pCnt ๐ด) ยท (logโ๐))) |
34 | 28, 33 | eqtr3d 2775 |
. 2
โข (๐ด โ โ โ
ฮฃ๐ โ (1...๐ด)if(๐ โ ((1...๐ด) โฉ โ), (logโ(๐โ(๐ pCnt ๐ด))), 0) = ฮฃ๐ โ ((1...๐ด) โฉ โ)((๐ pCnt ๐ด) ยท (logโ๐))) |
35 | 14 | adantl 483 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ ๐ โ โ) |
36 | | eleq1w 2817 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ โ โ โ ๐ โ โ)) |
37 | | id 22 |
. . . . . . . . 9
โข (๐ = ๐ โ ๐ = ๐) |
38 | | oveq1 7413 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ pCnt ๐ด) = (๐ pCnt ๐ด)) |
39 | 37, 38 | oveq12d 7424 |
. . . . . . . 8
โข (๐ = ๐ โ (๐โ(๐ pCnt ๐ด)) = (๐โ(๐ pCnt ๐ด))) |
40 | 36, 39 | ifbieq1d 4552 |
. . . . . . 7
โข (๐ = ๐ โ if(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1) = if(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1)) |
41 | 40 | fveq2d 6893 |
. . . . . 6
โข (๐ = ๐ โ (logโif(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1)) = (logโif(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1))) |
42 | | eqid 2733 |
. . . . . 6
โข (๐ โ โ โฆ
(logโif(๐ โ
โ, (๐โ(๐ pCnt ๐ด)), 1))) = (๐ โ โ โฆ (logโif(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1))) |
43 | | fvex 6902 |
. . . . . 6
โข
(logโif(๐
โ โ, (๐โ(๐ pCnt ๐ด)), 1)) โ V |
44 | 41, 42, 43 | fvmpt 6996 |
. . . . 5
โข (๐ โ โ โ ((๐ โ โ โฆ
(logโif(๐ โ
โ, (๐โ(๐ pCnt ๐ด)), 1)))โ๐) = (logโif(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1))) |
45 | 35, 44 | syl 17 |
. . . 4
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ ((๐ โ โ โฆ (logโif(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1)))โ๐) = (logโif(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1))) |
46 | | elnnuz 12863 |
. . . . 5
โข (๐ด โ โ โ ๐ด โ
(โคโฅโ1)) |
47 | 46 | biimpi 215 |
. . . 4
โข (๐ด โ โ โ ๐ด โ
(โคโฅโ1)) |
48 | 35 | adantr 482 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ (1...๐ด)) โง ๐ โ โ) โ ๐ โ โ) |
49 | | simpr 486 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ (1...๐ด)) โง ๐ โ โ) โ ๐ โ โ) |
50 | | simpll 766 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ (1...๐ด)) โง ๐ โ โ) โ ๐ด โ โ) |
51 | 49, 50 | pccld 16780 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ (1...๐ด)) โง ๐ โ โ) โ (๐ pCnt ๐ด) โ
โ0) |
52 | 48, 51 | nnexpcld 14205 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ (1...๐ด)) โง ๐ โ โ) โ (๐โ(๐ pCnt ๐ด)) โ โ) |
53 | | 1nn 12220 |
. . . . . . . . 9
โข 1 โ
โ |
54 | 53 | a1i 11 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ (1...๐ด)) โง ยฌ ๐ โ โ) โ 1 โ
โ) |
55 | 52, 54 | ifclda 4563 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ if(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1) โ โ) |
56 | 55 | nnrpd 13011 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ if(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1) โ
โ+) |
57 | 56 | relogcld 26123 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (logโif(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1)) โ โ) |
58 | 57 | recnd 11239 |
. . . 4
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (logโif(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1)) โ โ) |
59 | 45, 47, 58 | fsumser 15673 |
. . 3
โข (๐ด โ โ โ
ฮฃ๐ โ (1...๐ด)(logโif(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1)) = (seq1( + , (๐ โ โ โฆ (logโif(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1))))โ๐ด)) |
60 | | rpmulcl 12994 |
. . . . 5
โข ((๐ โ โ+
โง ๐ โ
โ+) โ (๐ ยท ๐) โ
โ+) |
61 | 60 | adantl 483 |
. . . 4
โข ((๐ด โ โ โง (๐ โ โ+
โง ๐ โ
โ+)) โ (๐ ยท ๐) โ
โ+) |
62 | | eqid 2733 |
. . . . . . 7
โข (๐ โ โ โฆ if(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1)) = (๐ โ โ โฆ if(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1)) |
63 | | ovex 7439 |
. . . . . . . 8
โข (๐โ(๐ pCnt ๐ด)) โ V |
64 | | 1ex 11207 |
. . . . . . . 8
โข 1 โ
V |
65 | 63, 64 | ifex 4578 |
. . . . . . 7
โข if(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1) โ V |
66 | 40, 62, 65 | fvmpt 6996 |
. . . . . 6
โข (๐ โ โ โ ((๐ โ โ โฆ if(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1))โ๐) = if(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1)) |
67 | 35, 66 | syl 17 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ ((๐ โ โ โฆ if(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1))โ๐) = if(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1)) |
68 | 67, 56 | eqeltrd 2834 |
. . . 4
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ ((๐ โ โ โฆ if(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1))โ๐) โ
โ+) |
69 | | relogmul 26092 |
. . . . 5
โข ((๐ โ โ+
โง ๐ โ
โ+) โ (logโ(๐ ยท ๐)) = ((logโ๐) + (logโ๐))) |
70 | 69 | adantl 483 |
. . . 4
โข ((๐ด โ โ โง (๐ โ โ+
โง ๐ โ
โ+)) โ (logโ(๐ ยท ๐)) = ((logโ๐) + (logโ๐))) |
71 | 67 | fveq2d 6893 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (logโ((๐ โ โ โฆ if(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1))โ๐)) = (logโif(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1))) |
72 | 71, 45 | eqtr4d 2776 |
. . . 4
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (logโ((๐ โ โ โฆ if(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1))โ๐)) = ((๐ โ โ โฆ (logโif(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1)))โ๐)) |
73 | 61, 68, 47, 70, 72 | seqhomo 14012 |
. . 3
โข (๐ด โ โ โ
(logโ(seq1( ยท , (๐ โ โ โฆ if(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1)))โ๐ด)) = (seq1( + , (๐ โ โ โฆ (logโif(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1))))โ๐ด)) |
74 | 62 | pcprod 16825 |
. . . 4
โข (๐ด โ โ โ (seq1(
ยท , (๐ โ
โ โฆ if(๐ โ
โ, (๐โ(๐ pCnt ๐ด)), 1)))โ๐ด) = ๐ด) |
75 | 74 | fveq2d 6893 |
. . 3
โข (๐ด โ โ โ
(logโ(seq1( ยท , (๐ โ โ โฆ if(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1)))โ๐ด)) = (logโ๐ด)) |
76 | 59, 73, 75 | 3eqtr2d 2779 |
. 2
โข (๐ด โ โ โ
ฮฃ๐ โ (1...๐ด)(logโif(๐ โ โ, (๐โ(๐ pCnt ๐ด)), 1)) = (logโ๐ด)) |
77 | 10, 34, 76 | 3eqtr3a 2797 |
1
โข (๐ด โ โ โ
ฮฃ๐ โ ((1...๐ด) โฉ โ)((๐ pCnt ๐ด) ยท (logโ๐)) = (logโ๐ด)) |