![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ltled | GIF version |
Description: 'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
ltd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
ltd.2 | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
ltled.1 | ⊢ (𝜑 → 𝐴 < 𝐵) |
Ref | Expression |
---|---|
ltled | ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltled.1 | . 2 ⊢ (𝜑 → 𝐴 < 𝐵) | |
2 | ltd.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
3 | ltd.2 | . . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
4 | ltle 8043 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)) | |
5 | 2, 3, 4 | syl2anc 411 | . 2 ⊢ (𝜑 → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)) |
6 | 1, 5 | mpd 13 | 1 ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2148 class class class wbr 4003 ℝcr 7809 < clt 7990 ≤ cle 7991 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-sep 4121 ax-pow 4174 ax-pr 4209 ax-un 4433 ax-setind 4536 ax-cnex 7901 ax-resscn 7902 ax-pre-ltirr 7922 ax-pre-lttrn 7924 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-rab 2464 df-v 2739 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-pw 3577 df-sn 3598 df-pr 3599 df-op 3601 df-uni 3810 df-br 4004 df-opab 4065 df-xp 4632 df-cnv 4634 df-pnf 7992 df-mnf 7993 df-xr 7994 df-ltxr 7995 df-le 7996 |
This theorem is referenced by: ltnsymd 8075 addgt0d 8476 lt2addd 8522 lt2msq1 8840 lediv12a 8849 ledivp1 8858 nn2ge 8950 fznatpl1 10073 exbtwnzlemex 10247 apbtwnz 10271 iseqf1olemkle 10481 expnbnd 10640 nn0ltexp2 10685 cvg1nlemres 10989 resqrexlemnm 11022 resqrexlemcvg 11023 resqrexlemglsq 11026 sqrtgt0 11038 leabs 11078 ltabs 11091 abslt 11092 absle 11093 maxabslemab 11210 2zsupmax 11229 2zinfmin 11246 xrmaxiflemab 11250 fsum3cvg3 11399 divcnv 11500 expcnvre 11506 absltap 11512 cvgratnnlemnexp 11527 cvgratnnlemmn 11528 cvgratnnlemfm 11532 mertenslemi1 11538 cos12dec 11770 dvdslelemd 11843 divalglemnn 11917 divalglemeuneg 11922 lcmgcdlem 12071 isprm5lem 12135 znege1 12172 sqrt2irraplemnn 12173 eulerthlemrprm 12223 eulerthlema 12224 4sqlem7 12376 ennnfonelemex 12409 strleund 12556 suplociccreex 13995 ivthinclemlm 14005 ivthinclemum 14006 ivthinclemlopn 14007 ivthinclemuopn 14009 ivthdec 14015 dveflem 14080 efltlemlt 14088 sin0pilem1 14095 sin0pilem2 14096 coseq0negpitopi 14150 tangtx 14152 cosq34lt1 14164 cos02pilt1 14165 apdifflemf 14676 |
Copyright terms: Public domain | W3C validator |