Theorem ltnlei 11258

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

Syntax hints:  ¬ wn 3   ↔ wb 207   ∈ wcel 2119   class class class wbr 5072  ℝcr 11028   < clt 11170   ≤ cle 11171

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-cnv 5626  df-xr 11174  df-le 11176

This theorem is referenced by:  letrii  11262  nn0ge2m1nn  12498  0nelfz1  13488  fzpreddisj  13518  hashnn0n0nn  14344  hashge2el2dif  14433  hash3tpde  14446  divalglem5  16357  divalglem6  16358  sadcadd  16418  htpycc  24965  pco1  25000  pcohtpylem  25004  pcopt  25007  pcopt2  25008  pcoass  25009  pcorevlem  25011  vitalilem5  25597  vieta1lem2  26295  ppiltx  27158  ppiublem1  27183  chtub  27193  axlowdimlem16  29044  axlowdim  29048  lfgrnloop  29212  lfuhgr1v0e  29341  lfgrwlkprop  29772  ballotlem2  34673  subfacp1lem1  35407  subfacp1lem5  35412  bcneg1  35964  poimirlem9  37996  poimirlem16  38003  poimirlem17  38004  poimirlem19  38006  poimirlem20  38007  poimirlem22  38009  fdc  38112  pellexlem6  43279  jm2.23  43441  nprmdvdsfacm1lem2  48099