Metamath Proof Explorer


Theorem dp3mul10

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

Ref Expression
Hypotheses dp3mul10.a A 0
dp3mul10.b B 0
dp3mul10.c C
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 0
2 dp3mul10.b B 0
3 dp3mul10.c C
4 2 nn0rei B
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
10 9 nncni 10
11 1 nn0cni A
12 10 11 mulcli 10 A
13 4 recni B
14 3 recni C
15 9 nnne0i 10 0
16 14 10 15 divcli C 10
17 12 13 16 addassi 10 A + B + C 10 = 10 A + B + 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 |-