Theorem lenltd 11277

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2113   class class class wbr 5096  ℝcr 11023   < clt 11164   ≤ cle 11165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-xp 5628  df-cnv 5630  df-xr 11168  df-le 11170

This theorem is referenced by:  ltnsymd  11280  nltled  11281  lensymd  11282  leadd1  11603  leord1  11662  lediv1  12005  lemuldiv  12020  lerec  12023  le2msq  12040  suprleub  12106  infregelb  12124  suprfinzcl  12604  uzinfi  12839  rpnnen1lem5  12892  nn0disj  13558  fleqceilz  13772  modsumfzodifsn  13865  addmodlteq  13867  leexp2  14092  expnngt1  14162  hashf1  14378  swrdccatin2  14650  isercoll  15589  ruclem3  16156  sadcaddlem  16382  pcfac  16825  sylow1lem1  19525  fvmptnn04if  22791  chfacfisf  22796  chfacfisfcpmat  22797  ivthlem2  25407  ioorcl2  25527  itg1ge0a  25666  mbfi1fseqlem4  25673  itg2monolem1  25705  itg2cnlem1  25716  mdegmullem  26037  quotcan  26271  logdivle  26585  cxple  26658  gausslemma2dlem1a  27330  padicabv  27595  upgrewlkle2  29629  pthdlem1  29788  ssnnssfz  32816  smattr  33905  smatbl  33906  smatbr  33907  esumpcvgval  34184  eulerpartlems  34466  dstfrvunirn  34581  ballotlemodife  34604  erdszelem7  35340  erdszelem8  35341  unbdqndv2lem1  36652  poimirlem2  37762  poimirlem7  37767  poimirlem10  37770  poimirlem11  37771  areacirc  37853  aks4d1p1p7  42267  aks4d1p3  42271  aks4d1p5  42273  hashscontpow1  42314  sticksstones22  42361  aks6d1c6lem4  42366  aks5lem8  42394  readvrec  42559  frlmvscadiccat  42703  rencldnfilem  43004  irrapxlem1  43006  monotoddzzfi  43126  sqrtcvallem1  43814  reabsifneg  43815  reabsifpos  43817  radcnvrat  44497  reclt0d  45573  reclt0  45577  sqrlearg  45741  dvnxpaek  46128  volico  46169  sublevolico  46170  fourierdlem12  46305  fourierdlem42  46335  elaa2lem  46419  iundjiun  46646  hoidmvval0  46773  hoidmv1lelem2  46778  hoidmv1lelem3  46779  hoidmvlelem4  46784  hspdifhsp  46802  volico2  46827  ovolval2lem  46829  vonioo  46868  smfconst  46935  fzopredsuc  47511  stgoldbwt  47964  nnsum3primesle9  47982  bgoldbtbndlem1  47993  ssnn0ssfz  48537