Theorem lelttric 11366

Description: Trichotomy law. (Contributed by NM, 4-Apr-2005.)

Assertion

Ref	Expression
lelttric	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ∨ 𝐵 < 𝐴))

Proof of Theorem lelttric

Step	Hyp	Ref	Expression
1		pm2.1 896	. 2 ⊢ (¬ 𝐵 < 𝐴 ∨ 𝐵 < 𝐴)
2		lenlt 11337	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
3	2	orbi1d 916	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∨ 𝐵 < 𝐴) ↔ (¬ 𝐵 < 𝐴 ∨ 𝐵 < 𝐴)))
4	1, 3	mpbiri 258	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ∨ 𝐵 < 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   ∈ wcel 2106   class class class wbr 5148  ℝcr 11152   < clt 11293   ≤ cle 11294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-xp 5695  df-cnv 5697  df-xr 11297  df-le 11299

This theorem is referenced by:  ltlecasei  11367  fzsplit2  13586  uzsplit  13633  fzospliti  13728  fzouzsplit  13731  discr1  14275  faclbnd  14326  faclbnd4lem1  14329  faclbnd4lem4  14332  dvdslelem  16343  dvdsprmpweqle  16920  icccmplem2  24859  icccmp  24861  bcmono  27336  bpos1lem  27341  bposlem3  27345  bpos  27352  fzsplit3  32802  submateq  33770  lzunuz  42756  jm2.24  42952  fzuntgd  43448  iccpartnel  47363  bgoldbtbnd  47734  tgoldbach  47742  reorelicc  48560