Theorem lenltd 11296

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2109   class class class wbr 5102  ℝcr 11043   < clt 11184   ≤ cle 11185

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 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-cnv 5639  df-xr 11188  df-le 11190

This theorem is referenced by:  ltnsymd  11299  nltled  11300  lensymd  11301  leadd1  11622  leord1  11681  lediv1  12024  lemuldiv  12039  lerec  12042  le2msq  12059  suprleub  12125  infregelb  12143  suprfinzcl  12624  uzinfi  12863  rpnnen1lem5  12916  nn0disj  13581  fleqceilz  13792  modsumfzodifsn  13885  addmodlteq  13887  leexp2  14112  expnngt1  14182  hashf1  14398  swrdccatin2  14670  isercoll  15610  ruclem3  16177  sadcaddlem  16403  pcfac  16846  sylow1lem1  19512  fvmptnn04if  22769  chfacfisf  22774  chfacfisfcpmat  22775  ivthlem2  25386  ioorcl2  25506  itg1ge0a  25645  mbfi1fseqlem4  25652  itg2monolem1  25684  itg2cnlem1  25695  mdegmullem  26016  quotcan  26250  logdivle  26564  cxple  26637  gausslemma2dlem1a  27309  padicabv  27574  upgrewlkle2  29587  pthdlem1  29746  ssnnssfz  32760  smattr  33782  smatbl  33783  smatbr  33784  esumpcvgval  34061  eulerpartlems  34344  dstfrvunirn  34459  ballotlemodife  34482  erdszelem7  35177  erdszelem8  35178  unbdqndv2lem1  36490  poimirlem2  37609  poimirlem7  37614  poimirlem10  37617  poimirlem11  37618  areacirc  37700  aks4d1p1p7  42055  aks4d1p3  42059  aks4d1p5  42061  hashscontpow1  42102  sticksstones22  42149  aks6d1c6lem4  42154  aks5lem8  42182  readvrec  42343  frlmvscadiccat  42487  rencldnfilem  42801  irrapxlem1  42803  monotoddzzfi  42924  sqrtcvallem1  43613  reabsifneg  43614  reabsifpos  43616  radcnvrat  44296  reclt0d  45376  reclt0  45380  sqrlearg  45544  dvnxpaek  45933  volico  45974  sublevolico  45975  fourierdlem12  46110  fourierdlem42  46140  elaa2lem  46224  iundjiun  46451  hoidmvval0  46578  hoidmv1lelem2  46583  hoidmv1lelem3  46584  hoidmvlelem4  46589  hspdifhsp  46607  volico2  46632  ovolval2lem  46634  vonioo  46673  smfconst  46740  fzopredsuc  47317  stgoldbwt  47770  nnsum3primesle9  47788  bgoldbtbndlem1  47799  ssnn0ssfz  48330