Description: Extract the upper bound of an interval. (Contributed by Mario Carneiro, 17-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ixx.1 | |
|
ixxub.2 | |
||
ixxub.3 | |
||
ixxub.4 | |
||
ixxub.5 | |
||
Assertion | ixxub | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ixx.1 | |
|
2 | ixxub.2 | |
|
3 | ixxub.3 | |
|
4 | ixxub.4 | |
|
5 | ixxub.5 | |
|
6 | 1 | elixx1 | |
7 | 6 | 3adant3 | |
8 | 7 | biimpa | |
9 | 8 | simp1d | |
10 | 9 | ex | |
11 | 10 | ssrdv | |
12 | supxrcl | |
|
13 | 11 12 | syl | |
14 | simp2 | |
|
15 | 8 | simp3d | |
16 | 14 | adantr | |
17 | 9 16 3 | syl2anc | |
18 | 15 17 | mpd | |
19 | 18 | ralrimiva | |
20 | supxrleub | |
|
21 | 11 14 20 | syl2anc | |
22 | 19 21 | mpbird | |
23 | simprl | |
|
24 | 11 | ad2antrr | |
25 | qre | |
|
26 | 25 | rexrd | |
27 | 26 | ad2antlr | |
28 | simp1 | |
|
29 | 28 | ad2antrr | |
30 | 13 | ad2antrr | |
31 | simp3 | |
|
32 | n0 | |
|
33 | 31 32 | sylib | |
34 | 28 | adantr | |
35 | 13 | adantr | |
36 | 8 | simp2d | |
37 | 34 9 5 | syl2anc | |
38 | 36 37 | mpd | |
39 | supxrub | |
|
40 | 11 39 | sylan | |
41 | 34 9 35 38 40 | xrletrd | |
42 | 33 41 | exlimddv | |
43 | 42 | ad2antrr | |
44 | 29 30 27 43 23 | xrlelttrd | |
45 | 29 27 4 | syl2anc | |
46 | 44 45 | mpd | |
47 | simprr | |
|
48 | 14 | ad2antrr | |
49 | 27 48 2 | syl2anc | |
50 | 47 49 | mpd | |
51 | 7 | ad2antrr | |
52 | 27 46 50 51 | mpbir3and | |
53 | 24 52 39 | syl2anc | |
54 | 27 30 | xrlenltd | |
55 | 53 54 | mpbid | |
56 | 23 55 | pm2.65da | |
57 | 56 | nrexdv | |
58 | qbtwnxr | |
|
59 | 58 | 3expia | |
60 | 13 14 59 | syl2anc | |
61 | 57 60 | mtod | |
62 | 14 13 61 | xrnltled | |
63 | 13 14 22 62 | xrletrid | |