Theorem lenltd 11436

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2108   class class class wbr 5166  ℝcr 11183   < clt 11324   ≤ cle 11325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-cnv 5708  df-xr 11328  df-le 11330

This theorem is referenced by:  ltnsymd  11439  nltled  11440  lensymd  11441  leadd1  11758  leord1  11817  lediv1  12160  lemuldiv  12175  lerec  12178  le2msq  12195  suprleub  12261  infregelb  12279  suprfinzcl  12757  uzinfi  12993  rpnnen1lem5  13046  nn0disj  13701  fleqceilz  13905  modsumfzodifsn  13995  addmodlteq  13997  leexp2  14221  expnngt1  14290  hashf1  14506  swrdccatin2  14777  isercoll  15716  ruclem3  16281  sadcaddlem  16503  pcfac  16946  sylow1lem1  19640  fvmptnn04if  22876  chfacfisf  22881  chfacfisfcpmat  22882  ivthlem2  25506  ioorcl2  25626  itg1ge0a  25766  mbfi1fseqlem4  25773  itg2monolem1  25805  itg2cnlem1  25816  mdegmullem  26137  quotcan  26369  logdivle  26682  cxple  26755  gausslemma2dlem1a  27427  padicabv  27692  upgrewlkle2  29642  pthdlem1  29802  ssnnssfz  32792  smattr  33745  smatbl  33746  smatbr  33747  esumpcvgval  34042  eulerpartlems  34325  dstfrvunirn  34439  ballotlemodife  34462  erdszelem7  35165  erdszelem8  35166  unbdqndv2lem1  36475  poimirlem2  37582  poimirlem7  37587  poimirlem10  37590  poimirlem11  37591  areacirc  37673  aks4d1p1p7  42031  aks4d1p3  42035  aks4d1p5  42037  hashscontpow1  42078  sticksstones22  42125  aks6d1c6lem4  42130  aks5lem8  42158  metakunt7  42168  metakunt12  42173  metakunt22  42183  metakunt28  42189  metakunt29  42190  metakunt30  42191  frlmvscadiccat  42461  rencldnfilem  42776  irrapxlem1  42778  monotoddzzfi  42899  sqrtcvallem1  43593  reabsifneg  43594  reabsifpos  43596  radcnvrat  44283  reclt0d  45302  reclt0  45306  sqrlearg  45471  dvnxpaek  45863  volico  45904  sublevolico  45905  fourierdlem12  46040  fourierdlem42  46070  elaa2lem  46154  iundjiun  46381  hoidmvval0  46508  hoidmv1lelem2  46513  hoidmv1lelem3  46514  hoidmvlelem4  46519  hspdifhsp  46537  volico2  46562  ovolval2lem  46564  vonioo  46603  smfconst  46670  fzopredsuc  47238  stgoldbwt  47650  nnsum3primesle9  47668  bgoldbtbndlem1  47679  ssnn0ssfz  48074