Theorem ltnlei 11267

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∈ wcel 2114   class class class wbr 5085  ℝcr 11037   < clt 11179   ≤ cle 11180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-cnv 5639  df-xr 11183  df-le 11185

This theorem is referenced by:  letrii  11271  nn0ge2m1nn  12507  0nelfz1  13497  fzpreddisj  13527  hashnn0n0nn  14353  hashge2el2dif  14442  hash3tpde  14455  divalglem5  16366  divalglem6  16367  sadcadd  16427  htpycc  24947  pco1  24982  pcohtpylem  24986  pcopt  24989  pcopt2  24990  pcoass  24991  pcorevlem  24993  vitalilem5  25579  vieta1lem2  26277  ppiltx  27140  ppiublem1  27165  chtub  27175  axlowdimlem16  29026  axlowdim  29030  lfgrnloop  29194  lfuhgr1v0e  29323  lfgrwlkprop  29754  ballotlem2  34633  subfacp1lem1  35361  subfacp1lem5  35366  bcneg1  35918  poimirlem9  37950  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem22  37963  fdc  38066  pellexlem6  43262  jm2.23  43424  nprmdvdsfacm1lem2  48084