Theorem lenltd 11288

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∈ wcel 2121   class class class wbr 5074  ℝcr 11033   < clt 11175   ≤ cle 11176

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 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5220  ax-pr 5364

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075  df-opab 5137  df-xp 5626  df-cnv 5628  df-xr 11179  df-le 11181

This theorem is referenced by:  ltnsymd  11291  nltled  11292  lensymd  11293  leadd1  11614  leord1  11673  lediv1  12016  lemuldiv  12031  lerec  12034  le2msq  12051  suprleub  12117  infregelb  12135  suprfinzcl  12638  uzinfi  12873  rpnnen1lem5  12926  nn0disj  13593  fleqceilz  13808  modsumfzodifsn  13901  addmodlteq  13903  leexp2  14128  expnngt1  14198  hashf1  14414  swrdccatin2  14686  isercoll  15625  ruclem3  16195  sadcaddlem  16421  pcfac  16865  sylow1lem1  19567  fvmptnn04if  22835  chfacfisf  22840  chfacfisfcpmat  22841  ivthlem2  25440  ioorcl2  25560  itg1ge0a  25699  mbfi1fseqlem4  25706  itg2monolem1  25738  itg2cnlem1  25749  mdegmullem  26064  quotcan  26296  logdivle  26607  cxple  26680  gausslemma2dlem1a  27349  padicabv  27614  upgrewlkle2  29695  pthdlem1  29854  ssnnssfz  32881  smattr  33993  smatbl  33994  smatbr  33995  esumpcvgval  34272  eulerpartlems  34554  dstfrvunirn  34669  ballotlemodife  34692  erdszelem7  35438  erdszelem8  35439  unbdqndv2lem1  36828  poimirlem2  38002  poimirlem7  38007  poimirlem10  38010  poimirlem11  38011  areacirc  38093  aks4d1p1p7  42572  aks4d1p3  42576  aks4d1p5  42578  hashscontpow1  42619  sticksstones22  42666  aks6d1c6lem4  42671  aks5lem8  42699  readvrec  42852  frlmvscadiccat  43009  rencldnfilem  43278  irrapxlem1  43280  monotoddzzfi  43400  sqrtcvallem1  44088  reabsifneg  44089  reabsifpos  44091  radcnvrat  44771  reclt0d  45843  reclt0  45847  sqrlearg  46010  dvnxpaek  46397  volico  46438  sublevolico  46439  fourierdlem12  46574  fourierdlem42  46604  elaa2lem  46688  iundjiun  46915  hoidmvval0  47042  hoidmv1lelem2  47047  hoidmv1lelem3  47048  hoidmvlelem4  47053  hspdifhsp  47071  volico2  47096  ovolval2lem  47098  vonioo  47137  smfconst  47204  fzopredsuc  47799  stgoldbwt  48279  nnsum3primesle9  48297  bgoldbtbndlem1  48308  ssnn0ssfz  48852