| 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 11115 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | |
| 4 | 1, 2, 3 | mp2an 699 | 1 ⊢ (𝐴 + 𝐵) ∈ ℂ |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2121 (class class class)co 7360 ℂcc 11031 + caddc 11036 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-addcl 11093 |
| This theorem depends on definitions: df-bi 209 df-an 398 |
| This theorem is referenced by: eqneg 11870 2cn 12251 3cn 12257 4cn 12261 5cn 12264 6cn 12267 7cn 12270 8cn 12273 9cn 12276 nummac 12684 binom2i 14169 sqeqori 14171 crreczi 14185 nn0opthlem1 14225 nn0opth2i 14228 3dvds2dec 16297 mod2xnegi 17037 karatsuba 17049 pige3ALT 26506 eff1o 26535 1cubrlem 26827 1cubr 26828 bposlem8 27276 ax5seglem7 29026 ipidsq 30803 ip1ilem 30919 pythi 30943 normlem2 31204 normlem3 31205 normlem7 31209 normlem9 31211 bcseqi 31213 norm-ii-i 31230 normpythi 31235 normpari 31247 polid2i 31250 lnopunilem1 32103 lnophmlem2 32110 dpmul100 32979 dpadd3 32994 dpmul4 32996 cos9thpiminplylem4 33981 cos9thpiminplylem5 33982 ballotlem2 34685 hgt750lem2 34848 quad3 35913 faclimlem1 35986 itg2addnclem3 38055 sqmid3api 42775 235t711 42797 sn-0tie0 42956 fltnltalem 43127 areaquad 43676 resqrtvalex 44104 imsqrtvalex 44105 fourierswlem 46687 fouriersw 46688 2t6m3t4e0 48853 |
| Copyright terms: Public domain | W3C validator |