Theorem lenltd 10639

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∈ wcel 2083   class class class wbr 4968  ℝcr 10389   < clt 10528   ≤ cle 10529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pr 5228

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-br 4969  df-opab 5031  df-xp 5456  df-cnv 5458  df-xr 10532  df-le 10534

This theorem is referenced by:  ltnsymd  10642  nltled  10643  lensymd  10644  leadd1  10962  leord1  11021  lediv1  11359  lemuldiv  11374  lerec  11377  le2msq  11394  suprleub  11461  infregelb  11479  suprfinzcl  11951  uzinfi  12181  rpnnen1lem5  12234  nn0disj  12877  fleqceilz  13076  modsumfzodifsn  13166  addmodlteq  13168  leexp2  13389  expnngt1  13456  hashf1  13667  ccatsymb  13784  swrdccatin2  13931  isercoll  14862  ruclem3  15423  sadcaddlem  15643  pcfac  16068  sylow1lem1  18457  fvmptnn04if  21145  chfacfisf  21150  chfacfisfcpmat  21151  ivthlem2  23740  ioorcl2  23860  itg1ge0a  23999  mbfi1fseqlem4  24006  itg2monolem1  24038  itg2cnlem1  24049  mdegmullem  24359  quotcan  24585  logdivle  24890  cxple  24963  gausslemma2dlem1a  25627  padicabv  25892  upgrewlkle2  27075  pthdlem1  27233  ssnnssfz  30194  smattr  30675  smatbl  30676  smatbr  30677  esumpcvgval  30950  eulerpartlems  31231  dstfrvunirn  31345  ballotlemodife  31368  erdszelem7  32054  erdszelem8  32055  unbdqndv2lem1  33459  poimirlem2  34446  poimirlem7  34451  poimirlem10  34454  poimirlem11  34455  areacirc  34539  frlmvscadiccat  38693  rencldnfilem  38923  irrapxlem1  38925  monotoddzzfi  39045  radcnvrat  40205  reclt0d  41220  reclt0  41225  sqrlearg  41392  dvnxpaek  41790  volico  41832  sublevolico  41833  fourierdlem12  41968  fourierdlem42  41998  elaa2lem  42082  iundjiun  42306  hoidmvval0  42433  hoidmv1lelem2  42438  hoidmv1lelem3  42439  hoidmvlelem4  42444  hspdifhsp  42462  volico2  42487  ovolval2lem  42489  vonioo  42528  smfconst  42590  fzopredsuc  43061  stgoldbwt  43445  nnsum3primesle9  43463  bgoldbtbndlem1  43474  ssnn0ssfz  43897