Theorem lenltd 11373

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ wcel 2146   class class class wbr 5111  ℝcr 11116   < clt 11260   ≤ cle 11261

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-cnv 5671  df-xr 11264  df-le 11266

This theorem is used by:  ltnsymd  11376  nltled  11377  lensymd  11378  leadd1  11699  leord1  11758  lediv1  12097  lemuldiv  12112  lerec  12115  le2msq  12132  suprleub  12198  infregelb  12216  suprfinzcl  12728  uzinfi  12970  rpnnen1lem5  13023  nn0disj  13691  fleqceilz  13907  modsumfzodifsn  14000  addmodlteq  14002  leexp2  14227  expnngt1  14297  hashf1  14514  swrdccatin2  14790  isercoll  15745  ruclem3  16313  sadcaddlem  16539  pcfac  16983  sylow1lem1  19714  fvmptnn04if  23058  chfacfisf  23063  chfacfisfcpmat  23064  ivthlem2  25664  ioorcl2  25784  itg1ge0a  25923  mbfi1fseqlem4  25930  itg2monolem1  25962  itg2cnlem1  25973  mdegmullem  26288  quotcan  26523  logdivle  26840  cxple  26913  gausslemma2dlem1a  27582  padicabv  27847  upgrewlkle2  30016  pthdlem1  30181  ssnnssfz  33204  smattr  34255  smatbl  34256  smatbr  34257  esumpcvgval  34534  eulerpartlems  34817  dstfrvunirn  34932  ballotlemodife  34955  erdszelem7  35728  erdszelem8  35729  unbdqndv2lem1  37157  poimirlem2  38332  poimirlem7  38337  poimirlem10  38340  poimirlem11  38341  areacirc  38423  aks4d1p1p7  42901  aks4d1p3  42905  aks4d1p5  42907  hashscontpow1  42948  sticksstones22  42995  aks6d1c6lem4  43000  aks5lem8  43028  readvrec  43183  frlmvscadiccat  43340  rencldnfilem  43607  irrapxlem1  43609  monotoddzzfi  43729  sqrtcvallem1  44417  reabsifneg  44418  reabsifpos  44420  radcnvrat  45084  reclt0d  46162  reclt0  46166  sqrlearg  46329  dvnxpaek  46716  volico  46757  sublevolico  46758  fourierdlem12  46893  fourierdlem42  46923  elaa2lem  47007  iundjiun  47234  hoidmvval0  47361  hoidmv1lelem2  47366  hoidmv1lelem3  47367  hoidmvlelem4  47372  hspdifhsp  47390  volico2  47415  ovolval2lem  47417  vonioo  47456  smfconst  47523  fzopredsuc  48121  stgoldbwt  48601  nnsum3primesle9  48619  bgoldbtbndlem1  48630  ssnn0ssfz  49188