Theorem ltnlei 10321

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

Syntax hints:  ¬ wn 3   ↔ wb 196   ∈ wcel 2127   class class class wbr 4792  ℝcr 10098   < clt 10237   ≤ cle 10238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pr 5043

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-br 4793  df-opab 4853  df-xp 5260  df-cnv 5262  df-xr 10241  df-le 10243

This theorem is referenced by:  letrii  10325  nn0ge2m1nn  11523  zgt1rpn0n1  12035  0nelfz1  12524  fzpreddisj  12554  hashnn0n0nn  13343  hashge2el2dif  13425  n2dvds1  15277  divalglem5  15293  divalglem6  15294  sadcadd  15353  strlemor1OLD  16142  htpycc  22951  pco1  22986  pcohtpylem  22990  pcopt  22993  pcopt2  22994  pcoass  22995  pcorevlem  22997  vitalilem5  23551  vieta1lem2  24236  ppiltx  25073  ppiublem1  25097  chtub  25107  axlowdimlem16  26007  axlowdim  26011  lfgrnloop  26190  lfuhgr1v0e  26316  lfgrwlkprop  26765  ballotlem2  30830  subfacp1lem1  31439  subfacp1lem5  31444  bcneg1  31900  poimirlem9  33700  poimirlem16  33707  poimirlem17  33708  poimirlem19  33710  poimirlem20  33711  poimirlem22  33713  fdc  33823  pellexlem6  37869  jm2.23  38034