Theorem dpadd3

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

	Ref	Expression
Hypotheses	dpmul.a	$$⊢A\in {\mathbb{N}}_0$$
	dpmul.b	$$⊢B\in {\mathbb{N}}_0$$
	dpmul.c	$$⊢C\in {\mathbb{N}}_0$$
	dpmul.d	$$⊢D\in {\mathbb{N}}_0$$
	dpmul.e	$$⊢E\in {\mathbb{N}}_0$$
	dpmul.g	$$⊢G\in {\mathbb{N}}_0$$
	dpadd3.f	$$⊢F\in {\mathbb{N}}_0$$
	dpadd3.h	$$⊢H\in {\mathbb{N}}_0$$
	dpadd3.i	$$⊢I\in {\mathbb{N}}_0$$
	dpadd3.1	No typesetting found for |- ( ; ; A B C + ; ; D E F ) = ; ; G H I with typecode |-
Assertion	dpadd3	Could not format assertion : No typesetting found for |- ( ( A . _ B C ) + ( D . _ E F ) ) = ( G . _ H I ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dpmul.a	$$⊢A\in {\mathbb{N}}_0$$
2		dpmul.b	$$⊢B\in {\mathbb{N}}_0$$
3		dpmul.c	$$⊢C\in {\mathbb{N}}_0$$
4		dpmul.d	$$⊢D\in {\mathbb{N}}_0$$
5		dpmul.e	$$⊢E\in {\mathbb{N}}_0$$
6		dpmul.g	$$⊢G\in {\mathbb{N}}_0$$
7		dpadd3.f	$$⊢F\in {\mathbb{N}}_0$$
8		dpadd3.h	$$⊢H\in {\mathbb{N}}_0$$
9		dpadd3.i	$$⊢I\in {\mathbb{N}}_0$$
10		dpadd3.1	Could not format ( ; ; A B C + ; ; D E F ) = ; ; G H I : No typesetting found for |- ( ; ; A B C + ; ; D E F ) = ; ; G H I with typecode |-
11	2	nn0rei	$$⊢B\in ℝ$$
12	3	nn0rei	$$⊢C\in ℝ$$
13		dp2cl	Could not format ( ( B e. RR /\ C e. RR ) -> _ B C e. RR ) : No typesetting found for |- ( ( B e. RR /\ C e. RR ) -> _ B C e. RR ) with typecode |-
14	11 12 13	mp2an	Could not format _ B C e. RR : No typesetting found for |- _ B C e. RR with typecode |-
15		dpcl	Could not format ( ( A e. NN0 /\ _ B C e. RR ) -> ( A . _ B C ) e. RR ) : No typesetting found for |- ( ( A e. NN0 /\ _ B C e. RR ) -> ( A . _ B C ) e. RR ) with typecode |-
16	1 14 15	mp2an	Could not format ( A . _ B C ) e. RR : No typesetting found for |- ( A . _ B C ) e. RR with typecode |-
17	16	recni	Could not format ( A . _ B C ) e. CC : No typesetting found for |- ( A . _ B C ) e. CC with typecode |-
18	5	nn0rei	$$⊢E\in ℝ$$
19	7	nn0rei	$$⊢F\in ℝ$$
20		dp2cl	Could not format ( ( E e. RR /\ F e. RR ) -> _ E F e. RR ) : No typesetting found for |- ( ( E e. RR /\ F e. RR ) -> _ E F e. RR ) with typecode |-
21	18 19 20	mp2an	Could not format _ E F e. RR : No typesetting found for |- _ E F e. RR with typecode |-
22		dpcl	Could not format ( ( D e. NN0 /\ _ E F e. RR ) -> ( D . _ E F ) e. RR ) : No typesetting found for |- ( ( D e. NN0 /\ _ E F e. RR ) -> ( D . _ E F ) e. RR ) with typecode |-
23	4 21 22	mp2an	Could not format ( D . _ E F ) e. RR : No typesetting found for |- ( D . _ E F ) e. RR with typecode |-
24	23	recni	Could not format ( D . _ E F ) e. CC : No typesetting found for |- ( D . _ E F ) e. CC with typecode |-
25	17 24	addcli	Could not format ( ( A . _ B C ) + ( D . _ E F ) ) e. CC : No typesetting found for |- ( ( A . _ B C ) + ( D . _ E F ) ) e. CC with typecode |-
26	8	nn0rei	$$⊢H\in ℝ$$
27	9	nn0rei	$$⊢I\in ℝ$$
28		dp2cl	Could not format ( ( H e. RR /\ I e. RR ) -> _ H I e. RR ) : No typesetting found for |- ( ( H e. RR /\ I e. RR ) -> _ H I e. RR ) with typecode |-
29	26 27 28	mp2an	Could not format _ H I e. RR : No typesetting found for |- _ H I e. RR with typecode |-
30		dpcl	Could not format ( ( G e. NN0 /\ _ H I e. RR ) -> ( G . _ H I ) e. RR ) : No typesetting found for |- ( ( G e. NN0 /\ _ H I e. RR ) -> ( G . _ H I ) e. RR ) with typecode |-
31	6 29 30	mp2an	Could not format ( G . _ H I ) e. RR : No typesetting found for |- ( G . _ H I ) e. RR with typecode |-
32	31	recni	Could not format ( G . _ H I ) e. CC : No typesetting found for |- ( G . _ H I ) e. CC with typecode |-
33		10nn	$$⊢10\in \mathbb{N}$$
34	33	decnncl2	$$⊢100\in \mathbb{N}$$
35	34	nncni	$$⊢100\in ℂ$$
36	34	nnne0i	$$⊢100\ne 0$$
37	35 36	pm3.2i	$$⊢\left(100\in ℂ\wedge 100\ne 0\right)$$
38	25 32 37	3pm3.2i	Could not format ( ( ( A . _ B C ) + ( D . _ E F ) ) e. CC /\ ( G . _ H I ) e. CC /\ ( ; ; 1 0 0 e. CC /\ ; ; 1 0 0 =/= 0 ) ) : No typesetting found for |- ( ( ( A . _ B C ) + ( D . _ E F ) ) e. CC /\ ( G . _ H I ) e. CC /\ ( ; ; 1 0 0 e. CC /\ ; ; 1 0 0 =/= 0 ) ) with typecode |-
39	17 24 35	adddiri	Could not format ( ( ( A . _ B C ) + ( D . _ E F ) ) x. ; ; 1 0 0 ) = ( ( ( A . _ B C ) x. ; ; 1 0 0 ) + ( ( D . _ E F ) x. ; ; 1 0 0 ) ) : No typesetting found for |- ( ( ( A . _ B C ) + ( D . _ E F ) ) x. ; ; 1 0 0 ) = ( ( ( A . _ B C ) x. ; ; 1 0 0 ) + ( ( D . _ E F ) x. ; ; 1 0 0 ) ) with typecode |-
40	1 2 12	dpmul100	Could not format ( ( A . _ B C ) x. ; ; 1 0 0 ) = ; ; A B C : No typesetting found for |- ( ( A . _ B C ) x. ; ; 1 0 0 ) = ; ; A B C with typecode |-
41	4 5 19	dpmul100	Could not format ( ( D . _ E F ) x. ; ; 1 0 0 ) = ; ; D E F : No typesetting found for |- ( ( D . _ E F ) x. ; ; 1 0 0 ) = ; ; D E F with typecode |-
42	40 41	oveq12i	Could not format ( ( ( A . _ B C ) x. ; ; 1 0 0 ) + ( ( D . _ E F ) x. ; ; 1 0 0 ) ) = ( ; ; A B C + ; ; D E F ) : No typesetting found for |- ( ( ( A . _ B C ) x. ; ; 1 0 0 ) + ( ( D . _ E F ) x. ; ; 1 0 0 ) ) = ( ; ; A B C + ; ; D E F ) with typecode |-
43	6 8 27	dpmul100	Could not format ( ( G . _ H I ) x. ; ; 1 0 0 ) = ; ; G H I : No typesetting found for |- ( ( G . _ H I ) x. ; ; 1 0 0 ) = ; ; G H I with typecode |-
44	10 42 43	3eqtr4i	Could not format ( ( ( A . _ B C ) x. ; ; 1 0 0 ) + ( ( D . _ E F ) x. ; ; 1 0 0 ) ) = ( ( G . _ H I ) x. ; ; 1 0 0 ) : No typesetting found for |- ( ( ( A . _ B C ) x. ; ; 1 0 0 ) + ( ( D . _ E F ) x. ; ; 1 0 0 ) ) = ( ( G . _ H I ) x. ; ; 1 0 0 ) with typecode |-
45	39 44	eqtri	Could not format ( ( ( A . _ B C ) + ( D . _ E F ) ) x. ; ; 1 0 0 ) = ( ( G . _ H I ) x. ; ; 1 0 0 ) : No typesetting found for |- ( ( ( A . _ B C ) + ( D . _ E F ) ) x. ; ; 1 0 0 ) = ( ( G . _ H I ) x. ; ; 1 0 0 ) with typecode |-
46		mulcan2	Could not format ( ( ( ( A . _ B C ) + ( D . _ E F ) ) e. CC /\ ( G . _ H I ) e. CC /\ ( ; ; 1 0 0 e. CC /\ ; ; 1 0 0 =/= 0 ) ) -> ( ( ( ( A . _ B C ) + ( D . _ E F ) ) x. ; ; 1 0 0 ) = ( ( G . _ H I ) x. ; ; 1 0 0 ) <-> ( ( A . _ B C ) + ( D . _ E F ) ) = ( G . _ H I ) ) ) : No typesetting found for |- ( ( ( ( A . _ B C ) + ( D . _ E F ) ) e. CC /\ ( G . _ H I ) e. CC /\ ( ; ; 1 0 0 e. CC /\ ; ; 1 0 0 =/= 0 ) ) -> ( ( ( ( A . _ B C ) + ( D . _ E F ) ) x. ; ; 1 0 0 ) = ( ( G . _ H I ) x. ; ; 1 0 0 ) <-> ( ( A . _ B C ) + ( D . _ E F ) ) = ( G . _ H I ) ) ) with typecode |-
47	46	biimpa	Could not format ( ( ( ( ( A . _ B C ) + ( D . _ E F ) ) e. CC /\ ( G . _ H I ) e. CC /\ ( ; ; 1 0 0 e. CC /\ ; ; 1 0 0 =/= 0 ) ) /\ ( ( ( A . _ B C ) + ( D . _ E F ) ) x. ; ; 1 0 0 ) = ( ( G . _ H I ) x. ; ; 1 0 0 ) ) -> ( ( A . _ B C ) + ( D . _ E F ) ) = ( G . _ H I ) ) : No typesetting found for |- ( ( ( ( ( A . _ B C ) + ( D . _ E F ) ) e. CC /\ ( G . _ H I ) e. CC /\ ( ; ; 1 0 0 e. CC /\ ; ; 1 0 0 =/= 0 ) ) /\ ( ( ( A . _ B C ) + ( D . _ E F ) ) x. ; ; 1 0 0 ) = ( ( G . _ H I ) x. ; ; 1 0 0 ) ) -> ( ( A . _ B C ) + ( D . _ E F ) ) = ( G . _ H I ) ) with typecode |-
48	38 45 47	mp2an	Could not format ( ( A . _ B C ) + ( D . _ E F ) ) = ( G . _ H I ) : No typesetting found for |- ( ( A . _ B C ) + ( D . _ E F ) ) = ( G . _ H I ) with typecode |-