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

Theorem 00id 11389
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 11216 . 2 0 โˆˆ โ„
2 ax-rnegex 11181 . 2 (0 โˆˆ โ„ โ†’ โˆƒ๐‘ โˆˆ โ„ (0 + ๐‘) = 0)
3 oveq2 7417 . . . . . . 7 (๐‘ = 0 โ†’ (0 + ๐‘) = (0 + 0))
43eqeq1d 2735 . . . . . 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 11182 . . . . . . 7 ((๐‘ โˆˆ โ„ โˆง ๐‘ โ‰  0) โ†’ โˆƒ๐‘ฆ โˆˆ โ„ (๐‘ ยท ๐‘ฆ) = 1)
87adantlr 714 . . . . . 6 (((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โ†’ โˆƒ๐‘ฆ โˆˆ โ„ (๐‘ ยท ๐‘ฆ) = 1)
9 simplll 774 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ๐‘ โˆˆ โ„)
109recnd 11242 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ๐‘ โˆˆ โ„‚)
11 simprl 770 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ๐‘ฆ โˆˆ โ„)
1211recnd 11242 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ๐‘ฆ โˆˆ โ„‚)
13 0cn 11206 . . . . . . . . . . 11 0 โˆˆ โ„‚
14 mulass 11198 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ โˆง 0 โˆˆ โ„‚) โ†’ ((๐‘ ยท ๐‘ฆ) ยท 0) = (๐‘ ยท (๐‘ฆ ยท 0)))
1513, 14mp3an3 1451 . . . . . . . . . 10 ((๐‘ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ ((๐‘ ยท ๐‘ฆ) ยท 0) = (๐‘ ยท (๐‘ฆ ยท 0)))
1610, 12, 15syl2anc 585 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ((๐‘ ยท ๐‘ฆ) ยท 0) = (๐‘ ยท (๐‘ฆ ยท 0)))
17 oveq1 7416 . . . . . . . . . . 11 ((๐‘ ยท ๐‘ฆ) = 1 โ†’ ((๐‘ ยท ๐‘ฆ) ยท 0) = (1 ยท 0))
1813mullidi 11219 . . . . . . . . . . 11 (1 ยท 0) = 0
1917, 18eqtrdi 2789 . . . . . . . . . 10 ((๐‘ ยท ๐‘ฆ) = 1 โ†’ ((๐‘ ยท ๐‘ฆ) ยท 0) = 0)
2019ad2antll 728 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ((๐‘ ยท ๐‘ฆ) ยท 0) = 0)
2116, 20eqtr3d 2775 . . . . . . . 8 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (๐‘ ยท (๐‘ฆ ยท 0)) = 0)
2221oveq1d 7424 . . . . . . 7 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ((๐‘ ยท (๐‘ฆ ยท 0)) + 0) = (0 + 0))
23 simpllr 775 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (0 + ๐‘) = 0)
2423oveq1d 7424 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ((0 + ๐‘) ยท (๐‘ฆ ยท 0)) = (0 ยท (๐‘ฆ ยท 0)))
25 remulcl 11195 . . . . . . . . . . . . . . 15 ((๐‘ฆ โˆˆ โ„ โˆง 0 โˆˆ โ„) โ†’ (๐‘ฆ ยท 0) โˆˆ โ„)
261, 25mpan2 690 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„ โ†’ (๐‘ฆ ยท 0) โˆˆ โ„)
2726ad2antrl 727 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (๐‘ฆ ยท 0) โˆˆ โ„)
2827recnd 11242 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (๐‘ฆ ยท 0) โˆˆ โ„‚)
29 adddir 11205 . . . . . . . . . . . 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 2775 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (0 ยท (๐‘ฆ ยท 0)) = ((0 ยท (๐‘ฆ ยท 0)) + (๐‘ ยท (๐‘ฆ ยท 0))))
3231oveq1d 7424 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ((0 ยท (๐‘ฆ ยท 0)) + 0) = (((0 ยท (๐‘ฆ ยท 0)) + (๐‘ ยท (๐‘ฆ ยท 0))) + 0))
33 remulcl 11195 . . . . . . . . . . . . 13 ((0 โˆˆ โ„ โˆง (๐‘ฆ ยท 0) โˆˆ โ„) โ†’ (0 ยท (๐‘ฆ ยท 0)) โˆˆ โ„)
341, 26, 33sylancr 588 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„ โ†’ (0 ยท (๐‘ฆ ยท 0)) โˆˆ โ„)
3534ad2antrl 727 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (0 ยท (๐‘ฆ ยท 0)) โˆˆ โ„)
3635recnd 11242 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (0 ยท (๐‘ฆ ยท 0)) โˆˆ โ„‚)
37 remulcl 11195 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„ โˆง (๐‘ฆ ยท 0) โˆˆ โ„) โ†’ (๐‘ ยท (๐‘ฆ ยท 0)) โˆˆ โ„)
389, 27, 37syl2anc 585 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (๐‘ ยท (๐‘ฆ ยท 0)) โˆˆ โ„)
3938recnd 11242 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (๐‘ ยท (๐‘ฆ ยท 0)) โˆˆ โ„‚)
40 addass 11197 . . . . . . . . . . 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 2774 . . . . . . . 8 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ ((0 ยท (๐‘ฆ ยท 0)) + ((๐‘ ยท (๐‘ฆ ยท 0)) + 0)) = ((0 ยท (๐‘ฆ ยท 0)) + 0))
4426, 37sylan2 594 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โ†’ (๐‘ ยท (๐‘ฆ ยท 0)) โˆˆ โ„)
45 readdcl 11193 . . . . . . . . . . 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 11388 . . . . . . . . . 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 2775 . . . . . 6 ((((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฆ) = 1)) โ†’ (0 + 0) = 0)
538, 52rexlimddv 3162 . . . . 5 (((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โˆง ๐‘ โ‰  0) โ†’ (0 + 0) = 0)
5453expcom 415 . . . 4 (๐‘ โ‰  0 โ†’ ((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โ†’ (0 + 0) = 0))
556, 54pm2.61ine 3026 . . 3 ((๐‘ โˆˆ โ„ โˆง (0 + ๐‘) = 0) โ†’ (0 + 0) = 0)
5655rexlimiva 3148 . 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 2941  โˆƒwrex 3071  (class class class)co 7409  โ„‚cc 11108  โ„cr 11109  0cc0 11110  1c1 11111   + caddc 11113   ยท cmul 11115
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 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186
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 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-ltxr 11253
This theorem is referenced by:  mul02lem1  11390  mul02lem2  11391  addrid  11394  addlid  11397  addgt0  11700  addgegt0  11701  addgtge0  11702  addge0  11703  add20  11726  recextlem2  11845  crne0  12205  decaddm10  12736  10p10e20  12772  ser0  14020  faclbnd4lem3  14255  bcpasc  14281  relexpaddg  15000  fsumadd  15686  fsumrelem  15753  arisum  15806  fsumcube  16004  sadcaddlem  16398  sadcadd  16399  sadadd2  16401  bezout  16485  bezoutr1  16506  nnnn0modprm0  16739  pcaddlem  16821  4sqlem19  16896  139prm  17057  163prm  17058  317prm  17059  631prm  17060  1259lem1  17064  1259lem2  17065  1259lem4  17067  2503lem1  17070  2503lem2  17071  2503lem3  17072  4001lem1  17074  4001lem2  17075  4001lem3  17076  4001lem4  17077  sylow1lem1  19466  cnfld0  20969  psrbagaddcl  21481  psrbagaddclOLD  21482  mplcoe3  21593  reparphti  24513  cphpyth  24733  itg1addlem4  25216  itg1addlem4OLD  25217  ibladdlem  25337  itgaddlem1  25340  iblabslem  25345  iblabs  25346  coeaddlem  25763  dcubic  26351  log2ublem3  26453  log2ub  26454  chtublem  26714  logfacrlim  26727  2sqnn  26942  dchrisumlem1  26992  vtxdg0e  28731  1kp2ke3k  29699  dip0r  29970  pythi  30103  normpythi  30395  ocsh  30536  0lnfn  31238  lnopeq0i  31260  nlelshi  31313  unierri  31357  probun  33418  hgt750lem2  33664  gg-reparphti  35172  poimirlem3  36491  poimirlem4  36492  ismblfin  36529  itg2addnc  36542  ibladdnclem  36544  itgaddnclem1  36546  itgaddnclem2  36547  iblabsnclem  36551  iblabsnc  36552  iblmulc2nc  36553  ftc1anclem8  36568  ftc1anc  36569  3lexlogpow5ineq1  40919  dffltz  41376  relexpaddss  42469  stoweidlem44  44760  fourierdlem42  44865  fourierdlem103  44925  fourierdlem104  44926  sqwvfoura  44944  sqwvfourb  44945  fmtno5lem4  46224  139prmALT  46264  pzriprnglem4  46808  line2ylem  47437
  Copyright terms: Public domain W3C validator