Step | Hyp | Ref
| Expression |
1 | | ruclem1.3 |
. . . . 5
β’ (π β π΄ β β) |
2 | 1 | leidd 11728 |
. . . 4
β’ (π β π΄ β€ π΄) |
3 | | ruclem1.4 |
. . . . . . . . 9
β’ (π β π΅ β β) |
4 | 1, 3 | readdcld 11191 |
. . . . . . . 8
β’ (π β (π΄ + π΅) β β) |
5 | 4 | rehalfcld 12407 |
. . . . . . 7
β’ (π β ((π΄ + π΅) / 2) β β) |
6 | 5, 3 | readdcld 11191 |
. . . . . 6
β’ (π β (((π΄ + π΅) / 2) + π΅) β β) |
7 | 6 | rehalfcld 12407 |
. . . . 5
β’ (π β ((((π΄ + π΅) / 2) + π΅) / 2) β β) |
8 | | ruclem2.8 |
. . . . . . 7
β’ (π β π΄ < π΅) |
9 | | avglt1 12398 |
. . . . . . . 8
β’ ((π΄ β β β§ π΅ β β) β (π΄ < π΅ β π΄ < ((π΄ + π΅) / 2))) |
10 | 1, 3, 9 | syl2anc 585 |
. . . . . . 7
β’ (π β (π΄ < π΅ β π΄ < ((π΄ + π΅) / 2))) |
11 | 8, 10 | mpbid 231 |
. . . . . 6
β’ (π β π΄ < ((π΄ + π΅) / 2)) |
12 | | avglt2 12399 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΅ β β) β (π΄ < π΅ β ((π΄ + π΅) / 2) < π΅)) |
13 | 1, 3, 12 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π΄ < π΅ β ((π΄ + π΅) / 2) < π΅)) |
14 | 8, 13 | mpbid 231 |
. . . . . . 7
β’ (π β ((π΄ + π΅) / 2) < π΅) |
15 | | avglt1 12398 |
. . . . . . . 8
β’ ((((π΄ + π΅) / 2) β β β§ π΅ β β) β (((π΄ + π΅) / 2) < π΅ β ((π΄ + π΅) / 2) < ((((π΄ + π΅) / 2) + π΅) / 2))) |
16 | 5, 3, 15 | syl2anc 585 |
. . . . . . 7
β’ (π β (((π΄ + π΅) / 2) < π΅ β ((π΄ + π΅) / 2) < ((((π΄ + π΅) / 2) + π΅) / 2))) |
17 | 14, 16 | mpbid 231 |
. . . . . 6
β’ (π β ((π΄ + π΅) / 2) < ((((π΄ + π΅) / 2) + π΅) / 2)) |
18 | 1, 5, 7, 11, 17 | lttrd 11323 |
. . . . 5
β’ (π β π΄ < ((((π΄ + π΅) / 2) + π΅) / 2)) |
19 | 1, 7, 18 | ltled 11310 |
. . . 4
β’ (π β π΄ β€ ((((π΄ + π΅) / 2) + π΅) / 2)) |
20 | | breq2 5114 |
. . . . 5
β’ (π΄ = if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2)) β (π΄ β€ π΄ β π΄ β€ if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2)))) |
21 | | breq2 5114 |
. . . . 5
β’
(((((π΄ + π΅) / 2) + π΅) / 2) = if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2)) β (π΄ β€ ((((π΄ + π΅) / 2) + π΅) / 2) β π΄ β€ if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2)))) |
22 | 20, 21 | ifboth 4530 |
. . . 4
β’ ((π΄ β€ π΄ β§ π΄ β€ ((((π΄ + π΅) / 2) + π΅) / 2)) β π΄ β€ if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2))) |
23 | 2, 19, 22 | syl2anc 585 |
. . 3
β’ (π β π΄ β€ if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2))) |
24 | | ruc.1 |
. . . . 5
β’ (π β πΉ:ββΆβ) |
25 | | ruc.2 |
. . . . 5
β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) |
26 | | ruclem1.5 |
. . . . 5
β’ (π β π β β) |
27 | | ruclem1.6 |
. . . . 5
β’ π = (1st
β(β¨π΄, π΅β©π·π)) |
28 | | ruclem1.7 |
. . . . 5
β’ π = (2nd
β(β¨π΄, π΅β©π·π)) |
29 | 24, 25, 1, 3, 26, 27, 28 | ruclem1 16120 |
. . . 4
β’ (π β ((β¨π΄, π΅β©π·π) β (β Γ β) β§
π = if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2)) β§ π = if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅))) |
30 | 29 | simp2d 1144 |
. . 3
β’ (π β π = if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2))) |
31 | 23, 30 | breqtrrd 5138 |
. 2
β’ (π β π΄ β€ π) |
32 | | iftrue 4497 |
. . . . . 6
β’ (((π΄ + π΅) / 2) < π β if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2)) = π΄) |
33 | | iftrue 4497 |
. . . . . 6
β’ (((π΄ + π΅) / 2) < π β if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅) = ((π΄ + π΅) / 2)) |
34 | 32, 33 | breq12d 5123 |
. . . . 5
β’ (((π΄ + π΅) / 2) < π β (if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2)) < if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅) β π΄ < ((π΄ + π΅) / 2))) |
35 | 11, 34 | syl5ibrcom 247 |
. . . 4
β’ (π β (((π΄ + π΅) / 2) < π β if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2)) < if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅))) |
36 | | avglt2 12399 |
. . . . . . 7
β’ ((((π΄ + π΅) / 2) β β β§ π΅ β β) β (((π΄ + π΅) / 2) < π΅ β ((((π΄ + π΅) / 2) + π΅) / 2) < π΅)) |
37 | 5, 3, 36 | syl2anc 585 |
. . . . . 6
β’ (π β (((π΄ + π΅) / 2) < π΅ β ((((π΄ + π΅) / 2) + π΅) / 2) < π΅)) |
38 | 14, 37 | mpbid 231 |
. . . . 5
β’ (π β ((((π΄ + π΅) / 2) + π΅) / 2) < π΅) |
39 | | iffalse 4500 |
. . . . . 6
β’ (Β¬
((π΄ + π΅) / 2) < π β if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2)) = ((((π΄ + π΅) / 2) + π΅) / 2)) |
40 | | iffalse 4500 |
. . . . . 6
β’ (Β¬
((π΄ + π΅) / 2) < π β if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅) = π΅) |
41 | 39, 40 | breq12d 5123 |
. . . . 5
β’ (Β¬
((π΄ + π΅) / 2) < π β (if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2)) < if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅) β ((((π΄ + π΅) / 2) + π΅) / 2) < π΅)) |
42 | 38, 41 | syl5ibrcom 247 |
. . . 4
β’ (π β (Β¬ ((π΄ + π΅) / 2) < π β if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2)) < if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅))) |
43 | 35, 42 | pm2.61d 179 |
. . 3
β’ (π β if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2)) < if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅)) |
44 | 29 | simp3d 1145 |
. . 3
β’ (π β π = if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅)) |
45 | 43, 30, 44 | 3brtr4d 5142 |
. 2
β’ (π β π < π) |
46 | 5, 3, 14 | ltled 11310 |
. . . 4
β’ (π β ((π΄ + π΅) / 2) β€ π΅) |
47 | 3 | leidd 11728 |
. . . 4
β’ (π β π΅ β€ π΅) |
48 | | breq1 5113 |
. . . . 5
β’ (((π΄ + π΅) / 2) = if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅) β (((π΄ + π΅) / 2) β€ π΅ β if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅) β€ π΅)) |
49 | | breq1 5113 |
. . . . 5
β’ (π΅ = if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅) β (π΅ β€ π΅ β if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅) β€ π΅)) |
50 | 48, 49 | ifboth 4530 |
. . . 4
β’ ((((π΄ + π΅) / 2) β€ π΅ β§ π΅ β€ π΅) β if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅) β€ π΅) |
51 | 46, 47, 50 | syl2anc 585 |
. . 3
β’ (π β if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅) β€ π΅) |
52 | 44, 51 | eqbrtrd 5132 |
. 2
β’ (π β π β€ π΅) |
53 | 31, 45, 52 | 3jca 1129 |
1
β’ (π β (π΄ β€ π β§ π < π β§ π β€ π΅)) |