Step | Hyp | Ref
| Expression |
1 | | ser3ge0.1 |
. . . 4
β’ (π β π β (β€β₯βπ)) |
2 | | vex 2742 |
. . . . . 6
β’ π β V |
3 | | ser3le.3 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β (πΊβπ) β β) |
4 | | ser3ge0.2 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
5 | 3, 4 | resubcld 8340 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β ((πΊβπ) β (πΉβπ)) β β) |
6 | | fveq2 5517 |
. . . . . . . 8
β’ (π₯ = π β (πΊβπ₯) = (πΊβπ)) |
7 | | fveq2 5517 |
. . . . . . . 8
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
8 | 6, 7 | oveq12d 5895 |
. . . . . . 7
β’ (π₯ = π β ((πΊβπ₯) β (πΉβπ₯)) = ((πΊβπ) β (πΉβπ))) |
9 | | eqid 2177 |
. . . . . . 7
β’ (π₯ β V β¦ ((πΊβπ₯) β (πΉβπ₯))) = (π₯ β V β¦ ((πΊβπ₯) β (πΉβπ₯))) |
10 | 8, 9 | fvmptg 5594 |
. . . . . 6
β’ ((π β V β§ ((πΊβπ) β (πΉβπ)) β β) β ((π₯ β V β¦ ((πΊβπ₯) β (πΉβπ₯)))βπ) = ((πΊβπ) β (πΉβπ))) |
11 | 2, 5, 10 | sylancr 414 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ)) β ((π₯ β V β¦ ((πΊβπ₯) β (πΉβπ₯)))βπ) = ((πΊβπ) β (πΉβπ))) |
12 | 11, 5 | eqeltrd 2254 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β ((π₯ β V β¦ ((πΊβπ₯) β (πΉβπ₯)))βπ) β β) |
13 | | elfzuz 10023 |
. . . . . . 7
β’ (π β (π...π) β π β (β€β₯βπ)) |
14 | | serle.4 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) β€ (πΊβπ)) |
15 | 13, 14 | sylan2 286 |
. . . . . 6
β’ ((π β§ π β (π...π)) β (πΉβπ) β€ (πΊβπ)) |
16 | 3, 4 | subge0d 8494 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β (0 β€ ((πΊβπ) β (πΉβπ)) β (πΉβπ) β€ (πΊβπ))) |
17 | 13, 16 | sylan2 286 |
. . . . . 6
β’ ((π β§ π β (π...π)) β (0 β€ ((πΊβπ) β (πΉβπ)) β (πΉβπ) β€ (πΊβπ))) |
18 | 15, 17 | mpbird 167 |
. . . . 5
β’ ((π β§ π β (π...π)) β 0 β€ ((πΊβπ) β (πΉβπ))) |
19 | 13, 11 | sylan2 286 |
. . . . 5
β’ ((π β§ π β (π...π)) β ((π₯ β V β¦ ((πΊβπ₯) β (πΉβπ₯)))βπ) = ((πΊβπ) β (πΉβπ))) |
20 | 18, 19 | breqtrrd 4033 |
. . . 4
β’ ((π β§ π β (π...π)) β 0 β€ ((π₯ β V β¦ ((πΊβπ₯) β (πΉβπ₯)))βπ)) |
21 | 1, 12, 20 | ser3ge0 10519 |
. . 3
β’ (π β 0 β€ (seqπ( + , (π₯ β V β¦ ((πΊβπ₯) β (πΉβπ₯))))βπ)) |
22 | 3 | recnd 7988 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β (πΊβπ) β β) |
23 | 4 | recnd 7988 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
24 | 1, 22, 23, 11 | ser3sub 10508 |
. . 3
β’ (π β (seqπ( + , (π₯ β V β¦ ((πΊβπ₯) β (πΉβπ₯))))βπ) = ((seqπ( + , πΊ)βπ) β (seqπ( + , πΉ)βπ))) |
25 | 21, 24 | breqtrd 4031 |
. 2
β’ (π β 0 β€ ((seqπ( + , πΊ)βπ) β (seqπ( + , πΉ)βπ))) |
26 | | eqid 2177 |
. . . . 5
β’
(β€β₯βπ) = (β€β₯βπ) |
27 | | eluzel2 9535 |
. . . . . 6
β’ (π β
(β€β₯βπ) β π β β€) |
28 | 1, 27 | syl 14 |
. . . . 5
β’ (π β π β β€) |
29 | 26, 28, 3 | serfre 10477 |
. . . 4
β’ (π β seqπ( + , πΊ):(β€β₯βπ)βΆβ) |
30 | 29, 1 | ffvelcdmd 5654 |
. . 3
β’ (π β (seqπ( + , πΊ)βπ) β β) |
31 | 26, 28, 4 | serfre 10477 |
. . . 4
β’ (π β seqπ( + , πΉ):(β€β₯βπ)βΆβ) |
32 | 31, 1 | ffvelcdmd 5654 |
. . 3
β’ (π β (seqπ( + , πΉ)βπ) β β) |
33 | 30, 32 | subge0d 8494 |
. 2
β’ (π β (0 β€ ((seqπ( + , πΊ)βπ) β (seqπ( + , πΉ)βπ)) β (seqπ( + , πΉ)βπ) β€ (seqπ( + , πΊ)βπ))) |
34 | 25, 33 | mpbid 147 |
1
β’ (π β (seqπ( + , πΉ)βπ) β€ (seqπ( + , πΊ)βπ)) |