Metamath Proof Explorer


Theorem 00id

Description: 0 is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013)

Ref Expression
Assertion 00id ( 0 + 0 ) = 0

Proof

Step Hyp Ref Expression
1 0re 0 ∈ ℝ
2 ax-rnegex ( 0 ∈ ℝ → ∃ 𝑐 ∈ ℝ ( 0 + 𝑐 ) = 0 )
3 oveq2 ( 𝑐 = 0 → ( 0 + 𝑐 ) = ( 0 + 0 ) )
4 3 eqeq1d ( 𝑐 = 0 → ( ( 0 + 𝑐 ) = 0 ↔ ( 0 + 0 ) = 0 ) )
5 4 biimpd ( 𝑐 = 0 → ( ( 0 + 𝑐 ) = 0 → ( 0 + 0 ) = 0 ) )
6 5 adantld ( 𝑐 = 0 → ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) → ( 0 + 0 ) = 0 ) )
7 ax-rrecex ( ( 𝑐 ∈ ℝ ∧ 𝑐 ≠ 0 ) → ∃ 𝑦 ∈ ℝ ( 𝑐 · 𝑦 ) = 1 )
8 7 adantlr ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) → ∃ 𝑦 ∈ ℝ ( 𝑐 · 𝑦 ) = 1 )
9 simplll ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → 𝑐 ∈ ℝ )
10 9 recnd ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → 𝑐 ∈ ℂ )
11 simprl ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → 𝑦 ∈ ℝ )
12 11 recnd ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → 𝑦 ∈ ℂ )
13 0cn 0 ∈ ℂ
14 mulass ( ( 𝑐 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 0 ∈ ℂ ) → ( ( 𝑐 · 𝑦 ) · 0 ) = ( 𝑐 · ( 𝑦 · 0 ) ) )
15 13 14 mp3an3 ( ( 𝑐 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑐 · 𝑦 ) · 0 ) = ( 𝑐 · ( 𝑦 · 0 ) ) )
16 10 12 15 syl2anc ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( ( 𝑐 · 𝑦 ) · 0 ) = ( 𝑐 · ( 𝑦 · 0 ) ) )
17 oveq1 ( ( 𝑐 · 𝑦 ) = 1 → ( ( 𝑐 · 𝑦 ) · 0 ) = ( 1 · 0 ) )
18 13 mulid2i ( 1 · 0 ) = 0
19 17 18 eqtrdi ( ( 𝑐 · 𝑦 ) = 1 → ( ( 𝑐 · 𝑦 ) · 0 ) = 0 )
20 19 ad2antll ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( ( 𝑐 · 𝑦 ) · 0 ) = 0 )
21 16 20 eqtr3d ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( 𝑐 · ( 𝑦 · 0 ) ) = 0 )
22 21 oveq1d ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( ( 𝑐 · ( 𝑦 · 0 ) ) + 0 ) = ( 0 + 0 ) )
23 simpllr ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( 0 + 𝑐 ) = 0 )
24 23 oveq1d ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( ( 0 + 𝑐 ) · ( 𝑦 · 0 ) ) = ( 0 · ( 𝑦 · 0 ) ) )
25 remulcl ( ( 𝑦 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝑦 · 0 ) ∈ ℝ )
26 1 25 mpan2 ( 𝑦 ∈ ℝ → ( 𝑦 · 0 ) ∈ ℝ )
27 26 ad2antrl ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( 𝑦 · 0 ) ∈ ℝ )
28 27 recnd ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( 𝑦 · 0 ) ∈ ℂ )
29 adddir ( ( 0 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ ( 𝑦 · 0 ) ∈ ℂ ) → ( ( 0 + 𝑐 ) · ( 𝑦 · 0 ) ) = ( ( 0 · ( 𝑦 · 0 ) ) + ( 𝑐 · ( 𝑦 · 0 ) ) ) )
30 13 10 28 29 mp3an2i ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( ( 0 + 𝑐 ) · ( 𝑦 · 0 ) ) = ( ( 0 · ( 𝑦 · 0 ) ) + ( 𝑐 · ( 𝑦 · 0 ) ) ) )
31 24 30 eqtr3d ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( 0 · ( 𝑦 · 0 ) ) = ( ( 0 · ( 𝑦 · 0 ) ) + ( 𝑐 · ( 𝑦 · 0 ) ) ) )
32 31 oveq1d ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( ( 0 · ( 𝑦 · 0 ) ) + 0 ) = ( ( ( 0 · ( 𝑦 · 0 ) ) + ( 𝑐 · ( 𝑦 · 0 ) ) ) + 0 ) )
33 remulcl ( ( 0 ∈ ℝ ∧ ( 𝑦 · 0 ) ∈ ℝ ) → ( 0 · ( 𝑦 · 0 ) ) ∈ ℝ )
34 1 26 33 sylancr ( 𝑦 ∈ ℝ → ( 0 · ( 𝑦 · 0 ) ) ∈ ℝ )
35 34 ad2antrl ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( 0 · ( 𝑦 · 0 ) ) ∈ ℝ )
36 35 recnd ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( 0 · ( 𝑦 · 0 ) ) ∈ ℂ )
37 remulcl ( ( 𝑐 ∈ ℝ ∧ ( 𝑦 · 0 ) ∈ ℝ ) → ( 𝑐 · ( 𝑦 · 0 ) ) ∈ ℝ )
38 9 27 37 syl2anc ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( 𝑐 · ( 𝑦 · 0 ) ) ∈ ℝ )
39 38 recnd ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( 𝑐 · ( 𝑦 · 0 ) ) ∈ ℂ )
40 addass ( ( ( 0 · ( 𝑦 · 0 ) ) ∈ ℂ ∧ ( 𝑐 · ( 𝑦 · 0 ) ) ∈ ℂ ∧ 0 ∈ ℂ ) → ( ( ( 0 · ( 𝑦 · 0 ) ) + ( 𝑐 · ( 𝑦 · 0 ) ) ) + 0 ) = ( ( 0 · ( 𝑦 · 0 ) ) + ( ( 𝑐 · ( 𝑦 · 0 ) ) + 0 ) ) )
41 13 40 mp3an3 ( ( ( 0 · ( 𝑦 · 0 ) ) ∈ ℂ ∧ ( 𝑐 · ( 𝑦 · 0 ) ) ∈ ℂ ) → ( ( ( 0 · ( 𝑦 · 0 ) ) + ( 𝑐 · ( 𝑦 · 0 ) ) ) + 0 ) = ( ( 0 · ( 𝑦 · 0 ) ) + ( ( 𝑐 · ( 𝑦 · 0 ) ) + 0 ) ) )
42 36 39 41 syl2anc ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( ( ( 0 · ( 𝑦 · 0 ) ) + ( 𝑐 · ( 𝑦 · 0 ) ) ) + 0 ) = ( ( 0 · ( 𝑦 · 0 ) ) + ( ( 𝑐 · ( 𝑦 · 0 ) ) + 0 ) ) )
43 32 42 eqtr2d ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( ( 0 · ( 𝑦 · 0 ) ) + ( ( 𝑐 · ( 𝑦 · 0 ) ) + 0 ) ) = ( ( 0 · ( 𝑦 · 0 ) ) + 0 ) )
44 26 37 sylan2 ( ( 𝑐 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑐 · ( 𝑦 · 0 ) ) ∈ ℝ )
45 readdcl ( ( ( 𝑐 · ( 𝑦 · 0 ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 𝑐 · ( 𝑦 · 0 ) ) + 0 ) ∈ ℝ )
46 44 1 45 sylancl ( ( 𝑐 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑐 · ( 𝑦 · 0 ) ) + 0 ) ∈ ℝ )
47 9 11 46 syl2anc ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( ( 𝑐 · ( 𝑦 · 0 ) ) + 0 ) ∈ ℝ )
48 readdcan ( ( ( ( 𝑐 · ( 𝑦 · 0 ) ) + 0 ) ∈ ℝ ∧ 0 ∈ ℝ ∧ ( 0 · ( 𝑦 · 0 ) ) ∈ ℝ ) → ( ( ( 0 · ( 𝑦 · 0 ) ) + ( ( 𝑐 · ( 𝑦 · 0 ) ) + 0 ) ) = ( ( 0 · ( 𝑦 · 0 ) ) + 0 ) ↔ ( ( 𝑐 · ( 𝑦 · 0 ) ) + 0 ) = 0 ) )
49 1 48 mp3an2 ( ( ( ( 𝑐 · ( 𝑦 · 0 ) ) + 0 ) ∈ ℝ ∧ ( 0 · ( 𝑦 · 0 ) ) ∈ ℝ ) → ( ( ( 0 · ( 𝑦 · 0 ) ) + ( ( 𝑐 · ( 𝑦 · 0 ) ) + 0 ) ) = ( ( 0 · ( 𝑦 · 0 ) ) + 0 ) ↔ ( ( 𝑐 · ( 𝑦 · 0 ) ) + 0 ) = 0 ) )
50 47 35 49 syl2anc ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( ( ( 0 · ( 𝑦 · 0 ) ) + ( ( 𝑐 · ( 𝑦 · 0 ) ) + 0 ) ) = ( ( 0 · ( 𝑦 · 0 ) ) + 0 ) ↔ ( ( 𝑐 · ( 𝑦 · 0 ) ) + 0 ) = 0 ) )
51 43 50 mpbid ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( ( 𝑐 · ( 𝑦 · 0 ) ) + 0 ) = 0 )
52 22 51 eqtr3d ( ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑐 · 𝑦 ) = 1 ) ) → ( 0 + 0 ) = 0 )
53 8 52 rexlimddv ( ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) ∧ 𝑐 ≠ 0 ) → ( 0 + 0 ) = 0 )
54 53 expcom ( 𝑐 ≠ 0 → ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) → ( 0 + 0 ) = 0 ) )
55 6 54 pm2.61ine ( ( 𝑐 ∈ ℝ ∧ ( 0 + 𝑐 ) = 0 ) → ( 0 + 0 ) = 0 )
56 55 rexlimiva ( ∃ 𝑐 ∈ ℝ ( 0 + 𝑐 ) = 0 → ( 0 + 0 ) = 0 )
57 1 2 56 mp2b ( 0 + 0 ) = 0