Theorem lenltd 11381

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 11313	. 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 11124   < clt 11268   ≤ cle 11269

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 2732  ax-sep 5251  ax-pr 5398

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 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5661  df-cnv 5663  df-xr 11272  df-le 11274

This theorem is used by:  ltnsymd  11384  nltled  11385  lensymd  11386  leadd1  11707  leord1  11766  lediv1  12105  lemuldiv  12120  lerec  12123  le2msq  12140  suprleub  12206  infregelb  12224  suprfinzcl  12736  uzinfi  12978  rpnnen1lem5  13032  nn0disj  13700  fleqceilz  13916  modsumfzodifsn  14009  addmodlteq  14011  leexp2  14236  expnngt1  14306  hashf1  14523  swrdccatin2  14799  isercoll  15756  ruclem3  16322  sadcaddlem  16548  pcfac  16992  sylow1lem1  19726  fvmptnn04if  23075  chfacfisf  23080  chfacfisfcpmat  23081  ivthlem2  25681  ioorcl2  25801  itg1ge0a  25940  mbfi1fseqlem4  25947  itg2monolem1  25979  itg2cnlem1  25990  mdegmullem  26304  quotcan  26542  logdivle  26860  cxple  26933  gausslemma2dlem1a  27602  padicabv  27867  upgrewlkle2  30067  pthdlem1  30232  ssnnssfz  33259  smattr  34310  smatbl  34311  smatbr  34312  esumpcvgval  34589  eulerpartlems  34872  dstfrvunirn  34987  ballotlemodife  35010  erdszelem7  35777  erdszelem8  35778  unbdqndv2lem1  37207  poimirlem2  38372  poimirlem7  38377  poimirlem10  38380  poimirlem11  38381  areacirc  38463  aks4d1p1p7  42941  aks4d1p3  42945  aks4d1p5  42947  hashscontpow1  42988  sticksstones22  43035  aks6d1c6lem4  43040  aks5lem8  43068  readvrec  43238  frlmvscadiccat  43395  rencldnfilem  43662  irrapxlem1  43664  monotoddzzfi  43784  sqrtcvallem1  44472  reabsifneg  44473  reabsifpos  44475  radcnvrat  45139  reclt0d  46217  reclt0  46221  sqrlearg  46384  dvnxpaek  46771  volico  46812  sublevolico  46813  fourierdlem12  46948  fourierdlem42  46978  elaa2lem  47062  iundjiun  47289  hoidmvval0  47416  hoidmv1lelem2  47421  hoidmv1lelem3  47422  hoidmvlelem4  47427  hspdifhsp  47445  volico2  47470  ovolval2lem  47472  vonioo  47511  smfconst  47578  fzopredsuc  48213  stgoldbwt  48693  nnsum3primesle9  48711  bgoldbtbndlem1  48722  ssnn0ssfz  49280