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 10018 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | |
4 | 1, 2, 3 | mp2an 708 | 1 ⊢ (𝐴 + 𝐵) ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1990 (class class class)co 6650 ℂcc 9934 + caddc 9939 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-addcl 9996 |
This theorem depends on definitions: df-bi 197 df-an 386 |
This theorem is referenced by: eqneg 10745 nummac 11558 binom2i 12974 sqeqori 12976 crreczi 12989 nn0opthlem1 13055 nn0opth2i 13058 3dvds2dec 15056 3dvds2decOLD 15057 mod2xnegi 15775 karatsuba 15792 karatsubaOLD 15793 pige3 24269 eff1o 24295 1cubrlem 24568 1cubr 24569 bposlem8 25016 ax5seglem7 25815 ipidsq 27565 ip1ilem 27681 pythi 27705 normlem2 27968 normlem3 27969 normlem7 27973 normlem9 27975 bcseqi 27977 norm-ii-i 27994 normpythi 27999 normpari 28011 polid2i 28014 lnopunilem1 28869 lnophmlem2 28876 dpmul100 29605 dpadd3 29620 dpmul4 29622 ballotlem2 30550 hgt750lem2 30730 quad3 31564 faclimlem1 31629 itg2addnclem3 33463 areaquad 37802 fourierswlem 40447 fouriersw 40448 2t6m3t4e0 42126 |
Copyright terms: Public domain | W3C validator |