Step | Hyp | Ref
| Expression |
1 | | eqid 2177 |
. 2
β’
(β€β₯βπ) = (β€β₯βπ) |
2 | | prodrb.3 |
. . 3
β’ (π β π β (β€β₯βπ)) |
3 | | eluzelz 9537 |
. . 3
β’ (π β
(β€β₯βπ) β π β β€) |
4 | 2, 3 | syl 14 |
. 2
β’ (π β π β β€) |
5 | | seqex 10447 |
. . 3
β’ seqπ( Β· , πΉ) β V |
6 | 5 | a1i 9 |
. 2
β’ (π β seqπ( Β· , πΉ) β V) |
7 | | eqid 2177 |
. . . 4
β’
(β€β₯βπ) = (β€β₯βπ) |
8 | | eluzel2 9533 |
. . . . 5
β’ (π β
(β€β₯βπ) β π β β€) |
9 | 2, 8 | syl 14 |
. . . 4
β’ (π β π β β€) |
10 | | eluzelz 9537 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β π β β€) |
11 | 10 | adantl 277 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β π β β€) |
12 | | iftrue 3540 |
. . . . . . . . 9
β’ (π β π΄ β if(π β π΄, π΅, 1) = π΅) |
13 | 12 | adantl 277 |
. . . . . . . 8
β’ (((π β§ π β (β€β₯βπ)) β§ π β π΄) β if(π β π΄, π΅, 1) = π΅) |
14 | | prodmo.2 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β π΅ β β) |
15 | 14 | adantlr 477 |
. . . . . . . 8
β’ (((π β§ π β (β€β₯βπ)) β§ π β π΄) β π΅ β β) |
16 | 13, 15 | eqeltrd 2254 |
. . . . . . 7
β’ (((π β§ π β (β€β₯βπ)) β§ π β π΄) β if(π β π΄, π΅, 1) β β) |
17 | | iffalse 3543 |
. . . . . . . . 9
β’ (Β¬
π β π΄ β if(π β π΄, π΅, 1) = 1) |
18 | | ax-1cn 7904 |
. . . . . . . . 9
β’ 1 β
β |
19 | 17, 18 | eqeltrdi 2268 |
. . . . . . . 8
β’ (Β¬
π β π΄ β if(π β π΄, π΅, 1) β β) |
20 | 19 | adantl 277 |
. . . . . . 7
β’ (((π β§ π β (β€β₯βπ)) β§ Β¬ π β π΄) β if(π β π΄, π΅, 1) β β) |
21 | | prodrbdc.dc |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β DECID
π β π΄) |
22 | | exmiddc 836 |
. . . . . . . 8
β’
(DECID π β π΄ β (π β π΄ β¨ Β¬ π β π΄)) |
23 | 21, 22 | syl 14 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β (π β π΄ β¨ Β¬ π β π΄)) |
24 | 16, 20, 23 | mpjaodan 798 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β if(π β π΄, π΅, 1) β β) |
25 | | prodmo.1 |
. . . . . . 7
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 1)) |
26 | 25 | fvmpt2 5600 |
. . . . . 6
β’ ((π β β€ β§ if(π β π΄, π΅, 1) β β) β (πΉβπ) = if(π β π΄, π΅, 1)) |
27 | 11, 24, 26 | syl2anc 411 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) = if(π β π΄, π΅, 1)) |
28 | 27, 24 | eqeltrd 2254 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
29 | 7, 9, 28 | prodf 11546 |
. . 3
β’ (π β seqπ( Β· , πΉ):(β€β₯βπ)βΆβ) |
30 | 29, 2 | ffvelcdmd 5653 |
. 2
β’ (π β (seqπ( Β· , πΉ)βπ) β β) |
31 | | mulrid 7954 |
. . . . 5
β’ (π β β β (π Β· 1) = π) |
32 | 31 | adantl 277 |
. . . 4
β’ (((π β§ π β (β€β₯βπ)) β§ π β β) β (π Β· 1) = π) |
33 | 2 | adantr 276 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
34 | | simpr 110 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
35 | 9 | adantr 276 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β π β β€) |
36 | 28 | adantlr 477 |
. . . . . 6
β’ (((π β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
37 | 7, 35, 36 | prodf 11546 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ)) β seqπ( Β· , πΉ):(β€β₯βπ)βΆβ) |
38 | 37, 33 | ffvelcdmd 5653 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β (seqπ( Β· , πΉ)βπ) β β) |
39 | | elfzuz 10021 |
. . . . . 6
β’ (π β ((π + 1)...π) β π β (β€β₯β(π + 1))) |
40 | | eluzelz 9537 |
. . . . . . . . 9
β’ (π β
(β€β₯β(π + 1)) β π β β€) |
41 | 40 | adantl 277 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯β(π + 1))) β π β
β€) |
42 | | fprodcvg.4 |
. . . . . . . . . . . 12
β’ (π β π΄ β (π...π)) |
43 | 42 | sseld 3155 |
. . . . . . . . . . 11
β’ (π β (π β π΄ β π β (π...π))) |
44 | | fznuz 10102 |
. . . . . . . . . . 11
β’ (π β (π...π) β Β¬ π β (β€β₯β(π + 1))) |
45 | 43, 44 | syl6 33 |
. . . . . . . . . 10
β’ (π β (π β π΄ β Β¬ π β (β€β₯β(π + 1)))) |
46 | 45 | con2d 624 |
. . . . . . . . 9
β’ (π β (π β (β€β₯β(π + 1)) β Β¬ π β π΄)) |
47 | 46 | imp 124 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯β(π + 1))) β Β¬ π β π΄) |
48 | 41, 47 | eldifd 3140 |
. . . . . . 7
β’ ((π β§ π β (β€β₯β(π + 1))) β π β (β€ β π΄)) |
49 | | fveqeq2 5525 |
. . . . . . . 8
β’ (π = π β ((πΉβπ) = 1 β (πΉβπ) = 1)) |
50 | | eldifi 3258 |
. . . . . . . . . 10
β’ (π β (β€ β π΄) β π β β€) |
51 | | eldifn 3259 |
. . . . . . . . . . . 12
β’ (π β (β€ β π΄) β Β¬ π β π΄) |
52 | 51, 17 | syl 14 |
. . . . . . . . . . 11
β’ (π β (β€ β π΄) β if(π β π΄, π΅, 1) = 1) |
53 | 52, 18 | eqeltrdi 2268 |
. . . . . . . . . 10
β’ (π β (β€ β π΄) β if(π β π΄, π΅, 1) β β) |
54 | 50, 53, 26 | syl2anc 411 |
. . . . . . . . 9
β’ (π β (β€ β π΄) β (πΉβπ) = if(π β π΄, π΅, 1)) |
55 | 54, 52 | eqtrd 2210 |
. . . . . . . 8
β’ (π β (β€ β π΄) β (πΉβπ) = 1) |
56 | 49, 55 | vtoclga 2804 |
. . . . . . 7
β’ (π β (β€ β π΄) β (πΉβπ) = 1) |
57 | 48, 56 | syl 14 |
. . . . . 6
β’ ((π β§ π β (β€β₯β(π + 1))) β (πΉβπ) = 1) |
58 | 39, 57 | sylan2 286 |
. . . . 5
β’ ((π β§ π β ((π + 1)...π)) β (πΉβπ) = 1) |
59 | 58 | adantlr 477 |
. . . 4
β’ (((π β§ π β (β€β₯βπ)) β§ π β ((π + 1)...π)) β (πΉβπ) = 1) |
60 | | fveq2 5516 |
. . . . . 6
β’ (π = π β (πΉβπ) = (πΉβπ)) |
61 | 60 | eleq1d 2246 |
. . . . 5
β’ (π = π β ((πΉβπ) β β β (πΉβπ) β β)) |
62 | 28 | ralrimiva 2550 |
. . . . . 6
β’ (π β βπ β (β€β₯βπ)(πΉβπ) β β) |
63 | 62 | ad2antrr 488 |
. . . . 5
β’ (((π β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β βπ β
(β€β₯βπ)(πΉβπ) β β) |
64 | | simpr 110 |
. . . . 5
β’ (((π β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
65 | 61, 63, 64 | rspcdva 2847 |
. . . 4
β’ (((π β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
66 | | mulcl 7938 |
. . . . 5
β’ ((π β β β§ π£ β β) β (π Β· π£) β β) |
67 | 66 | adantl 277 |
. . . 4
β’ (((π β§ π β (β€β₯βπ)) β§ (π β β β§ π£ β β)) β (π Β· π£) β β) |
68 | 32, 33, 34, 38, 59, 65, 67 | seq3id2 10509 |
. . 3
β’ ((π β§ π β (β€β₯βπ)) β (seqπ( Β· , πΉ)βπ) = (seqπ( Β· , πΉ)βπ)) |
69 | 68 | eqcomd 2183 |
. 2
β’ ((π β§ π β (β€β₯βπ)) β (seqπ( Β· , πΉ)βπ) = (seqπ( Β· , πΉ)βπ)) |
70 | 1, 4, 6, 30, 69 | climconst 11298 |
1
β’ (π β seqπ( Β· , πΉ) β (seqπ( Β· , πΉ)βπ)) |