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  35170  erdszelem8  35171  unbdqndv2lem1  36483  poimirlem2  37602  poimirlem7  37607  poimirlem10  37610  poimirlem11  37611  areacirc  37693  aks4d1p1p7  42047  aks4d1p3  42051  aks4d1p5  42053  hashscontpow1  42094  sticksstones22  42141  aks6d1c6lem4  42146  aks5lem8  42174  readvrec  42335  frlmvscadiccat  42479  rencldnfilem  42793  irrapxlem1  42795  monotoddzzfi  42915  sqrtcvallem1  43604  reabsifneg  43605  reabsifpos  43607  radcnvrat  44287  reclt0d  45366  reclt0  45370  sqrlearg  45534  dvnxpaek  45923  volico  45964  sublevolico  45965  fourierdlem12  46100  fourierdlem42  46130  elaa2lem  46214  iundjiun  46441  hoidmvval0  46568  hoidmv1lelem2  46573  hoidmv1lelem3  46574  hoidmvlelem4  46579  hspdifhsp  46597  volico2  46622  ovolval2lem  46624  vonioo  46663  smfconst  46730  fzopredsuc  47307  stgoldbwt  47760  nnsum3primesle9  47778  bgoldbtbndlem1  47789  ssnn0ssfz  48333