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

Metamath Proof Explorer

Theorem dpadd2

Description: Addition with one decimal, no carry. (Contributed by Thierry Arnoux, 29-Dec-2021)

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

Proof

Step Hyp Ref Expression
1 dpadd2.a ⊢ 𝐴 ∈ ℕ0
2 dpadd2.b ⊢ 𝐵 ∈ ℝ+
3 dpadd2.c ⊢ 𝐶 ∈ ℕ0
4 dpadd2.d ⊢ 𝐷 ∈ ℝ+
5 dpadd2.e ⊢ 𝐸 ∈ ℕ0
6 dpadd2.f ⊢ 𝐹 ∈ ℝ+
7 dpadd2.g ⊢ 𝐺 ∈ ℕ0
8 dpadd2.h ⊢ 𝐻 ∈ ℕ0
9 dpadd2.i ⊢ ( 𝐺 + 𝐻 ) = 𝐼
10 dpadd2.1 ⊢ ( ( 𝐴 . 𝐵 ) + ( 𝐶 . 𝐷 ) ) = ( 𝐸 . 𝐹 )
11 1 nn0rei ⊢ 𝐴 ∈ ℝ
12 rpre ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ )
13 2 12 ax-mp ⊢ 𝐵 ∈ ℝ
14 dp2cl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 𝐵 ∈ ℝ )
15 11 13 14 mp2an ⊢ 𝐴 𝐵 ∈ ℝ
16 7 15 dpval2 ⊢ ( 𝐺 . 𝐴 𝐵 ) = ( 𝐺 + ( 𝐴 𝐵 / 1 0 ) )
17 3 nn0rei ⊢ 𝐶 ∈ ℝ
18 rpre ⊢ ( 𝐷 ∈ ℝ+ → 𝐷 ∈ ℝ )
19 4 18 ax-mp ⊢ 𝐷 ∈ ℝ
20 dp2cl ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → 𝐶 𝐷 ∈ ℝ )
21 17 19 20 mp2an ⊢ 𝐶 𝐷 ∈ ℝ
22 8 21 dpval2 ⊢ ( 𝐻 . 𝐶 𝐷 ) = ( 𝐻 + ( 𝐶 𝐷 / 1 0 ) )
23 16 22 oveq12i ⊢ ( ( 𝐺 . 𝐴 𝐵 ) + ( 𝐻 . 𝐶 𝐷 ) ) = ( ( 𝐺 + ( 𝐴 𝐵 / 1 0 ) ) + ( 𝐻 + ( 𝐶 𝐷 / 1 0 ) ) )
24 7 nn0cni ⊢ 𝐺 ∈ ℂ
25 15 recni ⊢ 𝐴 𝐵 ∈ ℂ
26 10nn ⊢ 1 0 ∈ ℕ
27 26 nncni ⊢ 1 0 ∈ ℂ
28 26 nnne0i ⊢ 1 0 ≠ 0
29 25 27 28 divcli ⊢ ( 𝐴 𝐵 / 1 0 ) ∈ ℂ
30 8 nn0cni ⊢ 𝐻 ∈ ℂ
31 21 recni ⊢ 𝐶 𝐷 ∈ ℂ
32 31 27 28 divcli ⊢ ( 𝐶 𝐷 / 1 0 ) ∈ ℂ
33 24 29 30 32 add4i ⊢ ( ( 𝐺 + ( 𝐴 𝐵 / 1 0 ) ) + ( 𝐻 + ( 𝐶 𝐷 / 1 0 ) ) ) = ( ( 𝐺 + 𝐻 ) + ( ( 𝐴 𝐵 / 1 0 ) + ( 𝐶 𝐷 / 1 0 ) ) )
34 25 31 27 28 divdiri ⊢ ( ( 𝐴 𝐵 + 𝐶 𝐷 ) / 1 0 ) = ( ( 𝐴 𝐵 / 1 0 ) + ( 𝐶 𝐷 / 1 0 ) )
35 dpval ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 . 𝐵 ) = 𝐴 𝐵 )
36 1 13 35 mp2an ⊢ ( 𝐴 . 𝐵 ) = 𝐴 𝐵
37 dpval ⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℝ ) → ( 𝐶 . 𝐷 ) = 𝐶 𝐷 )
38 3 19 37 mp2an ⊢ ( 𝐶 . 𝐷 ) = 𝐶 𝐷
39 36 38 oveq12i ⊢ ( ( 𝐴 . 𝐵 ) + ( 𝐶 . 𝐷 ) ) = ( 𝐴 𝐵 + 𝐶 𝐷 )
40 rpre ⊢ ( 𝐹 ∈ ℝ+ → 𝐹 ∈ ℝ )
41 6 40 ax-mp ⊢ 𝐹 ∈ ℝ
42 dpval ⊢ ( ( 𝐸 ∈ ℕ0 ∧ 𝐹 ∈ ℝ ) → ( 𝐸 . 𝐹 ) = 𝐸 𝐹 )
43 5 41 42 mp2an ⊢ ( 𝐸 . 𝐹 ) = 𝐸 𝐹
44 10 39 43 3eqtr3i ⊢ ( 𝐴 𝐵 + 𝐶 𝐷 ) = 𝐸 𝐹
45 44 oveq1i ⊢ ( ( 𝐴 𝐵 + 𝐶 𝐷 ) / 1 0 ) = ( 𝐸 𝐹 / 1 0 )
46 34 45 eqtr3i ⊢ ( ( 𝐴 𝐵 / 1 0 ) + ( 𝐶 𝐷 / 1 0 ) ) = ( 𝐸 𝐹 / 1 0 )
47 9 46 oveq12i ⊢ ( ( 𝐺 + 𝐻 ) + ( ( 𝐴 𝐵 / 1 0 ) + ( 𝐶 𝐷 / 1 0 ) ) ) = ( 𝐼 + ( 𝐸 𝐹 / 1 0 ) )
48 7 8 nn0addcli ⊢ ( 𝐺 + 𝐻 ) ∈ ℕ0
49 9 48 eqeltrri ⊢ 𝐼 ∈ ℕ0
50 5 nn0rei ⊢ 𝐸 ∈ ℝ
51 dp2cl ⊢ ( ( 𝐸 ∈ ℝ ∧ 𝐹 ∈ ℝ ) → 𝐸 𝐹 ∈ ℝ )
52 50 41 51 mp2an ⊢ 𝐸 𝐹 ∈ ℝ
53 49 52 dpval2 ⊢ ( 𝐼 . 𝐸 𝐹 ) = ( 𝐼 + ( 𝐸 𝐹 / 1 0 ) )
54 47 53 eqtr4i ⊢ ( ( 𝐺 + 𝐻 ) + ( ( 𝐴 𝐵 / 1 0 ) + ( 𝐶 𝐷 / 1 0 ) ) ) = ( 𝐼 . 𝐸 𝐹 )
55 23 33 54 3eqtri ⊢ ( ( 𝐺 . 𝐴 𝐵 ) + ( 𝐻 . 𝐶 𝐷 ) ) = ( 𝐼 . 𝐸 𝐹 )