Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  addid2 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

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnegex 9009 . 2
2 cnegex 9009 . . . . . 6
32ad2antrl 708 . . . . 5
4 0cn 8847 . . . . . . . . . . . 12
5 addass 8840 . . . . . . . . . . . 12
64, 4, 5mp3an12 1267 . . . . . . . . . . 11
76adantr 451 . . . . . . . . . 10
873ad2ant3 978 . . . . . . . . 9
9 00id 9003 . . . . . . . . . . 11
109oveq1i 5884 . . . . . . . . . 10
11 simp1 955 . . . . . . . . . . . . 13
12 simp2l 981 . . . . . . . . . . . . 13
13 simp3l 983 . . . . . . . . . . . . 13
1411, 12, 13addassd 8873 . . . . . . . . . . . 12
15 simp2r 982 . . . . . . . . . . . . 13
1615oveq1d 5889 . . . . . . . . . . . 12
17 simp3r 984 . . . . . . . . . . . . 13
1817oveq2d 5890 . . . . . . . . . . . 12
1914, 16, 183eqtr3rd 2337 . . . . . . . . . . 11
20 addid1 9008 . . . . . . . . . . . 12
21203ad2ant1 976 . . . . . . . . . . 11
2219, 21eqtr3d 2330 . . . . . . . . . 10
2310, 22syl5eq 2340 . . . . . . . . 9
2422oveq2d 5890 . . . . . . . . 9
258, 23, 243eqtr3rd 2337 . . . . . . . 8
26253expia 1153 . . . . . . 7
2726exp3a 425 . . . . . 6
2827rexlimdv 2679 . . . . 5
293, 28mpd 14 . . . 4
3029exp32 588 . . 3
3130rexlimdv 2679 . 2
321, 31mpd 14 1