![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > addcl | Structured version Visualization version GIF version |
Description: Alias for ax-addcl 10586, for naming consistency with addcli 10636. Use this theorem instead of ax-addcl 10586 or axaddcl 10562. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
addcl | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addcl 10586 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2111 (class class class)co 7135 ℂcc 10524 + caddc 10529 |
This theorem was proved from axioms: ax-addcl 10586 |
This theorem is referenced by: adddir 10621 0cn 10622 addcli 10636 addcld 10649 muladd11 10799 peano2cn 10801 muladd11r 10842 add4 10849 0cnALT2 10864 negeu 10865 pncan 10881 2addsub 10889 addsubeq4 10890 nppcan2 10906 pnpcan 10914 ppncan 10917 muladd 11061 mulsub 11072 recex 11261 muleqadd 11273 conjmul 11346 halfaddsubcl 11857 halfaddsub 11858 serf 13394 seradd 13408 sersub 13409 binom3 13581 bernneq 13586 lswccatn0lsw 13936 revccat 14119 2cshwcshw 14178 shftlem 14419 shftval2 14426 shftval5 14429 2shfti 14431 crre 14465 crim 14466 cjadd 14492 addcj 14499 sqabsadd 14634 absreimsq 14644 absreim 14645 abstri 14682 sqreulem 14711 sqreu 14712 addcn2 14942 o1add 14962 climadd 14980 clim2ser 15003 clim2ser2 15004 isermulc2 15006 isercolllem3 15015 summolem3 15063 summolem2a 15064 fsumcl 15082 fsummulc2 15131 fsumrelem 15154 binom 15177 isumsplit 15187 risefacval2 15356 risefaccl 15361 risefallfac 15370 risefacp1 15375 binomfallfac 15387 binomrisefac 15388 bpoly3 15404 efcj 15437 ef4p 15458 tanval3 15479 efi4p 15482 sinadd 15509 cosadd 15510 tanadd 15512 addsin 15515 demoivreALT 15546 opoe 15704 pythagtriplem4 16146 pythagtriplem12 16153 pythagtriplem14 16155 pythagtriplem16 16157 gzaddcl 16263 cnaddablx 18981 cnaddabl 18982 cncrng 20112 cnperf 23425 cnlmod 23745 cnstrcvs 23746 cncvs 23750 dvaddbr 24541 dvaddf 24545 dveflem 24582 plyaddcl 24817 plymulcl 24818 plysubcl 24819 coeaddlem 24846 dgrcolem1 24870 dgrcolem2 24871 quotlem 24896 quotcl2 24898 quotdgr 24899 sinperlem 25073 ptolemy 25089 tangtx 25098 sinkpi 25114 efif1olem2 25135 logrnaddcl 25166 logneg 25179 logimul 25205 cxpadd 25270 binom4 25436 atanf 25466 atanneg 25493 atancj 25496 efiatan 25498 atanlogaddlem 25499 atanlogadd 25500 atanlogsublem 25501 atanlogsub 25502 efiatan2 25503 2efiatan 25504 tanatan 25505 cosatan 25507 cosatanne0 25508 atantan 25509 atanbndlem 25511 atans2 25517 dvatan 25521 atantayl 25523 efrlim 25555 dfef2 25556 gamcvg2lem 25644 ftalem7 25664 prmorcht 25763 bposlem9 25876 lgsquad2lem1 25968 2sqlem2 26002 cncph 28602 hhssnv 29047 hoadddir 29587 superpos 30137 knoppcnlem8 33952 cos2h 35048 tan2h 35049 ftc1anclem3 35132 ftc1anclem7 35136 ftc1anclem8 35137 ftc1anc 35138 facp2 39347 fac2xp3 39385 fsumsermpt 42221 stirlinglem5 42720 stirlinglem7 42722 cnapbmcpd 43852 fmtnodvds 44061 opoeALTV 44201 mogoldbblem 44238 |
Copyright terms: Public domain | W3C validator |