Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ltaddnq 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.)
Assertion
Ref Expression
ltaddnq ((𝐴Q𝐵Q) → 𝐴 <Q (𝐴 +Q 𝐵))

Dummy variables 𝑟 𝑠 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1lt2nq 6658 . . . . . . 7 1Q <Q (1Q +Q 1Q)
2 1nq 6618 . . . . . . . 8 1QQ
3 addclnq 6627 . . . . . . . . 9 ((1QQ ∧ 1QQ) → (1Q +Q 1Q) ∈ Q)
42, 2, 3mp2an 417 . . . . . . . 8 (1Q +Q 1Q) ∈ Q
5 ltmnqg 6653 . . . . . . . 8 ((1QQ ∧ (1Q +Q 1Q) ∈ Q𝐵Q) → (1Q <Q (1Q +Q 1Q) ↔ (𝐵 ·Q 1Q) <Q (𝐵 ·Q (1Q +Q 1Q))))
62, 4, 5mp3an12 1259 . . . . . . 7 (𝐵Q → (1Q <Q (1Q +Q 1Q) ↔ (𝐵 ·Q 1Q) <Q (𝐵 ·Q (1Q +Q 1Q))))
71, 6mpbii 146 . . . . . 6 (𝐵Q → (𝐵 ·Q 1Q) <Q (𝐵 ·Q (1Q +Q 1Q)))
8 mulidnq 6641 . . . . . 6 (𝐵Q → (𝐵 ·Q 1Q) = 𝐵)
9 distrnqg 6639 . . . . . . . 8 ((𝐵Q ∧ 1QQ ∧ 1QQ) → (𝐵 ·Q (1Q +Q 1Q)) = ((𝐵 ·Q 1Q) +Q (𝐵 ·Q 1Q)))
102, 2, 9mp3an23 1261 . . . . . . 7 (𝐵Q → (𝐵 ·Q (1Q +Q 1Q)) = ((𝐵 ·Q 1Q) +Q (𝐵 ·Q 1Q)))
118, 8oveq12d 5561 . . . . . . 7 (𝐵Q → ((𝐵 ·Q 1Q) +Q (𝐵 ·Q 1Q)) = (𝐵 +Q 𝐵))
1210, 11eqtrd 2114 . . . . . 6 (𝐵Q → (𝐵 ·Q (1Q +Q 1Q)) = (𝐵 +Q 𝐵))
137, 8, 123brtr3d 3822 . . . . 5 (𝐵Q𝐵 <Q (𝐵 +Q 𝐵))
1413adantl 271 . . . 4 ((𝐴Q𝐵Q) → 𝐵 <Q (𝐵 +Q 𝐵))
15 simpr 108 . . . . 5 ((𝐴Q𝐵Q) → 𝐵Q)
16 addclnq 6627 . . . . . . 7 ((𝐵Q𝐵Q) → (𝐵 +Q 𝐵) ∈ Q)
1716anidms 389 . . . . . 6 (𝐵Q → (𝐵 +Q 𝐵) ∈ Q)
1817adantl 271 . . . . 5 ((𝐴Q𝐵Q) → (𝐵 +Q 𝐵) ∈ Q)
19 simpl 107 . . . . 5 ((𝐴Q𝐵Q) → 𝐴Q)
20 ltanqg 6652 . . . . 5 ((𝐵Q ∧ (𝐵 +Q 𝐵) ∈ Q𝐴Q) → (𝐵 <Q (𝐵 +Q 𝐵) ↔ (𝐴 +Q 𝐵) <Q (𝐴 +Q (𝐵 +Q 𝐵))))
2115, 18, 19, 20syl3anc 1170 . . . 4 ((𝐴Q𝐵Q) → (𝐵 <Q (𝐵 +Q 𝐵) ↔ (𝐴 +Q 𝐵) <Q (𝐴 +Q (𝐵 +Q 𝐵))))
2214, 21mpbid 145 . . 3 ((𝐴Q𝐵Q) → (𝐴 +Q 𝐵) <Q (𝐴 +Q (𝐵 +Q 𝐵)))
23 addcomnqg 6633 . . 3 ((𝐴Q𝐵Q) → (𝐴 +Q 𝐵) = (𝐵 +Q 𝐴))
24 addcomnqg 6633 . . . . 5 ((𝑟Q𝑠Q) → (𝑟 +Q 𝑠) = (𝑠 +Q 𝑟))
2524adantl 271 . . . 4 (((𝐴Q𝐵Q) ∧ (𝑟Q𝑠Q)) → (𝑟 +Q 𝑠) = (𝑠 +Q 𝑟))
26 addassnqg 6634 . . . . 5 ((𝑟Q𝑠Q𝑡Q) → ((𝑟 +Q 𝑠) +Q 𝑡) = (𝑟 +Q (𝑠 +Q 𝑡)))
2726adantl 271 . . . 4 (((𝐴Q𝐵Q) ∧ (𝑟Q𝑠Q𝑡Q)) → ((𝑟 +Q 𝑠) +Q 𝑡) = (𝑟 +Q (𝑠 +Q 𝑡)))
2819, 15, 15, 25, 27caov12d 5713 . . 3 ((𝐴Q𝐵Q) → (𝐴 +Q (𝐵 +Q 𝐵)) = (𝐵 +Q (𝐴 +Q 𝐵)))
2922, 23, 283brtr3d 3822 . 2 ((𝐴Q𝐵Q) → (𝐵 +Q 𝐴) <Q (𝐵 +Q (𝐴 +Q 𝐵)))
30 addclnq 6627 . . 3 ((𝐴Q𝐵Q) → (𝐴 +Q 𝐵) ∈ Q)
31 ltanqg 6652 . . 3 ((𝐴Q ∧ (𝐴 +Q 𝐵) ∈ Q𝐵Q) → (𝐴 <Q (𝐴 +Q 𝐵) ↔ (𝐵 +Q 𝐴) <Q (𝐵 +Q (𝐴 +Q 𝐵))))
3219, 30, 15, 31syl3anc 1170 . 2 ((𝐴Q𝐵Q) → (𝐴 <Q (𝐴 +Q 𝐵) ↔ (𝐵 +Q 𝐴) <Q (𝐵 +Q (𝐴 +Q 𝐵))))
3329, 32mpbird 165 1 ((𝐴Q𝐵Q) → 𝐴 <Q (𝐴 +Q 𝐵))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103   ∧ w3a 920   = wceq 1285   ∈ wcel 1434   class class class wbr 3793  (class class class)co 5543  Qcnq 6532  1Qc1q 6533   +Q cplq 6534   ·Q cmq 6535
 Copyright terms: Public domain W3C validator