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 31188

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

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 ∧ wa 396 = wceq 1539 ∈ wcel 2106 class class class wbr 5074 (class class class)co 7275 ℂcc 10869 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 · cmul 10876 < clt 11009 − cmin 11205 / cdiv 11632 2c2 12028 ℕ₀cn0 12233 cdc 12437 ℝ⁺crp 12730 ↑cexp 13782 cdp2 31145 .cdp 31162

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-er 8498 df-en 8734 df-dom 8735 df-sdom 8736 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-4 12038 df-5 12039 df-6 12040 df-7 12041 df-8 12042 df-9 12043 df-n0 12234 df-z 12320 df-dec 12438 df-uz 12583 df-rp 12731 df-seq 13722 df-exp 13783 df-dp2 31146 df-dp 31163

This theorem is referenced by: hgt750lem2 32632

W3C validator