Theorem ltnlei 11348

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∈ wcel 2146   class class class wbr 5111  ℝcr 11116   < clt 11260   ≤ cle 11261

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-cnv 5671  df-xr 11264  df-le 11266

This theorem is used by:  letrii  11352  nn0ge2m1nn  12591  0nelfz1  13589  fzpreddisj  13620  hashnn0n0nn  14447  hashge2el2dif  14537  hash3tpde  14550  divalglem5  16479  divalglem6  16480  sadcadd  16540  htpycc  25192  pco1  25227  pcohtpylem  25231  pcopt  25234  pcopt2  25235  pcoass  25236  pcorevlem  25238  vitalilem5  25824  vieta1lem2  26525  ppiltx  27394  ppiublem1  27419  chtub  27429  axlowdimlem16  29364  axlowdim  29368  lfgrnloop  29532  lfuhgr1v0e  29664  lfgrwlkprop  30099  ballotlem2  34946  subfacp1lem1  35710  subfacp1lem5  35715  bcneg1  36267  poimirlem9  38339  poimirlem16  38346  poimirlem17  38347  poimirlem19  38349  poimirlem20  38350  poimirlem22  38352  fdc  38456  pellexlem6  43621  jm2.23  43783  nprmdvdsfacm1lem2  48433