Step | Hyp | Ref
| Expression |
1 | | 1red 11163 |
. . . . 5
β’ (((π β§ (πβ(πΏβπ)) = 1) β§ (ββ(πβπ΄)) β β) β 1 β
β) |
2 | | 0red 11165 |
. . . . 5
β’ (((π β§ (πβ(πΏβπ)) = 1) β§ Β¬ (ββ(πβπ΄)) β β) β 0 β
β) |
3 | 1, 2 | ifclda 4526 |
. . . 4
β’ ((π β§ (πβ(πΏβπ)) = 1) β if((ββ(πβπ΄)) β β, 1, 0) β
β) |
4 | | 1red 11163 |
. . . 4
β’ ((π β§ (πβ(πΏβπ)) = 1) β 1 β
β) |
5 | | fzfid 13885 |
. . . . . 6
β’ (π β (0...π΄) β Fin) |
6 | | dchrisum0flb.r |
. . . . . . . 8
β’ (π β π:(Baseβπ)βΆβ) |
7 | | rpvmasum.a |
. . . . . . . . . . 11
β’ (π β π β β) |
8 | 7 | nnnn0d 12480 |
. . . . . . . . . 10
β’ (π β π β
β0) |
9 | | rpvmasum.z |
. . . . . . . . . . 11
β’ π =
(β€/nβ€βπ) |
10 | | eqid 2737 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
11 | | rpvmasum.l |
. . . . . . . . . . 11
β’ πΏ = (β€RHomβπ) |
12 | 9, 10, 11 | znzrhfo 20970 |
. . . . . . . . . 10
β’ (π β β0
β πΏ:β€βontoβ(Baseβπ)) |
13 | | fof 6761 |
. . . . . . . . . 10
β’ (πΏ:β€βontoβ(Baseβπ) β πΏ:β€βΆ(Baseβπ)) |
14 | 8, 12, 13 | 3syl 18 |
. . . . . . . . 9
β’ (π β πΏ:β€βΆ(Baseβπ)) |
15 | | dchrisum0flblem1.1 |
. . . . . . . . . 10
β’ (π β π β β) |
16 | | prmz 16558 |
. . . . . . . . . 10
β’ (π β β β π β
β€) |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
β’ (π β π β β€) |
18 | 14, 17 | ffvelcdmd 7041 |
. . . . . . . 8
β’ (π β (πΏβπ) β (Baseβπ)) |
19 | 6, 18 | ffvelcdmd 7041 |
. . . . . . 7
β’ (π β (πβ(πΏβπ)) β β) |
20 | | elfznn0 13541 |
. . . . . . 7
β’ (π β (0...π΄) β π β β0) |
21 | | reexpcl 13991 |
. . . . . . 7
β’ (((πβ(πΏβπ)) β β β§ π β β0) β ((πβ(πΏβπ))βπ) β β) |
22 | 19, 20, 21 | syl2an 597 |
. . . . . 6
β’ ((π β§ π β (0...π΄)) β ((πβ(πΏβπ))βπ) β β) |
23 | 5, 22 | fsumrecl 15626 |
. . . . 5
β’ (π β Ξ£π β (0...π΄)((πβ(πΏβπ))βπ) β β) |
24 | 23 | adantr 482 |
. . . 4
β’ ((π β§ (πβ(πΏβπ)) = 1) β Ξ£π β (0...π΄)((πβ(πΏβπ))βπ) β β) |
25 | | breq1 5113 |
. . . . . 6
β’ (1 =
if((ββ(πβπ΄)) β β, 1, 0) β (1 β€ 1
β if((ββ(πβπ΄)) β β, 1, 0) β€
1)) |
26 | | breq1 5113 |
. . . . . 6
β’ (0 =
if((ββ(πβπ΄)) β β, 1, 0) β (0 β€ 1
β if((ββ(πβπ΄)) β β, 1, 0) β€
1)) |
27 | | 1le1 11790 |
. . . . . 6
β’ 1 β€
1 |
28 | | 0le1 11685 |
. . . . . 6
β’ 0 β€
1 |
29 | 25, 26, 27, 28 | keephyp 4562 |
. . . . 5
β’
if((ββ(πβπ΄)) β β, 1, 0) β€
1 |
30 | 29 | a1i 11 |
. . . 4
β’ ((π β§ (πβ(πΏβπ)) = 1) β if((ββ(πβπ΄)) β β, 1, 0) β€
1) |
31 | | dchrisum0flblem1.2 |
. . . . . . . . . 10
β’ (π β π΄ β
β0) |
32 | | nn0uz 12812 |
. . . . . . . . . 10
β’
β0 = (β€β₯β0) |
33 | 31, 32 | eleqtrdi 2848 |
. . . . . . . . 9
β’ (π β π΄ β
(β€β₯β0)) |
34 | | fzn0 13462 |
. . . . . . . . 9
β’
((0...π΄) β
β
β π΄ β
(β€β₯β0)) |
35 | 33, 34 | sylibr 233 |
. . . . . . . 8
β’ (π β (0...π΄) β β
) |
36 | | hashnncl 14273 |
. . . . . . . . 9
β’
((0...π΄) β Fin
β ((β―β(0...π΄)) β β β (0...π΄) β
β
)) |
37 | 5, 36 | syl 17 |
. . . . . . . 8
β’ (π β ((β―β(0...π΄)) β β β
(0...π΄) β
β
)) |
38 | 35, 37 | mpbird 257 |
. . . . . . 7
β’ (π β (β―β(0...π΄)) β
β) |
39 | 38 | adantr 482 |
. . . . . 6
β’ ((π β§ (πβ(πΏβπ)) = 1) β (β―β(0...π΄)) β
β) |
40 | 39 | nnge1d 12208 |
. . . . 5
β’ ((π β§ (πβ(πΏβπ)) = 1) β 1 β€
(β―β(0...π΄))) |
41 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ (πβ(πΏβπ)) = 1) β (πβ(πΏβπ)) = 1) |
42 | 41 | oveq1d 7377 |
. . . . . . . 8
β’ ((π β§ (πβ(πΏβπ)) = 1) β ((πβ(πΏβπ))βπ) = (1βπ)) |
43 | | elfzelz 13448 |
. . . . . . . . 9
β’ (π β (0...π΄) β π β β€) |
44 | | 1exp 14004 |
. . . . . . . . 9
β’ (π β β€ β
(1βπ) =
1) |
45 | 43, 44 | syl 17 |
. . . . . . . 8
β’ (π β (0...π΄) β (1βπ) = 1) |
46 | 42, 45 | sylan9eq 2797 |
. . . . . . 7
β’ (((π β§ (πβ(πΏβπ)) = 1) β§ π β (0...π΄)) β ((πβ(πΏβπ))βπ) = 1) |
47 | 46 | sumeq2dv 15595 |
. . . . . 6
β’ ((π β§ (πβ(πΏβπ)) = 1) β Ξ£π β (0...π΄)((πβ(πΏβπ))βπ) = Ξ£π β (0...π΄)1) |
48 | | fzfid 13885 |
. . . . . . 7
β’ ((π β§ (πβ(πΏβπ)) = 1) β (0...π΄) β Fin) |
49 | | ax-1cn 11116 |
. . . . . . 7
β’ 1 β
β |
50 | | fsumconst 15682 |
. . . . . . 7
β’
(((0...π΄) β Fin
β§ 1 β β) β Ξ£π β (0...π΄)1 = ((β―β(0...π΄)) Β· 1)) |
51 | 48, 49, 50 | sylancl 587 |
. . . . . 6
β’ ((π β§ (πβ(πΏβπ)) = 1) β Ξ£π β (0...π΄)1 = ((β―β(0...π΄)) Β· 1)) |
52 | 39 | nncnd 12176 |
. . . . . . 7
β’ ((π β§ (πβ(πΏβπ)) = 1) β (β―β(0...π΄)) β
β) |
53 | 52 | mulid1d 11179 |
. . . . . 6
β’ ((π β§ (πβ(πΏβπ)) = 1) β ((β―β(0...π΄)) Β· 1) =
(β―β(0...π΄))) |
54 | 47, 51, 53 | 3eqtrd 2781 |
. . . . 5
β’ ((π β§ (πβ(πΏβπ)) = 1) β Ξ£π β (0...π΄)((πβ(πΏβπ))βπ) = (β―β(0...π΄))) |
55 | 40, 54 | breqtrrd 5138 |
. . . 4
β’ ((π β§ (πβ(πΏβπ)) = 1) β 1 β€ Ξ£π β (0...π΄)((πβ(πΏβπ))βπ)) |
56 | 3, 4, 24, 30, 55 | letrd 11319 |
. . 3
β’ ((π β§ (πβ(πΏβπ)) = 1) β if((ββ(πβπ΄)) β β, 1, 0) β€ Ξ£π β (0...π΄)((πβ(πΏβπ))βπ)) |
57 | | oveq1 7369 |
. . . . . . 7
β’ (1 =
if((ββ(πβπ΄)) β β, 1, 0) β (1 Β·
(1 β (πβ(πΏβπ)))) = (if((ββ(πβπ΄)) β β, 1, 0) Β· (1 β
(πβ(πΏβπ))))) |
58 | 57 | breq1d 5120 |
. . . . . 6
β’ (1 =
if((ββ(πβπ΄)) β β, 1, 0) β ((1 Β·
(1 β (πβ(πΏβπ)))) β€ (1 β ((πβ(πΏβπ))β(π΄ + 1))) β (if((ββ(πβπ΄)) β β, 1, 0) Β· (1 β
(πβ(πΏβπ)))) β€ (1 β ((πβ(πΏβπ))β(π΄ + 1))))) |
59 | | oveq1 7369 |
. . . . . . 7
β’ (0 =
if((ββ(πβπ΄)) β β, 1, 0) β (0 Β·
(1 β (πβ(πΏβπ)))) = (if((ββ(πβπ΄)) β β, 1, 0) Β· (1 β
(πβ(πΏβπ))))) |
60 | 59 | breq1d 5120 |
. . . . . 6
β’ (0 =
if((ββ(πβπ΄)) β β, 1, 0) β ((0 Β·
(1 β (πβ(πΏβπ)))) β€ (1 β ((πβ(πΏβπ))β(π΄ + 1))) β (if((ββ(πβπ΄)) β β, 1, 0) Β· (1 β
(πβ(πΏβπ)))) β€ (1 β ((πβ(πΏβπ))β(π΄ + 1))))) |
61 | | 1re 11162 |
. . . . . . . . . 10
β’ 1 β
β |
62 | 19 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (πβ(πΏβπ)) β 1) β (πβ(πΏβπ)) β β) |
63 | | resubcl 11472 |
. . . . . . . . . 10
β’ ((1
β β β§ (πβ(πΏβπ)) β β) β (1 β (πβ(πΏβπ))) β β) |
64 | 61, 62, 63 | sylancr 588 |
. . . . . . . . 9
β’ ((π β§ (πβ(πΏβπ)) β 1) β (1 β (πβ(πΏβπ))) β β) |
65 | 64 | adantr 482 |
. . . . . . . 8
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β (1 β (πβ(πΏβπ))) β β) |
66 | 65 | leidd 11728 |
. . . . . . 7
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β (1 β (πβ(πΏβπ))) β€ (1 β (πβ(πΏβπ)))) |
67 | 64 | recnd 11190 |
. . . . . . . . 9
β’ ((π β§ (πβ(πΏβπ)) β 1) β (1 β (πβ(πΏβπ))) β β) |
68 | 67 | adantr 482 |
. . . . . . . 8
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β (1 β (πβ(πΏβπ))) β β) |
69 | 68 | mulid2d 11180 |
. . . . . . 7
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β (1 Β· (1
β (πβ(πΏβπ)))) = (1 β (πβ(πΏβπ)))) |
70 | | nn0p1nn 12459 |
. . . . . . . . . . . . 13
β’ (π΄ β β0
β (π΄ + 1) β
β) |
71 | 31, 70 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π΄ + 1) β β) |
72 | 71 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) = 0) β (π΄ + 1) β β) |
73 | 72 | 0expd 14051 |
. . . . . . . . . 10
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) = 0) β (0β(π΄ + 1)) = 0) |
74 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) = 0) β (πβ(πΏβπ)) = 0) |
75 | 74 | oveq1d 7377 |
. . . . . . . . . 10
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) = 0) β ((πβ(πΏβπ))β(π΄ + 1)) = (0β(π΄ + 1))) |
76 | 73, 75, 74 | 3eqtr4d 2787 |
. . . . . . . . 9
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) = 0) β ((πβ(πΏβπ))β(π΄ + 1)) = (πβ(πΏβπ))) |
77 | | neg1cn 12274 |
. . . . . . . . . . . . 13
β’ -1 β
β |
78 | 31 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β π΄ β
β0) |
79 | | expp1 13981 |
. . . . . . . . . . . . 13
β’ ((-1
β β β§ π΄
β β0) β (-1β(π΄ + 1)) = ((-1βπ΄) Β· -1)) |
80 | 77, 78, 79 | sylancr 588 |
. . . . . . . . . . . 12
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β (-1β(π΄ + 1)) = ((-1βπ΄) Β· -1)) |
81 | | prmnn 16557 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β π β
β) |
82 | 15, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β β) |
83 | 82, 31 | nnexpcld 14155 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (πβπ΄) β β) |
84 | 83 | nncnd 12176 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (πβπ΄) β β) |
85 | 84 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β (πβπ΄) β β) |
86 | 85 | sqsqrtd 15331 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β
((ββ(πβπ΄))β2) = (πβπ΄)) |
87 | 86 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β (π pCnt ((ββ(πβπ΄))β2)) = (π pCnt (πβπ΄))) |
88 | 15 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β π β β) |
89 | | nnq 12894 |
. . . . . . . . . . . . . . . . . . 19
β’
((ββ(πβπ΄)) β β β
(ββ(πβπ΄)) β β) |
90 | 89 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β
(ββ(πβπ΄)) β β) |
91 | | nnne0 12194 |
. . . . . . . . . . . . . . . . . . 19
β’
((ββ(πβπ΄)) β β β
(ββ(πβπ΄)) β 0) |
92 | 91 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β
(ββ(πβπ΄)) β 0) |
93 | | 2z 12542 |
. . . . . . . . . . . . . . . . . . 19
β’ 2 β
β€ |
94 | 93 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β 2 β
β€) |
95 | | pcexp 16738 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§
((ββ(πβπ΄)) β β β§
(ββ(πβπ΄)) β 0) β§ 2 β β€) β
(π pCnt
((ββ(πβπ΄))β2)) = (2 Β· (π pCnt (ββ(πβπ΄))))) |
96 | 88, 90, 92, 94, 95 | syl121anc 1376 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β (π pCnt ((ββ(πβπ΄))β2)) = (2 Β· (π pCnt (ββ(πβπ΄))))) |
97 | 78 | nn0zd 12532 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β π΄ β β€) |
98 | | pcid 16752 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π΄ β β€) β (π pCnt (πβπ΄)) = π΄) |
99 | 88, 97, 98 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β (π pCnt (πβπ΄)) = π΄) |
100 | 87, 96, 99 | 3eqtr3rd 2786 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β π΄ = (2 Β· (π pCnt (ββ(πβπ΄))))) |
101 | 100 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β (-1βπ΄) = (-1β(2 Β· (π pCnt (ββ(πβπ΄)))))) |
102 | 77 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β -1 β
β) |
103 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β
(ββ(πβπ΄)) β β) |
104 | 88, 103 | pccld 16729 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β (π pCnt (ββ(πβπ΄))) β
β0) |
105 | | 2nn0 12437 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
β0 |
106 | 105 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β 2 β
β0) |
107 | 102, 104,
106 | expmuld 14061 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β (-1β(2
Β· (π pCnt
(ββ(πβπ΄))))) = ((-1β2)β(π pCnt (ββ(πβπ΄))))) |
108 | | neg1sqe1 14107 |
. . . . . . . . . . . . . . . . 17
β’
(-1β2) = 1 |
109 | 108 | oveq1i 7372 |
. . . . . . . . . . . . . . . 16
β’
((-1β2)β(π
pCnt (ββ(πβπ΄)))) = (1β(π pCnt (ββ(πβπ΄)))) |
110 | 104 | nn0zd 12532 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β (π pCnt (ββ(πβπ΄))) β β€) |
111 | | 1exp 14004 |
. . . . . . . . . . . . . . . . 17
β’ ((π pCnt (ββ(πβπ΄))) β β€ β (1β(π pCnt (ββ(πβπ΄)))) = 1) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β (1β(π pCnt (ββ(πβπ΄)))) = 1) |
113 | 109, 112 | eqtrid 2789 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β
((-1β2)β(π pCnt
(ββ(πβπ΄)))) = 1) |
114 | 101, 107,
113 | 3eqtrd 2781 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β (-1βπ΄) = 1) |
115 | 114 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β ((-1βπ΄) Β· -1) = (1 Β·
-1)) |
116 | 77 | mulid2i 11167 |
. . . . . . . . . . . . 13
β’ (1
Β· -1) = -1 |
117 | 115, 116 | eqtrdi 2793 |
. . . . . . . . . . . 12
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β ((-1βπ΄) Β· -1) =
-1) |
118 | 80, 117 | eqtrd 2777 |
. . . . . . . . . . 11
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β (-1β(π΄ + 1)) = -1) |
119 | 118 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) β 0) β (-1β(π΄ + 1)) = -1) |
120 | 19 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’ (π β (πβ(πΏβπ)) β β) |
121 | 120 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (πβ(πΏβπ)) β 1) β (πβ(πΏβπ)) β β) |
122 | 121 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) β 0) β (πβ(πΏβπ)) β β) |
123 | 122 | negnegd 11510 |
. . . . . . . . . . . 12
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) β 0) β --(πβ(πΏβπ)) = (πβ(πΏβπ))) |
124 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (πβ(πΏβπ)) β 1) β (πβ(πΏβπ)) β 1) |
125 | 124 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) β 0) β (πβ(πΏβπ)) β 1) |
126 | | rpvmasum2.g |
. . . . . . . . . . . . . . . . . . 19
β’ πΊ = (DChrβπ) |
127 | | rpvmasum2.d |
. . . . . . . . . . . . . . . . . . 19
β’ π· = (BaseβπΊ) |
128 | | dchrisum0f.x |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β π·) |
129 | 128 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) β 0) β π β π·) |
130 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
β’
(Unitβπ) =
(Unitβπ) |
131 | 126, 9, 127, 10, 130, 128, 18 | dchrn0 26614 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((πβ(πΏβπ)) β 0 β (πΏβπ) β (Unitβπ))) |
132 | 131 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β ((πβ(πΏβπ)) β 0 β (πΏβπ) β (Unitβπ))) |
133 | 132 | biimpa 478 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) β 0) β (πΏβπ) β (Unitβπ)) |
134 | 126, 127,
129, 9, 130, 133 | dchrabs 26624 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) β 0) β (absβ(πβ(πΏβπ))) = 1) |
135 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . 18
β’
((absβ(πβ(πΏβπ))) = (πβ(πΏβπ)) β ((absβ(πβ(πΏβπ))) = 1 β (πβ(πΏβπ)) = 1)) |
136 | 134, 135 | syl5ibcom 244 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) β 0) β ((absβ(πβ(πΏβπ))) = (πβ(πΏβπ)) β (πβ(πΏβπ)) = 1)) |
137 | 136 | necon3ad 2957 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) β 0) β ((πβ(πΏβπ)) β 1 β Β¬ (absβ(πβ(πΏβπ))) = (πβ(πΏβπ)))) |
138 | 125, 137 | mpd 15 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) β 0) β Β¬ (absβ(πβ(πΏβπ))) = (πβ(πΏβπ))) |
139 | 62 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) β 0) β (πβ(πΏβπ)) β β) |
140 | 139 | absord 15307 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) β 0) β ((absβ(πβ(πΏβπ))) = (πβ(πΏβπ)) β¨ (absβ(πβ(πΏβπ))) = -(πβ(πΏβπ)))) |
141 | 140 | ord 863 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) β 0) β (Β¬ (absβ(πβ(πΏβπ))) = (πβ(πΏβπ)) β (absβ(πβ(πΏβπ))) = -(πβ(πΏβπ)))) |
142 | 138, 141 | mpd 15 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) β 0) β (absβ(πβ(πΏβπ))) = -(πβ(πΏβπ))) |
143 | 142, 134 | eqtr3d 2779 |
. . . . . . . . . . . . 13
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) β 0) β -(πβ(πΏβπ)) = 1) |
144 | 143 | negeqd 11402 |
. . . . . . . . . . . 12
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) β 0) β --(πβ(πΏβπ)) = -1) |
145 | 123, 144 | eqtr3d 2779 |
. . . . . . . . . . 11
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) β 0) β (πβ(πΏβπ)) = -1) |
146 | 145 | oveq1d 7377 |
. . . . . . . . . 10
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) β 0) β ((πβ(πΏβπ))β(π΄ + 1)) = (-1β(π΄ + 1))) |
147 | 119, 146,
145 | 3eqtr4d 2787 |
. . . . . . . . 9
β’ ((((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β§ (πβ(πΏβπ)) β 0) β ((πβ(πΏβπ))β(π΄ + 1)) = (πβ(πΏβπ))) |
148 | 76, 147 | pm2.61dane 3033 |
. . . . . . . 8
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β ((πβ(πΏβπ))β(π΄ + 1)) = (πβ(πΏβπ))) |
149 | 148 | oveq2d 7378 |
. . . . . . 7
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β (1 β ((πβ(πΏβπ))β(π΄ + 1))) = (1 β (πβ(πΏβπ)))) |
150 | 66, 69, 149 | 3brtr4d 5142 |
. . . . . 6
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ (ββ(πβπ΄)) β β) β (1 Β· (1
β (πβ(πΏβπ)))) β€ (1 β ((πβ(πΏβπ))β(π΄ + 1)))) |
151 | 67 | mul02d 11360 |
. . . . . . . 8
β’ ((π β§ (πβ(πΏβπ)) β 1) β (0 Β· (1 β
(πβ(πΏβπ)))) = 0) |
152 | | peano2nn0 12460 |
. . . . . . . . . . . . 13
β’ (π΄ β β0
β (π΄ + 1) β
β0) |
153 | 31, 152 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π΄ + 1) β
β0) |
154 | 19, 153 | reexpcld 14075 |
. . . . . . . . . . 11
β’ (π β ((πβ(πΏβπ))β(π΄ + 1)) β β) |
155 | 154 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (πβ(πΏβπ)) β 1) β ((πβ(πΏβπ))β(π΄ + 1)) β β) |
156 | 155 | recnd 11190 |
. . . . . . . . . . 11
β’ ((π β§ (πβ(πΏβπ)) β 1) β ((πβ(πΏβπ))β(π΄ + 1)) β β) |
157 | 156 | abscld 15328 |
. . . . . . . . . 10
β’ ((π β§ (πβ(πΏβπ)) β 1) β (absβ((πβ(πΏβπ))β(π΄ + 1))) β β) |
158 | | 1red 11163 |
. . . . . . . . . 10
β’ ((π β§ (πβ(πΏβπ)) β 1) β 1 β
β) |
159 | 155 | leabsd 15306 |
. . . . . . . . . 10
β’ ((π β§ (πβ(πΏβπ)) β 1) β ((πβ(πΏβπ))β(π΄ + 1)) β€ (absβ((πβ(πΏβπ))β(π΄ + 1)))) |
160 | 153 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (πβ(πΏβπ)) β 1) β (π΄ + 1) β
β0) |
161 | 121, 160 | absexpd 15344 |
. . . . . . . . . . 11
β’ ((π β§ (πβ(πΏβπ)) β 1) β (absβ((πβ(πΏβπ))β(π΄ + 1))) = ((absβ(πβ(πΏβπ)))β(π΄ + 1))) |
162 | 121 | abscld 15328 |
. . . . . . . . . . . 12
β’ ((π β§ (πβ(πΏβπ)) β 1) β (absβ(πβ(πΏβπ))) β β) |
163 | 121 | absge0d 15336 |
. . . . . . . . . . . 12
β’ ((π β§ (πβ(πΏβπ)) β 1) β 0 β€ (absβ(πβ(πΏβπ)))) |
164 | 126, 127,
9, 10, 128, 18 | dchrabs2 26626 |
. . . . . . . . . . . . 13
β’ (π β (absβ(πβ(πΏβπ))) β€ 1) |
165 | 164 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (πβ(πΏβπ)) β 1) β (absβ(πβ(πΏβπ))) β€ 1) |
166 | | exple1 14088 |
. . . . . . . . . . . 12
β’
((((absβ(πβ(πΏβπ))) β β β§ 0 β€
(absβ(πβ(πΏβπ))) β§ (absβ(πβ(πΏβπ))) β€ 1) β§ (π΄ + 1) β β0) β
((absβ(πβ(πΏβπ)))β(π΄ + 1)) β€ 1) |
167 | 162, 163,
165, 160, 166 | syl31anc 1374 |
. . . . . . . . . . 11
β’ ((π β§ (πβ(πΏβπ)) β 1) β ((absβ(πβ(πΏβπ)))β(π΄ + 1)) β€ 1) |
168 | 161, 167 | eqbrtrd 5132 |
. . . . . . . . . 10
β’ ((π β§ (πβ(πΏβπ)) β 1) β (absβ((πβ(πΏβπ))β(π΄ + 1))) β€ 1) |
169 | 155, 157,
158, 159, 168 | letrd 11319 |
. . . . . . . . 9
β’ ((π β§ (πβ(πΏβπ)) β 1) β ((πβ(πΏβπ))β(π΄ + 1)) β€ 1) |
170 | | subge0 11675 |
. . . . . . . . . 10
β’ ((1
β β β§ ((πβ(πΏβπ))β(π΄ + 1)) β β) β (0 β€ (1
β ((πβ(πΏβπ))β(π΄ + 1))) β ((πβ(πΏβπ))β(π΄ + 1)) β€ 1)) |
171 | 61, 155, 170 | sylancr 588 |
. . . . . . . . 9
β’ ((π β§ (πβ(πΏβπ)) β 1) β (0 β€ (1 β ((πβ(πΏβπ))β(π΄ + 1))) β ((πβ(πΏβπ))β(π΄ + 1)) β€ 1)) |
172 | 169, 171 | mpbird 257 |
. . . . . . . 8
β’ ((π β§ (πβ(πΏβπ)) β 1) β 0 β€ (1 β ((πβ(πΏβπ))β(π΄ + 1)))) |
173 | 151, 172 | eqbrtrd 5132 |
. . . . . . 7
β’ ((π β§ (πβ(πΏβπ)) β 1) β (0 Β· (1 β
(πβ(πΏβπ)))) β€ (1 β ((πβ(πΏβπ))β(π΄ + 1)))) |
174 | 173 | adantr 482 |
. . . . . 6
β’ (((π β§ (πβ(πΏβπ)) β 1) β§ Β¬ (ββ(πβπ΄)) β β) β (0 Β· (1
β (πβ(πΏβπ)))) β€ (1 β ((πβ(πΏβπ))β(π΄ + 1)))) |
175 | 58, 60, 150, 174 | ifbothda 4529 |
. . . . 5
β’ ((π β§ (πβ(πΏβπ)) β 1) β (if((ββ(πβπ΄)) β β, 1, 0) Β· (1 β
(πβ(πΏβπ)))) β€ (1 β ((πβ(πΏβπ))β(π΄ + 1)))) |
176 | | 0re 11164 |
. . . . . . . 8
β’ 0 β
β |
177 | 61, 176 | ifcli 4538 |
. . . . . . 7
β’
if((ββ(πβπ΄)) β β, 1, 0) β
β |
178 | 177 | a1i 11 |
. . . . . 6
β’ ((π β§ (πβ(πΏβπ)) β 1) β if((ββ(πβπ΄)) β β, 1, 0) β
β) |
179 | | resubcl 11472 |
. . . . . . 7
β’ ((1
β β β§ ((πβ(πΏβπ))β(π΄ + 1)) β β) β (1 β
((πβ(πΏβπ))β(π΄ + 1))) β β) |
180 | 61, 155, 179 | sylancr 588 |
. . . . . 6
β’ ((π β§ (πβ(πΏβπ)) β 1) β (1 β ((πβ(πΏβπ))β(π΄ + 1))) β β) |
181 | 62 | leabsd 15306 |
. . . . . . . . 9
β’ ((π β§ (πβ(πΏβπ)) β 1) β (πβ(πΏβπ)) β€ (absβ(πβ(πΏβπ)))) |
182 | 62, 162, 158, 181, 165 | letrd 11319 |
. . . . . . . 8
β’ ((π β§ (πβ(πΏβπ)) β 1) β (πβ(πΏβπ)) β€ 1) |
183 | 124 | necomd 3000 |
. . . . . . . 8
β’ ((π β§ (πβ(πΏβπ)) β 1) β 1 β (πβ(πΏβπ))) |
184 | 62, 158, 182, 183 | leneltd 11316 |
. . . . . . 7
β’ ((π β§ (πβ(πΏβπ)) β 1) β (πβ(πΏβπ)) < 1) |
185 | | posdif 11655 |
. . . . . . . 8
β’ (((πβ(πΏβπ)) β β β§ 1 β β)
β ((πβ(πΏβπ)) < 1 β 0 < (1 β (πβ(πΏβπ))))) |
186 | 62, 61, 185 | sylancl 587 |
. . . . . . 7
β’ ((π β§ (πβ(πΏβπ)) β 1) β ((πβ(πΏβπ)) < 1 β 0 < (1 β (πβ(πΏβπ))))) |
187 | 184, 186 | mpbid 231 |
. . . . . 6
β’ ((π β§ (πβ(πΏβπ)) β 1) β 0 < (1 β (πβ(πΏβπ)))) |
188 | | lemuldiv 12042 |
. . . . . 6
β’
((if((ββ(πβπ΄)) β β, 1, 0) β β
β§ (1 β ((πβ(πΏβπ))β(π΄ + 1))) β β β§ ((1 β
(πβ(πΏβπ))) β β β§ 0 < (1 β
(πβ(πΏβπ))))) β ((if((ββ(πβπ΄)) β β, 1, 0) Β· (1 β
(πβ(πΏβπ)))) β€ (1 β ((πβ(πΏβπ))β(π΄ + 1))) β if((ββ(πβπ΄)) β β, 1, 0) β€ ((1 β
((πβ(πΏβπ))β(π΄ + 1))) / (1 β (πβ(πΏβπ)))))) |
189 | 178, 180,
64, 187, 188 | syl112anc 1375 |
. . . . 5
β’ ((π β§ (πβ(πΏβπ)) β 1) β ((if((ββ(πβπ΄)) β β, 1, 0) Β· (1 β
(πβ(πΏβπ)))) β€ (1 β ((πβ(πΏβπ))β(π΄ + 1))) β if((ββ(πβπ΄)) β β, 1, 0) β€ ((1 β
((πβ(πΏβπ))β(π΄ + 1))) / (1 β (πβ(πΏβπ)))))) |
190 | 175, 189 | mpbid 231 |
. . . 4
β’ ((π β§ (πβ(πΏβπ)) β 1) β if((ββ(πβπ΄)) β β, 1, 0) β€ ((1 β
((πβ(πΏβπ))β(π΄ + 1))) / (1 β (πβ(πΏβπ))))) |
191 | 31 | nn0zd 12532 |
. . . . . . . 8
β’ (π β π΄ β β€) |
192 | | fzval3 13648 |
. . . . . . . 8
β’ (π΄ β β€ β
(0...π΄) = (0..^(π΄ + 1))) |
193 | 191, 192 | syl 17 |
. . . . . . 7
β’ (π β (0...π΄) = (0..^(π΄ + 1))) |
194 | 193 | adantr 482 |
. . . . . 6
β’ ((π β§ (πβ(πΏβπ)) β 1) β (0...π΄) = (0..^(π΄ + 1))) |
195 | 194 | sumeq1d 15593 |
. . . . 5
β’ ((π β§ (πβ(πΏβπ)) β 1) β Ξ£π β (0...π΄)((πβ(πΏβπ))βπ) = Ξ£π β (0..^(π΄ + 1))((πβ(πΏβπ))βπ)) |
196 | | 0nn0 12435 |
. . . . . . 7
β’ 0 β
β0 |
197 | 196 | a1i 11 |
. . . . . 6
β’ ((π β§ (πβ(πΏβπ)) β 1) β 0 β
β0) |
198 | 153, 32 | eleqtrdi 2848 |
. . . . . . 7
β’ (π β (π΄ + 1) β
(β€β₯β0)) |
199 | 198 | adantr 482 |
. . . . . 6
β’ ((π β§ (πβ(πΏβπ)) β 1) β (π΄ + 1) β
(β€β₯β0)) |
200 | 121, 124,
197, 199 | geoserg 15758 |
. . . . 5
β’ ((π β§ (πβ(πΏβπ)) β 1) β Ξ£π β (0..^(π΄ + 1))((πβ(πΏβπ))βπ) = ((((πβ(πΏβπ))β0) β ((πβ(πΏβπ))β(π΄ + 1))) / (1 β (πβ(πΏβπ))))) |
201 | 121 | exp0d 14052 |
. . . . . . 7
β’ ((π β§ (πβ(πΏβπ)) β 1) β ((πβ(πΏβπ))β0) = 1) |
202 | 201 | oveq1d 7377 |
. . . . . 6
β’ ((π β§ (πβ(πΏβπ)) β 1) β (((πβ(πΏβπ))β0) β ((πβ(πΏβπ))β(π΄ + 1))) = (1 β ((πβ(πΏβπ))β(π΄ + 1)))) |
203 | 202 | oveq1d 7377 |
. . . . 5
β’ ((π β§ (πβ(πΏβπ)) β 1) β ((((πβ(πΏβπ))β0) β ((πβ(πΏβπ))β(π΄ + 1))) / (1 β (πβ(πΏβπ)))) = ((1 β ((πβ(πΏβπ))β(π΄ + 1))) / (1 β (πβ(πΏβπ))))) |
204 | 195, 200,
203 | 3eqtrd 2781 |
. . . 4
β’ ((π β§ (πβ(πΏβπ)) β 1) β Ξ£π β (0...π΄)((πβ(πΏβπ))βπ) = ((1 β ((πβ(πΏβπ))β(π΄ + 1))) / (1 β (πβ(πΏβπ))))) |
205 | 190, 204 | breqtrrd 5138 |
. . 3
β’ ((π β§ (πβ(πΏβπ)) β 1) β if((ββ(πβπ΄)) β β, 1, 0) β€ Ξ£π β (0...π΄)((πβ(πΏβπ))βπ)) |
206 | 56, 205 | pm2.61dane 3033 |
. 2
β’ (π β if((ββ(πβπ΄)) β β, 1, 0) β€ Ξ£π β (0...π΄)((πβ(πΏβπ))βπ)) |
207 | | rpvmasum2.1 |
. . . . 5
β’ 1 =
(0gβπΊ) |
208 | | dchrisum0f.f |
. . . . 5
β’ πΉ = (π β β β¦ Ξ£π£ β {π β β β£ π β₯ π} (πβ(πΏβπ£))) |
209 | 9, 11, 7, 126, 127, 207, 208 | dchrisum0fval 26869 |
. . . 4
β’ ((πβπ΄) β β β (πΉβ(πβπ΄)) = Ξ£π β {π β β β£ π β₯ (πβπ΄)} (πβ(πΏβπ))) |
210 | 83, 209 | syl 17 |
. . 3
β’ (π β (πΉβ(πβπ΄)) = Ξ£π β {π β β β£ π β₯ (πβπ΄)} (πβ(πΏβπ))) |
211 | | 2fveq3 6852 |
. . . 4
β’ (π = (πβπ) β (πβ(πΏβπ)) = (πβ(πΏβ(πβπ)))) |
212 | | eqid 2737 |
. . . . . 6
β’ (π β (0...π΄) β¦ (πβπ)) = (π β (0...π΄) β¦ (πβπ)) |
213 | 212 | dvdsppwf1o 26551 |
. . . . 5
β’ ((π β β β§ π΄ β β0)
β (π β (0...π΄) β¦ (πβπ)):(0...π΄)β1-1-ontoβ{π β β β£ π β₯ (πβπ΄)}) |
214 | 15, 31, 213 | syl2anc 585 |
. . . 4
β’ (π β (π β (0...π΄) β¦ (πβπ)):(0...π΄)β1-1-ontoβ{π β β β£ π β₯ (πβπ΄)}) |
215 | | oveq2 7370 |
. . . . . 6
β’ (π = π β (πβπ) = (πβπ)) |
216 | | ovex 7395 |
. . . . . 6
β’ (πβπ) β V |
217 | 215, 212,
216 | fvmpt3i 6958 |
. . . . 5
β’ (π β (0...π΄) β ((π β (0...π΄) β¦ (πβπ))βπ) = (πβπ)) |
218 | 217 | adantl 483 |
. . . 4
β’ ((π β§ π β (0...π΄)) β ((π β (0...π΄) β¦ (πβπ))βπ) = (πβπ)) |
219 | 6 | adantr 482 |
. . . . . 6
β’ ((π β§ π β {π β β β£ π β₯ (πβπ΄)}) β π:(Baseβπ)βΆβ) |
220 | | elrabi 3644 |
. . . . . . . 8
β’ (π β {π β β β£ π β₯ (πβπ΄)} β π β β) |
221 | 220 | nnzd 12533 |
. . . . . . 7
β’ (π β {π β β β£ π β₯ (πβπ΄)} β π β β€) |
222 | | ffvelcdm 7037 |
. . . . . . 7
β’ ((πΏ:β€βΆ(Baseβπ) β§ π β β€) β (πΏβπ) β (Baseβπ)) |
223 | 14, 221, 222 | syl2an 597 |
. . . . . 6
β’ ((π β§ π β {π β β β£ π β₯ (πβπ΄)}) β (πΏβπ) β (Baseβπ)) |
224 | 219, 223 | ffvelcdmd 7041 |
. . . . 5
β’ ((π β§ π β {π β β β£ π β₯ (πβπ΄)}) β (πβ(πΏβπ)) β β) |
225 | 224 | recnd 11190 |
. . . 4
β’ ((π β§ π β {π β β β£ π β₯ (πβπ΄)}) β (πβ(πΏβπ)) β β) |
226 | 211, 5, 214, 218, 225 | fsumf1o 15615 |
. . 3
β’ (π β Ξ£π β {π β β β£ π β₯ (πβπ΄)} (πβ(πΏβπ)) = Ξ£π β (0...π΄)(πβ(πΏβ(πβπ)))) |
227 | | zsubrg 20866 |
. . . . . . . . . . 11
β’ β€
β (SubRingββfld) |
228 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(mulGrpββfld) =
(mulGrpββfld) |
229 | 228 | subrgsubm 20251 |
. . . . . . . . . . 11
β’ (β€
β (SubRingββfld) β β€ β
(SubMndβ(mulGrpββfld))) |
230 | 227, 229 | mp1i 13 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π΄)) β β€ β
(SubMndβ(mulGrpββfld))) |
231 | 20 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π΄)) β π β β0) |
232 | 17 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π΄)) β π β β€) |
233 | | eqid 2737 |
. . . . . . . . . . 11
β’
(.gβ(mulGrpββfld)) =
(.gβ(mulGrpββfld)) |
234 | | zringmpg 20908 |
. . . . . . . . . . . 12
β’
((mulGrpββfld) βΎs β€) =
(mulGrpββ€ring) |
235 | 234 | eqcomi 2746 |
. . . . . . . . . . 11
β’
(mulGrpββ€ring) =
((mulGrpββfld) βΎs
β€) |
236 | | eqid 2737 |
. . . . . . . . . . 11
β’
(.gβ(mulGrpββ€ring)) =
(.gβ(mulGrpββ€ring)) |
237 | 233, 235,
236 | submmulg 18927 |
. . . . . . . . . 10
β’ ((β€
β (SubMndβ(mulGrpββfld)) β§ π β β0
β§ π β β€)
β (π(.gβ(mulGrpββfld))π) = (π(.gβ(mulGrpββ€ring))π)) |
238 | 230, 231,
232, 237 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π β (0...π΄)) β (π(.gβ(mulGrpββfld))π) = (π(.gβ(mulGrpββ€ring))π)) |
239 | 82 | nncnd 12176 |
. . . . . . . . . 10
β’ (π β π β β) |
240 | | cnfldexp 20846 |
. . . . . . . . . 10
β’ ((π β β β§ π β β0)
β (π(.gβ(mulGrpββfld))π) = (πβπ)) |
241 | 239, 20, 240 | syl2an 597 |
. . . . . . . . 9
β’ ((π β§ π β (0...π΄)) β (π(.gβ(mulGrpββfld))π) = (πβπ)) |
242 | 238, 241 | eqtr3d 2779 |
. . . . . . . 8
β’ ((π β§ π β (0...π΄)) β (π(.gβ(mulGrpββ€ring))π) = (πβπ)) |
243 | 242 | fveq2d 6851 |
. . . . . . 7
β’ ((π β§ π β (0...π΄)) β (πΏβ(π(.gβ(mulGrpββ€ring))π)) = (πΏβ(πβπ))) |
244 | 9 | zncrng 20967 |
. . . . . . . . . . 11
β’ (π β β0
β π β
CRing) |
245 | | crngring 19983 |
. . . . . . . . . . 11
β’ (π β CRing β π β Ring) |
246 | 8, 244, 245 | 3syl 18 |
. . . . . . . . . 10
β’ (π β π β Ring) |
247 | 11 | zrhrhm 20928 |
. . . . . . . . . 10
β’ (π β Ring β πΏ β (β€ring
RingHom π)) |
248 | | eqid 2737 |
. . . . . . . . . . 11
β’
(mulGrpββ€ring) =
(mulGrpββ€ring) |
249 | | eqid 2737 |
. . . . . . . . . . 11
β’
(mulGrpβπ) =
(mulGrpβπ) |
250 | 248, 249 | rhmmhm 20162 |
. . . . . . . . . 10
β’ (πΏ β (β€ring
RingHom π) β πΏ β
((mulGrpββ€ring) MndHom (mulGrpβπ))) |
251 | 246, 247,
250 | 3syl 18 |
. . . . . . . . 9
β’ (π β πΏ β
((mulGrpββ€ring) MndHom (mulGrpβπ))) |
252 | 251 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0...π΄)) β πΏ β
((mulGrpββ€ring) MndHom (mulGrpβπ))) |
253 | | zringbas 20891 |
. . . . . . . . . 10
β’ β€ =
(Baseββ€ring) |
254 | 248, 253 | mgpbas 19909 |
. . . . . . . . 9
β’ β€ =
(Baseβ(mulGrpββ€ring)) |
255 | | eqid 2737 |
. . . . . . . . 9
β’
(.gβ(mulGrpβπ)) =
(.gβ(mulGrpβπ)) |
256 | 254, 236,
255 | mhmmulg 18924 |
. . . . . . . 8
β’ ((πΏ β
((mulGrpββ€ring) MndHom (mulGrpβπ)) β§ π β β0 β§ π β β€) β (πΏβ(π(.gβ(mulGrpββ€ring))π)) = (π(.gβ(mulGrpβπ))(πΏβπ))) |
257 | 252, 231,
232, 256 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π β (0...π΄)) β (πΏβ(π(.gβ(mulGrpββ€ring))π)) = (π(.gβ(mulGrpβπ))(πΏβπ))) |
258 | 243, 257 | eqtr3d 2779 |
. . . . . 6
β’ ((π β§ π β (0...π΄)) β (πΏβ(πβπ)) = (π(.gβ(mulGrpβπ))(πΏβπ))) |
259 | 258 | fveq2d 6851 |
. . . . 5
β’ ((π β§ π β (0...π΄)) β (πβ(πΏβ(πβπ))) = (πβ(π(.gβ(mulGrpβπ))(πΏβπ)))) |
260 | 126, 9, 127 | dchrmhm 26605 |
. . . . . . . 8
β’ π· β ((mulGrpβπ) MndHom
(mulGrpββfld)) |
261 | 260, 128 | sselid 3947 |
. . . . . . 7
β’ (π β π β ((mulGrpβπ) MndHom
(mulGrpββfld))) |
262 | 261 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (0...π΄)) β π β ((mulGrpβπ) MndHom
(mulGrpββfld))) |
263 | 18 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (0...π΄)) β (πΏβπ) β (Baseβπ)) |
264 | 249, 10 | mgpbas 19909 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβ(mulGrpβπ)) |
265 | 264, 255,
233 | mhmmulg 18924 |
. . . . . 6
β’ ((π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β§ π β β0 β§ (πΏβπ) β (Baseβπ)) β (πβ(π(.gβ(mulGrpβπ))(πΏβπ))) = (π(.gβ(mulGrpββfld))(πβ(πΏβπ)))) |
266 | 262, 231,
263, 265 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π β (0...π΄)) β (πβ(π(.gβ(mulGrpβπ))(πΏβπ))) = (π(.gβ(mulGrpββfld))(πβ(πΏβπ)))) |
267 | | cnfldexp 20846 |
. . . . . 6
β’ (((πβ(πΏβπ)) β β β§ π β β0) β (π(.gβ(mulGrpββfld))(πβ(πΏβπ)))
= ((πβ(πΏβπ))βπ)) |
268 | 120, 20, 267 | syl2an 597 |
. . . . 5
β’ ((π β§ π β (0...π΄)) β (π(.gβ(mulGrpββfld))(πβ(πΏβπ)))
= ((πβ(πΏβπ))βπ)) |
269 | 259, 266,
268 | 3eqtrd 2781 |
. . . 4
β’ ((π β§ π β (0...π΄)) β (πβ(πΏβ(πβπ))) = ((πβ(πΏβπ))βπ)) |
270 | 269 | sumeq2dv 15595 |
. . 3
β’ (π β Ξ£π β (0...π΄)(πβ(πΏβ(πβπ))) = Ξ£π β (0...π΄)((πβ(πΏβπ))βπ)) |
271 | 210, 226,
270 | 3eqtrd 2781 |
. 2
β’ (π β (πΉβ(πβπ΄)) = Ξ£π β (0...π΄)((πβ(πΏβπ))βπ)) |
272 | 206, 271 | breqtrrd 5138 |
1
β’ (π β if((ββ(πβπ΄)) β β, 1, 0) β€ (πΉβ(πβπ΄))) |