Theorem dpmul4

Description: An upper bound to multiplication of decimal numbers with 4 digits. (Contributed by Thierry Arnoux, 25-Dec-2021)

	Ref	Expression
Hypotheses	dpmul.a	⊢ 𝐴 ∈ ℕ0
	dpmul.b	⊢ 𝐵 ∈ ℕ0
	dpmul.c	⊢ 𝐶 ∈ ℕ0
	dpmul.d	⊢ 𝐷 ∈ ℕ0
	dpmul.e	⊢ 𝐸 ∈ ℕ0
	dpmul.g	⊢ 𝐺 ∈ ℕ0
	dpmul.j	⊢ 𝐽 ∈ ℕ0
	dpmul.k	⊢ 𝐾 ∈ ℕ0
	dpmul4.f	⊢ 𝐹 ∈ ℕ0
	dpmul4.h	⊢ 𝐻 ∈ ℕ0
	dpmul4.i	⊢ 𝐼 ∈ ℕ0
	dpmul4.l	⊢ 𝐿 ∈ ℕ0
	dpmul4.m	⊢ 𝑀 ∈ ℕ0
	dpmul4.n	⊢ 𝑁 ∈ ℕ0
	dpmul4.o	⊢ 𝑂 ∈ ℕ0
	dpmul4.p	⊢ 𝑃 ∈ ℕ0
	dpmul4.q	⊢ 𝑄 ∈ ℕ0
	dpmul4.r	⊢ 𝑅 ∈ ℕ0
	dpmul4.s	⊢ 𝑆 ∈ ℕ0
	dpmul4.t	⊢ 𝑇 ∈ ℕ0
	dpmul4.u	⊢ 𝑈 ∈ ℕ0
	dpmul4.w	⊢ 𝑊 ∈ ℕ0
	dpmul4.x	⊢ 𝑋 ∈ ℕ0
	dpmul4.y	⊢ 𝑌 ∈ ℕ0
	dpmul4.z	⊢ 𝑍 ∈ ℕ0
	dpmul4.a	⊢ 𝑈 < ; 1 0
	dpmul4.b	⊢ 𝑃 < ; 1 0
	dpmul4.c	⊢ 𝑄 < ; 1 0
	dpmul4.1	⊢ ( ; ; 𝐿 𝑀 𝑁 + 𝑂 ) = ; ; ; 𝑅 𝑆 𝑇 𝑈
	dpmul4.2	⊢ ( ( 𝐴 . 𝐵 ) · ( 𝐸 . 𝐹 ) ) = ( 𝐼 . _ 𝐽 𝐾 )
	dpmul4.3	⊢ ( ( 𝐶 . 𝐷 ) · ( 𝐺 . 𝐻 ) ) = ( 𝑂 . _ 𝑃 𝑄 )
	dpmul4.4	⊢ ( ; ; ; 𝐼 𝐽 𝐾 1 + ; ; 𝑅 𝑆 𝑇 ) = ; ; ; 𝑊 𝑋 𝑌 𝑍
	dpmul4.5	⊢ ( ( ( 𝐴 . 𝐵 ) + ( 𝐶 . 𝐷 ) ) · ( ( 𝐸 . 𝐹 ) + ( 𝐺 . 𝐻 ) ) ) = ( ( ( 𝐼 . _ 𝐽 𝐾 ) + ( 𝐿 . _ 𝑀 𝑁 ) ) + ( 𝑂 . _ 𝑃 𝑄 ) )
