Step | Hyp | Ref
| Expression |
1 | | ruc.2 |
. . . . . 6
β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) |
2 | 1 | oveqd 7426 |
. . . . 5
β’ (π β (β¨π΄, π΅β©π·π) = (β¨π΄, π΅β©(π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))π)) |
3 | | ruclem1.3 |
. . . . . . 7
β’ (π β π΄ β β) |
4 | | ruclem1.4 |
. . . . . . 7
β’ (π β π΅ β β) |
5 | 3, 4 | opelxpd 5716 |
. . . . . 6
β’ (π β β¨π΄, π΅β© β (β Γ
β)) |
6 | | ruclem1.5 |
. . . . . 6
β’ (π β π β β) |
7 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π₯ = β¨π΄, π΅β© β§ π¦ = π) β π¦ = π) |
8 | 7 | breq2d 5161 |
. . . . . . . . . 10
β’ ((π₯ = β¨π΄, π΅β© β§ π¦ = π) β (π < π¦ β π < π)) |
9 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π₯ = β¨π΄, π΅β© β§ π¦ = π) β π₯ = β¨π΄, π΅β©) |
10 | 9 | fveq2d 6896 |
. . . . . . . . . . 11
β’ ((π₯ = β¨π΄, π΅β© β§ π¦ = π) β (1st βπ₯) = (1st
ββ¨π΄, π΅β©)) |
11 | 10 | opeq1d 4880 |
. . . . . . . . . 10
β’ ((π₯ = β¨π΄, π΅β© β§ π¦ = π) β β¨(1st βπ₯), πβ© = β¨(1st
ββ¨π΄, π΅β©), πβ©) |
12 | 9 | fveq2d 6896 |
. . . . . . . . . . . . 13
β’ ((π₯ = β¨π΄, π΅β© β§ π¦ = π) β (2nd βπ₯) = (2nd
ββ¨π΄, π΅β©)) |
13 | 12 | oveq2d 7425 |
. . . . . . . . . . . 12
β’ ((π₯ = β¨π΄, π΅β© β§ π¦ = π) β (π + (2nd βπ₯)) = (π + (2nd ββ¨π΄, π΅β©))) |
14 | 13 | oveq1d 7424 |
. . . . . . . . . . 11
β’ ((π₯ = β¨π΄, π΅β© β§ π¦ = π) β ((π + (2nd βπ₯)) / 2) = ((π + (2nd ββ¨π΄, π΅β©)) / 2)) |
15 | 14, 12 | opeq12d 4882 |
. . . . . . . . . 10
β’ ((π₯ = β¨π΄, π΅β© β§ π¦ = π) β β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β© = β¨((π + (2nd
ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©) |
16 | 8, 11, 15 | ifbieq12d 4557 |
. . . . . . . . 9
β’ ((π₯ = β¨π΄, π΅β© β§ π¦ = π) β if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©) = if(π < π, β¨(1st ββ¨π΄, π΅β©), πβ©, β¨((π + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©)) |
17 | 16 | csbeq2dv 3901 |
. . . . . . . 8
β’ ((π₯ = β¨π΄, π΅β© β§ π¦ = π) β β¦(((1st
βπ₯) + (2nd
βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©) =
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π, β¨(1st ββ¨π΄, π΅β©), πβ©, β¨((π + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©)) |
18 | 10, 12 | oveq12d 7427 |
. . . . . . . . . 10
β’ ((π₯ = β¨π΄, π΅β© β§ π¦ = π) β ((1st βπ₯) + (2nd βπ₯)) = ((1st
ββ¨π΄, π΅β©) + (2nd
ββ¨π΄, π΅β©))) |
19 | 18 | oveq1d 7424 |
. . . . . . . . 9
β’ ((π₯ = β¨π΄, π΅β© β§ π¦ = π) β (((1st βπ₯) + (2nd βπ₯)) / 2) = (((1st
ββ¨π΄, π΅β©) + (2nd
ββ¨π΄, π΅β©)) / 2)) |
20 | 19 | csbeq1d 3898 |
. . . . . . . 8
β’ ((π₯ = β¨π΄, π΅β© β§ π¦ = π) β β¦(((1st
βπ₯) + (2nd
βπ₯)) / 2) / πβ¦if(π < π, β¨(1st ββ¨π΄, π΅β©), πβ©, β¨((π + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©) =
β¦(((1st ββ¨π΄, π΅β©) + (2nd ββ¨π΄, π΅β©)) / 2) / πβ¦if(π < π, β¨(1st ββ¨π΄, π΅β©), πβ©, β¨((π + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©)) |
21 | 17, 20 | eqtrd 2773 |
. . . . . . 7
β’ ((π₯ = β¨π΄, π΅β© β§ π¦ = π) β β¦(((1st
βπ₯) + (2nd
βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©) =
β¦(((1st ββ¨π΄, π΅β©) + (2nd ββ¨π΄, π΅β©)) / 2) / πβ¦if(π < π, β¨(1st ββ¨π΄, π΅β©), πβ©, β¨((π + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©)) |
22 | | eqid 2733 |
. . . . . . 7
β’ (π₯ β (β Γ
β), π¦ β β
β¦ β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©)) = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©)) |
23 | | opex 5465 |
. . . . . . . . 9
β’
β¨(1st ββ¨π΄, π΅β©), πβ© β V |
24 | | opex 5465 |
. . . . . . . . 9
β’
β¨((π +
(2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β© β
V |
25 | 23, 24 | ifex 4579 |
. . . . . . . 8
β’ if(π < π, β¨(1st ββ¨π΄, π΅β©), πβ©, β¨((π + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©) β
V |
26 | 25 | csbex 5312 |
. . . . . . 7
β’
β¦(((1st ββ¨π΄, π΅β©) + (2nd ββ¨π΄, π΅β©)) / 2) / πβ¦if(π < π, β¨(1st ββ¨π΄, π΅β©), πβ©, β¨((π + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©) β
V |
27 | 21, 22, 26 | ovmpoa 7563 |
. . . . . 6
β’
((β¨π΄, π΅β© β (β Γ
β) β§ π β
β) β (β¨π΄,
π΅β©(π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))π) = β¦(((1st
ββ¨π΄, π΅β©) + (2nd
ββ¨π΄, π΅β©)) / 2) / πβ¦if(π < π, β¨(1st ββ¨π΄, π΅β©), πβ©, β¨((π + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©)) |
28 | 5, 6, 27 | syl2anc 585 |
. . . . 5
β’ (π β (β¨π΄, π΅β©(π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))π) = β¦(((1st
ββ¨π΄, π΅β©) + (2nd
ββ¨π΄, π΅β©)) / 2) / πβ¦if(π < π, β¨(1st ββ¨π΄, π΅β©), πβ©, β¨((π + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©)) |
29 | 2, 28 | eqtrd 2773 |
. . . 4
β’ (π β (β¨π΄, π΅β©π·π) = β¦(((1st
ββ¨π΄, π΅β©) + (2nd
ββ¨π΄, π΅β©)) / 2) / πβ¦if(π < π, β¨(1st ββ¨π΄, π΅β©), πβ©, β¨((π + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©)) |
30 | | op1stg 7987 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΅ β β) β
(1st ββ¨π΄, π΅β©) = π΄) |
31 | 3, 4, 30 | syl2anc 585 |
. . . . . . . 8
β’ (π β (1st
ββ¨π΄, π΅β©) = π΄) |
32 | | op2ndg 7988 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΅ β β) β
(2nd ββ¨π΄, π΅β©) = π΅) |
33 | 3, 4, 32 | syl2anc 585 |
. . . . . . . 8
β’ (π β (2nd
ββ¨π΄, π΅β©) = π΅) |
34 | 31, 33 | oveq12d 7427 |
. . . . . . 7
β’ (π β ((1st
ββ¨π΄, π΅β©) + (2nd
ββ¨π΄, π΅β©)) = (π΄ + π΅)) |
35 | 34 | oveq1d 7424 |
. . . . . 6
β’ (π β (((1st
ββ¨π΄, π΅β©) + (2nd
ββ¨π΄, π΅β©)) / 2) = ((π΄ + π΅) / 2)) |
36 | 35 | csbeq1d 3898 |
. . . . 5
β’ (π β
β¦(((1st ββ¨π΄, π΅β©) + (2nd ββ¨π΄, π΅β©)) / 2) / πβ¦if(π < π, β¨(1st ββ¨π΄, π΅β©), πβ©, β¨((π + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©) =
β¦((π΄ + π΅) / 2) / πβ¦if(π < π, β¨(1st ββ¨π΄, π΅β©), πβ©, β¨((π + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©)) |
37 | | ovex 7442 |
. . . . . . 7
β’ ((π΄ + π΅) / 2) β V |
38 | | breq1 5152 |
. . . . . . . 8
β’ (π = ((π΄ + π΅) / 2) β (π < π β ((π΄ + π΅) / 2) < π)) |
39 | | opeq2 4875 |
. . . . . . . 8
β’ (π = ((π΄ + π΅) / 2) β β¨(1st
ββ¨π΄, π΅β©), πβ© = β¨(1st
ββ¨π΄, π΅β©), ((π΄ + π΅) / 2)β©) |
40 | | oveq1 7416 |
. . . . . . . . . 10
β’ (π = ((π΄ + π΅) / 2) β (π + (2nd ββ¨π΄, π΅β©)) = (((π΄ + π΅) / 2) + (2nd ββ¨π΄, π΅β©))) |
41 | 40 | oveq1d 7424 |
. . . . . . . . 9
β’ (π = ((π΄ + π΅) / 2) β ((π + (2nd ββ¨π΄, π΅β©)) / 2) = ((((π΄ + π΅) / 2) + (2nd ββ¨π΄, π΅β©)) / 2)) |
42 | 41 | opeq1d 4880 |
. . . . . . . 8
β’ (π = ((π΄ + π΅) / 2) β β¨((π + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β© = β¨((((π΄ + π΅) / 2) + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©) |
43 | 38, 39, 42 | ifbieq12d 4557 |
. . . . . . 7
β’ (π = ((π΄ + π΅) / 2) β if(π < π, β¨(1st ββ¨π΄, π΅β©), πβ©, β¨((π + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©) = if(((π΄ + π΅) / 2) < π, β¨(1st ββ¨π΄, π΅β©), ((π΄ + π΅) / 2)β©, β¨((((π΄ + π΅) / 2) + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©)) |
44 | 37, 43 | csbie 3930 |
. . . . . 6
β’
β¦((π΄ +
π΅) / 2) / πβ¦if(π < π, β¨(1st ββ¨π΄, π΅β©), πβ©, β¨((π + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©) = if(((π΄ + π΅) / 2) < π, β¨(1st ββ¨π΄, π΅β©), ((π΄ + π΅) / 2)β©, β¨((((π΄ + π΅) / 2) + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©) |
45 | 31 | opeq1d 4880 |
. . . . . . 7
β’ (π β β¨(1st
ββ¨π΄, π΅β©), ((π΄ + π΅) / 2)β© = β¨π΄, ((π΄ + π΅) / 2)β©) |
46 | 33 | oveq2d 7425 |
. . . . . . . . 9
β’ (π β (((π΄ + π΅) / 2) + (2nd ββ¨π΄, π΅β©)) = (((π΄ + π΅) / 2) + π΅)) |
47 | 46 | oveq1d 7424 |
. . . . . . . 8
β’ (π β ((((π΄ + π΅) / 2) + (2nd ββ¨π΄, π΅β©)) / 2) = ((((π΄ + π΅) / 2) + π΅) / 2)) |
48 | 47, 33 | opeq12d 4882 |
. . . . . . 7
β’ (π β β¨((((π΄ + π΅) / 2) + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β© = β¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©) |
49 | 45, 48 | ifeq12d 4550 |
. . . . . 6
β’ (π β if(((π΄ + π΅) / 2) < π, β¨(1st ββ¨π΄, π΅β©), ((π΄ + π΅) / 2)β©, β¨((((π΄ + π΅) / 2) + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©) = if(((π΄ + π΅) / 2) < π, β¨π΄, ((π΄ + π΅) / 2)β©, β¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©)) |
50 | 44, 49 | eqtrid 2785 |
. . . . 5
β’ (π β β¦((π΄ + π΅) / 2) / πβ¦if(π < π, β¨(1st ββ¨π΄, π΅β©), πβ©, β¨((π + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©) = if(((π΄ + π΅) / 2) < π, β¨π΄, ((π΄ + π΅) / 2)β©, β¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©)) |
51 | 36, 50 | eqtrd 2773 |
. . . 4
β’ (π β
β¦(((1st ββ¨π΄, π΅β©) + (2nd ββ¨π΄, π΅β©)) / 2) / πβ¦if(π < π, β¨(1st ββ¨π΄, π΅β©), πβ©, β¨((π + (2nd ββ¨π΄, π΅β©)) / 2), (2nd
ββ¨π΄, π΅β©)β©) = if(((π΄ + π΅) / 2) < π, β¨π΄, ((π΄ + π΅) / 2)β©, β¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©)) |
52 | 29, 51 | eqtrd 2773 |
. . 3
β’ (π β (β¨π΄, π΅β©π·π) = if(((π΄ + π΅) / 2) < π, β¨π΄, ((π΄ + π΅) / 2)β©, β¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©)) |
53 | 3, 4 | readdcld 11243 |
. . . . . 6
β’ (π β (π΄ + π΅) β β) |
54 | 53 | rehalfcld 12459 |
. . . . 5
β’ (π β ((π΄ + π΅) / 2) β β) |
55 | 3, 54 | opelxpd 5716 |
. . . 4
β’ (π β β¨π΄, ((π΄ + π΅) / 2)β© β (β Γ
β)) |
56 | 54, 4 | readdcld 11243 |
. . . . . 6
β’ (π β (((π΄ + π΅) / 2) + π΅) β β) |
57 | 56 | rehalfcld 12459 |
. . . . 5
β’ (π β ((((π΄ + π΅) / 2) + π΅) / 2) β β) |
58 | 57, 4 | opelxpd 5716 |
. . . 4
β’ (π β β¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β© β (β Γ
β)) |
59 | 55, 58 | ifcld 4575 |
. . 3
β’ (π β if(((π΄ + π΅) / 2) < π, β¨π΄, ((π΄ + π΅) / 2)β©, β¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©) β (β Γ
β)) |
60 | 52, 59 | eqeltrd 2834 |
. 2
β’ (π β (β¨π΄, π΅β©π·π) β (β Γ
β)) |
61 | | ruclem1.6 |
. . 3
β’ π = (1st
β(β¨π΄, π΅β©π·π)) |
62 | 52 | fveq2d 6896 |
. . . 4
β’ (π β (1st
β(β¨π΄, π΅β©π·π)) = (1st βif(((π΄ + π΅) / 2) < π, β¨π΄, ((π΄ + π΅) / 2)β©, β¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©))) |
63 | | fvif 6908 |
. . . . 5
β’
(1st βif(((π΄ + π΅) / 2) < π, β¨π΄, ((π΄ + π΅) / 2)β©, β¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©)) = if(((π΄ + π΅) / 2) < π, (1st ββ¨π΄, ((π΄ + π΅) / 2)β©), (1st
ββ¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©)) |
64 | | op1stg 7987 |
. . . . . . 7
β’ ((π΄ β β β§ ((π΄ + π΅) / 2) β V) β (1st
ββ¨π΄, ((π΄ + π΅) / 2)β©) = π΄) |
65 | 3, 37, 64 | sylancl 587 |
. . . . . 6
β’ (π β (1st
ββ¨π΄, ((π΄ + π΅) / 2)β©) = π΄) |
66 | | ovex 7442 |
. . . . . . 7
β’ ((((π΄ + π΅) / 2) + π΅) / 2) β V |
67 | | op1stg 7987 |
. . . . . . 7
β’
((((((π΄ + π΅) / 2) + π΅) / 2) β V β§ π΅ β β) β (1st
ββ¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©) = ((((π΄ + π΅) / 2) + π΅) / 2)) |
68 | 66, 4, 67 | sylancr 588 |
. . . . . 6
β’ (π β (1st
ββ¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©) = ((((π΄ + π΅) / 2) + π΅) / 2)) |
69 | 65, 68 | ifeq12d 4550 |
. . . . 5
β’ (π β if(((π΄ + π΅) / 2) < π, (1st ββ¨π΄, ((π΄ + π΅) / 2)β©), (1st
ββ¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©)) = if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2))) |
70 | 63, 69 | eqtrid 2785 |
. . . 4
β’ (π β (1st
βif(((π΄ + π΅) / 2) < π, β¨π΄, ((π΄ + π΅) / 2)β©, β¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©)) = if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2))) |
71 | 62, 70 | eqtrd 2773 |
. . 3
β’ (π β (1st
β(β¨π΄, π΅β©π·π)) = if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2))) |
72 | 61, 71 | eqtrid 2785 |
. 2
β’ (π β π = if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2))) |
73 | | ruclem1.7 |
. . 3
β’ π = (2nd
β(β¨π΄, π΅β©π·π)) |
74 | 52 | fveq2d 6896 |
. . . 4
β’ (π β (2nd
β(β¨π΄, π΅β©π·π)) = (2nd βif(((π΄ + π΅) / 2) < π, β¨π΄, ((π΄ + π΅) / 2)β©, β¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©))) |
75 | | fvif 6908 |
. . . . 5
β’
(2nd βif(((π΄ + π΅) / 2) < π, β¨π΄, ((π΄ + π΅) / 2)β©, β¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©)) = if(((π΄ + π΅) / 2) < π, (2nd ββ¨π΄, ((π΄ + π΅) / 2)β©), (2nd
ββ¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©)) |
76 | | op2ndg 7988 |
. . . . . . 7
β’ ((π΄ β β β§ ((π΄ + π΅) / 2) β V) β (2nd
ββ¨π΄, ((π΄ + π΅) / 2)β©) = ((π΄ + π΅) / 2)) |
77 | 3, 37, 76 | sylancl 587 |
. . . . . 6
β’ (π β (2nd
ββ¨π΄, ((π΄ + π΅) / 2)β©) = ((π΄ + π΅) / 2)) |
78 | | op2ndg 7988 |
. . . . . . 7
β’
((((((π΄ + π΅) / 2) + π΅) / 2) β V β§ π΅ β β) β (2nd
ββ¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©) = π΅) |
79 | 66, 4, 78 | sylancr 588 |
. . . . . 6
β’ (π β (2nd
ββ¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©) = π΅) |
80 | 77, 79 | ifeq12d 4550 |
. . . . 5
β’ (π β if(((π΄ + π΅) / 2) < π, (2nd ββ¨π΄, ((π΄ + π΅) / 2)β©), (2nd
ββ¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©)) = if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅)) |
81 | 75, 80 | eqtrid 2785 |
. . . 4
β’ (π β (2nd
βif(((π΄ + π΅) / 2) < π, β¨π΄, ((π΄ + π΅) / 2)β©, β¨((((π΄ + π΅) / 2) + π΅) / 2), π΅β©)) = if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅)) |
82 | 74, 81 | eqtrd 2773 |
. . 3
β’ (π β (2nd
β(β¨π΄, π΅β©π·π)) = if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅)) |
83 | 73, 82 | eqtrid 2785 |
. 2
β’ (π β π = if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅)) |
84 | 60, 72, 83 | 3jca 1129 |
1
β’ (π β ((β¨π΄, π΅β©π·π) β (β Γ β) β§
π = if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2)) β§ π = if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅))) |