Theorem lenltd 11262

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2109   class class class wbr 5092  ℝcr 11008   < clt 11149   ≤ cle 11150

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 5235  ax-nul 5245  ax-pr 5371

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-xp 5625  df-cnv 5627  df-xr 11153  df-le 11155

This theorem is referenced by:  ltnsymd  11265  nltled  11266  lensymd  11267  leadd1  11588  leord1  11647  lediv1  11990  lemuldiv  12005  lerec  12008  le2msq  12025  suprleub  12091  infregelb  12109  suprfinzcl  12590  uzinfi  12829  rpnnen1lem5  12882  nn0disj  13547  fleqceilz  13758  modsumfzodifsn  13851  addmodlteq  13853  leexp2  14078  expnngt1  14148  hashf1  14364  swrdccatin2  14635  isercoll  15575  ruclem3  16142  sadcaddlem  16368  pcfac  16811  sylow1lem1  19477  fvmptnn04if  22734  chfacfisf  22739  chfacfisfcpmat  22740  ivthlem2  25351  ioorcl2  25471  itg1ge0a  25610  mbfi1fseqlem4  25617  itg2monolem1  25649  itg2cnlem1  25660  mdegmullem  25981  quotcan  26215  logdivle  26529  cxple  26602  gausslemma2dlem1a  27274  padicabv  27539  upgrewlkle2  29552  pthdlem1  29711  ssnnssfz  32730  smattr  33766  smatbl  33767  smatbr  33768  esumpcvgval  34045  eulerpartlems  34328  dstfrvunirn  34443  ballotlemodife  34466  erdszelem7  35174  erdszelem8  35175  unbdqndv2lem1  36487  poimirlem2  37606  poimirlem7  37611  poimirlem10  37614  poimirlem11  37615  areacirc  37697  aks4d1p1p7  42051  aks4d1p3  42055  aks4d1p5  42057  hashscontpow1  42098  sticksstones22  42145  aks6d1c6lem4  42150  aks5lem8  42178  readvrec  42339  frlmvscadiccat  42483  rencldnfilem  42797  irrapxlem1  42799  monotoddzzfi  42919  sqrtcvallem1  43608  reabsifneg  43609  reabsifpos  43611  radcnvrat  44291  reclt0d  45370  reclt0  45374  sqrlearg  45538  dvnxpaek  45927  volico  45968  sublevolico  45969  fourierdlem12  46104  fourierdlem42  46134  elaa2lem  46218  iundjiun  46445  hoidmvval0  46572  hoidmv1lelem2  46577  hoidmv1lelem3  46578  hoidmvlelem4  46583  hspdifhsp  46601  volico2  46626  ovolval2lem  46628  vonioo  46667  smfconst  46734  fzopredsuc  47311  stgoldbwt  47764  nnsum3primesle9  47782  bgoldbtbndlem1  47793  ssnn0ssfz  48337