Description: The sum of two positive reals is greater than one of them. Proposition 9-3.5(iii) of Gleason p. 123. (Contributed by NM, 26-Mar-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | ltaddpr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prn0 | |
|
2 | n0 | |
|
3 | 1 2 | sylib | |
4 | 3 | adantl | |
5 | addclpr | |
|
6 | df-plp | |
|
7 | addclnq | |
|
8 | 6 7 | genpprecl | |
9 | 8 | imp | |
10 | elprnq | |
|
11 | addnqf | |
|
12 | 11 | fdmi | |
13 | 0nnq | |
|
14 | 12 13 | ndmovrcl | |
15 | ltaddnq | |
|
16 | 10 14 15 | 3syl | |
17 | prcdnq | |
|
18 | 16 17 | mpd | |
19 | 5 9 18 | syl2an2r | |
20 | 19 | exp32 | |
21 | 20 | com23 | |
22 | 21 | alrimdv | |
23 | dfss2 | |
|
24 | 22 23 | syl6ibr | |
25 | vex | |
|
26 | 25 | prlem934 | |
27 | 26 | adantr | |
28 | eleq2 | |
|
29 | 28 | biimprcd | |
30 | 29 | con3d | |
31 | 8 30 | syl6 | |
32 | 31 | expd | |
33 | 32 | com34 | |
34 | 33 | rexlimdv | |
35 | 27 34 | mpd | |
36 | 24 35 | jcad | |
37 | dfpss2 | |
|
38 | 36 37 | syl6ibr | |
39 | 38 | exlimdv | |
40 | 4 39 | mpd | |
41 | ltprord | |
|
42 | 5 41 | syldan | |
43 | 40 42 | mpbird | |