Step | Hyp | Ref
| Expression |
1 | | pcmpt.3 |
. 2
β’ (π β π β β) |
2 | | fveq2 5515 |
. . . . . 6
β’ (π = 1 β (seq1( Β· ,
πΉ)βπ) = (seq1( Β· , πΉ)β1)) |
3 | 2 | oveq2d 5890 |
. . . . 5
β’ (π = 1 β (π pCnt (seq1( Β· , πΉ)βπ)) = (π pCnt (seq1( Β· , πΉ)β1))) |
4 | | breq2 4007 |
. . . . . 6
β’ (π = 1 β (π β€ π β π β€ 1)) |
5 | 4 | ifbid 3555 |
. . . . 5
β’ (π = 1 β if(π β€ π, π΅, 0) = if(π β€ 1, π΅, 0)) |
6 | 3, 5 | eqeq12d 2192 |
. . . 4
β’ (π = 1 β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)β1)) = if(π β€ 1, π΅, 0))) |
7 | 6 | imbi2d 230 |
. . 3
β’ (π = 1 β ((π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0)) β (π β (π pCnt (seq1( Β· , πΉ)β1)) = if(π β€ 1, π΅, 0)))) |
8 | | fveq2 5515 |
. . . . . 6
β’ (π = π β (seq1( Β· , πΉ)βπ) = (seq1( Β· , πΉ)βπ)) |
9 | 8 | oveq2d 5890 |
. . . . 5
β’ (π = π β (π pCnt (seq1( Β· , πΉ)βπ)) = (π pCnt (seq1( Β· , πΉ)βπ))) |
10 | | breq2 4007 |
. . . . . 6
β’ (π = π β (π β€ π β π β€ π)) |
11 | 10 | ifbid 3555 |
. . . . 5
β’ (π = π β if(π β€ π, π΅, 0) = if(π β€ π, π΅, 0)) |
12 | 9, 11 | eqeq12d 2192 |
. . . 4
β’ (π = π β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0))) |
13 | 12 | imbi2d 230 |
. . 3
β’ (π = π β ((π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0)) β (π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0)))) |
14 | | fveq2 5515 |
. . . . . 6
β’ (π = (π + 1) β (seq1( Β· , πΉ)βπ) = (seq1( Β· , πΉ)β(π + 1))) |
15 | 14 | oveq2d 5890 |
. . . . 5
β’ (π = (π + 1) β (π pCnt (seq1( Β· , πΉ)βπ)) = (π pCnt (seq1( Β· , πΉ)β(π + 1)))) |
16 | | breq2 4007 |
. . . . . 6
β’ (π = (π + 1) β (π β€ π β π β€ (π + 1))) |
17 | 16 | ifbid 3555 |
. . . . 5
β’ (π = (π + 1) β if(π β€ π, π΅, 0) = if(π β€ (π + 1), π΅, 0)) |
18 | 15, 17 | eqeq12d 2192 |
. . . 4
β’ (π = (π + 1) β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0))) |
19 | 18 | imbi2d 230 |
. . 3
β’ (π = (π + 1) β ((π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0)) β (π β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0)))) |
20 | | fveq2 5515 |
. . . . . 6
β’ (π = π β (seq1( Β· , πΉ)βπ) = (seq1( Β· , πΉ)βπ)) |
21 | 20 | oveq2d 5890 |
. . . . 5
β’ (π = π β (π pCnt (seq1( Β· , πΉ)βπ)) = (π pCnt (seq1( Β· , πΉ)βπ))) |
22 | | breq2 4007 |
. . . . . 6
β’ (π = π β (π β€ π β π β€ π)) |
23 | 22 | ifbid 3555 |
. . . . 5
β’ (π = π β if(π β€ π, π΅, 0) = if(π β€ π, π΅, 0)) |
24 | 21, 23 | eqeq12d 2192 |
. . . 4
β’ (π = π β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0))) |
25 | 24 | imbi2d 230 |
. . 3
β’ (π = π β ((π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0)) β (π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0)))) |
26 | | pcmpt.4 |
. . . . 5
β’ (π β π β β) |
27 | | pc1 12304 |
. . . . 5
β’ (π β β β (π pCnt 1) = 0) |
28 | 26, 27 | syl 14 |
. . . 4
β’ (π β (π pCnt 1) = 0) |
29 | | 1zzd 9279 |
. . . . . . 7
β’ (π β 1 β
β€) |
30 | | elnnuz 9563 |
. . . . . . . 8
β’ (π β β β π β
(β€β₯β1)) |
31 | | simpr 110 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β β) |
32 | 31 | adantr 276 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β β) β π β β) |
33 | | simpr 110 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β β) β π β β) |
34 | | pcmpt.2 |
. . . . . . . . . . . . . 14
β’ (π β βπ β β π΄ β
β0) |
35 | 34 | ad2antrr 488 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β β) β βπ β β π΄ β
β0) |
36 | | nfcsb1v 3090 |
. . . . . . . . . . . . . . 15
β’
β²πβ¦π / πβ¦π΄ |
37 | 36 | nfel1 2330 |
. . . . . . . . . . . . . 14
β’
β²πβ¦π / πβ¦π΄ β β0 |
38 | | csbeq1a 3066 |
. . . . . . . . . . . . . . 15
β’ (π = π β π΄ = β¦π / πβ¦π΄) |
39 | 38 | eleq1d 2246 |
. . . . . . . . . . . . . 14
β’ (π = π β (π΄ β β0 β
β¦π / πβ¦π΄ β
β0)) |
40 | 37, 39 | rspc 2835 |
. . . . . . . . . . . . 13
β’ (π β β β
(βπ β β
π΄ β
β0 β β¦π / πβ¦π΄ β
β0)) |
41 | 33, 35, 40 | sylc 62 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β β) β β¦π / πβ¦π΄ β
β0) |
42 | 32, 41 | nnexpcld 10675 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β β) β (πββ¦π / πβ¦π΄) β β) |
43 | | 1nn 8929 |
. . . . . . . . . . . 12
β’ 1 β
β |
44 | 43 | a1i 9 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ Β¬ π β β) β 1 β
β) |
45 | | prmdc 12129 |
. . . . . . . . . . . 12
β’ (π β β β
DECID π
β β) |
46 | 45 | adantl 277 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β DECID
π β
β) |
47 | 42, 44, 46 | ifcldadc 3563 |
. . . . . . . . . 10
β’ ((π β§ π β β) β if(π β β, (πββ¦π / πβ¦π΄), 1) β β) |
48 | | nfcv 2319 |
. . . . . . . . . . 11
β’
β²ππ |
49 | 48 | nfel1 2330 |
. . . . . . . . . . . 12
β’
β²π π β β |
50 | | nfcv 2319 |
. . . . . . . . . . . . 13
β’
β²πβ |
51 | 48, 50, 36 | nfov 5904 |
. . . . . . . . . . . 12
β’
β²π(πββ¦π / πβ¦π΄) |
52 | | nfcv 2319 |
. . . . . . . . . . . 12
β’
β²π1 |
53 | 49, 51, 52 | nfif 3562 |
. . . . . . . . . . 11
β’
β²πif(π β β, (πββ¦π / πβ¦π΄), 1) |
54 | | eleq1 2240 |
. . . . . . . . . . . 12
β’ (π = π β (π β β β π β β)) |
55 | | id 19 |
. . . . . . . . . . . . 13
β’ (π = π β π = π) |
56 | 55, 38 | oveq12d 5892 |
. . . . . . . . . . . 12
β’ (π = π β (πβπ΄) = (πββ¦π / πβ¦π΄)) |
57 | 54, 56 | ifbieq1d 3556 |
. . . . . . . . . . 11
β’ (π = π β if(π β β, (πβπ΄), 1) = if(π β β, (πββ¦π / πβ¦π΄), 1)) |
58 | | pcmpt.1 |
. . . . . . . . . . 11
β’ πΉ = (π β β β¦ if(π β β, (πβπ΄), 1)) |
59 | 48, 53, 57, 58 | fvmptf 5608 |
. . . . . . . . . 10
β’ ((π β β β§ if(π β β, (πββ¦π / πβ¦π΄), 1) β β) β (πΉβπ) = if(π β β, (πββ¦π / πβ¦π΄), 1)) |
60 | 31, 47, 59 | syl2anc 411 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΉβπ) = if(π β β, (πββ¦π / πβ¦π΄), 1)) |
61 | 60, 47 | eqeltrd 2254 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΉβπ) β β) |
62 | 30, 61 | sylan2br 288 |
. . . . . . 7
β’ ((π β§ π β (β€β₯β1))
β (πΉβπ) β
β) |
63 | | nnmulcl 8939 |
. . . . . . . 8
β’ ((π β β β§ π β β) β (π Β· π) β β) |
64 | 63 | adantl 277 |
. . . . . . 7
β’ ((π β§ (π β β β§ π β β)) β (π Β· π) β β) |
65 | 29, 62, 64 | seq3-1 10459 |
. . . . . 6
β’ (π β (seq1( Β· , πΉ)β1) = (πΉβ1)) |
66 | | 1nprm 12113 |
. . . . . . . . . 10
β’ Β¬ 1
β β |
67 | | eleq1 2240 |
. . . . . . . . . 10
β’ (π = 1 β (π β β β 1 β
β)) |
68 | 66, 67 | mtbiri 675 |
. . . . . . . . 9
β’ (π = 1 β Β¬ π β
β) |
69 | 68 | iffalsed 3544 |
. . . . . . . 8
β’ (π = 1 β if(π β β, (πβπ΄), 1) = 1) |
70 | | 1ex 7951 |
. . . . . . . 8
β’ 1 β
V |
71 | 69, 58, 70 | fvmpt 5593 |
. . . . . . 7
β’ (1 β
β β (πΉβ1)
= 1) |
72 | 43, 71 | ax-mp 5 |
. . . . . 6
β’ (πΉβ1) = 1 |
73 | 65, 72 | eqtrdi 2226 |
. . . . 5
β’ (π β (seq1( Β· , πΉ)β1) = 1) |
74 | 73 | oveq2d 5890 |
. . . 4
β’ (π β (π pCnt (seq1( Β· , πΉ)β1)) = (π pCnt 1)) |
75 | | prmgt1 12131 |
. . . . . . 7
β’ (π β β β 1 <
π) |
76 | | 1z 9278 |
. . . . . . . 8
β’ 1 β
β€ |
77 | | prmz 12110 |
. . . . . . . 8
β’ (π β β β π β
β€) |
78 | | zltnle 9298 |
. . . . . . . 8
β’ ((1
β β€ β§ π
β β€) β (1 < π β Β¬ π β€ 1)) |
79 | 76, 77, 78 | sylancr 414 |
. . . . . . 7
β’ (π β β β (1 <
π β Β¬ π β€ 1)) |
80 | 75, 79 | mpbid 147 |
. . . . . 6
β’ (π β β β Β¬
π β€ 1) |
81 | 80 | iffalsed 3544 |
. . . . 5
β’ (π β β β if(π β€ 1, π΅, 0) = 0) |
82 | 26, 81 | syl 14 |
. . . 4
β’ (π β if(π β€ 1, π΅, 0) = 0) |
83 | 28, 74, 82 | 3eqtr4d 2220 |
. . 3
β’ (π β (π pCnt (seq1( Β· , πΉ)β1)) = if(π β€ 1, π΅, 0)) |
84 | 26 | adantr 276 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ (π + 1) = π)) β π β β) |
85 | 58, 34 | pcmptcl 12339 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΉ:ββΆβ β§ seq1( Β·
, πΉ):ββΆβ)) |
86 | 85 | simpld 112 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:ββΆβ) |
87 | | peano2nn 8930 |
. . . . . . . . . . . . . . 15
β’ (π β β β (π + 1) β
β) |
88 | | ffvelcdm 5649 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:ββΆβ β§
(π + 1) β β)
β (πΉβ(π + 1)) β
β) |
89 | 86, 87, 88 | syl2an 289 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (πΉβ(π + 1)) β β) |
90 | 89 | adantrr 479 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ (π + 1) = π)) β (πΉβ(π + 1)) β β) |
91 | 84, 90 | pccld 12299 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) = π)) β (π pCnt (πΉβ(π + 1))) β
β0) |
92 | 91 | nn0cnd 9230 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) = π)) β (π pCnt (πΉβ(π + 1))) β β) |
93 | 92 | addid2d 8106 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (π + 1) = π)) β (0 + (π pCnt (πΉβ(π + 1)))) = (π pCnt (πΉβ(π + 1)))) |
94 | 87 | ad2antrl 490 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ (π + 1) = π)) β (π + 1) β β) |
95 | 87 | ad2antlr 489 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ (π + 1) β β) β (π + 1) β
β) |
96 | | simpr 110 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ (π + 1) β β) β (π + 1) β
β) |
97 | 34 | ad2antrr 488 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ (π + 1) β β) β βπ β β π΄ β
β0) |
98 | | nfcsb1v 3090 |
. . . . . . . . . . . . . . . . . . 19
β’
β²πβ¦(π + 1) / πβ¦π΄ |
99 | 98 | nfel1 2330 |
. . . . . . . . . . . . . . . . . 18
β’
β²πβ¦(π + 1) / πβ¦π΄ β β0 |
100 | | csbeq1a 3066 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π + 1) β π΄ = β¦(π + 1) / πβ¦π΄) |
101 | 100 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π + 1) β (π΄ β β0 β
β¦(π + 1) /
πβ¦π΄ β
β0)) |
102 | 99, 101 | rspc 2835 |
. . . . . . . . . . . . . . . . 17
β’ ((π + 1) β β β
(βπ β β
π΄ β
β0 β β¦(π + 1) / πβ¦π΄ β
β0)) |
103 | 96, 97, 102 | sylc 62 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ (π + 1) β β) β
β¦(π + 1) /
πβ¦π΄ β
β0) |
104 | 95, 103 | nnexpcld 10675 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ (π + 1) β β) β ((π + 1)ββ¦(π + 1) / πβ¦π΄) β β) |
105 | 43 | a1i 9 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ Β¬ (π + 1) β β) β 1
β β) |
106 | 87 | adantl 277 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (π + 1) β β) |
107 | | prmdc 12129 |
. . . . . . . . . . . . . . . 16
β’ ((π + 1) β β β
DECID (π +
1) β β) |
108 | 106, 107 | syl 14 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β DECID
(π + 1) β
β) |
109 | 104, 105,
108 | ifcldadc 3563 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β if((π + 1) β β, ((π + 1)ββ¦(π + 1) / πβ¦π΄), 1) β β) |
110 | 109 | adantrr 479 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ (π + 1) = π)) β if((π + 1) β β, ((π + 1)ββ¦(π + 1) / πβ¦π΄), 1) β β) |
111 | | nfcv 2319 |
. . . . . . . . . . . . . 14
β’
β²π(π + 1) |
112 | | nfv 1528 |
. . . . . . . . . . . . . . 15
β’
β²π(π + 1) β
β |
113 | 111, 50, 98 | nfov 5904 |
. . . . . . . . . . . . . . 15
β’
β²π((π + 1)ββ¦(π + 1) / πβ¦π΄) |
114 | 112, 113,
52 | nfif 3562 |
. . . . . . . . . . . . . 14
β’
β²πif((π + 1) β β, ((π + 1)ββ¦(π + 1) / πβ¦π΄), 1) |
115 | | eleq1 2240 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β (π β β β (π + 1) β β)) |
116 | | id 19 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β π = (π + 1)) |
117 | 116, 100 | oveq12d 5892 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β (πβπ΄) = ((π + 1)ββ¦(π + 1) / πβ¦π΄)) |
118 | 115, 117 | ifbieq1d 3556 |
. . . . . . . . . . . . . 14
β’ (π = (π + 1) β if(π β β, (πβπ΄), 1) = if((π + 1) β β, ((π + 1)ββ¦(π + 1) / πβ¦π΄), 1)) |
119 | 111, 114,
118, 58 | fvmptf 5608 |
. . . . . . . . . . . . 13
β’ (((π + 1) β β β§
if((π + 1) β β,
((π +
1)ββ¦(π +
1) / πβ¦π΄), 1) β β) β
(πΉβ(π + 1)) = if((π + 1) β β, ((π + 1)ββ¦(π + 1) / πβ¦π΄), 1)) |
120 | 94, 110, 119 | syl2anc 411 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) = π)) β (πΉβ(π + 1)) = if((π + 1) β β, ((π + 1)ββ¦(π + 1) / πβ¦π΄), 1)) |
121 | | simprr 531 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§ (π + 1) = π)) β (π + 1) = π) |
122 | 121, 84 | eqeltrd 2254 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ (π + 1) = π)) β (π + 1) β β) |
123 | 122 | iftrued 3541 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) = π)) β if((π + 1) β β, ((π + 1)ββ¦(π + 1) / πβ¦π΄), 1) = ((π + 1)ββ¦(π + 1) / πβ¦π΄)) |
124 | 121 | csbeq1d 3064 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§ (π + 1) = π)) β β¦(π + 1) / πβ¦π΄ = β¦π / πβ¦π΄) |
125 | | nfcvd 2320 |
. . . . . . . . . . . . . . . 16
β’ (π β β β
β²ππ΅) |
126 | | pcmpt.5 |
. . . . . . . . . . . . . . . 16
β’ (π = π β π΄ = π΅) |
127 | 125, 126 | csbiegf 3100 |
. . . . . . . . . . . . . . 15
β’ (π β β β
β¦π / πβ¦π΄ = π΅) |
128 | 84, 127 | syl 14 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§ (π + 1) = π)) β β¦π / πβ¦π΄ = π΅) |
129 | 124, 128 | eqtrd 2210 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ (π + 1) = π)) β β¦(π + 1) / πβ¦π΄ = π΅) |
130 | 121, 129 | oveq12d 5892 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) = π)) β ((π + 1)ββ¦(π + 1) / πβ¦π΄) = (πβπ΅)) |
131 | 120, 123,
130 | 3eqtrd 2214 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) = π)) β (πΉβ(π + 1)) = (πβπ΅)) |
132 | 131 | oveq2d 5890 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (π + 1) = π)) β (π pCnt (πΉβ(π + 1))) = (π pCnt (πβπ΅))) |
133 | 126 | eleq1d 2246 |
. . . . . . . . . . . . . 14
β’ (π = π β (π΄ β β0 β π΅ β
β0)) |
134 | 133 | rspcv 2837 |
. . . . . . . . . . . . 13
β’ (π β β β
(βπ β β
π΄ β
β0 β π΅ β
β0)) |
135 | 26, 34, 134 | sylc 62 |
. . . . . . . . . . . 12
β’ (π β π΅ β
β0) |
136 | 135 | adantr 276 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) = π)) β π΅ β
β0) |
137 | | pcidlem 12321 |
. . . . . . . . . . 11
β’ ((π β β β§ π΅ β β0)
β (π pCnt (πβπ΅)) = π΅) |
138 | 26, 136, 137 | syl2an2r 595 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (π + 1) = π)) β (π pCnt (πβπ΅)) = π΅) |
139 | 93, 132, 138 | 3eqtrd 2214 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (π + 1) = π)) β (0 + (π pCnt (πΉβ(π + 1)))) = π΅) |
140 | | oveq1 5881 |
. . . . . . . . . 10
β’ ((π pCnt (seq1( Β· , πΉ)βπ)) = 0 β ((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1)))) = (0 + (π pCnt (πΉβ(π + 1))))) |
141 | 140 | eqeq1d 2186 |
. . . . . . . . 9
β’ ((π pCnt (seq1( Β· , πΉ)βπ)) = 0 β (((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1)))) = π΅ β (0 + (π pCnt (πΉβ(π + 1)))) = π΅)) |
142 | 139, 141 | syl5ibrcom 157 |
. . . . . . . 8
β’ ((π β§ (π β β β§ (π + 1) = π)) β ((π pCnt (seq1( Β· , πΉ)βπ)) = 0 β ((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1)))) = π΅)) |
143 | | nnre 8925 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β) |
144 | 143 | ltp1d 8886 |
. . . . . . . . . . . . 13
β’ (π β β β π < (π + 1)) |
145 | | nnz 9271 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β€) |
146 | 87 | nnzd 9373 |
. . . . . . . . . . . . . 14
β’ (π β β β (π + 1) β
β€) |
147 | | zltnle 9298 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ (π + 1) β β€) β
(π < (π + 1) β Β¬ (π + 1) β€ π)) |
148 | 145, 146,
147 | syl2anc 411 |
. . . . . . . . . . . . 13
β’ (π β β β (π < (π + 1) β Β¬ (π + 1) β€ π)) |
149 | 144, 148 | mpbid 147 |
. . . . . . . . . . . 12
β’ (π β β β Β¬
(π + 1) β€ π) |
150 | 149 | ad2antrl 490 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) = π)) β Β¬ (π + 1) β€ π) |
151 | 121 | breq1d 4013 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) = π)) β ((π + 1) β€ π β π β€ π)) |
152 | 150, 151 | mtbid 672 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (π + 1) = π)) β Β¬ π β€ π) |
153 | 152 | iffalsed 3544 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (π + 1) = π)) β if(π β€ π, π΅, 0) = 0) |
154 | 153 | eqeq2d 2189 |
. . . . . . . 8
β’ ((π β§ (π β β β§ (π + 1) = π)) β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)βπ)) = 0)) |
155 | | simpr 110 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π β β) |
156 | | nnuz 9562 |
. . . . . . . . . . . . . 14
β’ β =
(β€β₯β1) |
157 | 155, 156 | eleqtrdi 2270 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π β
(β€β₯β1)) |
158 | 62 | adantlr 477 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β (β€β₯β1))
β (πΉβπ) β
β) |
159 | 63 | adantl 277 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ (π β β β§ π β β)) β (π Β· π) β β) |
160 | 157, 158,
159 | seq3p1 10461 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (seq1( Β· ,
πΉ)β(π + 1)) = ((seq1( Β· ,
πΉ)βπ) Β· (πΉβ(π + 1)))) |
161 | 160 | oveq2d 5890 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = (π pCnt ((seq1( Β· , πΉ)βπ) Β· (πΉβ(π + 1))))) |
162 | 26 | adantr 276 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β) |
163 | 85 | simprd 114 |
. . . . . . . . . . . . . 14
β’ (π β seq1( Β· , πΉ):ββΆβ) |
164 | 163 | ffvelcdmda 5651 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (seq1( Β· ,
πΉ)βπ) β β) |
165 | | nnz 9271 |
. . . . . . . . . . . . . 14
β’ ((seq1(
Β· , πΉ)βπ) β β β (seq1(
Β· , πΉ)βπ) β
β€) |
166 | | nnne0 8946 |
. . . . . . . . . . . . . 14
β’ ((seq1(
Β· , πΉ)βπ) β β β (seq1(
Β· , πΉ)βπ) β 0) |
167 | 165, 166 | jca 306 |
. . . . . . . . . . . . 13
β’ ((seq1(
Β· , πΉ)βπ) β β β ((seq1(
Β· , πΉ)βπ) β β€ β§ (seq1(
Β· , πΉ)βπ) β 0)) |
168 | 164, 167 | syl 14 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((seq1( Β· ,
πΉ)βπ) β β€ β§ (seq1( Β· ,
πΉ)βπ) β 0)) |
169 | | nnz 9271 |
. . . . . . . . . . . . . 14
β’ ((πΉβ(π + 1)) β β β (πΉβ(π + 1)) β β€) |
170 | | nnne0 8946 |
. . . . . . . . . . . . . 14
β’ ((πΉβ(π + 1)) β β β (πΉβ(π + 1)) β 0) |
171 | 169, 170 | jca 306 |
. . . . . . . . . . . . 13
β’ ((πΉβ(π + 1)) β β β ((πΉβ(π + 1)) β β€ β§ (πΉβ(π + 1)) β 0)) |
172 | 89, 171 | syl 14 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((πΉβ(π + 1)) β β€ β§ (πΉβ(π + 1)) β 0)) |
173 | | pcmul 12300 |
. . . . . . . . . . . 12
β’ ((π β β β§ ((seq1(
Β· , πΉ)βπ) β β€ β§ (seq1(
Β· , πΉ)βπ) β 0) β§ ((πΉβ(π + 1)) β β€ β§ (πΉβ(π + 1)) β 0)) β (π pCnt ((seq1( Β· , πΉ)βπ) Β· (πΉβ(π + 1)))) = ((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1))))) |
174 | 162, 168,
172, 173 | syl3anc 1238 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π pCnt ((seq1( Β· , πΉ)βπ) Β· (πΉβ(π + 1)))) = ((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1))))) |
175 | 161, 174 | eqtrd 2210 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = ((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1))))) |
176 | 175 | adantrr 479 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (π + 1) = π)) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = ((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1))))) |
177 | | prmnn 12109 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β) |
178 | 26, 177 | syl 14 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
179 | 178 | nnred 8931 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
180 | 179 | adantr 276 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) = π)) β π β β) |
181 | 180 | leidd 8470 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) = π)) β π β€ π) |
182 | 181, 121 | breqtrrd 4031 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (π + 1) = π)) β π β€ (π + 1)) |
183 | 182 | iftrued 3541 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (π + 1) = π)) β if(π β€ (π + 1), π΅, 0) = π΅) |
184 | 176, 183 | eqeq12d 2192 |
. . . . . . . 8
β’ ((π β§ (π β β β§ (π + 1) = π)) β ((π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0) β ((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1)))) = π΅)) |
185 | 142, 154,
184 | 3imtr4d 203 |
. . . . . . 7
β’ ((π β§ (π β β β§ (π + 1) = π)) β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0))) |
186 | 185 | expr 375 |
. . . . . 6
β’ ((π β§ π β β) β ((π + 1) = π β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0)))) |
187 | 175 | adantrr 479 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = ((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1))))) |
188 | | simplrr 536 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β (π + 1) β π) |
189 | 188 | necomd 2433 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β π β (π + 1)) |
190 | 26 | ad2antrr 488 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β π β
β) |
191 | | simpr 110 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β (π + 1) β
β) |
192 | 34 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β βπ β β π΄ β
β0) |
193 | 191, 192,
102 | sylc 62 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β
β¦(π + 1) /
πβ¦π΄ β
β0) |
194 | | prmdvdsexpr 12149 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ (π + 1) β β β§
β¦(π + 1) /
πβ¦π΄ β β0)
β (π β₯ ((π + 1)ββ¦(π + 1) / πβ¦π΄) β π = (π + 1))) |
195 | 190, 191,
193, 194 | syl3anc 1238 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β (π β₯ ((π + 1)ββ¦(π + 1) / πβ¦π΄) β π = (π + 1))) |
196 | 195 | necon3ad 2389 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β (π β (π + 1) β Β¬ π β₯ ((π + 1)ββ¦(π + 1) / πβ¦π΄))) |
197 | 189, 196 | mpd 13 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β Β¬ π β₯ ((π + 1)ββ¦(π + 1) / πβ¦π΄)) |
198 | 87 | ad2antrl 490 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π + 1) β β) |
199 | 109 | adantrr 479 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β β β§ (π + 1) β π)) β if((π + 1) β β, ((π + 1)ββ¦(π + 1) / πβ¦π΄), 1) β β) |
200 | 198, 199,
119 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β β β§ (π + 1) β π)) β (πΉβ(π + 1)) = if((π + 1) β β, ((π + 1)ββ¦(π + 1) / πβ¦π΄), 1)) |
201 | | iftrue 3539 |
. . . . . . . . . . . . . . . 16
β’ ((π + 1) β β β
if((π + 1) β β,
((π +
1)ββ¦(π +
1) / πβ¦π΄), 1) = ((π + 1)ββ¦(π + 1) / πβ¦π΄)) |
202 | 200, 201 | sylan9eq 2230 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β (πΉβ(π + 1)) = ((π + 1)ββ¦(π + 1) / πβ¦π΄)) |
203 | 202 | breq2d 4015 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β (π β₯ (πΉβ(π + 1)) β π β₯ ((π + 1)ββ¦(π + 1) / πβ¦π΄))) |
204 | 197, 203 | mtbird 673 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β Β¬ π β₯ (πΉβ(π + 1))) |
205 | 86, 198, 88 | syl2an2r 595 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β β β§ (π + 1) β π)) β (πΉβ(π + 1)) β β) |
206 | 205 | adantr 276 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β (πΉβ(π + 1)) β β) |
207 | | pceq0 12320 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (πΉβ(π + 1)) β β) β ((π pCnt (πΉβ(π + 1))) = 0 β Β¬ π β₯ (πΉβ(π + 1)))) |
208 | 190, 206,
207 | syl2anc 411 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β ((π pCnt (πΉβ(π + 1))) = 0 β Β¬ π β₯ (πΉβ(π + 1)))) |
209 | 204, 208 | mpbird 167 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β (π pCnt (πΉβ(π + 1))) = 0) |
210 | | iffalse 3542 |
. . . . . . . . . . . . . . 15
β’ (Β¬
(π + 1) β β
β if((π + 1) β
β, ((π +
1)ββ¦(π +
1) / πβ¦π΄), 1) = 1) |
211 | 200, 210 | sylan9eq 2230 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ Β¬ (π + 1) β β) β (πΉβ(π + 1)) = 1) |
212 | 211 | oveq2d 5890 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ Β¬ (π + 1) β β) β (π pCnt (πΉβ(π + 1))) = (π pCnt 1)) |
213 | 28 | ad2antrr 488 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ Β¬ (π + 1) β β) β (π pCnt 1) = 0) |
214 | 212, 213 | eqtrd 2210 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ Β¬ (π + 1) β β) β (π pCnt (πΉβ(π + 1))) = 0) |
215 | | exmiddc 836 |
. . . . . . . . . . . . 13
β’
(DECID (π + 1) β β β ((π + 1) β β β¨ Β¬
(π + 1) β
β)) |
216 | 198, 107,
215 | 3syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) β π)) β ((π + 1) β β β¨ Β¬ (π + 1) β
β)) |
217 | 209, 214,
216 | mpjaodan 798 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π pCnt (πΉβ(π + 1))) = 0) |
218 | 217 | oveq2d 5890 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (π + 1) β π)) β ((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1)))) = ((π pCnt (seq1( Β· , πΉ)βπ)) + 0)) |
219 | 26 | adantr 276 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ (π + 1) β π)) β π β β) |
220 | 164 | adantrr 479 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ (π + 1) β π)) β (seq1( Β· , πΉ)βπ) β β) |
221 | 219, 220 | pccld 12299 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π pCnt (seq1( Β· , πΉ)βπ)) β
β0) |
222 | 221 | nn0cnd 9230 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π pCnt (seq1( Β· , πΉ)βπ)) β β) |
223 | 222 | addid1d 8105 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (π + 1) β π)) β ((π pCnt (seq1( Β· , πΉ)βπ)) + 0) = (π pCnt (seq1( Β· , πΉ)βπ))) |
224 | 187, 218,
223 | 3eqtrd 2214 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = (π pCnt (seq1( Β· , πΉ)βπ))) |
225 | 219, 77 | syl 14 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) β π)) β π β β€) |
226 | 146 | ad2antrl 490 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π + 1) β β€) |
227 | | zltlen 9330 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ (π + 1) β β€) β
(π < (π + 1) β (π β€ (π + 1) β§ (π + 1) β π))) |
228 | 225, 226,
227 | syl2anc 411 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π < (π + 1) β (π β€ (π + 1) β§ (π + 1) β π))) |
229 | | simprl 529 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) β π)) β π β β) |
230 | | nnleltp1 9311 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β β) β (π β€ π β π < (π + 1))) |
231 | 178, 229,
230 | syl2an2r 595 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π β€ π β π < (π + 1))) |
232 | | simprr 531 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π + 1) β π) |
233 | 232 | biantrud 304 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π β€ (π + 1) β (π β€ (π + 1) β§ (π + 1) β π))) |
234 | 228, 231,
233 | 3bitr4rd 221 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π β€ (π + 1) β π β€ π)) |
235 | 234 | ifbid 3555 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (π + 1) β π)) β if(π β€ (π + 1), π΅, 0) = if(π β€ π, π΅, 0)) |
236 | 224, 235 | eqeq12d 2192 |
. . . . . . . 8
β’ ((π β§ (π β β β§ (π + 1) β π)) β ((π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0) β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0))) |
237 | 236 | biimprd 158 |
. . . . . . 7
β’ ((π β§ (π β β β§ (π + 1) β π)) β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0))) |
238 | 237 | expr 375 |
. . . . . 6
β’ ((π β§ π β β) β ((π + 1) β π β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0)))) |
239 | 106 | nnzd 9373 |
. . . . . . . 8
β’ ((π β§ π β β) β (π + 1) β β€) |
240 | 162, 77 | syl 14 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β€) |
241 | | zdceq 9327 |
. . . . . . . 8
β’ (((π + 1) β β€ β§ π β β€) β
DECID (π +
1) = π) |
242 | 239, 240,
241 | syl2anc 411 |
. . . . . . 7
β’ ((π β§ π β β) β DECID
(π + 1) = π) |
243 | | dcne 2358 |
. . . . . . 7
β’
(DECID (π + 1) = π β ((π + 1) = π β¨ (π + 1) β π)) |
244 | 242, 243 | sylib 122 |
. . . . . 6
β’ ((π β§ π β β) β ((π + 1) = π β¨ (π + 1) β π)) |
245 | 186, 238,
244 | mpjaod 718 |
. . . . 5
β’ ((π β§ π β β) β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0))) |
246 | 245 | expcom 116 |
. . . 4
β’ (π β β β (π β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0)))) |
247 | 246 | a2d 26 |
. . 3
β’ (π β β β ((π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0)) β (π β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0)))) |
248 | 7, 13, 19, 25, 83, 247 | nnind 8934 |
. 2
β’ (π β β β (π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0))) |
249 | 1, 248 | mpcom 36 |
1
β’ (π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0)) |