Theorem lenltd 11405

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2106   class class class wbr 5148  ℝcr 11152   < clt 11293   ≤ cle 11294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-xp 5695  df-cnv 5697  df-xr 11297  df-le 11299

This theorem is referenced by:  ltnsymd  11408  nltled  11409  lensymd  11410  leadd1  11729  leord1  11788  lediv1  12131  lemuldiv  12146  lerec  12149  le2msq  12166  suprleub  12232  infregelb  12250  suprfinzcl  12730  uzinfi  12968  rpnnen1lem5  13021  nn0disj  13681  fleqceilz  13891  modsumfzodifsn  13982  addmodlteq  13984  leexp2  14208  expnngt1  14277  hashf1  14493  swrdccatin2  14764  isercoll  15701  ruclem3  16266  sadcaddlem  16491  pcfac  16933  sylow1lem1  19631  fvmptnn04if  22871  chfacfisf  22876  chfacfisfcpmat  22877  ivthlem2  25501  ioorcl2  25621  itg1ge0a  25761  mbfi1fseqlem4  25768  itg2monolem1  25800  itg2cnlem1  25811  mdegmullem  26132  quotcan  26366  logdivle  26679  cxple  26752  gausslemma2dlem1a  27424  padicabv  27689  upgrewlkle2  29639  pthdlem1  29799  ssnnssfz  32796  smattr  33760  smatbl  33761  smatbr  33762  esumpcvgval  34059  eulerpartlems  34342  dstfrvunirn  34456  ballotlemodife  34479  erdszelem7  35182  erdszelem8  35183  unbdqndv2lem1  36492  poimirlem2  37609  poimirlem7  37614  poimirlem10  37617  poimirlem11  37618  areacirc  37700  aks4d1p1p7  42056  aks4d1p3  42060  aks4d1p5  42062  hashscontpow1  42103  sticksstones22  42150  aks6d1c6lem4  42155  aks5lem8  42183  metakunt7  42193  metakunt12  42198  metakunt22  42208  metakunt28  42214  metakunt29  42215  metakunt30  42216  readvrec  42371  frlmvscadiccat  42493  rencldnfilem  42808  irrapxlem1  42810  monotoddzzfi  42931  sqrtcvallem1  43621  reabsifneg  43622  reabsifpos  43624  radcnvrat  44310  reclt0d  45337  reclt0  45341  sqrlearg  45506  dvnxpaek  45898  volico  45939  sublevolico  45940  fourierdlem12  46075  fourierdlem42  46105  elaa2lem  46189  iundjiun  46416  hoidmvval0  46543  hoidmv1lelem2  46548  hoidmv1lelem3  46549  hoidmvlelem4  46554  hspdifhsp  46572  volico2  46597  ovolval2lem  46599  vonioo  46638  smfconst  46705  fzopredsuc  47273  stgoldbwt  47701  nnsum3primesle9  47719  bgoldbtbndlem1  47730  ssnn0ssfz  48194