Step | Hyp | Ref
| Expression |
1 | | mullid 11217 |
. . 3
β’ (π β β β (1
Β· π) = π) |
2 | 1 | adantl 481 |
. 2
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β β) β (1 Β· π) = π) |
3 | | 1cnd 11213 |
. 2
β’ ((π β§ π΄ β (β€β₯βπ)) β 1 β
β) |
4 | | prodrb.3 |
. . 3
β’ (π β π β (β€β₯βπ)) |
5 | 4 | adantr 480 |
. 2
β’ ((π β§ π΄ β (β€β₯βπ)) β π β (β€β₯βπ)) |
6 | | iftrue 4529 |
. . . . . . . . 9
β’ (π β π΄ β if(π β π΄, π΅, 1) = π΅) |
7 | 6 | adantl 481 |
. . . . . . . 8
β’ (((π β§ π β β€) β§ π β π΄) β if(π β π΄, π΅, 1) = π΅) |
8 | | prodmo.2 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β π΅ β β) |
9 | 8 | adantlr 712 |
. . . . . . . 8
β’ (((π β§ π β β€) β§ π β π΄) β π΅ β β) |
10 | 7, 9 | eqeltrd 2827 |
. . . . . . 7
β’ (((π β§ π β β€) β§ π β π΄) β if(π β π΄, π΅, 1) β β) |
11 | 10 | ex 412 |
. . . . . 6
β’ ((π β§ π β β€) β (π β π΄ β if(π β π΄, π΅, 1) β β)) |
12 | | iffalse 4532 |
. . . . . . 7
β’ (Β¬
π β π΄ β if(π β π΄, π΅, 1) = 1) |
13 | | ax-1cn 11170 |
. . . . . . 7
β’ 1 β
β |
14 | 12, 13 | eqeltrdi 2835 |
. . . . . 6
β’ (Β¬
π β π΄ β if(π β π΄, π΅, 1) β β) |
15 | 11, 14 | pm2.61d1 180 |
. . . . 5
β’ ((π β§ π β β€) β if(π β π΄, π΅, 1) β β) |
16 | | prodmo.1 |
. . . . 5
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 1)) |
17 | 15, 16 | fmptd 7109 |
. . . 4
β’ (π β πΉ:β€βΆβ) |
18 | | uzssz 12847 |
. . . . 5
β’
(β€β₯βπ) β β€ |
19 | 18, 4 | sselid 3975 |
. . . 4
β’ (π β π β β€) |
20 | 17, 19 | ffvelcdmd 7081 |
. . 3
β’ (π β (πΉβπ) β β) |
21 | 20 | adantr 480 |
. 2
β’ ((π β§ π΄ β (β€β₯βπ)) β (πΉβπ) β β) |
22 | | elfzelz 13507 |
. . . . 5
β’ (π β (π...(π β 1)) β π β β€) |
23 | 22 | adantl 481 |
. . . 4
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β π β β€) |
24 | | simplr 766 |
. . . . . 6
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β π΄ β (β€β₯βπ)) |
25 | 19 | zcnd 12671 |
. . . . . . . . . 10
β’ (π β π β β) |
26 | 25 | adantr 480 |
. . . . . . . . 9
β’ ((π β§ π΄ β (β€β₯βπ)) β π β β) |
27 | 26 | adantr 480 |
. . . . . . . 8
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β π β β) |
28 | | 1cnd 11213 |
. . . . . . . 8
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β 1 β
β) |
29 | 27, 28 | npcand 11579 |
. . . . . . 7
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β ((π β 1) + 1) = π) |
30 | 29 | fveq2d 6889 |
. . . . . 6
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β
(β€β₯β((π β 1) + 1)) =
(β€β₯βπ)) |
31 | 24, 30 | sseqtrrd 4018 |
. . . . 5
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β π΄ β
(β€β₯β((π β 1) + 1))) |
32 | | fznuz 13589 |
. . . . . 6
β’ (π β (π...(π β 1)) β Β¬ π β (β€β₯β((π β 1) +
1))) |
33 | 32 | adantl 481 |
. . . . 5
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β Β¬ π β
(β€β₯β((π β 1) + 1))) |
34 | 31, 33 | ssneldd 3980 |
. . . 4
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β Β¬ π β π΄) |
35 | 23, 34 | eldifd 3954 |
. . 3
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β π β (β€ β π΄)) |
36 | | fveqeq2 6894 |
. . . 4
β’ (π = π β ((πΉβπ) = 1 β (πΉβπ) = 1)) |
37 | | eldifi 4121 |
. . . . . 6
β’ (π β (β€ β π΄) β π β β€) |
38 | | eldifn 4122 |
. . . . . . . 8
β’ (π β (β€ β π΄) β Β¬ π β π΄) |
39 | 38, 12 | syl 17 |
. . . . . . 7
β’ (π β (β€ β π΄) β if(π β π΄, π΅, 1) = 1) |
40 | 39, 13 | eqeltrdi 2835 |
. . . . . 6
β’ (π β (β€ β π΄) β if(π β π΄, π΅, 1) β β) |
41 | 16 | fvmpt2 7003 |
. . . . . 6
β’ ((π β β€ β§ if(π β π΄, π΅, 1) β β) β (πΉβπ) = if(π β π΄, π΅, 1)) |
42 | 37, 40, 41 | syl2anc 583 |
. . . . 5
β’ (π β (β€ β π΄) β (πΉβπ) = if(π β π΄, π΅, 1)) |
43 | 42, 39 | eqtrd 2766 |
. . . 4
β’ (π β (β€ β π΄) β (πΉβπ) = 1) |
44 | 36, 43 | vtoclga 3560 |
. . 3
β’ (π β (β€ β π΄) β (πΉβπ) = 1) |
45 | 35, 44 | syl 17 |
. 2
β’ (((π β§ π΄ β (β€β₯βπ)) β§ π β (π...(π β 1))) β (πΉβπ) = 1) |
46 | 2, 3, 5, 21, 45 | seqid 14018 |
1
β’ ((π β§ π΄ β (β€β₯βπ)) β (seqπ( Β· , πΉ) βΎ
(β€β₯βπ)) = seqπ( Β· , πΉ)) |