Step | Hyp | Ref
| Expression |
1 | | addid2 11343 |
. . 3
β’ (π β β β (0 +
π) = π) |
2 | 1 | adantl 483 |
. 2
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β β) β (0 + π) = π) |
3 | | 0cnd 11153 |
. 2
β’ ((π β§ π΄ β (β€β₯βπ)) β 0 β
β) |
4 | | sumrb.3 |
. . 3
β’ (π β π β (β€β₯βπ)) |
5 | 4 | adantr 482 |
. 2
β’ ((π β§ π΄ β (β€β₯βπ)) β π β (β€β₯βπ)) |
6 | | iftrue 4493 |
. . . . . . . . . 10
β’ (π β π΄ β if(π β π΄, π΅, 0) = π΅) |
7 | 6 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β if(π β π΄, π΅, 0) = π΅) |
8 | | summo.2 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β π΅ β β) |
9 | 7, 8 | eqeltrd 2834 |
. . . . . . . 8
β’ ((π β§ π β π΄) β if(π β π΄, π΅, 0) β β) |
10 | 9 | ex 414 |
. . . . . . 7
β’ (π β (π β π΄ β if(π β π΄, π΅, 0) β β)) |
11 | | iffalse 4496 |
. . . . . . . 8
β’ (Β¬
π β π΄ β if(π β π΄, π΅, 0) = 0) |
12 | | 0cn 11152 |
. . . . . . . 8
β’ 0 β
β |
13 | 11, 12 | eqeltrdi 2842 |
. . . . . . 7
β’ (Β¬
π β π΄ β if(π β π΄, π΅, 0) β β) |
14 | 10, 13 | pm2.61d1 180 |
. . . . . 6
β’ (π β if(π β π΄, π΅, 0) β β) |
15 | 14 | adantr 482 |
. . . . 5
β’ ((π β§ π β β€) β if(π β π΄, π΅, 0) β β) |
16 | | summo.1 |
. . . . 5
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) |
17 | 15, 16 | fmptd 7063 |
. . . 4
β’ (π β πΉ:β€βΆβ) |
18 | 17 | adantr 482 |
. . 3
β’ ((π β§ π΄ β (β€β₯βπ)) β πΉ:β€βΆβ) |
19 | | eluzelz 12778 |
. . . . 5
β’ (π β
(β€β₯βπ) β π β β€) |
20 | 4, 19 | syl 17 |
. . . 4
β’ (π β π β β€) |
21 | 20 | adantr 482 |
. . 3
β’ ((π β§ π΄ β (β€β₯βπ)) β π β β€) |
22 | 18, 21 | ffvelcdmd 7037 |
. 2
β’ ((π β§ π΄ β (β€β₯βπ)) β (πΉβπ) β β) |
23 | | elfzelz 13447 |
. . . . 5
β’ (π β (π...(π β 1)) β π β β€) |
24 | 23 | adantl 483 |
. . . 4
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β π β β€) |
25 | | simplr 768 |
. . . . . 6
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β π΄ β (β€β₯βπ)) |
26 | 20 | zcnd 12613 |
. . . . . . . . 9
β’ (π β π β β) |
27 | 26 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β π β β) |
28 | | ax-1cn 11114 |
. . . . . . . 8
β’ 1 β
β |
29 | | npcan 11415 |
. . . . . . . 8
β’ ((π β β β§ 1 β
β) β ((π β
1) + 1) = π) |
30 | 27, 28, 29 | sylancl 587 |
. . . . . . 7
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β ((π β 1) + 1) = π) |
31 | 30 | fveq2d 6847 |
. . . . . 6
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β
(β€β₯β((π β 1) + 1)) =
(β€β₯βπ)) |
32 | 25, 31 | sseqtrrd 3986 |
. . . . 5
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β π΄ β
(β€β₯β((π β 1) + 1))) |
33 | | fznuz 13529 |
. . . . . 6
β’ (π β (π...(π β 1)) β Β¬ π β (β€β₯β((π β 1) +
1))) |
34 | 33 | adantl 483 |
. . . . 5
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β Β¬ π β
(β€β₯β((π β 1) + 1))) |
35 | 32, 34 | ssneldd 3948 |
. . . 4
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β Β¬ π β π΄) |
36 | 24, 35 | eldifd 3922 |
. . 3
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β π β (β€ β π΄)) |
37 | | fveqeq2 6852 |
. . . 4
β’ (π = π β ((πΉβπ) = 0 β (πΉβπ) = 0)) |
38 | | eldifi 4087 |
. . . . . 6
β’ (π β (β€ β π΄) β π β β€) |
39 | | eldifn 4088 |
. . . . . . . 8
β’ (π β (β€ β π΄) β Β¬ π β π΄) |
40 | 39, 11 | syl 17 |
. . . . . . 7
β’ (π β (β€ β π΄) β if(π β π΄, π΅, 0) = 0) |
41 | 40, 12 | eqeltrdi 2842 |
. . . . . 6
β’ (π β (β€ β π΄) β if(π β π΄, π΅, 0) β β) |
42 | 16 | fvmpt2 6960 |
. . . . . 6
β’ ((π β β€ β§ if(π β π΄, π΅, 0) β β) β (πΉβπ) = if(π β π΄, π΅, 0)) |
43 | 38, 41, 42 | syl2anc 585 |
. . . . 5
β’ (π β (β€ β π΄) β (πΉβπ) = if(π β π΄, π΅, 0)) |
44 | 43, 40 | eqtrd 2773 |
. . . 4
β’ (π β (β€ β π΄) β (πΉβπ) = 0) |
45 | 37, 44 | vtoclga 3533 |
. . 3
β’ (π β (β€ β π΄) β (πΉβπ) = 0) |
46 | 36, 45 | syl 17 |
. 2
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β (πΉβπ) = 0) |
47 | 2, 3, 5, 22, 46 | seqid 13959 |
1
β’ ((π β§ π΄ β (β€β₯βπ)) β (seqπ( + , πΉ) βΎ
(β€β₯βπ)) = seqπ( + , πΉ)) |