Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  addid2 Structured version   Unicode version

 Description: 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.)
Assertion
Ref Expression

Proof of Theorem addid2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnegex 9247 . 2
2 cnegex 9247 . . . 4
32ad2antrl 709 . . 3
4 0cn 9084 . . . . . . . . . 10
5 addass 9077 . . . . . . . . . 10
64, 4, 5mp3an12 1269 . . . . . . . . 9
76adantr 452 . . . . . . . 8
873ad2ant3 980 . . . . . . 7
9 00id 9241 . . . . . . . . 9
109oveq1i 6091 . . . . . . . 8
11 simp1 957 . . . . . . . . . . 11
12 simp2l 983 . . . . . . . . . . 11
13 simp3l 985 . . . . . . . . . . 11
1411, 12, 13addassd 9110 . . . . . . . . . 10
15 simp2r 984 . . . . . . . . . . 11
1615oveq1d 6096 . . . . . . . . . 10
17 simp3r 986 . . . . . . . . . . 11
1817oveq2d 6097 . . . . . . . . . 10
1914, 16, 183eqtr3rd 2477 . . . . . . . . 9
20 addid1 9246 . . . . . . . . . 10
21203ad2ant1 978 . . . . . . . . 9
2219, 21eqtr3d 2470 . . . . . . . 8
2310, 22syl5eq 2480 . . . . . . 7
2422oveq2d 6097 . . . . . . 7
258, 23, 243eqtr3rd 2477 . . . . . 6
26253expia 1155 . . . . 5
2726exp3a 426 . . . 4
2827rexlimdv 2829 . . 3
293, 28mpd 15 . 2
301, 29rexlimddv 2834 1