dfdec100

Description: Split the hundreds from a decimal value. (Contributed by Thierry Arnoux, 25-Dec-2021)

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

Proof

Step	Hyp	Ref	Expression
1		dfdec100.a	$⊢ A \in ℕ_{0}$
2		dfdec100.b	$⊢ B \in ℕ_{0}$
3		dfdec100.c	$⊢ C \in ℝ$
4		dfdec10	Could not format ; B C = ( ( ; 1 0 x. B ) + C ) : No typesetting found for \|- ; B C = ( ( ; 1 0 x. B ) + C ) with typecode \|-
5	4	oveq2i	Could not format ( ( ; ; 1 0 0 x. A ) + ; B C ) = ( ( ; ; 1 0 0 x. A ) + ( ( ; 1 0 x. B ) + C ) ) : No typesetting found for \|- ( ( ; ; 1 0 0 x. A ) + ; B C ) = ( ( ; ; 1 0 0 x. A ) + ( ( ; 1 0 x. B ) + C ) ) with typecode \|-
6		10nn0	$⊢ 10 \in ℕ_{0}$
7	6	dec0u	$⊢ 10 \cdot 10 = 100$
8	6	nn0cni	$⊢ 10 \in ℂ$
9	8 8	mulcli	$⊢ 10 \cdot 10 \in ℂ$
10	7 9	eqeltrri	$⊢ 100 \in ℂ$
11	1	nn0cni	$⊢ A \in ℂ$
12	10 11	mulcli	$⊢ 100 A \in ℂ$
13	2	nn0cni	$⊢ B \in ℂ$
14	8 13	mulcli	$⊢ 10 B \in ℂ$
15	3	recni	$⊢ C \in ℂ$
16	12 14 15	addassi	$⊢ 100 A + 10 B + C = 100 A + 10 B + C$
17		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 \|-
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	oveq2i	Could not format ( ; 1 0 x. ; A B ) = ( ; 1 0 x. ( ( ; 1 0 x. A ) + B ) ) : No typesetting found for \|- ( ; 1 0 x. ; A B ) = ( ; 1 0 x. ( ( ; 1 0 x. A ) + B ) ) with typecode \|-
20	8 11	mulcli	$⊢ 10 A \in ℂ$
21	8 20 13	adddii	$⊢ 10 (10 A + B) = 10 10 A + 10 B$
22	8 8 11	mulassi	$⊢ 10 \cdot 10 A = 10 10 A$
23	7	oveq1i	$⊢ 10 \cdot 10 A = 100 A$
24	22 23	eqtr3i	$⊢ 10 10 A = 100 A$
25	24	oveq1i	$⊢ 10 10 A + 10 B = 100 A + 10 B$
26	19 21 25	3eqtri	Could not format ( ; 1 0 x. ; A B ) = ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) : No typesetting found for \|- ( ; 1 0 x. ; A B ) = ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) with typecode \|-
27	26	oveq1i	Could not format ( ( ; 1 0 x. ; A B ) + C ) = ( ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) + C ) : No typesetting found for \|- ( ( ; 1 0 x. ; A B ) + C ) = ( ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) + C ) with typecode \|-
28	17 27	eqtr2i	Could not format ( ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) + C ) = ; ; A B C : No typesetting found for \|- ( ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) + C ) = ; ; A B C with typecode \|-
29	5 16 28	3eqtr2ri	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 \|-

Metamath Proof Explorer

Theorem dfdec100

Proof