Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltaddnq Structured version   Visualization version   GIF version

 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.)
Assertion
Ref Expression
ltaddnq ((𝐴Q𝐵Q) → 𝐴 <Q (𝐴 +Q 𝐵))

Dummy variables 𝑥 𝑦 𝑠 𝑟 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 22 . . 3 (𝑥 = 𝐴𝑥 = 𝐴)
2 oveq1 7156 . . 3 (𝑥 = 𝐴 → (𝑥 +Q 𝑦) = (𝐴 +Q 𝑦))
31, 2breq12d 5065 . 2 (𝑥 = 𝐴 → (𝑥 <Q (𝑥 +Q 𝑦) ↔ 𝐴 <Q (𝐴 +Q 𝑦)))
4 oveq2 7157 . . 3 (𝑦 = 𝐵 → (𝐴 +Q 𝑦) = (𝐴 +Q 𝐵))
54breq2d 5064 . 2 (𝑦 = 𝐵 → (𝐴 <Q (𝐴 +Q 𝑦) ↔ 𝐴 <Q (𝐴 +Q 𝐵)))
6 1lt2nq 10393 . . . . . . . 8 1Q <Q (1Q +Q 1Q)
7 ltmnq 10392 . . . . . . . 8 (𝑦Q → (1Q <Q (1Q +Q 1Q) ↔ (𝑦 ·Q 1Q) <Q (𝑦 ·Q (1Q +Q 1Q))))
86, 7mpbii 236 . . . . . . 7 (𝑦Q → (𝑦 ·Q 1Q) <Q (𝑦 ·Q (1Q +Q 1Q)))
9 mulidnq 10383 . . . . . . 7 (𝑦Q → (𝑦 ·Q 1Q) = 𝑦)
10 distrnq 10381 . . . . . . . 8 (𝑦 ·Q (1Q +Q 1Q)) = ((𝑦 ·Q 1Q) +Q (𝑦 ·Q 1Q))
119, 9oveq12d 7167 . . . . . . . 8 (𝑦Q → ((𝑦 ·Q 1Q) +Q (𝑦 ·Q 1Q)) = (𝑦 +Q 𝑦))
1210, 11syl5eq 2871 . . . . . . 7 (𝑦Q → (𝑦 ·Q (1Q +Q 1Q)) = (𝑦 +Q 𝑦))
138, 9, 123brtr3d 5083 . . . . . 6 (𝑦Q𝑦 <Q (𝑦 +Q 𝑦))
14 ltanq 10391 . . . . . 6 (𝑥Q → (𝑦 <Q (𝑦 +Q 𝑦) ↔ (𝑥 +Q 𝑦) <Q (𝑥 +Q (𝑦 +Q 𝑦))))
1513, 14syl5ib 247 . . . . 5 (𝑥Q → (𝑦Q → (𝑥 +Q 𝑦) <Q (𝑥 +Q (𝑦 +Q 𝑦))))
1615imp 410 . . . 4 ((𝑥Q𝑦Q) → (𝑥 +Q 𝑦) <Q (𝑥 +Q (𝑦 +Q 𝑦)))
17 addcomnq 10371 . . . 4 (𝑥 +Q 𝑦) = (𝑦 +Q 𝑥)
18 vex 3483 . . . . 5 𝑥 ∈ V
19 vex 3483 . . . . 5 𝑦 ∈ V
20 addcomnq 10371 . . . . 5 (𝑟 +Q 𝑠) = (𝑠 +Q 𝑟)
21 addassnq 10378 . . . . 5 ((𝑟 +Q 𝑠) +Q 𝑡) = (𝑟 +Q (𝑠 +Q 𝑡))
2218, 19, 19, 20, 21caov12 7370 . . . 4 (𝑥 +Q (𝑦 +Q 𝑦)) = (𝑦 +Q (𝑥 +Q 𝑦))
2316, 17, 223brtr3g 5085 . . 3 ((𝑥Q𝑦Q) → (𝑦 +Q 𝑥) <Q (𝑦 +Q (𝑥 +Q 𝑦)))
24 ltanq 10391 . . . 4 (𝑦Q → (𝑥 <Q (𝑥 +Q 𝑦) ↔ (𝑦 +Q 𝑥) <Q (𝑦 +Q (𝑥 +Q 𝑦))))
2524adantl 485 . . 3 ((𝑥Q𝑦Q) → (𝑥 <Q (𝑥 +Q 𝑦) ↔ (𝑦 +Q 𝑥) <Q (𝑦 +Q (𝑥 +Q 𝑦))))
2623, 25mpbird 260 . 2 ((𝑥Q𝑦Q) → 𝑥 <Q (𝑥 +Q 𝑦))
273, 5, 26vtocl2ga 3561 1 ((𝐴Q𝐵Q) → 𝐴 <Q (𝐴 +Q 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2115   class class class wbr 5052  (class class class)co 7149  Qcnq 10272  1Qc1q 10273   +Q cplq 10275   ·Q cmq 10276
 Copyright terms: Public domain W3C validator