Theorem dp2clq

Description: Closure for a decimal fraction. (Contributed by Thierry Arnoux, 16-Dec-2021)

	Ref	Expression
Hypotheses	dp2clq.a	⊢ 𝐴 ∈ ℕ0
	dp2clq.b	⊢ 𝐵 ∈ ℚ
Assertion	dp2clq	⊢ _ 𝐴 𝐵 ∈ ℚ

Proof

Step	Hyp	Ref	Expression
1		dp2clq.a	⊢ 𝐴 ∈ ℕ0
2		dp2clq.b	⊢ 𝐵 ∈ ℚ
3		df-dp2	⊢ _ 𝐴 𝐵 = ( 𝐴 + ( 𝐵 / ; 1 0 ) )
4		nn0ssq	⊢ ℕ0 ⊆ ℚ
5	4 1	sselii	⊢ 𝐴 ∈ ℚ
6		10nn0	⊢ ; 1 0 ∈ ℕ0
7	4 6	sselii	⊢ ; 1 0 ∈ ℚ
8		0re	⊢ 0 ∈ ℝ
9		10pos	⊢ 0 < ; 1 0
10	8 9	gtneii	⊢ ; 1 0 ≠ 0
11		qdivcl	⊢ ( ( 𝐵 ∈ ℚ ∧ ; 1 0 ∈ ℚ ∧ ; 1 0 ≠ 0 ) → ( 𝐵 / ; 1 0 ) ∈ ℚ )
12	2 7 10 11	mp3an	⊢ ( 𝐵 / ; 1 0 ) ∈ ℚ
13		qaddcl	⊢ ( ( 𝐴 ∈ ℚ ∧ ( 𝐵 / ; 1 0 ) ∈ ℚ ) → ( 𝐴 + ( 𝐵 / ; 1 0 ) ) ∈ ℚ )
14	5 12 13	mp2an	⊢ ( 𝐴 + ( 𝐵 / ; 1 0 ) ) ∈ ℚ
15	3 14	eqeltri	⊢ _ 𝐴 𝐵 ∈ ℚ