Theorem lenltd 11466

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ wcel 2146   class class class wbr 5105  ℝcr 11209   < clt 11353   ≤ cle 11354

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5251  ax-pr 5394

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-br 5106  df-opab 5170  df-xp 5660  df-cnv 5662  df-xr 11357  df-le 11359

This theorem is used by:  ltnsymd  11469  nltled  11470  lensymd  11471  leadd1  11794  leord1  11853  lediv1  12192  lemuldiv  12207  lerec  12210  le2msq  12227  suprleub  12293  infregelb  12311  suprfinzcl  12823  uzinfi  13065  rpnnen1lem5  13119  nn0disj  13788  fleqceilz  14004  modsumfzodifsn  14097  addmodlteq  14099  leexp2  14324  expnngt1  14395  hashf1  14612  swrdccatin2  14889  isercoll  15847  ruclem3  16413  sadcaddlem  16639  pcfac  17089  sylow1lem1  19824  fvmptnn04if  23179  chfacfisf  23184  chfacfisfcpmat  23185  ivthlem2  25785  ioorcl2  25905  itg1ge0a  26044  mbfi1fseqlem4  26051  itg2monolem1  26083  itg2cnlem1  26094  mdegmullem  26408  quotcan  26644  logdivle  26962  cxple  27035  gausslemma2dlem1a  27704  padicabv  27969  upgrewlkle2  30199  pthdlem1  30364  ssnnssfz  33432  smattr  34484  smatbl  34485  smatbr  34486  esumpcvgval  34763  eulerpartlems  35045  dstfrvunirn  35160  ballotlemodife  35183  erdszelem7  36083  erdszelem8  36084  unbdqndv2lem1  37502  poimirlem2  38680  poimirlem7  38685  poimirlem10  38688  poimirlem11  38689  areacirc  38771  aks4d1p1p7  43264  aks4d1p3  43268  aks4d1p5  43270  hashscontpow1  43311  sticksstones22  43358  aks6d1c6lem4  43363  aks5lem8  43391  readvrec  43553  frlmvscadiccat  43713  rencldnfilem  43967  irrapxlem1  43969  monotoddzzfi  44089  sqrtcvallem1  44771  reabsifneg  44772  reabsifpos  44774  radcnvrat  45438  reclt0d  46537  reclt0  46541  sqrlearg  46704  dvnxpaek  47091  volico  47132  sublevolico  47133  fourierdlem12  47268  fourierdlem42  47298  elaa2lem  47382  iundjiun  47609  hoidmvval0  47736  hoidmv1lelem2  47741  hoidmv1lelem3  47742  hoidmvlelem4  47747  hspdifhsp  47765  volico2  47790  ovolval2lem  47792  vonioo  47831  smfconst  47898  fzopredsuc  48533  stgoldbwt  49013  nnsum3primesle9  49031  bgoldbtbndlem1  49042  ssnn0ssfz  49600