Step | Hyp | Ref
| Expression |
1 | | mulid1 11154 |
. . 3
β’ (π β β β (π Β· 1) = π) |
2 | 1 | adantl 483 |
. 2
β’ ((π β§ π β β) β (π Β· 1) = π) |
3 | | lgsdilem2.2 |
. . . 4
β’ (π β π β β€) |
4 | | lgsdilem2.4 |
. . . 4
β’ (π β π β 0) |
5 | | nnabscl 15211 |
. . . 4
β’ ((π β β€ β§ π β 0) β (absβπ) β
β) |
6 | 3, 4, 5 | syl2anc 585 |
. . 3
β’ (π β (absβπ) β
β) |
7 | | nnuz 12807 |
. . 3
β’ β =
(β€β₯β1) |
8 | 6, 7 | eleqtrdi 2848 |
. 2
β’ (π β (absβπ) β
(β€β₯β1)) |
9 | 6 | nnzd 12527 |
. . 3
β’ (π β (absβπ) β
β€) |
10 | | lgsdilem2.3 |
. . . . . 6
β’ (π β π β β€) |
11 | 3, 10 | zmulcld 12614 |
. . . . 5
β’ (π β (π Β· π) β β€) |
12 | 3 | zcnd 12609 |
. . . . . 6
β’ (π β π β β) |
13 | 10 | zcnd 12609 |
. . . . . 6
β’ (π β π β β) |
14 | | lgsdilem2.5 |
. . . . . 6
β’ (π β π β 0) |
15 | 12, 13, 4, 14 | mulne0d 11808 |
. . . . 5
β’ (π β (π Β· π) β 0) |
16 | | nnabscl 15211 |
. . . . 5
β’ (((π Β· π) β β€ β§ (π Β· π) β 0) β (absβ(π Β· π)) β β) |
17 | 11, 15, 16 | syl2anc 585 |
. . . 4
β’ (π β (absβ(π Β· π)) β β) |
18 | 17 | nnzd 12527 |
. . 3
β’ (π β (absβ(π Β· π)) β β€) |
19 | 12 | abscld 15322 |
. . . . 5
β’ (π β (absβπ) β
β) |
20 | 13 | abscld 15322 |
. . . . 5
β’ (π β (absβπ) β
β) |
21 | 12 | absge0d 15330 |
. . . . 5
β’ (π β 0 β€ (absβπ)) |
22 | | nnabscl 15211 |
. . . . . . 7
β’ ((π β β€ β§ π β 0) β (absβπ) β
β) |
23 | 10, 14, 22 | syl2anc 585 |
. . . . . 6
β’ (π β (absβπ) β
β) |
24 | 23 | nnge1d 12202 |
. . . . 5
β’ (π β 1 β€ (absβπ)) |
25 | 19, 20, 21, 24 | lemulge11d 12093 |
. . . 4
β’ (π β (absβπ) β€ ((absβπ) Β· (absβπ))) |
26 | 12, 13 | absmuld 15340 |
. . . 4
β’ (π β (absβ(π Β· π)) = ((absβπ) Β· (absβπ))) |
27 | 25, 26 | breqtrrd 5134 |
. . 3
β’ (π β (absβπ) β€ (absβ(π Β· π))) |
28 | | eluz2 12770 |
. . 3
β’
((absβ(π
Β· π)) β
(β€β₯β(absβπ)) β ((absβπ) β β€ β§ (absβ(π Β· π)) β β€ β§ (absβπ) β€ (absβ(π Β· π)))) |
29 | 9, 18, 27, 28 | syl3anbrc 1344 |
. 2
β’ (π β (absβ(π Β· π)) β
(β€β₯β(absβπ))) |
30 | | lgsdilem2.1 |
. . . . . 6
β’ (π β π΄ β β€) |
31 | | lgsdilem2.6 |
. . . . . . 7
β’ πΉ = (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
32 | 31 | lgsfcl3 26669 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β πΉ:ββΆβ€) |
33 | 30, 3, 4, 32 | syl3anc 1372 |
. . . . 5
β’ (π β πΉ:ββΆβ€) |
34 | | elfznn 13471 |
. . . . 5
β’ (π β (1...(absβπ)) β π β β) |
35 | | ffvelcdm 7033 |
. . . . 5
β’ ((πΉ:ββΆβ€ β§
π β β) β
(πΉβπ) β β€) |
36 | 33, 34, 35 | syl2an 597 |
. . . 4
β’ ((π β§ π β (1...(absβπ))) β (πΉβπ) β β€) |
37 | 36 | zcnd 12609 |
. . 3
β’ ((π β§ π β (1...(absβπ))) β (πΉβπ) β β) |
38 | | mulcl 11136 |
. . . 4
β’ ((π β β β§ π₯ β β) β (π Β· π₯) β β) |
39 | 38 | adantl 483 |
. . 3
β’ ((π β§ (π β β β§ π₯ β β)) β (π Β· π₯) β β) |
40 | 8, 37, 39 | seqcl 13929 |
. 2
β’ (π β (seq1( Β· , πΉ)β(absβπ)) β
β) |
41 | 6 | peano2nnd 12171 |
. . . . 5
β’ (π β ((absβπ) + 1) β
β) |
42 | | elfzuz 13438 |
. . . . 5
β’ (π β (((absβπ) + 1)...(absβ(π Β· π))) β π β
(β€β₯β((absβπ) + 1))) |
43 | | eluznn 12844 |
. . . . 5
β’
((((absβπ) +
1) β β β§ π
β (β€β₯β((absβπ) + 1))) β π β β) |
44 | 41, 42, 43 | syl2an 597 |
. . . 4
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β π β β) |
45 | | eleq1w 2821 |
. . . . . 6
β’ (π = π β (π β β β π β β)) |
46 | | oveq2 7366 |
. . . . . . 7
β’ (π = π β (π΄ /L π) = (π΄ /L π)) |
47 | | oveq1 7365 |
. . . . . . 7
β’ (π = π β (π pCnt π) = (π pCnt π)) |
48 | 46, 47 | oveq12d 7376 |
. . . . . 6
β’ (π = π β ((π΄ /L π)β(π pCnt π)) = ((π΄ /L π)β(π pCnt π))) |
49 | 45, 48 | ifbieq1d 4511 |
. . . . 5
β’ (π = π β if(π β β, ((π΄ /L π)β(π pCnt π)), 1) = if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
50 | | ovex 7391 |
. . . . . 6
β’ ((π΄ /L π)β(π pCnt π)) β V |
51 | | 1ex 11152 |
. . . . . 6
β’ 1 β
V |
52 | 50, 51 | ifex 4537 |
. . . . 5
β’ if(π β β, ((π΄ /L π)β(π pCnt π)), 1) β V |
53 | 49, 31, 52 | fvmpt 6949 |
. . . 4
β’ (π β β β (πΉβπ) = if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
54 | 44, 53 | syl 17 |
. . 3
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β (πΉβπ) = if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
55 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β π β β) |
56 | 3 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β π β β€) |
57 | | zq 12880 |
. . . . . . . . . 10
β’ (π β β€ β π β
β) |
58 | 56, 57 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β π β β) |
59 | | pcabs 16748 |
. . . . . . . . 9
β’ ((π β β β§ π β β) β (π pCnt (absβπ)) = (π pCnt π)) |
60 | 55, 58, 59 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β (π pCnt (absβπ)) = (π pCnt π)) |
61 | | elfzle1 13445 |
. . . . . . . . . . . . . 14
β’ (π β (((absβπ) + 1)...(absβ(π Β· π))) β ((absβπ) + 1) β€ π) |
62 | 61 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β ((absβπ) + 1) β€ π) |
63 | | elfzelz 13442 |
. . . . . . . . . . . . . 14
β’ (π β (((absβπ) + 1)...(absβ(π Β· π))) β π β β€) |
64 | | zltp1le 12554 |
. . . . . . . . . . . . . 14
β’
(((absβπ)
β β€ β§ π
β β€) β ((absβπ) < π β ((absβπ) + 1) β€ π)) |
65 | 9, 63, 64 | syl2an 597 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β ((absβπ) < π β ((absβπ) + 1) β€ π)) |
66 | 62, 65 | mpbird 257 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β (absβπ) < π) |
67 | 19 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β (absβπ) β β) |
68 | 63 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β π β β€) |
69 | 68 | zred 12608 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β π β β) |
70 | 67, 69 | ltnled 11303 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β ((absβπ) < π β Β¬ π β€ (absβπ))) |
71 | 66, 70 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β Β¬ π β€ (absβπ)) |
72 | 71 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β Β¬ π β€ (absβπ)) |
73 | | prmz 16552 |
. . . . . . . . . . . 12
β’ (π β β β π β
β€) |
74 | 73 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β π β β€) |
75 | 4 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β π β 0) |
76 | 56, 75, 5 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β (absβπ) β
β) |
77 | | dvdsle 16193 |
. . . . . . . . . . 11
β’ ((π β β€ β§
(absβπ) β
β) β (π β₯
(absβπ) β π β€ (absβπ))) |
78 | 74, 76, 77 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β (π β₯ (absβπ) β π β€ (absβπ))) |
79 | 72, 78 | mtod 197 |
. . . . . . . . 9
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β Β¬ π β₯ (absβπ)) |
80 | | pceq0 16744 |
. . . . . . . . . 10
β’ ((π β β β§
(absβπ) β
β) β ((π pCnt
(absβπ)) = 0 β
Β¬ π β₯
(absβπ))) |
81 | 55, 76, 80 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β ((π pCnt (absβπ)) = 0 β Β¬ π β₯ (absβπ))) |
82 | 79, 81 | mpbird 257 |
. . . . . . . 8
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β (π pCnt (absβπ)) = 0) |
83 | 60, 82 | eqtr3d 2779 |
. . . . . . 7
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β (π pCnt π) = 0) |
84 | 83 | oveq2d 7374 |
. . . . . 6
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β ((π΄ /L π)β(π pCnt π)) = ((π΄ /L π)β0)) |
85 | 30 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β π΄ β β€) |
86 | | lgscl 26662 |
. . . . . . . . 9
β’ ((π΄ β β€ β§ π β β€) β (π΄ /L π) β
β€) |
87 | 85, 74, 86 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β (π΄ /L π) β β€) |
88 | 87 | zcnd 12609 |
. . . . . . 7
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β (π΄ /L π) β β) |
89 | 88 | exp0d 14046 |
. . . . . 6
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β ((π΄ /L π)β0) = 1) |
90 | 84, 89 | eqtrd 2777 |
. . . . 5
β’ (((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β§ π β β) β ((π΄ /L π)β(π pCnt π)) = 1) |
91 | 90 | ifeq1da 4518 |
. . . 4
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β if(π β β, ((π΄ /L π)β(π pCnt π)), 1) = if(π β β, 1, 1)) |
92 | | ifid 4527 |
. . . 4
β’ if(π β β, 1, 1) =
1 |
93 | 91, 92 | eqtrdi 2793 |
. . 3
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β if(π β β, ((π΄ /L π)β(π pCnt π)), 1) = 1) |
94 | 54, 93 | eqtrd 2777 |
. 2
β’ ((π β§ π β (((absβπ) + 1)...(absβ(π Β· π)))) β (πΉβπ) = 1) |
95 | 2, 8, 29, 40, 94 | seqid2 13955 |
1
β’ (π β (seq1( Β· , πΉ)β(absβπ)) = (seq1( Β· , πΉ)β(absβ(π Β· π)))) |