![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > readdcli | Structured version Visualization version GIF version |
Description: Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.) |
Ref | Expression |
---|---|
recni.1 | ⊢ 𝐴 ∈ ℝ |
axri.2 | ⊢ 𝐵 ∈ ℝ |
Ref | Expression |
---|---|
readdcli | ⊢ (𝐴 + 𝐵) ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recni.1 | . 2 ⊢ 𝐴 ∈ ℝ | |
2 | axri.2 | . 2 ⊢ 𝐵 ∈ ℝ | |
3 | readdcl 11189 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | |
4 | 1, 2, 3 | mp2an 690 | 1 ⊢ (𝐴 + 𝐵) ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 (class class class)co 7405 ℝcr 11105 + caddc 11109 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-addrcl 11167 |
This theorem depends on definitions: df-bi 206 df-an 397 |
This theorem is referenced by: resubcli 11518 eqneg 11930 ledivp1i 12135 ltdivp1i 12136 nnne0 12242 2re 12282 3re 12288 4re 12292 5re 12295 6re 12298 7re 12301 8re 12304 9re 12307 10re 12692 numltc 12699 nn0opthlem2 14225 hashunlei 14381 hashge2el2dif 14437 abs3lemi 15353 ef01bndlem 16123 divalglem6 16337 log2ub 26443 mumullem2 26673 bposlem8 26783 dchrvmasumlem2 26990 ex-fl 29689 norm-ii-i 30377 norm3lem 30389 nmoptrii 31334 bdophsi 31336 unierri 31344 staddi 31486 stadd3i 31488 dp2ltc 32040 dpmul4 32067 ballotlem2 33475 hgt750lem 33651 poimirlem16 36492 itg2addnclem3 36529 fdc 36601 remul02 41274 sn-0tie0 41308 pellqrex 41602 stirlinglem11 44786 fouriersw 44933 zm1nn 45996 evengpoap3 46453 |
Copyright terms: Public domain | W3C validator |