This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ltaddnq

Description: The sum of two fractions is greater than one of them. (Contributed by NM, 14-Mar-1996) (Revised by Mario Carneiro, 10-May-2013) (New usage is discouraged.)

Ref Expression
Assertion ltaddnq 
|- ( ( A e. Q. /\ B e. Q. ) -> A

Proof

Step Hyp Ref Expression
1 id 
 |-  ( x = A -> x = A )
2 oveq1 
 |-  ( x = A -> ( x +Q y ) = ( A +Q y ) )
3 1 2 breq12d 
 |-  ( x = A -> ( x  A
4 oveq2 
 |-  ( y = B -> ( A +Q y ) = ( A +Q B ) )
5 4 breq2d 
 |-  ( y = B -> ( A  A
6 1lt2nq 
 |-  1Q
7 ltmnq 
 |-  ( y e. Q. -> ( 1Q  ( y .Q 1Q )
8 6 7 mpbii 
 |-  ( y e. Q. -> ( y .Q 1Q )
9 mulidnq 
 |-  ( y e. Q. -> ( y .Q 1Q ) = y )
10 distrnq 
 |-  ( y .Q ( 1Q +Q 1Q ) ) = ( ( y .Q 1Q ) +Q ( y .Q 1Q ) )
11 9 9 oveq12d 
 |-  ( y e. Q. -> ( ( y .Q 1Q ) +Q ( y .Q 1Q ) ) = ( y +Q y ) )
12 10 11 eqtrid 
 |-  ( y e. Q. -> ( y .Q ( 1Q +Q 1Q ) ) = ( y +Q y ) )
13 8 9 12 3brtr3d 
 |-  ( y e. Q. -> y
14 ltanq 
 |-  ( x e. Q. -> ( y  ( x +Q y )
15 13 14 imbitrid 
 |-  ( x e. Q. -> ( y e. Q. -> ( x +Q y )
16 15 imp 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( x +Q y )
17 addcomnq 
 |-  ( x +Q y ) = ( y +Q x )
18 vex 
 |-  x e. _V
19 vex 
 |-  y e. _V
20 addcomnq 
 |-  ( r +Q s ) = ( s +Q r )
21 addassnq 
 |-  ( ( r +Q s ) +Q t ) = ( r +Q ( s +Q t ) )
22 18 19 19 20 21 caov12 
 |-  ( x +Q ( y +Q y ) ) = ( y +Q ( x +Q y ) )
23 16 17 22 3brtr3g 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( y +Q x )
24 ltanq 
 |-  ( y e. Q. -> ( x  ( y +Q x )
25 24 adantl 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( x  ( y +Q x )
26 23 25 mpbird 
 |-  ( ( x e. Q. /\ y e. Q. ) -> x
27 3 5 26 vtocl2ga 
 |-  ( ( A e. Q. /\ B e. Q. ) -> A