Metamath Proof Explorer

Theorem addid1

Description: 0 is an additive identity. This used to be one of our complex number axioms, until it was found to be dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion addid1 
|- ( A e. CC -> ( A + 0 ) = A )

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 ax-rnegex 
 |-  ( 1 e. RR -> E. c e. RR ( 1 + c ) = 0 )
3 ax-1ne0 
 |-  1 =/= 0
4 oveq2 
 |-  ( c = 0 -> ( 1 + c ) = ( 1 + 0 ) )
5 4 eqeq1d 
 |-  ( c = 0 -> ( ( 1 + c ) = 0 <-> ( 1 + 0 ) = 0 ) )
6 5 biimpcd 
 |-  ( ( 1 + c ) = 0 -> ( c = 0 -> ( 1 + 0 ) = 0 ) )
7 oveq2 
 |-  ( ( 1 + 0 ) = 0 -> ( ( ( _i x. _i ) x. ( _i x. _i ) ) x. ( 1 + 0 ) ) = ( ( ( _i x. _i ) x. ( _i x. _i ) ) x. 0 ) )
8 ax-icn 
 |-  _i e. CC
9 8 8 mulcli 
 |-  ( _i x. _i ) e. CC
10 9 9 mulcli 
 |-  ( ( _i x. _i ) x. ( _i x. _i ) ) e. CC
11 ax-1cn 
 |-  1 e. CC
12 0cn 
 |-  0 e. CC
13 10 11 12 adddii 
 |-  ( ( ( _i x. _i ) x. ( _i x. _i ) ) x. ( 1 + 0 ) ) = ( ( ( ( _i x. _i ) x. ( _i x. _i ) ) x. 1 ) + ( ( ( _i x. _i ) x. ( _i x. _i ) ) x. 0 ) )
14 10 mulid1i 
 |-  ( ( ( _i x. _i ) x. ( _i x. _i ) ) x. 1 ) = ( ( _i x. _i ) x. ( _i x. _i ) )
15 mul01 
 |-  ( ( ( _i x. _i ) x. ( _i x. _i ) ) e. CC -> ( ( ( _i x. _i ) x. ( _i x. _i ) ) x. 0 ) = 0 )
16 10 15 ax-mp 
 |-  ( ( ( _i x. _i ) x. ( _i x. _i ) ) x. 0 ) = 0
17 ax-i2m1 
 |-  ( ( _i x. _i ) + 1 ) = 0
18 16 17 eqtr4i 
 |-  ( ( ( _i x. _i ) x. ( _i x. _i ) ) x. 0 ) = ( ( _i x. _i ) + 1 )
19 14 18 oveq12i 
 |-  ( ( ( ( _i x. _i ) x. ( _i x. _i ) ) x. 1 ) + ( ( ( _i x. _i ) x. ( _i x. _i ) ) x. 0 ) ) = ( ( ( _i x. _i ) x. ( _i x. _i ) ) + ( ( _i x. _i ) + 1 ) )
20 13 19 eqtri 
 |-  ( ( ( _i x. _i ) x. ( _i x. _i ) ) x. ( 1 + 0 ) ) = ( ( ( _i x. _i ) x. ( _i x. _i ) ) + ( ( _i x. _i ) + 1 ) )
21 20 16 eqeq12i 
 |-  ( ( ( ( _i x. _i ) x. ( _i x. _i ) ) x. ( 1 + 0 ) ) = ( ( ( _i x. _i ) x. ( _i x. _i ) ) x. 0 ) <-> ( ( ( _i x. _i ) x. ( _i x. _i ) ) + ( ( _i x. _i ) + 1 ) ) = 0 )
22 10 9 11 addassi 
 |-  ( ( ( ( _i x. _i ) x. ( _i x. _i ) ) + ( _i x. _i ) ) + 1 ) = ( ( ( _i x. _i ) x. ( _i x. _i ) ) + ( ( _i x. _i ) + 1 ) )
