Metamath Proof Explorer


Theorem ltaddpr

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 A𝑷B𝑷A<𝑷A+𝑷B

Proof

Step Hyp Ref Expression
1 prn0 B𝑷B
2 n0 ByyB
3 1 2 sylib B𝑷yyB
4 3 adantl A𝑷B𝑷yyB
5 addclpr A𝑷B𝑷A+𝑷B𝑷
6 df-plp +𝑷=w𝑷,v𝑷x|ywzvx=y+𝑸z
7 addclnq y𝑸z𝑸y+𝑸z𝑸
8 6 7 genpprecl A𝑷B𝑷xAyBx+𝑸yA+𝑷B
9 8 imp A𝑷B𝑷xAyBx+𝑸yA+𝑷B
10 elprnq A+𝑷B𝑷x+𝑸yA+𝑷Bx+𝑸y𝑸
11 addnqf +𝑸:𝑸×𝑸𝑸
12 11 fdmi dom+𝑸=𝑸×𝑸
13 0nnq ¬𝑸
14 12 13 ndmovrcl x+𝑸y𝑸x𝑸y𝑸
15 ltaddnq x𝑸y𝑸x<𝑸x+𝑸y
16 10 14 15 3syl A+𝑷B𝑷x+𝑸yA+𝑷Bx<𝑸x+𝑸y
17 prcdnq A+𝑷B𝑷x+𝑸yA+𝑷Bx<𝑸x+𝑸yxA+𝑷B
18 16 17 mpd A+𝑷B𝑷x+𝑸yA+𝑷BxA+𝑷B
19 5 9 18 syl2an2r A𝑷B𝑷xAyBxA+𝑷B
20 19 exp32 A𝑷B𝑷xAyBxA+𝑷B
21 20 com23 A𝑷B𝑷yBxAxA+𝑷B
22 21 alrimdv A𝑷B𝑷yBxxAxA+𝑷B
23 dfss2 AA+𝑷BxxAxA+𝑷B
24 22 23 syl6ibr A𝑷B𝑷yBAA+𝑷B
25 vex yV
26 25 prlem934 A𝑷xA¬x+𝑸yA
27 26 adantr A𝑷B𝑷xA¬x+𝑸yA
28 eleq2 A=A+𝑷Bx+𝑸yAx+𝑸yA+𝑷B
29 28 biimprcd x+𝑸yA+𝑷BA=A+𝑷Bx+𝑸yA
30 29 con3d x+𝑸yA+𝑷B¬x+𝑸yA¬A=A+𝑷B
31 8 30 syl6 A𝑷B𝑷xAyB¬x+𝑸yA¬A=A+𝑷B
32 31 expd A𝑷B𝑷xAyB¬x+𝑸yA¬A=A+𝑷B
33 32 com34 A𝑷B𝑷xA¬x+𝑸yAyB¬A=A+𝑷B
34 33 rexlimdv A𝑷B𝑷xA¬x+𝑸yAyB¬A=A+𝑷B
35 27 34 mpd A𝑷B𝑷yB¬A=A+𝑷B
36 24 35 jcad A𝑷B𝑷yBAA+𝑷B¬A=A+𝑷B
37 dfpss2 AA+𝑷BAA+𝑷B¬A=A+𝑷B
38 36 37 syl6ibr A𝑷B𝑷yBAA+𝑷B
39 38 exlimdv A𝑷B𝑷yyBAA+𝑷B
40 4 39 mpd A𝑷B𝑷AA+𝑷B
41 ltprord A𝑷A+𝑷B𝑷A<𝑷A+𝑷BAA+𝑷B
42 5 41 syldan A𝑷B𝑷A<𝑷A+𝑷BAA+𝑷B
43 40 42 mpbird A𝑷B𝑷A<𝑷A+𝑷B