Theorem dpmul4 33146

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

Hypotheses

Ref	Expression
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	⊢ 𝑈 < ;10
dpmul4.b	⊢ 𝑃 < ;10
dpmul4.c	⊢ 𝑄 < ;10
dpmul4.1	⊢ (;;𝐿𝑀𝑁 + 𝑂) = ;;;𝑅𝑆𝑇𝑈
dpmul4.2	⊢ ((𝐴.𝐵) · (𝐸.𝐹)) = (𝐼._𝐽𝐾)
dpmul4.3	⊢ ((𝐶.𝐷) · (𝐺.𝐻)) = (𝑂._𝑃𝑄)
dpmul4.4	⊢ (;;;𝐼𝐽𝐾1 + ;;𝑅𝑆𝑇) = ;;;𝑊𝑋𝑌𝑍
dpmul4.5	⊢ (((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) = (((𝐼._𝐽𝐾) + (𝐿._𝑀𝑁)) + (𝑂._𝑃𝑄))

Assertion

Ref	Expression
dpmul4	⊢ ((𝐴._𝐵_𝐶𝐷) · (𝐸._𝐹_𝐺𝐻)) < (𝑊._𝑋_𝑌𝑍)

Proof of Theorem dpmul4

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

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1563   ∈ wcel 2145   class class class wbr 5105  (class class class)co 7400  ℂcc 11086  ℝcr 11087  0cc0 11088  1c1 11089   + caddc 11091   · cmul 11093   < clt 11231   − cmin 11429   / cdiv 11859  2c2 12286  ℕ₀cn0 12495  ;cdc 12702  ℝ⁺crp 13007  ↑cexp 14088  _cdp2 33103  .cdp 33120

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-cnex 11144  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7851  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-div 11860  df-nn 12225  df-2 12294  df-3 12295  df-4 12296  df-5 12297  df-6 12298  df-7 12299  df-8 12300  df-9 12301  df-n0 12496  df-z 12583  df-dec 12703  df-uz 12854  df-rp 13008  df-seq 14029  df-exp 14089  df-dp2 33104  df-dp 33121

This theorem is referenced by:  hgt750lem2  34956