Theorem lenltd 11356

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ wcel 2149   class class class wbr 5113  ℝcr 11099   < clt 11243   ≤ cle 11244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-xp 5668  df-cnv 5670  df-xr 11247  df-le 11249

This theorem is referenced by:  ltnsymd  11359  nltled  11360  lensymd  11361  leadd1  11682  leord1  11741  lediv1  12080  lemuldiv  12095  lerec  12098  le2msq  12115  suprleub  12181  infregelb  12199  suprfinzcl  12710  uzinfi  12952  rpnnen1lem5  13005  nn0disj  13672  fleqceilz  13887  modsumfzodifsn  13980  addmodlteq  13982  leexp2  14207  expnngt1  14277  hashf1  14494  swrdccatin2  14766  isercoll  15719  ruclem3  16289  sadcaddlem  16515  pcfac  16959  sylow1lem1  19668  fvmptnn04if  22975  chfacfisf  22980  chfacfisfcpmat  22981  ivthlem2  25580  ioorcl2  25700  itg1ge0a  25839  mbfi1fseqlem4  25846  itg2monolem1  25878  itg2cnlem1  25889  mdegmullem  26204  quotcan  26439  logdivle  26753  cxple  26826  gausslemma2dlem1a  27495  padicabv  27760  upgrewlkle2  29897  pthdlem1  30056  ssnnssfz  33073  smattr  34134  smatbl  34135  smatbr  34136  esumpcvgval  34413  eulerpartlems  34695  dstfrvunirn  34810  ballotlemodife  34833  erdszelem7  35588  erdszelem8  35589  unbdqndv2lem1  36987  poimirlem2  38161  poimirlem7  38166  poimirlem10  38169  poimirlem11  38170  areacirc  38252  aks4d1p1p7  42731  aks4d1p3  42735  aks4d1p5  42737  hashscontpow1  42778  sticksstones22  42825  aks6d1c6lem4  42830  aks5lem8  42858  readvrec  43013  frlmvscadiccat  43170  rencldnfilem  43439  irrapxlem1  43441  monotoddzzfi  43561  sqrtcvallem1  44249  reabsifneg  44250  reabsifpos  44252  radcnvrat  44916  reclt0d  45994  reclt0  45998  sqrlearg  46161  dvnxpaek  46548  volico  46589  sublevolico  46590  fourierdlem12  46725  fourierdlem42  46755  elaa2lem  46839  iundjiun  47066  hoidmvval0  47193  hoidmv1lelem2  47198  hoidmv1lelem3  47199  hoidmvlelem4  47204  hspdifhsp  47222  volico2  47247  ovolval2lem  47249  vonioo  47288  smfconst  47355  fzopredsuc  47950  stgoldbwt  48430  nnsum3primesle9  48448  bgoldbtbndlem1  48459  ssnn0ssfz  49014