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

Metamath Proof Explorer

Theorem decsplit1

Description: Split a decimal number into two parts. Base case: N = 1 . (Contributed by Mario Carneiro, 16-Jul-2015) (Revised by AV, 8-Sep-2021)

Ref Expression
Hypothesis decsplit0.1 ⊢ A ∈ ℕ 0
Assertion decsplit1 Could not format assertion : No typesetting found for |- ( ( A x. ( ; 1 0 ^ 1 ) ) + B ) = ; A B with typecode |-

Proof

Step Hyp Ref Expression
1 decsplit0.1 ⊢ A ∈ ℕ 0
2 10nn0 ⊢ 10 ∈ ℕ 0
3 2 numexp1 ⊢ 10 1 = 10
4 3 oveq2i ⊢ A ⁢ 10 1 = A ⋅ 10
5 2 nn0cni ⊢ 10 ∈ ℂ
6 1 nn0cni ⊢ A ∈ ℂ
7 5 6 mulcomi ⊢ 10 ⁢ A = A ⋅ 10
8 4 7 eqtr4i ⊢ A ⁢ 10 1 = 10 ⁢ A
9 8 oveq1i ⊢ A ⁢ 10 1 + B = 10 ⁢ A + B
10 dfdec10 Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
11 9 10 eqtr4i Could not format ( ( A x. ( ; 1 0 ^ 1 ) ) + B ) = ; A B : No typesetting found for |- ( ( A x. ( ; 1 0 ^ 1 ) ) + B ) = ; A B with typecode |-