Theorem ltnlei 11361

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∈ wcel 2109   class class class wbr 5124  ℝcr 11133   < clt 11274   ≤ cle 11275

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

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 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  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 5125  df-opab 5187  df-xp 5665  df-cnv 5667  df-xr 11278  df-le 11280

This theorem is referenced by:  letrii  11365  nn0ge2m1nn  12576  0nelfz1  13565  fzpreddisj  13595  hashnn0n0nn  14414  hashge2el2dif  14503  hash3tpde  14516  divalglem5  16421  divalglem6  16422  sadcadd  16482  htpycc  24935  pco1  24971  pcohtpylem  24975  pcopt  24978  pcopt2  24979  pcoass  24980  pcorevlem  24982  vitalilem5  25570  vieta1lem2  26276  ppiltx  27144  ppiublem1  27170  chtub  27180  axlowdimlem16  28941  axlowdim  28945  lfgrnloop  29109  lfuhgr1v0e  29238  lfgrwlkprop  29672  ballotlem2  34526  subfacp1lem1  35206  subfacp1lem5  35211  bcneg1  35758  poimirlem9  37658  poimirlem16  37665  poimirlem17  37666  poimirlem19  37668  poimirlem20  37669  poimirlem22  37671  fdc  37774  pellexlem6  42832  jm2.23  42995