Theorem ltnlei 11331

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 11330	. 2 ⊢ (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)
4	3	con2bii 360	1 ⊢ (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 209   ∈ wcel 2149   class class class wbr 5113  ℝcr 11099   < clt 11243   ≤ cle 11244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-xp 5668  df-cnv 5670  df-xr 11247  df-le 11249

This theorem is referenced by:  letrii  11335  nn0ge2m1nn  12574  0nelfz1  13571  fzpreddisj  13601  hashnn0n0nn  14427  hashge2el2dif  14517  hash3tpde  14530  divalglem5  16455  divalglem6  16456  sadcadd  16516  htpycc  25108  pco1  25143  pcohtpylem  25147  pcopt  25150  pcopt2  25151  pcoass  25152  pcorevlem  25154  vitalilem5  25740  vieta1lem2  26441  ppiltx  27307  ppiublem1  27332  chtub  27342  axlowdimlem16  29248  axlowdim  29252  lfgrnloop  29416  lfuhgr1v0e  29545  lfgrwlkprop  29976  ballotlem2  34824  subfacp1lem1  35570  subfacp1lem5  35575  bcneg1  36127  poimirlem9  38168  poimirlem16  38175  poimirlem17  38176  poimirlem19  38178  poimirlem20  38179  poimirlem22  38181  fdc  38284  pellexlem6  43453  jm2.23  43615  nprmdvdsfacm1lem2  48262