ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ltaddnq GIF version

Theorem ltaddnq 7237
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 𝐵))

Proof of Theorem ltaddnq
Dummy variables 𝑟 𝑠 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1lt2nq 7236 . . . . . . 7 1Q <Q (1Q +Q 1Q)
2 1nq 7196 . . . . . . . 8 1QQ
3 addclnq 7205 . . . . . . . . 9 ((1QQ ∧ 1QQ) → (1Q +Q 1Q) ∈ Q)
42, 2, 3mp2an 423 . . . . . . . 8 (1Q +Q 1Q) ∈ Q
5 ltmnqg 7231 . . . . . . . 8 ((1QQ ∧ (1Q +Q 1Q) ∈ Q𝐵Q) → (1Q <Q (1Q +Q 1Q) ↔ (𝐵 ·Q 1Q) <Q (𝐵 ·Q (1Q +Q 1Q))))
62, 4, 5mp3an12 1306 . . . . . . 7 (𝐵Q → (1Q <Q (1Q +Q 1Q) ↔ (𝐵 ·Q 1Q) <Q (𝐵 ·Q (1Q +Q 1Q))))
71, 6mpbii 147 . . . . . 6 (𝐵Q → (𝐵 ·Q 1Q) <Q (𝐵 ·Q (1Q +Q 1Q)))
8 mulidnq 7219 . . . . . 6 (𝐵Q → (𝐵 ·Q 1Q) = 𝐵)
9 distrnqg 7217 . . . . . . . 8 ((𝐵Q ∧ 1QQ ∧ 1QQ) → (𝐵 ·Q (1Q +Q 1Q)) = ((𝐵 ·Q 1Q) +Q (𝐵 ·Q 1Q)))
102, 2, 9mp3an23 1308 . . . . . . 7 (𝐵Q → (𝐵 ·Q (1Q +Q 1Q)) = ((𝐵 ·Q 1Q) +Q (𝐵 ·Q 1Q)))
118, 8oveq12d 5798 . . . . . . 7 (𝐵Q → ((𝐵 ·Q 1Q) +Q (𝐵 ·Q 1Q)) = (𝐵 +Q 𝐵))
1210, 11eqtrd 2173 . . . . . 6 (𝐵Q → (𝐵 ·Q (1Q +Q 1Q)) = (𝐵 +Q 𝐵))
137, 8, 123brtr3d 3965 . . . . 5 (𝐵Q𝐵 <Q (𝐵 +Q 𝐵))
1413adantl 275 . . . 4 ((𝐴Q𝐵Q) → 𝐵 <Q (𝐵 +Q 𝐵))
15 simpr 109 . . . . 5 ((𝐴Q𝐵Q) → 𝐵Q)
16 addclnq 7205 . . . . . . 7 ((𝐵Q𝐵Q) → (𝐵 +Q 𝐵) ∈ Q)
1716anidms 395 . . . . . 6 (𝐵Q → (𝐵 +Q 𝐵) ∈ Q)
1817adantl 275 . . . . 5 ((𝐴Q𝐵Q) → (𝐵 +Q 𝐵) ∈ Q)
19 simpl 108 . . . . 5 ((𝐴Q𝐵Q) → 𝐴Q)
20 ltanqg 7230 . . . . 5 ((𝐵Q ∧ (𝐵 +Q 𝐵) ∈ Q𝐴Q) → (𝐵 <Q (𝐵 +Q 𝐵) ↔ (𝐴 +Q 𝐵) <Q (𝐴 +Q (𝐵 +Q 𝐵))))
2115, 18, 19, 20syl3anc 1217 . . . 4 ((𝐴Q𝐵Q) → (𝐵 <Q (𝐵 +Q 𝐵) ↔ (𝐴 +Q 𝐵) <Q (𝐴 +Q (𝐵 +Q 𝐵))))
2214, 21mpbid 146 . . 3 ((𝐴Q𝐵Q) → (𝐴 +Q 𝐵) <Q (𝐴 +Q (𝐵 +Q 𝐵)))
23 addcomnqg 7211 . . 3 ((𝐴Q𝐵Q) → (𝐴 +Q 𝐵) = (𝐵 +Q 𝐴))
24 addcomnqg 7211 . . . . 5 ((𝑟Q𝑠Q) → (𝑟 +Q 𝑠) = (𝑠 +Q 𝑟))
2524adantl 275 . . . 4 (((𝐴Q𝐵Q) ∧ (𝑟Q𝑠Q)) → (𝑟 +Q 𝑠) = (𝑠 +Q 𝑟))
26 addassnqg 7212 . . . . 5 ((𝑟Q𝑠Q𝑡Q) → ((𝑟 +Q 𝑠) +Q 𝑡) = (𝑟 +Q (𝑠 +Q 𝑡)))
2726adantl 275 . . . 4 (((𝐴Q𝐵Q) ∧ (𝑟Q𝑠Q𝑡Q)) → ((𝑟 +Q 𝑠) +Q 𝑡) = (𝑟 +Q (𝑠 +Q 𝑡)))
2819, 15, 15, 25, 27caov12d 5958 . . 3 ((𝐴Q𝐵Q) → (𝐴 +Q (𝐵 +Q 𝐵)) = (𝐵 +Q (𝐴 +Q 𝐵)))
2922, 23, 283brtr3d 3965 . 2 ((𝐴Q𝐵Q) → (𝐵 +Q 𝐴) <Q (𝐵 +Q (𝐴 +Q 𝐵)))
30 addclnq 7205 . . 3 ((𝐴Q𝐵Q) → (𝐴 +Q 𝐵) ∈ Q)
31 ltanqg 7230 . . 3 ((𝐴Q ∧ (𝐴 +Q 𝐵) ∈ Q𝐵Q) → (𝐴 <Q (𝐴 +Q 𝐵) ↔ (𝐵 +Q 𝐴) <Q (𝐵 +Q (𝐴 +Q 𝐵))))
3219, 30, 15, 31syl3anc 1217 . 2 ((𝐴Q𝐵Q) → (𝐴 <Q (𝐴 +Q 𝐵) ↔ (𝐵 +Q 𝐴) <Q (𝐵 +Q (𝐴 +Q 𝐵))))
3329, 32mpbird 166 1 ((𝐴Q𝐵Q) → 𝐴 <Q (𝐴 +Q 𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  w3a 963   = wceq 1332  wcel 1481   class class class wbr 3935  (class class class)co 5780  Qcnq 7110  1Qc1q 7111   +Q cplq 7112   ·Q cmq 7113   <Q cltq 7115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4049  ax-sep 4052  ax-nul 4060  ax-pow 4104  ax-pr 4137  ax-un 4361  ax-setind 4458  ax-iinf 4508
This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2691  df-sbc 2913  df-csb 3007  df-dif 3076  df-un 3078  df-in 3080  df-ss 3087  df-nul 3367  df-pw 3515  df-sn 3536  df-pr 3537  df-op 3539  df-uni 3743  df-int 3778  df-iun 3821  df-br 3936  df-opab 3996  df-mpt 3997  df-tr 4033  df-eprel 4217  df-id 4221  df-iord 4294  df-on 4296  df-suc 4299  df-iom 4511  df-xp 4551  df-rel 4552  df-cnv 4553  df-co 4554  df-dm 4555  df-rn 4556  df-res 4557  df-ima 4558  df-iota 5094  df-fun 5131  df-fn 5132  df-f 5133  df-f1 5134  df-fo 5135  df-f1o 5136  df-fv 5137  df-ov 5783  df-oprab 5784  df-mpo 5785  df-1st 6044  df-2nd 6045  df-recs 6208  df-irdg 6273  df-1o 6319  df-oadd 6323  df-omul 6324  df-er 6435  df-ec 6437  df-qs 6441  df-ni 7134  df-pli 7135  df-mi 7136  df-lti 7137  df-plpq 7174  df-mpq 7175  df-enq 7177  df-nqqs 7178  df-plqqs 7179  df-mqqs 7180  df-1nqqs 7181  df-ltnqqs 7183
This theorem is referenced by:  ltexnqq  7238  nsmallnqq  7242  subhalfnqq  7244  ltbtwnnqq  7245  prarloclemarch2  7249  ltexprlemm  7430  ltexprlemopl  7431  addcanprleml  7444  addcanprlemu  7445  recexprlemm  7454  cauappcvgprlemm  7475  cauappcvgprlemopl  7476  cauappcvgprlem2  7490  caucvgprlemnkj  7496  caucvgprlemnbj  7497  caucvgprlemm  7498  caucvgprlemopl  7499  caucvgprprlemnjltk  7521  caucvgprprlemopl  7527  suplocexprlemmu  7548
  Copyright terms: Public domain W3C validator