Theorem lenltd 11406

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∈ wcel 2098   class class class wbr 5152  ℝcr 11153   < clt 11294   ≤ cle 11295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pr 5432

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3949  df-un 3951  df-ss 3963  df-nul 4325  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-br 5153  df-opab 5215  df-xp 5687  df-cnv 5689  df-xr 11298  df-le 11300

This theorem is referenced by:  ltnsymd  11409  nltled  11410  lensymd  11411  leadd1  11728  leord1  11787  lediv1  12126  lemuldiv  12141  lerec  12144  le2msq  12161  suprleub  12227  infregelb  12245  suprfinzcl  12723  uzinfi  12959  rpnnen1lem5  13012  nn0disj  13666  fleqceilz  13869  modsumfzodifsn  13959  addmodlteq  13961  leexp2  14185  expnngt1  14253  hashf1  14471  swrdccatin2  14732  isercoll  15667  ruclem3  16230  sadcaddlem  16452  pcfac  16896  sylow1lem1  19591  fvmptnn04if  22834  chfacfisf  22839  chfacfisfcpmat  22840  ivthlem2  25464  ioorcl2  25584  itg1ge0a  25724  mbfi1fseqlem4  25731  itg2monolem1  25763  itg2cnlem1  25774  mdegmullem  26097  quotcan  26329  logdivle  26641  cxple  26714  gausslemma2dlem1a  27386  padicabv  27651  upgrewlkle2  29535  pthdlem1  29695  ssnnssfz  32678  smattr  33570  smatbl  33571  smatbr  33572  esumpcvgval  33867  eulerpartlems  34150  dstfrvunirn  34264  ballotlemodife  34287  erdszelem7  34977  erdszelem8  34978  unbdqndv2lem1  36160  poimirlem2  37271  poimirlem7  37276  poimirlem10  37279  poimirlem11  37280  areacirc  37362  aks4d1p1p7  41721  aks4d1p3  41725  aks4d1p5  41727  hashscontpow1  41767  sticksstones22  41814  aks6d1c6lem4  41819  metakunt7  41840  metakunt12  41845  metakunt22  41855  metakunt28  41861  metakunt29  41862  metakunt30  41863  frlmvscadiccat  41927  rencldnfilem  42414  irrapxlem1  42416  monotoddzzfi  42537  sqrtcvallem1  43235  reabsifneg  43236  reabsifpos  43238  radcnvrat  43925  reclt0d  44939  reclt0  44943  sqrlearg  45108  dvnxpaek  45500  volico  45541  sublevolico  45542  fourierdlem12  45677  fourierdlem42  45707  elaa2lem  45791  iundjiun  46018  hoidmvval0  46145  hoidmv1lelem2  46150  hoidmv1lelem3  46151  hoidmvlelem4  46156  hspdifhsp  46174  volico2  46199  ovolval2lem  46201  vonioo  46240  smfconst  46307  fzopredsuc  46873  stgoldbwt  47285  nnsum3primesle9  47303  bgoldbtbndlem1  47314  ssnn0ssfz  47665