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

Theorem 00id 9759
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 9594 . 2  |-  0  e.  RR
2 ax-rnegex 9561 . 2  |-  ( 0  e.  RR  ->  E. c  e.  RR  ( 0  +  c )  =  0 )
3 oveq2 6257 . . . . . . 7  |-  ( c  =  0  ->  (
0  +  c )  =  ( 0  +  0 ) )
43eqeq1d 2430 . . . . . 6  |-  ( c  =  0  ->  (
( 0  +  c )  =  0  <->  (
0  +  0 )  =  0 ) )
54biimpd 210 . . . . 5  |-  ( c  =  0  ->  (
( 0  +  c )  =  0  -> 
( 0  +  0 )  =  0 ) )
65adantld 468 . . . 4  |-  ( c  =  0  ->  (
( c  e.  RR  /\  ( 0  +  c )  =  0 )  ->  ( 0  +  0 )  =  0 ) )
7 ax-rrecex 9562 . . . . . . 7  |-  ( ( c  e.  RR  /\  c  =/=  0 )  ->  E. y  e.  RR  ( c  x.  y
)  =  1 )
87adantlr 719 . . . . . 6  |-  ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0
)  ->  E. y  e.  RR  ( c  x.  y )  =  1 )
9 simplll 766 . . . . . . . . . . 11  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  c  e.  RR )
109recnd 9620 . . . . . . . . . 10  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  c  e.  CC )
11 simprl 762 . . . . . . . . . . 11  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  y  e.  RR )
1211recnd 9620 . . . . . . . . . 10  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  y  e.  CC )
13 0cn 9586 . . . . . . . . . . 11  |-  0  e.  CC
14 mulass 9578 . . . . . . . . . . 11  |-  ( ( c  e.  CC  /\  y  e.  CC  /\  0  e.  CC )  ->  (
( c  x.  y
)  x.  0 )  =  ( c  x.  ( y  x.  0 ) ) )
1513, 14mp3an3 1349 . . . . . . . . . 10  |-  ( ( c  e.  CC  /\  y  e.  CC )  ->  ( ( c  x.  y )  x.  0 )  =  ( c  x.  ( y  x.  0 ) ) )
1610, 12, 15syl2anc 665 . . . . . . . . 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 6256 . . . . . . . . . . 11  |-  ( ( c  x.  y )  =  1  ->  (
( c  x.  y
)  x.  0 )  =  ( 1  x.  0 ) )
1813mulid2i 9597 . . . . . . . . . . 11  |-  ( 1  x.  0 )  =  0
1917, 18syl6eq 2478 . . . . . . . . . 10  |-  ( ( c  x.  y )  =  1  ->  (
( c  x.  y
)  x.  0 )  =  0 )
2019ad2antll 733 . . . . . . . . 9  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( (
c  x.  y )  x.  0 )  =  0 )
2116, 20eqtr3d 2464 . . . . . . . 8  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( c  x.  ( y  x.  0 ) )  =  0 )
2221oveq1d 6264 . . . . . . 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 767 . . . . . . . . . . . 12  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( 0  +  c )  =  0 )
2423oveq1d 6264 . . . . . . . . . . 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 9575 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  RR  /\  0  e.  RR )  ->  ( y  x.  0 )  e.  RR )
261, 25mpan2 675 . . . . . . . . . . . . . 14  |-  ( y  e.  RR  ->  (
y  x.  0 )  e.  RR )
2726ad2antrl 732 . . . . . . . . . . . . 13  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( y  x.  0 )  e.  RR )
2827recnd 9620 . . . . . . . . . . . 12  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( y  x.  0 )  e.  CC )
29 adddir 9585 . . . . . . . . . . . . 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 1347 . . . . . . . . . . . 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 665 . . . . . . . . . . 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 2464 . . . . . . . . . 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 6264 . . . . . . . . 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 9575 . . . . . . . . . . . . 13  |-  ( ( 0  e.  RR  /\  ( y  x.  0 )  e.  RR )  ->  ( 0  x.  ( y  x.  0 ) )  e.  RR )
351, 26, 34sylancr 667 . . . . . . . . . . . 12  |-  ( y  e.  RR  ->  (
0  x.  ( y  x.  0 ) )  e.  RR )
3635ad2antrl 732 . . . . . . . . . . 11  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( 0  x.  ( y  x.  0 ) )  e.  RR )
3736recnd 9620 . . . . . . . . . 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 9575 . . . . . . . . . . . 12  |-  ( ( c  e.  RR  /\  ( y  x.  0 )  e.  RR )  ->  ( c  x.  ( y  x.  0 ) )  e.  RR )
399, 27, 38syl2anc 665 . . . . . . . . . . 11  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( c  x.  ( y  x.  0 ) )  e.  RR )
4039recnd 9620 . . . . . . . . . 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 9577 . . . . . . . . . . 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 1349 . . . . . . . . . 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 665 . . . . . . . . 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 2463 . . . . . . . 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 476 . . . . . . . . . . 11  |-  ( ( c  e.  RR  /\  y  e.  RR )  ->  ( c  x.  (
y  x.  0 ) )  e.  RR )
46 readdcl 9573 . . . . . . . . . . 11  |-  ( ( ( c  x.  (
y  x.  0 ) )  e.  RR  /\  0  e.  RR )  ->  ( ( c  x.  ( y  x.  0 ) )  +  0 )  e.  RR )
4745, 1, 46sylancl 666 . . . . . . . . . 10  |-  ( ( c  e.  RR  /\  y  e.  RR )  ->  ( ( c  x.  ( y  x.  0 ) )  +  0 )  e.  RR )
489, 11, 47syl2anc 665 . . . . . . . . 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 9758 . . . . . . . . . 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 1348 . . . . . . . . 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 665 . . . . . . . 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 213 . . . . . . 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 2464 . . . . . 6  |-  ( ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0 )  /\  (
y  e.  RR  /\  ( c  x.  y
)  =  1 ) )  ->  ( 0  +  0 )  =  0 )
548, 53rexlimddv 2860 . . . . 5  |-  ( ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  /\  c  =/=  0
)  ->  ( 0  +  0 )  =  0 )
5554expcom 436 . . . 4  |-  ( c  =/=  0  ->  (
( c  e.  RR  /\  ( 0  +  c )  =  0 )  ->  ( 0  +  0 )  =  0 ) )
566, 55pm2.61ine 2684 . . 3  |-  ( ( c  e.  RR  /\  ( 0  +  c )  =  0 )  ->  ( 0  +  0 )  =  0 )
5756rexlimiva 2852 . 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 187    /\ wa 370    = wceq 1437    e. wcel 1872    =/= wne 2599   E.wrex 2715  (class class class)co 6249   CCcc 9488   RRcr 9489   0cc0 9490   1c1 9491    + caddc 9493    x. cmul 9495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-nel 2602  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-opab 4426  df-mpt 4427  df-id 4711  df-po 4717  df-so 4718  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-ov 6252  df-er 7318  df-en 7525  df-dom 7526  df-sdom 7527  df-pnf 9628  df-mnf 9629  df-ltxr 9631
This theorem is referenced by:  mul02lem1  9760  mul02lem2  9761  addid1  9764  addid2  9767  negdiiOLD  9910  addgt0  10051  addgegt0  10052  addgtge0  10053  addge0  10054  add20  10077  recextlem2  10194  crne0  10553  10p10e20  11072  ser0  12215  faclbnd4lem3  12430  bcpasc  12456  relexpaddg  13060  fsumadd  13748  fsumrelem  13810  arisum  13861  fsumcube  14056  sadcaddlem  14374  sadcadd  14375  sadadd2  14377  bezout  14453  nnnn0modprm0  14700  pcaddlem  14776  4sqlem19  14856  37prm  15035  139prm  15038  163prm  15039  317prm  15040  631prm  15041  1259lem1  15045  1259lem2  15046  1259lem3  15047  1259lem4  15048  2503lem1  15051  2503lem2  15052  2503lem3  15053  4001lem1  15055  4001lem2  15056  4001lem3  15057  4001lem4  15058  sylow1lem1  17193  psrbagaddcl  18537  mplcoe3  18633  cnfld0  18935  reparphti  21970  itg1addlem4  22599  ibladdlem  22719  itgaddlem1  22722  iblabslem  22727  iblabs  22728  coeaddlem  23145  dcubic  23714  log2ublem3  23816  log2ub  23817  chtublem  24081  logfacrlim  24094  dchrisumlem1  24269  chpdifbndlem2  24334  vdgr0  25570  vdgr1a  25576  1kp2ke3k  25838  dip0r  26298  pythi  26433  normpythi  26737  ocsh  26878  0lnfn  27580  lnopeq0i  27602  nlelshi  27655  unierri  27699  probun  29204  poimirlem3  31850  poimirlem4  31851  ismblfin  31888  itg2addnc  31903  ibladdnclem  31905  itgaddnclem1  31907  itgaddnclem2  31908  iblabsnclem  31912  iblabsnc  31913  iblmulc2nc  31914  ftc1anclem8  31931  ftc1anc  31932  bezoutr1  35749  relexpaddss  36223  stoweidlem44  37788  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem103  37956  fourierdlem104  37957  sqwvfoura  37975  sqwvfourb  37976
  Copyright terms: Public domain W3C validator