Theorem ltnlei 11237

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∈ wcel 2109   class class class wbr 5092  ℝcr 11008   < clt 11149   ≤ cle 11150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-xp 5625  df-cnv 5627  df-xr 11153  df-le 11155

This theorem is referenced by:  letrii  11241  nn0ge2m1nn  12454  0nelfz1  13446  fzpreddisj  13476  hashnn0n0nn  14298  hashge2el2dif  14387  hash3tpde  14400  divalglem5  16308  divalglem6  16309  sadcadd  16369  htpycc  24877  pco1  24913  pcohtpylem  24917  pcopt  24920  pcopt2  24921  pcoass  24922  pcorevlem  24924  vitalilem5  25511  vieta1lem2  26217  ppiltx  27085  ppiublem1  27111  chtub  27121  axlowdimlem16  28902  axlowdim  28906  lfgrnloop  29070  lfuhgr1v0e  29199  lfgrwlkprop  29631  ballotlem2  34457  subfacp1lem1  35156  subfacp1lem5  35161  bcneg1  35713  poimirlem9  37613  poimirlem16  37620  poimirlem17  37621  poimirlem19  37623  poimirlem20  37624  poimirlem22  37626  fdc  37729  pellexlem6  42811  jm2.23  42973