Theorem ltnlei 11304

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

Syntax hints:  ¬ wn 3   ↔ wb 208   ∈ wcel 2142   class class class wbr 5100  ℝcr 11072   < clt 11216   ≤ cle 11217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5653  df-cnv 5655  df-xr 11220  df-le 11222

This theorem is referenced by:  letrii  11308  nn0ge2m1nn  12551  0nelfz1  13548  fzpreddisj  13578  hashnn0n0nn  14404  hashge2el2dif  14493  hash3tpde  14506  divalglem5  16431  divalglem6  16432  sadcadd  16492  htpycc  25042  pco1  25077  pcohtpylem  25081  pcopt  25084  pcopt2  25085  pcoass  25086  pcorevlem  25088  vitalilem5  25674  vieta1lem2  26375  ppiltx  27241  ppiublem1  27266  chtub  27276  axlowdimlem16  29158  axlowdim  29162  lfgrnloop  29326  lfuhgr1v0e  29455  lfgrwlkprop  29886  ballotlem2  34786  subfacp1lem1  35529  subfacp1lem5  35534  bcneg1  36086  poimirlem9  38128  poimirlem16  38135  poimirlem17  38136  poimirlem19  38138  poimirlem20  38139  poimirlem22  38141  fdc  38244  pellexlem6  43411  jm2.23  43573  nprmdvdsfacm1lem2  48230