Theorem lenltd 11360

Description: 'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
ltd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
lenltd	⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))

Proof of Theorem lenltd

Step	Hyp	Ref	Expression
1		ltd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		ltd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		lenlt 11292	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∈ wcel 2107   class class class wbr 5149  ℝcr 11109   < clt 11248   ≤ cle 11249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-xp 5683  df-cnv 5685  df-xr 11252  df-le 11254

This theorem is referenced by:  ltnsymd  11363  nltled  11364  lensymd  11365  leadd1  11682  leord1  11741  lediv1  12079  lemuldiv  12094  lerec  12097  le2msq  12114  suprleub  12180  infregelb  12198  suprfinzcl  12676  uzinfi  12912  rpnnen1lem5  12965  nn0disj  13617  fleqceilz  13819  modsumfzodifsn  13909  addmodlteq  13911  leexp2  14136  expnngt1  14204  hashf1  14418  swrdccatin2  14679  isercoll  15614  ruclem3  16176  sadcaddlem  16398  pcfac  16832  sylow1lem1  19466  fvmptnn04if  22351  chfacfisf  22356  chfacfisfcpmat  22357  ivthlem2  24969  ioorcl2  25089  itg1ge0a  25229  mbfi1fseqlem4  25236  itg2monolem1  25268  itg2cnlem1  25279  mdegmullem  25596  quotcan  25822  logdivle  26130  cxple  26203  gausslemma2dlem1a  26868  padicabv  27133  upgrewlkle2  28894  pthdlem1  29054  ssnnssfz  32029  smattr  32810  smatbl  32811  smatbr  32812  esumpcvgval  33107  eulerpartlems  33390  dstfrvunirn  33504  ballotlemodife  33527  erdszelem7  34219  erdszelem8  34220  unbdqndv2lem1  35433  poimirlem2  36538  poimirlem7  36543  poimirlem10  36546  poimirlem11  36547  areacirc  36629  aks4d1p1p7  40987  aks4d1p3  40991  aks4d1p5  40993  sticksstones22  41032  metakunt7  41039  metakunt12  41044  metakunt22  41054  metakunt28  41060  metakunt29  41061  metakunt30  41062  frlmvscadiccat  41128  rencldnfilem  41606  irrapxlem1  41608  monotoddzzfi  41729  sqrtcvallem1  42430  reabsifneg  42431  reabsifpos  42433  radcnvrat  43121  reclt0d  44145  reclt0  44149  sqrlearg  44314  dvnxpaek  44706  volico  44747  sublevolico  44748  fourierdlem12  44883  fourierdlem42  44913  elaa2lem  44997  iundjiun  45224  hoidmvval0  45351  hoidmv1lelem2  45356  hoidmv1lelem3  45357  hoidmvlelem4  45362  hspdifhsp  45380  volico2  45405  ovolval2lem  45407  vonioo  45446  smfconst  45513  fzopredsuc  46079  stgoldbwt  46492  nnsum3primesle9  46510  bgoldbtbndlem1  46521  ssnn0ssfz  47073