Theorem dpadd3

Description: Addition with two decimals. (Contributed by Thierry Arnoux, 27-Dec-2021)

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

Proof

Step	Hyp	Ref	Expression
1		dpmul.a	⊢ 𝐴 ∈ ℕ0
2		dpmul.b	⊢ 𝐵 ∈ ℕ0
3		dpmul.c	⊢ 𝐶 ∈ ℕ0
4		dpmul.d	⊢ 𝐷 ∈ ℕ0
5		dpmul.e	⊢ 𝐸 ∈ ℕ0
6		dpmul.g	⊢ 𝐺 ∈ ℕ0
7		dpadd3.f	⊢ 𝐹 ∈ ℕ0
8		dpadd3.h	⊢ 𝐻 ∈ ℕ0
9		dpadd3.i	⊢ 𝐼 ∈ ℕ0
10		dpadd3.1	⊢ ( ; ; 𝐴 𝐵 𝐶 + ; ; 𝐷 𝐸 𝐹 ) = ; ; 𝐺 𝐻 𝐼
11	2	nn0rei	⊢ 𝐵 ∈ ℝ
12	3	nn0rei	⊢ 𝐶 ∈ ℝ
13		dp2cl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → _ 𝐵 𝐶 ∈ ℝ )
14	11 12 13	mp2an	⊢ _ 𝐵 𝐶 ∈ ℝ
15		dpcl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ _ 𝐵 𝐶 ∈ ℝ ) → ( 𝐴 . _ 𝐵 𝐶 ) ∈ ℝ )
16	1 14 15	mp2an	⊢ ( 𝐴 . _ 𝐵 𝐶 ) ∈ ℝ
17	16	recni	⊢ ( 𝐴 . _ 𝐵 𝐶 ) ∈ ℂ
18	5	nn0rei	⊢ 𝐸 ∈ ℝ
19	7	nn0rei	⊢ 𝐹 ∈ ℝ
20		dp2cl	⊢ ( ( 𝐸 ∈ ℝ ∧ 𝐹 ∈ ℝ ) → _ 𝐸 𝐹 ∈ ℝ )
21	18 19 20	mp2an	⊢ _ 𝐸 𝐹 ∈ ℝ
22		dpcl	⊢ ( ( 𝐷 ∈ ℕ0 ∧ _ 𝐸 𝐹 ∈ ℝ ) → ( 𝐷 . _ 𝐸 𝐹 ) ∈ ℝ )
23	4 21 22	mp2an	⊢ ( 𝐷 . _ 𝐸 𝐹 ) ∈ ℝ
24	23	recni	⊢ ( 𝐷 . _ 𝐸 𝐹 ) ∈ ℂ
25	17 24	addcli	⊢ ( ( 𝐴 . _ 𝐵 𝐶 ) + ( 𝐷 . _ 𝐸 𝐹 ) ) ∈ ℂ
26	8	nn0rei	⊢ 𝐻 ∈ ℝ
27	9	nn0rei	⊢ 𝐼 ∈ ℝ
28		dp2cl	⊢ ( ( 𝐻 ∈ ℝ ∧ 𝐼 ∈ ℝ ) → _ 𝐻 𝐼 ∈ ℝ )
29	26 27 28	mp2an	⊢ _ 𝐻 𝐼 ∈ ℝ
30		dpcl	⊢ ( ( 𝐺 ∈ ℕ0 ∧ _ 𝐻 𝐼 ∈ ℝ ) → ( 𝐺 . _ 𝐻 𝐼 ) ∈ ℝ )
31	6 29 30	mp2an	⊢ ( 𝐺 . _ 𝐻 𝐼 ) ∈ ℝ
32	31	recni	⊢ ( 𝐺 . _ 𝐻 𝐼 ) ∈ ℂ
33		10nn	⊢ ; 1 0 ∈ ℕ
34	33	decnncl2	⊢ ; ; 1 0 0 ∈ ℕ
35	34	nncni	⊢ ; ; 1 0 0 ∈ ℂ
36	34	nnne0i	⊢ ; ; 1 0 0 ≠ 0
37	35 36	pm3.2i	⊢ ( ; ; 1 0 0 ∈ ℂ ∧ ; ; 1 0 0 ≠ 0 )
38	25 32 37	3pm3.2i	⊢ ( ( ( 𝐴 . _ 𝐵 𝐶 ) + ( 𝐷 . _ 𝐸 𝐹 ) ) ∈ ℂ ∧ ( 𝐺 . _ 𝐻 𝐼 ) ∈ ℂ ∧ ( ; ; 1 0 0 ∈ ℂ ∧ ; ; 1 0 0 ≠ 0 ) )
39	17 24 35	adddiri	⊢ ( ( ( 𝐴 . _ 𝐵 𝐶 ) + ( 𝐷 . _ 𝐸 𝐹 ) ) · ; ; 1 0 0 ) = ( ( ( 𝐴 . _ 𝐵 𝐶 ) · ; ; 1 0 0 ) + ( ( 𝐷 . _ 𝐸 𝐹 ) · ; ; 1 0 0 ) )
40	1 2 12	dpmul100	⊢ ( ( 𝐴 . _ 𝐵 𝐶 ) · ; ; 1 0 0 ) = ; ; 𝐴 𝐵 𝐶
41	4 5 19	dpmul100	⊢ ( ( 𝐷 . _ 𝐸 𝐹 ) · ; ; 1 0 0 ) = ; ; 𝐷 𝐸 𝐹
42	40 41	oveq12i	⊢ ( ( ( 𝐴 . _ 𝐵 𝐶 ) · ; ; 1 0 0 ) + ( ( 𝐷 . _ 𝐸 𝐹 ) · ; ; 1 0 0 ) ) = ( ; ; 𝐴 𝐵 𝐶 + ; ; 𝐷 𝐸 𝐹 )
43	6 8 27	dpmul100	⊢ ( ( 𝐺 . _ 𝐻 𝐼 ) · ; ; 1 0 0 ) = ; ; 𝐺 𝐻 𝐼
44	10 42 43	3eqtr4i	⊢ ( ( ( 𝐴 . _ 𝐵 𝐶 ) · ; ; 1 0 0 ) + ( ( 𝐷 . _ 𝐸 𝐹 ) · ; ; 1 0 0 ) ) = ( ( 𝐺 . _ 𝐻 𝐼 ) · ; ; 1 0 0 )
45	39 44	eqtri	⊢ ( ( ( 𝐴 . _ 𝐵 𝐶 ) + ( 𝐷 . _ 𝐸 𝐹 ) ) · ; ; 1 0 0 ) = ( ( 𝐺 . _ 𝐻 𝐼 ) · ; ; 1 0 0 )
46		mulcan2	⊢ ( ( ( ( 𝐴 . _ 𝐵 𝐶 ) + ( 𝐷 . _ 𝐸 𝐹 ) ) ∈ ℂ ∧ ( 𝐺 . _ 𝐻 𝐼 ) ∈ ℂ ∧ ( ; ; 1 0 0 ∈ ℂ ∧ ; ; 1 0 0 ≠ 0 ) ) → ( ( ( ( 𝐴 . _ 𝐵 𝐶 ) + ( 𝐷 . _ 𝐸 𝐹 ) ) · ; ; 1 0 0 ) = ( ( 𝐺 . _ 𝐻 𝐼 ) · ; ; 1 0 0 ) ↔ ( ( 𝐴 . _ 𝐵 𝐶 ) + ( 𝐷 . _ 𝐸 𝐹 ) ) = ( 𝐺 . _ 𝐻 𝐼 ) ) )
47	46	biimpa	⊢ ( ( ( ( ( 𝐴 . _ 𝐵 𝐶 ) + ( 𝐷 . _ 𝐸 𝐹 ) ) ∈ ℂ ∧ ( 𝐺 . _ 𝐻 𝐼 ) ∈ ℂ ∧ ( ; ; 1 0 0 ∈ ℂ ∧ ; ; 1 0 0 ≠ 0 ) ) ∧ ( ( ( 𝐴 . _ 𝐵 𝐶 ) + ( 𝐷 . _ 𝐸 𝐹 ) ) · ; ; 1 0 0 ) = ( ( 𝐺 . _ 𝐻 𝐼 ) · ; ; 1 0 0 ) ) → ( ( 𝐴 . _ 𝐵 𝐶 ) + ( 𝐷 . _ 𝐸 𝐹 ) ) = ( 𝐺 . _ 𝐻 𝐼 ) )
48	38 45 47	mp2an	⊢ ( ( 𝐴 . _ 𝐵 𝐶 ) + ( 𝐷 . _ 𝐸 𝐹 ) ) = ( 𝐺 . _ 𝐻 𝐼 )