Theorem lenltd 11283

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∈ wcel 2119   class class class wbr 5072  ℝcr 11028   < clt 11170   ≤ cle 11171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-cnv 5626  df-xr 11174  df-le 11176

This theorem is referenced by:  ltnsymd  11286  nltled  11287  lensymd  11288  leadd1  11609  leord1  11668  lediv1  12012  lemuldiv  12027  lerec  12030  le2msq  12047  suprleub  12113  infregelb  12131  suprfinzcl  12634  uzinfi  12869  rpnnen1lem5  12922  nn0disj  13589  fleqceilz  13804  modsumfzodifsn  13897  addmodlteq  13899  leexp2  14124  expnngt1  14194  hashf1  14410  swrdccatin2  14682  isercoll  15621  ruclem3  16191  sadcaddlem  16417  pcfac  16861  sylow1lem1  19564  fvmptnn04if  22832  chfacfisf  22837  chfacfisfcpmat  22838  ivthlem2  25437  ioorcl2  25557  itg1ge0a  25696  mbfi1fseqlem4  25703  itg2monolem1  25735  itg2cnlem1  25746  mdegmullem  26061  quotcan  26293  logdivle  26604  cxple  26677  gausslemma2dlem1a  27346  padicabv  27611  upgrewlkle2  29693  pthdlem1  29852  ssnnssfz  32879  smattr  33983  smatbl  33984  smatbr  33985  esumpcvgval  34262  eulerpartlems  34544  dstfrvunirn  34659  ballotlemodife  34682  erdszelem7  35425  erdszelem8  35426  unbdqndv2lem1  36815  poimirlem2  37989  poimirlem7  37994  poimirlem10  37997  poimirlem11  37998  areacirc  38080  aks4d1p1p7  42559  aks4d1p3  42563  aks4d1p5  42565  hashscontpow1  42606  sticksstones22  42653  aks6d1c6lem4  42658  aks5lem8  42686  readvrec  42839  frlmvscadiccat  42996  rencldnfilem  43265  irrapxlem1  43267  monotoddzzfi  43387  sqrtcvallem1  44075  reabsifneg  44076  reabsifpos  44078  radcnvrat  44758  reclt0d  45831  reclt0  45835  sqrlearg  45998  dvnxpaek  46385  volico  46426  sublevolico  46427  fourierdlem12  46562  fourierdlem42  46592  elaa2lem  46676  iundjiun  46903  hoidmvval0  47030  hoidmv1lelem2  47035  hoidmv1lelem3  47036  hoidmvlelem4  47041  hspdifhsp  47059  volico2  47084  ovolval2lem  47086  vonioo  47125  smfconst  47192  fzopredsuc  47787  stgoldbwt  48267  nnsum3primesle9  48285  bgoldbtbndlem1  48296  ssnn0ssfz  48840