Theorem ltnlei 11271

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∈ wcel 2109   class class class wbr 5102  ℝcr 11043   < clt 11184   ≤ cle 11185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-cnv 5639  df-xr 11188  df-le 11190

This theorem is referenced by:  letrii  11275  nn0ge2m1nn  12488  0nelfz1  13480  fzpreddisj  13510  hashnn0n0nn  14332  hashge2el2dif  14421  hash3tpde  14434  divalglem5  16343  divalglem6  16344  sadcadd  16404  htpycc  24912  pco1  24948  pcohtpylem  24952  pcopt  24955  pcopt2  24956  pcoass  24957  pcorevlem  24959  vitalilem5  25546  vieta1lem2  26252  ppiltx  27120  ppiublem1  27146  chtub  27156  axlowdimlem16  28937  axlowdim  28941  lfgrnloop  29105  lfuhgr1v0e  29234  lfgrwlkprop  29666  ballotlem2  34473  subfacp1lem1  35159  subfacp1lem5  35164  bcneg1  35716  poimirlem9  37616  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem22  37629  fdc  37732  pellexlem6  42815  jm2.23  42978