Step | Hyp | Ref
| Expression |
1 | | 1arithlem4.2 |
. . . . 5
β’ πΊ = (π¦ β β β¦ if(π¦ β β, (π¦β(πΉβπ¦)), 1)) |
2 | | 1arithlem4.3 |
. . . . . . 7
β’ (π β πΉ:ββΆβ0) |
3 | 2 | ffvelcdmda 5651 |
. . . . . 6
β’ ((π β§ π¦ β β) β (πΉβπ¦) β
β0) |
4 | 3 | ralrimiva 2550 |
. . . . 5
β’ (π β βπ¦ β β (πΉβπ¦) β
β0) |
5 | 1, 4 | pcmptcl 12339 |
. . . 4
β’ (π β (πΊ:ββΆβ β§ seq1( Β·
, πΊ):ββΆβ)) |
6 | 5 | simprd 114 |
. . 3
β’ (π β seq1( Β· , πΊ):ββΆβ) |
7 | | 1arithlem4.4 |
. . 3
β’ (π β π β β) |
8 | 6, 7 | ffvelcdmd 5652 |
. 2
β’ (π β (seq1( Β· , πΊ)βπ) β β) |
9 | | 1arith.1 |
. . . . . . 7
β’ π = (π β β β¦ (π β β β¦ (π pCnt π))) |
10 | 9 | 1arithlem2 12361 |
. . . . . 6
β’ (((seq1(
Β· , πΊ)βπ) β β β§ π β β) β ((πβ(seq1( Β· , πΊ)βπ))βπ) = (π pCnt (seq1( Β· , πΊ)βπ))) |
11 | 8, 10 | sylan 283 |
. . . . 5
β’ ((π β§ π β β) β ((πβ(seq1( Β· , πΊ)βπ))βπ) = (π pCnt (seq1( Β· , πΊ)βπ))) |
12 | 4 | adantr 276 |
. . . . . 6
β’ ((π β§ π β β) β βπ¦ β β (πΉβπ¦) β
β0) |
13 | 7 | adantr 276 |
. . . . . 6
β’ ((π β§ π β β) β π β β) |
14 | | simpr 110 |
. . . . . 6
β’ ((π β§ π β β) β π β β) |
15 | | fveq2 5515 |
. . . . . 6
β’ (π¦ = π β (πΉβπ¦) = (πΉβπ)) |
16 | 1, 12, 13, 14, 15 | pcmpt 12340 |
. . . . 5
β’ ((π β§ π β β) β (π pCnt (seq1( Β· , πΊ)βπ)) = if(π β€ π, (πΉβπ), 0)) |
17 | | 1arithlem4.5 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ π β€ π)) β (πΉβπ) = 0) |
18 | 17 | anassrs 400 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β€ π) β (πΉβπ) = 0) |
19 | 18 | ifeq2d 3552 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β€ π) β if(π β€ π, (πΉβπ), (πΉβπ)) = if(π β€ π, (πΉβπ), 0)) |
20 | | prmz 12110 |
. . . . . . . . . . 11
β’ (π β β β π β
β€) |
21 | 20 | adantl 277 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β β€) |
22 | 13 | nnzd 9373 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β β€) |
23 | | zdcle 9328 |
. . . . . . . . . 10
β’ ((π β β€ β§ π β β€) β
DECID π β€
π) |
24 | 21, 22, 23 | syl2anc 411 |
. . . . . . . . 9
β’ ((π β§ π β β) β DECID
π β€ π) |
25 | | ifiddc 3568 |
. . . . . . . . 9
β’
(DECID π β€ π β if(π β€ π, (πΉβπ), (πΉβπ)) = (πΉβπ)) |
26 | 24, 25 | syl 14 |
. . . . . . . 8
β’ ((π β§ π β β) β if(π β€ π, (πΉβπ), (πΉβπ)) = (πΉβπ)) |
27 | 26 | adantr 276 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β€ π) β if(π β€ π, (πΉβπ), (πΉβπ)) = (πΉβπ)) |
28 | 19, 27 | eqtr3d 2212 |
. . . . . 6
β’ (((π β§ π β β) β§ π β€ π) β if(π β€ π, (πΉβπ), 0) = (πΉβπ)) |
29 | | iftrue 3539 |
. . . . . . 7
β’ (π β€ π β if(π β€ π, (πΉβπ), 0) = (πΉβπ)) |
30 | 29 | adantl 277 |
. . . . . 6
β’ (((π β§ π β β) β§ π β€ π) β if(π β€ π, (πΉβπ), 0) = (πΉβπ)) |
31 | | zletric 9296 |
. . . . . . 7
β’ ((π β β€ β§ π β β€) β (π β€ π β¨ π β€ π)) |
32 | 22, 21, 31 | syl2anc 411 |
. . . . . 6
β’ ((π β§ π β β) β (π β€ π β¨ π β€ π)) |
33 | 28, 30, 32 | mpjaodan 798 |
. . . . 5
β’ ((π β§ π β β) β if(π β€ π, (πΉβπ), 0) = (πΉβπ)) |
34 | 11, 16, 33 | 3eqtrrd 2215 |
. . . 4
β’ ((π β§ π β β) β (πΉβπ) = ((πβ(seq1( Β· , πΊ)βπ))βπ)) |
35 | 34 | ralrimiva 2550 |
. . 3
β’ (π β βπ β β (πΉβπ) = ((πβ(seq1( Β· , πΊ)βπ))βπ)) |
36 | 9 | 1arithlem3 12362 |
. . . . 5
β’ ((seq1(
Β· , πΊ)βπ) β β β (πβ(seq1( Β· , πΊ)βπ)):ββΆβ0) |
37 | 8, 36 | syl 14 |
. . . 4
β’ (π β (πβ(seq1( Β· , πΊ)βπ)):ββΆβ0) |
38 | | ffn 5365 |
. . . . 5
β’ (πΉ:ββΆβ0 β
πΉ Fn
β) |
39 | | ffn 5365 |
. . . . 5
β’ ((πβ(seq1( Β· , πΊ)βπ)):ββΆβ0 β
(πβ(seq1( Β· ,
πΊ)βπ)) Fn β) |
40 | | eqfnfv 5613 |
. . . . 5
β’ ((πΉ Fn β β§ (πβ(seq1( Β· , πΊ)βπ)) Fn β) β (πΉ = (πβ(seq1( Β· , πΊ)βπ)) β βπ β β (πΉβπ) = ((πβ(seq1( Β· , πΊ)βπ))βπ))) |
41 | 38, 39, 40 | syl2an 289 |
. . . 4
β’ ((πΉ:ββΆβ0 β§
(πβ(seq1( Β· ,
πΊ)βπ)):ββΆβ0)
β (πΉ = (πβ(seq1( Β· , πΊ)βπ)) β βπ β β (πΉβπ) = ((πβ(seq1( Β· , πΊ)βπ))βπ))) |
42 | 2, 37, 41 | syl2anc 411 |
. . 3
β’ (π β (πΉ = (πβ(seq1( Β· , πΊ)βπ)) β βπ β β (πΉβπ) = ((πβ(seq1( Β· , πΊ)βπ))βπ))) |
43 | 35, 42 | mpbird 167 |
. 2
β’ (π β πΉ = (πβ(seq1( Β· , πΊ)βπ))) |
44 | | fveq2 5515 |
. . 3
β’ (π₯ = (seq1( Β· , πΊ)βπ) β (πβπ₯) = (πβ(seq1( Β· , πΊ)βπ))) |
45 | 44 | rspceeqv 2859 |
. 2
β’ (((seq1(
Β· , πΊ)βπ) β β β§ πΉ = (πβ(seq1( Β· , πΊ)βπ))) β βπ₯ β β πΉ = (πβπ₯)) |
46 | 8, 43, 45 | syl2anc 411 |
1
β’ (π β βπ₯ β β πΉ = (πβπ₯)) |