Step | Hyp | Ref
| Expression |
1 | | eqid 2726 |
. 2
β’
(β€β₯βπ) = (β€β₯βπ) |
2 | | prodrb.3 |
. . 3
β’ (π β π β (β€β₯βπ)) |
3 | | eluzelz 12836 |
. . 3
β’ (π β
(β€β₯βπ) β π β β€) |
4 | 2, 3 | syl 17 |
. 2
β’ (π β π β β€) |
5 | | seqex 13974 |
. . 3
β’ seqπ( Β· , πΉ) β V |
6 | 5 | a1i 11 |
. 2
β’ (π β seqπ( Β· , πΉ) β V) |
7 | | eqid 2726 |
. . . 4
β’
(β€β₯βπ) = (β€β₯βπ) |
8 | | eluzel2 12831 |
. . . . 5
β’ (π β
(β€β₯βπ) β π β β€) |
9 | 2, 8 | syl 17 |
. . . 4
β’ (π β π β β€) |
10 | | eluzelz 12836 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β π β β€) |
11 | 10 | adantl 481 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β π β β€) |
12 | | iftrue 4529 |
. . . . . . . . . 10
β’ (π β π΄ β if(π β π΄, π΅, 1) = π΅) |
13 | 12 | adantl 481 |
. . . . . . . . 9
β’ (((π β§ π β (β€β₯βπ)) β§ π β π΄) β if(π β π΄, π΅, 1) = π΅) |
14 | | prodmo.2 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β π΅ β β) |
15 | 14 | adantlr 712 |
. . . . . . . . 9
β’ (((π β§ π β (β€β₯βπ)) β§ π β π΄) β π΅ β β) |
16 | 13, 15 | eqeltrd 2827 |
. . . . . . . 8
β’ (((π β§ π β (β€β₯βπ)) β§ π β π΄) β if(π β π΄, π΅, 1) β β) |
17 | 16 | ex 412 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β (π β π΄ β if(π β π΄, π΅, 1) β β)) |
18 | | iffalse 4532 |
. . . . . . . 8
β’ (Β¬
π β π΄ β if(π β π΄, π΅, 1) = 1) |
19 | | ax-1cn 11170 |
. . . . . . . 8
β’ 1 β
β |
20 | 18, 19 | eqeltrdi 2835 |
. . . . . . 7
β’ (Β¬
π β π΄ β if(π β π΄, π΅, 1) β β) |
21 | 17, 20 | pm2.61d1 180 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β if(π β π΄, π΅, 1) β β) |
22 | | prodmo.1 |
. . . . . . 7
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 1)) |
23 | 22 | fvmpt2 7003 |
. . . . . 6
β’ ((π β β€ β§ if(π β π΄, π΅, 1) β β) β (πΉβπ) = if(π β π΄, π΅, 1)) |
24 | 11, 21, 23 | syl2anc 583 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) = if(π β π΄, π΅, 1)) |
25 | 24, 21 | eqeltrd 2827 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
26 | 7, 9, 25 | prodf 15839 |
. . 3
β’ (π β seqπ( Β· , πΉ):(β€β₯βπ)βΆβ) |
27 | 26, 2 | ffvelcdmd 7081 |
. 2
β’ (π β (seqπ( Β· , πΉ)βπ) β β) |
28 | | mulrid 11216 |
. . . . 5
β’ (π β β β (π Β· 1) = π) |
29 | 28 | adantl 481 |
. . . 4
β’ (((π β§ π β (β€β₯βπ)) β§ π β β) β (π Β· 1) = π) |
30 | 2 | adantr 480 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
31 | | simpr 484 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
32 | 9 | adantr 480 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β π β β€) |
33 | 25 | adantlr 712 |
. . . . . 6
β’ (((π β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
34 | 7, 32, 33 | prodf 15839 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ)) β seqπ( Β· , πΉ):(β€β₯βπ)βΆβ) |
35 | 34, 30 | ffvelcdmd 7081 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β (seqπ( Β· , πΉ)βπ) β β) |
36 | | elfzuz 13503 |
. . . . . 6
β’ (π β ((π + 1)...π) β π β (β€β₯β(π + 1))) |
37 | | eluzelz 12836 |
. . . . . . . . 9
β’ (π β
(β€β₯β(π + 1)) β π β β€) |
38 | 37 | adantl 481 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯β(π + 1))) β π β
β€) |
39 | | fprodcvg.4 |
. . . . . . . . . . . 12
β’ (π β π΄ β (π...π)) |
40 | 39 | sseld 3976 |
. . . . . . . . . . 11
β’ (π β (π β π΄ β π β (π...π))) |
41 | | fznuz 13589 |
. . . . . . . . . . 11
β’ (π β (π...π) β Β¬ π β (β€β₯β(π + 1))) |
42 | 40, 41 | syl6 35 |
. . . . . . . . . 10
β’ (π β (π β π΄ β Β¬ π β (β€β₯β(π + 1)))) |
43 | 42 | con2d 134 |
. . . . . . . . 9
β’ (π β (π β (β€β₯β(π + 1)) β Β¬ π β π΄)) |
44 | 43 | imp 406 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯β(π + 1))) β Β¬ π β π΄) |
45 | 38, 44 | eldifd 3954 |
. . . . . . 7
β’ ((π β§ π β (β€β₯β(π + 1))) β π β (β€ β π΄)) |
46 | | fveqeq2 6894 |
. . . . . . . 8
β’ (π = π β ((πΉβπ) = 1 β (πΉβπ) = 1)) |
47 | | eldifi 4121 |
. . . . . . . . . 10
β’ (π β (β€ β π΄) β π β β€) |
48 | | eldifn 4122 |
. . . . . . . . . . . 12
β’ (π β (β€ β π΄) β Β¬ π β π΄) |
49 | 48, 18 | syl 17 |
. . . . . . . . . . 11
β’ (π β (β€ β π΄) β if(π β π΄, π΅, 1) = 1) |
50 | 49, 19 | eqeltrdi 2835 |
. . . . . . . . . 10
β’ (π β (β€ β π΄) β if(π β π΄, π΅, 1) β β) |
51 | 47, 50, 23 | syl2anc 583 |
. . . . . . . . 9
β’ (π β (β€ β π΄) β (πΉβπ) = if(π β π΄, π΅, 1)) |
52 | 51, 49 | eqtrd 2766 |
. . . . . . . 8
β’ (π β (β€ β π΄) β (πΉβπ) = 1) |
53 | 46, 52 | vtoclga 3560 |
. . . . . . 7
β’ (π β (β€ β π΄) β (πΉβπ) = 1) |
54 | 45, 53 | syl 17 |
. . . . . 6
β’ ((π β§ π β (β€β₯β(π + 1))) β (πΉβπ) = 1) |
55 | 36, 54 | sylan2 592 |
. . . . 5
β’ ((π β§ π β ((π + 1)...π)) β (πΉβπ) = 1) |
56 | 55 | adantlr 712 |
. . . 4
β’ (((π β§ π β (β€β₯βπ)) β§ π β ((π + 1)...π)) β (πΉβπ) = 1) |
57 | 29, 30, 31, 35, 56 | seqid2 14019 |
. . 3
β’ ((π β§ π β (β€β₯βπ)) β (seqπ( Β· , πΉ)βπ) = (seqπ( Β· , πΉ)βπ)) |
58 | 57 | eqcomd 2732 |
. 2
β’ ((π β§ π β (β€β₯βπ)) β (seqπ( Β· , πΉ)βπ) = (seqπ( Β· , πΉ)βπ)) |
59 | 1, 4, 6, 27, 58 | climconst 15493 |
1
β’ (π β seqπ( Β· , πΉ) β (seqπ( Β· , πΉ)βπ)) |