dpadd

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

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

Proof

Step	Hyp	Ref	Expression
1		dpmul.a	$⊢ A \in ℕ_{0}$
2		dpmul.b	$⊢ B \in ℕ_{0}$
3		dpmul.c	$⊢ C \in ℕ_{0}$
4		dpmul.d	$⊢ D \in ℕ_{0}$
5		dpmul.e	$⊢ E \in ℕ_{0}$
6		dpadd.f	$⊢ F \in ℕ_{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 ℕ$
13	12	nncni	$⊢ 10 \in ℂ$
14	12	nnne0i	$⊢ 10 \neq 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	$⊢ (A . B) + (C . D) = E . F$

Metamath Proof Explorer

Theorem dpadd

Proof