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 syl5eq
 |-  ( ( 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 ) )