![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > halfcn | Structured version Visualization version GIF version |
Description: One-half is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
halfcn | ⊢ (1 / 2) ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2cn 11508 | . 2 ⊢ 2 ∈ ℂ | |
2 | 2ne0 11544 | . 2 ⊢ 2 ≠ 0 | |
3 | 1, 2 | reccli 11163 | 1 ⊢ (1 / 2) ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2048 (class class class)co 6970 ℂcc 10325 1c1 10328 / cdiv 11090 2c2 11488 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 ax-resscn 10384 ax-1cn 10385 ax-icn 10386 ax-addcl 10387 ax-addrcl 10388 ax-mulcl 10389 ax-mulrcl 10390 ax-mulcom 10391 ax-addass 10392 ax-mulass 10393 ax-distr 10394 ax-i2m1 10395 ax-1ne0 10396 ax-1rid 10397 ax-rnegex 10398 ax-rrecex 10399 ax-cnre 10400 ax-pre-lttri 10401 ax-pre-lttrn 10402 ax-pre-ltadd 10403 ax-pre-mulgt0 10404 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-reu 3089 df-rmo 3090 df-rab 3091 df-v 3411 df-sbc 3678 df-csb 3783 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-nul 4174 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4707 df-br 4924 df-opab 4986 df-mpt 5003 df-id 5305 df-po 5319 df-so 5320 df-xp 5406 df-rel 5407 df-cnv 5408 df-co 5409 df-dm 5410 df-rn 5411 df-res 5412 df-ima 5413 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-riota 6931 df-ov 6973 df-oprab 6974 df-mpo 6975 df-er 8081 df-en 8299 df-dom 8300 df-sdom 8301 df-pnf 10468 df-mnf 10469 df-xr 10470 df-ltxr 10471 df-le 10472 df-sub 10664 df-neg 10665 df-div 11091 df-2 11496 |
This theorem is referenced by: halfpm6th 11661 rddif 14551 geo2sum 15079 geo2lim 15081 geoihalfsum 15088 bpoly1 15255 bpoly2 15261 bpoly3 15262 efcllem 15281 ege2le3 15293 efival 15355 flodddiv4 15614 pcoass 23321 iscmet3lem3 23586 mbfi1fseqlem6 24014 dvmptre 24259 aaliou3lem2 24625 aaliou3lem3 24626 sincos4thpi 24792 cxpsqrt 24977 dvsqrt 25014 dvcnsqrt 25016 resqrtcn 25021 ang180lem3 25080 heron 25107 efiatan 25181 efiatan2 25186 gausslemma2dlem1a 25633 ipdirilem 28373 mayete3i 29276 opsqrlem6 29693 dnibndlem3 33279 dnibndlem6 33282 cntotbnd 34464 stirlinglem1 41736 dirkerper 41758 dirkertrigeqlem3 41762 dirkeritg 41764 dirkercncflem2 41766 fourierdlem18 41787 fourierdlem57 41825 fourierdlem58 41826 fourierdlem62 41830 fourierdlem103 41871 fourierdlem104 41872 0nodd 43385 |
Copyright terms: Public domain | W3C validator |