Theorem ltnlei 11290

Description: 'Less than' in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.)

Hypotheses

Ref	Expression
lt.1	⊢ 𝐴 ∈ ℝ
lt.2	⊢ 𝐵 ∈ ℝ

Assertion

Ref	Expression
ltnlei	⊢ (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)

Proof of Theorem ltnlei

Step	Hyp	Ref	Expression
1		lt.2	. . 3 ⊢ 𝐵 ∈ ℝ
2		lt.1	. . 3 ⊢ 𝐴 ∈ ℝ
3	1, 2	lenlti 11289	. 2 ⊢ (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)
4	3	con2bii 359	1 ⊢ (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 208   ∈ wcel 2132   class class class wbr 5090  ℝcr 11058   < clt 11202   ≤ cle 11203

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-sep 5236  ax-pr 5380

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-br 5091  df-opab 5153  df-xp 5642  df-cnv 5644  df-xr 11206  df-le 11208

This theorem is referenced by:  letrii  11294  nn0ge2m1nn  12537  0nelfz1  13534  fzpreddisj  13564  hashnn0n0nn  14390  hashge2el2dif  14479  hash3tpde  14492  divalglem5  16403  divalglem6  16404  sadcadd  16464  htpycc  25011  pco1  25046  pcohtpylem  25050  pcopt  25053  pcopt2  25054  pcoass  25055  pcorevlem  25057  vitalilem5  25643  vieta1lem2  26341  ppiltx  27207  ppiublem1  27232  chtub  27242  axlowdimlem16  29093  axlowdim  29097  lfgrnloop  29261  lfuhgr1v0e  29390  lfgrwlkprop  29821  ballotlem2  34730  subfacp1lem1  35467  subfacp1lem5  35472  bcneg1  36024  poimirlem9  38066  poimirlem16  38073  poimirlem17  38074  poimirlem19  38076  poimirlem20  38077  poimirlem22  38079  fdc  38182  pellexlem6  43349  jm2.23  43511  nprmdvdsfacm1lem2  48168