Metamath Proof Explorer
Description: Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016)
|
|
Ref |
Expression |
|
Hypotheses |
recld.1 |
|
|
|
readdd.2 |
|
|
Assertion |
resubd |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
recld.1 |
|
2 |
|
readdd.2 |
|
3 |
|
resub |
|
4 |
1 2 3
|
syl2anc |
|