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 ) |