Metamath Proof Explorer

Theorem dpfrac1

Description: Prove a simple equivalence involving the decimal point. See df-dp and dpcl . (Contributed by David A. Wheeler, 15-May-2015) (Revised by AV, 9-Sep-2021)

Ref Expression
Assertion dpfrac1 
|- ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = ( ; A B / ; 1 0 ) )

Proof

Step Hyp Ref Expression
1 df-dp2 
 |-  _ A B = ( A + ( B / ; 1 0 ) )
2 dpval 
 |-  ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = _ A B )
3 nn0cn 
 |-  ( A e. NN0 -> A e. CC )
4 recn 
 |-  ( B e. RR -> B e. CC )
5 dfdec10 
 |-  ; A B = ( ( ; 1 0 x. A ) + B )
6 5 oveq1i 
 |-  ( ; A B / ; 1 0 ) = ( ( ( ; 1 0 x. A ) + B ) / ; 1 0 )
7 10re 
 |-  ; 1 0 e. RR
8 7 recni 
 |-  ; 1 0 e. CC
9 8 a1i 
 |-  ( A e. CC -> ; 1 0 e. CC )
10 id 
 |-  ( A e. CC -> A e. CC )
11 9 10 mulcld 
 |-  ( A e. CC -> ( ; 1 0 x. A ) e. CC )
12 10pos 
 |-  0 < ; 1 0
13 7 12 gt0ne0ii 
 |-  ; 1 0 =/= 0
14 8 13 pm3.2i 
 |-  ( ; 1 0 e. CC /\ ; 1 0 =/= 0 )
15 divdir 
 |-  ( ( ( ; 1 0 x. A ) e. CC /\ B e. CC /\ ( ; 1 0 e. CC /\ ; 1 0 =/= 0 ) ) -> ( ( ( ; 1 0 x. A ) + B ) / ; 1 0 ) = ( ( ( ; 1 0 x. A ) / ; 1 0 ) + ( B / ; 1 0 ) ) )
16 14 15 mp3an3 
 |-  ( ( ( ; 1 0 x. A ) e. CC /\ B e. CC ) -> ( ( ( ; 1 0 x. A ) + B ) / ; 1 0 ) = ( ( ( ; 1 0 x. A ) / ; 1 0 ) + ( B / ; 1 0 ) ) )
17 11 16 sylan 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ; 1 0 x. A ) + B ) / ; 1 0 ) = ( ( ( ; 1 0 x. A ) / ; 1 0 ) + ( B / ; 1 0 ) ) )
18 divcan3 
 |-  ( ( A e. CC /\ ; 1 0 e. CC /\ ; 1 0 =/= 0 ) -> ( ( ; 1 0 x. A ) / ; 1 0 ) = A )
19 8 13 18 mp3an23 
 |-  ( A e. CC -> ( ( ; 1 0 x. A ) / ; 1 0 ) = A )
20 19 oveq1d 
 |-  ( A e. CC -> ( ( ( ; 1 0 x. A ) / ; 1 0 ) + ( B / ; 1 0 ) ) = ( A + ( B / ; 1 0 ) ) )
21 20 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ; 1 0 x. A ) / ; 1 0 ) + ( B / ; 1 0 ) ) = ( A + ( B / ; 1 0 ) ) )
22 17 21 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ; 1 0 x. A ) + B ) / ; 1 0 ) = ( A + ( B / ; 1 0 ) ) )
23 6 22 eqtrid 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ; A B / ; 1 0 ) = ( A + ( B / ; 1 0 ) ) )
24 3 4 23 syl2an 
 |-  ( ( A e. NN0 /\ B e. RR ) -> ( ; A B / ; 1 0 ) = ( A + ( B / ; 1 0 ) ) )
25 1 2 24 3eqtr4a 
 |-  ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = ( ; A B / ; 1 0 ) )