![]() |
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 11214 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | |
4 | 1, 2, 3 | mp2an 691 | 1 ⊢ (𝐴 + 𝐵) ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 (class class class)co 7414 ℂcc 11130 + caddc 11135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-addcl 11192 |
This theorem depends on definitions: df-bi 206 df-an 396 |
This theorem is referenced by: eqneg 11958 2cn 12311 3cn 12317 4cn 12321 5cn 12324 6cn 12327 7cn 12330 8cn 12333 9cn 12336 nummac 12746 binom2i 14201 sqeqori 14203 crreczi 14216 nn0opthlem1 14253 nn0opth2i 14256 3dvds2dec 16303 mod2xnegi 17033 karatsuba 17046 pige3ALT 26447 eff1o 26476 1cubrlem 26766 1cubr 26767 bposlem8 27217 ax5seglem7 28739 ipidsq 30513 ip1ilem 30629 pythi 30653 normlem2 30914 normlem3 30915 normlem7 30919 normlem9 30921 bcseqi 30923 norm-ii-i 30940 normpythi 30945 normpari 30957 polid2i 30960 lnopunilem1 31813 lnophmlem2 31820 dpmul100 32614 dpadd3 32629 dpmul4 32631 ballotlem2 34098 hgt750lem2 34274 quad3 35264 faclimlem1 35327 itg2addnclem3 37135 sqmid3api 41829 235t711 41839 sn-0tie0 41966 fltnltalem 42058 areaquad 42616 resqrtvalex 43047 imsqrtvalex 43048 fourierswlem 45590 fouriersw 45591 2t6m3t4e0 47384 |
Copyright terms: Public domain | W3C validator |