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	syl5ib	|- ( 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