Theorem lenltd 11386

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2109   class class class wbr 5124  ℝcr 11133   < clt 11274   ≤ cle 11275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-xp 5665  df-cnv 5667  df-xr 11278  df-le 11280

This theorem is referenced by:  ltnsymd  11389  nltled  11390  lensymd  11391  leadd1  11710  leord1  11769  lediv1  12112  lemuldiv  12127  lerec  12130  le2msq  12147  suprleub  12213  infregelb  12231  suprfinzcl  12712  uzinfi  12949  rpnnen1lem5  13002  nn0disj  13666  fleqceilz  13876  modsumfzodifsn  13967  addmodlteq  13969  leexp2  14194  expnngt1  14264  hashf1  14480  swrdccatin2  14752  isercoll  15689  ruclem3  16256  sadcaddlem  16481  pcfac  16924  sylow1lem1  19584  fvmptnn04if  22792  chfacfisf  22797  chfacfisfcpmat  22798  ivthlem2  25410  ioorcl2  25530  itg1ge0a  25669  mbfi1fseqlem4  25676  itg2monolem1  25708  itg2cnlem1  25719  mdegmullem  26040  quotcan  26274  logdivle  26588  cxple  26661  gausslemma2dlem1a  27333  padicabv  27598  upgrewlkle2  29591  pthdlem1  29753  ssnnssfz  32769  smattr  33835  smatbl  33836  smatbr  33837  esumpcvgval  34114  eulerpartlems  34397  dstfrvunirn  34512  ballotlemodife  34535  erdszelem7  35224  erdszelem8  35225  unbdqndv2lem1  36532  poimirlem2  37651  poimirlem7  37656  poimirlem10  37659  poimirlem11  37660  areacirc  37742  aks4d1p1p7  42092  aks4d1p3  42096  aks4d1p5  42098  hashscontpow1  42139  sticksstones22  42186  aks6d1c6lem4  42191  aks5lem8  42219  readvrec  42372  frlmvscadiccat  42496  rencldnfilem  42810  irrapxlem1  42812  monotoddzzfi  42933  sqrtcvallem1  43622  reabsifneg  43623  reabsifpos  43625  radcnvrat  44305  reclt0d  45381  reclt0  45385  sqrlearg  45549  dvnxpaek  45938  volico  45979  sublevolico  45980  fourierdlem12  46115  fourierdlem42  46145  elaa2lem  46229  iundjiun  46456  hoidmvval0  46583  hoidmv1lelem2  46588  hoidmv1lelem3  46589  hoidmvlelem4  46594  hspdifhsp  46612  volico2  46637  ovolval2lem  46639  vonioo  46678  smfconst  46745  fzopredsuc  47319  stgoldbwt  47757  nnsum3primesle9  47775  bgoldbtbndlem1  47786  ssnn0ssfz  48291