Description: 0 is a left identity for addition. This used to be one of our complex number axioms, until it was discovered that it was dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | addlid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnegex | |
|
2 | cnegex | |
|
3 | 2 | ad2antrl | |
4 | 0cn | |
|
5 | addass | |
|
6 | 4 4 5 | mp3an12 | |
7 | 6 | adantr | |
8 | 7 | 3ad2ant3 | |
9 | 00id | |
|
10 | 9 | oveq1i | |
11 | simp1 | |
|
12 | simp2l | |
|
13 | simp3l | |
|
14 | 11 12 13 | addassd | |
15 | simp2r | |
|
16 | 15 | oveq1d | |
17 | simp3r | |
|
18 | 17 | oveq2d | |
19 | 14 16 18 | 3eqtr3rd | |
20 | addrid | |
|
21 | 20 | 3ad2ant1 | |
22 | 19 21 | eqtr3d | |
23 | 10 22 | eqtrid | |
24 | 22 | oveq2d | |
25 | 8 23 24 | 3eqtr3rd | |
26 | 25 | 3expia | |
27 | 26 | expd | |
28 | 27 | rexlimdv | |
29 | 3 28 | mpd | |
30 | 1 29 | rexlimddv | |