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 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 𝐵 ) )