![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > leloe | Structured version Visualization version GIF version |
Description: 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by NM, 13-May-1999.) |
Ref | Expression |
---|---|
leloe | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lenlt 11289 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | |
2 | axlttri 11282 | . . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 < 𝐴 ↔ ¬ (𝐵 = 𝐴 ∨ 𝐴 < 𝐵))) | |
3 | 2 | ancoms 460 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 < 𝐴 ↔ ¬ (𝐵 = 𝐴 ∨ 𝐴 < 𝐵))) |
4 | 3 | con2bid 355 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐵 = 𝐴 ∨ 𝐴 < 𝐵) ↔ ¬ 𝐵 < 𝐴)) |
5 | eqcom 2740 | . . . . 5 ⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵) | |
6 | 5 | orbi1i 913 | . . . 4 ⊢ ((𝐵 = 𝐴 ∨ 𝐴 < 𝐵) ↔ (𝐴 = 𝐵 ∨ 𝐴 < 𝐵)) |
7 | orcom 869 | . . . 4 ⊢ ((𝐴 = 𝐵 ∨ 𝐴 < 𝐵) ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)) | |
8 | 6, 7 | bitri 275 | . . 3 ⊢ ((𝐵 = 𝐴 ∨ 𝐴 < 𝐵) ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)) |
9 | 4, 8 | bitr3di 286 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (¬ 𝐵 < 𝐴 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) |
10 | 1, 9 | bitrd 279 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∨ wo 846 = wceq 1542 ∈ wcel 2107 class class class wbr 5148 ℝcr 11106 < clt 11245 ≤ cle 11246 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-resscn 11164 ax-pre-lttri 11181 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-er 8700 df-en 8937 df-dom 8938 df-sdom 8939 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 |
This theorem is referenced by: ltle 11299 leltne 11300 lelttr 11301 ltletr 11303 letr 11305 leid 11307 ltlen 11312 leloei 11328 leloed 11354 lemul1 12063 lemul1a 12065 squeeze0 12114 sup3 12168 nn0ge0 12494 nn0sub 12519 elnn0z 12568 xlemul1a 13264 modfzo0difsn 13905 om2uzlti 13912 om2uzlt2i 13913 sqlecan 14170 discr 14200 facdiv 14244 facwordi 14246 resqrex 15194 sqrt2irr 16189 lcmf 16567 ge2nprmge4 16635 efgsfo 19602 efgred 19611 itg2mulc 25257 itgabs 25344 dgrlt 25772 sinq12ge0 26010 sineq0 26025 cxpge0 26183 cxplea 26196 cxple2 26197 cxple2a 26199 cxpcn3lem 26245 cxpcn3 26246 cxpaddlelem 26249 cxpaddle 26250 ang180lem3 26306 atanlogaddlem 26408 rlimcnp2 26461 jensen 26483 amgm 26485 htthlem 30158 hiidge0 30339 staddi 31487 stadd3i 31489 poimirlem28 36505 itgaddnclem2 36536 itgabsnc 36546 pellfund14gap 41611 sineq0ALT 43684 icccncfext 44590 ltnltne 45994 iccpartnel 46093 odz2prm2pw 46218 evenltle 46372 gbowge7 46418 bgoldbtbndlem1 46460 elfzolborelfzop1 47154 |
Copyright terms: Public domain | W3C validator |