Theorem ltnlei 10610

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

Syntax hints:  ¬ wn 3   ↔ wb 207   ∈ wcel 2080   class class class wbr 4964  ℝcr 10385   < clt 10524   ≤ cle 10525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-sep 5097  ax-nul 5104  ax-pr 5224

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ral 3109  df-rex 3110  df-rab 3113  df-v 3438  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-nul 4214  df-if 4384  df-sn 4475  df-pr 4477  df-op 4481  df-br 4965  df-opab 5027  df-xp 5452  df-cnv 5454  df-xr 10528  df-le 10530

This theorem is referenced by:  letrii  10614  nn0ge2m1nn  11814  0nelfz1  12776  fzpreddisj  12806  hashnn0n0nn  13600  hashge2el2dif  13684  n2dvds1OLD  15551  divalglem5  15581  divalglem6  15582  sadcadd  15640  htpycc  23267  pco1  23302  pcohtpylem  23306  pcopt  23309  pcopt2  23310  pcoass  23311  pcorevlem  23313  vitalilem5  23896  vieta1lem2  24583  ppiltx  25436  ppiublem1  25460  chtub  25470  axlowdimlem16  26426  axlowdim  26430  lfgrnloop  26593  lfuhgr1v0e  26719  lfgrwlkprop  27151  ballotlem2  31355  subfacp1lem1  32028  subfacp1lem5  32033  bcneg1  32570  poimirlem9  34445  poimirlem16  34452  poimirlem17  34453  poimirlem19  34455  poimirlem20  34456  poimirlem22  34458  fdc  34565  pellexlem6  38929  jm2.23  39091