Step | Hyp | Ref
| Expression |
1 | | simp1 997 |
. . . . 5
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β πΆ β (βMetβπ)) |
2 | | xmetcl 13788 |
. . . . . . 7
β’ ((πΆ β (βMetβπ) β§ π₯ β π β§ π¦ β π) β (π₯πΆπ¦) β
β*) |
3 | | xmetge0 13801 |
. . . . . . 7
β’ ((πΆ β (βMetβπ) β§ π₯ β π β§ π¦ β π) β 0 β€ (π₯πΆπ¦)) |
4 | | elxrge0 9977 |
. . . . . . 7
β’ ((π₯πΆπ¦) β (0[,]+β) β ((π₯πΆπ¦) β β* β§ 0 β€
(π₯πΆπ¦))) |
5 | 2, 3, 4 | sylanbrc 417 |
. . . . . 6
β’ ((πΆ β (βMetβπ) β§ π₯ β π β§ π¦ β π) β (π₯πΆπ¦) β (0[,]+β)) |
6 | 5 | 3expb 1204 |
. . . . 5
β’ ((πΆ β (βMetβπ) β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β (0[,]+β)) |
7 | 1, 6 | sylan 283 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β (0[,]+β)) |
8 | | xmetf 13786 |
. . . . . . 7
β’ (πΆ β (βMetβπ) β πΆ:(π Γ π)βΆβ*) |
9 | 8 | 3ad2ant1 1018 |
. . . . . 6
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β πΆ:(π Γ π)βΆβ*) |
10 | 9 | ffnd 5366 |
. . . . 5
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β πΆ Fn (π Γ π)) |
11 | | fnovim 5982 |
. . . . 5
β’ (πΆ Fn (π Γ π) β πΆ = (π₯ β π, π¦ β π β¦ (π₯πΆπ¦))) |
12 | 10, 11 | syl 14 |
. . . 4
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β πΆ = (π₯ β π, π¦ β π β¦ (π₯πΆπ¦))) |
13 | | eqidd 2178 |
. . . 4
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β (π§ β (0[,]+β) β¦
inf({π§, π
}, β*, < )) = (π§ β (0[,]+β) β¦
inf({π§, π
}, β*, <
))) |
14 | | preq1 3669 |
. . . . 5
β’ (π§ = (π₯πΆπ¦) β {π§, π
} = {(π₯πΆπ¦), π
}) |
15 | 14 | infeq1d 7010 |
. . . 4
β’ (π§ = (π₯πΆπ¦) β inf({π§, π
}, β*, < ) = inf({(π₯πΆπ¦), π
}, β*, <
)) |
16 | 7, 12, 13, 15 | fmpoco 6216 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β ((π§ β (0[,]+β) β¦
inf({π§, π
}, β*, < )) β
πΆ) = (π₯ β π, π¦ β π β¦ inf({(π₯πΆπ¦), π
}, β*, <
))) |
17 | | stdbdmet.1 |
. . 3
β’ π· = (π₯ β π, π¦ β π β¦ inf({(π₯πΆπ¦), π
}, β*, <
)) |
18 | 16, 17 | eqtr4di 2228 |
. 2
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β ((π§ β (0[,]+β) β¦
inf({π§, π
}, β*, < )) β
πΆ) = π·) |
19 | | elxrge0 9977 |
. . . . . 6
β’ (π§ β (0[,]+β) β
(π§ β
β* β§ 0 β€ π§)) |
20 | 19 | simplbi 274 |
. . . . 5
β’ (π§ β (0[,]+β) β
π§ β
β*) |
21 | | simp2 998 |
. . . . 5
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β π
β
β*) |
22 | | xrmincl 11273 |
. . . . 5
β’ ((π§ β β*
β§ π
β
β*) β inf({π§, π
}, β*, < ) β
β*) |
23 | 20, 21, 22 | syl2anr 290 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π§ β (0[,]+β)) β inf({π§, π
}, β*, < ) β
β*) |
24 | 23 | fmpttd 5671 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β (π§ β (0[,]+β) β¦
inf({π§, π
}, β*, <
)):(0[,]+β)βΆβ*) |
25 | | eqid 2177 |
. . . . . 6
β’ (π§ β (0[,]+β) β¦
inf({π§, π
}, β*, < )) = (π§ β (0[,]+β) β¦
inf({π§, π
}, β*, <
)) |
26 | | preq1 3669 |
. . . . . . 7
β’ (π§ = π β {π§, π
} = {π, π
}) |
27 | 26 | infeq1d 7010 |
. . . . . 6
β’ (π§ = π β inf({π§, π
}, β*, < ) = inf({π, π
}, β*, <
)) |
28 | | simpr 110 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β π β
(0[,]+β)) |
29 | | elxrge0 9977 |
. . . . . . . 8
β’ (π β (0[,]+β) β
(π β
β* β§ 0 β€ π)) |
30 | 29 | simplbi 274 |
. . . . . . 7
β’ (π β (0[,]+β) β
π β
β*) |
31 | | xrmincl 11273 |
. . . . . . 7
β’ ((π β β*
β§ π
β
β*) β inf({π, π
}, β*, < ) β
β*) |
32 | 30, 21, 31 | syl2anr 290 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β inf({π, π
}, β*, < ) β
β*) |
33 | 25, 27, 28, 32 | fvmptd3 5609 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β ((π§ β (0[,]+β) β¦
inf({π§, π
}, β*, < ))βπ) = inf({π, π
}, β*, <
)) |
34 | 33 | eqeq1d 2186 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (((π§ β (0[,]+β) β¦
inf({π§, π
}, β*, < ))βπ) = 0 β inf({π, π
}, β*, < ) =
0)) |
35 | | 0xr 8003 |
. . . . . . . . 9
β’ 0 β
β* |
36 | 35 | a1i 9 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β 0 β
β*) |
37 | 30 | adantl 277 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β π β
β*) |
38 | 21 | adantr 276 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β π
β
β*) |
39 | | xrltmininf 11277 |
. . . . . . . 8
β’ ((0
β β* β§ π β β* β§ π
β β*)
β (0 < inf({π,
π
}, β*,
< ) β (0 < π
β§ 0 < π
))) |
40 | 36, 37, 38, 39 | syl3anc 1238 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (0 <
inf({π, π
}, β*, < ) β (0
< π β§ 0 < π
))) |
41 | | simp3 999 |
. . . . . . . . 9
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β 0 < π
) |
42 | 41 | adantr 276 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β 0 < π
) |
43 | 42 | biantrud 304 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (0 < π β (0 < π β§ 0 < π
))) |
44 | 40, 43 | bitr4d 191 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (0 <
inf({π, π
}, β*, < ) β 0 <
π)) |
45 | 44 | notbid 667 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (Β¬ 0 <
inf({π, π
}, β*, < ) β Β¬
0 < π)) |
46 | 28, 29 | sylib 122 |
. . . . . . . . . 10
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (π β β*
β§ 0 β€ π)) |
47 | 46 | simprd 114 |
. . . . . . . . 9
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β 0 β€ π) |
48 | | xrltle 9797 |
. . . . . . . . . . . 12
β’ ((0
β β* β§ π
β β*) β (0 <
π
β 0 β€ π
)) |
49 | 35, 21, 48 | sylancr 414 |
. . . . . . . . . . 11
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β (0 < π
β 0 β€ π
)) |
50 | 41, 49 | mpd 13 |
. . . . . . . . . 10
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β 0 β€ π
) |
51 | 50 | adantr 276 |
. . . . . . . . 9
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β 0 β€ π
) |
52 | | xrlemininf 11278 |
. . . . . . . . . 10
β’ ((0
β β* β§ π β β* β§ π
β β*)
β (0 β€ inf({π,
π
}, β*,
< ) β (0 β€ π
β§ 0 β€ π
))) |
53 | 36, 37, 38, 52 | syl3anc 1238 |
. . . . . . . . 9
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (0 β€
inf({π, π
}, β*, < ) β (0
β€ π β§ 0 β€ π
))) |
54 | 47, 51, 53 | mpbir2and 944 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β 0 β€
inf({π, π
}, β*, <
)) |
55 | | xrlenlt 8021 |
. . . . . . . . 9
β’ ((0
β β* β§ inf({π, π
}, β*, < ) β
β*) β (0 β€ inf({π, π
}, β*, < ) β Β¬
inf({π, π
}, β*, < ) <
0)) |
56 | 35, 32, 55 | sylancr 414 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (0 β€
inf({π, π
}, β*, < ) β Β¬
inf({π, π
}, β*, < ) <
0)) |
57 | 54, 56 | mpbid 147 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β Β¬
inf({π, π
}, β*, < ) <
0) |
58 | 57 | biantrurd 305 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (Β¬ 0 <
inf({π, π
}, β*, < ) β (Β¬
inf({π, π
}, β*, < ) < 0 β§
Β¬ 0 < inf({π, π
}, β*, <
)))) |
59 | | xrlttri3 9796 |
. . . . . . 7
β’
((inf({π, π
}, β*, < )
β β* β§ 0 β β*) β
(inf({π, π
}, β*, < ) = 0 β
(Β¬ inf({π, π
}, β*, < )
< 0 β§ Β¬ 0 < inf({π, π
}, β*, <
)))) |
60 | 32, 36, 59 | syl2anc 411 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (inf({π, π
}, β*, < ) = 0 β
(Β¬ inf({π, π
}, β*, < )
< 0 β§ Β¬ 0 < inf({π, π
}, β*, <
)))) |
61 | 58, 60 | bitr4d 191 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (Β¬ 0 <
inf({π, π
}, β*, < ) β
inf({π, π
}, β*, < ) =
0)) |
62 | | xrlenlt 8021 |
. . . . . . . . 9
β’ ((0
β β* β§ π β β*) β (0 β€
π β Β¬ π < 0)) |
63 | 35, 37, 62 | sylancr 414 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (0 β€ π β Β¬ π < 0)) |
64 | 47, 63 | mpbid 147 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β Β¬ π < 0) |
65 | 64 | biantrurd 305 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (Β¬ 0 <
π β (Β¬ π < 0 β§ Β¬ 0 < π))) |
66 | | xrlttri3 9796 |
. . . . . . 7
β’ ((π β β*
β§ 0 β β*) β (π = 0 β (Β¬ π < 0 β§ Β¬ 0 < π))) |
67 | 37, 36, 66 | syl2anc 411 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (π = 0 β (Β¬ π < 0 β§ Β¬ 0 < π))) |
68 | 65, 67 | bitr4d 191 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (Β¬ 0 <
π β π = 0)) |
69 | 45, 61, 68 | 3bitr3d 218 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (inf({π, π
}, β*, < ) = 0 β
π = 0)) |
70 | 34, 69 | bitrd 188 |
. . 3
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ π β (0[,]+β)) β (((π§ β (0[,]+β) β¦
inf({π§, π
}, β*, < ))βπ) = 0 β π = 0)) |
71 | 30 | ad2antrl 490 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β π β
β*) |
72 | 21 | adantr 276 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β π
β
β*) |
73 | | xrmin1inf 11274 |
. . . . . . . 8
β’ ((π β β*
β§ π
β
β*) β inf({π, π
}, β*, < ) β€ π) |
74 | 71, 72, 73 | syl2anc 411 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β inf({π, π
}, β*, < )
β€ π) |
75 | 71, 72, 31 | syl2anc 411 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β inf({π, π
}, β*, < )
β β*) |
76 | | elxrge0 9977 |
. . . . . . . . . 10
β’ (π β (0[,]+β) β
(π β
β* β§ 0 β€ π)) |
77 | 76 | simplbi 274 |
. . . . . . . . 9
β’ (π β (0[,]+β) β
π β
β*) |
78 | 77 | ad2antll 491 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β π β
β*) |
79 | | xrletr 9807 |
. . . . . . . 8
β’
((inf({π, π
}, β*, < )
β β* β§ π β β* β§ π β β*)
β ((inf({π, π
}, β*, < )
β€ π β§ π β€ π) β inf({π, π
}, β*, < ) β€ π)) |
80 | 75, 71, 78, 79 | syl3anc 1238 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β ((inf({π, π
}, β*, < )
β€ π β§ π β€ π) β inf({π, π
}, β*, < ) β€ π)) |
81 | 74, 80 | mpand 429 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (π β€ π β inf({π, π
}, β*, < ) β€ π)) |
82 | | xrmin2inf 11275 |
. . . . . . 7
β’ ((π β β*
β§ π
β
β*) β inf({π, π
}, β*, < ) β€ π
) |
83 | 71, 72, 82 | syl2anc 411 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β inf({π, π
}, β*, < )
β€ π
) |
84 | 81, 83 | jctird 317 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (π β€ π β (inf({π, π
}, β*, < ) β€ π β§ inf({π, π
}, β*, < ) β€ π
))) |
85 | | xrlemininf 11278 |
. . . . . 6
β’
((inf({π, π
}, β*, < )
β β* β§ π β β* β§ π
β β*)
β (inf({π, π
}, β*, < )
β€ inf({π, π
}, β*, < )
β (inf({π, π
}, β*, < )
β€ π β§ inf({π, π
}, β*, < ) β€ π
))) |
86 | 75, 78, 72, 85 | syl3anc 1238 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (inf({π, π
}, β*, < )
β€ inf({π, π
}, β*, < )
β (inf({π, π
}, β*, < )
β€ π β§ inf({π, π
}, β*, < ) β€ π
))) |
87 | 84, 86 | sylibrd 169 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (π β€ π β inf({π, π
}, β*, < ) β€
inf({π, π
}, β*, <
))) |
88 | 33 | adantrr 479 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β ((π§ β
(0[,]+β) β¦ inf({π§, π
}, β*, < ))βπ) = inf({π, π
}, β*, <
)) |
89 | | preq1 3669 |
. . . . . . 7
β’ (π§ = π β {π§, π
} = {π, π
}) |
90 | 89 | infeq1d 7010 |
. . . . . 6
β’ (π§ = π β inf({π§, π
}, β*, < ) = inf({π, π
}, β*, <
)) |
91 | | simpr 110 |
. . . . . . 7
β’ ((π β (0[,]+β) β§
π β (0[,]+β))
β π β
(0[,]+β)) |
92 | 91 | adantl 277 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β π β
(0[,]+β)) |
93 | | xrmincl 11273 |
. . . . . . 7
β’ ((π β β*
β§ π
β
β*) β inf({π, π
}, β*, < ) β
β*) |
94 | 78, 72, 93 | syl2anc 411 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β inf({π, π
}, β*, < )
β β*) |
95 | 25, 90, 92, 94 | fvmptd3 5609 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β ((π§ β
(0[,]+β) β¦ inf({π§, π
}, β*, < ))βπ) = inf({π, π
}, β*, <
)) |
96 | 88, 95 | breq12d 4016 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (((π§ β
(0[,]+β) β¦ inf({π§, π
}, β*, < ))βπ) β€ ((π§ β (0[,]+β) β¦ inf({π§, π
}, β*, < ))βπ) β inf({π, π
}, β*, < ) β€
inf({π, π
}, β*, <
))) |
97 | 87, 96 | sylibrd 169 |
. . 3
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (π β€ π β ((π§ β (0[,]+β) β¦ inf({π§, π
}, β*, < ))βπ) β€ ((π§ β (0[,]+β) β¦ inf({π§, π
}, β*, < ))βπ))) |
98 | 29 | simprbi 275 |
. . . . . 6
β’ (π β (0[,]+β) β 0
β€ π) |
99 | 98 | ad2antrl 490 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β 0 β€ π) |
100 | 76 | simprbi 275 |
. . . . . 6
β’ (π β (0[,]+β) β 0
β€ π) |
101 | 100 | ad2antll 491 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β 0 β€ π) |
102 | 41 | adantr 276 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β 0 < π
) |
103 | | xrbdtri 11283 |
. . . . 5
β’ (((π β β*
β§ 0 β€ π) β§
(π β
β* β§ 0 β€ π) β§ (π
β β* β§ 0 <
π
)) β inf({(π +π π), π
}, β*, < ) β€
(inf({π, π
}, β*, < )
+π inf({π, π
}, β*, <
))) |
104 | 71, 99, 78, 101, 72, 102, 103 | syl222anc 1254 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β inf({(π
+π π),
π
}, β*,
< ) β€ (inf({π, π
}, β*, < )
+π inf({π, π
}, β*, <
))) |
105 | | preq1 3669 |
. . . . . 6
β’ (π§ = (π +π π) β {π§, π
} = {(π +π π), π
}) |
106 | 105 | infeq1d 7010 |
. . . . 5
β’ (π§ = (π +π π) β inf({π§, π
}, β*, < ) = inf({(π +π π), π
}, β*, <
)) |
107 | | ge0xaddcl 9982 |
. . . . . 6
β’ ((π β (0[,]+β) β§
π β (0[,]+β))
β (π
+π π)
β (0[,]+β)) |
108 | 107 | adantl 277 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (π
+π π)
β (0[,]+β)) |
109 | 71, 78 | xaddcld 9883 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (π
+π π)
β β*) |
110 | | xrmincl 11273 |
. . . . . 6
β’ (((π +π π) β β*
β§ π
β
β*) β inf({(π +π π), π
}, β*, < ) β
β*) |
111 | 109, 72, 110 | syl2anc 411 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β inf({(π
+π π),
π
}, β*,
< ) β β*) |
112 | 25, 106, 108, 111 | fvmptd3 5609 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β ((π§ β
(0[,]+β) β¦ inf({π§, π
}, β*, < ))β(π +π π)) = inf({(π +π π), π
}, β*, <
)) |
113 | 88, 95 | oveq12d 5892 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β (((π§ β
(0[,]+β) β¦ inf({π§, π
}, β*, < ))βπ) +π ((π§ β (0[,]+β) β¦
inf({π§, π
}, β*, < ))βπ)) = (inf({π, π
}, β*, < )
+π inf({π, π
}, β*, <
))) |
114 | 104, 112,
113 | 3brtr4d 4035 |
. . 3
β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β (0[,]+β) β§
π β (0[,]+β)))
β ((π§ β
(0[,]+β) β¦ inf({π§, π
}, β*, < ))β(π +π π)) β€ (((π§ β (0[,]+β) β¦ inf({π§, π
}, β*, < ))βπ) +π ((π§ β (0[,]+β) β¦
inf({π§, π
}, β*, < ))βπ))) |
115 | 1, 24, 70, 97, 114 | comet 13935 |
. 2
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β ((π§ β (0[,]+β) β¦
inf({π§, π
}, β*, < )) β
πΆ) β
(βMetβπ)) |
116 | 18, 115 | eqeltrrd 2255 |
1
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β π· β (βMetβπ)) |