Theorem ltnlei 11441

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∈ wcel 2146   class class class wbr 5105  ℝcr 11209   < clt 11353   ≤ cle 11354

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5251  ax-pr 5394

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-br 5106  df-opab 5170  df-xp 5660  df-cnv 5662  df-xr 11357  df-le 11359

This theorem is used by:  letrii  11445  nn0ge2m1nn  12686  0nelfz1  13686  fzpreddisj  13717  hashnn0n0nn  14545  hashge2el2dif  14635  hash3tpde  14648  divalglem5  16579  divalglem6  16580  sadcadd  16640  htpycc  25313  pco1  25348  pcohtpylem  25352  pcopt  25355  pcopt2  25356  pcoass  25357  pcorevlem  25359  vitalilem5  25945  vieta1lem2  26646  ppiltx  27516  ppiublem1  27541  chtub  27551  axlowdimlem16  29547  axlowdim  29551  lfgrnloop  29715  lfuhgr1v0e  29847  lfgrwlkprop  30282  ballotlem2  35174  subfacp1lem1  36065  subfacp1lem5  36070  bcneg1  36628  poimirlem9  38687  poimirlem16  38694  poimirlem17  38695  poimirlem19  38697  poimirlem20  38698  poimirlem22  38700  fdc  38819  pellexlem6  43981  jm2.23  44143  nprmdvdsfacm1lem2  48845