![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3cn | Structured version Visualization version GIF version |
Description: The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.) |
Ref | Expression |
---|---|
3cn | ⊢ 3 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3 11497 | . 2 ⊢ 3 = (2 + 1) | |
2 | 2cn 11508 | . . 3 ⊢ 2 ∈ ℂ | |
3 | ax-1cn 10385 | . . 3 ⊢ 1 ∈ ℂ | |
4 | 2, 3 | addcli 10438 | . 2 ⊢ (2 + 1) ∈ ℂ |
5 | 1, 4 | eqeltri 2856 | 1 ⊢ 3 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2048 (class class class)co 6970 ℂcc 10325 1c1 10328 + caddc 10330 2c2 11488 3c3 11489 |
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-ext 2745 ax-1cn 10385 ax-addcl 10387 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-cleq 2765 df-clel 2840 df-2 11496 df-3 11497 |
This theorem is referenced by: 3ex 11516 4cn 11519 4m1e3 11569 3p2e5 11591 3p3e6 11592 4p4e8 11595 5p4e9 11598 3t1e3 11605 3t2e6 11606 3t3e9 11607 8th4div3 11660 halfpm6th 11661 6p4e10 11978 9t8e72 12034 halfthird 12049 sq3 13369 expnass 13378 fac3 13448 sqrlem7 14459 caurcvgr 14881 bpoly2 15261 bpoly3 15262 bpoly4 15263 ef01bndlem 15387 sin01bnd 15388 cos01bnd 15389 cos1bnd 15390 cos2bnd 15391 cos01gt0 15394 rpnnen2lem3 15419 rpnnen2lem11 15427 3dvdsdec 15531 3dvds2dec 15532 3lcm2e6woprm 15805 prmo3 16223 2exp6 16268 2exp16 16270 7prm 16290 13prm 16295 17prm 16296 19prm 16297 37prm 16300 43prm 16301 83prm 16302 139prm 16303 163prm 16304 317prm 16305 631prm 16306 1259lem1 16310 1259lem2 16311 1259lem3 16312 1259lem4 16313 1259lem5 16314 1259prm 16315 2503lem1 16316 2503lem2 16317 2503lem3 16318 2503prm 16319 4001lem1 16320 4001lem2 16321 4001lem3 16322 4001lem4 16323 4001prm 16324 tangtx 24784 sincos6thpi 24794 sincos3rdpi 24795 pigt3 24796 pige3ALT 24798 2logb9irrALT 25067 ang180lem2 25079 1cubr 25111 dcubic1lem 25112 dcubic2 25113 dcubic1 25114 dcubic 25115 mcubic 25116 cubic2 25117 cubic 25118 binom4 25119 quart1cl 25123 quart1lem 25124 quart1 25125 quartlem1 25126 quartlem3 25128 log2cnv 25214 log2tlbnd 25215 log2ublem2 25217 log2ublem3 25218 log2ub 25219 basellem5 25354 basellem8 25357 basellem9 25358 cht3 25442 ppiub 25472 chtub 25480 bclbnd 25548 bposlem6 25557 bposlem8 25559 bposlem9 25560 lgsdir2lem1 25593 lgsdir2lem5 25597 2lgslem3b 25665 2lgslem3d 25667 2lgsoddprmlem3c 25680 2lgsoddprmlem3d 25681 addsqnreup 25711 pntibndlem1 25857 pntlemk 25874 ex-opab 27979 ex-exp 27997 ex-dvds 28003 ex-gcd 28004 ex-lcm 28005 ex-prmo 28006 ex-ind-dvds 28008 fib5 31266 fib6 31267 hgt750lem 31531 hgt750lem2 31532 hgt750leme 31538 problem4 32371 problem5 32372 sinccvglem 32375 mblfinlem3 34320 itg2addnclem2 34333 itg2addnclem3 34334 heiborlem6 34484 heiborlem7 34485 235t711 38554 ex-decpmul 38555 jm2.23 38934 inductionexd 39813 lhe4.4ex1a 40021 stoweidlem13 41675 stoweidlem26 41688 stoweidlem34 41696 wallispilem4 41730 wallispi2lem1 41733 fmtno5lem1 43023 fmtno5lem2 43024 257prm 43031 fmtno4prmfac 43042 fmtno4nprmfac193 43044 139prmALT 43067 127prm 43071 mod42tp1mod8 43075 3exp4mod41 43089 41prothprmlem2 43091 6even 43184 11t31e341 43205 2exp340mod341 43206 gbpart8 43241 sbgoldbwt 43250 sbgoldbst 43251 evengpop3 43271 evengpoap3 43272 nnsum4primeseven 43273 nnsum4primesevenALTV 43274 2t6m3t4e0 43700 linevalexample 43757 zlmodzxzequa 43858 zlmodzxzequap 43861 |
Copyright terms: Public domain | W3C validator |