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

Theorem 00id 9666
Description:  0 is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013.)
Assertion
Ref Expression
00id  |-  ( 0  +  0 )  =  0

Proof of Theorem 00id
Dummy variables  y 
c are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0re 9507 . 2  |-  0  e.  RR
2 ax-rnegex 9474 . 2  |-  ( 0  e.  RR  ->  E. c  e.  RR  ( 0  +  c )  =  0 )
3 oveq2 6204 . . . . . . 7  |-  ( c  =  0  ->  (
0  +  c )  =  ( 0  +  0 ) )
43eqeq1d 2384 . . . . . 6  |-  ( c  =  0  ->  (
( 0  +  c )  =  0  <->  (
0  +  0 )  =  0 ) )
54biimpd 207 . . . . 5  |-  ( c  =  0  ->  (
( 0  +  c )  =  0  -> 
( 0  +  0 )  =  0 ) )
65adantld 465 . . . 4  |-  ( c  =  0  ->  (
( c  e.  RR  /\  ( 0  +  c )  =  0 )  ->  ( 0  +  0 )  =  0 ) )
7 ax-rrecex 9475 . . . . . . 7  |-  ( ( c  e.  RR  /\  c  =/=  0 )  ->  E. y  e.  RR  ( c  x.  y
)  =  1 )
87adantlr 712 . . . . . 6  |-  ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0
)  ->  E. y  e.  RR  ( c  x.  y )  =  1 )
9 simplll 757 . . . . . . . . . . 11  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  c  e.  RR )
109recnd 9533 . . . . . . . . . 10  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  c  e.  CC )
11 simprl 754 . . . . . . . . . . 11  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  y  e.  RR )
1211recnd 9533 . . . . . . . . . 10  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  y  e.  CC )
13 0cn 9499 . . . . . . . . . . 11  |-  0  e.  CC
14 mulass 9491 . . . . . . . . . . 11  |-  ( ( c  e.  CC  /\  y  e.  CC  /\  0  e.  CC )  ->  (
( c  x.  y
)  x.  0 )  =  ( c  x.  ( y  x.  0 ) ) )
1513, 14mp3an3 1311 . . . . . . . . . 10  |-  ( ( c  e.  CC  /\  y  e.  CC )  ->  ( ( c  x.  y )  x.  0 )  =  ( c  x.  ( y  x.  0 ) ) )
1610, 12, 15syl2anc 659 . . . . . . . . 9  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( (
c  x.  y )  x.  0 )  =  ( c  x.  (
y  x.  0 ) ) )
17 oveq1 6203 . . . . . . . . . . 11  |-  ( ( c  x.  y )  =  1  ->  (
( c  x.  y
)  x.  0 )  =  ( 1  x.  0 ) )
1813mulid2i 9510 . . . . . . . . . . 11  |-  ( 1  x.  0 )  =  0
1917, 18syl6eq 2439 . . . . . . . . . 10  |-  ( ( c  x.  y )  =  1  ->  (
( c  x.  y
)  x.  0 )  =  0 )
2019ad2antll 726 . . . . . . . . 9  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( (
c  x.  y )  x.  0 )  =  0 )
2116, 20eqtr3d 2425 . . . . . . . 8  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( c  x.  ( y  x.  0 ) )  =  0 )
2221oveq1d 6211 . . . . . . 7  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( (
c  x.  ( y  x.  0 ) )  +  0 )  =  ( 0  +  0 ) )
23 simpllr 758 . . . . . . . . . . . 12  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( 0  +  c )  =  0 )
2423oveq1d 6211 . . . . . . . . . . 11  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( (
0  +  c )  x.  ( y  x.  0 ) )  =  ( 0  x.  (
y  x.  0 ) ) )
25 remulcl 9488 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  RR  /\  0  e.  RR )  ->  ( y  x.  0 )  e.  RR )
261, 25mpan2 669 . . . . . . . . . . . . . 14  |-  ( y  e.  RR  ->  (
y  x.  0 )  e.  RR )
2726ad2antrl 725 . . . . . . . . . . . . 13  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( y  x.  0 )  e.  RR )
2827recnd 9533 . . . . . . . . . . . 12  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( y  x.  0 )  e.  CC )
29 adddir 9498 . . . . . . . . . . . . 13  |-  ( ( 0  e.  CC  /\  c  e.  CC  /\  (
y  x.  0 )  e.  CC )  -> 
( ( 0  +  c )  x.  (
y  x.  0 ) )  =  ( ( 0  x.  ( y  x.  0 ) )  +  ( c  x.  ( y  x.  0 ) ) ) )
3013, 29mp3an1 1309 . . . . . . . . . . . 12  |-  ( ( c  e.  CC  /\  ( y  x.  0 )  e.  CC )  ->  ( ( 0  +  c )  x.  ( y  x.  0 ) )  =  ( ( 0  x.  (
y  x.  0 ) )  +  ( c  x.  ( y  x.  0 ) ) ) )
3110, 28, 30syl2anc 659 . . . . . . . . . . 11  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( (
0  +  c )  x.  ( y  x.  0 ) )  =  ( ( 0  x.  ( y  x.  0 ) )  +  ( c  x.  ( y  x.  0 ) ) ) )
3224, 31eqtr3d 2425 . . . . . . . . . 10  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( 0  x.  ( y  x.  0 ) )  =  ( ( 0  x.  ( y  x.  0 ) )  +  ( c  x.  ( y  x.  0 ) ) ) )
3332oveq1d 6211 . . . . . . . . 9  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( (
0  x.  ( y  x.  0 ) )  +  0 )  =  ( ( ( 0  x.  ( y  x.  0 ) )  +  ( c  x.  (
y  x.  0 ) ) )  +  0 ) )
34 remulcl 9488 . . . . . . . . . . . . 13  |-  ( ( 0  e.  RR  /\  ( y  x.  0 )  e.  RR )  ->  ( 0  x.  ( y  x.  0 ) )  e.  RR )
351, 26, 34sylancr 661 . . . . . . . . . . . 12  |-  ( y  e.  RR  ->  (
0  x.  ( y  x.  0 ) )  e.  RR )
3635ad2antrl 725 . . . . . . . . . . 11  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( 0  x.  ( y  x.  0 ) )  e.  RR )
3736recnd 9533 . . . . . . . . . 10  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( 0  x.  ( y  x.  0 ) )  e.  CC )
38 remulcl 9488 . . . . . . . . . . . 12  |-  ( ( c  e.  RR  /\  ( y  x.  0 )  e.  RR )  ->  ( c  x.  ( y  x.  0 ) )  e.  RR )
399, 27, 38syl2anc 659 . . . . . . . . . . 11  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( c  x.  ( y  x.  0 ) )  e.  RR )
4039recnd 9533 . . . . . . . . . 10  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( c  x.  ( y  x.  0 ) )  e.  CC )
41 addass 9490 . . . . . . . . . . 11  |-  ( ( ( 0  x.  (
y  x.  0 ) )  e.  CC  /\  ( c  x.  (
y  x.  0 ) )  e.  CC  /\  0  e.  CC )  ->  ( ( ( 0  x.  ( y  x.  0 ) )  +  ( c  x.  (
y  x.  0 ) ) )  +  0 )  =  ( ( 0  x.  ( y  x.  0 ) )  +  ( ( c  x.  ( y  x.  0 ) )  +  0 ) ) )
4213, 41mp3an3 1311 . . . . . . . . . 10  |-  ( ( ( 0  x.  (
y  x.  0 ) )  e.  CC  /\  ( c  x.  (
y  x.  0 ) )  e.  CC )  ->  ( ( ( 0  x.  ( y  x.  0 ) )  +  ( c  x.  ( y  x.  0 ) ) )  +  0 )  =  ( ( 0  x.  (
y  x.  0 ) )  +  ( ( c  x.  ( y  x.  0 ) )  +  0 ) ) )
4337, 40, 42syl2anc 659 . . . . . . . . 9  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( (
( 0  x.  (
y  x.  0 ) )  +  ( c  x.  ( y  x.  0 ) ) )  +  0 )  =  ( ( 0  x.  ( y  x.  0 ) )  +  ( ( c  x.  (
y  x.  0 ) )  +  0 ) ) )
4433, 43eqtr2d 2424 . . . . . . . 8  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( (
0  x.  ( y  x.  0 ) )  +  ( ( c  x.  ( y  x.  0 ) )  +  0 ) )  =  ( ( 0  x.  ( y  x.  0 ) )  +  0 ) )
4526, 38sylan2 472 . . . . . . . . . . 11  |-  ( ( c  e.  RR  /\  y  e.  RR )  ->  ( c  x.  (
y  x.  0 ) )  e.  RR )
46 readdcl 9486 . . . . . . . . . . 11  |-  ( ( ( c  x.  (
y  x.  0 ) )  e.  RR  /\  0  e.  RR )  ->  ( ( c  x.  ( y  x.  0 ) )  +  0 )  e.  RR )
4745, 1, 46sylancl 660 . . . . . . . . . 10  |-  ( ( c  e.  RR  /\  y  e.  RR )  ->  ( ( c  x.  ( y  x.  0 ) )  +  0 )  e.  RR )
489, 11, 47syl2anc 659 . . . . . . . . 9  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( (
c  x.  ( y  x.  0 ) )  +  0 )  e.  RR )
49 readdcan 9665 . . . . . . . . . 10  |-  ( ( ( ( c  x.  ( y  x.  0 ) )  +  0 )  e.  RR  /\  0  e.  RR  /\  (
0  x.  ( y  x.  0 ) )  e.  RR )  -> 
( ( ( 0  x.  ( y  x.  0 ) )  +  ( ( c  x.  ( y  x.  0 ) )  +  0 ) )  =  ( ( 0  x.  (
y  x.  0 ) )  +  0 )  <-> 
( ( c  x.  ( y  x.  0 ) )  +  0 )  =  0 ) )
501, 49mp3an2 1310 . . . . . . . . 9  |-  ( ( ( ( c  x.  ( y  x.  0 ) )  +  0 )  e.  RR  /\  ( 0  x.  (
y  x.  0 ) )  e.  RR )  ->  ( ( ( 0  x.  ( y  x.  0 ) )  +  ( ( c  x.  ( y  x.  0 ) )  +  0 ) )  =  ( ( 0  x.  ( y  x.  0 ) )  +  0 )  <->  ( ( c  x.  ( y  x.  0 ) )  +  0 )  =  0 ) )
5148, 36, 50syl2anc 659 . . . . . . . 8  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( (
( 0  x.  (
y  x.  0 ) )  +  ( ( c  x.  ( y  x.  0 ) )  +  0 ) )  =  ( ( 0  x.  ( y  x.  0 ) )  +  0 )  <->  ( (
c  x.  ( y  x.  0 ) )  +  0 )  =  0 ) )
5244, 51mpbid 210 . . . . . . 7  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( (
c  x.  ( y  x.  0 ) )  +  0 )  =  0 )
5322, 52eqtr3d 2425 . . . . . 6  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( 0  +  0 )  =  0 )
548, 53rexlimddv 2878 . . . . 5  |-  ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0
)  ->  ( 0  +  0 )  =  0 )
5554expcom 433 . . . 4  |-  ( c  =/=  0  ->  (
( c  e.  RR  /\  ( 0  +  c )  =  0 )  ->  ( 0  +  0 )  =  0 ) )
566, 55pm2.61ine 2695 . . 3  |-  ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  ->  ( 0  +  0 )  =  0 )
5756rexlimiva 2870 . 2  |-  ( E. c  e.  RR  (
0  +  c )  =  0  ->  (
0  +  0 )  =  0 )
581, 2, 57mp2b 10 1  |-  ( 0  +  0 )  =  0
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1399    e. wcel 1826    =/= wne 2577   E.wrex 2733  (class class class)co 6196   CCcc 9401   RRcr 9402   0cc0 9403   1c1 9404    + caddc 9406    x. cmul 9408
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-resscn 9460  ax-1cn 9461  ax-icn 9462  ax-addcl 9463  ax-addrcl 9464  ax-mulcl 9465  ax-mulrcl 9466  ax-mulcom 9467  ax-addass 9468  ax-mulass 9469  ax-distr 9470  ax-i2m1 9471  ax-1ne0 9472  ax-1rid 9473  ax-rnegex 9474  ax-rrecex 9475  ax-cnre 9476  ax-pre-lttri 9477  ax-pre-lttrn 9478  ax-pre-ltadd 9479
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-nel 2580  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-mpt 4427  df-id 4709  df-po 4714  df-so 4715  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-ov 6199  df-er 7229  df-en 7436  df-dom 7437  df-sdom 7438  df-pnf 9541  df-mnf 9542  df-ltxr 9544
This theorem is referenced by:  mul02lem1  9667  mul02lem2  9668  addid1  9671  addid2  9674  negdiiOLD  9817  addgt0  9956  addgegt0  9957  addgtge0  9958  addge0  9959  add20  9982  recextlem2  10097  crne0  10445  10p10e20  10965  ser0  12062  faclbnd4lem3  12275  bcpasc  12301  relexpaddg  12888  fsumadd  13563  fsumrelem  13623  arisum  13673  sadcaddlem  14109  sadcadd  14110  sadadd2  14112  bezout  14182  nnnn0modprm0  14333  pcaddlem  14409  4sqlem19  14483  37prm  14608  139prm  14611  163prm  14612  317prm  14613  631prm  14614  1259lem1  14615  1259lem2  14616  1259lem3  14617  1259lem4  14618  2503lem1  14621  2503lem2  14622  2503lem3  14623  4001lem1  14625  4001lem2  14626  4001lem3  14627  4001lem4  14628  sylow1lem1  16735  psrbagaddcl  18133  psrbagaddclOLD  18134  mplcoe3  18241  mplcoe3OLD  18242  cnfld0  18555  reparphti  21582  itg1addlem4  22191  ibladdlem  22311  itgaddlem1  22314  iblabslem  22319  iblabs  22320  coeaddlem  22731  dcubic  23293  log2ublem3  23395  log2ub  23396  chtublem  23603  logfacrlim  23616  dchrisumlem1  23791  chpdifbndlem2  23856  vdgr0  25021  vdgr1a  25027  1kp2ke3k  25288  dip0r  25747  pythi  25882  normpythi  26176  ocsh  26318  0lnfn  27020  lnopeq0i  27042  nlelshi  27095  unierri  27139  probun  28541  fsumcube  29975  ismblfin  30220  itg2addnc  30235  ibladdnclem  30237  itgaddnclem1  30239  itgaddnclem2  30240  iblabsnclem  30244  iblabsnc  30245  iblmulc2nc  30246  ftc1anclem8  30263  ftc1anc  30264  bezoutr1  31089  stoweidlem44  31992  fourierdlem42  32097  fourierdlem103  32158  fourierdlem104  32159  sqwvfoura  32177  sqwvfourb  32178  relexpaddss  38223
  Copyright terms: Public domain W3C validator