![]() |
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 10356 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | |
4 | 1, 2, 3 | mp2an 682 | 1 ⊢ (𝐴 + 𝐵) ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 (class class class)co 6924 ℂcc 10272 + caddc 10277 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-addcl 10334 |
This theorem depends on definitions: df-bi 199 df-an 387 |
This theorem is referenced by: eqneg 11097 2cn 11454 3cn 11460 4cn 11465 5cn 11469 6cn 11473 7cn 11477 8cn 11481 9cn 11485 nummac 11895 binom2i 13297 sqeqori 13299 crreczi 13312 nn0opthlem1 13377 nn0opth2i 13380 3dvds2dec 15465 mod2xnegi 16183 karatsuba 16196 pige3 24711 eff1o 24737 1cubrlem 25023 1cubr 25024 bposlem8 25472 ax5seglem7 26288 ipidsq 28141 ip1ilem 28257 pythi 28281 normlem2 28544 normlem3 28545 normlem7 28549 normlem9 28551 bcseqi 28553 norm-ii-i 28570 normpythi 28575 normpari 28587 polid2i 28590 lnopunilem1 29445 lnophmlem2 29452 dpmul100 30171 dpadd3 30186 dpmul4 30188 ballotlem2 31153 hgt750lem2 31336 quad3 32165 faclimlem1 32227 itg2addnclem3 34093 sqmid3api 38155 235t711 38163 areaquad 38770 fourierswlem 41384 fouriersw 41385 2t6m3t4e0 43151 |
Copyright terms: Public domain | W3C validator |