Theorem ltnlei 11088

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∈ wcel 2110   class class class wbr 5079  ℝcr 10863   < clt 11002   ≤ cle 11003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-br 5080  df-opab 5142  df-xp 5595  df-cnv 5597  df-xr 11006  df-le 11008

This theorem is referenced by:  letrii  11092  nn0ge2m1nn  12294  0nelfz1  13266  fzpreddisj  13296  hashnn0n0nn  14096  hashge2el2dif  14184  divalglem5  16096  divalglem6  16097  sadcadd  16155  htpycc  24133  pco1  24168  pcohtpylem  24172  pcopt  24175  pcopt2  24176  pcoass  24177  pcorevlem  24179  vitalilem5  24766  vieta1lem2  25461  ppiltx  26316  ppiublem1  26340  chtub  26350  axlowdimlem16  27315  axlowdim  27319  lfgrnloop  27485  lfuhgr1v0e  27611  lfgrwlkprop  28044  ballotlem2  32443  subfacp1lem1  33129  subfacp1lem5  33134  bcneg1  33690  poimirlem9  35774  poimirlem16  35781  poimirlem17  35782  poimirlem19  35784  poimirlem20  35785  poimirlem22  35787  fdc  35891  pellexlem6  40645  jm2.23  40807