![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 4ne0 | Structured version Visualization version GIF version |
Description: The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.) |
Ref | Expression |
---|---|
4ne0 | ⊢ 4 ≠ 0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 4re 11437 | . 2 ⊢ 4 ∈ ℝ | |
2 | 4pos 11466 | . 2 ⊢ 0 < 4 | |
3 | 1, 2 | gt0ne0ii 10889 | 1 ⊢ 4 ≠ 0 |
Colors of variables: wff setvar class |
Syntax hints: ≠ wne 3000 0cc0 10253 4c4 11409 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-sep 5006 ax-nul 5014 ax-pow 5066 ax-pr 5128 ax-un 7210 ax-resscn 10310 ax-1cn 10311 ax-icn 10312 ax-addcl 10313 ax-addrcl 10314 ax-mulcl 10315 ax-mulrcl 10316 ax-mulcom 10317 ax-addass 10318 ax-mulass 10319 ax-distr 10320 ax-i2m1 10321 ax-1ne0 10322 ax-1rid 10323 ax-rnegex 10324 ax-rrecex 10325 ax-cnre 10326 ax-pre-lttri 10327 ax-pre-lttrn 10328 ax-pre-ltadd 10329 ax-pre-mulgt0 10330 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3or 1114 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2606 df-eu 2641 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ne 3001 df-nel 3104 df-ral 3123 df-rex 3124 df-reu 3125 df-rab 3127 df-v 3417 df-sbc 3664 df-csb 3759 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4660 df-br 4875 df-opab 4937 df-mpt 4954 df-id 5251 df-po 5264 df-so 5265 df-xp 5349 df-rel 5350 df-cnv 5351 df-co 5352 df-dm 5353 df-rn 5354 df-res 5355 df-ima 5356 df-iota 6087 df-fun 6126 df-fn 6127 df-f 6128 df-f1 6129 df-fo 6130 df-f1o 6131 df-fv 6132 df-riota 6867 df-ov 6909 df-oprab 6910 df-mpt2 6911 df-er 8010 df-en 8224 df-dom 8225 df-sdom 8226 df-pnf 10394 df-mnf 10395 df-xr 10396 df-ltxr 10397 df-le 10398 df-sub 10588 df-neg 10589 df-2 11415 df-3 11416 df-4 11417 |
This theorem is referenced by: 8th4div3 11579 div4p1lem1div2 11614 fldiv4p1lem1div2 12932 fldiv4lem1div2uz2 12933 fldiv4lem1div2 12934 discr 13296 sqoddm1div8 13325 4bc2eq6 13410 bpoly3 15162 bpoly4 15163 flodddiv4 15511 flodddiv4lt 15513 flodddiv4t2lthalf 15514 6lcm4e12 15703 cphipval2 23410 4cphipval2 23411 minveclem3 23598 uniioombl 23756 sincos4thpi 24666 sincos6thpi 24668 heron 24979 quad2 24980 dcubic 24987 mcubic 24988 cubic 24990 dquartlem1 24992 dquartlem2 24993 dquart 24994 quart1cl 24995 quart1lem 24996 quart1 24997 quartlem4 25001 quart 25002 log2tlbnd 25086 bclbnd 25419 bposlem7 25429 bposlem8 25430 bposlem9 25431 gausslemma2dlem0d 25498 gausslemma2dlem3 25507 gausslemma2dlem4 25508 gausslemma2dlem5 25510 m1lgs 25527 2lgslem1a2 25529 2lgslem1 25533 2lgslem2 25534 2lgslem3a 25535 2lgslem3b 25536 2lgslem3c 25537 2lgslem3d 25538 pntibndlem2 25694 4ipval2 28119 ipidsq 28121 dipcl 28123 dipcj 28125 dip0r 28128 dipcn 28131 ip1ilem 28237 ipasslem10 28250 polid2i 28570 lnopeq0i 29422 lnophmlem2 29432 quad3 32109 limclner 40679 stoweid 41075 wallispi2lem1 41083 stirlinglem3 41088 stirlinglem12 41097 stirlinglem13 41098 fouriersw 41243 |
Copyright terms: Public domain | W3C validator |