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	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → 𝐴 <Q ( 𝐴 +Q 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
2		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 +Q 𝑦 ) = ( 𝐴 +Q 𝑦 ) )
3	1 2	breq12d	⊢ ( 𝑥 = 𝐴 → ( 𝑥 <Q ( 𝑥 +Q 𝑦 ) ↔ 𝐴 <Q ( 𝐴 +Q 𝑦 ) ) )
4		oveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 +Q 𝑦 ) = ( 𝐴 +Q 𝐵 ) )
5	4	breq2d	⊢ ( 𝑦 = 𝐵 → ( 𝐴 <Q ( 𝐴 +Q 𝑦 ) ↔ 𝐴 <Q ( 𝐴 +Q 𝐵 ) ) )
6		1lt2nq	⊢ 1Q <Q ( 1Q +Q 1Q )
7		ltmnq	⊢ ( 𝑦 ∈ Q → ( 1Q <Q ( 1Q +Q 1Q ) ↔ ( 𝑦 ·Q 1Q ) <Q ( 𝑦 ·Q ( 1Q +Q 1Q ) ) ) )
8	6 7	mpbii	⊢ ( 𝑦 ∈ Q → ( 𝑦 ·Q 1Q ) <Q ( 𝑦 ·Q ( 1Q +Q 1Q ) ) )
9		mulidnq	⊢ ( 𝑦 ∈ Q → ( 𝑦 ·Q 1Q ) = 𝑦 )
10		distrnq	⊢ ( 𝑦 ·Q ( 1Q +Q 1Q ) ) = ( ( 𝑦 ·Q 1Q ) +Q ( 𝑦 ·Q 1Q ) )
11	9 9	oveq12d	⊢ ( 𝑦 ∈ Q → ( ( 𝑦 ·Q 1Q ) +Q ( 𝑦 ·Q 1Q ) ) = ( 𝑦 +Q 𝑦 ) )
12	10 11	eqtrid	⊢ ( 𝑦 ∈ Q → ( 𝑦 ·Q ( 1Q +Q 1Q ) ) = ( 𝑦 +Q 𝑦 ) )
13	8 9 12	3brtr3d	⊢ ( 𝑦 ∈ Q → 𝑦 <Q ( 𝑦 +Q 𝑦 ) )
14		ltanq	⊢ ( 𝑥 ∈ Q → ( 𝑦 <Q ( 𝑦 +Q 𝑦 ) ↔ ( 𝑥 +Q 𝑦 ) <Q ( 𝑥 +Q ( 𝑦 +Q 𝑦 ) ) ) )
15	13 14	imbitrid	⊢ ( 𝑥 ∈ Q → ( 𝑦 ∈ Q → ( 𝑥 +Q 𝑦 ) <Q ( 𝑥 +Q ( 𝑦 +Q 𝑦 ) ) ) )
16	15	imp	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑥 +Q 𝑦 ) <Q ( 𝑥 +Q ( 𝑦 +Q 𝑦 ) ) )
17		addcomnq	⊢ ( 𝑥 +Q 𝑦 ) = ( 𝑦 +Q 𝑥 )
18		vex	⊢ 𝑥 ∈ V
19		vex	⊢ 𝑦 ∈ V
20		addcomnq	⊢ ( 𝑟 +Q 𝑠 ) = ( 𝑠 +Q 𝑟 )
21		addassnq	⊢ ( ( 𝑟 +Q 𝑠 ) +Q 𝑡 ) = ( 𝑟 +Q ( 𝑠 +Q 𝑡 ) )
22	18 19 19 20 21	caov12	⊢ ( 𝑥 +Q ( 𝑦 +Q 𝑦 ) ) = ( 𝑦 +Q ( 𝑥 +Q 𝑦 ) )
23	16 17 22	3brtr3g	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑦 +Q 𝑥 ) <Q ( 𝑦 +Q ( 𝑥 +Q 𝑦 ) ) )
24		ltanq	⊢ ( 𝑦 ∈ Q → ( 𝑥 <Q ( 𝑥 +Q 𝑦 ) ↔ ( 𝑦 +Q 𝑥 ) <Q ( 𝑦 +Q ( 𝑥 +Q 𝑦 ) ) ) )
25	24	adantl	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑥 <Q ( 𝑥 +Q 𝑦 ) ↔ ( 𝑦 +Q 𝑥 ) <Q ( 𝑦 +Q ( 𝑥 +Q 𝑦 ) ) ) )
26	23 25	mpbird	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → 𝑥 <Q ( 𝑥 +Q 𝑦 ) )
27	3 5 26	vtocl2ga	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → 𝐴 <Q ( 𝐴 +Q 𝐵 ) )