| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > leloed | Structured version Visualization version GIF version | ||
| Description: 'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
| Ref | Expression |
|---|---|
| ltd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
| ltd.2 | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
| Ref | Expression |
|---|---|
| leloed | ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ltd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
| 2 | ltd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
| 3 | leloe 11313 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) | |
| 4 | 1, 2, 3 | syl2anc 596 | 1 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∨ wo 861 = wceq 1570 ∈ wcel 2146 class class class wbr 5111 ℝcr 11116 < clt 11260 ≤ cle 11261 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-resscn 11174 ax-pre-lttri 11191 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-br 5112 df-opab 5176 df-mpt 5195 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-er 8700 df-en 8950 df-dom 8951 df-sdom 8952 df-pnf 11262 df-mnf 11263 df-xr 11264 df-ltxr 11265 df-le 11266 |
| This theorem is used by: mulge0 11749 prodgt0 12079 lemul1 12084 fimaxre 12176 fiminre 12179 supfirege 12219 nn0le2is012 12678 nn0o1gt2 16463 2mulprm 16775 reconnlem1 25037 reconnlem2 25038 ivthle 25668 ivthle2 25669 ovolicc2lem3 25731 itgsplitioo 26050 dvlip 26205 dvge0 26218 dvfsumlem1 26238 dgrco 26485 plydivex 26511 coseq00topi 26720 logreclem 26980 scvxcvx 27203 pntrlog2bndlem5 27798 fzo0opth 33220 dnibndlem13 37138 lcmineqlem23 42878 lcmineqlem 42879 aks4d1p1 42903 sticksstones12a 42984 sticksstones22 42995 elpell1qr2 43659 pellfundex 43673 fmul01lt1lem2 46361 wallispilem3 46841 fourierdlem25 46906 fourierdlem42 46923 chnsubseqwl 47655 lighneallem4b 48421 nprmdvdsfacm1lem2 48433 nn0o1gt2ALTV 48519 stgoldbwt 48601 sbgoldbwt 48602 sbgoldbalt 48606 nnsum3primesle9 48619 bgoldbtbndlem1 48630 |
| Copyright terms: Public domain | W3C validator |