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 | | 1stcof 7956 |
. . . 4
β’ (πΊ:β0βΆ(β Γ
β) β (1st β πΊ):β0βΆβ) |
7 | 5, 6 | syl 17 |
. . 3
β’ (π β (1st β
πΊ):β0βΆβ) |
8 | 7 | frnd 6681 |
. 2
β’ (π β ran (1st
β πΊ) β
β) |
9 | 7 | fdmd 6684 |
. . . 4
β’ (π β dom (1st
β πΊ) =
β0) |
10 | | 0nn0 12435 |
. . . . 5
β’ 0 β
β0 |
11 | | ne0i 4299 |
. . . . 5
β’ (0 β
β0 β β0 β β
) |
12 | 10, 11 | mp1i 13 |
. . . 4
β’ (π β β0 β
β
) |
13 | 9, 12 | eqnetrd 3012 |
. . 3
β’ (π β dom (1st
β πΊ) β
β
) |
14 | | dm0rn0 5885 |
. . . 4
β’ (dom
(1st β πΊ)
= β
β ran (1st β πΊ) = β
) |
15 | 14 | necon3bii 2997 |
. . 3
β’ (dom
(1st β πΊ)
β β
β ran (1st β πΊ) β β
) |
16 | 13, 15 | sylib 217 |
. 2
β’ (π β ran (1st
β πΊ) β
β
) |
17 | | fvco3 6945 |
. . . . . 6
β’ ((πΊ:β0βΆ(β Γ
β) β§ π β
β0) β ((1st β πΊ)βπ) = (1st β(πΊβπ))) |
18 | 5, 17 | sylan 581 |
. . . . 5
β’ ((π β§ π β β0) β
((1st β πΊ)βπ) = (1st β(πΊβπ))) |
19 | 1 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β0) β πΉ:ββΆβ) |
20 | 2 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β0) β π· = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) |
21 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β β0) β π β
β0) |
22 | 10 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β β0) β 0 β
β0) |
23 | 19, 20, 3, 4, 21, 22 | ruclem10 16128 |
. . . . . . 7
β’ ((π β§ π β β0) β
(1st β(πΊβπ)) < (2nd β(πΊβ0))) |
24 | 1, 2, 3, 4 | ruclem4 16123 |
. . . . . . . . . 10
β’ (π β (πΊβ0) = β¨0,
1β©) |
25 | 24 | fveq2d 6851 |
. . . . . . . . 9
β’ (π β (2nd
β(πΊβ0)) =
(2nd ββ¨0, 1β©)) |
26 | | c0ex 11156 |
. . . . . . . . . 10
β’ 0 β
V |
27 | | 1ex 11158 |
. . . . . . . . . 10
β’ 1 β
V |
28 | 26, 27 | op2nd 7935 |
. . . . . . . . 9
β’
(2nd ββ¨0, 1β©) = 1 |
29 | 25, 28 | eqtrdi 2793 |
. . . . . . . 8
β’ (π β (2nd
β(πΊβ0)) =
1) |
30 | 29 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β0) β
(2nd β(πΊβ0)) = 1) |
31 | 23, 30 | breqtrd 5136 |
. . . . . 6
β’ ((π β§ π β β0) β
(1st β(πΊβπ)) < 1) |
32 | 5 | ffvelcdmda 7040 |
. . . . . . . 8
β’ ((π β§ π β β0) β (πΊβπ) β (β Γ
β)) |
33 | | xp1st 7958 |
. . . . . . . 8
β’ ((πΊβπ) β (β Γ β) β
(1st β(πΊβπ)) β β) |
34 | 32, 33 | syl 17 |
. . . . . . 7
β’ ((π β§ π β β0) β
(1st β(πΊβπ)) β β) |
35 | | 1re 11162 |
. . . . . . 7
β’ 1 β
β |
36 | | ltle 11250 |
. . . . . . 7
β’
(((1st β(πΊβπ)) β β β§ 1 β β)
β ((1st β(πΊβπ)) < 1 β (1st
β(πΊβπ)) β€ 1)) |
37 | 34, 35, 36 | sylancl 587 |
. . . . . 6
β’ ((π β§ π β β0) β
((1st β(πΊβπ)) < 1 β (1st
β(πΊβπ)) β€ 1)) |
38 | 31, 37 | mpd 15 |
. . . . 5
β’ ((π β§ π β β0) β
(1st β(πΊβπ)) β€ 1) |
39 | 18, 38 | eqbrtrd 5132 |
. . . 4
β’ ((π β§ π β β0) β
((1st β πΊ)βπ) β€ 1) |
40 | 39 | ralrimiva 3144 |
. . 3
β’ (π β βπ β β0 ((1st
β πΊ)βπ) β€ 1) |
41 | 7 | ffnd 6674 |
. . . 4
β’ (π β (1st β
πΊ) Fn
β0) |
42 | | breq1 5113 |
. . . . 5
β’ (π§ = ((1st β
πΊ)βπ) β (π§ β€ 1 β ((1st β πΊ)βπ) β€ 1)) |
43 | 42 | ralrn 7043 |
. . . 4
β’
((1st β πΊ) Fn β0 β
(βπ§ β ran
(1st β πΊ)π§ β€ 1 β βπ β β0 ((1st
β πΊ)βπ) β€ 1)) |
44 | 41, 43 | syl 17 |
. . 3
β’ (π β (βπ§ β ran (1st
β πΊ)π§ β€ 1 β βπ β β0
((1st β πΊ)βπ) β€ 1)) |
45 | 40, 44 | mpbird 257 |
. 2
β’ (π β βπ§ β ran (1st β πΊ)π§ β€ 1) |
46 | 8, 16, 45 | 3jca 1129 |
1
β’ (π β (ran (1st
β πΊ) β β
β§ ran (1st β πΊ) β β
β§ βπ§ β ran (1st
β πΊ)π§ β€ 1)) |