dpmul4 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dpmul4		Structured version Visualization version GIF version

Theorem dpmul4 32896

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

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

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2108 class class class wbr 5143 (class class class)co 7431 ℂcc 11153 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 · cmul 11160 < clt 11295 − cmin 11492 / cdiv 11920 2c2 12321 ℕ₀cn0 12526 cdc 12733 ℝ⁺crp 13034 ↑cexp 14102 cdp2 32853 .cdp 32870

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-er 8745 df-en 8986 df-dom 8987 df-sdom 8988 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-4 12331 df-5 12332 df-6 12333 df-7 12334 df-8 12335 df-9 12336 df-n0 12527 df-z 12614 df-dec 12734 df-uz 12879 df-rp 13035 df-seq 14043 df-exp 14103 df-dp2 32854 df-dp 32871

This theorem is referenced by: hgt750lem2 34667

W3C validator