Metamath Proof Explorer

Theorem dpexpp1

Description: Add one zero to the mantisse, and a one to the exponent in a scientific notation. (Contributed by Thierry Arnoux, 16-Dec-2021)

Ref Expression
Hypotheses dpexpp1.a ⊢ 𝐴 ∈ ℕ0
dpexpp1.b ⊢ 𝐵 ∈ ℝ+
dpexpp1.1 ⊢ ( 𝑃 + 1 ) = 𝑄
dpexpp1.p ⊢ 𝑃 ∈ ℤ
dpexpp1.q ⊢ 𝑄 ∈ ℤ
Assertion dpexpp1 ( ( 𝐴 . 𝐵 ) · ( 1 0 ↑ 𝑃 ) ) = ( ( 0 . 𝐴 𝐵 ) · ( 1 0 ↑ 𝑄 ) )

Proof

Step Hyp Ref Expression
1 dpexpp1.a ⊢ 𝐴 ∈ ℕ0
2 dpexpp1.b ⊢ 𝐵 ∈ ℝ+
3 dpexpp1.1 ⊢ ( 𝑃 + 1 ) = 𝑄
4 dpexpp1.p ⊢ 𝑃 ∈ ℤ
5 dpexpp1.q ⊢ 𝑄 ∈ ℤ
6 0re ⊢ 0 ∈ ℝ
7 10pos ⊢ 0 < 1 0
8 6 7 gtneii ⊢ 1 0 ≠ 0
9 1 2 rpdp2cl ⊢ 𝐴 𝐵 ∈ ℝ+
10 rpre ⊢ ( 𝐴 𝐵 ∈ ℝ+ → 𝐴 𝐵 ∈ ℝ )
11 9 10 ax-mp ⊢ 𝐴 𝐵 ∈ ℝ
12 11 recni ⊢ 𝐴 𝐵 ∈ ℂ
13 10re ⊢ 1 0 ∈ ℝ
14 13 7 pm3.2i ⊢ ( 1 0 ∈ ℝ ∧ 0 < 1 0 )
15 elrp ⊢ ( 1 0 ∈ ℝ+ ↔ ( 1 0 ∈ ℝ ∧ 0 < 1 0 ) )
16 14 15 mpbir ⊢ 1 0 ∈ ℝ+
17 rpexpcl ⊢ ( ( 1 0 ∈ ℝ+ ∧ 𝑃 ∈ ℤ ) → ( 1 0 ↑ 𝑃 ) ∈ ℝ+ )
18 16 4 17 mp2an ⊢ ( 1 0 ↑ 𝑃 ) ∈ ℝ+
19 rpcn ⊢ ( ( 1 0 ↑ 𝑃 ) ∈ ℝ+ → ( 1 0 ↑ 𝑃 ) ∈ ℂ )
20 18 19 ax-mp ⊢ ( 1 0 ↑ 𝑃 ) ∈ ℂ
21 12 20 mulcli ⊢ ( 𝐴 𝐵 · ( 1 0 ↑ 𝑃 ) ) ∈ ℂ
22 10nn0 ⊢ 1 0 ∈ ℕ0
23 22 nn0cni ⊢ 1 0 ∈ ℂ
24 21 23 divcan1zi ⊢ ( 1 0 ≠ 0 → ( ( ( 𝐴 𝐵 · ( 1 0 ↑ 𝑃 ) ) / 1 0 ) · 1 0 ) = ( 𝐴 𝐵 · ( 1 0 ↑ 𝑃 ) ) )
25 8 24 ax-mp ⊢ ( ( ( 𝐴 𝐵 · ( 1 0 ↑ 𝑃 ) ) / 1 0 ) · 1 0 ) = ( 𝐴 𝐵 · ( 1 0 ↑ 𝑃 ) )
26 23 8 pm3.2i ⊢ ( 1 0 ∈ ℂ ∧ 1 0 ≠ 0 )
27 div23 ⊢ ( ( 𝐴 𝐵 ∈ ℂ ∧ ( 1 0 ↑ 𝑃 ) ∈ ℂ ∧ ( 1 0 ∈ ℂ ∧ 1 0 ≠ 0 ) ) → ( ( 𝐴 𝐵 · ( 1 0 ↑ 𝑃 ) ) / 1 0 ) = ( ( 𝐴 𝐵 / 1 0 ) · ( 1 0 ↑ 𝑃 ) ) )
28 12 20 26 27 mp3an ⊢ ( ( 𝐴 𝐵 · ( 1 0 ↑ 𝑃 ) ) / 1 0 ) = ( ( 𝐴 𝐵 / 1 0 ) · ( 1 0 ↑ 𝑃 ) )
29 28 oveq1i ⊢ ( ( ( 𝐴 𝐵 · ( 1 0 ↑ 𝑃 ) ) / 1 0 ) · 1 0 ) = ( ( ( 𝐴 𝐵 / 1 0 ) · ( 1 0 ↑ 𝑃 ) ) · 1 0 )
30 25 29 eqtr3i ⊢ ( 𝐴 𝐵 · ( 1 0 ↑ 𝑃 ) ) = ( ( ( 𝐴 𝐵 / 1 0 ) · ( 1 0 ↑ 𝑃 ) ) · 1 0 )
31 12 23 8 divcli ⊢ ( 𝐴 𝐵 / 1 0 ) ∈ ℂ
32 31 20 23 mulassi ⊢ ( ( ( 𝐴 𝐵 / 1 0 ) · ( 1 0 ↑ 𝑃 ) ) · 1 0 ) = ( ( 𝐴 𝐵 / 1 0 ) · ( ( 1 0 ↑ 𝑃 ) · 1 0 ) )
33 expp1z ⊢ ( ( 1 0 ∈ ℂ ∧ 1 0 ≠ 0 ∧ 𝑃 ∈ ℤ ) → ( 1 0 ↑ ( 𝑃 + 1 ) ) = ( ( 1 0 ↑ 𝑃 ) · 1 0 ) )
34 23 8 4 33 mp3an ⊢ ( 1 0 ↑ ( 𝑃 + 1 ) ) = ( ( 1 0 ↑ 𝑃 ) · 1 0 )
35 3 oveq2i ⊢ ( 1 0 ↑ ( 𝑃 + 1 ) ) = ( 1 0 ↑ 𝑄 )
36 34 35 eqtr3i ⊢ ( ( 1 0 ↑ 𝑃 ) · 1 0 ) = ( 1 0 ↑ 𝑄 )
37 36 oveq2i ⊢ ( ( 𝐴 𝐵 / 1 0 ) · ( ( 1 0 ↑ 𝑃 ) · 1 0 ) ) = ( ( 𝐴 𝐵 / 1 0 ) · ( 1 0 ↑ 𝑄 ) )
38 30 32 37 3eqtri ⊢ ( 𝐴 𝐵 · ( 1 0 ↑ 𝑃 ) ) = ( ( 𝐴 𝐵 / 1 0 ) · ( 1 0 ↑ 𝑄 ) )
39 1 2 dpval3rp ⊢ ( 𝐴 . 𝐵 ) = 𝐴 𝐵
40 39 oveq1i ⊢ ( ( 𝐴 . 𝐵 ) · ( 1 0 ↑ 𝑃 ) ) = ( 𝐴 𝐵 · ( 1 0 ↑ 𝑃 ) )
41 0nn0 ⊢ 0 ∈ ℕ0
42 41 9 dpval3rp ⊢ ( 0 . 𝐴 𝐵 ) = 0 𝐴 𝐵
43 9 dp20h ⊢ 0 𝐴 𝐵 = ( 𝐴 𝐵 / 1 0 )
44 42 43 eqtri ⊢ ( 0 . 𝐴 𝐵 ) = ( 𝐴 𝐵 / 1 0 )
45 44 oveq1i ⊢ ( ( 0 . 𝐴 𝐵 ) · ( 1 0 ↑ 𝑄 ) ) = ( ( 𝐴 𝐵 / 1 0 ) · ( 1 0 ↑ 𝑄 ) )
46 38 40 45 3eqtr4i ⊢ ( ( 𝐴 . 𝐵 ) · ( 1 0 ↑ 𝑃 ) ) = ( ( 0 . 𝐴 𝐵 ) · ( 1 0 ↑ 𝑄 ) )