Theorem dpadd

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

	Ref	Expression
Hypotheses	dpmul.a	$$⊢A\in {\mathbb{N}}_0$$
	dpmul.b	$$⊢B\in {\mathbb{N}}_0$$
	dpmul.c	$$⊢C\in {\mathbb{N}}_0$$
	dpmul.d	$$⊢D\in {\mathbb{N}}_0$$
	dpmul.e	$$⊢E\in {\mathbb{N}}_0$$
	dpadd.f	$$⊢F\in {\mathbb{N}}_0$$
	dpadd.1	No typesetting found for |- ( ; A B + ; C D ) = ; E F with typecode |-
Assertion	dpadd	$$⊢\left(A.B\right)+\left(C.D\right)=E.F$$

Proof

Step	Hyp	Ref	Expression
1		dpmul.a	$$⊢A\in {\mathbb{N}}_0$$
2		dpmul.b	$$⊢B\in {\mathbb{N}}_0$$
3		dpmul.c	$$⊢C\in {\mathbb{N}}_0$$
4		dpmul.d	$$⊢D\in {\mathbb{N}}_0$$
5		dpmul.e	$$⊢E\in {\mathbb{N}}_0$$
6		dpadd.f	$$⊢F\in {\mathbb{N}}_0$$
7		dpadd.1	Could not format ( ; A B + ; C D ) = ; E F : No typesetting found for |- ( ; A B + ; C D ) = ; E F with typecode |-
8	1 2	deccl	Could not format ; A B e. NN0 : No typesetting found for |- ; A B e. NN0 with typecode |-
9	8	nn0cni	Could not format ; A B e. CC : No typesetting found for |- ; A B e. CC with typecode |-
10	3 4	deccl	Could not format ; C D e. NN0 : No typesetting found for |- ; C D e. NN0 with typecode |-
11	10	nn0cni	Could not format ; C D e. CC : No typesetting found for |- ; C D e. CC with typecode |-
12		10nn	$$⊢10\in \mathbb{N}$$
13	12	nncni	$$⊢10\in ℂ$$
14	12	nnne0i	$$⊢10\ne 0$$
15	9 11 13 14	divdiri	Could not format ( ( ; A B + ; C D ) / ; 1 0 ) = ( ( ; A B / ; 1 0 ) + ( ; C D / ; 1 0 ) ) : No typesetting found for |- ( ( ; A B + ; C D ) / ; 1 0 ) = ( ( ; A B / ; 1 0 ) + ( ; C D / ; 1 0 ) ) with typecode |-
16	7	oveq1i	Could not format ( ( ; A B + ; C D ) / ; 1 0 ) = ( ; E F / ; 1 0 ) : No typesetting found for |- ( ( ; A B + ; C D ) / ; 1 0 ) = ( ; E F / ; 1 0 ) with typecode |-
17	15 16	eqtr3i	Could not format ( ( ; A B / ; 1 0 ) + ( ; C D / ; 1 0 ) ) = ( ; E F / ; 1 0 ) : No typesetting found for |- ( ( ; A B / ; 1 0 ) + ( ; C D / ; 1 0 ) ) = ( ; E F / ; 1 0 ) with typecode |-
18	2	nn0rei	$$⊢B\in ℝ$$
19	1 18	decdiv10	Could not format ( ; A B / ; 1 0 ) = ( A . B ) : No typesetting found for |- ( ; A B / ; 1 0 ) = ( A . B ) with typecode |-
20	4	nn0rei	$$⊢D\in ℝ$$
21	3 20	decdiv10	Could not format ( ; C D / ; 1 0 ) = ( C . D ) : No typesetting found for |- ( ; C D / ; 1 0 ) = ( C . D ) with typecode |-
22	19 21	oveq12i	Could not format ( ( ; A B / ; 1 0 ) + ( ; C D / ; 1 0 ) ) = ( ( A . B ) + ( C . D ) ) : No typesetting found for |- ( ( ; A B / ; 1 0 ) + ( ; C D / ; 1 0 ) ) = ( ( A . B ) + ( C . D ) ) with typecode |-
23	6	nn0rei	$$⊢F\in ℝ$$
24	5 23	decdiv10	Could not format ( ; E F / ; 1 0 ) = ( E . F ) : No typesetting found for |- ( ; E F / ; 1 0 ) = ( E . F ) with typecode |-
25	17 22 24	3eqtr3i	$$⊢\left(A.B\right)+\left(C.D\right)=E.F$$