Theorem ltnlei 11254

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∈ wcel 2113   class class class wbr 5098  ℝcr 11025   < clt 11166   ≤ cle 11167

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 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-cnv 5632  df-xr 11170  df-le 11172

This theorem is referenced by:  letrii  11258  nn0ge2m1nn  12471  0nelfz1  13459  fzpreddisj  13489  hashnn0n0nn  14314  hashge2el2dif  14403  hash3tpde  14416  divalglem5  16324  divalglem6  16325  sadcadd  16385  htpycc  24935  pco1  24971  pcohtpylem  24975  pcopt  24978  pcopt2  24979  pcoass  24980  pcorevlem  24982  vitalilem5  25569  vieta1lem2  26275  ppiltx  27143  ppiublem1  27169  chtub  27179  axlowdimlem16  29030  axlowdim  29034  lfgrnloop  29198  lfuhgr1v0e  29327  lfgrwlkprop  29759  ballotlem2  34646  subfacp1lem1  35373  subfacp1lem5  35378  bcneg1  35930  poimirlem9  37830  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem22  37843  fdc  37946  pellexlem6  43086  jm2.23  43248