23 9 mulid1i 
 |-  ( ( _i x. _i ) x. 1 ) = ( _i x. _i )
24 23 oveq2i 
 |-  ( ( ( _i x. _i ) x. ( _i x. _i ) ) + ( ( _i x. _i ) x. 1 ) ) = ( ( ( _i x. _i ) x. ( _i x. _i ) ) + ( _i x. _i ) )
25 9 9 11 adddii 
 |-  ( ( _i x. _i ) x. ( ( _i x. _i ) + 1 ) ) = ( ( ( _i x. _i ) x. ( _i x. _i ) ) + ( ( _i x. _i ) x. 1 ) )
26 17 oveq2i 
 |-  ( ( _i x. _i ) x. ( ( _i x. _i ) + 1 ) ) = ( ( _i x. _i ) x. 0 )
27 mul01 
 |-  ( ( _i x. _i ) e. CC -> ( ( _i x. _i ) x. 0 ) = 0 )
28 9 27 ax-mp 
 |-  ( ( _i x. _i ) x. 0 ) = 0
29 26 28 eqtri 
 |-  ( ( _i x. _i ) x. ( ( _i x. _i ) + 1 ) ) = 0
30 25 29 eqtr3i 
 |-  ( ( ( _i x. _i ) x. ( _i x. _i ) ) + ( ( _i x. _i ) x. 1 ) ) = 0
31 24 30 eqtr3i 
 |-  ( ( ( _i x. _i ) x. ( _i x. _i ) ) + ( _i x. _i ) ) = 0
32 31 oveq1i 
 |-  ( ( ( ( _i x. _i ) x. ( _i x. _i ) ) + ( _i x. _i ) ) + 1 ) = ( 0 + 1 )
33 22 32 eqtr3i 
 |-  ( ( ( _i x. _i ) x. ( _i x. _i ) ) + ( ( _i x. _i ) + 1 ) ) = ( 0 + 1 )
34 00id 
 |-  ( 0 + 0 ) = 0
35 34 eqcomi 
 |-  0 = ( 0 + 0 )
36 33 35 eqeq12i 
 |-  ( ( ( ( _i x. _i ) x. ( _i x. _i ) ) + ( ( _i x. _i ) + 1 ) ) = 0 <-> ( 0 + 1 ) = ( 0 + 0 ) )
37 0re 
 |-  0 e. RR
38 readdcan 
 |-  ( ( 1 e. RR /\ 0 e. RR /\ 0 e. RR ) -> ( ( 0 + 1 ) = ( 0 + 0 ) <-> 1 = 0 ) )
39 1 37 37 38 mp3an 
 |-  ( ( 0 + 1 ) = ( 0 + 0 ) <-> 1 = 0 )
40 21 36 39 3bitri 
 |-  ( ( ( ( _i x. _i ) x. ( _i x. _i ) ) x. ( 1 + 0 ) ) = ( ( ( _i x. _i ) x. ( _i x. _i ) ) x. 0 ) <-> 1 = 0 )
41 7 40 sylib 
 |-  ( ( 1 + 0 ) = 0 -> 1 = 0 )
42 6 41 syl6 
 |-  ( ( 1 + c ) = 0 -> ( c = 0 -> 1 = 0 ) )
43 42 necon3d 
 |-  ( ( 1 + c ) = 0 -> ( 1 =/= 0 -> c =/= 0 ) )
44 3 43 mpi 
 |-  ( ( 1 + c ) = 0 -> c =/= 0 )
45 ax-rrecex 
 |-  ( ( c e. RR /\ c =/= 0 ) -> E. x e. RR ( c x. x ) = 1 )
46 44 45 sylan2 
 |-  ( ( c e. RR /\ ( 1 + c ) = 0 ) -> E. x e. RR ( c x. x ) = 1 )
