Theorem zringbas 21485

Description: The integers are the base of the ring of integers. (Contributed by Thierry Arnoux, 31-Oct-2017.) (Revised by AV, 9-Jun-2019.)

Assertion

Ref	Expression
zringbas	⊢ ℤ = (Base‘ℤring)

Proof of Theorem zringbas

Step	Hyp	Ref	Expression
1		zsscn 12573	. 2 ⊢ ℤ ⊆ ℂ
2		df-zring 21479	. . 3 ⊢ ℤring = (ℂfld ↾s ℤ)
3		cnfldbas 21408	. . 3 ⊢ ℂ = (Base‘ℂfld)
4	2, 3	ressbas2 17257	. 2 ⊢ (ℤ ⊆ ℂ → ℤ = (Base‘ℤring))
5	1, 4	ax-mp 5	1 ⊢ ℤ = (Base‘ℤring)

Syntax hints:   = wceq 1559   ⊆ wss 3904  ‘cfv 6517  ℂcc 11068  ℤcz 12565  Basecbs 17228  ℂ_fldccnfld 21404  ℤ_ringczring 21478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714  ax-cnex 11126  ax-resscn 11127  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-addrcl 11131  ax-mulcl 11132  ax-mulrcl 11133  ax-mulcom 11134  ax-addass 11135  ax-mulass 11136  ax-distr 11137  ax-i2m1 11138  ax-1ne0 11139  ax-1rid 11140  ax-rnegex 11141  ax-rrecex 11142  ax-cnre 11143  ax-pre-lttri 11144  ax-pre-lttrn 11145  ax-pre-ltadd 11146  ax-pre-mulgt0 11147

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-tp 4586  df-op 4588  df-uni 4865  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5540  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-pred 6284  df-ord 6345  df-on 6346  df-lim 6347  df-suc 6348  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-riota 7349  df-ov 7395  df-oprab 7396  df-mpo 7397  df-om 7843  df-1st 7966  df-2nd 7967  df-frecs 8257  df-wrecs 8288  df-recs 8337  df-rdg 8376  df-1o 8432  df-er 8673  df-en 8924  df-dom 8925  df-sdom 8926  df-fin 8927  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218  df-le 11219  df-sub 11413  df-neg 11414  df-nn 12208  df-2 12277  df-3 12278  df-4 12279  df-5 12280  df-6 12281  df-7 12282  df-8 12283  df-9 12284  df-n0 12479  df-z 12566  df-dec 12686  df-uz 12837  df-fz 13510  df-struct 17166  df-sets 17183  df-slot 17201  df-ndx 17213  df-base 17229  df-ress 17250  df-plusg 17282  df-mulr 17283  df-starv 17284  df-tset 17288  df-ple 17289  df-ds 17291  df-unif 17292  df-cnfld 21405  df-zring 21479

This theorem is referenced by:  dvdsrzring  21493  zringlpirlem1  21494  zringlpirlem3  21496  zringinvg  21497  zringunit  21498  zringndrg  21500  zringcyg  21501  prmirredlem  21504  prmirred  21506  expghm  21507  mulgghm2  21508  mulgrhm  21509  mulgrhm2  21510  pzriprnglem2  21514  pzriprnglem4  21516  pzriprnglem5  21517  pzriprnglem6  21518  pzriprnglem8  21520  pzriprnglem10  21522  pzriprnglem12  21524  pzriprng1ALT  21528  zlmlmod  21554  fermltlchr  21561  chrrhm  21563  domnchr  21564  znlidl  21565  znbas  21575  znzrh2  21577  znzrhfo  21579  zndvds  21581  znf1o  21583  zzngim  21584  znfld  21592  znidomb  21593  znunit  21595  znrrg  21597  cygznlem3  21601  frgpcyg  21605  zrhpsgnodpm  21624  zlmassa  21935  ply1fermltlchr  22355  dchrzrhmul  27287  lgsqrlem1  27387  lgsqrlem2  27388  lgsqrlem3  27389  lgsdchr  27396  lgseisenlem3  27418  lgseisenlem4  27419  dchrisum0flblem1  27549  gsummulgc2  33207  elrgspnlem1  33384  znfermltl  33513  elrspunidl  33575  zringidom  33708  zringfrac  33711  esplyfval0  33822  esplyfval2  33823  esplympl  33825  esplyfval3  33830  vieta  33838  mdetpmtr1  34081  mdetpmtr12  34083  mdetlap  34090  nmmulg  34224  cnzh  34226  rezh  34227  zrhf1ker  34231  zrhunitpreima  34234  elzrhunit  34235  zrhneg  34236  zrhcntr  34237  qqhval2lem  34239  qqhf  34244  qqhghm  34246  qqhrhm  34247  qqhnm  34248  zndvdchrrhm  42554  aks6d1c1p2  42690  aks6d1c1p3  42691  aks6d1c1  42697  hashscontpowcl  42701  hashscontpow  42703  aks6d1c4  42705  aks6d1c2  42711  aks6d1c5lem0  42716  aks6d1c5lem1  42717  aks6d1c5lem3  42718  aks6d1c5lem2  42719  aks6d1c5  42720  aks6d1c6lem1  42751  aks6d1c6lem3  42753  aks6d1c6isolem2  42756  aks6d1c6isolem3  42757  aks6d1c6lem5  42758  aks6d1c7lem1  42761  aks5lem3a  42770  aks5lem5a  42772  mzpmfp  43292  2zlidl  48826  zlmodzxzel  48941  zlmodzxzscm  48943  linevalexample  48981  zlmodzxzldeplem3  49088  zlmodzxzldep  49090  ldepsnlinclem1  49091  ldepsnlinclem2  49092