Step | Hyp | Ref
| Expression |
1 | | pcmpt.3 |
. 2
β’ (π β π β β) |
2 | | fveq2 6843 |
. . . . . 6
β’ (π = 1 β (seq1( Β· ,
πΉ)βπ) = (seq1( Β· , πΉ)β1)) |
3 | 2 | oveq2d 7374 |
. . . . 5
β’ (π = 1 β (π pCnt (seq1( Β· , πΉ)βπ)) = (π pCnt (seq1( Β· , πΉ)β1))) |
4 | | breq2 5110 |
. . . . . 6
β’ (π = 1 β (π β€ π β π β€ 1)) |
5 | 4 | ifbid 4510 |
. . . . 5
β’ (π = 1 β if(π β€ π, π΅, 0) = if(π β€ 1, π΅, 0)) |
6 | 3, 5 | eqeq12d 2749 |
. . . 4
β’ (π = 1 β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)β1)) = if(π β€ 1, π΅, 0))) |
7 | 6 | imbi2d 341 |
. . 3
β’ (π = 1 β ((π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0)) β (π β (π pCnt (seq1( Β· , πΉ)β1)) = if(π β€ 1, π΅, 0)))) |
8 | | fveq2 6843 |
. . . . . 6
β’ (π = π β (seq1( Β· , πΉ)βπ) = (seq1( Β· , πΉ)βπ)) |
9 | 8 | oveq2d 7374 |
. . . . 5
β’ (π = π β (π pCnt (seq1( Β· , πΉ)βπ)) = (π pCnt (seq1( Β· , πΉ)βπ))) |
10 | | breq2 5110 |
. . . . . 6
β’ (π = π β (π β€ π β π β€ π)) |
11 | 10 | ifbid 4510 |
. . . . 5
β’ (π = π β if(π β€ π, π΅, 0) = if(π β€ π, π΅, 0)) |
12 | 9, 11 | eqeq12d 2749 |
. . . 4
β’ (π = π β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0))) |
13 | 12 | imbi2d 341 |
. . 3
β’ (π = π β ((π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0)) β (π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0)))) |
14 | | fveq2 6843 |
. . . . . 6
β’ (π = (π + 1) β (seq1( Β· , πΉ)βπ) = (seq1( Β· , πΉ)β(π + 1))) |
15 | 14 | oveq2d 7374 |
. . . . 5
β’ (π = (π + 1) β (π pCnt (seq1( Β· , πΉ)βπ)) = (π pCnt (seq1( Β· , πΉ)β(π + 1)))) |
16 | | breq2 5110 |
. . . . . 6
β’ (π = (π + 1) β (π β€ π β π β€ (π + 1))) |
17 | 16 | ifbid 4510 |
. . . . 5
β’ (π = (π + 1) β if(π β€ π, π΅, 0) = if(π β€ (π + 1), π΅, 0)) |
18 | 15, 17 | eqeq12d 2749 |
. . . 4
β’ (π = (π + 1) β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0))) |
19 | 18 | imbi2d 341 |
. . 3
β’ (π = (π + 1) β ((π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0)) β (π β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0)))) |
20 | | fveq2 6843 |
. . . . . 6
β’ (π = π β (seq1( Β· , πΉ)βπ) = (seq1( Β· , πΉ)βπ)) |
21 | 20 | oveq2d 7374 |
. . . . 5
β’ (π = π β (π pCnt (seq1( Β· , πΉ)βπ)) = (π pCnt (seq1( Β· , πΉ)βπ))) |
22 | | breq2 5110 |
. . . . . 6
β’ (π = π β (π β€ π β π β€ π)) |
23 | 22 | ifbid 4510 |
. . . . 5
β’ (π = π β if(π β€ π, π΅, 0) = if(π β€ π, π΅, 0)) |
24 | 21, 23 | eqeq12d 2749 |
. . . 4
β’ (π = π β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0))) |
25 | 24 | imbi2d 341 |
. . 3
β’ (π = π β ((π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0)) β (π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0)))) |
26 | | pcmpt.4 |
. . . 4
β’ (π β π β β) |
27 | | 1z 12538 |
. . . . . . . . 9
β’ 1 β
β€ |
28 | | seq1 13925 |
. . . . . . . . 9
β’ (1 β
β€ β (seq1( Β· , πΉ)β1) = (πΉβ1)) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . 8
β’ (seq1(
Β· , πΉ)β1) =
(πΉβ1) |
30 | | 1nn 12169 |
. . . . . . . . 9
β’ 1 β
β |
31 | | 1nprm 16560 |
. . . . . . . . . . . 12
β’ Β¬ 1
β β |
32 | | eleq1 2822 |
. . . . . . . . . . . 12
β’ (π = 1 β (π β β β 1 β
β)) |
33 | 31, 32 | mtbiri 327 |
. . . . . . . . . . 11
β’ (π = 1 β Β¬ π β
β) |
34 | 33 | iffalsed 4498 |
. . . . . . . . . 10
β’ (π = 1 β if(π β β, (πβπ΄), 1) = 1) |
35 | | pcmpt.1 |
. . . . . . . . . 10
β’ πΉ = (π β β β¦ if(π β β, (πβπ΄), 1)) |
36 | | 1ex 11156 |
. . . . . . . . . 10
β’ 1 β
V |
37 | 34, 35, 36 | fvmpt 6949 |
. . . . . . . . 9
β’ (1 β
β β (πΉβ1)
= 1) |
38 | 30, 37 | ax-mp 5 |
. . . . . . . 8
β’ (πΉβ1) = 1 |
39 | 29, 38 | eqtri 2761 |
. . . . . . 7
β’ (seq1(
Β· , πΉ)β1) =
1 |
40 | 39 | oveq2i 7369 |
. . . . . 6
β’ (π pCnt (seq1( Β· , πΉ)β1)) = (π pCnt 1) |
41 | | pc1 16732 |
. . . . . 6
β’ (π β β β (π pCnt 1) = 0) |
42 | 40, 41 | eqtrid 2785 |
. . . . 5
β’ (π β β β (π pCnt (seq1( Β· , πΉ)β1)) =
0) |
43 | | prmgt1 16578 |
. . . . . . 7
β’ (π β β β 1 <
π) |
44 | | 1re 11160 |
. . . . . . . 8
β’ 1 β
β |
45 | | prmuz2 16577 |
. . . . . . . . 9
β’ (π β β β π β
(β€β₯β2)) |
46 | | eluzelre 12779 |
. . . . . . . . 9
β’ (π β
(β€β₯β2) β π β β) |
47 | 45, 46 | syl 17 |
. . . . . . . 8
β’ (π β β β π β
β) |
48 | | ltnle 11239 |
. . . . . . . 8
β’ ((1
β β β§ π
β β) β (1 < π β Β¬ π β€ 1)) |
49 | 44, 47, 48 | sylancr 588 |
. . . . . . 7
β’ (π β β β (1 <
π β Β¬ π β€ 1)) |
50 | 43, 49 | mpbid 231 |
. . . . . 6
β’ (π β β β Β¬
π β€ 1) |
51 | 50 | iffalsed 4498 |
. . . . 5
β’ (π β β β if(π β€ 1, π΅, 0) = 0) |
52 | 42, 51 | eqtr4d 2776 |
. . . 4
β’ (π β β β (π pCnt (seq1( Β· , πΉ)β1)) = if(π β€ 1, π΅, 0)) |
53 | 26, 52 | syl 17 |
. . 3
β’ (π β (π pCnt (seq1( Β· , πΉ)β1)) = if(π β€ 1, π΅, 0)) |
54 | 26 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ (π + 1) = π)) β π β β) |
55 | | pcmpt.2 |
. . . . . . . . . . . . . . . . 17
β’ (π β βπ β β π΄ β
β0) |
56 | 35, 55 | pcmptcl 16768 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΉ:ββΆβ β§ seq1( Β·
, πΉ):ββΆβ)) |
57 | 56 | simpld 496 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:ββΆβ) |
58 | | peano2nn 12170 |
. . . . . . . . . . . . . . 15
β’ (π β β β (π + 1) β
β) |
59 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:ββΆβ β§
(π + 1) β β)
β (πΉβ(π + 1)) β
β) |
60 | 57, 58, 59 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (πΉβ(π + 1)) β β) |
61 | 60 | adantrr 716 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ (π + 1) = π)) β (πΉβ(π + 1)) β β) |
62 | 54, 61 | pccld 16727 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) = π)) β (π pCnt (πΉβ(π + 1))) β
β0) |
63 | 62 | nn0cnd 12480 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) = π)) β (π pCnt (πΉβ(π + 1))) β β) |
64 | 63 | addid2d 11361 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (π + 1) = π)) β (0 + (π pCnt (πΉβ(π + 1)))) = (π pCnt (πΉβ(π + 1)))) |
65 | 58 | ad2antrl 727 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ (π + 1) = π)) β (π + 1) β β) |
66 | | ovex 7391 |
. . . . . . . . . . . . . . 15
β’ (πβπ΄) β V |
67 | 66, 36 | ifex 4537 |
. . . . . . . . . . . . . 14
β’ if(π β β, (πβπ΄), 1) β V |
68 | 67 | csbex 5269 |
. . . . . . . . . . . . 13
β’
β¦(π +
1) / πβ¦if(π β β, (πβπ΄), 1) β V |
69 | 35 | fvmpts 6952 |
. . . . . . . . . . . . . 14
β’ (((π + 1) β β β§
β¦(π + 1) /
πβ¦if(π β β, (πβπ΄), 1) β V) β (πΉβ(π + 1)) = β¦(π + 1) / πβ¦if(π β β, (πβπ΄), 1)) |
70 | | ovex 7391 |
. . . . . . . . . . . . . . 15
β’ (π + 1) β V |
71 | | nfv 1918 |
. . . . . . . . . . . . . . . 16
β’
β²π(π + 1) β
β |
72 | | nfcv 2904 |
. . . . . . . . . . . . . . . . 17
β’
β²π(π + 1) |
73 | | nfcv 2904 |
. . . . . . . . . . . . . . . . 17
β’
β²πβ |
74 | | nfcsb1v 3881 |
. . . . . . . . . . . . . . . . 17
β’
β²πβ¦(π + 1) / πβ¦π΄ |
75 | 72, 73, 74 | nfov 7388 |
. . . . . . . . . . . . . . . 16
β’
β²π((π + 1)ββ¦(π + 1) / πβ¦π΄) |
76 | | nfcv 2904 |
. . . . . . . . . . . . . . . 16
β’
β²π1 |
77 | 71, 75, 76 | nfif 4517 |
. . . . . . . . . . . . . . 15
β’
β²πif((π + 1) β β, ((π + 1)ββ¦(π + 1) / πβ¦π΄), 1) |
78 | | eleq1 2822 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β (π β β β (π + 1) β β)) |
79 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π + 1) β π = (π + 1)) |
80 | | csbeq1a 3870 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π + 1) β π΄ = β¦(π + 1) / πβ¦π΄) |
81 | 79, 80 | oveq12d 7376 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β (πβπ΄) = ((π + 1)ββ¦(π + 1) / πβ¦π΄)) |
82 | 78, 81 | ifbieq1d 4511 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β if(π β β, (πβπ΄), 1) = if((π + 1) β β, ((π + 1)ββ¦(π + 1) / πβ¦π΄), 1)) |
83 | 70, 77, 82 | csbief 3891 |
. . . . . . . . . . . . . 14
β’
β¦(π +
1) / πβ¦if(π β β, (πβπ΄), 1) = if((π + 1) β β, ((π + 1)ββ¦(π + 1) / πβ¦π΄), 1) |
84 | 69, 83 | eqtrdi 2789 |
. . . . . . . . . . . . 13
β’ (((π + 1) β β β§
β¦(π + 1) /
πβ¦if(π β β, (πβπ΄), 1) β V) β (πΉβ(π + 1)) = if((π + 1) β β, ((π + 1)ββ¦(π + 1) / πβ¦π΄), 1)) |
85 | 65, 68, 84 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) = π)) β (πΉβ(π + 1)) = if((π + 1) β β, ((π + 1)ββ¦(π + 1) / πβ¦π΄), 1)) |
86 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§ (π + 1) = π)) β (π + 1) = π) |
87 | 86, 54 | eqeltrd 2834 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ (π + 1) = π)) β (π + 1) β β) |
88 | 87 | iftrued 4495 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) = π)) β if((π + 1) β β, ((π + 1)ββ¦(π + 1) / πβ¦π΄), 1) = ((π + 1)ββ¦(π + 1) / πβ¦π΄)) |
89 | 86 | csbeq1d 3860 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§ (π + 1) = π)) β β¦(π + 1) / πβ¦π΄ = β¦π / πβ¦π΄) |
90 | | nfcvd 2905 |
. . . . . . . . . . . . . . . 16
β’ (π β β β
β²ππ΅) |
91 | | pcmpt.5 |
. . . . . . . . . . . . . . . 16
β’ (π = π β π΄ = π΅) |
92 | 90, 91 | csbiegf 3890 |
. . . . . . . . . . . . . . 15
β’ (π β β β
β¦π / πβ¦π΄ = π΅) |
93 | 54, 92 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§ (π + 1) = π)) β β¦π / πβ¦π΄ = π΅) |
94 | 89, 93 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ (π + 1) = π)) β β¦(π + 1) / πβ¦π΄ = π΅) |
95 | 86, 94 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) = π)) β ((π + 1)ββ¦(π + 1) / πβ¦π΄) = (πβπ΅)) |
96 | 85, 88, 95 | 3eqtrd 2777 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) = π)) β (πΉβ(π + 1)) = (πβπ΅)) |
97 | 96 | oveq2d 7374 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (π + 1) = π)) β (π pCnt (πΉβ(π + 1))) = (π pCnt (πβπ΅))) |
98 | 91 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (π = π β (π΄ β β0 β π΅ β
β0)) |
99 | 98 | rspcv 3576 |
. . . . . . . . . . . . 13
β’ (π β β β
(βπ β β
π΄ β
β0 β π΅ β
β0)) |
100 | 26, 55, 99 | sylc 65 |
. . . . . . . . . . . 12
β’ (π β π΅ β
β0) |
101 | 100 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) = π)) β π΅ β
β0) |
102 | | pcidlem 16749 |
. . . . . . . . . . 11
β’ ((π β β β§ π΅ β β0)
β (π pCnt (πβπ΅)) = π΅) |
103 | 54, 101, 102 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (π + 1) = π)) β (π pCnt (πβπ΅)) = π΅) |
104 | 64, 97, 103 | 3eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (π + 1) = π)) β (0 + (π pCnt (πΉβ(π + 1)))) = π΅) |
105 | | oveq1 7365 |
. . . . . . . . . 10
β’ ((π pCnt (seq1( Β· , πΉ)βπ)) = 0 β ((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1)))) = (0 + (π pCnt (πΉβ(π + 1))))) |
106 | 105 | eqeq1d 2735 |
. . . . . . . . 9
β’ ((π pCnt (seq1( Β· , πΉ)βπ)) = 0 β (((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1)))) = π΅ β (0 + (π pCnt (πΉβ(π + 1)))) = π΅)) |
107 | 104, 106 | syl5ibrcom 247 |
. . . . . . . 8
β’ ((π β§ (π β β β§ (π + 1) = π)) β ((π pCnt (seq1( Β· , πΉ)βπ)) = 0 β ((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1)))) = π΅)) |
108 | | nnre 12165 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β) |
109 | 108 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) = π)) β π β β) |
110 | | ltp1 12000 |
. . . . . . . . . . . . 13
β’ (π β β β π < (π + 1)) |
111 | | peano2re 11333 |
. . . . . . . . . . . . . 14
β’ (π β β β (π + 1) β
β) |
112 | | ltnle 11239 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π + 1) β β) β
(π < (π + 1) β Β¬ (π + 1) β€ π)) |
113 | 111, 112 | mpdan 686 |
. . . . . . . . . . . . 13
β’ (π β β β (π < (π + 1) β Β¬ (π + 1) β€ π)) |
114 | 110, 113 | mpbid 231 |
. . . . . . . . . . . 12
β’ (π β β β Β¬
(π + 1) β€ π) |
115 | 109, 114 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) = π)) β Β¬ (π + 1) β€ π) |
116 | 86 | breq1d 5116 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) = π)) β ((π + 1) β€ π β π β€ π)) |
117 | 115, 116 | mtbid 324 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (π + 1) = π)) β Β¬ π β€ π) |
118 | 117 | iffalsed 4498 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (π + 1) = π)) β if(π β€ π, π΅, 0) = 0) |
119 | 118 | eqeq2d 2744 |
. . . . . . . 8
β’ ((π β§ (π β β β§ (π + 1) = π)) β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)βπ)) = 0)) |
120 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π β β) |
121 | | nnuz 12811 |
. . . . . . . . . . . . . 14
β’ β =
(β€β₯β1) |
122 | 120, 121 | eleqtrdi 2844 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π β
(β€β₯β1)) |
123 | | seqp1 13927 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯β1) β (seq1( Β· , πΉ)β(π + 1)) = ((seq1( Β· , πΉ)βπ) Β· (πΉβ(π + 1)))) |
124 | 122, 123 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (seq1( Β· ,
πΉ)β(π + 1)) = ((seq1( Β· ,
πΉ)βπ) Β· (πΉβ(π + 1)))) |
125 | 124 | oveq2d 7374 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = (π pCnt ((seq1( Β· , πΉ)βπ) Β· (πΉβ(π + 1))))) |
126 | 26 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β) |
127 | 56 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (π β seq1( Β· , πΉ):ββΆβ) |
128 | 127 | ffvelcdmda 7036 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (seq1( Β· ,
πΉ)βπ) β β) |
129 | | nnz 12525 |
. . . . . . . . . . . . . 14
β’ ((seq1(
Β· , πΉ)βπ) β β β (seq1(
Β· , πΉ)βπ) β
β€) |
130 | | nnne0 12192 |
. . . . . . . . . . . . . 14
β’ ((seq1(
Β· , πΉ)βπ) β β β (seq1(
Β· , πΉ)βπ) β 0) |
131 | 129, 130 | jca 513 |
. . . . . . . . . . . . 13
β’ ((seq1(
Β· , πΉ)βπ) β β β ((seq1(
Β· , πΉ)βπ) β β€ β§ (seq1(
Β· , πΉ)βπ) β 0)) |
132 | 128, 131 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((seq1( Β· ,
πΉ)βπ) β β€ β§ (seq1( Β· ,
πΉ)βπ) β 0)) |
133 | | nnz 12525 |
. . . . . . . . . . . . . 14
β’ ((πΉβ(π + 1)) β β β (πΉβ(π + 1)) β β€) |
134 | | nnne0 12192 |
. . . . . . . . . . . . . 14
β’ ((πΉβ(π + 1)) β β β (πΉβ(π + 1)) β 0) |
135 | 133, 134 | jca 513 |
. . . . . . . . . . . . 13
β’ ((πΉβ(π + 1)) β β β ((πΉβ(π + 1)) β β€ β§ (πΉβ(π + 1)) β 0)) |
136 | 60, 135 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((πΉβ(π + 1)) β β€ β§ (πΉβ(π + 1)) β 0)) |
137 | | pcmul 16728 |
. . . . . . . . . . . 12
β’ ((π β β β§ ((seq1(
Β· , πΉ)βπ) β β€ β§ (seq1(
Β· , πΉ)βπ) β 0) β§ ((πΉβ(π + 1)) β β€ β§ (πΉβ(π + 1)) β 0)) β (π pCnt ((seq1( Β· , πΉ)βπ) Β· (πΉβ(π + 1)))) = ((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1))))) |
138 | 126, 132,
136, 137 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π pCnt ((seq1( Β· , πΉ)βπ) Β· (πΉβ(π + 1)))) = ((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1))))) |
139 | 125, 138 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = ((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1))))) |
140 | 139 | adantrr 716 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (π + 1) = π)) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = ((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1))))) |
141 | | prmnn 16555 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β) |
142 | 26, 141 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
143 | 142 | nnred 12173 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
144 | 143 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) = π)) β π β β) |
145 | 144 | leidd 11726 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) = π)) β π β€ π) |
146 | 145, 86 | breqtrrd 5134 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (π + 1) = π)) β π β€ (π + 1)) |
147 | 146 | iftrued 4495 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (π + 1) = π)) β if(π β€ (π + 1), π΅, 0) = π΅) |
148 | 140, 147 | eqeq12d 2749 |
. . . . . . . 8
β’ ((π β§ (π β β β§ (π + 1) = π)) β ((π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0) β ((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1)))) = π΅)) |
149 | 107, 119,
148 | 3imtr4d 294 |
. . . . . . 7
β’ ((π β§ (π β β β§ (π + 1) = π)) β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0))) |
150 | 149 | expr 458 |
. . . . . 6
β’ ((π β§ π β β) β ((π + 1) = π β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0)))) |
151 | 139 | adantrr 716 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = ((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1))))) |
152 | | simplrr 777 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β (π + 1) β π) |
153 | 152 | necomd 2996 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β π β (π + 1)) |
154 | 26 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β π β
β) |
155 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β (π + 1) β
β) |
156 | 55 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β βπ β β π΄ β
β0) |
157 | 74 | nfel1 2920 |
. . . . . . . . . . . . . . . . . . 19
β’
β²πβ¦(π + 1) / πβ¦π΄ β β0 |
158 | 80 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π + 1) β (π΄ β β0 β
β¦(π + 1) /
πβ¦π΄ β
β0)) |
159 | 157, 158 | rspc 3568 |
. . . . . . . . . . . . . . . . . 18
β’ ((π + 1) β β β
(βπ β β
π΄ β
β0 β β¦(π + 1) / πβ¦π΄ β
β0)) |
160 | 155, 156,
159 | sylc 65 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β
β¦(π + 1) /
πβ¦π΄ β
β0) |
161 | | prmdvdsexpr 16598 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ (π + 1) β β β§
β¦(π + 1) /
πβ¦π΄ β β0)
β (π β₯ ((π + 1)ββ¦(π + 1) / πβ¦π΄) β π = (π + 1))) |
162 | 154, 155,
160, 161 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β (π β₯ ((π + 1)ββ¦(π + 1) / πβ¦π΄) β π = (π + 1))) |
163 | 162 | necon3ad 2953 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β (π β (π + 1) β Β¬ π β₯ ((π + 1)ββ¦(π + 1) / πβ¦π΄))) |
164 | 153, 163 | mpd 15 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β Β¬ π β₯ ((π + 1)ββ¦(π + 1) / πβ¦π΄)) |
165 | 58 | ad2antrl 727 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π + 1) β β) |
166 | 165, 68, 84 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β β β§ (π + 1) β π)) β (πΉβ(π + 1)) = if((π + 1) β β, ((π + 1)ββ¦(π + 1) / πβ¦π΄), 1)) |
167 | | iftrue 4493 |
. . . . . . . . . . . . . . . 16
β’ ((π + 1) β β β
if((π + 1) β β,
((π +
1)ββ¦(π +
1) / πβ¦π΄), 1) = ((π + 1)ββ¦(π + 1) / πβ¦π΄)) |
168 | 166, 167 | sylan9eq 2793 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β (πΉβ(π + 1)) = ((π + 1)ββ¦(π + 1) / πβ¦π΄)) |
169 | 168 | breq2d 5118 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β (π β₯ (πΉβ(π + 1)) β π β₯ ((π + 1)ββ¦(π + 1) / πβ¦π΄))) |
170 | 164, 169 | mtbird 325 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β Β¬ π β₯ (πΉβ(π + 1))) |
171 | 57 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β β β§ (π + 1) β π)) β πΉ:ββΆβ) |
172 | 171, 165,
59 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β β β§ (π + 1) β π)) β (πΉβ(π + 1)) β β) |
173 | 172 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β (πΉβ(π + 1)) β β) |
174 | | pceq0 16748 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (πΉβ(π + 1)) β β) β ((π pCnt (πΉβ(π + 1))) = 0 β Β¬ π β₯ (πΉβ(π + 1)))) |
175 | 154, 173,
174 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β ((π pCnt (πΉβ(π + 1))) = 0 β Β¬ π β₯ (πΉβ(π + 1)))) |
176 | 170, 175 | mpbird 257 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ (π + 1) β β) β (π pCnt (πΉβ(π + 1))) = 0) |
177 | | iffalse 4496 |
. . . . . . . . . . . . . . 15
β’ (Β¬
(π + 1) β β
β if((π + 1) β
β, ((π +
1)ββ¦(π +
1) / πβ¦π΄), 1) = 1) |
178 | 166, 177 | sylan9eq 2793 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ Β¬ (π + 1) β β) β (πΉβ(π + 1)) = 1) |
179 | 178 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ Β¬ (π + 1) β β) β (π pCnt (πΉβ(π + 1))) = (π pCnt 1)) |
180 | 26, 41 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (π pCnt 1) = 0) |
181 | 180 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ Β¬ (π + 1) β β) β (π pCnt 1) = 0) |
182 | 179, 181 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§ (π + 1) β π)) β§ Β¬ (π + 1) β β) β (π pCnt (πΉβ(π + 1))) = 0) |
183 | 176, 182 | pm2.61dan 812 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π pCnt (πΉβ(π + 1))) = 0) |
184 | 183 | oveq2d 7374 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (π + 1) β π)) β ((π pCnt (seq1( Β· , πΉ)βπ)) + (π pCnt (πΉβ(π + 1)))) = ((π pCnt (seq1( Β· , πΉ)βπ)) + 0)) |
185 | 26 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ (π + 1) β π)) β π β β) |
186 | 128 | adantrr 716 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ (π + 1) β π)) β (seq1( Β· , πΉ)βπ) β β) |
187 | 185, 186 | pccld 16727 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π pCnt (seq1( Β· , πΉ)βπ)) β
β0) |
188 | 187 | nn0cnd 12480 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π pCnt (seq1( Β· , πΉ)βπ)) β β) |
189 | 188 | addid1d 11360 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (π + 1) β π)) β ((π pCnt (seq1( Β· , πΉ)βπ)) + 0) = (π pCnt (seq1( Β· , πΉ)βπ))) |
190 | 151, 184,
189 | 3eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = (π pCnt (seq1( Β· , πΉ)βπ))) |
191 | 142 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ (π + 1) β π)) β π β β) |
192 | 191 | nnred 12173 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) β π)) β π β β) |
193 | 165 | nnred 12173 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π + 1) β β) |
194 | 192, 193 | ltlend 11305 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π < (π + 1) β (π β€ (π + 1) β§ (π + 1) β π))) |
195 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) β π)) β π β β) |
196 | | nnleltp1 12563 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β β) β (π β€ π β π < (π + 1))) |
197 | 191, 195,
196 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π β€ π β π < (π + 1))) |
198 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π + 1) β π) |
199 | 198 | biantrud 533 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π β€ (π + 1) β (π β€ (π + 1) β§ (π + 1) β π))) |
200 | 194, 197,
199 | 3bitr4rd 312 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (π + 1) β π)) β (π β€ (π + 1) β π β€ π)) |
201 | 200 | ifbid 4510 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (π + 1) β π)) β if(π β€ (π + 1), π΅, 0) = if(π β€ π, π΅, 0)) |
202 | 190, 201 | eqeq12d 2749 |
. . . . . . . 8
β’ ((π β§ (π β β β§ (π + 1) β π)) β ((π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0) β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0))) |
203 | 202 | biimprd 248 |
. . . . . . 7
β’ ((π β§ (π β β β§ (π + 1) β π)) β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0))) |
204 | 203 | expr 458 |
. . . . . 6
β’ ((π β§ π β β) β ((π + 1) β π β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0)))) |
205 | 150, 204 | pm2.61dne 3028 |
. . . . 5
β’ ((π β§ π β β) β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0))) |
206 | 205 | expcom 415 |
. . . 4
β’ (π β β β (π β ((π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0) β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0)))) |
207 | 206 | a2d 29 |
. . 3
β’ (π β β β ((π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0)) β (π β (π pCnt (seq1( Β· , πΉ)β(π + 1))) = if(π β€ (π + 1), π΅, 0)))) |
208 | 7, 13, 19, 25, 53, 207 | nnind 12176 |
. 2
β’ (π β β β (π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0))) |
209 | 1, 208 | mpcom 38 |
1
β’ (π β (π pCnt (seq1( Β· , πΉ)βπ)) = if(π β€ π, π΅, 0)) |