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

Theorem addltmul 11118
Description: Sum is less than product for numbers greater than 2. (Contributed by Stefan Allan, 24-Sep-2010.)
Assertion
Ref Expression
addltmul (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (2 < 𝐴 ∧ 2 < 𝐵)) → (𝐴 + 𝐵) < (𝐴 · 𝐵))

Proof of Theorem addltmul
StepHypRef Expression
1 2re 10940 . . . . . . 7 2 ∈ ℝ
2 1re 9896 . . . . . . 7 1 ∈ ℝ
3 ltsub1 10376 . . . . . . 7 ((2 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (2 < 𝐴 ↔ (2 − 1) < (𝐴 − 1)))
41, 2, 3mp3an13 1407 . . . . . 6 (𝐴 ∈ ℝ → (2 < 𝐴 ↔ (2 − 1) < (𝐴 − 1)))
5 2m1e1 10985 . . . . . . 7 (2 − 1) = 1
65breq1i 4585 . . . . . 6 ((2 − 1) < (𝐴 − 1) ↔ 1 < (𝐴 − 1))
74, 6syl6bb 275 . . . . 5 (𝐴 ∈ ℝ → (2 < 𝐴 ↔ 1 < (𝐴 − 1)))
8 ltsub1 10376 . . . . . . 7 ((2 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 ∈ ℝ) → (2 < 𝐵 ↔ (2 − 1) < (𝐵 − 1)))
91, 2, 8mp3an13 1407 . . . . . 6 (𝐵 ∈ ℝ → (2 < 𝐵 ↔ (2 − 1) < (𝐵 − 1)))
105breq1i 4585 . . . . . 6 ((2 − 1) < (𝐵 − 1) ↔ 1 < (𝐵 − 1))
119, 10syl6bb 275 . . . . 5 (𝐵 ∈ ℝ → (2 < 𝐵 ↔ 1 < (𝐵 − 1)))
127, 11bi2anan9 913 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((2 < 𝐴 ∧ 2 < 𝐵) ↔ (1 < (𝐴 − 1) ∧ 1 < (𝐵 − 1))))
13 peano2rem 10200 . . . . 5 (𝐴 ∈ ℝ → (𝐴 − 1) ∈ ℝ)
14 peano2rem 10200 . . . . 5 (𝐵 ∈ ℝ → (𝐵 − 1) ∈ ℝ)
15 mulgt1 10734 . . . . . 6 ((((𝐴 − 1) ∈ ℝ ∧ (𝐵 − 1) ∈ ℝ) ∧ (1 < (𝐴 − 1) ∧ 1 < (𝐵 − 1))) → 1 < ((𝐴 − 1) · (𝐵 − 1)))
1615ex 449 . . . . 5 (((𝐴 − 1) ∈ ℝ ∧ (𝐵 − 1) ∈ ℝ) → ((1 < (𝐴 − 1) ∧ 1 < (𝐵 − 1)) → 1 < ((𝐴 − 1) · (𝐵 − 1))))
1713, 14, 16syl2an 493 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((1 < (𝐴 − 1) ∧ 1 < (𝐵 − 1)) → 1 < ((𝐴 − 1) · (𝐵 − 1))))
1812, 17sylbid 229 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((2 < 𝐴 ∧ 2 < 𝐵) → 1 < ((𝐴 − 1) · (𝐵 − 1))))
19 recn 9883 . . . . . 6 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
20 recn 9883 . . . . . 6 (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
21 ax-1cn 9851 . . . . . . 7 1 ∈ ℂ
22 mulsub 10325 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) ∧ (𝐵 ∈ ℂ ∧ 1 ∈ ℂ)) → ((𝐴 − 1) · (𝐵 − 1)) = (((𝐴 · 𝐵) + (1 · 1)) − ((𝐴 · 1) + (𝐵 · 1))))
2321, 22mpanl2 713 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 1 ∈ ℂ)) → ((𝐴 − 1) · (𝐵 − 1)) = (((𝐴 · 𝐵) + (1 · 1)) − ((𝐴 · 1) + (𝐵 · 1))))
2421, 23mpanr2 716 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 1) · (𝐵 − 1)) = (((𝐴 · 𝐵) + (1 · 1)) − ((𝐴 · 1) + (𝐵 · 1))))
2519, 20, 24syl2an 493 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 − 1) · (𝐵 − 1)) = (((𝐴 · 𝐵) + (1 · 1)) − ((𝐴 · 1) + (𝐵 · 1))))
2625breq2d 4590 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (1 < ((𝐴 − 1) · (𝐵 − 1)) ↔ 1 < (((𝐴 · 𝐵) + (1 · 1)) − ((𝐴 · 1) + (𝐵 · 1)))))
27 1t1e1 11025 . . . . . . 7 (1 · 1) = 1
2827oveq2i 6538 . . . . . 6 ((𝐴 · 𝐵) + (1 · 1)) = ((𝐴 · 𝐵) + 1)
2928breq2i 4586 . . . . 5 ((((𝐴 · 1) + (𝐵 · 1)) + 1) < ((𝐴 · 𝐵) + (1 · 1)) ↔ (((𝐴 · 1) + (𝐵 · 1)) + 1) < ((𝐴 · 𝐵) + 1))
30 remulcl 9878 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 · 1) ∈ ℝ)
312, 30mpan2 703 . . . . . . 7 (𝐴 ∈ ℝ → (𝐴 · 1) ∈ ℝ)
32 remulcl 9878 . . . . . . . 8 ((𝐵 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐵 · 1) ∈ ℝ)
332, 32mpan2 703 . . . . . . 7 (𝐵 ∈ ℝ → (𝐵 · 1) ∈ ℝ)
34 readdcl 9876 . . . . . . 7 (((𝐴 · 1) ∈ ℝ ∧ (𝐵 · 1) ∈ ℝ) → ((𝐴 · 1) + (𝐵 · 1)) ∈ ℝ)
3531, 33, 34syl2an 493 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 · 1) + (𝐵 · 1)) ∈ ℝ)
36 remulcl 9878 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
372, 2remulcli 9911 . . . . . . 7 (1 · 1) ∈ ℝ
38 readdcl 9876 . . . . . . 7 (((𝐴 · 𝐵) ∈ ℝ ∧ (1 · 1) ∈ ℝ) → ((𝐴 · 𝐵) + (1 · 1)) ∈ ℝ)
3936, 37, 38sylancl 693 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 · 𝐵) + (1 · 1)) ∈ ℝ)
40 ltaddsub2 10355 . . . . . . 7 ((((𝐴 · 1) + (𝐵 · 1)) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐴 · 𝐵) + (1 · 1)) ∈ ℝ) → ((((𝐴 · 1) + (𝐵 · 1)) + 1) < ((𝐴 · 𝐵) + (1 · 1)) ↔ 1 < (((𝐴 · 𝐵) + (1 · 1)) − ((𝐴 · 1) + (𝐵 · 1)))))
412, 40mp3an2 1404 . . . . . 6 ((((𝐴 · 1) + (𝐵 · 1)) ∈ ℝ ∧ ((𝐴 · 𝐵) + (1 · 1)) ∈ ℝ) → ((((𝐴 · 1) + (𝐵 · 1)) + 1) < ((𝐴 · 𝐵) + (1 · 1)) ↔ 1 < (((𝐴 · 𝐵) + (1 · 1)) − ((𝐴 · 1) + (𝐵 · 1)))))
4235, 39, 41syl2anc 691 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((((𝐴 · 1) + (𝐵 · 1)) + 1) < ((𝐴 · 𝐵) + (1 · 1)) ↔ 1 < (((𝐴 · 𝐵) + (1 · 1)) − ((𝐴 · 1) + (𝐵 · 1)))))
4329, 42syl5rbbr 274 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (1 < (((𝐴 · 𝐵) + (1 · 1)) − ((𝐴 · 1) + (𝐵 · 1))) ↔ (((𝐴 · 1) + (𝐵 · 1)) + 1) < ((𝐴 · 𝐵) + 1)))
44 ltadd1 10347 . . . . . . 7 ((((𝐴 · 1) + (𝐵 · 1)) ∈ ℝ ∧ (𝐴 · 𝐵) ∈ ℝ ∧ 1 ∈ ℝ) → (((𝐴 · 1) + (𝐵 · 1)) < (𝐴 · 𝐵) ↔ (((𝐴 · 1) + (𝐵 · 1)) + 1) < ((𝐴 · 𝐵) + 1)))
452, 44mp3an3 1405 . . . . . 6 ((((𝐴 · 1) + (𝐵 · 1)) ∈ ℝ ∧ (𝐴 · 𝐵) ∈ ℝ) → (((𝐴 · 1) + (𝐵 · 1)) < (𝐴 · 𝐵) ↔ (((𝐴 · 1) + (𝐵 · 1)) + 1) < ((𝐴 · 𝐵) + 1)))
4635, 36, 45syl2anc 691 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝐴 · 1) + (𝐵 · 1)) < (𝐴 · 𝐵) ↔ (((𝐴 · 1) + (𝐵 · 1)) + 1) < ((𝐴 · 𝐵) + 1)))
47 ax-1rid 9863 . . . . . . 7 (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
48 ax-1rid 9863 . . . . . . 7 (𝐵 ∈ ℝ → (𝐵 · 1) = 𝐵)
4947, 48oveqan12d 6546 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 · 1) + (𝐵 · 1)) = (𝐴 + 𝐵))
5049breq1d 4588 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝐴 · 1) + (𝐵 · 1)) < (𝐴 · 𝐵) ↔ (𝐴 + 𝐵) < (𝐴 · 𝐵)))
5146, 50bitr3d 269 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((((𝐴 · 1) + (𝐵 · 1)) + 1) < ((𝐴 · 𝐵) + 1) ↔ (𝐴 + 𝐵) < (𝐴 · 𝐵)))
5226, 43, 513bitrd 293 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (1 < ((𝐴 − 1) · (𝐵 − 1)) ↔ (𝐴 + 𝐵) < (𝐴 · 𝐵)))
5318, 52sylibd 228 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((2 < 𝐴 ∧ 2 < 𝐵) → (𝐴 + 𝐵) < (𝐴 · 𝐵)))
5453imp 444 1 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (2 < 𝐴 ∧ 2 < 𝐵)) → (𝐴 + 𝐵) < (𝐴 · 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383   = wceq 1475  wcel 1977   class class class wbr 4578  (class class class)co 6527  cc 9791  cr 9792  1c1 9794   + caddc 9796   · cmul 9798   < clt 9931  cmin 10118  2c2 10920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-br 4579  df-opab 4639  df-mpt 4640  df-id 4943  df-po 4949  df-so 4950  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-er 7607  df-en 7820  df-dom 7821  df-sdom 7822  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-2 10929
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator