Theorem lenltd 11279

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 11211	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2113   class class class wbr 5098  ℝcr 11025   < clt 11166   ≤ cle 11167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-cnv 5632  df-xr 11170  df-le 11172

This theorem is referenced by:  ltnsymd  11282  nltled  11283  lensymd  11284  leadd1  11605  leord1  11664  lediv1  12007  lemuldiv  12022  lerec  12025  le2msq  12042  suprleub  12108  infregelb  12126  suprfinzcl  12606  uzinfi  12841  rpnnen1lem5  12894  nn0disj  13560  fleqceilz  13774  modsumfzodifsn  13867  addmodlteq  13869  leexp2  14094  expnngt1  14164  hashf1  14380  swrdccatin2  14652  isercoll  15591  ruclem3  16158  sadcaddlem  16384  pcfac  16827  sylow1lem1  19527  fvmptnn04if  22793  chfacfisf  22798  chfacfisfcpmat  22799  ivthlem2  25409  ioorcl2  25529  itg1ge0a  25668  mbfi1fseqlem4  25675  itg2monolem1  25707  itg2cnlem1  25718  mdegmullem  26039  quotcan  26273  logdivle  26587  cxple  26660  gausslemma2dlem1a  27332  padicabv  27597  upgrewlkle2  29680  pthdlem1  29839  ssnnssfz  32867  smattr  33956  smatbl  33957  smatbr  33958  esumpcvgval  34235  eulerpartlems  34517  dstfrvunirn  34632  ballotlemodife  34655  erdszelem7  35391  erdszelem8  35392  unbdqndv2lem1  36709  poimirlem2  37823  poimirlem7  37828  poimirlem10  37831  poimirlem11  37832  areacirc  37914  aks4d1p1p7  42338  aks4d1p3  42342  aks4d1p5  42344  hashscontpow1  42385  sticksstones22  42432  aks6d1c6lem4  42437  aks5lem8  42465  readvrec  42627  frlmvscadiccat  42771  rencldnfilem  43072  irrapxlem1  43074  monotoddzzfi  43194  sqrtcvallem1  43882  reabsifneg  43883  reabsifpos  43885  radcnvrat  44565  reclt0d  45641  reclt0  45645  sqrlearg  45809  dvnxpaek  46196  volico  46237  sublevolico  46238  fourierdlem12  46373  fourierdlem42  46403  elaa2lem  46487  iundjiun  46714  hoidmvval0  46841  hoidmv1lelem2  46846  hoidmv1lelem3  46847  hoidmvlelem4  46852  hspdifhsp  46870  volico2  46895  ovolval2lem  46897  vonioo  46936  smfconst  47003  fzopredsuc  47579  stgoldbwt  48032  nnsum3primesle9  48050  bgoldbtbndlem1  48061  ssnn0ssfz  48605