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 ↑ 𝑄 ) )