![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > divge0 | Structured version Visualization version GIF version |
Description: The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 27-Sep-1999.) |
Ref | Expression |
---|---|
divge0 | ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 ≤ (𝐴 / 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ge0div 10971 | . . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐵) → (0 ≤ 𝐴 ↔ 0 ≤ (𝐴 / 𝐵))) | |
2 | 1 | biimpd 219 | . . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐵) → (0 ≤ 𝐴 → 0 ≤ (𝐴 / 𝐵))) |
3 | 2 | 3exp 1112 | . . . 4 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (0 < 𝐵 → (0 ≤ 𝐴 → 0 ≤ (𝐴 / 𝐵))))) |
4 | 3 | com34 91 | . . 3 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (0 ≤ 𝐴 → (0 < 𝐵 → 0 ≤ (𝐴 / 𝐵))))) |
5 | 4 | com23 86 | . 2 ⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐴 → (𝐵 ∈ ℝ → (0 < 𝐵 → 0 ≤ (𝐴 / 𝐵))))) |
6 | 5 | imp43 622 | 1 ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 ≤ (𝐴 / 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1072 ∈ wcel 2071 class class class wbr 4728 (class class class)co 6733 ℝcr 10016 0cc0 10017 < clt 10155 ≤ cle 10156 / cdiv 10765 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1818 ax-5 1920 ax-6 1986 ax-7 2022 ax-8 2073 ax-9 2080 ax-10 2100 ax-11 2115 ax-12 2128 ax-13 2323 ax-ext 2672 ax-sep 4857 ax-nul 4865 ax-pow 4916 ax-pr 4979 ax-un 7034 ax-resscn 10074 ax-1cn 10075 ax-icn 10076 ax-addcl 10077 ax-addrcl 10078 ax-mulcl 10079 ax-mulrcl 10080 ax-mulcom 10081 ax-addass 10082 ax-mulass 10083 ax-distr 10084 ax-i2m1 10085 ax-1ne0 10086 ax-1rid 10087 ax-rnegex 10088 ax-rrecex 10089 ax-cnre 10090 ax-pre-lttri 10091 ax-pre-lttrn 10092 ax-pre-ltadd 10093 ax-pre-mulgt0 10094 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1567 df-ex 1786 df-nf 1791 df-sb 1979 df-eu 2543 df-mo 2544 df-clab 2679 df-cleq 2685 df-clel 2688 df-nfc 2823 df-ne 2865 df-nel 2968 df-ral 2987 df-rex 2988 df-reu 2989 df-rmo 2990 df-rab 2991 df-v 3274 df-sbc 3510 df-csb 3608 df-dif 3651 df-un 3653 df-in 3655 df-ss 3662 df-nul 3992 df-if 4163 df-pw 4236 df-sn 4254 df-pr 4256 df-op 4260 df-uni 4513 df-br 4729 df-opab 4789 df-mpt 4806 df-id 5096 df-po 5107 df-so 5108 df-xp 5192 df-rel 5193 df-cnv 5194 df-co 5195 df-dm 5196 df-rn 5197 df-res 5198 df-ima 5199 df-iota 5932 df-fun 5971 df-fn 5972 df-f 5973 df-f1 5974 df-fo 5975 df-f1o 5976 df-fv 5977 df-riota 6694 df-ov 6736 df-oprab 6737 df-mpt2 6738 df-er 7830 df-en 8041 df-dom 8042 df-sdom 8043 df-pnf 10157 df-mnf 10158 df-xr 10159 df-ltxr 10160 df-le 10161 df-sub 10349 df-neg 10350 df-div 10766 |
This theorem is referenced by: mulge0b 10974 ledivp1 11006 divge0i 11014 divge0d 11994 divelunit 12396 adddivflid 12702 fldiv4p1lem1div2 12719 fldiv 12742 modid 12778 modmuladdnn0 12797 expnbnd 13076 sqrtdiv 14094 sqreulem 14187 iseralt 14503 efcllem 14896 ege2le3 14908 flodddiv4 15228 hashgcdlem 15584 iserodd 15631 fldivp1 15692 4sqlem14 15753 odmodnn0 18048 prmirredlem 19932 icopnfcnv 22831 lebnumii 22855 nmoleub2lem3 23004 ncvs1 23046 minveclem4 23292 mbfi1fseqlem1 23570 mbfi1fseqlem5 23574 radcnvlem1 24255 cxpaddle 24581 leibpilem1 24755 log2tlbnd 24760 birthdaylem3 24768 jensenlem2 24802 amgm 24805 basellem3 24897 ppiub 25017 logfac2 25030 gausslemma2dlem0d 25172 chto1ub 25253 vmadivsum 25259 rpvmasumlem 25264 dchrvmasumlem2 25275 dchrvmasumiflem1 25278 dchrisum0fno1 25288 dchrisum0re 25290 mulog2sumlem2 25312 selberg2lem 25327 pntrmax 25341 pntrsumo1 25342 pntpbnd1 25363 ostth2lem2 25411 axpaschlem 25908 axcontlem2 25933 nv1 27728 siii 27906 minvecolem4 27934 norm1 28304 strlem1 29307 unitdivcld 30145 cvmliftlem2 31464 cvmliftlem10 31472 cvmliftlem13 31474 snmlff 31507 poimirlem29 33638 poimirlem30 33639 poimirlem31 33640 poimirlem32 33641 pellexlem1 37780 pellexlem6 37785 jm2.22 37949 jm2.23 37950 stoweidlem36 40641 stoweidlem38 40643 nn0eo 42717 dignn0flhalf 42807 |
Copyright terms: Public domain | W3C validator |