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

Metamath Proof Explorer

Theorem dp20h

Description: Add a zero in the unit places. (Contributed by Thierry Arnoux, 16-Dec-2021)

Ref Expression
Hypothesis dp20h.1 ⊢ 𝐴 ∈ ℝ+
Assertion dp20h 0 𝐴 = ( 𝐴 / 1 0 )

Proof

Step Hyp Ref Expression
1 dp20h.1 ⊢ 𝐴 ∈ ℝ+
2 df-dp2 ⊢ 0 𝐴 = ( 0 + ( 𝐴 / 1 0 ) )
3 rpcn ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
4 1 3 ax-mp ⊢ 𝐴 ∈ ℂ
5 10nn0 ⊢ 1 0 ∈ ℕ0
6 5 nn0cni ⊢ 1 0 ∈ ℂ
7 0re ⊢ 0 ∈ ℝ
8 10pos ⊢ 0 < 1 0
9 7 8 gtneii ⊢ 1 0 ≠ 0
10 4 6 9 divcli ⊢ ( 𝐴 / 1 0 ) ∈ ℂ
11 10 addlidi ⊢ ( 0 + ( 𝐴 / 1 0 ) ) = ( 𝐴 / 1 0 )
12 2 11 eqtri ⊢ 0 𝐴 = ( 𝐴 / 1 0 )