This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dpadd3

Description: Addition with two decimals. (Contributed by Thierry Arnoux, 27-Dec-2021)

Ref Expression
Hypotheses dpmul.a ⊢ 𝐴 ∈ ℕ0
dpmul.b ⊢ 𝐵 ∈ ℕ0
dpmul.c ⊢ 𝐶 ∈ ℕ0
dpmul.d ⊢ 𝐷 ∈ ℕ0
dpmul.e ⊢ 𝐸 ∈ ℕ0
dpmul.g ⊢ 𝐺 ∈ ℕ0
dpadd3.f ⊢ 𝐹 ∈ ℕ0
dpadd3.h ⊢ 𝐻 ∈ ℕ0
dpadd3.i ⊢ 𝐼 ∈ ℕ0
dpadd3.1 ⊢ ( 𝐴 𝐵 𝐶 + 𝐷 𝐸 𝐹 ) = 𝐺 𝐻 𝐼
Assertion dpadd3 ( ( 𝐴 . 𝐵 𝐶 ) + ( 𝐷 . 𝐸 𝐹 ) ) = ( 𝐺 . 𝐻 𝐼 )

Proof

Step Hyp Ref Expression
1 dpmul.a ⊢ 𝐴 ∈ ℕ0
2 dpmul.b ⊢ 𝐵 ∈ ℕ0
3 dpmul.c ⊢ 𝐶 ∈ ℕ0
4 dpmul.d ⊢ 𝐷 ∈ ℕ0
5 dpmul.e ⊢ 𝐸 ∈ ℕ0
6 dpmul.g ⊢ 𝐺 ∈ ℕ0
7 dpadd3.f ⊢ 𝐹 ∈ ℕ0
8 dpadd3.h ⊢ 𝐻 ∈ ℕ0
9 dpadd3.i ⊢ 𝐼 ∈ ℕ0
10 dpadd3.1 ⊢ ( 𝐴 𝐵 𝐶 + 𝐷 𝐸 𝐹 ) = 𝐺 𝐻 𝐼
11 2 nn0rei ⊢ 𝐵 ∈ ℝ
12 3 nn0rei ⊢ 𝐶 ∈ ℝ
13 dp2cl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 𝐶 ∈ ℝ )
14 11 12 13 mp2an ⊢ 𝐵 𝐶 ∈ ℝ
15 dpcl ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 𝐶 ∈ ℝ ) → ( 𝐴 . 𝐵 𝐶 ) ∈ ℝ )
16 1 14 15 mp2an ⊢ ( 𝐴 . 𝐵 𝐶 ) ∈ ℝ
17 16 recni ⊢ ( 𝐴 . 𝐵 𝐶 ) ∈ ℂ
18 5 nn0rei ⊢ 𝐸 ∈ ℝ
19 7 nn0rei ⊢ 𝐹 ∈ ℝ
20 dp2cl ⊢ ( ( 𝐸 ∈ ℝ ∧ 𝐹 ∈ ℝ ) → 𝐸 𝐹 ∈ ℝ )
21 18 19 20 mp2an ⊢ 𝐸 𝐹 ∈ ℝ
22 dpcl ⊢ ( ( 𝐷 ∈ ℕ0 ∧ 𝐸 𝐹 ∈ ℝ ) → ( 𝐷 . 𝐸 𝐹 ) ∈ ℝ )
23 4 21 22 mp2an ⊢ ( 𝐷 . 𝐸 𝐹 ) ∈ ℝ
24 23 recni ⊢ ( 𝐷 . 𝐸 𝐹 ) ∈ ℂ
25 17 24 addcli ⊢ ( ( 𝐴 . 𝐵 𝐶 ) + ( 𝐷 . 𝐸 𝐹 ) ) ∈ ℂ
26 8 nn0rei ⊢ 𝐻 ∈ ℝ
27 9 nn0rei ⊢ 𝐼 ∈ ℝ
28 dp2cl ⊢ ( ( 𝐻 ∈ ℝ ∧ 𝐼 ∈ ℝ ) → 𝐻 𝐼 ∈ ℝ )
29 26 27 28 mp2an ⊢ 𝐻 𝐼 ∈ ℝ
30 dpcl ⊢ ( ( 𝐺 ∈ ℕ0 ∧ 𝐻 𝐼 ∈ ℝ ) → ( 𝐺 . 𝐻 𝐼 ) ∈ ℝ )
31 6 29 30 mp2an ⊢ ( 𝐺 . 𝐻 𝐼 ) ∈ ℝ
32 31 recni ⊢ ( 𝐺 . 𝐻 𝐼 ) ∈ ℂ
33 10nn ⊢ 1 0 ∈ ℕ
34 33 decnncl2 ⊢ 1 0 0 ∈ ℕ
35 34 nncni ⊢ 1 0 0 ∈ ℂ
36 34 nnne0i ⊢ 1 0 0 ≠ 0
37 35 36 pm3.2i ⊢ ( 1 0 0 ∈ ℂ ∧ 1 0 0 ≠ 0 )
38 25 32 37 3pm3.2i ⊢ ( ( ( 𝐴 . 𝐵 𝐶 ) + ( 𝐷 . 𝐸 𝐹 ) ) ∈ ℂ ∧ ( 𝐺 . 𝐻 𝐼 ) ∈ ℂ ∧ ( 1 0 0 ∈ ℂ ∧ 1 0 0 ≠ 0 ) )
39 17 24 35 adddiri ⊢ ( ( ( 𝐴 . 𝐵 𝐶 ) + ( 𝐷 . 𝐸 𝐹 ) ) · 1 0 0 ) = ( ( ( 𝐴 . 𝐵 𝐶 ) · 1 0 0 ) + ( ( 𝐷 . 𝐸 𝐹 ) · 1 0 0 ) )
40 1 2 12 dpmul100 ⊢ ( ( 𝐴 . 𝐵 𝐶 ) · 1 0 0 ) = 𝐴 𝐵 𝐶
41 4 5 19 dpmul100 ⊢ ( ( 𝐷 . 𝐸 𝐹 ) · 1 0 0 ) = 𝐷 𝐸 𝐹
42 40 41 oveq12i ⊢ ( ( ( 𝐴 . 𝐵 𝐶 ) · 1 0 0 ) + ( ( 𝐷 . 𝐸 𝐹 ) · 1 0 0 ) ) = ( 𝐴 𝐵 𝐶 + 𝐷 𝐸 𝐹 )
43 6 8 27 dpmul100 ⊢ ( ( 𝐺 . 𝐻 𝐼 ) · 1 0 0 ) = 𝐺 𝐻 𝐼
44 10 42 43 3eqtr4i ⊢ ( ( ( 𝐴 . 𝐵 𝐶 ) · 1 0 0 ) + ( ( 𝐷 . 𝐸 𝐹 ) · 1 0 0 ) ) = ( ( 𝐺 . 𝐻 𝐼 ) · 1 0 0 )
45 39 44 eqtri ⊢ ( ( ( 𝐴 . 𝐵 𝐶 ) + ( 𝐷 . 𝐸 𝐹 ) ) · 1 0 0 ) = ( ( 𝐺 . 𝐻 𝐼 ) · 1 0 0 )
46 mulcan2 ⊢ ( ( ( ( 𝐴 . 𝐵 𝐶 ) + ( 𝐷 . 𝐸 𝐹 ) ) ∈ ℂ ∧ ( 𝐺 . 𝐻 𝐼 ) ∈ ℂ ∧ ( 1 0 0 ∈ ℂ ∧ 1 0 0 ≠ 0 ) ) → ( ( ( ( 𝐴 . 𝐵 𝐶 ) + ( 𝐷 . 𝐸 𝐹 ) ) · 1 0 0 ) = ( ( 𝐺 . 𝐻 𝐼 ) · 1 0 0 ) ↔ ( ( 𝐴 . 𝐵 𝐶 ) + ( 𝐷 . 𝐸 𝐹 ) ) = ( 𝐺 . 𝐻 𝐼 ) ) )
47 46 biimpa ⊢ ( ( ( ( ( 𝐴 . 𝐵 𝐶 ) + ( 𝐷 . 𝐸 𝐹 ) ) ∈ ℂ ∧ ( 𝐺 . 𝐻 𝐼 ) ∈ ℂ ∧ ( 1 0 0 ∈ ℂ ∧ 1 0 0 ≠ 0 ) ) ∧ ( ( ( 𝐴 . 𝐵 𝐶 ) + ( 𝐷 . 𝐸 𝐹 ) ) · 1 0 0 ) = ( ( 𝐺 . 𝐻 𝐼 ) · 1 0 0 ) ) → ( ( 𝐴 . 𝐵 𝐶 ) + ( 𝐷 . 𝐸 𝐹 ) ) = ( 𝐺 . 𝐻 𝐼 ) )
48 38 45 47 mp2an ⊢ ( ( 𝐴 . 𝐵 𝐶 ) + ( 𝐷 . 𝐸 𝐹 ) ) = ( 𝐺 . 𝐻 𝐼 )