Theorem ltnlei 11252

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∈ wcel 2113   class class class wbr 5096  ℝcr 11023   < clt 11164   ≤ cle 11165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-xp 5628  df-cnv 5630  df-xr 11168  df-le 11170

This theorem is referenced by:  letrii  11256  nn0ge2m1nn  12469  0nelfz1  13457  fzpreddisj  13487  hashnn0n0nn  14312  hashge2el2dif  14401  hash3tpde  14414  divalglem5  16322  divalglem6  16323  sadcadd  16383  htpycc  24933  pco1  24969  pcohtpylem  24973  pcopt  24976  pcopt2  24977  pcoass  24978  pcorevlem  24980  vitalilem5  25567  vieta1lem2  26273  ppiltx  27141  ppiublem1  27167  chtub  27177  axlowdimlem16  28979  axlowdim  28983  lfgrnloop  29147  lfuhgr1v0e  29276  lfgrwlkprop  29708  ballotlem2  34595  subfacp1lem1  35322  subfacp1lem5  35327  bcneg1  35879  poimirlem9  37769  poimirlem16  37776  poimirlem17  37777  poimirlem19  37779  poimirlem20  37780  poimirlem22  37782  fdc  37885  pellexlem6  43018  jm2.23  43180