47 simpr 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> A e. CC )
48 simplrl 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> x e. RR )
49 48 recnd 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> x e. CC )
50 47 49 mulcld 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( A x. x ) e. CC )
51 simplll 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> c e. RR )
52 51 recnd 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> c e. CC )
53 12 a1i 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> 0 e. CC )
54 50 52 53 adddid 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( ( A x. x ) x. ( c + 0 ) ) = ( ( ( A x. x ) x. c ) + ( ( A x. x ) x. 0 ) ) )
55 11 a1i 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> 1 e. CC )
56 55 52 53 addassd 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( ( 1 + c ) + 0 ) = ( 1 + ( c + 0 ) ) )
57 simpllr 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( 1 + c ) = 0 )
58 57 oveq1d 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( ( 1 + c ) + 0 ) = ( 0 + 0 ) )
59 56 58 eqtr3d 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( 1 + ( c + 0 ) ) = ( 0 + 0 ) )
60 34 59 57 3eqtr4a 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( 1 + ( c + 0 ) ) = ( 1 + c ) )
61 37 a1i 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> 0 e. RR )
62 51 61 readdcld 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( c + 0 ) e. RR )
63 1 a1i 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> 1 e. RR )
64 readdcan 
 |-  ( ( ( c + 0 ) e. RR /\ c e. RR /\ 1 e. RR ) -> ( ( 1 + ( c + 0 ) ) = ( 1 + c ) <-> ( c + 0 ) = c ) )
65 62 51 63 64 syl3anc 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( ( 1 + ( c + 0 ) ) = ( 1 + c ) <-> ( c + 0 ) = c ) )
66 60 65 mpbid 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( c + 0 ) = c )
67 66 oveq2d 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( ( A x. x ) x. ( c + 0 ) ) = ( ( A x. x ) x. c ) )
68 54 67 eqtr3d 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( ( ( A x. x ) x. c ) + ( ( A x. x ) x. 0 ) ) = ( ( A x. x ) x. c ) )
69 mul31 
 |-  ( ( A e. CC /\ x e. CC /\ c e. CC ) -> ( ( A x. x ) x. c ) = ( ( c x. x ) x. A ) )
70 47 49 52 69 syl3anc 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( ( A x. x ) x. c ) = ( ( c x. x ) x. A ) )
71 simplrr 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( c x. x ) = 1 )
72 71 oveq1d 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( ( c x. x ) x. A ) = ( 1 x. A ) )
73 47 mulid2d 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( 1 x. A ) = A )
74 70 72 73 3eqtrd 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( ( A x. x ) x. c ) = A )
75 mul01 
 |-  ( ( A x. x ) e. CC -> ( ( A x. x ) x. 0 ) = 0 )
76 50 75 syl 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( ( A x. x ) x. 0 ) = 0 )
77 74 76 oveq12d 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( ( ( A x. x ) x. c ) + ( ( A x. x ) x. 0 ) ) = ( A + 0 ) )
78 68 77 74 3eqtr3d 
 |-  ( ( ( ( c e. RR /\ ( 1 + c ) = 0 ) /\ ( x e. RR /\ ( c x. x ) = 1 ) ) /\ A e. CC ) -> ( A + 0 ) = A )
79 78 exp42 
 |-  ( ( c e. RR /\ ( 1 + c ) = 0 ) -> ( x e. RR -> ( ( c x. x ) = 1 -> ( A e. CC -> ( A + 0 ) = A ) ) ) )
80 79 rexlimdv 
 |-  ( ( c e. RR /\ ( 1 + c ) = 0 ) -> ( E. x e. RR ( c x. x ) = 1 -> ( A e. CC -> ( A + 0 ) = A ) ) )
81 46 80 mpd 
 |-  ( ( c e. RR /\ ( 1 + c ) = 0 ) -> ( A e. CC -> ( A + 0 ) = A ) )
82 81 rexlimiva 
 |-  ( E. c e. RR ( 1 + c ) = 0 -> ( A e. CC -> ( A + 0 ) = A ) )
83 1 2 82 mp2b 
 |-  ( A e. CC -> ( A + 0 ) = A )