Theorem dpadd2

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

	Ref	Expression
Hypotheses	dpadd2.a	$$⊢A\in {\mathbb{N}}_0$$
	dpadd2.b	$$⊢B\in {ℝ}^{+}$$
	dpadd2.c	$$⊢C\in {\mathbb{N}}_0$$
	dpadd2.d	$$⊢D\in {ℝ}^{+}$$
	dpadd2.e	$$⊢E\in {\mathbb{N}}_0$$
	dpadd2.f	$$⊢F\in {ℝ}^{+}$$
	dpadd2.g	$$⊢G\in {\mathbb{N}}_0$$
	dpadd2.h	$$⊢H\in {\mathbb{N}}_0$$
	dpadd2.i	$$⊢G+H=I$$
	dpadd2.1	$$⊢\left(A.B\right)+\left(C.D\right)=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 {\mathbb{N}}_0$$
2		dpadd2.b	$$⊢B\in {ℝ}^{+}$$
3		dpadd2.c	$$⊢C\in {\mathbb{N}}_0$$
4		dpadd2.d	$$⊢D\in {ℝ}^{+}$$
5		dpadd2.e	$$⊢E\in {\mathbb{N}}_0$$
6		dpadd2.f	$$⊢F\in {ℝ}^{+}$$
7		dpadd2.g	$$⊢G\in {\mathbb{N}}_0$$
8		dpadd2.h	$$⊢H\in {\mathbb{N}}_0$$
9		dpadd2.i	$$⊢G+H=I$$
10		dpadd2.1	$$⊢\left(A.B\right)+\left(C.D\right)=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 \mathbb{N}$$
27	26	nncni	$$⊢10\in ℂ$$
28	26	nnne0i	$$⊢10\ne 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 {\mathbb{N}}_0$$
49	9 48	eqeltrri	$$⊢I\in {\mathbb{N}}_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 |-