Theorem lenltd 11456

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ wcel 2145   class class class wbr 5103  ℝcr 11199   < clt 11343   ≤ cle 11344

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-cnv 5659  df-xr 11347  df-le 11349

This theorem is used by:  ltnsymd  11459  nltled  11460  lensymd  11461  leadd1  11784  leord1  11843  lediv1  12182  lemuldiv  12197  lerec  12200  le2msq  12217  suprleub  12283  infregelb  12301  suprfinzcl  12813  uzinfi  13055  rpnnen1lem5  13109  nn0disj  13778  fleqceilz  13994  modsumfzodifsn  14087  addmodlteq  14089  leexp2  14314  expnngt1  14385  hashf1  14602  swrdccatin2  14878  isercoll  15835  ruclem3  16401  sadcaddlem  16627  pcfac  17077  sylow1lem1  19812  fvmptnn04if  23167  chfacfisf  23172  chfacfisfcpmat  23173  ivthlem2  25773  ioorcl2  25893  itg1ge0a  26032  mbfi1fseqlem4  26039  itg2monolem1  26071  itg2cnlem1  26082  mdegmullem  26396  quotcan  26632  logdivle  26950  cxple  27023  gausslemma2dlem1a  27692  padicabv  27957  upgrewlkle2  30187  pthdlem1  30352  ssnnssfz  33379  smattr  34431  smatbl  34432  smatbr  34433  esumpcvgval  34710  eulerpartlems  34992  dstfrvunirn  35107  ballotlemodife  35130  erdszelem7  35962  erdszelem8  35963  unbdqndv2lem1  37375  poimirlem2  38540  poimirlem7  38545  poimirlem10  38548  poimirlem11  38549  areacirc  38631  aks4d1p1p7  43124  aks4d1p3  43128  aks4d1p5  43130  hashscontpow1  43171  sticksstones22  43218  aks6d1c6lem4  43223  aks5lem8  43251  readvrec  43413  frlmvscadiccat  43573  rencldnfilem  43826  irrapxlem1  43828  monotoddzzfi  43948  sqrtcvallem1  44630  reabsifneg  44631  reabsifpos  44633  radcnvrat  45297  reclt0d  46397  reclt0  46401  sqrlearg  46564  dvnxpaek  46951  volico  46992  sublevolico  46993  fourierdlem12  47128  fourierdlem42  47158  elaa2lem  47242  iundjiun  47469  hoidmvval0  47596  hoidmv1lelem2  47601  hoidmv1lelem3  47602  hoidmvlelem4  47607  hspdifhsp  47625  volico2  47650  ovolval2lem  47652  vonioo  47691  smfconst  47758  fzopredsuc  48393  stgoldbwt  48873  nnsum3primesle9  48891  bgoldbtbndlem1  48902  ssnn0ssfz  49460