Assertion	dpmul4	⊢ ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ( 𝐸 . _ 𝐹 _ 𝐺 𝐻 ) ) < ( 𝑊 . _ 𝑋 _ 𝑌 𝑍 )

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		dpmul.j	⊢ 𝐽 ∈ ℕ0
8		dpmul.k	⊢ 𝐾 ∈ ℕ0
9		dpmul4.f	⊢ 𝐹 ∈ ℕ0
10		dpmul4.h	⊢ 𝐻 ∈ ℕ0
11		dpmul4.i	⊢ 𝐼 ∈ ℕ0
12		dpmul4.l	⊢ 𝐿 ∈ ℕ0
13		dpmul4.m	⊢ 𝑀 ∈ ℕ0
14		dpmul4.n	⊢ 𝑁 ∈ ℕ0
15		dpmul4.o	⊢ 𝑂 ∈ ℕ0
16		dpmul4.p	⊢ 𝑃 ∈ ℕ0
17		dpmul4.q	⊢ 𝑄 ∈ ℕ0
18		dpmul4.r	⊢ 𝑅 ∈ ℕ0
19		dpmul4.s	⊢ 𝑆 ∈ ℕ0
20		dpmul4.t	⊢ 𝑇 ∈ ℕ0
21		dpmul4.u	⊢ 𝑈 ∈ ℕ0
22		dpmul4.w	⊢ 𝑊 ∈ ℕ0
23		dpmul4.x	⊢ 𝑋 ∈ ℕ0
24		dpmul4.y	⊢ 𝑌 ∈ ℕ0
25		dpmul4.z	⊢ 𝑍 ∈ ℕ0
26		dpmul4.a	⊢ 𝑈 < ; 1 0
27		dpmul4.b	⊢ 𝑃 < ; 1 0
28		dpmul4.c	⊢ 𝑄 < ; 1 0
29		dpmul4.1	⊢ ( ; ; 𝐿 𝑀 𝑁 + 𝑂 ) = ; ; ; 𝑅 𝑆 𝑇 𝑈
30		dpmul4.2	⊢ ( ( 𝐴 . 𝐵 ) · ( 𝐸 . 𝐹 ) ) = ( 𝐼 . _ 𝐽 𝐾 )
31		dpmul4.3	⊢ ( ( 𝐶 . 𝐷 ) · ( 𝐺 . 𝐻 ) ) = ( 𝑂 . _ 𝑃 𝑄 )
32		dpmul4.4	⊢ ( ; ; ; 𝐼 𝐽 𝐾 1 + ; ; 𝑅 𝑆 𝑇 ) = ; ; ; 𝑊 𝑋 𝑌 𝑍
33		dpmul4.5	⊢ ( ( ( 𝐴 . 𝐵 ) + ( 𝐶 . 𝐷 ) ) · ( ( 𝐸 . 𝐹 ) + ( 𝐺 . 𝐻 ) ) ) = ( ( ( 𝐼 . _ 𝐽 𝐾 ) + ( 𝐿 . _ 𝑀 𝑁 ) ) + ( 𝑂 . _ 𝑃 𝑄 ) )
34	1 2	deccl	⊢ ; 𝐴 𝐵 ∈ ℕ0
35	3 4	deccl	⊢ ; 𝐶 𝐷 ∈ ℕ0
36	5 9	deccl	⊢ ; 𝐸 𝐹 ∈ ℕ0
37	6 10	deccl	⊢ ; 𝐺 𝐻 ∈ ℕ0
38	12 13	deccl	⊢ ; 𝐿 𝑀 ∈ ℕ0
39	38 14	deccl	⊢ ; ; 𝐿 𝑀 𝑁 ∈ ℕ0
40		2nn0	⊢ 2 ∈ ℕ0
41	2	nn0rei	⊢ 𝐵 ∈ ℝ
42		dpcl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 . 𝐵 ) ∈ ℝ )
43	1 41 42	mp2an	⊢ ( 𝐴 . 𝐵 ) ∈ ℝ
44	43	recni	⊢ ( 𝐴 . 𝐵 ) ∈ ℂ
45		10nn	⊢ ; 1 0 ∈ ℕ
46	45	nncni	⊢ ; 1 0 ∈ ℂ
47	9	nn0rei	⊢ 𝐹 ∈ ℝ
48		dpcl	⊢ ( ( 𝐸 ∈ ℕ0 ∧ 𝐹 ∈ ℝ ) → ( 𝐸 . 𝐹 ) ∈ ℝ )
49	5 47 48	mp2an	⊢ ( 𝐸 . 𝐹 ) ∈ ℝ
50	49	recni	⊢ ( 𝐸 . 𝐹 ) ∈ ℂ
51	44 46 50 46	mul4i	⊢ ( ( ( 𝐴 . 𝐵 ) · ; 1 0 ) · ( ( 𝐸 . 𝐹 ) · ; 1 0 ) ) = ( ( ( 𝐴 . 𝐵 ) · ( 𝐸 . 𝐹 ) ) · ( ; 1 0 · ; 1 0 ) )
52	44 50	mulcli	⊢ ( ( 𝐴 . 𝐵 ) · ( 𝐸 . 𝐹 ) ) ∈ ℂ
53	52 46 46	mulassi	⊢ ( ( ( ( 𝐴 . 𝐵 ) · ( 𝐸 . 𝐹 ) ) · ; 1 0 ) · ; 1 0 ) = ( ( ( 𝐴 . 𝐵 ) · ( 𝐸 . 𝐹 ) ) · ( ; 1 0 · ; 1 0 ) )
54	30	oveq1i	⊢ ( ( ( 𝐴 . 𝐵 ) · ( 𝐸 . 𝐹 ) ) · ; 1 0 ) = ( ( 𝐼 . _ 𝐽 𝐾 ) · ; 1 0 )
55	8	nn0rei	⊢ 𝐾 ∈ ℝ
56	11 7 55	dp3mul10	⊢ ( ( 𝐼 . _ 𝐽 𝐾 ) · ; 1 0 ) = ( ; 𝐼 𝐽 . 𝐾 )
57	54 56	eqtri	⊢ ( ( ( 𝐴 . 𝐵 ) · ( 𝐸 . 𝐹 ) ) · ; 1 0 ) = ( ; 𝐼 𝐽 . 𝐾 )
58	57	oveq1i	⊢ ( ( ( ( 𝐴 . 𝐵 ) · ( 𝐸 . 𝐹 ) ) · ; 1 0 ) · ; 1 0 ) = ( ( ; 𝐼 𝐽 . 𝐾 ) · ; 1 0 )
59	51 53 58	3eqtr2ri	⊢ ( ( ; 𝐼 𝐽 . 𝐾 ) · ; 1 0 ) = ( ( ( 𝐴 . 𝐵 ) · ; 1 0 ) · ( ( 𝐸 . 𝐹 ) · ; 1 0 ) )
60	11 7	deccl	⊢ ; 𝐼 𝐽 ∈ ℕ0
61	60 55	dpmul10	⊢ ( ( ; 𝐼 𝐽 . 𝐾 ) · ; 1 0 ) = ; ; 𝐼 𝐽 𝐾
62	1 41	dpmul10	⊢ ( ( 𝐴 . 𝐵 ) · ; 1 0 ) = ; 𝐴 𝐵
63	5 47	dpmul10	⊢ ( ( 𝐸 . 𝐹 ) · ; 1 0 ) = ; 𝐸 𝐹
64	62 63	oveq12i	⊢ ( ( ( 𝐴 . 𝐵 ) · ; 1 0 ) · ( ( 𝐸 . 𝐹 ) · ; 1 0 ) ) = ( ; 𝐴 𝐵 · ; 𝐸 𝐹 )
65	59 61 64	3eqtr3ri	⊢ ( ; 𝐴 𝐵 · ; 𝐸 𝐹 ) = ; ; 𝐼 𝐽 𝐾
66	4	nn0rei	⊢ 𝐷 ∈ ℝ
67		dpcl	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℝ ) → ( 𝐶 . 𝐷 ) ∈ ℝ )
68	3 66 67	mp2an	⊢ ( 𝐶 . 𝐷 ) ∈ ℝ
69	68	recni	⊢ ( 𝐶 . 𝐷 ) ∈ ℂ
70	10	nn0rei	⊢ 𝐻 ∈ ℝ
71		dpcl	⊢ ( ( 𝐺 ∈ ℕ0 ∧ 𝐻 ∈ ℝ ) → ( 𝐺 . 𝐻 ) ∈ ℝ )
72	6 70 71	mp2an	⊢ ( 𝐺 . 𝐻 ) ∈ ℝ
73	72	recni	⊢ ( 𝐺 . 𝐻 ) ∈ ℂ
74	69 46 73 46	mul4i	⊢ ( ( ( 𝐶 . 𝐷 ) · ; 1 0 ) · ( ( 𝐺 . 𝐻 ) · ; 1 0 ) ) = ( ( ( 𝐶 . 𝐷 ) · ( 𝐺 . 𝐻 ) ) · ( ; 1 0 · ; 1 0 ) )
75	69 73	mulcli	⊢ ( ( 𝐶 . 𝐷 ) · ( 𝐺 . 𝐻 ) ) ∈ ℂ
76	75 46 46	mulassi	⊢ ( ( ( ( 𝐶 . 𝐷 ) · ( 𝐺 . 𝐻 ) ) · ; 1 0 ) · ; 1 0 ) = ( ( ( 𝐶 . 𝐷 ) · ( 𝐺 . 𝐻 ) ) · ( ; 1 0 · ; 1 0 ) )
77	31	oveq1i	⊢ ( ( ( 𝐶 . 𝐷 ) · ( 𝐺 . 𝐻 ) ) · ; 1 0 ) = ( ( 𝑂 . _ 𝑃 𝑄 ) · ; 1 0 )
78	17	nn0rei	⊢ 𝑄 ∈ ℝ
79	15 16 78	dp3mul10	⊢ ( ( 𝑂 . _ 𝑃 𝑄 ) · ; 1 0 ) = ( ; 𝑂 𝑃 . 𝑄 )
80	77 79	eqtri	⊢ ( ( ( 𝐶 . 𝐷 ) · ( 𝐺 . 𝐻 ) ) · ; 1 0 ) = ( ; 𝑂 𝑃 . 𝑄 )
81	80	oveq1i	⊢ ( ( ( ( 𝐶 . 𝐷 ) · ( 𝐺 . 𝐻 ) ) · ; 1 0 ) · ; 1 0 ) = ( ( ; 𝑂 𝑃 . 𝑄 ) · ; 1 0 )
82	74 76 81	3eqtr2ri	⊢ ( ( ; 𝑂 𝑃 . 𝑄 ) · ; 1 0 ) = ( ( ( 𝐶 . 𝐷 ) · ; 1 0 ) · ( ( 𝐺 . 𝐻 ) · ; 1 0 ) )
83	15 16	deccl	⊢ ; 𝑂 𝑃 ∈ ℕ0
84	83 78	dpmul10	⊢ ( ( ; 𝑂 𝑃 . 𝑄 ) · ; 1 0 ) = ; ; 𝑂 𝑃 𝑄
85	3 66	dpmul10	⊢ ( ( 𝐶 . 𝐷 ) · ; 1 0 ) = ; 𝐶 𝐷
86	6 70	dpmul10	⊢ ( ( 𝐺 . 𝐻 ) · ; 1 0 ) = ; 𝐺 𝐻
87	85 86	oveq12i	⊢ ( ( ( 𝐶 . 𝐷 ) · ; 1 0 ) · ( ( 𝐺 . 𝐻 ) · ; 1 0 ) ) = ( ; 𝐶 𝐷 · ; 𝐺 𝐻 )
88	82 84 87	3eqtr3ri	⊢ ( ; 𝐶 𝐷 · ; 𝐺 𝐻 ) = ; ; 𝑂 𝑃 𝑄
89	44 69 46	adddiri	⊢ ( ( ( 𝐴 . 𝐵 ) + ( 𝐶 . 𝐷 ) ) · ; 1 0 ) = ( ( ( 𝐴 . 𝐵 ) · ; 1 0 ) + ( ( 𝐶 . 𝐷 ) · ; 1 0 ) )
90	62 85	oveq12i	⊢ ( ( ( 𝐴 . 𝐵 ) · ; 1 0 ) + ( ( 𝐶 . 𝐷 ) · ; 1 0 ) ) = ( ; 𝐴 𝐵 + ; 𝐶 𝐷 )
91	89 90	eqtr2i	⊢ ( ; 𝐴 𝐵 + ; 𝐶 𝐷 ) = ( ( ( 𝐴 . 𝐵 ) + ( 𝐶 . 𝐷 ) ) · ; 1 0 )
92	50 73 46	adddiri	⊢ ( ( ( 𝐸 . 𝐹 ) + ( 𝐺 . 𝐻 ) ) · ; 1 0 ) = ( ( ( 𝐸 . 𝐹 ) · ; 1 0 ) + ( ( 𝐺 . 𝐻 ) · ; 1 0 ) )
93	63 86	oveq12i	⊢ ( ( ( 𝐸 . 𝐹 ) · ; 1 0 ) + ( ( 𝐺 . 𝐻 ) · ; 1 0 ) ) = ( ; 𝐸 𝐹 + ; 𝐺 𝐻 )
94	92 93	eqtr2i	⊢ ( ; 𝐸 𝐹 + ; 𝐺 𝐻 ) = ( ( ( 𝐸 . 𝐹 ) + ( 𝐺 . 𝐻 ) ) · ; 1 0 )
95	91 94	oveq12i	⊢ ( ( ; 𝐴 𝐵 + ; 𝐶 𝐷 ) · ( ; 𝐸 𝐹 + ; 𝐺 𝐻 ) ) = ( ( ( ( 𝐴 . 𝐵 ) + ( 𝐶 . 𝐷 ) ) · ; 1 0 ) · ( ( ( 𝐸 . 𝐹 ) + ( 𝐺 . 𝐻 ) ) · ; 1 0 ) )
96	44 69	addcli	⊢ ( ( 𝐴 . 𝐵 ) + ( 𝐶 . 𝐷 ) ) ∈ ℂ
97	50 73	addcli	⊢ ( ( 𝐸 . 𝐹 ) + ( 𝐺 . 𝐻 ) ) ∈ ℂ
98	96 46 97 46	mul4i	⊢ ( ( ( ( 𝐴 . 𝐵 ) + ( 𝐶 . 𝐷 ) ) · ; 1 0 ) · ( ( ( 𝐸 . 𝐹 ) + ( 𝐺 . 𝐻 ) ) · ; 1 0 ) ) = ( ( ( ( 𝐴 . 𝐵 ) + ( 𝐶 . 𝐷 ) ) · ( ( 𝐸 . 𝐹 ) + ( 𝐺 . 𝐻 ) ) ) · ( ; 1 0 · ; 1 0 ) )
99	33	oveq1i	⊢ ( ( ( ( 𝐴 . 𝐵 ) + ( 𝐶 . 𝐷 ) ) · ( ( 𝐸 . 𝐹 ) + ( 𝐺 . 𝐻 ) ) ) · ( ; 1 0 · ; 1 0 ) ) = ( ( ( ( 𝐼 . _ 𝐽 𝐾 ) + ( 𝐿 . _ 𝑀 𝑁 ) ) + ( 𝑂 . _ 𝑃 𝑄 ) ) · ( ; 1 0 · ; 1 0 ) )
100	95 98 99	3eqtri	⊢ ( ( ; 𝐴 𝐵 + ; 𝐶 𝐷 ) · ( ; 𝐸 𝐹 + ; 𝐺 𝐻 ) ) = ( ( ( ( 𝐼 . _ 𝐽 𝐾 ) + ( 𝐿 . _ 𝑀 𝑁 ) ) + ( 𝑂 . _ 𝑃 𝑄 ) ) · ( ; 1 0 · ; 1 0 ) )
101		10nn0	⊢ ; 1 0 ∈ ℕ0
102	101	dec0u	⊢ ( ; 1 0 · ; 1 0 ) = ; ; 1 0 0
103	102	oveq2i	⊢ ( ( ( ( 𝐼 . _ 𝐽 𝐾 ) + ( 𝐿 . _ 𝑀 𝑁 ) ) + ( 𝑂 . _ 𝑃 𝑄 ) ) · ( ; 1 0 · ; 1 0 ) ) = ( ( ( ( 𝐼 . _ 𝐽 𝐾 ) + ( 𝐿 . _ 𝑀 𝑁 ) ) + ( 𝑂 . _ 𝑃 𝑄 ) ) · ; ; 1 0 0 )
104	30 52	eqeltrri	⊢ ( 𝐼 . _ 𝐽 𝐾 ) ∈ ℂ
105	13	nn0rei	⊢ 𝑀 ∈ ℝ
106	14	nn0rei	⊢ 𝑁 ∈ ℝ
107		dp2cl	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → _ 𝑀 𝑁 ∈ ℝ )
108	105 106 107	mp2an	⊢ _ 𝑀 𝑁 ∈ ℝ
109		dpcl	⊢ ( ( 𝐿 ∈ ℕ0 ∧ _ 𝑀 𝑁 ∈ ℝ ) → ( 𝐿 . _ 𝑀 𝑁 ) ∈ ℝ )
110	12 108 109	mp2an	⊢ ( 𝐿 . _ 𝑀 𝑁 ) ∈ ℝ
111	110	recni	⊢ ( 𝐿 . _ 𝑀 𝑁 ) ∈ ℂ
112	104 111	addcli	⊢ ( ( 𝐼 . _ 𝐽 𝐾 ) + ( 𝐿 . _ 𝑀 𝑁 ) ) ∈ ℂ
113	31 75	eqeltrri	⊢ ( 𝑂 . _ 𝑃 𝑄 ) ∈ ℂ
114		0nn0	⊢ 0 ∈ ℕ0
115	101 114	deccl	⊢ ; ; 1 0 0 ∈ ℕ0
116	115	nn0cni	⊢ ; ; 1 0 0 ∈ ℂ
117	112 113 116	adddiri	⊢ ( ( ( ( 𝐼 . _ 𝐽 𝐾 ) + ( 𝐿 . _ 𝑀 𝑁 ) ) + ( 𝑂 . _ 𝑃 𝑄 ) ) · ; ; 1 0 0 ) = ( ( ( ( 𝐼 . _ 𝐽 𝐾 ) + ( 𝐿 . _ 𝑀 𝑁 ) ) · ; ; 1 0 0 ) + ( ( 𝑂 . _ 𝑃 𝑄 ) · ; ; 1 0 0 ) )
118	104 111 116	adddiri	⊢ ( ( ( 𝐼 . _ 𝐽 𝐾 ) + ( 𝐿 . _ 𝑀 𝑁 ) ) · ; ; 1 0 0 ) = ( ( ( 𝐼 . _ 𝐽 𝐾 ) · ; ; 1 0 0 ) + ( ( 𝐿 . _ 𝑀 𝑁 ) · ; ; 1 0 0 ) )
119	118	oveq1i	⊢ ( ( ( ( 𝐼 . _ 𝐽 𝐾 ) + ( 𝐿 . _ 𝑀 𝑁 ) ) · ; ; 1 0 0 ) + ( ( 𝑂 . _ 𝑃 𝑄 ) · ; ; 1 0 0 ) ) = ( ( ( ( 𝐼 . _ 𝐽 𝐾 ) · ; ; 1 0 0 ) + ( ( 𝐿 . _ 𝑀 𝑁 ) · ; ; 1 0 0 ) ) + ( ( 𝑂 . _ 𝑃 𝑄 ) · ; ; 1 0 0 ) )
120	11 7 55	dpmul100	⊢ ( ( 𝐼 . _ 𝐽 𝐾 ) · ; ; 1 0 0 ) = ; ; 𝐼 𝐽 𝐾
121	12 13 106	dpmul100	⊢ ( ( 𝐿 . _ 𝑀 𝑁 ) · ; ; 1 0 0 ) = ; ; 𝐿 𝑀 𝑁
122	120 121	oveq12i	⊢ ( ( ( 𝐼 . _ 𝐽 𝐾 ) · ; ; 1 0 0 ) + ( ( 𝐿 . _ 𝑀 𝑁 ) · ; ; 1 0 0 ) ) = ( ; ; 𝐼 𝐽 𝐾 + ; ; 𝐿 𝑀 𝑁 )
123	15 16 78	dpmul100	⊢ ( ( 𝑂 . _ 𝑃 𝑄 ) · ; ; 1 0 0 ) = ; ; 𝑂 𝑃 𝑄
124	122 123	oveq12i	⊢ ( ( ( ( 𝐼 . _ 𝐽 𝐾 ) · ; ; 1 0 0 ) + ( ( 𝐿 . _ 𝑀 𝑁 ) · ; ; 1 0 0 ) ) + ( ( 𝑂 . _ 𝑃 𝑄 ) · ; ; 1 0 0 ) ) = ( ( ; ; 𝐼 𝐽 𝐾 + ; ; 𝐿 𝑀 𝑁 ) + ; ; 𝑂 𝑃 𝑄 )
125	117 119 124	3eqtri	⊢ ( ( ( ( 𝐼 . _ 𝐽 𝐾 ) + ( 𝐿 . _ 𝑀 𝑁 ) ) + ( 𝑂 . _ 𝑃 𝑄 ) ) · ; ; 1 0 0 ) = ( ( ; ; 𝐼 𝐽 𝐾 + ; ; 𝐿 𝑀 𝑁 ) + ; ; 𝑂 𝑃 𝑄 )
126	100 103 125	3eqtri	⊢ ( ( ; 𝐴 𝐵 + ; 𝐶 𝐷 ) · ( ; 𝐸 𝐹 + ; 𝐺 𝐻 ) ) = ( ( ; ; 𝐼 𝐽 𝐾 + ; ; 𝐿 𝑀 𝑁 ) + ; ; 𝑂 𝑃 𝑄 )
127		sq10	⊢ ( ; 1 0 ↑ 2 ) = ; ; 1 0 0
128	127	oveq2i	⊢ ( ; 𝐴 𝐵 · ( ; 1 0 ↑ 2 ) ) = ( ; 𝐴 𝐵 · ; ; 1 0 0 )
129	34	nn0cni	⊢ ; 𝐴 𝐵 ∈ ℂ
130	116 129	mulcomi	⊢ ( ; ; 1 0 0 · ; 𝐴 𝐵 ) = ( ; 𝐴 𝐵 · ; ; 1 0 0 )
131	128 130	eqtr4i	⊢ ( ; 𝐴 𝐵 · ( ; 1 0 ↑ 2 ) ) = ( ; ; 1 0 0 · ; 𝐴 𝐵 )
132	131	oveq1i	⊢ ( ( ; 𝐴 𝐵 · ( ; 1 0 ↑ 2 ) ) + ; 𝐶 𝐷 ) = ( ( ; ; 1 0 0 · ; 𝐴 𝐵 ) + ; 𝐶 𝐷 )
133	34 3 66	dfdec100	⊢ ; ; ; 𝐴 𝐵 𝐶 𝐷 = ( ( ; ; 1 0 0 · ; 𝐴 𝐵 ) + ; 𝐶 𝐷 )
134	132 133	eqtr4i	⊢ ( ( ; 𝐴 𝐵 · ( ; 1 0 ↑ 2 ) ) + ; 𝐶 𝐷 ) = ; ; ; 𝐴 𝐵 𝐶 𝐷
135	127	oveq2i	⊢ ( ; 𝐸 𝐹 · ( ; 1 0 ↑ 2 ) ) = ( ; 𝐸 𝐹 · ; ; 1 0 0 )
136	36	nn0cni	⊢ ; 𝐸 𝐹 ∈ ℂ
137	116 136	mulcomi	⊢ ( ; ; 1 0 0 · ; 𝐸 𝐹 ) = ( ; 𝐸 𝐹 · ; ; 1 0 0 )
138	135 137	eqtr4i	⊢ ( ; 𝐸 𝐹 · ( ; 1 0 ↑ 2 ) ) = ( ; ; 1 0 0 · ; 𝐸 𝐹 )
139	138	oveq1i	⊢ ( ( ; 𝐸 𝐹 · ( ; 1 0 ↑ 2 ) ) + ; 𝐺 𝐻 ) = ( ( ; ; 1 0 0 · ; 𝐸 𝐹 ) + ; 𝐺 𝐻 )
140	36 6 70	dfdec100	⊢ ; ; ; 𝐸 𝐹 𝐺 𝐻 = ( ( ; ; 1 0 0 · ; 𝐸 𝐹 ) + ; 𝐺 𝐻 )
141	139 140	eqtr4i	⊢ ( ( ; 𝐸 𝐹 · ( ; 1 0 ↑ 2 ) ) + ; 𝐺 𝐻 ) = ; ; ; 𝐸 𝐹 𝐺 𝐻
142	46	sqvali	⊢ ( ; 1 0 ↑ 2 ) = ( ; 1 0 · ; 1 0 )
143	142	oveq2i	⊢ ( ; ; 𝐼 𝐽 𝐾 · ( ; 1 0 ↑ 2 ) ) = ( ; ; 𝐼 𝐽 𝐾 · ( ; 1 0 · ; 1 0 ) )
144	60 8	deccl	⊢ ; ; 𝐼 𝐽 𝐾 ∈ ℕ0
145	144	nn0cni	⊢ ; ; 𝐼 𝐽 𝐾 ∈ ℂ
146	145 46 46	mulassi	⊢ ( ( ; ; 𝐼 𝐽 𝐾 · ; 1 0 ) · ; 1 0 ) = ( ; ; 𝐼 𝐽 𝐾 · ( ; 1 0 · ; 1 0 ) )
147	143 146	eqtr4i	⊢ ( ; ; 𝐼 𝐽 𝐾 · ( ; 1 0 ↑ 2 ) ) = ( ( ; ; 𝐼 𝐽 𝐾 · ; 1 0 ) · ; 1 0 )
148	18 19	deccl	⊢ ; 𝑅 𝑆 ∈ ℕ0
149	148 20	deccl	⊢ ; ; 𝑅 𝑆 𝑇 ∈ ℕ0
150	149	nn0cni	⊢ ; ; 𝑅 𝑆 𝑇 ∈ ℂ
151		ax-1cn	⊢ 1 ∈ ℂ
152	150 151	addcli	⊢ ( ; ; 𝑅 𝑆 𝑇 + 1 ) ∈ ℂ
153	145 46	mulcli	⊢ ( ; ; 𝐼 𝐽 𝐾 · ; 1 0 ) ∈ ℂ
154	151 153	addcomi	⊢ ( 1 + ( ; ; 𝐼 𝐽 𝐾 · ; 1 0 ) ) = ( ( ; ; 𝐼 𝐽 𝐾 · ; 1 0 ) + 1 )
155	46 145	mulcomi	⊢ ( ; 1 0 · ; ; 𝐼 𝐽 𝐾 ) = ( ; ; 𝐼 𝐽 𝐾 · ; 1 0 )
156	144	dec0u	⊢ ( ; 1 0 · ; ; 𝐼 𝐽 𝐾 ) = ; ; ; 𝐼 𝐽 𝐾 0
157	155 156	eqtr3i	⊢ ( ; ; 𝐼 𝐽 𝐾 · ; 1 0 ) = ; ; ; 𝐼 𝐽 𝐾 0
158	157	oveq1i	⊢ ( ( ; ; 𝐼 𝐽 𝐾 · ; 1 0 ) + 1 ) = ( ; ; ; 𝐼 𝐽 𝐾 0 + 1 )
159	151	addlidi	⊢ ( 0 + 1 ) = 1
160		eqid	⊢ ; ; ; 𝐼 𝐽 𝐾 0 = ; ; ; 𝐼 𝐽 𝐾 0
161	144 114 159 160	decsuc	⊢ ( ; ; ; 𝐼 𝐽 𝐾 0 + 1 ) = ; ; ; 𝐼 𝐽 𝐾 1
162	154 158 161	3eqtri	⊢ ( 1 + ( ; ; 𝐼 𝐽 𝐾 · ; 1 0 ) ) = ; ; ; 𝐼 𝐽 𝐾 1
163	162	oveq2i	⊢ ( ; ; 𝑅 𝑆 𝑇 + ( 1 + ( ; ; 𝐼 𝐽 𝐾 · ; 1 0 ) ) ) = ( ; ; 𝑅 𝑆 𝑇 + ; ; ; 𝐼 𝐽 𝐾 1 )
164	150 151 153	addassi	⊢ ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) + ( ; ; 𝐼 𝐽 𝐾 · ; 1 0 ) ) = ( ; ; 𝑅 𝑆 𝑇 + ( 1 + ( ; ; 𝐼 𝐽 𝐾 · ; 1 0 ) ) )
165		1nn0	⊢ 1 ∈ ℕ0
166	144 165	deccl	⊢ ; ; ; 𝐼 𝐽 𝐾 1 ∈ ℕ0
167	166	nn0cni	⊢ ; ; ; 𝐼 𝐽 𝐾 1 ∈ ℂ
168	167 150	addcomi	⊢ ( ; ; ; 𝐼 𝐽 𝐾 1 + ; ; 𝑅 𝑆 𝑇 ) = ( ; ; 𝑅 𝑆 𝑇 + ; ; ; 𝐼 𝐽 𝐾 1 )
169	163 164 168	3eqtr4i	⊢ ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) + ( ; ; 𝐼 𝐽 𝐾 · ; 1 0 ) ) = ( ; ; ; 𝐼 𝐽 𝐾 1 + ; ; 𝑅 𝑆 𝑇 )
170	169 32	eqtri	⊢ ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) + ( ; ; 𝐼 𝐽 𝐾 · ; 1 0 ) ) = ; ; ; 𝑊 𝑋 𝑌 𝑍
171	152 153 170	mvlladdi	⊢ ( ; ; 𝐼 𝐽 𝐾 · ; 1 0 ) = ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) )
172	171	oveq1i	⊢ ( ( ; ; 𝐼 𝐽 𝐾 · ; 1 0 ) · ; 1 0 ) = ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ; 1 0 )
173	147 172	eqtri	⊢ ( ; ; 𝐼 𝐽 𝐾 · ( ; 1 0 ↑ 2 ) ) = ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ; 1 0 )
174	173	oveq1i	⊢ ( ( ; ; 𝐼 𝐽 𝐾 · ( ; 1 0 ↑ 2 ) ) + ; ; 𝐿 𝑀 𝑁 ) = ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ; 1 0 ) + ; ; 𝐿 𝑀 𝑁 )
175		eqid	⊢ ( ( ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ; 1 0 ) + ; ; 𝐿 𝑀 𝑁 ) · ( ; 1 0 ↑ 2 ) ) + ; ; 𝑂 𝑃 𝑄 ) = ( ( ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ; 1 0 ) + ; ; 𝐿 𝑀 𝑁 ) · ( ; 1 0 ↑ 2 ) ) + ; ; 𝑂 𝑃 𝑄 )
176	34 35 36 37 39 40 65 88 126 134 141 174 175	karatsuba	⊢ ( ; ; ; 𝐴 𝐵 𝐶 𝐷 · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) = ( ( ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ; 1 0 ) + ; ; 𝐿 𝑀 𝑁 ) · ( ; 1 0 ↑ 2 ) ) + ; ; 𝑂 𝑃 𝑄 )
177	22 23	deccl	⊢ ; 𝑊 𝑋 ∈ ℕ0
178	177 24	deccl	⊢ ; ; 𝑊 𝑋 𝑌 ∈ ℕ0
179	178 25	deccl	⊢ ; ; ; 𝑊 𝑋 𝑌 𝑍 ∈ ℕ0
180	179	nn0cni	⊢ ; ; ; 𝑊 𝑋 𝑌 𝑍 ∈ ℂ
181	115 114	deccl	⊢ ; ; ; 1 0 0 0 ∈ ℕ0
182	181	nn0cni	⊢ ; ; ; 1 0 0 0 ∈ ℂ
183	180 182	mulcli	⊢ ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) ∈ ℂ
184	152 182	mulcli	⊢ ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) ∈ ℂ
185	183 184	subcli	⊢ ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) − ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) ) ∈ ℂ
186	39	nn0cni	⊢ ; ; 𝐿 𝑀 𝑁 ∈ ℂ
187	116 186	mulcli	⊢ ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) ∈ ℂ
188	15 16 78	dfdec100	⊢ ; ; 𝑂 𝑃 𝑄 = ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 )
189	83 17	deccl	⊢ ; ; 𝑂 𝑃 𝑄 ∈ ℕ0
190	189	nn0cni	⊢ ; ; 𝑂 𝑃 𝑄 ∈ ℂ
191	188 190	eqeltrri	⊢ ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ∈ ℂ
192	185 187 191	addassi	⊢ ( ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) − ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) ) + ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) = ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) − ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) ) + ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) )
193	46	sqcli	⊢ ( ; 1 0 ↑ 2 ) ∈ ℂ
194	145 193	mulcli	⊢ ( ; ; 𝐼 𝐽 𝐾 · ( ; 1 0 ↑ 2 ) ) ∈ ℂ
195	173 194	eqeltrri	⊢ ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ; 1 0 ) ∈ ℂ
196	195 186 116	adddiri	⊢ ( ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ; 1 0 ) + ; ; 𝐿 𝑀 𝑁 ) · ; ; 1 0 0 ) = ( ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ; 1 0 ) · ; ; 1 0 0 ) + ( ; ; 𝐿 𝑀 𝑁 · ; ; 1 0 0 ) )
197	127	oveq2i	⊢ ( ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ; 1 0 ) + ; ; 𝐿 𝑀 𝑁 ) · ( ; 1 0 ↑ 2 ) ) = ( ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ; 1 0 ) + ; ; 𝐿 𝑀 𝑁 ) · ; ; 1 0 0 )
198	180 152	subcli	⊢ ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) ∈ ℂ
199	198 46 116	mulassi	⊢ ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ; 1 0 ) · ; ; 1 0 0 ) = ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ( ; 1 0 · ; ; 1 0 0 ) )
200	115	dec0u	⊢ ( ; 1 0 · ; ; 1 0 0 ) = ; ; ; 1 0 0 0
201	200	oveq2i	⊢ ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ( ; 1 0 · ; ; 1 0 0 ) ) = ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ; ; ; 1 0 0 0 )
202	180 152 182	subdiri	⊢ ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ; ; ; 1 0 0 0 ) = ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) − ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) )
203	199 201 202	3eqtrri	⊢ ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) − ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) ) = ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ; 1 0 ) · ; ; 1 0 0 )
204	116 186	mulcomi	⊢ ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) = ( ; ; 𝐿 𝑀 𝑁 · ; ; 1 0 0 )
205	203 204	oveq12i	⊢ ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) − ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) ) + ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) ) = ( ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ; 1 0 ) · ; ; 1 0 0 ) + ( ; ; 𝐿 𝑀 𝑁 · ; ; 1 0 0 ) )
206	196 197 205	3eqtr4i	⊢ ( ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ; 1 0 ) + ; ; 𝐿 𝑀 𝑁 ) · ( ; 1 0 ↑ 2 ) ) = ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) − ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) ) + ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) )
207	206 188	oveq12i	⊢ ( ( ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ; 1 0 ) + ; ; 𝐿 𝑀 𝑁 ) · ( ; 1 0 ↑ 2 ) ) + ; ; 𝑂 𝑃 𝑄 ) = ( ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) − ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) ) + ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) )
208	187 191	addcli	⊢ ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) ∈ ℂ
209		subsub	⊢ ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) ∈ ℂ ∧ ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) ∈ ℂ ∧ ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) ∈ ℂ ) → ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) − ( ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) − ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) ) ) = ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) − ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) ) + ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) ) )
210	183 184 208 209	mp3an	⊢ ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) − ( ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) − ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) ) ) = ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) − ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) ) + ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) )
211	192 207 210	3eqtr4ri	⊢ ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) − ( ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) − ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) ) ) = ( ( ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 − ( ; ; 𝑅 𝑆 𝑇 + 1 ) ) · ; 1 0 ) + ; ; 𝐿 𝑀 𝑁 ) · ( ; 1 0 ↑ 2 ) ) + ; ; 𝑂 𝑃 𝑄 )
212	176 211	eqtr4i	⊢ ( ; ; ; 𝐴 𝐵 𝐶 𝐷 · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) = ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) − ( ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) − ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) ) )
213	179	nn0rei	⊢ ; ; ; 𝑊 𝑋 𝑌 𝑍 ∈ ℝ
214	181	nn0rei	⊢ ; ; ; 1 0 0 0 ∈ ℝ
215	213 214	remulcli	⊢ ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) ∈ ℝ
216	149	nn0rei	⊢ ; ; 𝑅 𝑆 𝑇 ∈ ℝ
217		1re	⊢ 1 ∈ ℝ
218	216 217	readdcli	⊢ ( ; ; 𝑅 𝑆 𝑇 + 1 ) ∈ ℝ
219	218 214	remulcli	⊢ ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) ∈ ℝ
220	115	nn0rei	⊢ ; ; 1 0 0 ∈ ℝ
221	39	nn0rei	⊢ ; ; 𝐿 𝑀 𝑁 ∈ ℝ
222	220 221	remulcli	⊢ ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) ∈ ℝ
223	15	nn0rei	⊢ 𝑂 ∈ ℝ
224	220 223	remulcli	⊢ ( ; ; 1 0 0 · 𝑂 ) ∈ ℝ
225	16 17	deccl	⊢ ; 𝑃 𝑄 ∈ ℕ0
226	225	nn0rei	⊢ ; 𝑃 𝑄 ∈ ℝ
227	224 226	readdcli	⊢ ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ∈ ℝ
228	222 227	readdcli	⊢ ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) ∈ ℝ
229	219 228	resubcli	⊢ ( ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) − ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) ) ∈ ℝ
230	224	recni	⊢ ( ; ; 1 0 0 · 𝑂 ) ∈ ℂ
231	226	recni	⊢ ; 𝑃 𝑄 ∈ ℂ
232	187 230 231	addassi	⊢ ( ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ; ; 1 0 0 · 𝑂 ) ) + ; 𝑃 𝑄 ) = ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) )
233	223	recni	⊢ 𝑂 ∈ ℂ
234	116 186 233	adddii	⊢ ( ; ; 1 0 0 · ( ; ; 𝐿 𝑀 𝑁 + 𝑂 ) ) = ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ; ; 1 0 0 · 𝑂 ) )
235	29	oveq2i	⊢ ( ; ; 1 0 0 · ( ; ; 𝐿 𝑀 𝑁 + 𝑂 ) ) = ( ; ; 1 0 0 · ; ; ; 𝑅 𝑆 𝑇 𝑈 )
236	234 235	eqtr3i	⊢ ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ; ; 1 0 0 · 𝑂 ) ) = ( ; ; 1 0 0 · ; ; ; 𝑅 𝑆 𝑇 𝑈 )
237	236	oveq1i	⊢ ( ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ; ; 1 0 0 · 𝑂 ) ) + ; 𝑃 𝑄 ) = ( ( ; ; 1 0 0 · ; ; ; 𝑅 𝑆 𝑇 𝑈 ) + ; 𝑃 𝑄 )
238	232 237	eqtr3i	⊢ ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) = ( ( ; ; 1 0 0 · ; ; ; 𝑅 𝑆 𝑇 𝑈 ) + ; 𝑃 𝑄 )
239	21 101 16 114 17 114 26 27 28	3decltc	⊢ ; ; 𝑈 𝑃 𝑄 < ; ; ; 1 0 0 0
240	21 16	deccl	⊢ ; 𝑈 𝑃 ∈ ℕ0
241	240 17	deccl	⊢ ; ; 𝑈 𝑃 𝑄 ∈ ℕ0
242	241	nn0rei	⊢ ; ; 𝑈 𝑃 𝑄 ∈ ℝ
243	216 214	remulcli	⊢ ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 ) ∈ ℝ
244	242 214 243	ltadd2i	⊢ ( ; ; 𝑈 𝑃 𝑄 < ; ; ; 1 0 0 0 ↔ ( ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 ) + ; ; 𝑈 𝑃 𝑄 ) < ( ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 ) + ; ; ; 1 0 0 0 ) )
245	239 244	mpbi	⊢ ( ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 ) + ; ; 𝑈 𝑃 𝑄 ) < ( ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 ) + ; ; ; 1 0 0 0 )
246	150 182	mulcli	⊢ ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 ) ∈ ℂ
247	21	nn0cni	⊢ 𝑈 ∈ ℂ
248	116 247	mulcli	⊢ ( ; ; 1 0 0 · 𝑈 ) ∈ ℂ
249	246 248 231	addassi	⊢ ( ( ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 ) + ( ; ; 1 0 0 · 𝑈 ) ) + ; 𝑃 𝑄 ) = ( ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 ) + ( ( ; ; 1 0 0 · 𝑈 ) + ; 𝑃 𝑄 ) )
250		dfdec10	⊢ ; ; ; 𝑅 𝑆 𝑇 𝑈 = ( ( ; 1 0 · ; ; 𝑅 𝑆 𝑇 ) + 𝑈 )
251	250	oveq2i	⊢ ( ; ; 1 0 0 · ; ; ; 𝑅 𝑆 𝑇 𝑈 ) = ( ; ; 1 0 0 · ( ( ; 1 0 · ; ; 𝑅 𝑆 𝑇 ) + 𝑈 ) )
252	46 150	mulcli	⊢ ( ; 1 0 · ; ; 𝑅 𝑆 𝑇 ) ∈ ℂ
253	116 252 247	adddii	⊢ ( ; ; 1 0 0 · ( ( ; 1 0 · ; ; 𝑅 𝑆 𝑇 ) + 𝑈 ) ) = ( ( ; ; 1 0 0 · ( ; 1 0 · ; ; 𝑅 𝑆 𝑇 ) ) + ( ; ; 1 0 0 · 𝑈 ) )
254	150 182	mulcomi	⊢ ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 ) = ( ; ; ; 1 0 0 0 · ; ; 𝑅 𝑆 𝑇 )
255	46 116	mulcomi	⊢ ( ; 1 0 · ; ; 1 0 0 ) = ( ; ; 1 0 0 · ; 1 0 )
256	255 200	eqtr3i	⊢ ( ; ; 1 0 0 · ; 1 0 ) = ; ; ; 1 0 0 0
257	256	oveq1i	⊢ ( ( ; ; 1 0 0 · ; 1 0 ) · ; ; 𝑅 𝑆 𝑇 ) = ( ; ; ; 1 0 0 0 · ; ; 𝑅 𝑆 𝑇 )
258	116 46 150	mulassi	⊢ ( ( ; ; 1 0 0 · ; 1 0 ) · ; ; 𝑅 𝑆 𝑇 ) = ( ; ; 1 0 0 · ( ; 1 0 · ; ; 𝑅 𝑆 𝑇 ) )
259	254 257 258	3eqtr2ri	⊢ ( ; ; 1 0 0 · ( ; 1 0 · ; ; 𝑅 𝑆 𝑇 ) ) = ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 )
260	259	oveq1i	⊢ ( ( ; ; 1 0 0 · ( ; 1 0 · ; ; 𝑅 𝑆 𝑇 ) ) + ( ; ; 1 0 0 · 𝑈 ) ) = ( ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 ) + ( ; ; 1 0 0 · 𝑈 ) )
261	251 253 260	3eqtri	⊢ ( ; ; 1 0 0 · ; ; ; 𝑅 𝑆 𝑇 𝑈 ) = ( ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 ) + ( ; ; 1 0 0 · 𝑈 ) )
262	261	oveq1i	⊢ ( ( ; ; 1 0 0 · ; ; ; 𝑅 𝑆 𝑇 𝑈 ) + ; 𝑃 𝑄 ) = ( ( ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 ) + ( ; ; 1 0 0 · 𝑈 ) ) + ; 𝑃 𝑄 )
263	21 16 78	dfdec100	⊢ ; ; 𝑈 𝑃 𝑄 = ( ( ; ; 1 0 0 · 𝑈 ) + ; 𝑃 𝑄 )
264	263	oveq2i	⊢ ( ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 ) + ; ; 𝑈 𝑃 𝑄 ) = ( ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 ) + ( ( ; ; 1 0 0 · 𝑈 ) + ; 𝑃 𝑄 ) )
265	249 262 264	3eqtr4i	⊢ ( ( ; ; 1 0 0 · ; ; ; 𝑅 𝑆 𝑇 𝑈 ) + ; 𝑃 𝑄 ) = ( ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 ) + ; ; 𝑈 𝑃 𝑄 )
266	150 151 182	adddiri	⊢ ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) = ( ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 ) + ( 1 · ; ; ; 1 0 0 0 ) )
267	182	mullidi	⊢ ( 1 · ; ; ; 1 0 0 0 ) = ; ; ; 1 0 0 0
268	267	oveq2i	⊢ ( ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 ) + ( 1 · ; ; ; 1 0 0 0 ) ) = ( ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 ) + ; ; ; 1 0 0 0 )
269	266 268	eqtri	⊢ ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) = ( ( ; ; 𝑅 𝑆 𝑇 · ; ; ; 1 0 0 0 ) + ; ; ; 1 0 0 0 )
270	245 265 269	3brtr4i	⊢ ( ( ; ; 1 0 0 · ; ; ; 𝑅 𝑆 𝑇 𝑈 ) + ; 𝑃 𝑄 ) < ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 )
271	238 270	eqbrtri	⊢ ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) < ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 )
272	228 219	posdifi	⊢ ( ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) < ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) ↔ 0 < ( ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) − ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) ) )
273	271 272	mpbi	⊢ 0 < ( ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) − ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) )
274		elrp	⊢ ( ( ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) − ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) ) ∈ ℝ+ ↔ ( ( ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) − ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) ) ∈ ℝ ∧ 0 < ( ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) − ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) ) ) )
275	229 273 274	mpbir2an	⊢ ( ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) − ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) ) ∈ ℝ+
276		ltsubrp	⊢ ( ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) ∈ ℝ ∧ ( ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) − ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) ) ∈ ℝ+ ) → ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) − ( ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) − ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) ) ) < ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) )
277	215 275 276	mp2an	⊢ ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) − ( ( ( ; ; 𝑅 𝑆 𝑇 + 1 ) · ; ; ; 1 0 0 0 ) − ( ( ; ; 1 0 0 · ; ; 𝐿 𝑀 𝑁 ) + ( ( ; ; 1 0 0 · 𝑂 ) + ; 𝑃 𝑄 ) ) ) ) < ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 )
278	212 277	eqbrtri	⊢ ( ; ; ; 𝐴 𝐵 𝐶 𝐷 · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) < ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 )
279	34 3	deccl	⊢ ; ; 𝐴 𝐵 𝐶 ∈ ℕ0
280	279 4	deccl	⊢ ; ; ; 𝐴 𝐵 𝐶 𝐷 ∈ ℕ0
281	280	nn0rei	⊢ ; ; ; 𝐴 𝐵 𝐶 𝐷 ∈ ℝ
282	36 6	deccl	⊢ ; ; 𝐸 𝐹 𝐺 ∈ ℕ0
283	282 10	deccl	⊢ ; ; ; 𝐸 𝐹 𝐺 𝐻 ∈ ℕ0
284	283	nn0rei	⊢ ; ; ; 𝐸 𝐹 𝐺 𝐻 ∈ ℝ
285	281 284	remulcli	⊢ ( ; ; ; 𝐴 𝐵 𝐶 𝐷 · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) ∈ ℝ
286	45	decnncl2	⊢ ; ; 1 0 0 ∈ ℕ
287	286	decnncl2	⊢ ; ; ; 1 0 0 0 ∈ ℕ
288	287	nngt0i	⊢ 0 < ; ; ; 1 0 0 0
289	214 288	pm3.2i	⊢ ( ; ; ; 1 0 0 0 ∈ ℝ ∧ 0 < ; ; ; 1 0 0 0 )
290		ltdiv1	⊢ ( ( ( ; ; ; 𝐴 𝐵 𝐶 𝐷 · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) ∈ ℝ ∧ ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) ∈ ℝ ∧ ( ; ; ; 1 0 0 0 ∈ ℝ ∧ 0 < ; ; ; 1 0 0 0 ) ) → ( ( ; ; ; 𝐴 𝐵 𝐶 𝐷 · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) < ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) ↔ ( ( ; ; ; 𝐴 𝐵 𝐶 𝐷 · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) / ; ; ; 1 0 0 0 ) < ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) ) )
291	285 215 289 290	mp3an	⊢ ( ( ; ; ; 𝐴 𝐵 𝐶 𝐷 · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) < ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) ↔ ( ( ; ; ; 𝐴 𝐵 𝐶 𝐷 · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) / ; ; ; 1 0 0 0 ) < ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) )
292	278 291	mpbi	⊢ ( ( ; ; ; 𝐴 𝐵 𝐶 𝐷 · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) / ; ; ; 1 0 0 0 ) < ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 )
293	280	nn0cni	⊢ ; ; ; 𝐴 𝐵 𝐶 𝐷 ∈ ℂ
294	283	nn0cni	⊢ ; ; ; 𝐸 𝐹 𝐺 𝐻 ∈ ℂ
295	214 288	gt0ne0ii	⊢ ; ; ; 1 0 0 0 ≠ 0
296	293 294 182 295	div23i	⊢ ( ( ; ; ; 𝐴 𝐵 𝐶 𝐷 · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) / ; ; ; 1 0 0 0 ) = ( ( ; ; ; 𝐴 𝐵 𝐶 𝐷 / ; ; ; 1 0 0 0 ) · ; ; ; 𝐸 𝐹 𝐺 𝐻 )
297	1 2 3 66	dpmul1000	⊢ ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ; ; ; 1 0 0 0 ) = ; ; ; 𝐴 𝐵 𝐶 𝐷
298	297	oveq1i	⊢ ( ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( ; ; ; 𝐴 𝐵 𝐶 𝐷 / ; ; ; 1 0 0 0 )
299	3	nn0rei	⊢ 𝐶 ∈ ℝ
300		dp2cl	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → _ 𝐶 𝐷 ∈ ℝ )
301	299 66 300	mp2an	⊢ _ 𝐶 𝐷 ∈ ℝ
302		dp2cl	⊢ ( ( 𝐵 ∈ ℝ ∧ _ 𝐶 𝐷 ∈ ℝ ) → _ 𝐵 _ 𝐶 𝐷 ∈ ℝ )
303	41 301 302	mp2an	⊢ _ 𝐵 _ 𝐶 𝐷 ∈ ℝ
304		dpcl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ _ 𝐵 _ 𝐶 𝐷 ∈ ℝ ) → ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) ∈ ℝ )
305	1 303 304	mp2an	⊢ ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) ∈ ℝ
306	305	recni	⊢ ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) ∈ ℂ
307	306 182 295	divcan4i	⊢ ( ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 )
308	298 307	eqtr3i	⊢ ( ; ; ; 𝐴 𝐵 𝐶 𝐷 / ; ; ; 1 0 0 0 ) = ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 )
309	308	oveq1i	⊢ ( ( ; ; ; 𝐴 𝐵 𝐶 𝐷 / ; ; ; 1 0 0 0 ) · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) = ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ; ; ; 𝐸 𝐹 𝐺 𝐻 )
310	296 309	eqtri	⊢ ( ( ; ; ; 𝐴 𝐵 𝐶 𝐷 · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) / ; ; ; 1 0 0 0 ) = ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ; ; ; 𝐸 𝐹 𝐺 𝐻 )
311	180 182 295	divcan4i	⊢ ( ( ; ; ; 𝑊 𝑋 𝑌 𝑍 · ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ; ; ; 𝑊 𝑋 𝑌 𝑍
312	292 310 311	3brtr3i	⊢ ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) < ; ; ; 𝑊 𝑋 𝑌 𝑍
313	305 284	remulcli	⊢ ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) ∈ ℝ
314		ltdiv1	⊢ ( ( ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) ∈ ℝ ∧ ; ; ; 𝑊 𝑋 𝑌 𝑍 ∈ ℝ ∧ ( ; ; ; 1 0 0 0 ∈ ℝ ∧ 0 < ; ; ; 1 0 0 0 ) ) → ( ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) < ; ; ; 𝑊 𝑋 𝑌 𝑍 ↔ ( ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) / ; ; ; 1 0 0 0 ) < ( ; ; ; 𝑊 𝑋 𝑌 𝑍 / ; ; ; 1 0 0 0 ) ) )
315	313 213 289 314	mp3an	⊢ ( ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) < ; ; ; 𝑊 𝑋 𝑌 𝑍 ↔ ( ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) / ; ; ; 1 0 0 0 ) < ( ; ; ; 𝑊 𝑋 𝑌 𝑍 / ; ; ; 1 0 0 0 ) )
316	312 315	mpbi	⊢ ( ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) / ; ; ; 1 0 0 0 ) < ( ; ; ; 𝑊 𝑋 𝑌 𝑍 / ; ; ; 1 0 0 0 )
317	306 294 182 295	divassi	⊢ ( ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) / ; ; ; 1 0 0 0 ) = ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ( ; ; ; 𝐸 𝐹 𝐺 𝐻 / ; ; ; 1 0 0 0 ) )
318	5 9 6 70	dpmul1000	⊢ ( ( 𝐸 . _ 𝐹 _ 𝐺 𝐻 ) · ; ; ; 1 0 0 0 ) = ; ; ; 𝐸 𝐹 𝐺 𝐻
319	318	oveq1i	⊢ ( ( ( 𝐸 . _ 𝐹 _ 𝐺 𝐻 ) · ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( ; ; ; 𝐸 𝐹 𝐺 𝐻 / ; ; ; 1 0 0 0 )
320	6	nn0rei	⊢ 𝐺 ∈ ℝ
321		dp2cl	⊢ ( ( 𝐺 ∈ ℝ ∧ 𝐻 ∈ ℝ ) → _ 𝐺 𝐻 ∈ ℝ )
322	320 70 321	mp2an	⊢ _ 𝐺 𝐻 ∈ ℝ
323		dp2cl	⊢ ( ( 𝐹 ∈ ℝ ∧ _ 𝐺 𝐻 ∈ ℝ ) → _ 𝐹 _ 𝐺 𝐻 ∈ ℝ )
324	47 322 323	mp2an	⊢ _ 𝐹 _ 𝐺 𝐻 ∈ ℝ
325		dpcl	⊢ ( ( 𝐸 ∈ ℕ0 ∧ _ 𝐹 _ 𝐺 𝐻 ∈ ℝ ) → ( 𝐸 . _ 𝐹 _ 𝐺 𝐻 ) ∈ ℝ )
326	5 324 325	mp2an	⊢ ( 𝐸 . _ 𝐹 _ 𝐺 𝐻 ) ∈ ℝ
327	326	recni	⊢ ( 𝐸 . _ 𝐹 _ 𝐺 𝐻 ) ∈ ℂ
328	327 182 295	divcan4i	⊢ ( ( ( 𝐸 . _ 𝐹 _ 𝐺 𝐻 ) · ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( 𝐸 . _ 𝐹 _ 𝐺 𝐻 )
329	319 328	eqtr3i	⊢ ( ; ; ; 𝐸 𝐹 𝐺 𝐻 / ; ; ; 1 0 0 0 ) = ( 𝐸 . _ 𝐹 _ 𝐺 𝐻 )
330	329	oveq2i	⊢ ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ( ; ; ; 𝐸 𝐹 𝐺 𝐻 / ; ; ; 1 0 0 0 ) ) = ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ( 𝐸 . _ 𝐹 _ 𝐺 𝐻 ) )
331	317 330	eqtri	⊢ ( ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ; ; ; 𝐸 𝐹 𝐺 𝐻 ) / ; ; ; 1 0 0 0 ) = ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ( 𝐸 . _ 𝐹 _ 𝐺 𝐻 ) )
332	25	nn0rei	⊢ 𝑍 ∈ ℝ
333	22 23 24 332	dpmul1000	⊢ ( ( 𝑊 . _ 𝑋 _ 𝑌 𝑍 ) · ; ; ; 1 0 0 0 ) = ; ; ; 𝑊 𝑋 𝑌 𝑍
334	333	oveq1i	⊢ ( ( ( 𝑊 . _ 𝑋 _ 𝑌 𝑍 ) · ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( ; ; ; 𝑊 𝑋 𝑌 𝑍 / ; ; ; 1 0 0 0 )
335	23	nn0rei	⊢ 𝑋 ∈ ℝ
336	24	nn0rei	⊢ 𝑌 ∈ ℝ
337		dp2cl	⊢ ( ( 𝑌 ∈ ℝ ∧ 𝑍 ∈ ℝ ) → _ 𝑌 𝑍 ∈ ℝ )
338	336 332 337	mp2an	⊢ _ 𝑌 𝑍 ∈ ℝ
339		dp2cl	⊢ ( ( 𝑋 ∈ ℝ ∧ _ 𝑌 𝑍 ∈ ℝ ) → _ 𝑋 _ 𝑌 𝑍 ∈ ℝ )
340	335 338 339	mp2an	⊢ _ 𝑋 _ 𝑌 𝑍 ∈ ℝ
341		dpcl	⊢ ( ( 𝑊 ∈ ℕ0 ∧ _ 𝑋 _ 𝑌 𝑍 ∈ ℝ ) → ( 𝑊 . _ 𝑋 _ 𝑌 𝑍 ) ∈ ℝ )
342	22 340 341	mp2an	⊢ ( 𝑊 . _ 𝑋 _ 𝑌 𝑍 ) ∈ ℝ
343	342	recni	⊢ ( 𝑊 . _ 𝑋 _ 𝑌 𝑍 ) ∈ ℂ
344	343 182 295	divcan4i	⊢ ( ( ( 𝑊 . _ 𝑋 _ 𝑌 𝑍 ) · ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( 𝑊 . _ 𝑋 _ 𝑌 𝑍 )
345	334 344	eqtr3i	⊢ ( ; ; ; 𝑊 𝑋 𝑌 𝑍 / ; ; ; 1 0 0 0 ) = ( 𝑊 . _ 𝑋 _ 𝑌 𝑍 )
346	316 331 345	3brtr3i	⊢ ( ( 𝐴 . _ 𝐵 _ 𝐶 𝐷 ) · ( 𝐸 . _ 𝐹 _ 𝐺 𝐻 ) ) < ( 𝑊 . _ 𝑋 _ 𝑌 𝑍 )