Description: Closure law for addition in the real subfield of complex numbers. Axiom 6 of 23 for real and complex numbers, justified by theorem axaddrcl . Proofs should normally use readdcl instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-addrcl | |- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cA | |- A |
|
| 1 | cr | |- RR |
|
| 2 | 0 1 | wcel | |- A e. RR |
| 3 | cB | |- B |
|
| 4 | 3 1 | wcel | |- B e. RR |
| 5 | 2 4 | wa | |- ( A e. RR /\ B e. RR ) |
| 6 | caddc | |- + |
|
| 7 | 0 3 6 | co | |- ( A + B ) |
| 8 | 7 1 | wcel | |- ( A + B ) e. RR |
| 9 | 5 8 | wi | |- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR ) |