![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > cnfldbas | Structured version Unicode version |
Description: The base set of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) |
Ref | Expression |
---|---|
cnfldbas |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnex 9464 |
. 2
![]() ![]() ![]() ![]() | |
2 | cnfldstr 17929 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | baseid 14322 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | snsstp1 4122 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | ssun1 3617 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | ssun1 3617 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | df-cnfld 17928 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 6, 7 | sseqtr4i 3487 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 5, 8 | sstri 3463 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 4, 9 | sstri 3463 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 2, 3, 10 | strfv 14310 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 1, 11 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-sep 4511 ax-nul 4519 ax-pow 4568 ax-pr 4629 ax-un 6472 ax-cnex 9439 ax-resscn 9440 ax-1cn 9441 ax-icn 9442 ax-addcl 9443 ax-addrcl 9444 ax-mulcl 9445 ax-mulrcl 9446 ax-mulcom 9447 ax-addass 9448 ax-mulass 9449 ax-distr 9450 ax-i2m1 9451 ax-1ne0 9452 ax-1rid 9453 ax-rnegex 9454 ax-rrecex 9455 ax-cnre 9456 ax-pre-lttri 9457 ax-pre-lttrn 9458 ax-pre-ltadd 9459 ax-pre-mulgt0 9460 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-nel 2647 df-ral 2800 df-rex 2801 df-reu 2802 df-rab 2804 df-v 3070 df-sbc 3285 df-csb 3387 df-dif 3429 df-un 3431 df-in 3433 df-ss 3440 df-pss 3442 df-nul 3736 df-if 3890 df-pw 3960 df-sn 3976 df-pr 3978 df-tp 3980 df-op 3982 df-uni 4190 df-int 4227 df-iun 4271 df-br 4391 df-opab 4449 df-mpt 4450 df-tr 4484 df-eprel 4730 df-id 4734 df-po 4739 df-so 4740 df-fr 4777 df-we 4779 df-ord 4820 df-on 4821 df-lim 4822 df-suc 4823 df-xp 4944 df-rel 4945 df-cnv 4946 df-co 4947 df-dm 4948 df-rn 4949 df-res 4950 df-ima 4951 df-iota 5479 df-fun 5518 df-fn 5519 df-f 5520 df-f1 5521 df-fo 5522 df-f1o 5523 df-fv 5524 df-riota 6151 df-ov 6193 df-oprab 6194 df-mpt2 6195 df-om 6577 df-1st 6677 df-2nd 6678 df-recs 6932 df-rdg 6966 df-1o 7020 df-oadd 7024 df-er 7201 df-en 7411 df-dom 7412 df-sdom 7413 df-fin 7414 df-pnf 9521 df-mnf 9522 df-xr 9523 df-ltxr 9524 df-le 9525 df-sub 9698 df-neg 9699 df-nn 10424 df-2 10481 df-3 10482 df-4 10483 df-5 10484 df-6 10485 df-7 10486 df-8 10487 df-9 10488 df-10 10489 df-n0 10681 df-z 10748 df-dec 10857 df-uz 10963 df-fz 11539 df-struct 14278 df-ndx 14279 df-slot 14280 df-base 14281 df-plusg 14353 df-mulr 14354 df-starv 14355 df-tset 14359 df-ple 14360 df-ds 14362 df-unif 14363 df-cnfld 17928 |
This theorem is referenced by: cncrng 17946 cnfld0 17949 cnfld1 17950 cnfldneg 17951 cnfldplusf 17952 cnfldsub 17953 cndrng 17954 cnflddiv 17955 cnfldinv 17956 cnfldmulg 17957 cnfldexp 17958 cnsrng 17959 cnsubmlem 17970 cnsubglem 17971 cnsubrglem 17972 cnsubdrglem 17973 absabv 17979 cnsubrg 17982 cnmgpabl 17983 cnmsubglem 17984 gzrngunit 17987 gsumfsum 17988 expmhm 17989 nn0srg 17990 rge0srg 17991 zringbas 17998 zring0 18002 zrngbas 18004 zrng0 18008 dvdsrz 18011 zlpirlem1 18017 zlpirlem3 18019 zringunit 18023 zrngunit 18024 expghm 18032 expghmOLD 18033 cnmsgnbas 18117 psgninv 18121 zrhpsgnmhm 18123 rebase 18145 re0g 18151 regsumsupp 18161 cnfldms 20471 cnfldnm 20474 cnfldtopn 20477 cnfldtopon 20478 clmsscn 20767 cphsubrglem 20812 cphreccllem 20813 cphdivcl 20817 cphabscl 20820 cphsqrcl2 20821 cphsqrcl3 20822 cphipcl 20826 cncms 20983 cnflduss 20984 cnfldcusp 20985 resscdrg 20986 ishl2 20998 recms 21000 tdeglem3 21644 tdeglem4 21645 tdeglem2 21646 plypf1 21796 dvply2g 21867 dvply2 21868 dvnply 21870 taylfvallem 21939 taylf 21942 tayl0 21943 taylpfval 21946 taylply2 21949 taylply 21950 jensenlem1 22496 jensenlem2 22497 jensen 22498 amgmlem 22499 amgm 22500 wilthlem2 22523 wilthlem3 22524 dchrelbas2 22692 dchrelbas3 22693 dchrn0 22705 dchrghm 22711 dchrabs 22715 sum2dchr 22729 lgseisenlem4 22807 qrngbas 22984 cchhllem 23268 regsumfsum 26384 xrge0slmod 26446 iistmd 26466 xrge0iifmhm 26503 xrge0pluscn 26504 zringnm 26522 zzsnmOLD 26524 cnzh 26533 rezh 26534 cnrrext 26573 esumpfinvallem 26657 cnpwstotbnd 28834 repwsmet 28871 rrnequiv 28872 mzpmfpOLD 29222 cnsrexpcl 29660 fsumcnsrcl 29661 cnsrplycl 29662 rngunsnply 29668 proot1ex 29707 deg1mhm 29713 |
Copyright terms: Public domain | W3C validator |