Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltaddnq Structured version   Unicode 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

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 20 . . 3
2 oveq1 6080 . . 3
31, 2breq12d 4217 . 2
4 oveq2 6081 . . 3
54breq2d 4216 . 2
6 1lt2nq 8842 . . . . . . . 8
7 ltmnq 8841 . . . . . . . 8
86, 7mpbii 203 . . . . . . 7
9 mulidnq 8832 . . . . . . 7
10 distrnq 8830 . . . . . . . 8
119, 9oveq12d 6091 . . . . . . . 8
1210, 11syl5eq 2479 . . . . . . 7
138, 9, 123brtr3d 4233 . . . . . 6
14 ltanq 8840 . . . . . 6
1513, 14syl5ib 211 . . . . 5
1615imp 419 . . . 4
17 addcomnq 8820 . . . 4
18 vex 2951 . . . . 5
19 vex 2951 . . . . 5
20 addcomnq 8820 . . . . 5
21 addassnq 8827 . . . . 5
2218, 19, 19, 20, 21caov12 6267 . . . 4
2316, 17, 223brtr3g 4235 . . 3
24 ltanq 8840 . . . 4