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 ℕ_{0}$
	dpexpp1.b	$⊢ B \in ℝ^{+}$
	dpexpp1.1	$⊢ P + 1 = Q$
	dpexpp1.p	$⊢ P \in ℤ$
	dpexpp1.q	$⊢ Q \in ℤ$
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 ℕ_{0}$
2		dpexpp1.b	$⊢ B \in ℝ^{+}$
3		dpexpp1.1	$⊢ P + 1 = Q$
4		dpexpp1.p	$⊢ P \in ℤ$
5		dpexpp1.q	$⊢ Q \in ℤ$
6		0re	$⊢ 0 \in ℝ$
7		10pos	$⊢ 0 < 10$
8	6 7	gtneii	$⊢ 10 \neq 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	$⊢ (10 \in ℝ \land 0 < 10)$
15		elrp	$⊢ 10 \in ℝ^{+} \leftrightarrow (10 \in ℝ \land 0 < 10)$
16	14 15	mpbir	$⊢ 10 \in ℝ^{+}$
17		rpexpcl	$⊢ (10 \in ℝ^{+} \land P \in ℤ) \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 ℕ_{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	$⊢ (10 \in ℂ \land 10 \neq 0)$
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	$⊢ (10 \in ℂ \land 10 \neq 0 \land P \in ℤ) \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 ℕ_{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 \|-

Metamath Proof Explorer

Theorem dpexpp1

Proof