![]() |
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 11322 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | |
2 | axlttri 11315 | . . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 < 𝐴 ↔ ¬ (𝐵 = 𝐴 ∨ 𝐴 < 𝐵))) | |
3 | 2 | ancoms 458 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 < 𝐴 ↔ ¬ (𝐵 = 𝐴 ∨ 𝐴 < 𝐵))) |
4 | 3 | con2bid 354 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐵 = 𝐴 ∨ 𝐴 < 𝐵) ↔ ¬ 𝐵 < 𝐴)) |
5 | eqcom 2735 | . . . . 5 ⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵) | |
6 | 5 | orbi1i 912 | . . . 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 395 ∨ wo 846 = wceq 1534 ∈ wcel 2099 class class class wbr 5148 ℝcr 11137 < clt 11278 ≤ cle 11279 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-sep 5299 ax-nul 5306 ax-pow 5365 ax-pr 5429 ax-un 7740 ax-resscn 11195 ax-pre-lttri 11212 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rab 3430 df-v 3473 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-iota 6500 df-fun 6550 df-fn 6551 df-f 6552 df-f1 6553 df-fo 6554 df-f1o 6555 df-fv 6556 df-er 8724 df-en 8964 df-dom 8965 df-sdom 8966 df-pnf 11280 df-mnf 11281 df-xr 11282 df-ltxr 11283 df-le 11284 |
This theorem is referenced by: ltle 11332 leltne 11333 lelttr 11334 ltletr 11336 letr 11338 leid 11340 ltlen 11345 leloei 11361 leloed 11387 lemul1 12096 lemul1a 12098 squeeze0 12147 sup3 12201 nn0ge0 12527 nn0sub 12552 elnn0z 12601 xlemul1a 13299 modfzo0difsn 13940 om2uzlti 13947 om2uzlt2i 13948 sqlecan 14204 discr 14234 facdiv 14278 facwordi 14280 resqrex 15229 sqrt2irr 16225 lcmf 16603 ge2nprmge4 16671 efgsfo 19693 efgred 19702 itg2mulc 25676 itgabs 25763 dgrlt 26200 sinq12ge0 26442 sineq0 26457 cxpge0 26616 cxplea 26629 cxple2 26630 cxple2a 26632 cxpcn3lem 26681 cxpcn3 26682 cxpaddlelem 26685 cxpaddle 26686 ang180lem3 26742 atanlogaddlem 26844 rlimcnp2 26897 jensen 26920 amgm 26922 htthlem 30726 hiidge0 30907 staddi 32055 stadd3i 32057 poimirlem28 37121 itgaddnclem2 37152 itgabsnc 37162 pellfund14gap 42307 sineq0ALT 44376 icccncfext 45275 ltnltne 46679 iccpartnel 46778 odz2prm2pw 46903 evenltle 47057 gbowge7 47103 bgoldbtbndlem1 47145 elfzolborelfzop1 47587 |
Copyright terms: Public domain | W3C validator |