Metamath Proof Explorer

Theorem dp2cl

Description: Closure for the decimal fraction constructor if both values are reals. (Contributed by David A. Wheeler, 15-May-2015)

Ref Expression
Assertion dp2cl 
|- ( ( A e. RR /\ B e. RR ) -> _ A B e. RR )

Proof

Step Hyp Ref Expression
1 df-dp2 
 |-  _ A B = ( A + ( B / ; 1 0 ) )
2 10re 
 |-  ; 1 0 e. RR
3 10pos 
 |-  0 < ; 1 0
4 2 3 gt0ne0ii 
 |-  ; 1 0 =/= 0
5 redivcl 
 |-  ( ( B e. RR /\ ; 1 0 e. RR /\ ; 1 0 =/= 0 ) -> ( B / ; 1 0 ) e. RR )
6 2 4 5 mp3an23 
 |-  ( B e. RR -> ( B / ; 1 0 ) e. RR )
7 readdcl 
 |-  ( ( A e. RR /\ ( B / ; 1 0 ) e. RR ) -> ( A + ( B / ; 1 0 ) ) e. RR )
8 6 7 sylan2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + ( B / ; 1 0 ) ) e. RR )
9 1 8 eqeltrid 
 |-  ( ( A e. RR /\ B e. RR ) -> _ A B e. RR )