This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem decdiv10

Description: Divide a decimal number by 10. (Contributed by Thierry Arnoux, 25-Dec-2021)

Ref Expression
Hypotheses dpval2.a ⊢ A ∈ ℕ 0
dpval2.b ⊢ B ∈ ℝ
Assertion decdiv10 Could not format assertion : No typesetting found for |- ( ; A B / ; 1 0 ) = ( A . B ) with typecode |-

Proof

Step Hyp Ref Expression
1 dpval2.a ⊢ A ∈ ℕ 0
2 dpval2.b ⊢ B ∈ ℝ
3 1 2 dpmul10 Could not format ( ( A . B ) x. ; 1 0 ) = ; A B : No typesetting found for |- ( ( A . B ) x. ; 1 0 ) = ; A B with typecode |-
4 3 oveq1i Could not format ( ( ( A . B ) x. ; 1 0 ) / ; 1 0 ) = ( ; A B / ; 1 0 ) : No typesetting found for |- ( ( ( A . B ) x. ; 1 0 ) / ; 1 0 ) = ( ; A B / ; 1 0 ) with typecode |-
5 dpcl ⊢ A ∈ ℕ 0 ∧ B ∈ ℝ → A . B ∈ ℝ
6 1 2 5 mp2an ⊢ A . B ∈ ℝ
7 6 recni ⊢ A . B ∈ ℂ
8 10nn ⊢ 10 ∈ ℕ
9 8 nncni ⊢ 10 ∈ ℂ
10 8 nnne0i ⊢ 10 ≠ 0
11 7 9 10 divcan4i ⊢ A . B ⋅ 10 10 = A . B
12 4 11 eqtr3i Could not format ( ; A B / ; 1 0 ) = ( A . B ) : No typesetting found for |- ( ; A B / ; 1 0 ) = ( A . B ) with typecode |-