dpadd2

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

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

Proof

Step	Hyp	Ref	Expression
1		dpadd2.a	$⊢ A \in ℕ_{0}$
2		dpadd2.b	$⊢ B \in ℝ^{+}$
3		dpadd2.c	$⊢ C \in ℕ_{0}$
4		dpadd2.d	$⊢ D \in ℝ^{+}$
5		dpadd2.e	$⊢ E \in ℕ_{0}$
6		dpadd2.f	$⊢ F \in ℝ^{+}$
7		dpadd2.g	$⊢ G \in ℕ_{0}$
8		dpadd2.h	$⊢ H \in ℕ_{0}$
9		dpadd2.i	$⊢ G + H = I$
10		dpadd2.1	$⊢ (A . B) + (C . D) = E . F$
11	1	nn0rei	$⊢ A \in ℝ$
12		rpre	$⊢ B \in ℝ^{+} \to B \in ℝ$
13	2 12	ax-mp	$⊢ B \in ℝ$
14		dp2cl	Could not format ( ( A e. RR /\ B e. RR ) -> _ A B e. RR ) : No typesetting found for \|- ( ( A e. RR /\ B e. RR ) -> _ A B e. RR ) with typecode \|-
15	11 13 14	mp2an	Could not format _ A B e. RR : No typesetting found for \|- _ A B e. RR with typecode \|-
16	7 15	dpval2	Could not format ( G . _ A B ) = ( G + ( _ A B / ; 1 0 ) ) : No typesetting found for \|- ( G . _ A B ) = ( G + ( _ A B / ; 1 0 ) ) with typecode \|-
17	3	nn0rei	$⊢ C \in ℝ$
18		rpre	$⊢ D \in ℝ^{+} \to D \in ℝ$
19	4 18	ax-mp	$⊢ D \in ℝ$
20		dp2cl	Could not format ( ( C e. RR /\ D e. RR ) -> _ C D e. RR ) : No typesetting found for \|- ( ( C e. RR /\ D e. RR ) -> _ C D e. RR ) with typecode \|-
21	17 19 20	mp2an	Could not format _ C D e. RR : No typesetting found for \|- _ C D e. RR with typecode \|-
22	8 21	dpval2	Could not format ( H . _ C D ) = ( H + ( _ C D / ; 1 0 ) ) : No typesetting found for \|- ( H . _ C D ) = ( H + ( _ C D / ; 1 0 ) ) with typecode \|-
23	16 22	oveq12i	Could not format ( ( G . _ A B ) + ( H . _ C D ) ) = ( ( G + ( _ A B / ; 1 0 ) ) + ( H + ( _ C D / ; 1 0 ) ) ) : No typesetting found for \|- ( ( G . _ A B ) + ( H . _ C D ) ) = ( ( G + ( _ A B / ; 1 0 ) ) + ( H + ( _ C D / ; 1 0 ) ) ) with typecode \|-
24	7	nn0cni	$⊢ G \in ℂ$
25	15	recni	Could not format _ A B e. CC : No typesetting found for \|- _ A B e. CC with typecode \|-
26		10nn	$⊢ 10 \in ℕ$
27	26	nncni	$⊢ 10 \in ℂ$
28	26	nnne0i	$⊢ 10 \neq 0$
29	25 27 28	divcli	Could not format ( _ A B / ; 1 0 ) e. CC : No typesetting found for \|- ( _ A B / ; 1 0 ) e. CC with typecode \|-
30	8	nn0cni	$⊢ H \in ℂ$
31	21	recni	Could not format _ C D e. CC : No typesetting found for \|- _ C D e. CC with typecode \|-
32	31 27 28	divcli	Could not format ( _ C D / ; 1 0 ) e. CC : No typesetting found for \|- ( _ C D / ; 1 0 ) e. CC with typecode \|-
33	24 29 30 32	add4i	Could not format ( ( G + ( _ A B / ; 1 0 ) ) + ( H + ( _ C D / ; 1 0 ) ) ) = ( ( G + H ) + ( ( _ A B / ; 1 0 ) + ( _ C D / ; 1 0 ) ) ) : No typesetting found for \|- ( ( G + ( _ A B / ; 1 0 ) ) + ( H + ( _ C D / ; 1 0 ) ) ) = ( ( G + H ) + ( ( _ A B / ; 1 0 ) + ( _ C D / ; 1 0 ) ) ) with typecode \|-
34	25 31 27 28	divdiri	Could not format ( ( _ A B + _ C D ) / ; 1 0 ) = ( ( _ A B / ; 1 0 ) + ( _ C D / ; 1 0 ) ) : No typesetting found for \|- ( ( _ A B + _ C D ) / ; 1 0 ) = ( ( _ A B / ; 1 0 ) + ( _ C D / ; 1 0 ) ) with typecode \|-
35		dpval	Could not format ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = _ A B ) : No typesetting found for \|- ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = _ A B ) with typecode \|-
36	1 13 35	mp2an	Could not format ( A . B ) = _ A B : No typesetting found for \|- ( A . B ) = _ A B with typecode \|-
37		dpval	Could not format ( ( C e. NN0 /\ D e. RR ) -> ( C . D ) = _ C D ) : No typesetting found for \|- ( ( C e. NN0 /\ D e. RR ) -> ( C . D ) = _ C D ) with typecode \|-
38	3 19 37	mp2an	Could not format ( C . D ) = _ C D : No typesetting found for \|- ( C . D ) = _ C D with typecode \|-
39	36 38	oveq12i	Could not format ( ( A . B ) + ( C . D ) ) = ( _ A B + _ C D ) : No typesetting found for \|- ( ( A . B ) + ( C . D ) ) = ( _ A B + _ C D ) with typecode \|-
40		rpre	$⊢ F \in ℝ^{+} \to F \in ℝ$
41	6 40	ax-mp	$⊢ F \in ℝ$
42		dpval	Could not format ( ( E e. NN0 /\ F e. RR ) -> ( E . F ) = _ E F ) : No typesetting found for \|- ( ( E e. NN0 /\ F e. RR ) -> ( E . F ) = _ E F ) with typecode \|-
43	5 41 42	mp2an	Could not format ( E . F ) = _ E F : No typesetting found for \|- ( E . F ) = _ E F with typecode \|-
44	10 39 43	3eqtr3i	Could not format ( _ A B + _ C D ) = _ E F : No typesetting found for \|- ( _ A B + _ C D ) = _ E F with typecode \|-
45	44	oveq1i	Could not format ( ( _ A B + _ C D ) / ; 1 0 ) = ( _ E F / ; 1 0 ) : No typesetting found for \|- ( ( _ A B + _ C D ) / ; 1 0 ) = ( _ E F / ; 1 0 ) with typecode \|-
46	34 45	eqtr3i	Could not format ( ( _ A B / ; 1 0 ) + ( _ C D / ; 1 0 ) ) = ( _ E F / ; 1 0 ) : No typesetting found for \|- ( ( _ A B / ; 1 0 ) + ( _ C D / ; 1 0 ) ) = ( _ E F / ; 1 0 ) with typecode \|-
47	9 46	oveq12i	Could not format ( ( G + H ) + ( ( _ A B / ; 1 0 ) + ( _ C D / ; 1 0 ) ) ) = ( I + ( _ E F / ; 1 0 ) ) : No typesetting found for \|- ( ( G + H ) + ( ( _ A B / ; 1 0 ) + ( _ C D / ; 1 0 ) ) ) = ( I + ( _ E F / ; 1 0 ) ) with typecode \|-
48	7 8	nn0addcli	$⊢ G + H \in ℕ_{0}$
49	9 48	eqeltrri	$⊢ I \in ℕ_{0}$
50	5	nn0rei	$⊢ E \in ℝ$
51		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 \|-
52	50 41 51	mp2an	Could not format _ E F e. RR : No typesetting found for \|- _ E F e. RR with typecode \|-
53	49 52	dpval2	Could not format ( I . _ E F ) = ( I + ( _ E F / ; 1 0 ) ) : No typesetting found for \|- ( I . _ E F ) = ( I + ( _ E F / ; 1 0 ) ) with typecode \|-
54	47 53	eqtr4i	Could not format ( ( G + H ) + ( ( _ A B / ; 1 0 ) + ( _ C D / ; 1 0 ) ) ) = ( I . _ E F ) : No typesetting found for \|- ( ( G + H ) + ( ( _ A B / ; 1 0 ) + ( _ C D / ; 1 0 ) ) ) = ( I . _ E F ) with typecode \|-
55	23 33 54	3eqtri	Could not format ( ( G . _ A B ) + ( H . _ C D ) ) = ( I . _ E F ) : No typesetting found for \|- ( ( G . _ A B ) + ( H . _ C D ) ) = ( I . _ E F ) with typecode \|-

Metamath Proof Explorer

Theorem dpadd2

Proof