Theorem lenltd 11130

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∈ wcel 2107   class class class wbr 5075  ℝcr 10879   < clt 11018   ≤ cle 11019

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-xp 5596  df-cnv 5598  df-xr 11022  df-le 11024

This theorem is referenced by:  ltnsymd  11133  nltled  11134  lensymd  11135  leadd1  11452  leord1  11511  lediv1  11849  lemuldiv  11864  lerec  11867  le2msq  11884  suprleub  11950  infregelb  11968  suprfinzcl  12445  uzinfi  12677  rpnnen1lem5  12730  nn0disj  13381  fleqceilz  13583  modsumfzodifsn  13673  addmodlteq  13675  leexp2  13898  expnngt1  13965  hashf1  14180  swrdccatin2  14451  isercoll  15388  ruclem3  15951  sadcaddlem  16173  pcfac  16609  sylow1lem1  19212  fvmptnn04if  22007  chfacfisf  22012  chfacfisfcpmat  22013  ivthlem2  24625  ioorcl2  24745  itg1ge0a  24885  mbfi1fseqlem4  24892  itg2monolem1  24924  itg2cnlem1  24935  mdegmullem  25252  quotcan  25478  logdivle  25786  cxple  25859  gausslemma2dlem1a  26522  padicabv  26787  upgrewlkle2  27982  pthdlem1  28143  ssnnssfz  31117  smattr  31758  smatbl  31759  smatbr  31760  esumpcvgval  32055  eulerpartlems  32336  dstfrvunirn  32450  ballotlemodife  32473  erdszelem7  33168  erdszelem8  33169  unbdqndv2lem1  34698  poimirlem2  35788  poimirlem7  35793  poimirlem10  35796  poimirlem11  35797  areacirc  35879  aks4d1p1p7  40089  aks4d1p3  40093  aks4d1p5  40095  sticksstones22  40131  metakunt7  40138  metakunt12  40143  metakunt22  40153  metakunt28  40159  metakunt29  40160  metakunt30  40161  frlmvscadiccat  40244  rencldnfilem  40649  irrapxlem1  40651  monotoddzzfi  40771  sqrtcvallem1  41246  reabsifneg  41247  reabsifpos  41249  radcnvrat  41939  reclt0d  42933  reclt0  42938  sqrlearg  43098  dvnxpaek  43490  volico  43531  sublevolico  43532  fourierdlem12  43667  fourierdlem42  43697  elaa2lem  43781  iundjiun  44005  hoidmvval0  44132  hoidmv1lelem2  44137  hoidmv1lelem3  44138  hoidmvlelem4  44143  hspdifhsp  44161  volico2  44186  ovolval2lem  44188  vonioo  44227  smfconst  44294  fzopredsuc  44826  stgoldbwt  45239  nnsum3primesle9  45257  bgoldbtbndlem1  45268  ssnn0ssfz  45696