Step | Hyp | Ref
| Expression |
1 | | ruc.1 |
. . . . 5
β’ (π β πΉ:ββΆβ) |
2 | | ruc.2 |
. . . . 5
β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) |
3 | | ruc.4 |
. . . . 5
β’ πΆ = ({β¨0, β¨0,
1β©β©} βͺ πΉ) |
4 | | ruc.5 |
. . . . 5
β’ πΊ = seq0(π·, πΆ) |
5 | 1, 2, 3, 4 | ruclem6 16124 |
. . . 4
β’ (π β πΊ:β0βΆ(β Γ
β)) |
6 | | ruclem10.6 |
. . . 4
β’ (π β π β
β0) |
7 | 5, 6 | ffvelcdmd 7041 |
. . 3
β’ (π β (πΊβπ) β (β Γ
β)) |
8 | | xp1st 7958 |
. . 3
β’ ((πΊβπ) β (β Γ β) β
(1st β(πΊβπ)) β β) |
9 | 7, 8 | syl 17 |
. 2
β’ (π β (1st
β(πΊβπ)) β
β) |
10 | | ruclem10.7 |
. . . . 5
β’ (π β π β
β0) |
11 | 10, 6 | ifcld 4537 |
. . . 4
β’ (π β if(π β€ π, π, π) β
β0) |
12 | 5, 11 | ffvelcdmd 7041 |
. . 3
β’ (π β (πΊβif(π β€ π, π, π)) β (β Γ
β)) |
13 | | xp1st 7958 |
. . 3
β’ ((πΊβif(π β€ π, π, π)) β (β Γ β) β
(1st β(πΊβif(π β€ π, π, π))) β β) |
14 | 12, 13 | syl 17 |
. 2
β’ (π β (1st
β(πΊβif(π β€ π, π, π))) β β) |
15 | 5, 10 | ffvelcdmd 7041 |
. . 3
β’ (π β (πΊβπ) β (β Γ
β)) |
16 | | xp2nd 7959 |
. . 3
β’ ((πΊβπ) β (β Γ β) β
(2nd β(πΊβπ)) β β) |
17 | 15, 16 | syl 17 |
. 2
β’ (π β (2nd
β(πΊβπ)) β
β) |
18 | 6 | nn0red 12481 |
. . . . . 6
β’ (π β π β β) |
19 | 10 | nn0red 12481 |
. . . . . 6
β’ (π β π β β) |
20 | | max1 13111 |
. . . . . 6
β’ ((π β β β§ π β β) β π β€ if(π β€ π, π, π)) |
21 | 18, 19, 20 | syl2anc 585 |
. . . . 5
β’ (π β π β€ if(π β€ π, π, π)) |
22 | 6 | nn0zd 12532 |
. . . . . 6
β’ (π β π β β€) |
23 | 11 | nn0zd 12532 |
. . . . . 6
β’ (π β if(π β€ π, π, π) β β€) |
24 | | eluz 12784 |
. . . . . 6
β’ ((π β β€ β§ if(π β€ π, π, π) β β€) β (if(π β€ π, π, π) β (β€β₯βπ) β π β€ if(π β€ π, π, π))) |
25 | 22, 23, 24 | syl2anc 585 |
. . . . 5
β’ (π β (if(π β€ π, π, π) β (β€β₯βπ) β π β€ if(π β€ π, π, π))) |
26 | 21, 25 | mpbird 257 |
. . . 4
β’ (π β if(π β€ π, π, π) β (β€β₯βπ)) |
27 | 1, 2, 3, 4, 6, 26 | ruclem9 16127 |
. . 3
β’ (π β ((1st
β(πΊβπ)) β€ (1st
β(πΊβif(π β€ π, π, π))) β§ (2nd β(πΊβif(π β€ π, π, π))) β€ (2nd β(πΊβπ)))) |
28 | 27 | simpld 496 |
. 2
β’ (π β (1st
β(πΊβπ)) β€ (1st
β(πΊβif(π β€ π, π, π)))) |
29 | | xp2nd 7959 |
. . . 4
β’ ((πΊβif(π β€ π, π, π)) β (β Γ β) β
(2nd β(πΊβif(π β€ π, π, π))) β β) |
30 | 12, 29 | syl 17 |
. . 3
β’ (π β (2nd
β(πΊβif(π β€ π, π, π))) β β) |
31 | 1, 2, 3, 4 | ruclem8 16126 |
. . . 4
β’ ((π β§ if(π β€ π, π, π) β β0) β
(1st β(πΊβif(π β€ π, π, π))) < (2nd β(πΊβif(π β€ π, π, π)))) |
32 | 11, 31 | mpdan 686 |
. . 3
β’ (π β (1st
β(πΊβif(π β€ π, π, π))) < (2nd β(πΊβif(π β€ π, π, π)))) |
33 | | max2 13113 |
. . . . . . 7
β’ ((π β β β§ π β β) β π β€ if(π β€ π, π, π)) |
34 | 18, 19, 33 | syl2anc 585 |
. . . . . 6
β’ (π β π β€ if(π β€ π, π, π)) |
35 | 10 | nn0zd 12532 |
. . . . . . 7
β’ (π β π β β€) |
36 | | eluz 12784 |
. . . . . . 7
β’ ((π β β€ β§ if(π β€ π, π, π) β β€) β (if(π β€ π, π, π) β (β€β₯βπ) β π β€ if(π β€ π, π, π))) |
37 | 35, 23, 36 | syl2anc 585 |
. . . . . 6
β’ (π β (if(π β€ π, π, π) β (β€β₯βπ) β π β€ if(π β€ π, π, π))) |
38 | 34, 37 | mpbird 257 |
. . . . 5
β’ (π β if(π β€ π, π, π) β (β€β₯βπ)) |
39 | 1, 2, 3, 4, 10, 38 | ruclem9 16127 |
. . . 4
β’ (π β ((1st
β(πΊβπ)) β€ (1st
β(πΊβif(π β€ π, π, π))) β§ (2nd β(πΊβif(π β€ π, π, π))) β€ (2nd β(πΊβπ)))) |
40 | 39 | simprd 497 |
. . 3
β’ (π β (2nd
β(πΊβif(π β€ π, π, π))) β€ (2nd β(πΊβπ))) |
41 | 14, 30, 17, 32, 40 | ltletrd 11322 |
. 2
β’ (π β (1st
β(πΊβif(π β€ π, π, π))) < (2nd β(πΊβπ))) |
42 | 9, 14, 17, 28, 41 | lelttrd 11320 |
1
β’ (π β (1st
β(πΊβπ)) < (2nd
β(πΊβπ))) |