Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . . . 5
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β πΆ β (βMetβπ)) |
2 | | xmetcl 23606 |
. . . . . . 7
β’ ((πΆ β (βMetβπ) β§ π₯ β π β§ π¦ β π) β (π₯πΆπ¦) β
β*) |
3 | | xmetge0 23619 |
. . . . . . 7
β’ ((πΆ β (βMetβπ) β§ π₯ β π β§ π¦ β π) β 0 β€ (π₯πΆπ¦)) |
4 | | elxrge0 13303 |
. . . . . . 7
β’ ((π₯πΆπ¦) β (0[,]+β) β ((π₯πΆπ¦) β β* β§ 0 β€
(π₯πΆπ¦))) |
5 | 2, 3, 4 | sylanbrc 584 |
. . . . . 6
β’ ((πΆ β (βMetβπ) β§ π₯ β π β§ π¦ β π) β (π₯πΆπ¦) β (0[,]+β)) |
6 | 5 | 3expb 1121 |
. . . . 5
β’ ((πΆ β (βMetβπ) β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β (0[,]+β)) |
7 | 1, 6 | sylan 581 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β (0[,]+β)) |
8 | | xmetf 23604 |
. . . . . . 7
β’ (πΆ β (βMetβπ) β πΆ:(π Γ π)βΆβ*) |
9 | 8 | 3ad2ant1 1134 |
. . . . . 6
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β πΆ:(π Γ π)βΆβ*) |
10 | 9 | ffnd 6665 |
. . . . 5
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β πΆ Fn (π Γ π)) |
11 | | fnov 7480 |
. . . . 5
β’ (πΆ Fn (π Γ π) β πΆ = (π₯ β π, π¦ β π β¦ (π₯πΆπ¦))) |
12 | 10, 11 | sylib 217 |
. . . 4
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β πΆ = (π₯ β π, π¦ β π β¦ (π₯πΆπ¦))) |
13 | | eqidd 2739 |
. . . 4
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β (π§ β (0[,]+β) β¦
if(π§ β€ π
, π§, π
)) = (π§ β (0[,]+β) β¦ if(π§ β€ π
, π§, π
))) |
14 | | breq1 5107 |
. . . . 5
β’ (π§ = (π₯πΆπ¦) β (π§ β€ π
β (π₯πΆπ¦) β€ π
)) |
15 | | id 22 |
. . . . 5
β’ (π§ = (π₯πΆπ¦) β π§ = (π₯πΆπ¦)) |
16 | 14, 15 | ifbieq1d 4509 |
. . . 4
β’ (π§ = (π₯πΆπ¦) β if(π§ β€ π
, π§, π
) = if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
)) |
17 | 7, 12, 13, 16 | fmpoco 8016 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β ((π§ β (0[,]+β) β¦
if(π§ β€ π
, π§, π
)) β πΆ) = (π₯ β π, π¦ β π β¦ if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
))) |
18 | | stdbdmet.1 |
. . 3
β’ π· = (π₯ β π, π¦ β π β¦ if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
)) |
19 | 17, 18 | eqtr4di 2796 |
. 2
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β ((π§ β (0[,]+β) β¦
if(π§ β€ π
, π§, π
)) β πΆ) = π·) |
20 | | eliccxr 13281 |
. . . . 5
β’ (π§ β (0[,]+β) β
π§ β
β*) |
21 | | simp2 1138 |
. . . . 5
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β π
β
β*) |
22 | | ifcl 4530 |
. . . . 5
β’ ((π§ β β*
β§ π
β
β*) β if(π§ β€ π
, π§, π
) β
β*) |
23 | 20, 21, 22 | syl2anr 598 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π§ β (0[,]+β)) β if(π§ β€ π
, π§, π
) β
β*) |
24 | 23 | fmpttd 7058 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β (π§ β (0[,]+β) β¦
if(π§ β€ π
, π§, π
)):(0[,]+β)βΆβ*) |
25 | | id 22 |
. . . . . 6
β’ (π β (0[,]+β) β
π β
(0[,]+β)) |
26 | | vex 3448 |
. . . . . . 7
β’ π β V |
27 | | ifexg 4534 |
. . . . . . 7
β’ ((π β V β§ π
β β*)
β if(π β€ π
, π, π
) β V) |
28 | 26, 21, 27 | sylancr 588 |
. . . . . 6
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β if(π β€ π
, π, π
) β V) |
29 | | breq1 5107 |
. . . . . . . 8
β’ (π§ = π β (π§ β€ π
β π β€ π
)) |
30 | | id 22 |
. . . . . . . 8
β’ (π§ = π β π§ = π) |
31 | 29, 30 | ifbieq1d 4509 |
. . . . . . 7
β’ (π§ = π β if(π§ β€ π
, π§, π
) = if(π β€ π
, π, π
)) |
32 | | eqid 2738 |
. . . . . . 7
β’ (π§ β (0[,]+β) β¦
if(π§ β€ π
, π§, π
)) = (π§ β (0[,]+β) β¦ if(π§ β€ π
, π§, π
)) |
33 | 31, 32 | fvmptg 6942 |
. . . . . 6
β’ ((π β (0[,]+β) β§
if(π β€ π
, π, π
) β V) β ((π§ β (0[,]+β) β¦ if(π§ β€ π
, π§, π
))βπ) = if(π β€ π
, π, π
)) |
34 | 25, 28, 33 | syl2anr 598 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β ((π§ β (0[,]+β) β¦
if(π§ β€ π
, π§, π
))βπ) = if(π β€ π
, π, π
)) |
35 | 34 | eqeq1d 2740 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (((π§ β (0[,]+β) β¦
if(π§ β€ π
, π§, π
))βπ) = 0 β if(π β€ π
, π, π
) = 0)) |
36 | | eqeq1 2742 |
. . . . . 6
β’ (π = if(π β€ π
, π, π
) β (π = 0 β if(π β€ π
, π, π
) = 0)) |
37 | 36 | bibi1d 344 |
. . . . 5
β’ (π = if(π β€ π
, π, π
) β ((π = 0 β π = 0) β (if(π β€ π
, π, π
) = 0 β π = 0))) |
38 | | eqeq1 2742 |
. . . . . 6
β’ (π
= if(π β€ π
, π, π
) β (π
= 0 β if(π β€ π
, π, π
) = 0)) |
39 | 38 | bibi1d 344 |
. . . . 5
β’ (π
= if(π β€ π
, π, π
) β ((π
= 0 β π = 0) β (if(π β€ π
, π, π
) = 0 β π = 0))) |
40 | | biidd 262 |
. . . . 5
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β§ π β€ π
) β (π = 0 β π = 0)) |
41 | | simp3 1139 |
. . . . . . . . 9
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β 0 < π
) |
42 | 41 | gt0ne0d 11653 |
. . . . . . . 8
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β π
β 0) |
43 | 42 | neneqd 2947 |
. . . . . . 7
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β Β¬ π
= 0) |
44 | 43 | ad2antrr 725 |
. . . . . 6
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β§ Β¬ π β€ π
) β Β¬ π
= 0) |
45 | | 0xr 11136 |
. . . . . . . . . . 11
β’ 0 β
β* |
46 | | xrltle 12997 |
. . . . . . . . . . 11
β’ ((0
β β* β§ π
β β*) β (0 <
π
β 0 β€ π
)) |
47 | 45, 21, 46 | sylancr 588 |
. . . . . . . . . 10
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β (0 < π
β 0 β€ π
)) |
48 | 41, 47 | mpd 15 |
. . . . . . . . 9
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β 0 β€ π
) |
49 | 48 | adantr 482 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β 0 β€ π
) |
50 | | breq1 5107 |
. . . . . . . 8
β’ (π = 0 β (π β€ π
β 0 β€ π
)) |
51 | 49, 50 | syl5ibrcom 247 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (π = 0 β π β€ π
)) |
52 | 51 | con3dimp 410 |
. . . . . 6
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β§ Β¬ π β€ π
) β Β¬ π = 0) |
53 | 44, 52 | 2falsed 377 |
. . . . 5
β’ ((((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β§ Β¬ π β€ π
) β (π
= 0 β π = 0)) |
54 | 37, 39, 40, 53 | ifbothda 4523 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (if(π β€ π
, π, π
) = 0 β π = 0)) |
55 | 35, 54 | bitrd 279 |
. . 3
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (((π§ β (0[,]+β) β¦
if(π§ β€ π
, π§, π
))βπ) = 0 β π = 0)) |
56 | | eliccxr 13281 |
. . . . . . . . 9
β’ (π β (0[,]+β) β
π β
β*) |
57 | 56 | ad2antrl 727 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β π β
β*) |
58 | 21 | adantr 482 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β π
β
β*) |
59 | | xrmin1 13025 |
. . . . . . . 8
β’ ((π β β*
β§ π
β
β*) β if(π β€ π
, π, π
) β€ π) |
60 | 57, 58, 59 | syl2anc 585 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β if(π β€ π
, π, π
) β€ π) |
61 | 57, 58 | ifcld 4531 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β if(π β€ π
, π, π
) β
β*) |
62 | | eliccxr 13281 |
. . . . . . . . 9
β’ (π β (0[,]+β) β
π β
β*) |
63 | 62 | ad2antll 728 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β π β
β*) |
64 | | xrletr 13006 |
. . . . . . . 8
β’
((if(π β€ π
, π, π
) β β* β§ π β β*
β§ π β
β*) β ((if(π β€ π
, π, π
) β€ π β§ π β€ π) β if(π β€ π
, π, π
) β€ π)) |
65 | 61, 57, 63, 64 | syl3anc 1372 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β ((if(π β€ π
, π, π
) β€ π β§ π β€ π) β if(π β€ π
, π, π
) β€ π)) |
66 | 60, 65 | mpand 694 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (π β€ π β if(π β€ π
, π, π
) β€ π)) |
67 | | xrmin2 13026 |
. . . . . . 7
β’ ((π β β*
β§ π
β
β*) β if(π β€ π
, π, π
) β€ π
) |
68 | 57, 58, 67 | syl2anc 585 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β if(π β€ π
, π, π
) β€ π
) |
69 | 66, 68 | jctird 528 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (π β€ π β (if(π β€ π
, π, π
) β€ π β§ if(π β€ π
, π, π
) β€ π
))) |
70 | | xrlemin 13032 |
. . . . . 6
β’
((if(π β€ π
, π, π
) β β* β§ π β β*
β§ π
β
β*) β (if(π β€ π
, π, π
) β€ if(π β€ π
, π, π
) β (if(π β€ π
, π, π
) β€ π β§ if(π β€ π
, π, π
) β€ π
))) |
71 | 61, 63, 58, 70 | syl3anc 1372 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (if(π β€ π
, π, π
) β€ if(π β€ π
, π, π
) β (if(π β€ π
, π, π
) β€ π β§ if(π β€ π
, π, π
) β€ π
))) |
72 | 69, 71 | sylibrd 259 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (π β€ π β if(π β€ π
, π, π
) β€ if(π β€ π
, π, π
))) |
73 | 34 | adantrr 716 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β ((π§ β
(0[,]+β) β¦ if(π§
β€ π
, π§, π
))βπ) = if(π β€ π
, π, π
)) |
74 | | simpr 486 |
. . . . . 6
β’ ((π β (0[,]+β) β§
π β (0[,]+β))
β π β
(0[,]+β)) |
75 | | vex 3448 |
. . . . . . 7
β’ π β V |
76 | | ifexg 4534 |
. . . . . . 7
β’ ((π β V β§ π
β β*)
β if(π β€ π
, π, π
) β V) |
77 | 75, 21, 76 | sylancr 588 |
. . . . . 6
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β if(π β€ π
, π, π
) β V) |
78 | | breq1 5107 |
. . . . . . . 8
β’ (π§ = π β (π§ β€ π
β π β€ π
)) |
79 | | id 22 |
. . . . . . . 8
β’ (π§ = π β π§ = π) |
80 | 78, 79 | ifbieq1d 4509 |
. . . . . . 7
β’ (π§ = π β if(π§ β€ π
, π§, π
) = if(π β€ π
, π, π
)) |
81 | 80, 32 | fvmptg 6942 |
. . . . . 6
β’ ((π β (0[,]+β) β§
if(π β€ π
, π, π
) β V) β ((π§ β (0[,]+β) β¦ if(π§ β€ π
, π§, π
))βπ) = if(π β€ π
, π, π
)) |
82 | 74, 77, 81 | syl2anr 598 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β ((π§ β
(0[,]+β) β¦ if(π§
β€ π
, π§, π
))βπ) = if(π β€ π
, π, π
)) |
83 | 73, 82 | breq12d 5117 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (((π§ β
(0[,]+β) β¦ if(π§
β€ π
, π§, π
))βπ) β€ ((π§ β (0[,]+β) β¦ if(π§ β€ π
, π§, π
))βπ) β if(π β€ π
, π, π
) β€ if(π β€ π
, π, π
))) |
84 | 72, 83 | sylibrd 259 |
. . 3
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (π β€ π β ((π§ β (0[,]+β) β¦ if(π§ β€ π
, π§, π
))βπ) β€ ((π§ β (0[,]+β) β¦ if(π§ β€ π
, π§, π
))βπ))) |
85 | 57, 63 | xaddcld 13149 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (π
+π π)
β β*) |
86 | | xrmin1 13025 |
. . . . . . 7
β’ (((π +π π) β β*
β§ π
β
β*) β if((π +π π) β€ π
, (π +π π), π
) β€ (π +π π)) |
87 | 85, 58, 86 | syl2anc 585 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β if((π
+π π)
β€ π
, (π +π π), π
) β€ (π +π π)) |
88 | 85, 58 | ifcld 4531 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β if((π
+π π)
β€ π
, (π +π π), π
) β
β*) |
89 | 57, 58 | xaddcld 13149 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (π
+π π
)
β β*) |
90 | | xrmin2 13026 |
. . . . . . . 8
β’ (((π +π π) β β*
β§ π
β
β*) β if((π +π π) β€ π
, (π +π π), π
) β€ π
) |
91 | 85, 58, 90 | syl2anc 585 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β if((π
+π π)
β€ π
, (π +π π), π
) β€ π
) |
92 | | xaddid2 13090 |
. . . . . . . . 9
β’ (π
β β*
β (0 +π π
) = π
) |
93 | 58, 92 | syl 17 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (0 +π π
) = π
) |
94 | 45 | a1i 11 |
. . . . . . . . 9
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β 0 β β*) |
95 | | elxrge0 13303 |
. . . . . . . . . . 11
β’ (π β (0[,]+β) β
(π β
β* β§ 0 β€ π)) |
96 | 95 | simprbi 498 |
. . . . . . . . . 10
β’ (π β (0[,]+β) β 0
β€ π) |
97 | 96 | ad2antrl 727 |
. . . . . . . . 9
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β 0 β€ π) |
98 | | xleadd1a 13101 |
. . . . . . . . 9
β’ (((0
β β* β§ π β β* β§ π
β β*)
β§ 0 β€ π) β (0
+π π
)
β€ (π
+π π
)) |
99 | 94, 57, 58, 97, 98 | syl31anc 1374 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (0 +π π
) β€ (π +π π
)) |
100 | 93, 99 | eqbrtrrd 5128 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β π
β€ (π +π π
)) |
101 | 88, 58, 89, 91, 100 | xrletrd 13010 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β if((π
+π π)
β€ π
, (π +π π), π
) β€ (π +π π
)) |
102 | | oveq2 7358 |
. . . . . . . 8
β’ (π = if(π β€ π
, π, π
) β (π +π π) = (π +π if(π β€ π
, π, π
))) |
103 | 102 | breq2d 5116 |
. . . . . . 7
β’ (π = if(π β€ π
, π, π
) β (if((π +π π) β€ π
, (π +π π), π
) β€ (π +π π) β if((π +π π) β€ π
, (π +π π), π
) β€ (π +π if(π β€ π
, π, π
)))) |
104 | | oveq2 7358 |
. . . . . . . 8
β’ (π
= if(π β€ π
, π, π
) β (π +π π
) = (π +π if(π β€ π
, π, π
))) |
105 | 104 | breq2d 5116 |
. . . . . . 7
β’ (π
= if(π β€ π
, π, π
) β (if((π +π π) β€ π
, (π +π π), π
) β€ (π +π π
) β if((π +π π) β€ π
, (π +π π), π
) β€ (π +π if(π β€ π
, π, π
)))) |
106 | 103, 105 | ifboth 4524 |
. . . . . 6
β’
((if((π
+π π)
β€ π
, (π +π π), π
) β€ (π +π π) β§ if((π +π π) β€ π
, (π +π π), π
) β€ (π +π π
)) β if((π +π π) β€ π
, (π +π π), π
) β€ (π +π if(π β€ π
, π, π
))) |
107 | 87, 101, 106 | syl2anc 585 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β if((π
+π π)
β€ π
, (π +π π), π
) β€ (π +π if(π β€ π
, π, π
))) |
108 | 63, 58 | ifcld 4531 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β if(π β€ π
, π, π
) β
β*) |
109 | 58, 108 | xaddcld 13149 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (π
+π if(π
β€ π
, π, π
)) β
β*) |
110 | 58 | xaddid1d 13091 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (π
+π 0) = π
) |
111 | | elxrge0 13303 |
. . . . . . . . . . 11
β’ (π β (0[,]+β) β
(π β
β* β§ 0 β€ π)) |
112 | 111 | simprbi 498 |
. . . . . . . . . 10
β’ (π β (0[,]+β) β 0
β€ π) |
113 | 112 | ad2antll 728 |
. . . . . . . . 9
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β 0 β€ π) |
114 | 48 | adantr 482 |
. . . . . . . . 9
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β 0 β€ π
) |
115 | | breq2 5108 |
. . . . . . . . . 10
β’ (π = if(π β€ π
, π, π
) β (0 β€ π β 0 β€ if(π β€ π
, π, π
))) |
116 | | breq2 5108 |
. . . . . . . . . 10
β’ (π
= if(π β€ π
, π, π
) β (0 β€ π
β 0 β€ if(π β€ π
, π, π
))) |
117 | 115, 116 | ifboth 4524 |
. . . . . . . . 9
β’ ((0 β€
π β§ 0 β€ π
) β 0 β€ if(π β€ π
, π, π
)) |
118 | 113, 114,
117 | syl2anc 585 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β 0 β€ if(π β€
π
, π, π
)) |
119 | | xleadd2a 13102 |
. . . . . . . 8
β’ (((0
β β* β§ if(π β€ π
, π, π
) β β* β§ π
β β*)
β§ 0 β€ if(π β€
π
, π, π
)) β (π
+π 0) β€ (π
+π if(π β€ π
, π, π
))) |
120 | 94, 108, 58, 118, 119 | syl31anc 1374 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (π
+π 0) β€ (π
+π if(π β€ π
, π, π
))) |
121 | 110, 120 | eqbrtrrd 5128 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β π
β€ (π
+π if(π β€ π
, π, π
))) |
122 | 88, 58, 109, 91, 121 | xrletrd 13010 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β if((π
+π π)
β€ π
, (π +π π), π
) β€ (π
+π if(π β€ π
, π, π
))) |
123 | | oveq1 7357 |
. . . . . . 7
β’ (π = if(π β€ π
, π, π
) β (π +π if(π β€ π
, π, π
)) = (if(π β€ π
, π, π
) +π if(π β€ π
, π, π
))) |
124 | 123 | breq2d 5116 |
. . . . . 6
β’ (π = if(π β€ π
, π, π
) β (if((π +π π) β€ π
, (π +π π), π
) β€ (π +π if(π β€ π
, π, π
)) β if((π +π π) β€ π
, (π +π π), π
) β€ (if(π β€ π
, π, π
) +π if(π β€ π
, π, π
)))) |
125 | | oveq1 7357 |
. . . . . . 7
β’ (π
= if(π β€ π
, π, π
) β (π
+π if(π β€ π
, π, π
)) = (if(π β€ π
, π, π
) +π if(π β€ π
, π, π
))) |
126 | 125 | breq2d 5116 |
. . . . . 6
β’ (π
= if(π β€ π
, π, π
) β (if((π +π π) β€ π
, (π +π π), π
) β€ (π
+π if(π β€ π
, π, π
)) β if((π +π π) β€ π
, (π +π π), π
) β€ (if(π β€ π
, π, π
) +π if(π β€ π
, π, π
)))) |
127 | 124, 126 | ifboth 4524 |
. . . . 5
β’
((if((π
+π π)
β€ π
, (π +π π), π
) β€ (π +π if(π β€ π
, π, π
)) β§ if((π +π π) β€ π
, (π +π π), π
) β€ (π
+π if(π β€ π
, π, π
))) β if((π +π π) β€ π
, (π +π π), π
) β€ (if(π β€ π
, π, π
) +π if(π β€ π
, π, π
))) |
128 | 107, 122,
127 | syl2anc 585 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β if((π
+π π)
β€ π
, (π +π π), π
) β€ (if(π β€ π
, π, π
) +π if(π β€ π
, π, π
))) |
129 | | ge0xaddcl 13308 |
. . . . 5
β’ ((π β (0[,]+β) β§
π β (0[,]+β))
β (π
+π π)
β (0[,]+β)) |
130 | | ovex 7383 |
. . . . . 6
β’ (π +π π) β V |
131 | | ifexg 4534 |
. . . . . 6
β’ (((π +π π) β V β§ π
β β*)
β if((π
+π π)
β€ π
, (π +π π), π
) β V) |
132 | 130, 21, 131 | sylancr 588 |
. . . . 5
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β if((π +π π) β€ π
, (π +π π), π
) β V) |
133 | | breq1 5107 |
. . . . . . 7
β’ (π§ = (π +π π) β (π§ β€ π
β (π +π π) β€ π
)) |
134 | | id 22 |
. . . . . . 7
β’ (π§ = (π +π π) β π§ = (π +π π)) |
135 | 133, 134 | ifbieq1d 4509 |
. . . . . 6
β’ (π§ = (π +π π) β if(π§ β€ π
, π§, π
) = if((π +π π) β€ π
, (π +π π), π
)) |
136 | 135, 32 | fvmptg 6942 |
. . . . 5
β’ (((π +π π) β (0[,]+β) β§
if((π +π
π) β€ π
, (π +π π), π
) β V) β ((π§ β (0[,]+β) β¦ if(π§ β€ π
, π§, π
))β(π +π π)) = if((π +π π) β€ π
, (π +π π), π
)) |
137 | 129, 132,
136 | syl2anr 598 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β ((π§ β
(0[,]+β) β¦ if(π§
β€ π
, π§, π
))β(π +π π)) = if((π +π π) β€ π
, (π +π π), π
)) |
138 | 73, 82 | oveq12d 7368 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (((π§ β
(0[,]+β) β¦ if(π§
β€ π
, π§, π
))βπ) +π ((π§ β (0[,]+β) β¦ if(π§ β€ π
, π§, π
))βπ)) = (if(π β€ π
, π, π
) +π if(π β€ π
, π, π
))) |
139 | 128, 137,
138 | 3brtr4d 5136 |
. . 3
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β ((π§ β
(0[,]+β) β¦ if(π§
β€ π
, π§, π
))β(π +π π)) β€ (((π§ β (0[,]+β) β¦ if(π§ β€ π
, π§, π
))βπ) +π ((π§ β (0[,]+β) β¦ if(π§ β€ π
, π§, π
))βπ))) |
140 | 1, 24, 55, 84, 139 | comet 23791 |
. 2
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β ((π§ β (0[,]+β) β¦
if(π§ β€ π
, π§, π
)) β πΆ) β (βMetβπ)) |
141 | 19, 140 | eqeltrrd 2840 |
1
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β π· β (βMetβπ)) |