Theorem ltnlei 11411

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∈ wcel 2108   class class class wbr 5166  ℝcr 11183   < clt 11324   ≤ cle 11325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-cnv 5708  df-xr 11328  df-le 11330

This theorem is referenced by:  letrii  11415  nn0ge2m1nn  12622  0nelfz1  13603  fzpreddisj  13633  hashnn0n0nn  14440  hashge2el2dif  14529  hash3tpde  14542  divalglem5  16445  divalglem6  16446  sadcadd  16504  htpycc  25031  pco1  25067  pcohtpylem  25071  pcopt  25074  pcopt2  25075  pcoass  25076  pcorevlem  25078  vitalilem5  25666  vieta1lem2  26371  ppiltx  27238  ppiublem1  27264  chtub  27274  axlowdimlem16  28990  axlowdim  28994  lfgrnloop  29160  lfuhgr1v0e  29289  lfgrwlkprop  29723  ballotlem2  34453  subfacp1lem1  35147  subfacp1lem5  35152  bcneg1  35698  poimirlem9  37589  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem22  37602  fdc  37705  pellexlem6  42790  jm2.23  42953