Theorem dpadd

Description: Addition with one decimal. (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
	dpadd.f	⊢ 𝐹 ∈ ℕ0
	dpadd.1	⊢ ( ; 𝐴 𝐵 + ; 𝐶 𝐷 ) = ; 𝐸 𝐹
Assertion	dpadd	⊢ ( ( 𝐴 . 𝐵 ) + ( 𝐶 . 𝐷 ) ) = ( 𝐸 . 𝐹 )

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		dpadd.f	⊢ 𝐹 ∈ ℕ0
7		dpadd.1	⊢ ( ; 𝐴 𝐵 + ; 𝐶 𝐷 ) = ; 𝐸 𝐹
8	1 2	deccl	⊢ ; 𝐴 𝐵 ∈ ℕ0
9	8	nn0cni	⊢ ; 𝐴 𝐵 ∈ ℂ
10	3 4	deccl	⊢ ; 𝐶 𝐷 ∈ ℕ0
11	10	nn0cni	⊢ ; 𝐶 𝐷 ∈ ℂ
12		10nn	⊢ ; 1 0 ∈ ℕ
13	12	nncni	⊢ ; 1 0 ∈ ℂ
14	12	nnne0i	⊢ ; 1 0 ≠ 0
15	9 11 13 14	divdiri	⊢ ( ( ; 𝐴 𝐵 + ; 𝐶 𝐷 ) / ; 1 0 ) = ( ( ; 𝐴 𝐵 / ; 1 0 ) + ( ; 𝐶 𝐷 / ; 1 0 ) )
16	7	oveq1i	⊢ ( ( ; 𝐴 𝐵 + ; 𝐶 𝐷 ) / ; 1 0 ) = ( ; 𝐸 𝐹 / ; 1 0 )
17	15 16	eqtr3i	⊢ ( ( ; 𝐴 𝐵 / ; 1 0 ) + ( ; 𝐶 𝐷 / ; 1 0 ) ) = ( ; 𝐸 𝐹 / ; 1 0 )
18	2	nn0rei	⊢ 𝐵 ∈ ℝ
19	1 18	decdiv10	⊢ ( ; 𝐴 𝐵 / ; 1 0 ) = ( 𝐴 . 𝐵 )
20	4	nn0rei	⊢ 𝐷 ∈ ℝ
21	3 20	decdiv10	⊢ ( ; 𝐶 𝐷 / ; 1 0 ) = ( 𝐶 . 𝐷 )
22	19 21	oveq12i	⊢ ( ( ; 𝐴 𝐵 / ; 1 0 ) + ( ; 𝐶 𝐷 / ; 1 0 ) ) = ( ( 𝐴 . 𝐵 ) + ( 𝐶 . 𝐷 ) )
23	6	nn0rei	⊢ 𝐹 ∈ ℝ
24	5 23	decdiv10	⊢ ( ; 𝐸 𝐹 / ; 1 0 ) = ( 𝐸 . 𝐹 )
25	17 22 24	3eqtr3i	⊢ ( ( 𝐴 . 𝐵 ) + ( 𝐶 . 𝐷 ) ) = ( 𝐸 . 𝐹 )