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\in {\mathbb{N}}_0$$
	dpexpp1.b	$$⊢B\in {ℝ}^{+}$$
	dpexpp1.1	$$⊢P+1=Q$$
	dpexpp1.p	$$⊢P\in \mathbb{Z}$$
	dpexpp1.q	$$⊢Q\in \mathbb{Z}$$
Assertion	dpexpp1	Could not format assertion : No typesetting found for |- ( ( A . B ) x. ( ; 1 0 ^ P ) ) = ( ( 0 . _ A B ) x. ( ; 1 0 ^ Q ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dpexpp1.a	$$⊢A\in {\mathbb{N}}_0$$
2		dpexpp1.b	$$⊢B\in {ℝ}^{+}$$
3		dpexpp1.1	$$⊢P+1=Q$$
4		dpexpp1.p	$$⊢P\in \mathbb{Z}$$
5		dpexpp1.q	$$⊢Q\in \mathbb{Z}$$
6		0re	$$⊢0\in ℝ$$
7		10pos	$$⊢0<10$$
8	6 7	gtneii	$$⊢10\ne 0$$
9	1 2	rpdp2cl	Could not format _ A B e. RR+ : No typesetting found for |- _ A B e. RR+ with typecode |-
10		rpre	Could not format ( _ A B e. RR+ -> _ A B e. RR ) : No typesetting found for |- ( _ A B e. RR+ -> _ A B e. RR ) with typecode |-
11	9 10	ax-mp	Could not format _ A B e. RR : No typesetting found for |- _ A B e. RR with typecode |-
12	11	recni	Could not format _ A B e. CC : No typesetting found for |- _ A B e. CC with typecode |-
13		10re	$$⊢10\in ℝ$$
14	13 7	pm3.2i	$$⊢\left(10\in ℝ\wedge 0<10\right)$$
15		elrp	$$⊢10\in {ℝ}^{+}\leftrightarrow \left(10\in ℝ\wedge 0<10\right)$$
16	14 15	mpbir	$$⊢10\in {ℝ}^{+}$$
17		rpexpcl	$$⊢\left(10\in {ℝ}^{+}\wedge P\in \mathbb{Z}\right)\to {10}^P\in {ℝ}^{+}$$
18	16 4 17	mp2an	$$⊢{10}^P\in {ℝ}^{+}$$
19		rpcn	$$⊢{10}^P\in {ℝ}^{+}\to {10}^P\in ℂ$$
20	18 19	ax-mp	$$⊢{10}^P\in ℂ$$
21	12 20	mulcli	Could not format ( _ A B x. ( ; 1 0 ^ P ) ) e. CC : No typesetting found for |- ( _ A B x. ( ; 1 0 ^ P ) ) e. CC with typecode |-
22		10nn0	$$⊢10\in {\mathbb{N}}_0$$
23	22	nn0cni	$$⊢10\in ℂ$$
24	21 23	divcan1zi	Could not format ( ; 1 0 =/= 0 -> ( ( ( _ A B x. ( ; 1 0 ^ P ) ) / ; 1 0 ) x. ; 1 0 ) = ( _ A B x. ( ; 1 0 ^ P ) ) ) : No typesetting found for |- ( ; 1 0 =/= 0 -> ( ( ( _ A B x. ( ; 1 0 ^ P ) ) / ; 1 0 ) x. ; 1 0 ) = ( _ A B x. ( ; 1 0 ^ P ) ) ) with typecode |-
25	8 24	ax-mp	Could not format ( ( ( _ A B x. ( ; 1 0 ^ P ) ) / ; 1 0 ) x. ; 1 0 ) = ( _ A B x. ( ; 1 0 ^ P ) ) : No typesetting found for |- ( ( ( _ A B x. ( ; 1 0 ^ P ) ) / ; 1 0 ) x. ; 1 0 ) = ( _ A B x. ( ; 1 0 ^ P ) ) with typecode |-
26	23 8	pm3.2i	$$⊢\left(10\in ℂ\wedge 10\ne 0\right)$$
27		div23	Could not format ( ( _ 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 ) ) ) : No typesetting found for |- ( ( _ 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 ) ) ) with typecode |-
28	12 20 26 27	mp3an	Could not format ( ( _ A B x. ( ; 1 0 ^ P ) ) / ; 1 0 ) = ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ P ) ) : No typesetting found for |- ( ( _ A B x. ( ; 1 0 ^ P ) ) / ; 1 0 ) = ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ P ) ) with typecode |-
29	28	oveq1i	Could not format ( ( ( _ A B x. ( ; 1 0 ^ P ) ) / ; 1 0 ) x. ; 1 0 ) = ( ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ P ) ) x. ; 1 0 ) : No typesetting found for |- ( ( ( _ A B x. ( ; 1 0 ^ P ) ) / ; 1 0 ) x. ; 1 0 ) = ( ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ P ) ) x. ; 1 0 ) with typecode |-
30	25 29	eqtr3i	Could not format ( _ A B x. ( ; 1 0 ^ P ) ) = ( ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ P ) ) x. ; 1 0 ) : No typesetting found for |- ( _ A B x. ( ; 1 0 ^ P ) ) = ( ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ P ) ) x. ; 1 0 ) with typecode |-
31	12 23 8	divcli	Could not format ( _ A B / ; 1 0 ) e. CC : No typesetting found for |- ( _ A B / ; 1 0 ) e. CC with typecode |-
32	31 20 23	mulassi	Could not format ( ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ P ) ) x. ; 1 0 ) = ( ( _ A B / ; 1 0 ) x. ( ( ; 1 0 ^ P ) x. ; 1 0 ) ) : No typesetting found for |- ( ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ P ) ) x. ; 1 0 ) = ( ( _ A B / ; 1 0 ) x. ( ( ; 1 0 ^ P ) x. ; 1 0 ) ) with typecode |-
33		expp1z	$$⊢\left(10\in ℂ\wedge 10\ne 0\wedge P\in \mathbb{Z}\right)\to {10}^{P+1}={10}^P\cdot 10$$
34	23 8 4 33	mp3an	$$⊢{10}^{P+1}={10}^P\cdot 10$$
35	3	oveq2i	$$⊢{10}^{P+1}={10}^Q$$
36	34 35	eqtr3i	$$⊢{10}^P\cdot 10={10}^Q$$
37	36	oveq2i	Could not format ( ( _ A B / ; 1 0 ) x. ( ( ; 1 0 ^ P ) x. ; 1 0 ) ) = ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ Q ) ) : No typesetting found for |- ( ( _ A B / ; 1 0 ) x. ( ( ; 1 0 ^ P ) x. ; 1 0 ) ) = ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ Q ) ) with typecode |-
38	30 32 37	3eqtri	Could not format ( _ A B x. ( ; 1 0 ^ P ) ) = ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ Q ) ) : No typesetting found for |- ( _ A B x. ( ; 1 0 ^ P ) ) = ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ Q ) ) with typecode |-
39	1 2	dpval3rp	Could not format ( A . B ) = _ A B : No typesetting found for |- ( A . B ) = _ A B with typecode |-
40	39	oveq1i	Could not format ( ( A . B ) x. ( ; 1 0 ^ P ) ) = ( _ A B x. ( ; 1 0 ^ P ) ) : No typesetting found for |- ( ( A . B ) x. ( ; 1 0 ^ P ) ) = ( _ A B x. ( ; 1 0 ^ P ) ) with typecode |-
41		0nn0	$$⊢0\in {\mathbb{N}}_0$$
42	41 9	dpval3rp	Could not format ( 0 . _ A B ) = _ 0 _ A B : No typesetting found for |- ( 0 . _ A B ) = _ 0 _ A B with typecode |-
43	9	dp20h	Could not format _ 0 _ A B = ( _ A B / ; 1 0 ) : No typesetting found for |- _ 0 _ A B = ( _ A B / ; 1 0 ) with typecode |-
44	42 43	eqtri	Could not format ( 0 . _ A B ) = ( _ A B / ; 1 0 ) : No typesetting found for |- ( 0 . _ A B ) = ( _ A B / ; 1 0 ) with typecode |-
45	44	oveq1i	Could not format ( ( 0 . _ A B ) x. ( ; 1 0 ^ Q ) ) = ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ Q ) ) : No typesetting found for |- ( ( 0 . _ A B ) x. ( ; 1 0 ^ Q ) ) = ( ( _ A B / ; 1 0 ) x. ( ; 1 0 ^ Q ) ) with typecode |-
46	38 40 45	3eqtr4i	Could not format ( ( A . B ) x. ( ; 1 0 ^ P ) ) = ( ( 0 . _ A B ) x. ( ; 1 0 ^ Q ) ) : No typesetting found for |- ( ( A . B ) x. ( ; 1 0 ^ P ) ) = ( ( 0 . _ A B ) x. ( ; 1 0 ^ Q ) ) with typecode |-