Step | Hyp | Ref
| Expression |
1 | | mulrid 7953 |
. . 3
β’ (π β β β (π Β· 1) = π) |
2 | 1 | adantl 277 |
. 2
β’ ((π β§ π β β) β (π Β· 1) = π) |
3 | | lgsdilem2.2 |
. . . 4
β’ (π β π β β€) |
4 | | lgsdilem2.4 |
. . . 4
β’ (π β π β 0) |
5 | | nnabscl 11108 |
. . . 4
β’ ((π β β€ β§ π β 0) β (absβπ) β
β) |
6 | 3, 4, 5 | syl2anc 411 |
. . 3
β’ (π β (absβπ) β
β) |
7 | | nnuz 9562 |
. . 3
β’ β =
(β€β₯β1) |
8 | 6, 7 | eleqtrdi 2270 |
. 2
β’ (π β (absβπ) β
(β€β₯β1)) |
9 | 6 | nnzd 9373 |
. . 3
β’ (π β (absβπ) β
β€) |
10 | | lgsdilem2.3 |
. . . . . 6
β’ (π β π β β€) |
11 | 3, 10 | zmulcld 9380 |
. . . . 5
β’ (π β (π Β· π) β β€) |
12 | 3 | zcnd 9375 |
. . . . . . 7
β’ (π β π β β) |
13 | 10 | zcnd 9375 |
. . . . . . 7
β’ (π β π β β) |
14 | | 0z 9263 |
. . . . . . . . 9
β’ 0 β
β€ |
15 | | zapne 9326 |
. . . . . . . . 9
β’ ((π β β€ β§ 0 β
β€) β (π # 0
β π β
0)) |
16 | 3, 14, 15 | sylancl 413 |
. . . . . . . 8
β’ (π β (π # 0 β π β 0)) |
17 | 4, 16 | mpbird 167 |
. . . . . . 7
β’ (π β π # 0) |
18 | | lgsdilem2.5 |
. . . . . . . 8
β’ (π β π β 0) |
19 | | zapne 9326 |
. . . . . . . . 9
β’ ((π β β€ β§ 0 β
β€) β (π # 0
β π β
0)) |
20 | 10, 14, 19 | sylancl 413 |
. . . . . . . 8
β’ (π β (π # 0 β π β 0)) |
21 | 18, 20 | mpbird 167 |
. . . . . . 7
β’ (π β π # 0) |
22 | 12, 13, 17, 21 | mulap0d 8614 |
. . . . . 6
β’ (π β (π Β· π) # 0) |
23 | | zapne 9326 |
. . . . . . 7
β’ (((π Β· π) β β€ β§ 0 β β€)
β ((π Β· π) # 0 β (π Β· π) β 0)) |
24 | 11, 14, 23 | sylancl 413 |
. . . . . 6
β’ (π β ((π Β· π) # 0 β (π Β· π) β 0)) |
25 | 22, 24 | mpbid 147 |
. . . . 5
β’ (π β (π Β· π) β 0) |
26 | | nnabscl 11108 |
. . . . 5
β’ (((π Β· π) β β€ β§ (π Β· π) β 0) β (absβ(π Β· π)) β β) |
27 | 11, 25, 26 | syl2anc 411 |
. . . 4
β’ (π β (absβ(π Β· π)) β β) |
28 | 27 | nnzd 9373 |
. . 3
β’ (π β (absβ(π Β· π)) β β€) |
29 | 12 | abscld 11189 |
. . . . 5
β’ (π β (absβπ) β
β) |
30 | 13 | abscld 11189 |
. . . . 5
β’ (π β (absβπ) β
β) |
31 | 12 | absge0d 11192 |
. . . . 5
β’ (π β 0 β€ (absβπ)) |
32 | | nnabscl 11108 |
. . . . . . 7
β’ ((π β β€ β§ π β 0) β (absβπ) β
β) |
33 | 10, 18, 32 | syl2anc 411 |
. . . . . 6
β’ (π β (absβπ) β
β) |
34 | 33 | nnge1d 8961 |
. . . . 5
β’ (π β 1 β€ (absβπ)) |
35 | 29, 30, 31, 34 | lemulge11d 8893 |
. . . 4
β’ (π β (absβπ) β€ ((absβπ) Β· (absβπ))) |
36 | 12, 13 | absmuld 11202 |
. . . 4
β’ (π β (absβ(π Β· π)) = ((absβπ) Β· (absβπ))) |
37 | 35, 36 | breqtrrd 4031 |
. . 3
β’ (π β (absβπ) β€ (absβ(π Β· π))) |
38 | | eluz2 9533 |
. . 3
β’
((absβ(π
Β· π)) β
(β€β₯β(absβπ)) β ((absβπ) β β€ β§ (absβ(π Β· π)) β β€ β§ (absβπ) β€ (absβ(π Β· π)))) |
39 | 9, 28, 37, 38 | syl3anbrc 1181 |
. 2
β’ (π β (absβ(π Β· π)) β
(β€β₯β(absβπ))) |
40 | | 1zzd 9279 |
. . . . 5
β’ (π β 1 β
β€) |
41 | | lgsdilem2.1 |
. . . . . . 7
β’ (π β π΄ β β€) |
42 | | lgsdilem2.6 |
. . . . . . . 8
β’ πΉ = (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
43 | 42 | lgsfcl3 14392 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β πΉ:ββΆβ€) |
44 | 41, 3, 4, 43 | syl3anc 1238 |
. . . . . 6
β’ (π β πΉ:ββΆβ€) |
45 | 44 | ffvelcdmda 5651 |
. . . . 5
β’ ((π β§ π β β) β (πΉβπ) β β€) |
46 | | zmulcl 9305 |
. . . . . 6
β’ ((π β β€ β§ π£ β β€) β (π Β· π£) β β€) |
47 | 46 | adantl 277 |
. . . . 5
β’ ((π β§ (π β β€ β§ π£ β β€)) β (π Β· π£) β β€) |
48 | 7, 40, 45, 47 | seqf 10460 |
. . . 4
β’ (π β seq1( Β· , πΉ):ββΆβ€) |
49 | 48, 6 | ffvelcdmd 5652 |
. . 3
β’ (π β (seq1( Β· , πΉ)β(absβπ)) β
β€) |
50 | 49 | zcnd 9375 |
. 2
β’ (π β (seq1( Β· , πΉ)β(absβπ)) β
β) |
51 | | eleq1w 2238 |
. . . . 5
β’ (π = π β (π β β β π β β)) |
52 | | oveq2 5882 |
. . . . . 6
β’ (π = π β (π΄ /L π) = (π΄ /L π)) |
53 | | oveq1 5881 |
. . . . . 6
β’ (π = π β (π pCnt π) = (π pCnt π)) |
54 | 52, 53 | oveq12d 5892 |
. . . . 5
β’ (π = π β ((π΄ /L π)β(π pCnt π)) = ((π΄ /L π)β(π pCnt π))) |
55 | 51, 54 | ifbieq1d 3556 |
. . . 4
β’ (π = π β if(π β β, ((π΄ /L π)β(π pCnt π)), 1) = if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
56 | 6 | peano2nnd 8933 |
. . . . 5
β’ (π β ((absβπ) + 1) β
β) |
57 | | elfzuz 10020 |
. . . . 5
β’ (π β (((absβπ) + 1)...(absβ(π Β· π))) β π β
(β€β₯β((absβπ) + 1))) |
58 | | eluznn 9599 |
. . . . 5
β’
((((absβπ) +
1) β β β§ π
β (β€β₯β((absβπ) + 1))) β π β β) |
59 | 56, 57, 58 | syl2an 289 |
. . . 4
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β π β β) |
60 | 41 | ad2antrr 488 |
. . . . . . 7
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β π΄ β β€) |
61 | | prmz 12110 |
. . . . . . . 8
β’ (π β β β π β
β€) |
62 | 61 | adantl 277 |
. . . . . . 7
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β π β β€) |
63 | | lgscl 14385 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β€) β (π΄ /L π) β
β€) |
64 | 60, 62, 63 | syl2anc 411 |
. . . . . 6
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β (π΄ /L π) β β€) |
65 | | simpr 110 |
. . . . . . 7
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β π β β) |
66 | 3 | ad2antrr 488 |
. . . . . . 7
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β π β β€) |
67 | 4 | ad2antrr 488 |
. . . . . . 7
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β π β 0) |
68 | | pczcl 12297 |
. . . . . . 7
β’ ((π β β β§ (π β β€ β§ π β 0)) β (π pCnt π) β
β0) |
69 | 65, 66, 67, 68 | syl12anc 1236 |
. . . . . 6
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β (π pCnt π) β
β0) |
70 | | zexpcl 10534 |
. . . . . 6
β’ (((π΄ /L π) β β€ β§ (π pCnt π) β β0) β ((π΄ /L π)β(π pCnt π)) β β€) |
71 | 64, 69, 70 | syl2anc 411 |
. . . . 5
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β ((π΄ /L π)β(π pCnt π)) β β€) |
72 | | 1zzd 9279 |
. . . . 5
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ Β¬ π β β) β 1 β
β€) |
73 | | prmdc 12129 |
. . . . . 6
β’ (π β β β
DECID π
β β) |
74 | 59, 73 | syl 14 |
. . . . 5
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β DECID π β
β) |
75 | 71, 72, 74 | ifcldadc 3563 |
. . . 4
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β if(π β β, ((π΄ /L π)β(π pCnt π)), 1) β β€) |
76 | 42, 55, 59, 75 | fvmptd3 5609 |
. . 3
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β (πΉβπ) = if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
77 | | zq 9625 |
. . . . . . . . . 10
β’ (π β β€ β π β
β) |
78 | 66, 77 | syl 14 |
. . . . . . . . 9
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β π β β) |
79 | | pcabs 12324 |
. . . . . . . . 9
β’ ((π β β β§ π β β) β (π pCnt (absβπ)) = (π pCnt π)) |
80 | 65, 78, 79 | syl2anc 411 |
. . . . . . . 8
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β (π pCnt (absβπ)) = (π pCnt π)) |
81 | | elfzle1 10026 |
. . . . . . . . . . . . . 14
β’ (π β (((absβπ) + 1)...(absβ(π Β· π))) β ((absβπ) + 1) β€ π) |
82 | 81 | adantl 277 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β ((absβπ) + 1) β€ π) |
83 | | elfzelz 10024 |
. . . . . . . . . . . . . 14
β’ (π β (((absβπ) + 1)...(absβ(π Β· π))) β π β β€) |
84 | | zltp1le 9306 |
. . . . . . . . . . . . . 14
β’
(((absβπ)
β β€ β§ π
β β€) β ((absβπ) < π β ((absβπ) + 1) β€ π)) |
85 | 9, 83, 84 | syl2an 289 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β ((absβπ) < π β ((absβπ) + 1) β€ π)) |
86 | 82, 85 | mpbird 167 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β (absβπ) < π) |
87 | | zltnle 9298 |
. . . . . . . . . . . . 13
β’
(((absβπ)
β β€ β§ π
β β€) β ((absβπ) < π β Β¬ π β€ (absβπ))) |
88 | 9, 83, 87 | syl2an 289 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β ((absβπ) < π β Β¬ π β€ (absβπ))) |
89 | 86, 88 | mpbid 147 |
. . . . . . . . . . 11
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β Β¬ π β€ (absβπ)) |
90 | 89 | adantr 276 |
. . . . . . . . . 10
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β Β¬ π β€ (absβπ)) |
91 | 66, 67, 5 | syl2anc 411 |
. . . . . . . . . . 11
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β (absβπ) β
β) |
92 | | dvdsle 11849 |
. . . . . . . . . . 11
β’ ((π β β€ β§
(absβπ) β
β) β (π β₯
(absβπ) β π β€ (absβπ))) |
93 | 62, 91, 92 | syl2anc 411 |
. . . . . . . . . 10
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β (π β₯ (absβπ) β π β€ (absβπ))) |
94 | 90, 93 | mtod 663 |
. . . . . . . . 9
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β Β¬ π β₯ (absβπ)) |
95 | | pceq0 12320 |
. . . . . . . . . 10
β’ ((π β β β§
(absβπ) β
β) β ((π pCnt
(absβπ)) = 0 β
Β¬ π β₯
(absβπ))) |
96 | 65, 91, 95 | syl2anc 411 |
. . . . . . . . 9
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β ((π pCnt (absβπ)) = 0 β Β¬ π β₯ (absβπ))) |
97 | 94, 96 | mpbird 167 |
. . . . . . . 8
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β (π pCnt (absβπ)) = 0) |
98 | 80, 97 | eqtr3d 2212 |
. . . . . . 7
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β (π pCnt π) = 0) |
99 | 98 | oveq2d 5890 |
. . . . . 6
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β ((π΄ /L π)β(π pCnt π)) = ((π΄ /L π)β0)) |
100 | 64 | zcnd 9375 |
. . . . . . 7
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β (π΄ /L π) β β) |
101 | 100 | exp0d 10647 |
. . . . . 6
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β ((π΄ /L π)β0) = 1) |
102 | 99, 101 | eqtrd 2210 |
. . . . 5
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β ((π΄ /L π)β(π pCnt π)) = 1) |
103 | 102, 74 | ifeq1dadc 3564 |
. . . 4
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β if(π β β, ((π΄ /L π)β(π pCnt π)), 1) = if(π β β, 1, 1)) |
104 | | ifiddc 3568 |
. . . . 5
β’
(DECID π β β β if(π β β, 1, 1) = 1) |
105 | 74, 104 | syl 14 |
. . . 4
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β if(π β β, 1, 1) = 1) |
106 | 103, 105 | eqtrd 2210 |
. . 3
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β if(π β β, ((π΄ /L π)β(π pCnt π)), 1) = 1) |
107 | 76, 106 | eqtrd 2210 |
. 2
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β (πΉβπ) = 1) |
108 | 44 | adantr 276 |
. . . 4
β’ ((π β§ π β (β€β₯β1))
β πΉ:ββΆβ€) |
109 | | elnnuz 9563 |
. . . . . 6
β’ (π β β β π β
(β€β₯β1)) |
110 | 109 | biimpri 133 |
. . . . 5
β’ (π β
(β€β₯β1) β π β β) |
111 | 110 | adantl 277 |
. . . 4
β’ ((π β§ π β (β€β₯β1))
β π β
β) |
112 | 108, 111 | ffvelcdmd 5652 |
. . 3
β’ ((π β§ π β (β€β₯β1))
β (πΉβπ) β
β€) |
113 | 112 | zcnd 9375 |
. 2
β’ ((π β§ π β (β€β₯β1))
β (πΉβπ) β
β) |
114 | | mulcl 7937 |
. . 3
β’ ((π β β β§ π£ β β) β (π Β· π£) β β) |
115 | 114 | adantl 277 |
. 2
β’ ((π β§ (π β β β§ π£ β β)) β (π Β· π£) β β) |
116 | 2, 8, 39, 50, 107, 113, 115 | seq3id2 10508 |
1
β’ (π β (seq1( Β· , πΉ)β(absβπ)) = (seq1( Β· , πΉ)β(absβ(π Β· π)))) |