Theorem ltnlei 11470

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∈ wcel 2147   class class class wbr 5108  ℝcr 11238   < clt 11382   ≤ cle 11383

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-xp 5664  df-cnv 5666  df-xr 11386  df-le 11388

This theorem is used by:  letrii  11474  nn0ge2m1nn  12716  0nelfz1  13716  fzpreddisj  13747  hashnn0n0nn  14576  hashge2el2dif  14666  hash3tpde  14679  divalglem5  16611  divalglem6  16612  sadcadd  16672  htpycc  25356  pco1  25391  pcohtpylem  25395  pcopt  25398  pcopt2  25399  pcoass  25400  pcorevlem  25402  vitalilem5  25988  vieta1lem2  26689  ppiltx  27561  ppiublem1  27586  chtub  27596  axlowdimlem16  29592  axlowdim  29596  lfgrnloop  29760  lfuhgr1v0e  29892  lfgrwlkprop  30327  ballotlem2  35232  subfacp1lem1  36152  subfacp1lem5  36157  bcneg1  36716  poimirlem9  38815  poimirlem16  38822  poimirlem17  38823  poimirlem19  38825  poimirlem20  38826  poimirlem22  38828  fdc  38945  pellexlem6  44107  jm2.23  44269  nprmdvdsfacm1lem2  48979