Theorem lenltd 11329

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∈ wcel 2142   class class class wbr 5100  ℝcr 11072   < clt 11216   ≤ cle 11217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5653  df-cnv 5655  df-xr 11220  df-le 11222

This theorem is referenced by:  ltnsymd  11332  nltled  11333  lensymd  11334  leadd1  11655  leord1  11714  lediv1  12057  lemuldiv  12072  lerec  12075  le2msq  12092  suprleub  12158  infregelb  12176  suprfinzcl  12687  uzinfi  12929  rpnnen1lem5  12982  nn0disj  13649  fleqceilz  13864  modsumfzodifsn  13957  addmodlteq  13959  leexp2  14184  expnngt1  14254  hashf1  14470  swrdccatin2  14742  isercoll  15695  ruclem3  16265  sadcaddlem  16491  pcfac  16935  sylow1lem1  19638  fvmptnn04if  22909  chfacfisf  22914  chfacfisfcpmat  22915  ivthlem2  25514  ioorcl2  25634  itg1ge0a  25773  mbfi1fseqlem4  25780  itg2monolem1  25812  itg2cnlem1  25823  mdegmullem  26138  quotcan  26373  logdivle  26687  cxple  26760  gausslemma2dlem1a  27429  padicabv  27694  upgrewlkle2  29807  pthdlem1  29966  ssnnssfz  32989  smattr  34096  smatbl  34097  smatbr  34098  esumpcvgval  34375  eulerpartlems  34657  dstfrvunirn  34772  ballotlemodife  34795  erdszelem7  35547  erdszelem8  35548  unbdqndv2lem1  36947  poimirlem2  38121  poimirlem7  38126  poimirlem10  38129  poimirlem11  38130  areacirc  38212  aks4d1p1p7  42691  aks4d1p3  42695  aks4d1p5  42697  hashscontpow1  42738  sticksstones22  42785  aks6d1c6lem4  42790  aks5lem8  42818  readvrec  42971  frlmvscadiccat  43128  rencldnfilem  43397  irrapxlem1  43399  monotoddzzfi  43519  sqrtcvallem1  44207  reabsifneg  44208  reabsifpos  44210  radcnvrat  44890  reclt0d  45962  reclt0  45966  sqrlearg  46129  dvnxpaek  46516  volico  46557  sublevolico  46558  fourierdlem12  46693  fourierdlem42  46723  elaa2lem  46807  iundjiun  47034  hoidmvval0  47161  hoidmv1lelem2  47166  hoidmv1lelem3  47167  hoidmvlelem4  47172  hspdifhsp  47190  volico2  47215  ovolval2lem  47217  vonioo  47256  smfconst  47323  fzopredsuc  47918  stgoldbwt  48398  nnsum3primesle9  48416  bgoldbtbndlem1  48427  ssnn0ssfz  48971