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

Theorem addid1 8868
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.)
Assertion
Ref Expression
addid1  |-  ( A  e.  CC  ->  ( A  +  0 )  =  A )

Proof of Theorem addid1
StepHypRef Expression
1 1re 8714 . 2  |-  1  e.  RR
2 ax-rnegex 8685 . 2  |-  ( 1  e.  RR  ->  E. c  e.  RR  ( 1  +  c )  =  0 )
3 ax-1ne0 8683 . . . . . 6  |-  1  =/=  0
4 oveq2 5715 . . . . . . . . . 10  |-  ( c  =  0  ->  (
1  +  c )  =  ( 1  +  0 ) )
54eqeq1d 2261 . . . . . . . . 9  |-  ( c  =  0  ->  (
( 1  +  c )  =  0  <->  (
1  +  0 )  =  0 ) )
65biimpcd 217 . . . . . . . 8  |-  ( ( 1  +  c )  =  0  ->  (
c  =  0  -> 
( 1  +  0 )  =  0 ) )
7 oveq2 5715 . . . . . . . . 9  |-  ( ( 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 8673 . . . . . . . . . . . . . . 15  |-  _i  e.  CC
98, 8mulcli 8719 . . . . . . . . . . . . . 14  |-  ( _i  x.  _i )  e.  CC
109, 9mulcli 8719 . . . . . . . . . . . . 13  |-  ( ( _i  x.  _i )  x.  ( _i  x.  _i ) )  e.  CC
11 ax-1cn 8672 . . . . . . . . . . . . 13  |-  1  e.  CC
12 0cn 8708 . . . . . . . . . . . . 13  |-  0  e.  CC
1310, 11, 12adddii 8724 . . . . . . . . . . . 12  |-  ( ( ( _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 ) )
1410mulid1i 8716 . . . . . . . . . . . . 13  |-  ( ( ( _i  x.  _i )  x.  ( _i  x.  _i ) )  x.  1 )  =  ( ( _i  x.  _i )  x.  ( _i  x.  _i ) )
15 mul01 8867 . . . . . . . . . . . . . . 15  |-  ( ( ( _i  x.  _i )  x.  ( _i  x.  _i ) )  e.  CC  ->  ( (
( _i  x.  _i )  x.  ( _i  x.  _i ) )  x.  0 )  =  0 )
1610, 15ax-mp 10 . . . . . . . . . . . . . 14  |-  ( ( ( _i  x.  _i )  x.  ( _i  x.  _i ) )  x.  0 )  =  0
17 ax-i2m1 8682 . . . . . . . . . . . . . 14  |-  ( ( _i  x.  _i )  +  1 )  =  0
1816, 17eqtr4i 2276 . . . . . . . . . . . . 13  |-  ( ( ( _i  x.  _i )  x.  ( _i  x.  _i ) )  x.  0 )  =  ( ( _i  x.  _i )  +  1 )
1914, 18oveq12i 5719 . . . . . . . . . . . 12  |-  ( ( ( ( _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 ) )
2013, 19eqtri 2273 . . . . . . . . . . 11  |-  ( ( ( _i  x.  _i )  x.  ( _i  x.  _i ) )  x.  ( 1  +  0 ) )  =  ( ( ( _i  x.  _i )  x.  (
_i  x.  _i )
)  +  ( ( _i  x.  _i )  +  1 ) )
2120, 16eqeq12i 2266 . . . . . . . . . 10  |-  ( ( ( ( _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 )
2210, 9, 11addassi 8722 . . . . . . . . . . . 12  |-  ( ( ( ( _i  x.  _i )  x.  (
_i  x.  _i )
)  +  ( _i  x.  _i ) )  +  1 )  =  ( ( ( _i  x.  _i )  x.  ( _i  x.  _i ) )  +  ( ( _i  x.  _i )  +  1 ) )
239mulid1i 8716 . . . . . . . . . . . . . . 15  |-  ( ( _i  x.  _i )  x.  1 )  =  ( _i  x.  _i )
2423oveq2i 5718 . . . . . . . . . . . . . 14  |-  ( ( ( _i  x.  _i )  x.  ( _i  x.  _i ) )  +  ( ( _i  x.  _i )  x.  1
) )  =  ( ( ( _i  x.  _i )  x.  (
_i  x.  _i )
)  +  ( _i  x.  _i ) )
259, 9, 11adddii 8724 . . . . . . . . . . . . . . 15  |-  ( ( _i  x.  _i )  x.  ( ( _i  x.  _i )  +  1 ) )  =  ( ( ( _i  x.  _i )  x.  ( _i  x.  _i ) )  +  ( ( _i  x.  _i )  x.  1 ) )
2617oveq2i 5718 . . . . . . . . . . . . . . . 16  |-  ( ( _i  x.  _i )  x.  ( ( _i  x.  _i )  +  1 ) )  =  ( ( _i  x.  _i )  x.  0
)
27 mul01 8867 . . . . . . . . . . . . . . . . 17  |-  ( ( _i  x.  _i )  e.  CC  ->  (
( _i  x.  _i )  x.  0 )  =  0 )
289, 27ax-mp 10 . . . . . . . . . . . . . . . 16  |-  ( ( _i  x.  _i )  x.  0 )  =  0
2926, 28eqtri 2273 . . . . . . . . . . . . . . 15  |-  ( ( _i  x.  _i )  x.  ( ( _i  x.  _i )  +  1 ) )  =  0
3025, 29eqtr3i 2275 . . . . . . . . . . . . . 14  |-  ( ( ( _i  x.  _i )  x.  ( _i  x.  _i ) )  +  ( ( _i  x.  _i )  x.  1
) )  =  0
3124, 30eqtr3i 2275 . . . . . . . . . . . . 13  |-  ( ( ( _i  x.  _i )  x.  ( _i  x.  _i ) )  +  ( _i  x.  _i ) )  =  0
3231oveq1i 5717 . . . . . . . . . . . 12  |-  ( ( ( ( _i  x.  _i )  x.  (
_i  x.  _i )
)  +  ( _i  x.  _i ) )  +  1 )  =  ( 0  +  1 )
3322, 32eqtr3i 2275 . . . . . . . . . . 11  |-  ( ( ( _i  x.  _i )  x.  ( _i  x.  _i ) )  +  ( ( _i  x.  _i )  +  1
) )  =  ( 0  +  1 )
34 00id 8863 . . . . . . . . . . . 12  |-  ( 0  +  0 )  =  0
3534eqcomi 2257 . . . . . . . . . . 11  |-  0  =  ( 0  +  0 )
3633, 35eqeq12i 2266 . . . . . . . . . 10  |-  ( ( ( ( _i  x.  _i )  x.  (
_i  x.  _i )
)  +  ( ( _i  x.  _i )  +  1 ) )  =  0  <->  ( 0  +  1 )  =  ( 0  +  0 ) )
37 0re 8715 . . . . . . . . . . 11  |-  0  e.  RR
38 readdcan 8862 . . . . . . . . . . 11  |-  ( ( 1  e.  RR  /\  0  e.  RR  /\  0  e.  RR )  ->  (
( 0  +  1 )  =  ( 0  +  0 )  <->  1  = 
0 ) )
391, 37, 37, 38mp3an 1282 . . . . . . . . . 10  |-  ( ( 0  +  1 )  =  ( 0  +  0 )  <->  1  = 
0 )
4021, 36, 393bitri 264 . . . . . . . . 9  |-  ( ( ( ( _i  x.  _i )  x.  (
_i  x.  _i )
)  x.  ( 1  +  0 ) )  =  ( ( ( _i  x.  _i )  x.  ( _i  x.  _i ) )  x.  0 )  <->  1  =  0 )
417, 40sylib 190 . . . . . . . 8  |-  ( ( 1  +  0 )  =  0  ->  1  =  0 )
426, 41syl6 31 . . . . . . 7  |-  ( ( 1  +  c )  =  0  ->  (
c  =  0  -> 
1  =  0 ) )
4342necon3d 2450 . . . . . 6  |-  ( ( 1  +  c )  =  0  ->  (
1  =/=  0  -> 
c  =/=  0 ) )
443, 43mpi 18 . . . . 5  |-  ( ( 1  +  c )  =  0  ->  c  =/=  0 )
45 ax-rrecex 8686 . . . . 5  |-  ( ( c  e.  RR  /\  c  =/=  0 )  ->  E. x  e.  RR  ( c  x.  x
)  =  1 )
4644, 45sylan2 462 . . . 4  |-  ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  ->  E. x  e.  RR  ( c  x.  x
)  =  1 )
47 simpr 449 . . . . . . . . . 10  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  A  e.  CC )
48 simplrl 739 . . . . . . . . . . 11  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  x  e.  RR )
4948recnd 8738 . . . . . . . . . 10  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  x  e.  CC )
5047, 49mulcld 8732 . . . . . . . . 9  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  ( A  x.  x )  e.  CC )
51 simplll 737 . . . . . . . . . 10  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  c  e.  RR )
5251recnd 8738 . . . . . . . . 9  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  c  e.  CC )
5312a1i 12 . . . . . . . . 9  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  0  e.  CC )
5450, 52, 53adddid 8736 . . . . . . . 8  |-  ( ( ( ( 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 ) ) )
5511a1i 12 . . . . . . . . . . . . 13  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  1  e.  CC )
5655, 52, 53addassd 8734 . . . . . . . . . . . 12  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  (
( 1  +  c )  +  0 )  =  ( 1  +  ( c  +  0 ) ) )
57 simpllr 738 . . . . . . . . . . . . 13  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  (
1  +  c )  =  0 )
5857oveq1d 5722 . . . . . . . . . . . 12  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  (
( 1  +  c )  +  0 )  =  ( 0  +  0 ) )
5956, 58eqtr3d 2287 . . . . . . . . . . 11  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  (
1  +  ( c  +  0 ) )  =  ( 0  +  0 ) )
6034, 59, 573eqtr4a 2311 . . . . . . . . . 10  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  (
1  +  ( c  +  0 ) )  =  ( 1  +  c ) )
6137a1i 12 . . . . . . . . . . . 12  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  0  e.  RR )
6251, 61readdcld 8739 . . . . . . . . . . 11  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  (
c  +  0 )  e.  RR )
631a1i 12 . . . . . . . . . . 11  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  1  e.  RR )
64 readdcan 8862 . . . . . . . . . . 11  |-  ( ( ( c  +  0 )  e.  RR  /\  c  e.  RR  /\  1  e.  RR )  ->  (
( 1  +  ( c  +  0 ) )  =  ( 1  +  c )  <->  ( c  +  0 )  =  c ) )
6562, 51, 63, 64syl3anc 1187 . . . . . . . . . 10  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  (
( 1  +  ( c  +  0 ) )  =  ( 1  +  c )  <->  ( c  +  0 )  =  c ) )
6660, 65mpbid 203 . . . . . . . . 9  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  (
c  +  0 )  =  c )
6766oveq2d 5723 . . . . . . . 8  |-  ( ( ( ( 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 ) )
6854, 67eqtr3d 2287 . . . . . . 7  |-  ( ( ( ( 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 8856 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  x  e.  CC  /\  c  e.  CC )  ->  (
( A  x.  x
)  x.  c )  =  ( ( c  x.  x )  x.  A ) )
7047, 49, 52, 69syl3anc 1187 . . . . . . . . 9  |-  ( ( ( ( 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 740 . . . . . . . . . 10  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  (
c  x.  x )  =  1 )
7271oveq1d 5722 . . . . . . . . 9  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  (
( c  x.  x
)  x.  A )  =  ( 1  x.  A ) )
7347mulid2d 8730 . . . . . . . . 9  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  (
1  x.  A )  =  A )
7470, 72, 733eqtrd 2289 . . . . . . . 8  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  (
( A  x.  x
)  x.  c )  =  A )
75 mul01 8867 . . . . . . . . 9  |-  ( ( A  x.  x )  e.  CC  ->  (
( A  x.  x
)  x.  0 )  =  0 )
7650, 75syl 17 . . . . . . . 8  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  (
( A  x.  x
)  x.  0 )  =  0 )
7774, 76oveq12d 5725 . . . . . . 7  |-  ( ( ( ( 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 ) )
7868, 77, 743eqtr3d 2293 . . . . . 6  |-  ( ( ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  /\  (
x  e.  RR  /\  ( c  x.  x
)  =  1 ) )  /\  A  e.  CC )  ->  ( A  +  0 )  =  A )
7978exp42 597 . . . . 5  |-  ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  ->  ( x  e.  RR  ->  ( (
c  x.  x )  =  1  ->  ( A  e.  CC  ->  ( A  +  0 )  =  A ) ) ) )
8079rexlimdv 2626 . . . 4  |-  ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  ->  ( E. x  e.  RR  ( c  x.  x )  =  1  ->  ( A  e.  CC  ->  ( A  +  0 )  =  A ) ) )
8146, 80mpd 16 . . 3  |-  ( ( c  e.  RR  /\  ( 1  +  c )  =  0 )  ->  ( A  e.  CC  ->  ( A  +  0 )  =  A ) )
8281rexlimiva 2622 . 2  |-  ( E. c  e.  RR  (
1  +  c )  =  0  ->  ( A  e.  CC  ->  ( A  +  0 )  =  A ) )
831, 2, 82mp2b 11 1  |-  ( A  e.  CC  ->  ( A  +  0 )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360    = wceq 1619    e. wcel 1621    =/= wne 2412   E.wrex 2508  (class class class)co 5707   CCcc 8612   RRcr 8613   0cc0 8614   1c1 8615   _ici 8616    + caddc 8617    x. cmul 8619
This theorem is referenced by:  cnegex  8869  addid2  8871  addcan2  8873  addid1i  8875  addid1d  8888  subid  8939  subid1  8940  shftval3  11412  reim0  11444  isercolllem3  11979  fsumcvg  12024  summolem2a  12027  ovolicc1  18669  relexpadd  23135  brbtwn2  23636  axsegconlem1  23648  ax5seglem4  23663  axeuclid  23694  axcontlem2  23696  axcontlem4  23698
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4035  ax-nul 4043  ax-pow 4079  ax-pr 4105  ax-un 4400  ax-resscn 8671  ax-1cn 8672  ax-icn 8673  ax-addcl 8674  ax-addrcl 8675  ax-mulcl 8676  ax-mulrcl 8677  ax-mulcom 8678  ax-addass 8679  ax-mulass 8680  ax-distr 8681  ax-i2m1 8682  ax-1ne0 8683  ax-1rid 8684  ax-rnegex 8685  ax-rrecex 8686  ax-cnre 8687  ax-pre-lttri 8688  ax-pre-lttrn 8689  ax-pre-ltadd 8690
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-nel 2415  df-ral 2511  df-rex 2512  df-rab 2514  df-v 2727  df-sbc 2920  df-csb 3007  df-dif 3078  df-un 3080  df-in 3082  df-ss 3086  df-nul 3360  df-if 3468  df-pw 3529  df-sn 3547  df-pr 3548  df-op 3550  df-uni 3725  df-br 3918  df-opab 3972  df-mpt 3973  df-id 4199  df-po 4204  df-so 4205  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-fun 4599  df-fn 4600  df-f 4601  df-f1 4602  df-fo 4603  df-f1o 4604  df-fv 4605  df-ov 5710  df-er 6543  df-en 6747  df-dom 6748  df-sdom 6749  df-pnf 8746  df-mnf 8747  df-ltxr 8749
  Copyright terms: Public domain W3C validator