![]() |
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 10306 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | |
4 | 1, 2, 3 | mp2an 684 | 1 ⊢ (𝐴 + 𝐵) ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2157 (class class class)co 6878 ℂcc 10222 + caddc 10227 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-addcl 10284 |
This theorem depends on definitions: df-bi 199 df-an 386 |
This theorem is referenced by: eqneg 11037 2cn 11388 3cn 11394 4cn 11399 5cn 11403 6cn 11407 7cn 11411 8cn 11415 9cn 11419 nummac 11829 binom2i 13228 sqeqori 13230 crreczi 13243 nn0opthlem1 13308 nn0opth2i 13311 3dvds2dec 15393 mod2xnegi 16108 karatsuba 16121 pige3 24611 eff1o 24637 1cubrlem 24920 1cubr 24921 bposlem8 25368 ax5seglem7 26172 ipidsq 28090 ip1ilem 28206 pythi 28230 normlem2 28493 normlem3 28494 normlem7 28498 normlem9 28500 bcseqi 28502 norm-ii-i 28519 normpythi 28524 normpari 28536 polid2i 28539 lnopunilem1 29394 lnophmlem2 29401 dpmul100 30121 dpadd3 30136 dpmul4 30138 ballotlem2 31067 hgt750lem2 31250 quad3 32079 faclimlem1 32143 itg2addnclem3 33951 sqmid3api 37994 235t711 38002 areaquad 38586 fourierswlem 41190 fouriersw 41191 2t6m3t4e0 42925 |
Copyright terms: Public domain | W3C validator |