Description: Reverse closure for addition: the second addend is real if the first addend is real and the sum is real. (Contributed by SN, 25-Apr-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | readdrcl2d.a | |- ( ph -> A e. RR ) |
|
| readdrcl2d.b | |- ( ph -> B e. CC ) |
||
| readdrcl2d.c | |- ( ph -> ( A + B ) e. RR ) |
||
| Assertion | readdrcl2d | |- ( ph -> B e. RR ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | readdrcl2d.a | |- ( ph -> A e. RR ) |
|
| 2 | readdrcl2d.b | |- ( ph -> B e. CC ) |
|
| 3 | readdrcl2d.c | |- ( ph -> ( A + B ) e. RR ) |
|
| 4 | 1 | recnd | |- ( ph -> A e. CC ) |
| 5 | 4 2 | pncan2d | |- ( ph -> ( ( A + B ) - A ) = B ) |
| 6 | 3 1 | resubcld | |- ( ph -> ( ( A + B ) - A ) e. RR ) |
| 7 | 5 6 | eqeltrrd | |- ( ph -> B e. RR ) |