Theorem dpadd2

Description: Addition with one decimal, no carry. (Contributed by Thierry Arnoux, 29-Dec-2021)

	Ref	Expression
Hypotheses	dpadd2.a	⊢ 𝐴 ∈ ℕ0
	dpadd2.b	⊢ 𝐵 ∈ ℝ+
	dpadd2.c	⊢ 𝐶 ∈ ℕ0
	dpadd2.d	⊢ 𝐷 ∈ ℝ+
	dpadd2.e	⊢ 𝐸 ∈ ℕ0
	dpadd2.f	⊢ 𝐹 ∈ ℝ+
	dpadd2.g	⊢ 𝐺 ∈ ℕ0
	dpadd2.h	⊢ 𝐻 ∈ ℕ0
	dpadd2.i	⊢ ( 𝐺 + 𝐻 ) = 𝐼
	dpadd2.1	⊢ ( ( 𝐴 . 𝐵 ) + ( 𝐶 . 𝐷 ) ) = ( 𝐸 . 𝐹 )
Assertion	dpadd2	⊢ ( ( 𝐺 . _ 𝐴 𝐵 ) + ( 𝐻 . _ 𝐶 𝐷 ) ) = ( 𝐼 . _ 𝐸 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		dpadd2.a	⊢ 𝐴 ∈ ℕ0
2		dpadd2.b	⊢ 𝐵 ∈ ℝ+
3		dpadd2.c	⊢ 𝐶 ∈ ℕ0
4		dpadd2.d	⊢ 𝐷 ∈ ℝ+
5		dpadd2.e	⊢ 𝐸 ∈ ℕ0
6		dpadd2.f	⊢ 𝐹 ∈ ℝ+
7		dpadd2.g	⊢ 𝐺 ∈ ℕ0
8		dpadd2.h	⊢ 𝐻 ∈ ℕ0
9		dpadd2.i	⊢ ( 𝐺 + 𝐻 ) = 𝐼
10		dpadd2.1	⊢ ( ( 𝐴 . 𝐵 ) + ( 𝐶 . 𝐷 ) ) = ( 𝐸 . 𝐹 )
11	1	nn0rei	⊢ 𝐴 ∈ ℝ
12		rpre	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ )
13	2 12	ax-mp	⊢ 𝐵 ∈ ℝ
14		dp2cl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → _ 𝐴 𝐵 ∈ ℝ )
15	11 13 14	mp2an	⊢ _ 𝐴 𝐵 ∈ ℝ
16	7 15	dpval2	⊢ ( 𝐺 . _ 𝐴 𝐵 ) = ( 𝐺 + ( _ 𝐴 𝐵 / ; 1 0 ) )
17	3	nn0rei	⊢ 𝐶 ∈ ℝ
18		rpre	⊢ ( 𝐷 ∈ ℝ+ → 𝐷 ∈ ℝ )
19	4 18	ax-mp	⊢ 𝐷 ∈ ℝ
20		dp2cl	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → _ 𝐶 𝐷 ∈ ℝ )
21	17 19 20	mp2an	⊢ _ 𝐶 𝐷 ∈ ℝ
22	8 21	dpval2	⊢ ( 𝐻 . _ 𝐶 𝐷 ) = ( 𝐻 + ( _ 𝐶 𝐷 / ; 1 0 ) )
23	16 22	oveq12i	⊢ ( ( 𝐺 . _ 𝐴 𝐵 ) + ( 𝐻 . _ 𝐶 𝐷 ) ) = ( ( 𝐺 + ( _ 𝐴 𝐵 / ; 1 0 ) ) + ( 𝐻 + ( _ 𝐶 𝐷 / ; 1 0 ) ) )
24	7	nn0cni	⊢ 𝐺 ∈ ℂ
25	15	recni	⊢ _ 𝐴 𝐵 ∈ ℂ
26		10nn	⊢ ; 1 0 ∈ ℕ
27	26	nncni	⊢ ; 1 0 ∈ ℂ
28	26	nnne0i	⊢ ; 1 0 ≠ 0
29	25 27 28	divcli	⊢ ( _ 𝐴 𝐵 / ; 1 0 ) ∈ ℂ
30	8	nn0cni	⊢ 𝐻 ∈ ℂ
31	21	recni	⊢ _ 𝐶 𝐷 ∈ ℂ
32	31 27 28	divcli	⊢ ( _ 𝐶 𝐷 / ; 1 0 ) ∈ ℂ
33	24 29 30 32	add4i	⊢ ( ( 𝐺 + ( _ 𝐴 𝐵 / ; 1 0 ) ) + ( 𝐻 + ( _ 𝐶 𝐷 / ; 1 0 ) ) ) = ( ( 𝐺 + 𝐻 ) + ( ( _ 𝐴 𝐵 / ; 1 0 ) + ( _ 𝐶 𝐷 / ; 1 0 ) ) )
34	25 31 27 28	divdiri	⊢ ( ( _ 𝐴 𝐵 + _ 𝐶 𝐷 ) / ; 1 0 ) = ( ( _ 𝐴 𝐵 / ; 1 0 ) + ( _ 𝐶 𝐷 / ; 1 0 ) )
35		dpval	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 . 𝐵 ) = _ 𝐴 𝐵 )
36	1 13 35	mp2an	⊢ ( 𝐴 . 𝐵 ) = _ 𝐴 𝐵
37		dpval	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℝ ) → ( 𝐶 . 𝐷 ) = _ 𝐶 𝐷 )
38	3 19 37	mp2an	⊢ ( 𝐶 . 𝐷 ) = _ 𝐶 𝐷
39	36 38	oveq12i	⊢ ( ( 𝐴 . 𝐵 ) + ( 𝐶 . 𝐷 ) ) = ( _ 𝐴 𝐵 + _ 𝐶 𝐷 )
40		rpre	⊢ ( 𝐹 ∈ ℝ+ → 𝐹 ∈ ℝ )
41	6 40	ax-mp	⊢ 𝐹 ∈ ℝ
42		dpval	⊢ ( ( 𝐸 ∈ ℕ0 ∧ 𝐹 ∈ ℝ ) → ( 𝐸 . 𝐹 ) = _ 𝐸 𝐹 )
43	5 41 42	mp2an	⊢ ( 𝐸 . 𝐹 ) = _ 𝐸 𝐹
44	10 39 43	3eqtr3i	⊢ ( _ 𝐴 𝐵 + _ 𝐶 𝐷 ) = _ 𝐸 𝐹
45	44	oveq1i	⊢ ( ( _ 𝐴 𝐵 + _ 𝐶 𝐷 ) / ; 1 0 ) = ( _ 𝐸 𝐹 / ; 1 0 )
46	34 45	eqtr3i	⊢ ( ( _ 𝐴 𝐵 / ; 1 0 ) + ( _ 𝐶 𝐷 / ; 1 0 ) ) = ( _ 𝐸 𝐹 / ; 1 0 )
47	9 46	oveq12i	⊢ ( ( 𝐺 + 𝐻 ) + ( ( _ 𝐴 𝐵 / ; 1 0 ) + ( _ 𝐶 𝐷 / ; 1 0 ) ) ) = ( 𝐼 + ( _ 𝐸 𝐹 / ; 1 0 ) )
48	7 8	nn0addcli	⊢ ( 𝐺 + 𝐻 ) ∈ ℕ0
49	9 48	eqeltrri	⊢ 𝐼 ∈ ℕ0
50	5	nn0rei	⊢ 𝐸 ∈ ℝ
51		dp2cl	⊢ ( ( 𝐸 ∈ ℝ ∧ 𝐹 ∈ ℝ ) → _ 𝐸 𝐹 ∈ ℝ )
52	50 41 51	mp2an	⊢ _ 𝐸 𝐹 ∈ ℝ
53	49 52	dpval2	⊢ ( 𝐼 . _ 𝐸 𝐹 ) = ( 𝐼 + ( _ 𝐸 𝐹 / ; 1 0 ) )
54	47 53	eqtr4i	⊢ ( ( 𝐺 + 𝐻 ) + ( ( _ 𝐴 𝐵 / ; 1 0 ) + ( _ 𝐶 𝐷 / ; 1 0 ) ) ) = ( 𝐼 . _ 𝐸 𝐹 )
55	23 33 54	3eqtri	⊢ ( ( 𝐺 . _ 𝐴 𝐵 ) + ( 𝐻 . _ 𝐶 𝐷 ) ) = ( 𝐼 . _ 𝐸 𝐹 )