Step | Hyp | Ref
| Expression |
1 | | rpvmasum2.g |
. . . 4
β’ πΊ = (DChrβπ) |
2 | | rpvmasum.z |
. . . 4
β’ π =
(β€/nβ€βπ) |
3 | | rpvmasum2.d |
. . . 4
β’ π· = (BaseβπΊ) |
4 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
5 | | rpvmasum2.w |
. . . . . . 7
β’ π = {π¦ β (π· β { 1 }) β£ Ξ£π β β ((π¦β(πΏβπ)) / π) = 0} |
6 | 5 | ssrab3 4079 |
. . . . . 6
β’ π β (π· β { 1 }) |
7 | | dchrisum0.b |
. . . . . 6
β’ (π β π β π) |
8 | 6, 7 | sselid 3979 |
. . . . 5
β’ (π β π β (π· β { 1 })) |
9 | 8 | eldifad 3959 |
. . . 4
β’ (π β π β π·) |
10 | 1, 2, 3, 4, 9 | dchrf 26725 |
. . 3
β’ (π β π:(Baseβπ)βΆβ) |
11 | 10 | ffnd 6715 |
. 2
β’ (π β π Fn (Baseβπ)) |
12 | 10 | ffvelcdmda 7082 |
. . . 4
β’ ((π β§ π₯ β (Baseβπ)) β (πβπ₯) β β) |
13 | | fvco3 6986 |
. . . . . 6
β’ ((π:(Baseβπ)βΆβ β§ π₯ β (Baseβπ)) β ((β β π)βπ₯) = (ββ(πβπ₯))) |
14 | 10, 13 | sylan 581 |
. . . . 5
β’ ((π β§ π₯ β (Baseβπ)) β ((β β π)βπ₯) = (ββ(πβπ₯))) |
15 | | logno1 26126 |
. . . . . . . 8
β’ Β¬
(π₯ β
β+ β¦ (logβπ₯)) β π(1) |
16 | | 1red 11211 |
. . . . . . . . . . 11
β’ ((π β§ (β β π) β π) β 1 β β) |
17 | | rpvmasum.l |
. . . . . . . . . . . . 13
β’ πΏ = (β€RHomβπ) |
18 | | rpvmasum.a |
. . . . . . . . . . . . 13
β’ (π β π β β) |
19 | | rpvmasum2.1 |
. . . . . . . . . . . . 13
β’ 1 =
(0gβπΊ) |
20 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(Unitβπ) =
(Unitβπ) |
21 | 18 | nnnn0d 12528 |
. . . . . . . . . . . . . . . 16
β’ (π β π β
β0) |
22 | 2 | zncrng 21084 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β π β
CRing) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π β CRing) |
24 | | crngring 20059 |
. . . . . . . . . . . . . . 15
β’ (π β CRing β π β Ring) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π β Ring) |
26 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(1rβπ) = (1rβπ) |
27 | 20, 26 | 1unit 20177 |
. . . . . . . . . . . . . 14
β’ (π β Ring β
(1rβπ)
β (Unitβπ)) |
28 | 25, 27 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (1rβπ) β (Unitβπ)) |
29 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (β‘πΏ β {(1rβπ)}) = (β‘πΏ β {(1rβπ)}) |
30 | | eqidd 2734 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (1rβπ) = (1rβπ)) |
31 | 2, 17, 18, 1, 3, 19, 5, 20, 28, 29, 30 | rpvmasum2 26995 |
. . . . . . . . . . . 12
β’ (π β (π₯ β β+ β¦
(((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) β ((logβπ₯) Β· (1 β (β―βπ))))) β
π(1)) |
32 | 31 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (β β π) β π) β (π₯ β β+ β¦
(((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) β ((logβπ₯) Β· (1 β (β―βπ))))) β
π(1)) |
33 | 18 | phicld 16701 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (Οβπ) β
β) |
34 | 33 | nnnn0d 12528 |
. . . . . . . . . . . . . . . . 17
β’ (π β (Οβπ) β
β0) |
35 | 34 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β β+) β
(Οβπ) β
β0) |
36 | 35 | nn0red 12529 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β β+) β
(Οβπ) β
β) |
37 | | fzfid 13934 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β β+) β
(1...(ββπ₯))
β Fin) |
38 | | inss1 4227 |
. . . . . . . . . . . . . . . . 17
β’
((1...(ββπ₯)) β© (β‘πΏ β {(1rβπ)})) β
(1...(ββπ₯)) |
39 | | ssfi 9169 |
. . . . . . . . . . . . . . . . 17
β’
(((1...(ββπ₯)) β Fin β§
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)})) β
(1...(ββπ₯)))
β ((1...(ββπ₯)) β© (β‘πΏ β {(1rβπ)})) β
Fin) |
40 | 37, 38, 39 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β β+) β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)})) β
Fin) |
41 | | elinel1 4194 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)})) β π β (1...(ββπ₯))) |
42 | | elfznn 13526 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
(1...(ββπ₯))
β π β
β) |
43 | 42 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
44 | 41, 43 | sylan2 594 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))) β π β β) |
45 | | vmacl 26602 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β
(Ξβπ) β
β) |
46 | | nndivre 12249 |
. . . . . . . . . . . . . . . . . 18
β’
(((Ξβπ)
β β β§ π
β β) β ((Ξβπ) / π) β β) |
47 | 45, 46 | mpancom 687 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β
((Ξβπ) / π) β
β) |
48 | 44, 47 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))) β
((Ξβπ) / π) β
β) |
49 | 40, 48 | fsumrecl 15676 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β β+) β
Ξ£π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π) β β) |
50 | 36, 49 | remulcld 11240 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β
((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) β β) |
51 | | relogcl 26066 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β+
β (logβπ₯) β
β) |
52 | 51 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β β+) β
(logβπ₯) β
β) |
53 | | 1re 11210 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
β |
54 | 1, 3 | dchrfi 26738 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β π· β Fin) |
55 | 18, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π· β Fin) |
56 | | difss 4130 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π· β { 1 }) β π· |
57 | 6, 56 | sstri 3990 |
. . . . . . . . . . . . . . . . . . . 20
β’ π β π· |
58 | | ssfi 9169 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π· β Fin β§ π β π·) β π β Fin) |
59 | 55, 57, 58 | sylancl 587 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β Fin) |
60 | | hashcl 14312 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Fin β
(β―βπ) β
β0) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (β―βπ) β
β0) |
62 | 61 | nn0red 12529 |
. . . . . . . . . . . . . . . . 17
β’ (π β (β―βπ) β
β) |
63 | | resubcl 11520 |
. . . . . . . . . . . . . . . . 17
β’ ((1
β β β§ (β―βπ) β β) β (1 β
(β―βπ)) β
β) |
64 | 53, 62, 63 | sylancr 588 |
. . . . . . . . . . . . . . . 16
β’ (π β (1 β
(β―βπ)) β
β) |
65 | 64 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β β+) β (1
β (β―βπ))
β β) |
66 | 52, 65 | remulcld 11240 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β
((logβπ₯) Β· (1
β (β―βπ)))
β β) |
67 | 50, 66 | resubcld 11638 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β
(((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) β ((logβπ₯) Β· (1 β (β―βπ)))) β
β) |
68 | 67 | recnd 11238 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β
(((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) β ((logβπ₯) Β· (1 β (β―βπ)))) β
β) |
69 | 68 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ (β β π) β π) β§ π₯ β β+) β
(((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) β ((logβπ₯) Β· (1 β (β―βπ)))) β
β) |
70 | 51 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ (β β π) β π) β§ π₯ β β+) β
(logβπ₯) β
β) |
71 | 70 | recnd 11238 |
. . . . . . . . . . 11
β’ (((π β§ (β β π) β π) β§ π₯ β β+) β
(logβπ₯) β
β) |
72 | 51 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β (logβπ₯) β
β) |
73 | 66 | ad2ant2r 746 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
((logβπ₯) Β· (1
β (β―βπ)))
β β) |
74 | 72, 73 | readdcld 11239 |
. . . . . . . . . . . . . 14
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
((logβπ₯) +
((logβπ₯) Β· (1
β (β―βπ)))) β β) |
75 | | 0red 11213 |
. . . . . . . . . . . . . 14
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β 0 β
β) |
76 | 50 | ad2ant2r 746 |
. . . . . . . . . . . . . 14
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) β β) |
77 | | 2re 12282 |
. . . . . . . . . . . . . . . . . 18
β’ 2 β
β |
78 | 77 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β 2 β
β) |
79 | 62 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
(β―βπ) β
β) |
80 | 78, 79 | resubcld 11638 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β (2 β
(β―βπ)) β
β) |
81 | | log1 26076 |
. . . . . . . . . . . . . . . . 17
β’
(logβ1) = 0 |
82 | | simprr 772 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β 1 β€ π₯) |
83 | | 1rp 12974 |
. . . . . . . . . . . . . . . . . . 19
β’ 1 β
β+ |
84 | | simprl 770 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β π₯ β
β+) |
85 | | logleb 26093 |
. . . . . . . . . . . . . . . . . . 19
β’ ((1
β β+ β§ π₯ β β+) β (1 β€
π₯ β (logβ1) β€
(logβπ₯))) |
86 | 83, 84, 85 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β (1 β€ π₯ β (logβ1) β€
(logβπ₯))) |
87 | 82, 86 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β (logβ1)
β€ (logβπ₯)) |
88 | 81, 87 | eqbrtrrid 5183 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β 0 β€
(logβπ₯)) |
89 | 59 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β π β Fin) |
90 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(invgβπΊ) = (invgβπΊ) |
91 | 1, 3, 9, 90 | dchrinv 26744 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β
((invgβπΊ)βπ) = (β β π)) |
92 | 1 | dchrabl 26737 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β πΊ β Abel) |
93 | 18, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΊ β Abel) |
94 | | ablgrp 19646 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (πΊ β Abel β πΊ β Grp) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β πΊ β Grp) |
96 | 3, 90 | grpinvcl 18868 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΊ β Grp β§ π β π·) β ((invgβπΊ)βπ) β π·) |
97 | 95, 9, 96 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β
((invgβπΊ)βπ) β π·) |
98 | 91, 97 | eqeltrrd 2835 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (β β π) β π·) |
99 | | eldifsni 4792 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π· β { 1 }) β π β 1 ) |
100 | 8, 99 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β 1 ) |
101 | 3, 19 | grpidcl 18846 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (πΊ β Grp β 1 β π·) |
102 | 95, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β 1 β π·) |
103 | 3, 90, 95, 9, 102 | grpinv11 18888 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β
(((invgβπΊ)βπ) = ((invgβπΊ)β 1 ) β π = 1 )) |
104 | 103 | necon3bid 2986 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β
(((invgβπΊ)βπ) β ((invgβπΊ)β 1 ) β π β 1 )) |
105 | 100, 104 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β
((invgβπΊ)βπ) β ((invgβπΊ)β 1 )) |
106 | 19, 90 | grpinvid 18880 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πΊ β Grp β
((invgβπΊ)β 1 ) = 1 ) |
107 | 95, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β
((invgβπΊ)β 1 ) = 1 ) |
108 | 105, 91, 107 | 3netr3d 3018 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (β β π) β 1 ) |
109 | | eldifsn 4789 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β β π) β (π· β { 1 }) β ((β
β π) β π· β§ (β β π) β 1 )) |
110 | 98, 108, 109 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (β β π) β (π· β { 1 })) |
111 | | nnuz 12861 |
. . . . . . . . . . . . . . . . . . . . 21
β’ β =
(β€β₯β1) |
112 | | 1zzd 12589 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β 1 β
β€) |
113 | | 2fveq3 6893 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = π β (πβ(πΏβπ)) = (πβ(πΏβπ))) |
114 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = π β π = π) |
115 | 113, 114 | oveq12d 7422 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = π β ((πβ(πΏβπ)) / π) = ((πβ(πΏβπ)) / π)) |
116 | 115 | fveq2d 6892 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β (ββ((πβ(πΏβπ)) / π)) = (ββ((πβ(πΏβπ)) / π))) |
117 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β¦
(ββ((πβ(πΏβπ)) / π))) = (π β β β¦
(ββ((πβ(πΏβπ)) / π))) |
118 | | fvex 6901 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(ββ((πβ(πΏβπ)) / π)) β V |
119 | 116, 117,
118 | fvmpt 6994 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β ((π β β β¦
(ββ((πβ(πΏβπ)) / π)))βπ) = (ββ((πβ(πΏβπ)) / π))) |
120 | 119 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β) β ((π β β β¦
(ββ((πβ(πΏβπ)) / π)))βπ) = (ββ((πβ(πΏβπ)) / π))) |
121 | | nnre 12215 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β β π β
β) |
122 | 121 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β β) β π β β) |
123 | 122 | cjred 15169 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β (ββπ) = π) |
124 | 123 | oveq2d 7420 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β) β
((ββ(πβ(πΏβπ))) / (ββπ)) = ((ββ(πβ(πΏβπ))) / π)) |
125 | 10 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β β) β π:(Baseβπ)βΆβ) |
126 | 2, 4, 17 | znzrhfo 21087 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β β0
β πΏ:β€βontoβ(Baseβπ)) |
127 | 21, 126 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β πΏ:β€βontoβ(Baseβπ)) |
128 | | fof 6802 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (πΏ:β€βontoβ(Baseβπ) β πΏ:β€βΆ(Baseβπ)) |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β πΏ:β€βΆ(Baseβπ)) |
130 | | nnz 12575 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β β π β
β€) |
131 | | ffvelcdm 7079 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΏ:β€βΆ(Baseβπ) β§ π β β€) β (πΏβπ) β (Baseβπ)) |
132 | 129, 130,
131 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β β) β (πΏβπ) β (Baseβπ)) |
133 | 125, 132 | ffvelcdmd 7083 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β (πβ(πΏβπ)) β β) |
134 | | nncn 12216 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β π β
β) |
135 | 134 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β π β β) |
136 | | nnne0 12242 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β π β 0) |
137 | 136 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β π β 0) |
138 | 133, 135,
137 | cjdivd 15166 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β) β
(ββ((πβ(πΏβπ)) / π)) = ((ββ(πβ(πΏβπ))) / (ββπ))) |
139 | | fvco3 6986 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π:(Baseβπ)βΆβ β§ (πΏβπ) β (Baseβπ)) β ((β β π)β(πΏβπ)) = (ββ(πβ(πΏβπ)))) |
140 | 125, 132,
139 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β ((β β
π)β(πΏβπ)) = (ββ(πβ(πΏβπ)))) |
141 | 140 | oveq1d 7419 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β) β (((β β
π)β(πΏβπ)) / π) = ((ββ(πβ(πΏβπ))) / π)) |
142 | 124, 138,
141 | 3eqtr4d 2783 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β) β
(ββ((πβ(πΏβπ)) / π)) = (((β β π)β(πΏβπ)) / π)) |
143 | 120, 142 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β ((π β β β¦
(ββ((πβ(πΏβπ)) / π)))βπ) = (((β β π)β(πΏβπ)) / π)) |
144 | 133 | cjcld 15139 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β) β
(ββ(πβ(πΏβπ))) β β) |
145 | 144, 135,
137 | divcld 11986 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β) β
((ββ(πβ(πΏβπ))) / π) β β) |
146 | 141, 145 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β (((β β
π)β(πΏβπ)) / π) β β) |
147 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β¦ ((πβ(πΏβπ)) / π)) = (π β β β¦ ((πβ(πΏβπ)) / π)) |
148 | 2, 17, 18, 1, 3, 19, 9, 100, 147 | dchrmusumlema 26976 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β βπ‘βπ β (0[,)+β)(seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦))) |
149 | | simprrl 780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π))) β π‘) |
150 | 7 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β π β π) |
151 | 18 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β π β β) |
152 | 9 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β π β π·) |
153 | 100 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β π β 1 ) |
154 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β π β (0[,)+β)) |
155 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)) |
156 | 2, 17, 151, 1, 3, 19, 152, 153, 147, 154, 149, 155, 5 | dchrvmaeq0 26987 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β (π β π β π‘ = 0)) |
157 | 150, 156 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β π‘ = 0) |
158 | 149, 157 | breqtrd 5173 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π))) β 0) |
159 | 158 | rexlimdvaa 3157 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (βπ β (0[,)+β)(seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)) β seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π))) β 0)) |
160 | 159 | exlimdv 1937 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (βπ‘βπ β (0[,)+β)(seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)) β seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π))) β 0)) |
161 | 148, 160 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π))) β 0) |
162 | | seqex 13964 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ seq1( + ,
(π β β β¦
(ββ((πβ(πΏβπ)) / π)))) β V |
163 | 162 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β seq1( + , (π β β β¦
(ββ((πβ(πΏβπ)) / π)))) β V) |
164 | | 2fveq3 6893 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = π β (πβ(πΏβπ)) = (πβ(πΏβπ))) |
165 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = π β π = π) |
166 | 164, 165 | oveq12d 7422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = π β ((πβ(πΏβπ)) / π) = ((πβ(πΏβπ)) / π)) |
167 | | ovex 7437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((πβ(πΏβπ)) / π) β V |
168 | 166, 147,
167 | fvmpt 6994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β β ((π β β β¦ ((πβ(πΏβπ)) / π))βπ) = ((πβ(πΏβπ)) / π)) |
169 | 168 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β β) β ((π β β β¦ ((πβ(πΏβπ)) / π))βπ) = ((πβ(πΏβπ)) / π)) |
170 | 133, 135,
137 | divcld 11986 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β β) β ((πβ(πΏβπ)) / π) β β) |
171 | 169, 170 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β β) β ((π β β β¦ ((πβ(πΏβπ)) / π))βπ) β β) |
172 | 111, 112,
171 | serf 13992 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π))):ββΆβ) |
173 | 172 | ffvelcdmda 7082 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β) β (seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π)))βπ) β β) |
174 | | fzfid 13934 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β β) β (1...π) β Fin) |
175 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β β) β π) |
176 | | elfznn 13526 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (1...π) β π β β) |
177 | 175, 176,
170 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β β) β§ π β (1...π)) β ((πβ(πΏβπ)) / π) β β) |
178 | 174, 177 | fsumcj 15752 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β
(ββΞ£π
β (1...π)((πβ(πΏβπ)) / π)) = Ξ£π β (1...π)(ββ((πβ(πΏβπ)) / π))) |
179 | 175, 176,
169 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β β) β§ π β (1...π)) β ((π β β β¦ ((πβ(πΏβπ)) / π))βπ) = ((πβ(πΏβπ)) / π)) |
180 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π β β) β π β β) |
181 | 180, 111 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β β) β π β
(β€β₯β1)) |
182 | 179, 181,
177 | fsumser 15672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β β) β Ξ£π β (1...π)((πβ(πΏβπ)) / π) = (seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π)))βπ)) |
183 | 182 | fveq2d 6892 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β
(ββΞ£π
β (1...π)((πβ(πΏβπ)) / π)) = (ββ(seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π)))βπ))) |
184 | 175, 176,
120 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β β) β§ π β (1...π)) β ((π β β β¦
(ββ((πβ(πΏβπ)) / π)))βπ) = (ββ((πβ(πΏβπ)) / π))) |
185 | 170 | cjcld 15139 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β β) β
(ββ((πβ(πΏβπ)) / π)) β β) |
186 | 175, 176,
185 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β β) β§ π β (1...π)) β (ββ((πβ(πΏβπ)) / π)) β β) |
187 | 184, 181,
186 | fsumser 15672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β Ξ£π β (1...π)(ββ((πβ(πΏβπ)) / π)) = (seq1( + , (π β β β¦
(ββ((πβ(πΏβπ)) / π))))βπ)) |
188 | 178, 183,
187 | 3eqtr3rd 2782 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β) β (seq1( + , (π β β β¦
(ββ((πβ(πΏβπ)) / π))))βπ) = (ββ(seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π)))βπ))) |
189 | 111, 161,
163, 112, 173, 188 | climcj 15545 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β seq1( + , (π β β β¦
(ββ((πβ(πΏβπ)) / π)))) β
(ββ0)) |
190 | | cj0 15101 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(ββ0) = 0 |
191 | 189, 190 | breqtrdi 5188 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β seq1( + , (π β β β¦
(ββ((πβ(πΏβπ)) / π)))) β 0) |
192 | 111, 112,
143, 146, 191 | isumclim 15699 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β Ξ£π β β (((β β π)β(πΏβπ)) / π) = 0) |
193 | | fveq1 6887 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π¦ = (β β π) β (π¦β(πΏβπ)) = ((β β π)β(πΏβπ))) |
194 | 193 | oveq1d 7419 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π¦ = (β β π) β ((π¦β(πΏβπ)) / π) = (((β β π)β(πΏβπ)) / π)) |
195 | 194 | sumeq2sdv 15646 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ = (β β π) β Ξ£π β β ((π¦β(πΏβπ)) / π) = Ξ£π β β (((β β π)β(πΏβπ)) / π)) |
196 | 195 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ = (β β π) β (Ξ£π β β ((π¦β(πΏβπ)) / π) = 0 β Ξ£π β β (((β β π)β(πΏβπ)) / π) = 0)) |
197 | 196, 5 | elrab2 3685 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β β π) β π β ((β β π) β (π· β { 1 }) β§ Ξ£π β β (((β
β π)β(πΏβπ)) / π) = 0)) |
198 | 110, 192,
197 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (β β π) β π) |
199 | 198 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β (β
β π) β π) |
200 | 7 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β π β π) |
201 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β (β
β π) β π) |
202 | 89, 199, 200, 201 | nehash2 14431 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β 2 β€
(β―βπ)) |
203 | | suble0 11724 |
. . . . . . . . . . . . . . . . . 18
β’ ((2
β β β§ (β―βπ) β β) β ((2 β
(β―βπ)) β€ 0
β 2 β€ (β―βπ))) |
204 | 77, 79, 203 | sylancr 588 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β ((2 β
(β―βπ)) β€ 0
β 2 β€ (β―βπ))) |
205 | 202, 204 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β (2 β
(β―βπ)) β€
0) |
206 | 80, 75, 72, 88, 205 | lemul2ad 12150 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
((logβπ₯) Β· (2
β (β―βπ)))
β€ ((logβπ₯)
Β· 0)) |
207 | | df-2 12271 |
. . . . . . . . . . . . . . . . . . 19
β’ 2 = (1 +
1) |
208 | 207 | oveq1i 7414 |
. . . . . . . . . . . . . . . . . 18
β’ (2
β (β―βπ))
= ((1 + 1) β (β―βπ)) |
209 | | 1cnd 11205 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β 1 β
β) |
210 | 79 | recnd 11238 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
(β―βπ) β
β) |
211 | 209, 209,
210 | addsubassd 11587 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β ((1 + 1) β
(β―βπ)) = (1 +
(1 β (β―βπ)))) |
212 | 208, 211 | eqtrid 2785 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β (2 β
(β―βπ)) = (1 +
(1 β (β―βπ)))) |
213 | 212 | oveq2d 7420 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
((logβπ₯) Β· (2
β (β―βπ)))
= ((logβπ₯) Β·
(1 + (1 β (β―βπ))))) |
214 | 71 | adantrr 716 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β (logβπ₯) β
β) |
215 | 64 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β (1 β
(β―βπ)) β
β) |
216 | 215 | recnd 11238 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β (1 β
(β―βπ)) β
β) |
217 | 214, 209,
216 | adddid 11234 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
((logβπ₯) Β· (1
+ (1 β (β―βπ)))) = (((logβπ₯) Β· 1) + ((logβπ₯) Β· (1 β
(β―βπ))))) |
218 | 214 | mulridd 11227 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
((logβπ₯) Β· 1)
= (logβπ₯)) |
219 | 218 | oveq1d 7419 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
(((logβπ₯) Β· 1)
+ ((logβπ₯) Β·
(1 β (β―βπ)))) = ((logβπ₯) + ((logβπ₯) Β· (1 β (β―βπ))))) |
220 | 213, 217,
219 | 3eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
((logβπ₯) Β· (2
β (β―βπ)))
= ((logβπ₯) +
((logβπ₯) Β· (1
β (β―βπ))))) |
221 | 214 | mul01d 11409 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
((logβπ₯) Β· 0)
= 0) |
222 | 206, 220,
221 | 3brtr3d 5178 |
. . . . . . . . . . . . . 14
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
((logβπ₯) +
((logβπ₯) Β· (1
β (β―βπ)))) β€ 0) |
223 | 33 | nnred 12223 |
. . . . . . . . . . . . . . . 16
β’ (π β (Οβπ) β
β) |
224 | 223 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
(Οβπ) β
β) |
225 | 49 | ad2ant2r 746 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π) β β) |
226 | 34 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
(Οβπ) β
β0) |
227 | 226 | nn0ge0d 12531 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β 0 β€
(Οβπ)) |
228 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))) β
(Ξβπ) β
β) |
229 | | vmage0 26605 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β 0 β€
(Ξβπ)) |
230 | 44, 229 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))) β 0 β€
(Ξβπ)) |
231 | 44 | nnred 12223 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))) β π β β) |
232 | 44 | nngt0d 12257 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))) β 0 < π) |
233 | | divge0 12079 |
. . . . . . . . . . . . . . . . . 18
β’
((((Ξβπ) β β β§ 0 β€
(Ξβπ)) β§
(π β β β§ 0
< π)) β 0 β€
((Ξβπ) / π)) |
234 | 228, 230,
231, 232, 233 | syl22anc 838 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))) β 0 β€
((Ξβπ) / π)) |
235 | 40, 48, 234 | fsumge0 15737 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β β+) β 0 β€
Ξ£π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) |
236 | 235 | ad2ant2r 746 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β 0 β€
Ξ£π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) |
237 | 224, 225,
227, 236 | mulge0d 11787 |
. . . . . . . . . . . . . 14
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β 0 β€
((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π))) |
238 | 74, 75, 76, 222, 237 | letrd 11367 |
. . . . . . . . . . . . 13
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
((logβπ₯) +
((logβπ₯) Β· (1
β (β―βπ)))) β€ ((Οβπ) Β· Ξ£π β ((1...(ββπ₯)) β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π))) |
239 | | leaddsub 11686 |
. . . . . . . . . . . . . 14
β’
(((logβπ₯)
β β β§ ((logβπ₯) Β· (1 β (β―βπ))) β β β§
((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) β β) β (((logβπ₯) + ((logβπ₯) Β· (1 β
(β―βπ)))) β€
((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) β (logβπ₯) β€ (((Οβπ) Β· Ξ£π β ((1...(ββπ₯)) β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) β ((logβπ₯) Β· (1 β (β―βπ)))))) |
240 | 72, 73, 76, 239 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
(((logβπ₯) +
((logβπ₯) Β· (1
β (β―βπ)))) β€ ((Οβπ) Β· Ξ£π β ((1...(ββπ₯)) β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) β (logβπ₯) β€ (((Οβπ) Β· Ξ£π β ((1...(ββπ₯)) β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) β ((logβπ₯) Β· (1 β (β―βπ)))))) |
241 | 238, 240 | mpbid 231 |
. . . . . . . . . . . 12
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β (logβπ₯) β€ (((Οβπ) Β· Ξ£π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) β ((logβπ₯) Β· (1 β (β―βπ))))) |
242 | 72, 88 | absidd 15365 |
. . . . . . . . . . . 12
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβ(logβπ₯)) =
(logβπ₯)) |
243 | 67 | ad2ant2r 746 |
. . . . . . . . . . . . 13
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
(((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) β ((logβπ₯) Β· (1 β (β―βπ)))) β
β) |
244 | 75, 72, 243, 88, 241 | letrd 11367 |
. . . . . . . . . . . . 13
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β 0 β€
(((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) β ((logβπ₯) Β· (1 β (β―βπ))))) |
245 | 243, 244 | absidd 15365 |
. . . . . . . . . . . 12
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβ(((Οβπ) Β· Ξ£π β ((1...(ββπ₯)) β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) β ((logβπ₯) Β· (1 β (β―βπ))))) = (((Οβπ) Β· Ξ£π β
((1...(ββπ₯))
β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) β ((logβπ₯) Β· (1 β (β―βπ))))) |
246 | 241, 242,
245 | 3brtr4d 5179 |
. . . . . . . . . . 11
β’ (((π β§ (β β π) β π) β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβ(logβπ₯))
β€ (absβ(((Οβπ) Β· Ξ£π β ((1...(ββπ₯)) β© (β‘πΏ β {(1rβπ)}))((Ξβπ) / π)) β ((logβπ₯) Β· (1 β (β―βπ)))))) |
247 | 16, 32, 69, 71, 246 | o1le 15595 |
. . . . . . . . . 10
β’ ((π β§ (β β π) β π) β (π₯ β β+ β¦
(logβπ₯)) β
π(1)) |
248 | 247 | ex 414 |
. . . . . . . . 9
β’ (π β ((β β π) β π β (π₯ β β+ β¦
(logβπ₯)) β
π(1))) |
249 | 248 | necon1bd 2959 |
. . . . . . . 8
β’ (π β (Β¬ (π₯ β β+ β¦
(logβπ₯)) β
π(1) β (β β π) = π)) |
250 | 15, 249 | mpi 20 |
. . . . . . 7
β’ (π β (β β π) = π) |
251 | 250 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβπ)) β (β β π) = π) |
252 | 251 | fveq1d 6890 |
. . . . 5
β’ ((π β§ π₯ β (Baseβπ)) β ((β β π)βπ₯) = (πβπ₯)) |
253 | 14, 252 | eqtr3d 2775 |
. . . 4
β’ ((π β§ π₯ β (Baseβπ)) β (ββ(πβπ₯)) = (πβπ₯)) |
254 | 12, 253 | cjrebd 15145 |
. . 3
β’ ((π β§ π₯ β (Baseβπ)) β (πβπ₯) β β) |
255 | 254 | ralrimiva 3147 |
. 2
β’ (π β βπ₯ β (Baseβπ)(πβπ₯) β β) |
256 | | ffnfv 7113 |
. 2
β’ (π:(Baseβπ)βΆβ β (π Fn (Baseβπ) β§ βπ₯ β (Baseβπ)(πβπ₯) β β)) |
257 | 11, 255, 256 | sylanbrc 584 |
1
β’ (π β π:(Baseβπ)βΆβ) |