dp3mul10

Description: Multiply by 10 a decimal expansion with 3 digits. (Contributed by Thierry Arnoux, 25-Dec-2021)

	Ref	Expression
Hypotheses	dp3mul10.a	$⊢ A \in ℕ_{0}$
	dp3mul10.b	$⊢ B \in ℕ_{0}$
	dp3mul10.c	$⊢ C \in ℝ$
Assertion	dp3mul10	Could not format assertion : No typesetting found for \|- ( ( A . _ B C ) x. ; 1 0 ) = ( ; A B . C ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		dp3mul10.a	$⊢ A \in ℕ_{0}$
2		dp3mul10.b	$⊢ B \in ℕ_{0}$
3		dp3mul10.c	$⊢ C \in ℝ$
4	2	nn0rei	$⊢ B \in ℝ$
5		dp2cl	Could not format ( ( B e. RR /\ C e. RR ) -> _ B C e. RR ) : No typesetting found for \|- ( ( B e. RR /\ C e. RR ) -> _ B C e. RR ) with typecode \|-
6	4 3 5	mp2an	Could not format _ B C e. RR : No typesetting found for \|- _ B C e. RR with typecode \|-
7	1 6	dpmul10	Could not format ( ( A . _ B C ) x. ; 1 0 ) = ; A _ B C : No typesetting found for \|- ( ( A . _ B C ) x. ; 1 0 ) = ; A _ B C with typecode \|-
8		dfdec10	Could not format ; A _ B C = ( ( ; 1 0 x. A ) + _ B C ) : No typesetting found for \|- ; A _ B C = ( ( ; 1 0 x. A ) + _ B C ) with typecode \|-
9		10nn	$⊢ 10 \in ℕ$
10	9	nncni	$⊢ 10 \in ℂ$
11	1	nn0cni	$⊢ A \in ℂ$
12	10 11	mulcli	$⊢ 10 A \in ℂ$
13	4	recni	$⊢ B \in ℂ$
14	3	recni	$⊢ C \in ℂ$
15	9	nnne0i	$⊢ 10 \neq 0$
16	14 10 15	divcli	$⊢ \frac{C}{10} \in ℂ$
17	12 13 16	addassi	$⊢ 10 A + B + (\frac{C}{10}) = 10 A + B + (\frac{C}{10})$
18		dfdec10	Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for \|- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode \|-
19	18	oveq1i	Could not format ( ; A B + ( C / ; 1 0 ) ) = ( ( ( ; 1 0 x. A ) + B ) + ( C / ; 1 0 ) ) : No typesetting found for \|- ( ; A B + ( C / ; 1 0 ) ) = ( ( ( ; 1 0 x. A ) + B ) + ( C / ; 1 0 ) ) with typecode \|-
20		df-dp2	Could not format _ B C = ( B + ( C / ; 1 0 ) ) : No typesetting found for \|- _ B C = ( B + ( C / ; 1 0 ) ) with typecode \|-
21	20	oveq2i	Could not format ( ( ; 1 0 x. A ) + _ B C ) = ( ( ; 1 0 x. A ) + ( B + ( C / ; 1 0 ) ) ) : No typesetting found for \|- ( ( ; 1 0 x. A ) + _ B C ) = ( ( ; 1 0 x. A ) + ( B + ( C / ; 1 0 ) ) ) with typecode \|-
22	17 19 21	3eqtr4ri	Could not format ( ( ; 1 0 x. A ) + _ B C ) = ( ; A B + ( C / ; 1 0 ) ) : No typesetting found for \|- ( ( ; 1 0 x. A ) + _ B C ) = ( ; A B + ( C / ; 1 0 ) ) with typecode \|-
23	1 2	deccl	Could not format ; A B e. NN0 : No typesetting found for \|- ; A B e. NN0 with typecode \|-
24	23 3	dpval2	Could not format ( ; A B . C ) = ( ; A B + ( C / ; 1 0 ) ) : No typesetting found for \|- ( ; A B . C ) = ( ; A B + ( C / ; 1 0 ) ) with typecode \|-
25	22 24	eqtr4i	Could not format ( ( ; 1 0 x. A ) + _ B C ) = ( ; A B . C ) : No typesetting found for \|- ( ( ; 1 0 x. A ) + _ B C ) = ( ; A B . C ) with typecode \|-
26	7 8 25	3eqtri	Could not format ( ( A . _ B C ) x. ; 1 0 ) = ( ; A B . C ) : No typesetting found for \|- ( ( A . _ B C ) x. ; 1 0 ) = ( ; A B . C ) with typecode \|-

Metamath Proof Explorer

Theorem dp3mul10

Proof