Step | Hyp | Ref
| Expression |
1 | | ruclem1.5 |
. . . . . . . . 9
β’ (π β π β β) |
2 | | ruclem1.3 |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
3 | | ruclem1.4 |
. . . . . . . . . . 11
β’ (π β π΅ β β) |
4 | 2, 3 | readdcld 11191 |
. . . . . . . . . 10
β’ (π β (π΄ + π΅) β β) |
5 | 4 | rehalfcld 12407 |
. . . . . . . . 9
β’ (π β ((π΄ + π΅) / 2) β β) |
6 | 1, 5 | lenltd 11308 |
. . . . . . . 8
β’ (π β (π β€ ((π΄ + π΅) / 2) β Β¬ ((π΄ + π΅) / 2) < π)) |
7 | | ruclem2.8 |
. . . . . . . . . . 11
β’ (π β π΄ < π΅) |
8 | | avglt2 12399 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π΅ β β) β (π΄ < π΅ β ((π΄ + π΅) / 2) < π΅)) |
9 | 2, 3, 8 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (π΄ < π΅ β ((π΄ + π΅) / 2) < π΅)) |
10 | 7, 9 | mpbid 231 |
. . . . . . . . . 10
β’ (π β ((π΄ + π΅) / 2) < π΅) |
11 | | avglt1 12398 |
. . . . . . . . . . 11
β’ ((((π΄ + π΅) / 2) β β β§ π΅ β β) β (((π΄ + π΅) / 2) < π΅ β ((π΄ + π΅) / 2) < ((((π΄ + π΅) / 2) + π΅) / 2))) |
12 | 5, 3, 11 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (((π΄ + π΅) / 2) < π΅ β ((π΄ + π΅) / 2) < ((((π΄ + π΅) / 2) + π΅) / 2))) |
13 | 10, 12 | mpbid 231 |
. . . . . . . . 9
β’ (π β ((π΄ + π΅) / 2) < ((((π΄ + π΅) / 2) + π΅) / 2)) |
14 | 5, 3 | readdcld 11191 |
. . . . . . . . . . 11
β’ (π β (((π΄ + π΅) / 2) + π΅) β β) |
15 | 14 | rehalfcld 12407 |
. . . . . . . . . 10
β’ (π β ((((π΄ + π΅) / 2) + π΅) / 2) β β) |
16 | | lelttr 11252 |
. . . . . . . . . 10
β’ ((π β β β§ ((π΄ + π΅) / 2) β β β§ ((((π΄ + π΅) / 2) + π΅) / 2) β β) β ((π β€ ((π΄ + π΅) / 2) β§ ((π΄ + π΅) / 2) < ((((π΄ + π΅) / 2) + π΅) / 2)) β π < ((((π΄ + π΅) / 2) + π΅) / 2))) |
17 | 1, 5, 15, 16 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β ((π β€ ((π΄ + π΅) / 2) β§ ((π΄ + π΅) / 2) < ((((π΄ + π΅) / 2) + π΅) / 2)) β π < ((((π΄ + π΅) / 2) + π΅) / 2))) |
18 | 13, 17 | mpan2d 693 |
. . . . . . . 8
β’ (π β (π β€ ((π΄ + π΅) / 2) β π < ((((π΄ + π΅) / 2) + π΅) / 2))) |
19 | 6, 18 | sylbird 260 |
. . . . . . 7
β’ (π β (Β¬ ((π΄ + π΅) / 2) < π β π < ((((π΄ + π΅) / 2) + π΅) / 2))) |
20 | 19 | imp 408 |
. . . . . 6
β’ ((π β§ Β¬ ((π΄ + π΅) / 2) < π) β π < ((((π΄ + π΅) / 2) + π΅) / 2)) |
21 | | ruc.1 |
. . . . . . . . 9
β’ (π β πΉ:ββΆβ) |
22 | | ruc.2 |
. . . . . . . . 9
β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) |
23 | | ruclem1.6 |
. . . . . . . . 9
β’ π = (1st
β(β¨π΄, π΅β©π·π)) |
24 | | ruclem1.7 |
. . . . . . . . 9
β’ π = (2nd
β(β¨π΄, π΅β©π·π)) |
25 | 21, 22, 2, 3, 1, 23,
24 | ruclem1 16120 |
. . . . . . . 8
β’ (π β ((β¨π΄, π΅β©π·π) β (β Γ β) β§
π = if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2)) β§ π = if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅))) |
26 | 25 | simp2d 1144 |
. . . . . . 7
β’ (π β π = if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2))) |
27 | | iffalse 4500 |
. . . . . . 7
β’ (Β¬
((π΄ + π΅) / 2) < π β if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2)) = ((((π΄ + π΅) / 2) + π΅) / 2)) |
28 | 26, 27 | sylan9eq 2797 |
. . . . . 6
β’ ((π β§ Β¬ ((π΄ + π΅) / 2) < π) β π = ((((π΄ + π΅) / 2) + π΅) / 2)) |
29 | 20, 28 | breqtrrd 5138 |
. . . . 5
β’ ((π β§ Β¬ ((π΄ + π΅) / 2) < π) β π < π) |
30 | 29 | ex 414 |
. . . 4
β’ (π β (Β¬ ((π΄ + π΅) / 2) < π β π < π)) |
31 | 30 | con1d 145 |
. . 3
β’ (π β (Β¬ π < π β ((π΄ + π΅) / 2) < π)) |
32 | 25 | simp3d 1145 |
. . . . . 6
β’ (π β π = if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅)) |
33 | | iftrue 4497 |
. . . . . 6
β’ (((π΄ + π΅) / 2) < π β if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅) = ((π΄ + π΅) / 2)) |
34 | 32, 33 | sylan9eq 2797 |
. . . . 5
β’ ((π β§ ((π΄ + π΅) / 2) < π) β π = ((π΄ + π΅) / 2)) |
35 | | simpr 486 |
. . . . 5
β’ ((π β§ ((π΄ + π΅) / 2) < π) β ((π΄ + π΅) / 2) < π) |
36 | 34, 35 | eqbrtrd 5132 |
. . . 4
β’ ((π β§ ((π΄ + π΅) / 2) < π) β π < π) |
37 | 36 | ex 414 |
. . 3
β’ (π β (((π΄ + π΅) / 2) < π β π < π)) |
38 | 31, 37 | syld 47 |
. 2
β’ (π β (Β¬ π < π β π < π)) |
39 | 38 | orrd 862 |
1
β’ (π β (π < π β¨ π < π)) |