Theorem cnring 21553

Description: The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)

Assertion

Ref	Expression
cnring	⊢ ℂfld ∈ Ring

Proof of Theorem cnring

Step	Hyp	Ref	Expression
1		cncrng 21552	. 2 ⊢ ℂfld ∈ CRing
2		crngring 20331	. 2 ⊢ (ℂfld ∈ CRing → ℂfld ∈ Ring)
3	1, 2	ax-mp 5	1 ⊢ ℂfld ∈ Ring

This proof depends on syntax axioms:   ∈ wcel 2143  Ringcrg 20319  CRingccrg 20320  ℂ_fldccnfld 21531

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11160  ax-resscn 11161  ax-1cn 11162  ax-icn 11163  ax-addcl 11164  ax-addrcl 11165  ax-mulcl 11166  ax-mulrcl 11167  ax-mulcom 11168  ax-addass 11169  ax-mulass 11170  ax-distr 11171  ax-i2m1 11172  ax-1ne0 11173  ax-1rid 11174  ax-rnegex 11175  ax-rrecex 11176  ax-cnre 11177  ax-pre-lttri 11178  ax-pre-lttrn 11179  ax-pre-ltadd 11180  ax-pre-mulgt0 11181  ax-addf 11183

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-tp 4594  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-1st 7982  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-1o 8449  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11447  df-neg 11448  df-nn 12238  df-2 12307  df-3 12308  df-4 12309  df-5 12310  df-6 12311  df-7 12312  df-8 12313  df-9 12314  df-n0 12509  df-z 12596  df-dec 12716  df-uz 12867  df-fz 13540  df-struct 17211  df-sets 17228  df-slot 17246  df-ndx 17258  df-base 17274  df-plusg 17327  df-mulr 17328  df-starv 17329  df-tset 17333  df-ple 17334  df-ds 17336  df-unif 17337  df-0g 17498  df-mgm 18702  df-sgrp 18781  df-mnd 18797  df-grp 19007  df-cmn 19856  df-mgp 20221  df-ring 20321  df-cring 20322  df-cnfld 21532

This theorem is used by:  cnfld0  21555  cnfld1  21556  cnfldneg  21557  cnfldsub  21559  cndrng  21560  cnflddiv  21561  cnfldinv  21562  cnfldmulg  21563  cnfldexp  21564  cnsrng  21565  cnsubmlem  21574  cnsubglem  21575  cnsubrglem  21576  cnsubdrglem  21577  absabv  21583  cnmgpid  21588  gsumfsum  21593  expmhm  21595  nn0srg  21596  rge0srg  21597  expghm  21634  fermltlchr  21688  zrhpsgnmhm  21743  regsumsupp  21781  mhpmulcl  22321  cnngp  24945  cnfldtgp  25037  cnlmod  25308  cnrlmod  25311  cnncvsaddassdemo  25331  cphsubrglem  25345  tdeglem1  26224  tdeglem3  26225  tdeglem4  26226  tdeglem2  26227  plypf1  26378  dvply2  26456  dvnply  26458  taylfvallem  26530  taylf  26533  tayl0  26534  taylpfval  26537  taylply  26541  efabl  26724  efsubm  26725  jensenlem1  27160  jensenlem2  27161  jensen  27162  amgmlem  27163  amgm  27164  wilthlem2  27242  wilthlem3  27243  dchrelbas3  27411  dchrghm  27429  dchrabs  27433  lgseisenlem4  27551  psgnid  33426  cnmsgn0g  33475  altgnsg  33478  znfermltl  33690  ccfldsrarelvec  34070  xrge0iifmhm  34338  zringnm  34357  rezh  34368  mhphflem  43356  rngunsnply  43924  proot1ex  43951  amgm2d  44952  amgm3d  44953  amgm4d  44954  amgmwlem  50677  amgmlemALT  50678  amgmw2d  50679