Theorem leloe 11221

Description: 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by NM, 13-May-1999.)

Assertion

Ref	Expression
leloe	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))

Proof of Theorem leloe

Step	Hyp	Ref	Expression
1		lenlt 11213	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
2		axlttri 11206	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 < 𝐴 ↔ ¬ (𝐵 = 𝐴 ∨ 𝐴 < 𝐵)))
3	2	ancoms 458	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 < 𝐴 ↔ ¬ (𝐵 = 𝐴 ∨ 𝐴 < 𝐵)))
4	3	con2bid 354	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐵 = 𝐴 ∨ 𝐴 < 𝐵) ↔ ¬ 𝐵 < 𝐴))
5		eqcom 2744	. . . . 5 ⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵)
6	5	orbi1i 914	. . . 4 ⊢ ((𝐵 = 𝐴 ∨ 𝐴 < 𝐵) ↔ (𝐴 = 𝐵 ∨ 𝐴 < 𝐵))
7		orcom 871	. . . 4 ⊢ ((𝐴 = 𝐵 ∨ 𝐴 < 𝐵) ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))
8	6, 7	bitri 275	. . 3 ⊢ ((𝐵 = 𝐴 ∨ 𝐴 < 𝐵) ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))
9	4, 8	bitr3di 286	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (¬ 𝐵 < 𝐴 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))
10	1, 9	bitrd 279	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114   class class class wbr 5086  ℝcr 11026   < clt 11168   ≤ cle 11169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-resscn 11084  ax-pre-lttri 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174

This theorem is referenced by:  ltle  11223  leltne  11224  lelttr  11225  ltletr  11227  letr  11229  leid  11231  ltlen  11236  leloei  11252  leloed  11278  lemul1  11996  lemul1a  11998  squeeze0  12048  sup3  12102  nn0ge0  12451  nn0sub  12476  elnn0z  12526  xlemul1a  13229  modfzo0difsn  13894  om2uzlti  13901  om2uzlt2i  13902  sqlecan  14160  discr  14191  facdiv  14238  facwordi  14240  resqrex  15201  sqrt2irr  16205  lcmf  16591  ge2nprmge4  16660  efgsfo  19703  efgred  19712  itg2mulc  25723  itgabs  25811  dgrlt  26243  sinq12ge0  26488  sineq0  26504  cxpge0  26663  cxplea  26676  cxple2  26677  cxple2a  26679  cxpcn3lem  26728  cxpcn3  26729  cxpaddlelem  26732  cxpaddle  26733  ang180lem3  26792  atanlogaddlem  26894  rlimcnp2  26947  jensen  26970  amgm  26972  htthlem  31008  hiidge0  31189  staddi  32337  stadd3i  32339  2exple2exp  32938  poimirlem28  37980  itgaddnclem2  38011  itgabsnc  38021  sn-sup3d  42948  pellfund14gap  43330  sineq0ALT  45378  icccncfext  46330  ltnltne  47744  iccpartnel  47895  nprmmul3  47986  odz2prm2pw  48023  evenltle  48190  gbowge7  48236  bgoldbtbndlem1  48278  elfzolborelfzop1  48992