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

Theorem 00id 11331
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 ๐‘ฆ ๐‘ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0re 11158 . 2 0 โˆˆ โ„
2 ax-rnegex 11123 . 2 (0 โˆˆ โ„ โ†’ โˆƒ๐‘ โˆˆ โ„ (0 + ๐‘) = 0)
3 oveq2 7366 . . . . . . 7 (๐‘ = 0 โ†’ (0 + ๐‘) = (0 + 0))
43eqeq1d 2739 . . . . . 6 (๐‘ = 0 โ†’ ((0 + ๐‘) = 0 โ†” (0 + 0) = 0))
54biimpd 228 . . . . 5 (๐‘ = 0 โ†’ ((0 + ๐‘) = 0 โ†’ (0 + 0) = 0))
65adantld 492 . . . 4 (๐‘ = 0 โ†’ ((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โ†’ (0 + 0) = 0))
7 ax-rrecex 11124 . . . . . . 7 ((๐‘ โˆˆ โ„ โˆง ๐‘ โ‰  0) โ†’ โˆƒ๐‘ฆ โˆˆ โ„ (๐‘ ยท ๐‘ฆ) = 1)
87adantlr 714 . . . . . 6 (((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โ†’ โˆƒ๐‘ฆ โˆˆ โ„ (๐‘ ยท ๐‘ฆ) = 1)
9 simplll 774 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ๐‘ โˆˆ โ„)
109recnd 11184 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ๐‘ โˆˆ โ„‚)
11 simprl 770 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ๐‘ฆ โˆˆ โ„)
1211recnd 11184 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ๐‘ฆ โˆˆ โ„‚)
13 0cn 11148 . . . . . . . . . . 11 0 โˆˆ โ„‚
14 mulass 11140 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ โˆง 0 โˆˆ โ„‚) โ†’ ((๐‘ ยท ๐‘ฆ) ยท 0) = (๐‘ ยท (๐‘ฆ ยท 0)))
1513, 14mp3an3 1451 . . . . . . . . . 10 ((๐‘ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ ((๐‘ ยท ๐‘ฆ) ยท 0) = (๐‘ ยท (๐‘ฆ ยท 0)))
1610, 12, 15syl2anc 585 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ((๐‘ ยท ๐‘ฆ) ยท 0) = (๐‘ ยท (๐‘ฆ ยท 0)))
17 oveq1 7365 . . . . . . . . . . 11 ((๐‘ ยท ๐‘ฆ) = 1 โ†’ ((๐‘ ยท ๐‘ฆ) ยท 0) = (1 ยท 0))
1813mulid2i 11161 . . . . . . . . . . 11 (1 ยท 0) = 0
1917, 18eqtrdi 2793 . . . . . . . . . 10 ((๐‘ ยท ๐‘ฆ) = 1 โ†’ ((๐‘ ยท ๐‘ฆ) ยท 0) = 0)
2019ad2antll 728 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ((๐‘ ยท ๐‘ฆ) ยท 0) = 0)
2116, 20eqtr3d 2779 . . . . . . . 8 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (๐‘ ยท (๐‘ฆ ยท 0)) = 0)
2221oveq1d 7373 . . . . . . 7 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ((๐‘ ยท (๐‘ฆ ยท 0)) + 0) = (0 + 0))
23 simpllr 775 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (0 + ๐‘) = 0)
2423oveq1d 7373 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ((0 + ๐‘) ยท (๐‘ฆ ยท 0)) = (0 ยท (๐‘ฆ ยท 0)))
25 remulcl 11137 . . . . . . . . . . . . . . 15 ((๐‘ฆ โˆˆ โ„ โˆง 0 โˆˆ โ„) โ†’ (๐‘ฆ ยท 0) โˆˆ โ„)
261, 25mpan2 690 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„ โ†’ (๐‘ฆ ยท 0) โˆˆ โ„)
2726ad2antrl 727 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (๐‘ฆ ยท 0) โˆˆ โ„)
2827recnd 11184 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (๐‘ฆ ยท 0) โˆˆ โ„‚)
29 adddir 11147 . . . . . . . . . . . 12 ((0 โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚ โˆง (๐‘ฆ ยท 0) โˆˆ โ„‚) โ†’ ((0 + ๐‘) ยท (๐‘ฆ ยท 0)) = ((0 ยท (๐‘ฆ ยท 0)) + (๐‘ ยท (๐‘ฆ ยท 0))))
3013, 10, 28, 29mp3an2i 1467 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ((0 + ๐‘) ยท (๐‘ฆ ยท 0)) = ((0 ยท (๐‘ฆ ยท 0)) + (๐‘ ยท (๐‘ฆ ยท 0))))
3124, 30eqtr3d 2779 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (0 ยท (๐‘ฆ ยท 0)) = ((0 ยท (๐‘ฆ ยท 0)) + (๐‘ ยท (๐‘ฆ ยท 0))))
3231oveq1d 7373 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ((0 ยท (๐‘ฆ ยท 0)) + 0) = (((0 ยท (๐‘ฆ ยท 0)) + (๐‘ ยท (๐‘ฆ ยท 0))) + 0))
33 remulcl 11137 . . . . . . . . . . . . 13 ((0 โˆˆ โ„ โˆง (๐‘ฆ ยท 0) โˆˆ โ„) โ†’ (0 ยท (๐‘ฆ ยท 0)) โˆˆ โ„)
341, 26, 33sylancr 588 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„ โ†’ (0 ยท (๐‘ฆ ยท 0)) โˆˆ โ„)
3534ad2antrl 727 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (0 ยท (๐‘ฆ ยท 0)) โˆˆ โ„)
3635recnd 11184 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (0 ยท (๐‘ฆ ยท 0)) โˆˆ โ„‚)
37 remulcl 11137 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„ โˆง (๐‘ฆ ยท 0) โˆˆ โ„) โ†’ (๐‘ ยท (๐‘ฆ ยท 0)) โˆˆ โ„)
389, 27, 37syl2anc 585 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (๐‘ ยท (๐‘ฆ ยท 0)) โˆˆ โ„)
3938recnd 11184 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (๐‘ ยท (๐‘ฆ ยท 0)) โˆˆ โ„‚)
40 addass 11139 . . . . . . . . . . 11 (((0 ยท (๐‘ฆ ยท 0)) โˆˆ โ„‚ โˆง (๐‘ ยท (๐‘ฆ ยท 0)) โˆˆ โ„‚ โˆง 0 โˆˆ โ„‚) โ†’ (((0 ยท (๐‘ฆ ยท 0)) + (๐‘ ยท (๐‘ฆ ยท 0))) + 0) = ((0 ยท (๐‘ฆ ยท 0)) + ((๐‘ ยท (๐‘ฆ ยท 0)) + 0)))
4113, 40mp3an3 1451 . . . . . . . . . 10 (((0 ยท (๐‘ฆ ยท 0)) โˆˆ โ„‚ โˆง (๐‘ ยท (๐‘ฆ ยท 0)) โˆˆ โ„‚) โ†’ (((0 ยท (๐‘ฆ ยท 0)) + (๐‘ ยท (๐‘ฆ ยท 0))) + 0) = ((0 ยท (๐‘ฆ ยท 0)) + ((๐‘ ยท (๐‘ฆ ยท 0)) + 0)))
4236, 39, 41syl2anc 585 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (((0 ยท (๐‘ฆ ยท 0)) + (๐‘ ยท (๐‘ฆ ยท 0))) + 0) = ((0 ยท (๐‘ฆ ยท 0)) + ((๐‘ ยท (๐‘ฆ ยท 0)) + 0)))
4332, 42eqtr2d 2778 . . . . . . . 8 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ((0 ยท (๐‘ฆ ยท 0)) + ((๐‘ ยท (๐‘ฆ ยท 0)) + 0)) = ((0 ยท (๐‘ฆ ยท 0)) + 0))
4426, 37sylan2 594 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โ†’ (๐‘ ยท (๐‘ฆ ยท 0)) โˆˆ โ„)
45 readdcl 11135 . . . . . . . . . . 11 (((๐‘ ยท (๐‘ฆ ยท 0)) โˆˆ โ„ โˆง 0 โˆˆ โ„) โ†’ ((๐‘ ยท (๐‘ฆ ยท 0)) + 0) โˆˆ โ„)
4644, 1, 45sylancl 587 . . . . . . . . . 10 ((๐‘ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โ†’ ((๐‘ ยท (๐‘ฆ ยท 0)) + 0) โˆˆ โ„)
479, 11, 46syl2anc 585 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ((๐‘ ยท (๐‘ฆ ยท 0)) + 0) โˆˆ โ„)
48 readdcan 11330 . . . . . . . . . 10 ((((๐‘ ยท (๐‘ฆ ยท 0)) + 0) โˆˆ โ„ โˆง 0 โˆˆ โ„ โˆง (0 ยท (๐‘ฆ ยท 0)) โˆˆ โ„) โ†’ (((0 ยท (๐‘ฆ ยท 0)) + ((๐‘ ยท (๐‘ฆ ยท 0)) + 0)) = ((0 ยท (๐‘ฆ ยท 0)) + 0) โ†” ((๐‘ ยท (๐‘ฆ ยท 0)) + 0) = 0))
491, 48mp3an2 1450 . . . . . . . . 9 ((((๐‘ ยท (๐‘ฆ ยท 0)) + 0) โˆˆ โ„ โˆง (0 ยท (๐‘ฆ ยท 0)) โˆˆ โ„) โ†’ (((0 ยท (๐‘ฆ ยท 0)) + ((๐‘ ยท (๐‘ฆ ยท 0)) + 0)) = ((0 ยท (๐‘ฆ ยท 0)) + 0) โ†” ((๐‘ ยท (๐‘ฆ ยท 0)) + 0) = 0))
5047, 35, 49syl2anc 585 . . . . . . . 8 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (((0 ยท (๐‘ฆ ยท 0)) + ((๐‘ ยท (๐‘ฆ ยท 0)) + 0)) = ((0 ยท (๐‘ฆ ยท 0)) + 0) โ†” ((๐‘ ยท (๐‘ฆ ยท 0)) + 0) = 0))
5143, 50mpbid 231 . . . . . . 7 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ((๐‘ ยท (๐‘ฆ ยท 0)) + 0) = 0)
5222, 51eqtr3d 2779 . . . . . 6 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (0 + 0) = 0)
538, 52rexlimddv 3159 . . . . 5 (((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โ†’ (0 + 0) = 0)
5453expcom 415 . . . 4 (๐‘ โ‰  0 โ†’ ((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โ†’ (0 + 0) = 0))
556, 54pm2.61ine 3029 . . 3 ((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โ†’ (0 + 0) = 0)
5655rexlimiva 3145 . 2 (โˆƒ๐‘ โˆˆ โ„ (0 + ๐‘) = 0 โ†’ (0 + 0) = 0)
571, 2, 56mp2b 10 1 (0 + 0) = 0
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944  โˆƒwrex 3074  (class class class)co 7358  โ„‚cc 11050  โ„cr 11051  0cc0 11052  1c1 11053   + caddc 11055   ยท cmul 11057
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-po 5546  df-so 5547  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11192  df-mnf 11193  df-ltxr 11195
This theorem is referenced by:  mul02lem1  11332  mul02lem2  11333  addid1  11336  addid2  11339  addgt0  11642  addgegt0  11643  addgtge0  11644  addge0  11645  add20  11668  recextlem2  11787  crne0  12147  decaddm10  12678  10p10e20  12714  ser0  13961  faclbnd4lem3  14196  bcpasc  14222  relexpaddg  14939  fsumadd  15626  fsumrelem  15693  arisum  15746  fsumcube  15944  sadcaddlem  16338  sadcadd  16339  sadadd2  16341  bezout  16425  bezoutr1  16446  nnnn0modprm0  16679  pcaddlem  16761  4sqlem19  16836  139prm  16997  163prm  16998  317prm  16999  631prm  17000  1259lem1  17004  1259lem2  17005  1259lem4  17007  2503lem1  17010  2503lem2  17011  2503lem3  17012  4001lem1  17014  4001lem2  17015  4001lem3  17016  4001lem4  17017  sylow1lem1  19381  cnfld0  20824  psrbagaddcl  21333  psrbagaddclOLD  21334  mplcoe3  21442  reparphti  24363  cphpyth  24583  itg1addlem4  25066  itg1addlem4OLD  25067  ibladdlem  25187  itgaddlem1  25190  iblabslem  25195  iblabs  25196  coeaddlem  25613  dcubic  26199  log2ublem3  26301  log2ub  26302  chtublem  26562  logfacrlim  26575  2sqnn  26790  dchrisumlem1  26840  vtxdg0e  28425  1kp2ke3k  29393  dip0r  29662  pythi  29795  normpythi  30087  ocsh  30228  0lnfn  30930  lnopeq0i  30952  nlelshi  31005  unierri  31049  probun  33022  hgt750lem2  33268  poimirlem3  36084  poimirlem4  36085  ismblfin  36122  itg2addnc  36135  ibladdnclem  36137  itgaddnclem1  36139  itgaddnclem2  36140  iblabsnclem  36144  iblabsnc  36145  iblmulc2nc  36146  ftc1anclem8  36161  ftc1anc  36162  3lexlogpow5ineq1  40514  dffltz  40975  relexpaddss  41997  stoweidlem44  44292  fourierdlem42  44397  fourierdlem103  44457  fourierdlem104  44458  sqwvfoura  44476  sqwvfourb  44477  fmtno5lem4  45755  139prmALT  45795  line2ylem  46844
  Copyright terms: Public domain W3C validator