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 30585

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

Colors of variables: wff setvar class

Syntax hints: ↔ wb 208 ∧ wa 398 = wceq 1533 ∈ wcel 2110 class class class wbr 5058 (class class class)co 7150 ℂcc 10529 ℝcr 10530 0cc0 10531 1c1 10532 + caddc 10534 · cmul 10536 < clt 10669 − cmin 10864 / cdiv 11291 2c2 11686 ℕ₀cn0 11891 cdc 12092 ℝ⁺crp 12383 ↑cexp 13423 cdp2 30542 .cdp 30559

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-tp 4565 df-op 4567 df-uni 4832 df-iun 4913 df-br 5059 df-opab 5121 df-mpt 5139 df-tr 5165 df-id 5454 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-we 5510 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-pred 6142 df-ord 6188 df-on 6189 df-lim 6190 df-suc 6191 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7575 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-er 8283 df-en 8504 df-dom 8505 df-sdom 8506 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-div 11292 df-nn 11633 df-2 11694 df-3 11695 df-4 11696 df-5 11697 df-6 11698 df-7 11699 df-8 11700 df-9 11701 df-n0 11892 df-z 11976 df-dec 12093 df-uz 12238 df-rp 12384 df-seq 13364 df-exp 13424 df-dp2 30543 df-dp 30560

This theorem is referenced by: hgt750lem2 31918

W3C validator