Theorem lenltd 10978

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ wcel 2110   class class class wbr 5053  ℝcr 10728   < clt 10867   ≤ cle 10868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054  df-opab 5116  df-xp 5557  df-cnv 5559  df-xr 10871  df-le 10873

This theorem is referenced by:  ltnsymd  10981  nltled  10982  lensymd  10983  leadd1  11300  leord1  11359  lediv1  11697  lemuldiv  11712  lerec  11715  le2msq  11732  suprleub  11798  infregelb  11816  suprfinzcl  12292  uzinfi  12524  rpnnen1lem5  12577  nn0disj  13228  fleqceilz  13427  modsumfzodifsn  13517  addmodlteq  13519  leexp2  13741  expnngt1  13808  hashf1  14023  swrdccatin2  14294  isercoll  15231  ruclem3  15794  sadcaddlem  16016  pcfac  16452  sylow1lem1  18987  fvmptnn04if  21746  chfacfisf  21751  chfacfisfcpmat  21752  ivthlem2  24349  ioorcl2  24469  itg1ge0a  24609  mbfi1fseqlem4  24616  itg2monolem1  24648  itg2cnlem1  24659  mdegmullem  24976  quotcan  25202  logdivle  25510  cxple  25583  gausslemma2dlem1a  26246  padicabv  26511  upgrewlkle2  27694  pthdlem1  27853  ssnnssfz  30828  smattr  31463  smatbl  31464  smatbr  31465  esumpcvgval  31758  eulerpartlems  32039  dstfrvunirn  32153  ballotlemodife  32176  erdszelem7  32872  erdszelem8  32873  unbdqndv2lem1  34426  poimirlem2  35516  poimirlem7  35521  poimirlem10  35524  poimirlem11  35525  areacirc  35607  aks4d1p1p7  39815  aks4d1p3  39819  sticksstones22  39846  metakunt7  39853  metakunt12  39858  metakunt22  39868  metakunt28  39874  metakunt29  39875  metakunt30  39876  frlmvscadiccat  39950  rencldnfilem  40345  irrapxlem1  40347  monotoddzzfi  40467  sqrtcvallem1  40915  reabsifneg  40916  reabsifpos  40918  radcnvrat  41605  reclt0d  42599  reclt0  42604  sqrlearg  42766  dvnxpaek  43158  volico  43199  sublevolico  43200  fourierdlem12  43335  fourierdlem42  43365  elaa2lem  43449  iundjiun  43673  hoidmvval0  43800  hoidmv1lelem2  43805  hoidmv1lelem3  43806  hoidmvlelem4  43811  hspdifhsp  43829  volico2  43854  ovolval2lem  43856  vonioo  43895  smfconst  43957  fzopredsuc  44488  stgoldbwt  44901  nnsum3primesle9  44919  bgoldbtbndlem1  44930  ssnn0ssfz  45358