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 Could not format assertion : No typesetting found for |- ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = ( ; A B / ; 1 0 ) ) with typecode |-

Proof

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