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\in {\mathbb{N}}_0\to A\in ℂ$$
4		recn	$$⊢B\in ℝ\to B\in ℂ$$
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\in ℝ$$
8	7	recni	$$⊢10\in ℂ$$
9	8	a1i	$$⊢A\in ℂ\to 10\in ℂ$$
10		id	$$⊢A\in ℂ\to A\in ℂ$$
11	9 10	mulcld	$$⊢A\in ℂ\to 10A\in ℂ$$
12		10pos	$$⊢0<10$$
13	7 12	gt0ne0ii	$$⊢10\ne 0$$
14	8 13	pm3.2i	$$⊢\left(10\in ℂ\wedge 10\ne 0\right)$$
15		divdir	$$⊢\left(10A\in ℂ\wedge B\in ℂ\wedge \left(10\in ℂ\wedge 10\ne 0\right)\right)\to \frac{10A+B}{10}=\left(\frac{10A}{10}\right)+\left(\frac{B}{10}\right)$$
16	14 15	mp3an3	$$⊢\left(10A\in ℂ\wedge B\in ℂ\right)\to \frac{10A+B}{10}=\left(\frac{10A}{10}\right)+\left(\frac{B}{10}\right)$$
17	11 16	sylan	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \frac{10A+B}{10}=\left(\frac{10A}{10}\right)+\left(\frac{B}{10}\right)$$
18		divcan3	$$⊢\left(A\in ℂ\wedge 10\in ℂ\wedge 10\ne 0\right)\to \frac{10A}{10}=A$$
19	8 13 18	mp3an23	$$⊢A\in ℂ\to \frac{10A}{10}=A$$
20	19	oveq1d	$$⊢A\in ℂ\to \left(\frac{10A}{10}\right)+\left(\frac{B}{10}\right)=A+\left(\frac{B}{10}\right)$$
21	20	adantr	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(\frac{10A}{10}\right)+\left(\frac{B}{10}\right)=A+\left(\frac{B}{10}\right)$$
22	17 21	eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \frac{10A+B}{10}=A+\left(\frac{B}{10}\right)$$
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 |-