Theorem lenltd 11286

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2114   class class class wbr 5086  ℝcr 11031   < clt 11173   ≤ cle 11174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5631  df-cnv 5633  df-xr 11177  df-le 11179

This theorem is referenced by:  ltnsymd  11289  nltled  11290  lensymd  11291  leadd1  11612  leord1  11671  lediv1  12015  lemuldiv  12030  lerec  12033  le2msq  12050  suprleub  12116  infregelb  12134  suprfinzcl  12637  uzinfi  12872  rpnnen1lem5  12925  nn0disj  13592  fleqceilz  13807  modsumfzodifsn  13900  addmodlteq  13902  leexp2  14127  expnngt1  14197  hashf1  14413  swrdccatin2  14685  isercoll  15624  ruclem3  16194  sadcaddlem  16420  pcfac  16864  sylow1lem1  19567  fvmptnn04if  22827  chfacfisf  22832  chfacfisfcpmat  22833  ivthlem2  25432  ioorcl2  25552  itg1ge0a  25691  mbfi1fseqlem4  25698  itg2monolem1  25730  itg2cnlem1  25741  mdegmullem  26056  quotcan  26289  logdivle  26602  cxple  26675  gausslemma2dlem1a  27345  padicabv  27610  upgrewlkle2  29693  pthdlem1  29852  ssnnssfz  32878  smattr  33962  smatbl  33963  smatbr  33964  esumpcvgval  34241  eulerpartlems  34523  dstfrvunirn  34638  ballotlemodife  34661  erdszelem7  35398  erdszelem8  35399  unbdqndv2lem1  36788  poimirlem2  37960  poimirlem7  37965  poimirlem10  37968  poimirlem11  37969  areacirc  38051  aks4d1p1p7  42530  aks4d1p3  42534  aks4d1p5  42536  hashscontpow1  42577  sticksstones22  42624  aks6d1c6lem4  42629  aks5lem8  42657  readvrec  42811  frlmvscadiccat  42968  rencldnfilem  43269  irrapxlem1  43271  monotoddzzfi  43391  sqrtcvallem1  44079  reabsifneg  44080  reabsifpos  44082  radcnvrat  44762  reclt0d  45837  reclt0  45841  sqrlearg  46004  dvnxpaek  46391  volico  46432  sublevolico  46433  fourierdlem12  46568  fourierdlem42  46598  elaa2lem  46682  iundjiun  46909  hoidmvval0  47036  hoidmv1lelem2  47041  hoidmv1lelem3  47042  hoidmvlelem4  47047  hspdifhsp  47065  volico2  47090  ovolval2lem  47092  vonioo  47131  smfconst  47198  fzopredsuc  47787  stgoldbwt  48267  nnsum3primesle9  48285  bgoldbtbndlem1  48296  ssnn0ssfz  48840