This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid 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 |-