Theorem ltnlei 11326

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

Syntax hints:  ¬ wn 3   ↔ wb 209   ∈ wcel 2143   class class class wbr 5109  ℝcr 11094   < clt 11238   ≤ cle 11239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-xp 5667  df-cnv 5669  df-xr 11242  df-le 11244

This theorem is referenced by:  letrii  11330  nn0ge2m1nn  12569  0nelfz1  13566  fzpreddisj  13597  hashnn0n0nn  14423  hashge2el2dif  14513  hash3tpde  14526  divalglem5  16450  divalglem6  16451  sadcadd  16511  htpycc  25139  pco1  25174  pcohtpylem  25178  pcopt  25181  pcopt2  25182  pcoass  25183  pcorevlem  25185  vitalilem5  25771  vieta1lem2  26472  ppiltx  27341  ppiublem1  27366  chtub  27376  axlowdimlem16  29307  axlowdim  29311  lfgrnloop  29475  lfuhgr1v0e  29604  lfgrwlkprop  30035  ballotlem2  34879  subfacp1lem1  35671  subfacp1lem5  35676  bcneg1  36228  poimirlem9  38300  poimirlem16  38307  poimirlem17  38308  poimirlem19  38310  poimirlem20  38311  poimirlem22  38313  fdc  38416  pellexlem6  43581  jm2.23  43743  nprmdvdsfacm1lem2  48393