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 ( ( 𝐴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 syl5ib ( 𝑥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 𝐵 ) )