Theorem ltnlei 11364

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∈ wcel 2107   class class class wbr 5123  ℝcr 11136   < clt 11277   ≤ cle 11278

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5124  df-opab 5186  df-xp 5671  df-cnv 5673  df-xr 11281  df-le 11283

This theorem is referenced by:  letrii  11368  nn0ge2m1nn  12579  0nelfz1  13565  fzpreddisj  13595  hashnn0n0nn  14412  hashge2el2dif  14501  hash3tpde  14514  divalglem5  16416  divalglem6  16417  sadcadd  16477  htpycc  24948  pco1  24984  pcohtpylem  24988  pcopt  24991  pcopt2  24992  pcoass  24993  pcorevlem  24995  vitalilem5  25583  vieta1lem2  26289  ppiltx  27156  ppiublem1  27182  chtub  27192  axlowdimlem16  28902  axlowdim  28906  lfgrnloop  29070  lfuhgr1v0e  29199  lfgrwlkprop  29633  ballotlem2  34450  subfacp1lem1  35143  subfacp1lem5  35148  bcneg1  35695  poimirlem9  37595  poimirlem16  37602  poimirlem17  37603  poimirlem19  37605  poimirlem20  37606  poimirlem22  37608  fdc  37711  pellexlem6  42808  jm2.23  42971