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 
|- A e. NN0
dpexpp1.b 
|- B e. RR+
dpexpp1.1 
|- ( P + 1 ) = Q
dpexpp1.p 
|- P e. ZZ
dpexpp1.q 
|- Q e. ZZ
Assertion dpexpp1 
|- ( ( A . B ) x. ( ; 1 0 ^ P ) ) = ( ( 0 . _ A B ) x. ( ; 1 0 ^ Q ) )

Proof

Step Hyp Ref Expression
1 dpexpp1.a 
 |-  A e. NN0
2 dpexpp1.b 
 |-  B e. RR+
3 dpexpp1.1 
 |-  ( P + 1 ) = Q
4 dpexpp1.p 
 |-  P e. ZZ
5 dpexpp1.q 
 |-  Q e. ZZ
6 0re 
 |-  0 e. RR
7 10pos 
 |-  0 < ; 1 0
8 6 7 gtneii 
 |-  ; 1 0 =/= 0
9 1 2 rpdp2cl 
 |-  _ A B e. RR+
10 rpre 
 |-  ( _ A B e. RR+ -> _ A B e. RR )
11 9 10 ax-mp 
 |-  _ A B e. RR
12 11 recni 
 |-  _ A B e. CC
13 10re 
 |-  ; 1 0 e. RR
14 13 7 pm3.2i 
 |-  ( ; 1 0 e. RR /\ 0 < ; 1 0 )
15 elrp 
 |-  ( ; 1 0 e. RR+ <-> ( ; 1 0 e. RR /\ 0 < ; 1 0 ) )
16 14 15 mpbir 
 |-  ; 1 0 e. RR+
17 rpexpcl 
 |-  ( ( ; 1 0 e. RR+ /\ P e. ZZ ) -> ( ; 1 0 ^ P ) e. RR+ )
18 16 4 17 mp2an 
 |-  ( ; 1 0 ^ P ) e. RR+
19 rpcn 
 |-  ( ( ; 1 0 ^ P ) e. RR+ -> ( ; 1 0 ^ P ) e. CC )
20 18 19 ax-mp 
 |-  ( ; 1 0 ^ P ) e. CC
21 12 20 mulcli 
 |-  ( _ A B x. ( ; 1 0 ^ P ) ) e. CC
22 10nn0 
 |-  ; 1 0 e. NN0
23 22 nn0cni 
 |-  ; 1 0 e. CC
24 21 23 divcan1zi 
 |-  ( ; 1 0 =/= 0 -> ( ( ( _ A B x. ( ; 1 0 ^ P ) ) / ; 1 0 ) x. ; 1 0 ) = ( _ A B x. ( ; 1 0 ^ P ) ) )
25 8 24 ax-mp 
 |-  ( ( ( _ A B x. ( ; 1 0 ^ P ) ) / ; 1 0 ) x. ; 1 0 ) = ( _ A B x. ( ; 1 0 ^ P ) )
26 23 8 pm3.2i 
 |-  ( ; 1 0 e. CC /\ ; 1 0 =/= 0 )
27 div23 
 |-  ( ( _ A B e. CC /\ ( ; 1 0 ^ P ) e. CC /\ ( ; 1 0 e. CC /\ ; 1 0 =/= 0 ) ) -> ( ( _ A B x. ( ; 1 0 ^ P ) ) / ; 1 0 ) = ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ P ) ) )
28 12 20 26 27 mp3an 
 |-  ( ( _ A B x. ( ; 1 0 ^ P ) ) / ; 1 0 ) = ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ P ) )
29 28 oveq1i 
 |-  ( ( ( _ A B x. ( ; 1 0 ^ P ) ) / ; 1 0 ) x. ; 1 0 ) = ( ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ P ) ) x. ; 1 0 )
30 25 29 eqtr3i 
 |-  ( _ A B x. ( ; 1 0 ^ P ) ) = ( ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ P ) ) x. ; 1 0 )
31 12 23 8 divcli 
 |-  ( _ A B / ; 1 0 ) e. CC
32 31 20 23 mulassi 
 |-  ( ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ P ) ) x. ; 1 0 ) = ( ( _ A B / ; 1 0 ) x. ( ( ; 1 0 ^ P ) x. ; 1 0 ) )
33 expp1z 
 |-  ( ( ; 1 0 e. CC /\ ; 1 0 =/= 0 /\ P e. ZZ ) -> ( ; 1 0 ^ ( P + 1 ) ) = ( ( ; 1 0 ^ P ) x. ; 1 0 ) )
34 23 8 4 33 mp3an 
 |-  ( ; 1 0 ^ ( P + 1 ) ) = ( ( ; 1 0 ^ P ) x. ; 1 0 )
35 3 oveq2i 
 |-  ( ; 1 0 ^ ( P + 1 ) ) = ( ; 1 0 ^ Q )
36 34 35 eqtr3i 
 |-  ( ( ; 1 0 ^ P ) x. ; 1 0 ) = ( ; 1 0 ^ Q )
37 36 oveq2i 
 |-  ( ( _ A B / ; 1 0 ) x. ( ( ; 1 0 ^ P ) x. ; 1 0 ) ) = ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ Q ) )
38 30 32 37 3eqtri 
 |-  ( _ A B x. ( ; 1 0 ^ P ) ) = ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ Q ) )
39 1 2 dpval3rp 
 |-  ( A . B ) = _ A B
40 39 oveq1i 
 |-  ( ( A . B ) x. ( ; 1 0 ^ P ) ) = ( _ A B x. ( ; 1 0 ^ P ) )
41 0nn0 
 |-  0 e. NN0
42 41 9 dpval3rp 
 |-  ( 0 . _ A B ) = _ 0 _ A B
43 9 dp20h 
 |-  _ 0 _ A B = ( _ A B / ; 1 0 )
44 42 43 eqtri 
 |-  ( 0 . _ A B ) = ( _ A B / ; 1 0 )
45 44 oveq1i 
 |-  ( ( 0 . _ A B ) x. ( ; 1 0 ^ Q ) ) = ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ Q ) )
46 38 40 45 3eqtr4i 
 |-  ( ( A . B ) x. ( ; 1 0 ^ P ) ) = ( ( 0 . _ A B ) x. ( ; 1 0 ^ Q ) )