Theorem axmulcl 5292

Description: Closure law for multiplication of complex numbers. Axiom 7 of 25 for real and complex numbers, derived from ZF set theory.

Assertion

Ref	Expression
axmulcl	|- ((A e. CC /\ B e. CC) -> (A x. B) e. CC)

Proof of Theorem axmulcl

Step	Hyp	Ref	Expression
1		axmulopr 5285	. 2 |- x. :(CC X. CC)-->CC
2	1	foprcl 4022	1 |- ((A e. CC /\ B e. CC) -> (A x. B) e. CC)

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 960  (class class class)co 3970  CCcc 5251   x. cmul 5258

This theorem is referenced by:  mulclt 5322  mulcl 5340  cnegextlem2 5365  cnegext 5367  mul4t 5439  muladdt 5440  subdit 5446  submul2t 5479  mulsubt 5496  recextlem1 5701  recext 5703  muleqaddt 5719  receu 5720  mulnzcnopr 5721  divasst 5755  divmuldivt 5789  divadddivt 5793  divdivdivt 5794  conjmult 5806  zneo 6209  qbtwnre 6286  expclt 6589  mulexpt 6602  sqclt 6619  subsqt 6650  subsq2t 6651  bernneq 6660  bernneq2 6661  cjclt 6772  crret 6777  crimt 6778  reim0t 6782  recjt 6825  imcjt 6826  cjreimt 6835  cjreim2t 6836  cj11t 6837  sqabsaddt 6855  sqabssubt 6856  absreimsqt 6863  absreimt 6864  fsummulc1 7040  binomlem1 7073  binomlem2 7074  binomlem4 7076  binomlem5 7077  climmullem4 7130  climmullem5 7131  climmullem8 7134  climsub 7137  caucvg3a 7171  caucvg3lem 7173  fnsmnt 7233  geoser 7241  geolimilem 7242  fsum0diaglem2 7264  fsum0diag2 7266  mulc1cncf 7286  efaddlem3 7347  efaddlem5 7349  efaddlem6 7350  efaddlem13 7357  efaddlem17 7361  efaddlem19 7363  efaddlem27 7371  efexpt 7379  abspef01tlub 7402  sinclt 7438  cosclt 7439  resinvalt 7440  recosvalt 7441  efi4pt 7442  resin4pt 7443  recos4pt 7444  resinclt 7445  recosclt 7446  sinnegt 7449  cosnegt 7450  efivalt 7454  efmivalt 7455  efeult 7456  sinsubt 7462  cossubt 7463  addsint 7464  subsint 7465  addcost 7466  subcost 7467  sincossqt 7468  sin2tt 7469  sin01bndlem2 7476  sin01bndlem3 7477  cos01bndlem2 7478  cos01bndlem3 7479  abseft 7491  demoivre 7492  demoivreALT 7493  znnen 7510  mulcn 7992  ablmul 8134  ipval2 8360  4ipval2 8361  4ipval3 8365  ipid 8366  ipcl 8368  ipcj 8370  ip1cnilem4 8379  ip1cnilem6 8381  cnph 8481  ipasslem2 8494  ipasslem4 8496  ipasslem8 8500  ipasslem9 8501  ipasslem11 8503  ubthlem7 8538  ubthlem8 8539  ubthlem9 8540  ubthlem10 8541  minveclem18 8565  sincolem 8667  sinperlem2 8689  sinper 8692  cosper 8693  efimpi 8700  sincosq1eq 8711  efgh 8720  efghgrpilem 8721  efif 8723  efif1lem4 8735  efielcirc 8741  shftefif1olem 8743  eff1lem 8745  eff1i 8746  effoi 8747  efper 8749  hhssnv 9136  pjthlem4 9224  pjthlem7 9227  spansncol 9493  homulasst 9730  lnfnmul 9975  riesz3 9997  mslb1 10608  2wsms 10609

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2699  ax-sep 2709  ax-nul 2716  ax-pow 2749  ax-pr 2786  ax-un 2873  ax-inf2 4641

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-reu 1654  df-rab 1655  df-v 1815  df-sbc 1945  df-csb 2006  df-dif 2053  df-un 2054  df-in 2055  df-ss 2057  df-pss 2059  df-nul 2285  df-if 2367  df-pw 2407  df-sn 2417  df-pr 2418  df-tp 2420  df-op 2421  df-uni 2509  df-int 2539  df-iun 2573  df-br 2626  df-opab 2673  df-tr 2687  df-eprel 2839  df-id 2842  df-po 2847  df-so 2857  df-fr 2924  df-we 2941  df-ord 2958  df-on 2959  df-lim 2960  df-suc 2961  df-om 3139  df-xp 3191  df-rel 3192  df-cnv 3193  df-co 3194  df-dm 3195  df-rn 3196  df-res 3197  df-ima 3198  df-fun 3199  df-fn 3200  df-f 3201  df-fv 3205  df-rdg 3939  df-opr 3972  df-oprab 3973  df-1st 4086  df-2nd 4087  df-1o 4140  df-oadd 4142  df-omul 4143  df-er 4268  df-ec 4270  df-qs 4273  df-ni 5019  df-pli 5020  df-mi 5021  df-lti 5022  df-plpq 5054  df-mpq 5055  df-enq 5056  df-nq 5057  df-plq 5058  df-mq 5059  df-rq 5060  df-ltq 5061  df-1q 5062  df-np 5105  df-1p 5106  df-plp 5107  df-mp 5108  df-ltp 5109  df-plpr 5183  df-mpr 5184  df-enr 5185  df-nr 5186  df-plr 5187  df-mr 5188  df-m1r 5192  df-c 5259  df-mul 5265

Copyright terms: Public domain