Metamath Proof Explorer


Theorem readdid1addid2d

Description: Given some real number B where A acts like a right additive identity, derive that A is a left additive identity. Note that the hypothesis is weaker than proving that A is a right additive identity (for all numbers). Although, if there is a right additive identity, then by readdcan , A is the right additive identity. (Contributed by Steven Nguyen, 14-Jan-2023)

Ref Expression
Hypotheses readdid1addid2d.a φ A
readdid1addid2d.b φ B
readdid1addid2d.1 φ B + A = B
Assertion readdid1addid2d φ C A + C = C

Proof

Step Hyp Ref Expression
1 readdid1addid2d.a φ A
2 readdid1addid2d.b φ B
3 readdid1addid2d.1 φ B + A = B
4 2 adantr φ C B
5 4 recnd φ C B
6 1 adantr φ C A
7 6 recnd φ C A
8 simpr φ C C
9 8 recnd φ C C
10 5 7 9 addassd φ C B + A + C = B + A + C
11 3 adantr φ C B + A = B
12 11 oveq1d φ C B + A + C = B + C
13 10 12 eqtr3d φ C B + A + C = B + C
14 6 8 readdcld φ C A + C
15 readdcan A + C C B B + A + C = B + C A + C = C
16 14 8 4 15 syl3anc φ C B + A + C = B + C A + C = C
17 13 16 mpbid φ C A + C = C