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 | ⊢ 𝐴 ∈ ℕ0 | |
| Assertion | decsplit1 | ⊢ ( ( 𝐴 · ( ; 1 0 ↑ 1 ) ) + 𝐵 ) = ; 𝐴 𝐵 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | decsplit0.1 | ⊢ 𝐴 ∈ ℕ0 | |
| 2 | 10nn0 | ⊢ ; 1 0 ∈ ℕ0 | |
| 3 | 2 | numexp1 | ⊢ ( ; 1 0 ↑ 1 ) = ; 1 0 |
| 4 | 3 | oveq2i | ⊢ ( 𝐴 · ( ; 1 0 ↑ 1 ) ) = ( 𝐴 · ; 1 0 ) |
| 5 | 2 | nn0cni | ⊢ ; 1 0 ∈ ℂ |
| 6 | 1 | nn0cni | ⊢ 𝐴 ∈ ℂ |
| 7 | 5 6 | mulcomi | ⊢ ( ; 1 0 · 𝐴 ) = ( 𝐴 · ; 1 0 ) |
| 8 | 4 7 | eqtr4i | ⊢ ( 𝐴 · ( ; 1 0 ↑ 1 ) ) = ( ; 1 0 · 𝐴 ) |
| 9 | 8 | oveq1i | ⊢ ( ( 𝐴 · ( ; 1 0 ↑ 1 ) ) + 𝐵 ) = ( ( ; 1 0 · 𝐴 ) + 𝐵 ) |
| 10 | dfdec10 | ⊢ ; 𝐴 𝐵 = ( ( ; 1 0 · 𝐴 ) + 𝐵 ) | |
| 11 | 9 10 | eqtr4i | ⊢ ( ( 𝐴 · ( ; 1 0 ↑ 1 ) ) + 𝐵 ) = ; 𝐴 𝐵 |