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 ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 . 𝐵 ) = ( 𝐴 𝐵 / 1 0 ) )

Proof

Step Hyp Ref Expression
1 df-dp2 ⊢ 𝐴 𝐵 = ( 𝐴 + ( 𝐵 / 1 0 ) )
2 dpval ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 . 𝐵 ) = 𝐴 𝐵 )
3 nn0cn ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ )
4 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
5 dfdec10 ⊢ 𝐴 𝐵 = ( ( 1 0 · 𝐴 ) + 𝐵 )
6 5 oveq1i ⊢ ( 𝐴 𝐵 / 1 0 ) = ( ( ( 1 0 · 𝐴 ) + 𝐵 ) / 1 0 )
7 10re ⊢ 1 0 ∈ ℝ
8 7 recni ⊢ 1 0 ∈ ℂ
9 8 a1i ⊢ ( 𝐴 ∈ ℂ → 1 0 ∈ ℂ )
10 id ⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
11 9 10 mulcld ⊢ ( 𝐴 ∈ ℂ → ( 1 0 · 𝐴 ) ∈ ℂ )
12 10pos ⊢ 0 < 1 0
13 7 12 gt0ne0ii ⊢ 1 0 ≠ 0
14 8 13 pm3.2i ⊢ ( 1 0 ∈ ℂ ∧ 1 0 ≠ 0 )
15 divdir ⊢ ( ( ( 1 0 · 𝐴 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 1 0 ∈ ℂ ∧ 1 0 ≠ 0 ) ) → ( ( ( 1 0 · 𝐴 ) + 𝐵 ) / 1 0 ) = ( ( ( 1 0 · 𝐴 ) / 1 0 ) + ( 𝐵 / 1 0 ) ) )
16 14 15 mp3an3 ⊢ ( ( ( 1 0 · 𝐴 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 1 0 · 𝐴 ) + 𝐵 ) / 1 0 ) = ( ( ( 1 0 · 𝐴 ) / 1 0 ) + ( 𝐵 / 1 0 ) ) )
17 11 16 sylan ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 1 0 · 𝐴 ) + 𝐵 ) / 1 0 ) = ( ( ( 1 0 · 𝐴 ) / 1 0 ) + ( 𝐵 / 1 0 ) ) )
18 divcan3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 0 ∈ ℂ ∧ 1 0 ≠ 0 ) → ( ( 1 0 · 𝐴 ) / 1 0 ) = 𝐴 )
19 8 13 18 mp3an23 ⊢ ( 𝐴 ∈ ℂ → ( ( 1 0 · 𝐴 ) / 1 0 ) = 𝐴 )
20 19 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( ( 1 0 · 𝐴 ) / 1 0 ) + ( 𝐵 / 1 0 ) ) = ( 𝐴 + ( 𝐵 / 1 0 ) ) )
21 20 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 1 0 · 𝐴 ) / 1 0 ) + ( 𝐵 / 1 0 ) ) = ( 𝐴 + ( 𝐵 / 1 0 ) ) )
22 17 21 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 1 0 · 𝐴 ) + 𝐵 ) / 1 0 ) = ( 𝐴 + ( 𝐵 / 1 0 ) ) )
23 6 22 eqtrid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 𝐵 / 1 0 ) = ( 𝐴 + ( 𝐵 / 1 0 ) ) )
24 3 4 23 syl2an ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 𝐵 / 1 0 ) = ( 𝐴 + ( 𝐵 / 1 0 ) ) )
25 1 2 24 3eqtr4a ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 . 𝐵 ) = ( 𝐴 𝐵 / 1 0 ) )