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 e. P. /\ B e. P. ) -> A

Proof

Step Hyp Ref Expression
1 prn0 
 |-  ( B e. P. -> B =/= (/) )
2 n0 
 |-  ( B =/= (/) <-> E. y y e. B )
3 1 2 sylib 
 |-  ( B e. P. -> E. y y e. B )
4 3 adantl 
 |-  ( ( A e. P. /\ B e. P. ) -> E. y y e. B )
5 addclpr 
 |-  ( ( A e. P. /\ B e. P. ) -> ( A +P. B ) e. P. )
6 df-plp 
 |-  +P. = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y +Q z ) } )
7 addclnq 
 |-  ( ( y e. Q. /\ z e. Q. ) -> ( y +Q z ) e. Q. )
8 6 7 genpprecl 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( x e. A /\ y e. B ) -> ( x +Q y ) e. ( A +P. B ) ) )
9 8 imp 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( x e. A /\ y e. B ) ) -> ( x +Q y ) e. ( A +P. B ) )
10 elprnq 
 |-  ( ( ( A +P. B ) e. P. /\ ( x +Q y ) e. ( A +P. B ) ) -> ( x +Q y ) e. Q. )
11 addnqf 
 |-  +Q : ( Q. X. Q. ) --> Q.
12 11 fdmi 
 |-  dom +Q = ( Q. X. Q. )
13 0nnq 
 |-  -. (/) e. Q.
14 12 13 ndmovrcl 
 |-  ( ( x +Q y ) e. Q. -> ( x e. Q. /\ y e. Q. ) )
15 ltaddnq 
 |-  ( ( x e. Q. /\ y e. Q. ) -> x
16 10 14 15 3syl 
 |-  ( ( ( A +P. B ) e. P. /\ ( x +Q y ) e. ( A +P. B ) ) -> x
17 prcdnq 
 |-  ( ( ( A +P. B ) e. P. /\ ( x +Q y ) e. ( A +P. B ) ) -> ( x  x e. ( A +P. B ) ) )
18 16 17 mpd 
 |-  ( ( ( A +P. B ) e. P. /\ ( x +Q y ) e. ( A +P. B ) ) -> x e. ( A +P. B ) )
19 5 9 18 syl2an2r 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( x e. A /\ y e. B ) ) -> x e. ( A +P. B ) )
20 19 exp32 
 |-  ( ( A e. P. /\ B e. P. ) -> ( x e. A -> ( y e. B -> x e. ( A +P. B ) ) ) )
21 20 com23 
 |-  ( ( A e. P. /\ B e. P. ) -> ( y e. B -> ( x e. A -> x e. ( A +P. B ) ) ) )
22 21 alrimdv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( y e. B -> A. x ( x e. A -> x e. ( A +P. B ) ) ) )
23 dfss2 
 |-  ( A C_ ( A +P. B ) <-> A. x ( x e. A -> x e. ( A +P. B ) ) )
24 22 23 syl6ibr 
 |-  ( ( A e. P. /\ B e. P. ) -> ( y e. B -> A C_ ( A +P. B ) ) )
25 vex 
 |-  y e. _V
26 25 prlem934 
 |-  ( A e. P. -> E. x e. A -. ( x +Q y ) e. A )
27 26 adantr 
 |-  ( ( A e. P. /\ B e. P. ) -> E. x e. A -. ( x +Q y ) e. A )
28 eleq2 
 |-  ( A = ( A +P. B ) -> ( ( x +Q y ) e. A <-> ( x +Q y ) e. ( A +P. B ) ) )
29 28 biimprcd 
 |-  ( ( x +Q y ) e. ( A +P. B ) -> ( A = ( A +P. B ) -> ( x +Q y ) e. A ) )
30 29 con3d 
 |-  ( ( x +Q y ) e. ( A +P. B ) -> ( -. ( x +Q y ) e. A -> -. A = ( A +P. B ) ) )
31 8 30 syl6 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( x e. A /\ y e. B ) -> ( -. ( x +Q y ) e. A -> -. A = ( A +P. B ) ) ) )
32 31 expd 
 |-  ( ( A e. P. /\ B e. P. ) -> ( x e. A -> ( y e. B -> ( -. ( x +Q y ) e. A -> -. A = ( A +P. B ) ) ) ) )
33 32 com34 
 |-  ( ( A e. P. /\ B e. P. ) -> ( x e. A -> ( -. ( x +Q y ) e. A -> ( y e. B -> -. A = ( A +P. B ) ) ) ) )
34 33 rexlimdv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( E. x e. A -. ( x +Q y ) e. A -> ( y e. B -> -. A = ( A +P. B ) ) ) )
35 27 34 mpd 
 |-  ( ( A e. P. /\ B e. P. ) -> ( y e. B -> -. A = ( A +P. B ) ) )
36 24 35 jcad 
 |-  ( ( A e. P. /\ B e. P. ) -> ( y e. B -> ( A C_ ( A +P. B ) /\ -. A = ( A +P. B ) ) ) )
37 dfpss2 
 |-  ( A C. ( A +P. B ) <-> ( A C_ ( A +P. B ) /\ -. A = ( A +P. B ) ) )
38 36 37 syl6ibr 
 |-  ( ( A e. P. /\ B e. P. ) -> ( y e. B -> A C. ( A +P. B ) ) )
39 38 exlimdv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( E. y y e. B -> A C. ( A +P. B ) ) )
40 4 39 mpd 
 |-  ( ( A e. P. /\ B e. P. ) -> A C. ( A +P. B ) )
41 ltprord 
 |-  ( ( A e. P. /\ ( A +P. B ) e. P. ) -> ( A 
 A C. ( A +P. B ) ) )
42 5 41 syldan 
 |-  ( ( A e. P. /\ B e. P. ) -> ( A 
 A C. ( A +P. B ) ) )
43 40 42 mpbird 
 |-  ( ( A e. P. /\ B e. P. ) -> A