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

Theorem rphalflt 10738
Description: Half of a positive real is less than the original number. (Contributed by Mario Carneiro, 21-May-2014.)
Assertion
Ref Expression
rphalflt (𝐴 ∈ ℝ+ → (𝐴 / 2) < 𝐴)

Proof of Theorem rphalflt
StepHypRef Expression
1 elrp 10714 . 2 (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
2 halfpos 10296 . . 3 (𝐴 ∈ ℝ → (0 < 𝐴 ↔ (𝐴 / 2) < 𝐴))
32biimpa 472 . 2 ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → (𝐴 / 2) < 𝐴)
41, 3sylbi 189 1 (𝐴 ∈ ℝ+ → (𝐴 / 2) < 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 360  wcel 1734   class class class wbr 4293  (class class class)co 6181  cr 9086  0cc0 9087   < clt 9217   / cdiv 9775  2c2 10147  +crp 10712
This theorem is referenced by:  rpnnen2lem11  12944  sqr2irr  12968  metcnpi3  18708  cfilucfilOLD  18731  cfilucfil  18732  reperflem  18981  iccntr  18984  icccmplem2  18986  reconnlem2  18990  cnllycmp  19113  bcthlem5  19413  minveclem3  19462  ivthlem2  19481  lhop1lem  20029  dvcnvre  20035  aaliou  20387  aaliou2b  20390  cosordlem  20565  tanord1  20571  argregt0  20637  argrege0  20638  isosctrlem1  20794  asinsin  20864  asin1  20866  atan1  20900  lgsqrlem2  21258  lgsquadlem2  21271  lgsquadlem3  21272  2sqlem8  21288  chebbnd1lem2  21296  pntibnd  21419  pntlem3  21435  ubthlem1  22504  nmcexi  23661  lgamucov  25288  ftc1anc  26744  stoweidlem62  28305  isosctrlem1ALT  30014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-5 1573  ax-17 1636  ax-9 1677  ax-8 1698  ax-13 1736  ax-14 1738  ax-6 1753  ax-7 1758  ax-11 1770  ax-12 1963  ax-ext 2460  ax-sep 4414  ax-nul 4422  ax-pow 4467  ax-pr 4493  ax-un 4793  ax-resscn 9144  ax-1cn 9145  ax-icn 9146  ax-addcl 9147  ax-addrcl 9148  ax-mulcl 9149  ax-mulrcl 9150  ax-mulcom 9151  ax-addass 9152  ax-mulass 9153  ax-distr 9154  ax-i2m1 9155  ax-1ne0 9156  ax-1rid 9157  ax-rnegex 9158  ax-rrecex 9159  ax-cnre 9160  ax-pre-lttri 9161  ax-pre-lttrn 9162  ax-pre-ltadd 9163  ax-pre-mulgt0 9164
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 939  df-3an 940  df-tru 1334  df-ex 1558  df-nf 1561  df-sb 1669  df-eu 2325  df-mo 2326  df-clab 2466  df-cleq 2472  df-clel 2475  df-nfc 2604  df-ne 2644  df-nel 2645  df-ral 2753  df-rex 2754  df-reu 2755  df-rmo 2756  df-rab 2757  df-v 3005  df-sbc 3210  df-csb 3311  df-dif 3353  df-un 3355  df-in 3357  df-ss 3364  df-nul 3658  df-if 3810  df-pw 3875  df-sn 3894  df-pr 3895  df-op 3897  df-uni 4094  df-br 4294  df-opab 4352  df-mpt 4353  df-id 4590  df-po 4595  df-so 4596  df-xp 4976  df-rel 4977  df-cnv 4978  df-co 4979  df-dm 4980  df-rn 4981  df-res 4982  df-ima 4983  df-iota 5516  df-fun 5555  df-fn 5556  df-f 5557  df-f1 5558  df-fo 5559  df-f1o 5560  df-fv 5561  df-ov 6184  df-oprab 6185  df-mpt2 6186  df-riota 6654  df-er 7000  df-en 7205  df-dom 7206  df-sdom 7207  df-pnf 9219  df-mnf 9220  df-xr 9221  df-ltxr 9222  df-le 9223  df-sub 9391  df-neg 9392  df-div 9776  df-2 10156  df-rp 10713
  Copyright terms: Public domain W3C validator