Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > addcli | Structured version Visualization version GIF version |
Description: Closure law for addition. (Contributed by NM, 23-Nov-1994.) |
Ref | Expression |
---|---|
axi.1 | ⊢ 𝐴 ∈ ℂ |
axi.2 | ⊢ 𝐵 ∈ ℂ |
Ref | Expression |
---|---|
addcli | ⊢ (𝐴 + 𝐵) ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axi.1 | . 2 ⊢ 𝐴 ∈ ℂ | |
2 | axi.2 | . 2 ⊢ 𝐵 ∈ ℂ | |
3 | addcl 10607 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | |
4 | 1, 2, 3 | mp2an 688 | 1 ⊢ (𝐴 + 𝐵) ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 (class class class)co 7145 ℂcc 10523 + caddc 10528 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-addcl 10585 |
This theorem depends on definitions: df-bi 208 df-an 397 |
This theorem is referenced by: eqneg 11348 2cn 11700 3cn 11706 4cn 11710 5cn 11713 6cn 11716 7cn 11719 8cn 11722 9cn 11725 nummac 12131 binom2i 13562 sqeqori 13564 crreczi 13577 nn0opthlem1 13616 nn0opth2i 13619 3dvds2dec 15670 mod2xnegi 16395 karatsuba 16408 pige3ALT 25032 eff1o 25060 1cubrlem 25346 1cubr 25347 bposlem8 25794 ax5seglem7 26648 ipidsq 28414 ip1ilem 28530 pythi 28554 normlem2 28815 normlem3 28816 normlem7 28820 normlem9 28822 bcseqi 28824 norm-ii-i 28841 normpythi 28846 normpari 28858 polid2i 28861 lnopunilem1 29714 lnophmlem2 29721 dpmul100 30500 dpadd3 30515 dpmul4 30517 ballotlem2 31645 hgt750lem2 31822 quad3 32810 faclimlem1 32872 itg2addnclem3 34826 sqmid3api 39047 235t711 39055 fltnltalem 39152 areaquad 39701 fourierswlem 42392 fouriersw 42393 2t6m3t4e0 44324 |
Copyright terms: Public domain | W3C validator |