dpadd3

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

	Ref	Expression
Hypotheses	dpmul.a	$⊢ A \in ℕ_{0}$
	dpmul.b	$⊢ B \in ℕ_{0}$
	dpmul.c	$⊢ C \in ℕ_{0}$
	dpmul.d	$⊢ D \in ℕ_{0}$
	dpmul.e	$⊢ E \in ℕ_{0}$
	dpmul.g	$⊢ G \in ℕ_{0}$
	dpadd3.f	$⊢ F \in ℕ_{0}$
	dpadd3.h	$⊢ H \in ℕ_{0}$
	dpadd3.i	$⊢ I \in ℕ_{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 ℕ_{0}$
2		dpmul.b	$⊢ B \in ℕ_{0}$
3		dpmul.c	$⊢ C \in ℕ_{0}$
4		dpmul.d	$⊢ D \in ℕ_{0}$
5		dpmul.e	$⊢ E \in ℕ_{0}$
6		dpmul.g	$⊢ G \in ℕ_{0}$
7		dpadd3.f	$⊢ F \in ℕ_{0}$
8		dpadd3.h	$⊢ H \in ℕ_{0}$
9		dpadd3.i	$⊢ I \in ℕ_{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 ℕ$
34	33	decnncl2	$⊢ 100 \in ℕ$
35	34	nncni	$⊢ 100 \in ℂ$
36	34	nnne0i	$⊢ 100 \neq 0$
37	35 36	pm3.2i	$⊢ (100 \in ℂ \land 100 \neq 0)$
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 \|-

Metamath Proof Explorer

Theorem dpadd3

Proof