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 syl6eq ⊢ ( ( 𝑐 · 𝑦 ) = 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