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 
|- A e. RR+
Assertion dp20h 
|- _ 0 A = ( A / ; 1 0 )

Proof

Step Hyp Ref Expression
1 dp20h.1 
 |-  A e. RR+
2 df-dp2 
 |-  _ 0 A = ( 0 + ( A / ; 1 0 ) )
3 rpcn 
 |-  ( A e. RR+ -> A e. CC )
4 1 3 ax-mp 
 |-  A e. CC
5 10nn0 
 |-  ; 1 0 e. NN0
6 5 nn0cni 
 |-  ; 1 0 e. CC
7 0re 
 |-  0 e. RR
8 10pos 
 |-  0 < ; 1 0
9 7 8 gtneii 
 |-  ; 1 0 =/= 0
10 4 6 9 divcli 
 |-  ( A / ; 1 0 ) e. CC
11 10 addid2i 
 |-  ( 0 + ( A / ; 1 0 ) ) = ( A / ; 1 0 )
12 2 11 eqtri 
 |-  _ 0 A = ( A / ; 1 0 )