dpmul100

Description: Multiply by 100 a decimal expansion. (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	dpmul100	Could not format assertion : No typesetting found for \|- ( ( A . _ B C ) x. ; ; 1 0 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	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 \|-
8	1	nn0cni	$⊢ A \in ℂ$
9	6	recni	Could not format _ B C e. CC : No typesetting found for \|- _ B C e. CC with typecode \|-
10		10nn0	$⊢ 10 \in ℕ_{0}$
11	10	nn0cni	$⊢ 10 \in ℂ$
12		10nn	$⊢ 10 \in ℕ$
13	12	nnne0i	$⊢ 10 \neq 0$
14	9 11 13	divcli	Could not format ( _ B C / ; 1 0 ) e. CC : No typesetting found for \|- ( _ B C / ; 1 0 ) e. CC with typecode \|-
15	8 14	addcli	Could not format ( A + ( _ B C / ; 1 0 ) ) e. CC : No typesetting found for \|- ( A + ( _ B C / ; 1 0 ) ) e. CC with typecode \|-
16	7 15	eqeltri	Could not format ( A . _ B C ) e. CC : No typesetting found for \|- ( A . _ B C ) e. CC with typecode \|-
17	16 11 11	mulassi	Could not format ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 ) = ( ( A . _ B C ) x. ( ; 1 0 x. ; 1 0 ) ) : No typesetting found for \|- ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 ) = ( ( A . _ B C ) x. ( ; 1 0 x. ; 1 0 ) ) with typecode \|-
18	1 2 3	dfdec100	Could not format ; ; A B C = ( ( ; ; 1 0 0 x. A ) + ; B C ) : No typesetting found for \|- ; ; A B C = ( ( ; ; 1 0 0 x. A ) + ; B C ) with typecode \|-
19	11 8 11	mul32i	$⊢ 10 A \cdot 10 = 10 \cdot 10 A$
20	10	dec0u	$⊢ 10 \cdot 10 = 100$
21	20	oveq1i	$⊢ 10 \cdot 10 A = 100 A$
22	19 21	eqtri	$⊢ 10 A \cdot 10 = 100 A$
23	2 3	dpval3	Could not format ( B . C ) = _ B C : No typesetting found for \|- ( B . C ) = _ B C with typecode \|-
24	23	oveq1i	Could not format ( ( B . C ) x. ; 1 0 ) = ( _ B C x. ; 1 0 ) : No typesetting found for \|- ( ( B . C ) x. ; 1 0 ) = ( _ B C x. ; 1 0 ) with typecode \|-
25	2 3	dpmul10	Could not format ( ( B . C ) x. ; 1 0 ) = ; B C : No typesetting found for \|- ( ( B . C ) x. ; 1 0 ) = ; B C with typecode \|-
26	24 25	eqtr3i	Could not format ( _ B C x. ; 1 0 ) = ; B C : No typesetting found for \|- ( _ B C x. ; 1 0 ) = ; B C with typecode \|-
27	22 26	oveq12i	Could not format ( ( ( ; 1 0 x. A ) x. ; 1 0 ) + ( _ B C x. ; 1 0 ) ) = ( ( ; ; 1 0 0 x. A ) + ; B C ) : No typesetting found for \|- ( ( ( ; 1 0 x. A ) x. ; 1 0 ) + ( _ B C x. ; 1 0 ) ) = ( ( ; ; 1 0 0 x. A ) + ; B C ) with typecode \|-
28	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 \|-
29		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 \|-
30	28 29	eqtri	Could not format ( ( A . _ B C ) x. ; 1 0 ) = ( ( ; 1 0 x. A ) + _ B C ) : No typesetting found for \|- ( ( A . _ B C ) x. ; 1 0 ) = ( ( ; 1 0 x. A ) + _ B C ) with typecode \|-
31	30	oveq1i	Could not format ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 ) = ( ( ( ; 1 0 x. A ) + _ B C ) x. ; 1 0 ) : No typesetting found for \|- ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 ) = ( ( ( ; 1 0 x. A ) + _ B C ) x. ; 1 0 ) with typecode \|-
32	11 8	mulcli	$⊢ 10 A \in ℂ$
33	32 9 11	adddiri	Could not format ( ( ( ; 1 0 x. A ) + _ B C ) x. ; 1 0 ) = ( ( ( ; 1 0 x. A ) x. ; 1 0 ) + ( _ B C x. ; 1 0 ) ) : No typesetting found for \|- ( ( ( ; 1 0 x. A ) + _ B C ) x. ; 1 0 ) = ( ( ( ; 1 0 x. A ) x. ; 1 0 ) + ( _ B C x. ; 1 0 ) ) with typecode \|-
34	31 33	eqtr2i	Could not format ( ( ( ; 1 0 x. A ) x. ; 1 0 ) + ( _ B C x. ; 1 0 ) ) = ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 ) : No typesetting found for \|- ( ( ( ; 1 0 x. A ) x. ; 1 0 ) + ( _ B C x. ; 1 0 ) ) = ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 ) with typecode \|-
35	18 27 34	3eqtr2ri	Could not format ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 ) = ; ; A B C : No typesetting found for \|- ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 ) = ; ; A B C with typecode \|-
36	20	oveq2i	Could not format ( ( A . _ B C ) x. ( ; 1 0 x. ; 1 0 ) ) = ( ( A . _ B C ) x. ; ; 1 0 0 ) : No typesetting found for \|- ( ( A . _ B C ) x. ( ; 1 0 x. ; 1 0 ) ) = ( ( A . _ B C ) x. ; ; 1 0 0 ) with typecode \|-
37	17 35 36	3eqtr3ri	Could not format ( ( A . _ B C ) x. ; ; 1 0 0 ) = ; ; A B C : No typesetting found for \|- ( ( A . _ B C ) x. ; ; 1 0 0 ) = ; ; A B C with typecode \|-

Metamath Proof Explorer

Theorem dpmul100

Proof