hgt750lem2

Description: Decimal multiplication galore! (Contributed by Thierry Arnoux, 26-Dec-2021)

		Ref	Expression
	Assertion	hgt750lem2	$⊢ 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 < 7.348$

Proof

Step	Hyp	Ref	Expression
1		1nn0	$⊢ 1 \in ℕ_{0}$
2		0re	$⊢ 0 \in ℝ$
3		7re	$⊢ 7 \in ℝ$
4		9re	$⊢ 9 \in ℝ$
5		5re	$⊢ 5 \in ℝ$
6	5 5	pm3.2i	$⊢ (5 \in ℝ \land 5 \in ℝ)$
7		dp2cl	$⊢ (5 \in ℝ \land 5 \in ℝ) \to 55 \in ℝ$
8	6 7	ax-mp	$⊢ 55 \in ℝ$
9	4 8	pm3.2i	$⊢ (9 \in ℝ \land 55 \in ℝ)$
10		dp2cl	$⊢ (9 \in ℝ \land 55 \in ℝ) \to 955 \in ℝ$
11	9 10	ax-mp	$⊢ 955 \in ℝ$
12	4 11	pm3.2i	$⊢ (9 \in ℝ \land 955 \in ℝ)$
13		dp2cl	$⊢ (9 \in ℝ \land 955 \in ℝ) \to 9955 \in ℝ$
14	12 13	ax-mp	$⊢ 9955 \in ℝ$
15	3 14	pm3.2i	$⊢ (7 \in ℝ \land 9955 \in ℝ)$
16		dp2cl	$⊢ (7 \in ℝ \land 9955 \in ℝ) \to 79955 \in ℝ$
17	15 16	ax-mp	$⊢ 79955 \in ℝ$
18	2 17	pm3.2i	$⊢ (0 \in ℝ \land 79955 \in ℝ)$
19		dp2cl	$⊢ (0 \in ℝ \land 79955 \in ℝ) \to 079955 \in ℝ$
20	18 19	ax-mp	$⊢ 079955 \in ℝ$
21		dpcl	$⊢ (1 \in ℕ_{0} \land 079955 \in ℝ) \to 1.079955 \in ℝ$
22	1 20 21	mp2an	$⊢ 1.079955 \in ℝ$
23	22	resqcli	$⊢ {1.079955}^{2} \in ℝ$
24		4nn0	$⊢ 4 \in ℕ_{0}$
25		4nn	$⊢ 4 \in ℕ$
26		nnrp	$⊢ 4 \in ℕ \to 4 \in ℝ^{+}$
27	25 26	ax-mp	$⊢ 4 \in ℝ^{+}$
28	1 27	rpdp2cl	$⊢ 14 \in ℝ^{+}$
29	24 28	rpdp2cl	$⊢ 414 \in ℝ^{+}$
30	1 29	rpdpcl	$⊢ 1.414 \in ℝ^{+}$
31		rpre	$⊢ 1.414 \in ℝ^{+} \to 1.414 \in ℝ$
32	30 31	ax-mp	$⊢ 1.414 \in ℝ$
33	23 32	remulcli	$⊢ {1.079955}^{2} \cdot 1.414 \in ℝ$
34		6re	$⊢ 6 \in ℝ$
35		1re	$⊢ 1 \in ℝ$
36	5 35	pm3.2i	$⊢ (5 \in ℝ \land 1 \in ℝ)$
37		dp2cl	$⊢ (5 \in ℝ \land 1 \in ℝ) \to 51 \in ℝ$
38	36 37	ax-mp	$⊢ 51 \in ℝ$
39	34 38	pm3.2i	$⊢ (6 \in ℝ \land 51 \in ℝ)$
40		dp2cl	$⊢ (6 \in ℝ \land 51 \in ℝ) \to 651 \in ℝ$
41	39 40	ax-mp	$⊢ 651 \in ℝ$
42		dpcl	$⊢ (1 \in ℕ_{0} \land 651 \in ℝ) \to 1.651 \in ℝ$
43	1 41 42	mp2an	$⊢ 1.651 \in ℝ$
44	33 43	pm3.2i	$⊢ ({1.079955}^{2} \cdot 1.414 \in ℝ \land 1.651 \in ℝ)$
45	22	sqge0i	$⊢ 0 \leq {1.079955}^{2}$
46		rpgt0	$⊢ 1.414 \in ℝ^{+} \to 0 < 1.414$
47	30 46	ax-mp	$⊢ 0 < 1.414$
48	2 32 47	ltleii	$⊢ 0 \leq 1.414$
49	23 32	mulge0i	$⊢ (0 \leq {1.079955}^{2} \land 0 \leq 1.414) \to 0 \leq {1.079955}^{2} \cdot 1.414$
50	45 48 49	mp2an	$⊢ 0 \leq {1.079955}^{2} \cdot 1.414$
51		0nn0	$⊢ 0 \in ℕ_{0}$
52		7nn0	$⊢ 7 \in ℕ_{0}$
53		9nn0	$⊢ 9 \in ℕ_{0}$
54		5nn0	$⊢ 5 \in ℕ_{0}$
55		5nn	$⊢ 5 \in ℕ$
56		nnrp	$⊢ 5 \in ℕ \to 5 \in ℝ^{+}$
57	55 56	ax-mp	$⊢ 5 \in ℝ^{+}$
58	54 57	rpdp2cl	$⊢ 55 \in ℝ^{+}$
59	53 58	rpdp2cl	$⊢ 955 \in ℝ^{+}$
60	53 59	rpdp2cl	$⊢ 9955 \in ℝ^{+}$
61	52 60	rpdp2cl	$⊢ 79955 \in ℝ^{+}$
62	51 61	rpdp2cl	$⊢ 079955 \in ℝ^{+}$
63		8nn	$⊢ 8 \in ℕ$
64	63	rpdp2cl2	$⊢ 80 \in ℝ^{+}$
65	51 64	rpdp2cl	$⊢ 080 \in ℝ^{+}$
66		9lt10	$⊢ 9 < 10$
67		5lt10	$⊢ 5 < 10$
68	54 57 67 67	dp2lt10	$⊢ 55 < 10$
69	53 58 66 68	dp2lt10	$⊢ 955 < 10$
70	53 59 66 69	dp2lt10	$⊢ 9955 < 10$
71		7p1e8	$⊢ 7 + 1 = 8$
72	52 60 70 71	dp2ltsuc	$⊢ 79955 < 8$
73		8nn0	$⊢ 8 \in ℕ_{0}$
74	73	dp20u	$⊢ 80 = 8$
75	72 74	breqtrri	$⊢ 79955 < 80$
76	51 61 64 75	dp2lt	$⊢ 079955 < 080$
77	1 62 65 76	dplt	$⊢ 1.079955 < 1.080$
78	1 62	rpdpcl	$⊢ 1.079955 \in ℝ^{+}$
79		rpge0	$⊢ 1.079955 \in ℝ^{+} \to 0 \leq 1.079955$
80	78 79	ax-mp	$⊢ 0 \leq 1.079955$
81	1 65	rpdpcl	$⊢ 1.080 \in ℝ^{+}$
82		rpge0	$⊢ 1.080 \in ℝ^{+} \to 0 \leq 1.080$
83	81 82	ax-mp	$⊢ 0 \leq 1.080$
84		8re	$⊢ 8 \in ℝ$
85	84 2	pm3.2i	$⊢ (8 \in ℝ \land 0 \in ℝ)$
86		dp2cl	$⊢ (8 \in ℝ \land 0 \in ℝ) \to 80 \in ℝ$
87	85 86	ax-mp	$⊢ 80 \in ℝ$
88	2 87	pm3.2i	$⊢ (0 \in ℝ \land 80 \in ℝ)$
89		dp2cl	$⊢ (0 \in ℝ \land 80 \in ℝ) \to 080 \in ℝ$
90	88 89	ax-mp	$⊢ 080 \in ℝ$
91		dpcl	$⊢ (1 \in ℕ_{0} \land 080 \in ℝ) \to 1.080 \in ℝ$
92	1 90 91	mp2an	$⊢ 1.080 \in ℝ$
93	22 92	lt2sqi	$⊢ (0 \leq 1.079955 \land 0 \leq 1.080) \to (1.079955 < 1.080 \leftrightarrow {1.079955}^{2} < {1.080}^{2})$
94	80 83 93	mp2an	$⊢ 1.079955 < 1.080 \leftrightarrow {1.079955}^{2} < {1.080}^{2}$
95	77 94	mpbi	$⊢ {1.079955}^{2} < {1.080}^{2}$
96	92	recni	$⊢ 1.080 \in ℂ$
97	96	sqvali	$⊢ {1.080}^{2} = 1.080 \cdot 1.080$
98		6nn0	$⊢ 6 \in ℕ_{0}$
99	1 98	deccl	$⊢ 16 \in ℕ_{0}$
100	98 24	deccl	$⊢ 64 \in ℕ_{0}$
101		4lt10	$⊢ 4 < 10$
102		10pos	$⊢ 0 < 10$
103	99 51	deccl	$⊢ 160 \in ℕ_{0}$
104		eqid	$⊢ 1600 = 1600$
105		eqid	$⊢ 64 = 64$
106		eqid	$⊢ 160 = 160$
107	98	dec0h	$⊢ 6 = 06$
108	99	nn0cni	$⊢ 16 \in ℂ$
109	108	addridi	$⊢ 16 + 0 = 16$
110		6cn	$⊢ 6 \in ℂ$
111	110	addlidi	$⊢ 0 + 6 = 6$
112	99 51 51 98 106 107 109 111	decadd	$⊢ 160 + 6 = 166$
113		4cn	$⊢ 4 \in ℂ$
114	113	addlidi	$⊢ 0 + 4 = 4$
115	103 51 98 24 104 105 112 114	decadd	$⊢ 1600 + 64 = 1664$
116		1t1e1	$⊢ 1 \cdot 1 = 1$
117	1	dp0u	$⊢ 1.0 = 1$
118	117 117	oveq12i	$⊢ 1.0 \cdot 1.0 = 1 \cdot 1$
119	51	dp20u	$⊢ 00 = 0$
120	119	oveq2i	$⊢ 1.00 = 1.0$
121	120 117	eqtri	$⊢ 1.00 = 1$
122	116 118 121	3eqtr4i	$⊢ 1.0 \cdot 1.0 = 1.00$
123		8t8e64	$⊢ 8 \cdot 8 = 64$
124	73	dp0u	$⊢ 8.0 = 8$
125	124 124	oveq12i	$⊢ 8.0 \cdot 8.0 = 8 \cdot 8$
126	119	oveq2i	$⊢ 64.00 = 64.0$
127	100	dp0u	$⊢ 64.0 = 64$
128	126 127	eqtri	$⊢ 64.00 = 64$
129	123 125 128	3eqtr4i	$⊢ 8.0 \cdot 8.0 = 64.00$
130		10nn0	$⊢ 10 \in ℕ_{0}$
131	130 51	deccl	$⊢ 100 \in ℕ_{0}$
132		eqid	$⊢ 1001 = 1001$
133		eqid	$⊢ 166 = 166$
134		eqid	$⊢ 100 = 100$
135		eqid	$⊢ 16 = 16$
136		dec10p	$⊢ 10 + 1 = 11$
137	130 51 1 98 134 135 136 111	decadd	$⊢ 100 + 16 = 116$
138		ax-1cn	$⊢ 1 \in ℂ$
139	138 110	addcomi	$⊢ 1 + 6 = 6 + 1$
140		6p1e7	$⊢ 6 + 1 = 7$
141	139 140	eqtri	$⊢ 1 + 6 = 7$
142	131 1 99 98 132 133 137 141	decadd	$⊢ 1001 + 166 = 1167$
143		eqid	$⊢ 17 = 17$
144	141	oveq1i	$⊢ 1 + 6 + 1 = 7 + 1$
145	144 71	eqtri	$⊢ 1 + 6 + 1 = 8$
146		7p4e11	$⊢ 7 + 4 = 11$
147	1 52 98 24 143 105 145 1 146	decaddc	$⊢ 17 + 64 = 81$
148	119	oveq2i	$⊢ 16.00 = 16.0$
149	99	dp0u	$⊢ 16.0 = 16$
150	148 149	eqtri	$⊢ 16.00 = 16$
151	121 150	oveq12i	$⊢ 1.00 + 16.00 = 1 + 16$
152	1	dec0h	$⊢ 1 = 01$
153	138	addlidi	$⊢ 0 + 1 = 1$
154	51 1 1 98 152 135 153 141	decadd	$⊢ 1 + 16 = 17$
155	151 154	eqtri	$⊢ 1.00 + 16.00 = 17$
156	155 128	oveq12i	$⊢ 1.00 + 16.00 + 64.00 = 17 + 64$
157	117 124	oveq12i	$⊢ 1.0 + 8.0 = 1 + 8$
158		8cn	$⊢ 8 \in ℂ$
159	138 158	addcomi	$⊢ 1 + 8 = 8 + 1$
160		8p1e9	$⊢ 8 + 1 = 9$
161	157 159 160	3eqtri	$⊢ 1.0 + 8.0 = 9$
162	161 161	oveq12i	$⊢ (1.0 + 8.0) (1.0 + 8.0) = 9 \cdot 9$
163		9t9e81	$⊢ 9 \cdot 9 = 81$
164	162 163	eqtri	$⊢ (1.0 + 8.0) (1.0 + 8.0) = 81$
165	147 156 164	3eqtr4ri	$⊢ (1.0 + 8.0) (1.0 + 8.0) = 1.00 + 16.00 + 64.00$
166	1 51 73 51 1 73 51 51 51 51 1 99 51 51 100 51 51 1 98 98 24 1 1 98 52 101 102 102 115 122 129 142 165	dpmul4	$⊢ 1.080 \cdot 1.080 < 1.167$
167	97 166	eqbrtri	$⊢ {1.080}^{2} < 1.167$
168	92	resqcli	$⊢ {1.080}^{2} \in ℝ$
169	34 3	pm3.2i	$⊢ (6 \in ℝ \land 7 \in ℝ)$
170		dp2cl	$⊢ (6 \in ℝ \land 7 \in ℝ) \to 67 \in ℝ$
171	169 170	ax-mp	$⊢ 67 \in ℝ$
172	35 171	pm3.2i	$⊢ (1 \in ℝ \land 67 \in ℝ)$
173		dp2cl	$⊢ (1 \in ℝ \land 67 \in ℝ) \to 167 \in ℝ$
174	172 173	ax-mp	$⊢ 167 \in ℝ$
175		dpcl	$⊢ (1 \in ℕ_{0} \land 167 \in ℝ) \to 1.167 \in ℝ$
176	1 174 175	mp2an	$⊢ 1.167 \in ℝ$
177	23 168 176	lttri	$⊢ ({1.079955}^{2} < {1.080}^{2} \land {1.080}^{2} < 1.167) \to {1.079955}^{2} < 1.167$
178	95 167 177	mp2an	$⊢ {1.079955}^{2} < 1.167$
179	23 176 32 47	ltmul1ii	$⊢ {1.079955}^{2} < 1.167 \leftrightarrow {1.079955}^{2} \cdot 1.414 < 1.167 \cdot 1.414$
180	178 179	mpbi	$⊢ {1.079955}^{2} \cdot 1.414 < 1.167 \cdot 1.414$
181		2nn0	$⊢ 2 \in ℕ_{0}$
182		3nn0	$⊢ 3 \in ℕ_{0}$
183		1lt10	$⊢ 1 < 10$
184		3lt10	$⊢ 3 < 10$
185		8lt10	$⊢ 8 < 10$
186	130 53	deccl	$⊢ 109 \in ℕ_{0}$
187		eqid	$⊢ 1092 = 1092$
188	53	dec0h	$⊢ 9 = 09$
189	186	nn0cni	$⊢ 109 \in ℂ$
190	189	addridi	$⊢ 109 + 0 = 109$
191		dec10p	$⊢ 10 + 0 = 10$
192	138	addridi	$⊢ 1 + 0 = 1$
193	1 51 51 1 191 152 192 153	decadd	$⊢ 10 + 0 + 1 = 11$
194		9p1e10	$⊢ 9 + 1 = 10$
195	130 53 51 1 190 152 193 51 194	decaddc	$⊢ 109 + 0 + 1 = 110$
196		9cn	$⊢ 9 \in ℂ$
197		2cn	$⊢ 2 \in ℂ$
198	196 197	addcomi	$⊢ 9 + 2 = 2 + 9$
199		9p2e11	$⊢ 9 + 2 = 11$
200	198 199	eqtr3i	$⊢ 2 + 9 = 11$
201	186 181 51 53 187 188 195 1 200	decaddc	$⊢ 1092 + 9 = 1101$
202	113 138	mulcomi	$⊢ 4 \cdot 1 = 1 \cdot 4$
203	113	mulridi	$⊢ 4 \cdot 1 = 4$
204	202 203	eqtr3i	$⊢ 1 \cdot 4 = 4$
205	24	dec0h	$⊢ 4 = 04$
206	203 202 205	3eqtr3i	$⊢ 1 \cdot 4 = 04$
207	138 113	addcli	$⊢ 1 + 4 \in ℂ$
208	207	addridi	$⊢ 1 + 4 + 0 = 1 + 4$
209	113 138	addcomi	$⊢ 4 + 1 = 1 + 4$
210		4p1e5	$⊢ 4 + 1 = 5$
211	208 209 210	3eqtr2i	$⊢ 1 + 4 + 0 = 5$
212	54	dec0h	$⊢ 5 = 05$
213	211 212	eqtri	$⊢ 1 + 4 + 0 = 05$
214	1 1 1 24 51 51 54 24 116 204 116 206 213 192	dpmul	$⊢ 1.1 \cdot 1.4 = 1.54$
215	110	mulridi	$⊢ 6 \cdot 1 = 6$
216		6t4e24	$⊢ 6 \cdot 4 = 24$
217		7cn	$⊢ 7 \in ℂ$
218	217	mulridi	$⊢ 7 \cdot 1 = 7$
219		7t4e28	$⊢ 7 \cdot 4 = 28$
220	181 24	deccl	$⊢ 24 \in ℕ_{0}$
221	220	nn0cni	$⊢ 24 \in ℂ$
222	221 217	addcomi	$⊢ 24 + 7 = 7 + 24$
223		eqid	$⊢ 24 = 24$
224		2p1e3	$⊢ 2 + 1 = 3$
225	217 113 146	addcomli	$⊢ 4 + 7 = 11$
226	181 24 52 223 224 1 225	decaddci	$⊢ 24 + 7 = 31$
227	222 226	eqtr3i	$⊢ 7 + 24 = 31$
228	227	oveq1i	$⊢ 7 + 24 + 2 = 31 + 2$
229		eqid	$⊢ 31 = 31$
230	197 138 224	addcomli	$⊢ 1 + 2 = 3$
231	182 1 181 229 230	decaddi	$⊢ 31 + 2 = 33$
232	228 231	eqtri	$⊢ 7 + 24 + 2 = 33$
233		6p3e9	$⊢ 6 + 3 = 9$
234	98 52 1 24 181 182 182 73 215 216 218 219 232 233	dpmul	$⊢ 6.7 \cdot 1.4 = 9.38$
235	1 54	deccl	$⊢ 15 \in ℕ_{0}$
236	235 24	deccl	$⊢ 154 \in ℕ_{0}$
237	51 1	deccl	$⊢ 01 \in ℕ_{0}$
238	237 1	deccl	$⊢ 011 \in ℕ_{0}$
239		eqid	$⊢ 1541 = 1541$
240	152	deceq1i	$⊢ 11 = 011$
241	240	deceq1i	$⊢ 110 = 0110$
242		eqid	$⊢ 154 = 154$
243		eqid	$⊢ 011 = 011$
244	152	oveq2i	$⊢ 15 + 1 = 15 + 01$
245		eqid	$⊢ 15 = 15$
246		5p1e6	$⊢ 5 + 1 = 6$
247	1 54 1 245 246	decaddi	$⊢ 15 + 1 = 16$
248	244 247	eqtr3i	$⊢ 15 + 01 = 16$
249	235 24 237 1 242 243 248 210	decadd	$⊢ 154 + 011 = 165$
250	236 1 238 51 239 241 249 192	decadd	$⊢ 1541 + 110 = 1651$
251		7t2e14	$⊢ 7 \cdot 2 = 14$
252		8t7e56	$⊢ 8 \cdot 7 = 56$
253	158 217 252	mulcomli	$⊢ 7 \cdot 8 = 56$
254		8t2e16	$⊢ 8 \cdot 2 = 16$
255		eqid	$⊢ 56 = 56$
256		5cn	$⊢ 5 \in ℂ$
257	256 138 246	addcomli	$⊢ 1 + 5 = 6$
258	257	oveq1i	$⊢ 1 + 5 + 1 = 6 + 1$
259	258 140	eqtri	$⊢ 1 + 5 + 1 = 7$
260		6p6e12	$⊢ 6 + 6 = 12$
261	1 98 54 98 135 255 259 181 260	decaddc	$⊢ 16 + 56 = 72$
262	261	oveq1i	$⊢ 16 + 56 + 6 = 72 + 6$
263		eqid	$⊢ 72 = 72$
264		6p2e8	$⊢ 6 + 2 = 8$
265	110 197 264	addcomli	$⊢ 2 + 6 = 8$
266	52 181 98 263 265	decaddi	$⊢ 72 + 6 = 78$
267	262 266	eqtri	$⊢ 16 + 56 + 6 = 78$
268		eqid	$⊢ 14 = 14$
269		1p1e2	$⊢ 1 + 1 = 2$
270	1 24 52 268 269 1 225	decaddci	$⊢ 14 + 7 = 21$
271	52 73 181 73 98 52 73 24 251 253 254 123 267 270	dpmul	$⊢ 7.8 \cdot 2.8 = 21.84$
272		eqid	$⊢ 11 = 11$
273		eqid	$⊢ 67 = 67$
274	217 138 71	addcomli	$⊢ 1 + 7 = 8$
275	1 1 98 52 272 273 141 274	decadd	$⊢ 11 + 67 = 78$
276	1 1 98 52 52 73 275	dpadd	$⊢ 1.1 + 6.7 = 7.8$
277		4p4e8	$⊢ 4 + 4 = 8$
278	1 24 1 24 268 268 269 277	decadd	$⊢ 14 + 14 = 28$
279	1 24 1 24 181 73 278	dpadd	$⊢ 1.4 + 1.4 = 2.8$
280	276 279	oveq12i	$⊢ (1.1 + 6.7) (1.4 + 1.4) = 7.8 \cdot 2.8$
281	1 181	deccl	$⊢ 12 \in ℕ_{0}$
282		eqid	$⊢ 109 = 109$
283	130	nn0cni	$⊢ 10 \in ℂ$
284	283 138 136	addcomli	$⊢ 1 + 10 = 11$
285	1 1 269 284	decsuc	$⊢ 1 + 10 + 1 = 12$
286		9p5e14	$⊢ 9 + 5 = 14$
287	196 256 286	addcomli	$⊢ 5 + 9 = 14$
288	1 54 130 53 245 282 285 24 287	decaddc	$⊢ 15 + 109 = 124$
289		4p2e6	$⊢ 4 + 2 = 6$
290	235 24 186 181 242 187 288 289	decadd	$⊢ 154 + 1092 = 1246$
291	1 54 24 130 53 281 181 24 98 290	dpadd3	$⊢ 1.54 + 10.92 = 12.46$
292	291	oveq1i	$⊢ 1.54 + 10.92 + 9.38 = 12.46 + 9.38$
293	181 1	deccl	$⊢ 21 \in ℕ_{0}$
294	281 24	deccl	$⊢ 124 \in ℕ_{0}$
295	53 182	deccl	$⊢ 93 \in ℕ_{0}$
296		eqid	$⊢ 1246 = 1246$
297		eqid	$⊢ 938 = 938$
298		eqid	$⊢ 124 = 124$
299		eqid	$⊢ 93 = 93$
300		eqid	$⊢ 12 = 12$
301	1 181 53 300 269 1 200	decaddci	$⊢ 12 + 9 = 21$
302		4p3e7	$⊢ 4 + 3 = 7$
303	281 24 53 182 298 299 301 302	decadd	$⊢ 124 + 93 = 217$
304	293 52 71 303	decsuc	$⊢ 124 + 93 + 1 = 218$
305		8p6e14	$⊢ 8 + 6 = 14$
306	158 110 305	addcomli	$⊢ 6 + 8 = 14$
307	294 98 295 73 296 297 304 24 306	decaddc	$⊢ 1246 + 938 = 2184$
308	281 24 98 53 182 293 73 73 24 307	dpadd3	$⊢ 12.46 + 9.38 = 21.84$
309	292 308	eqtri	$⊢ 1.54 + 10.92 + 9.38 = 21.84$
310	271 280 309	3eqtr4i	$⊢ (1.1 + 6.7) (1.4 + 1.4) = 1.54 + 10.92 + 9.38$
311	1 1 98 52 1 1 54 24 24 24 1 130 53 181 53 182 73 1 1 51 1 1 98 54 1 183 184 185 201 214 234 250 310	dpmul4	$⊢ 1.167 \cdot 1.414 < 1.651$
312	176 32	remulcli	$⊢ 1.167 \cdot 1.414 \in ℝ$
313	33 312 43	lttri	$⊢ ({1.079955}^{2} \cdot 1.414 < 1.167 \cdot 1.414 \land 1.167 \cdot 1.414 < 1.651) \to {1.079955}^{2} \cdot 1.414 < 1.651$
314	180 311 313	mp2an	$⊢ {1.079955}^{2} \cdot 1.414 < 1.651$
315	50 314	pm3.2i	$⊢ (0 \leq {1.079955}^{2} \cdot 1.414 \land {1.079955}^{2} \cdot 1.414 < 1.651)$
316	44 315	pm3.2i	$⊢ (({1.079955}^{2} \cdot 1.414 \in ℝ \land 1.651 \in ℝ) \land (0 \leq {1.079955}^{2} \cdot 1.414 \land {1.079955}^{2} \cdot 1.414 < 1.651))$
317		4re	$⊢ 4 \in ℝ$
318		2re	$⊢ 2 \in ℝ$
319		3re	$⊢ 3 \in ℝ$
320	34 319	pm3.2i	$⊢ (6 \in ℝ \land 3 \in ℝ)$
321		dp2cl	$⊢ (6 \in ℝ \land 3 \in ℝ) \to 63 \in ℝ$
322	320 321	ax-mp	$⊢ 63 \in ℝ$
323	318 322	pm3.2i	$⊢ (2 \in ℝ \land 63 \in ℝ)$
324		dp2cl	$⊢ (2 \in ℝ \land 63 \in ℝ) \to 263 \in ℝ$
325	323 324	ax-mp	$⊢ 263 \in ℝ$
326	317 325	pm3.2i	$⊢ (4 \in ℝ \land 263 \in ℝ)$
327		dp2cl	$⊢ (4 \in ℝ \land 263 \in ℝ) \to 4263 \in ℝ$
328	326 327	ax-mp	$⊢ 4263 \in ℝ$
329		dpcl	$⊢ (1 \in ℕ_{0} \land 4263 \in ℝ) \to 1.4263 \in ℝ$
330	1 328 329	mp2an	$⊢ 1.4263 \in ℝ$
331	84 319	pm3.2i	$⊢ (8 \in ℝ \land 3 \in ℝ)$
332		dp2cl	$⊢ (8 \in ℝ \land 3 \in ℝ) \to 83 \in ℝ$
333	331 332	ax-mp	$⊢ 83 \in ℝ$
334	84 333	pm3.2i	$⊢ (8 \in ℝ \land 83 \in ℝ)$
335		dp2cl	$⊢ (8 \in ℝ \land 83 \in ℝ) \to 883 \in ℝ$
336	334 335	ax-mp	$⊢ 883 \in ℝ$
337	319 336	pm3.2i	$⊢ (3 \in ℝ \land 883 \in ℝ)$
338		dp2cl	$⊢ (3 \in ℝ \land 883 \in ℝ) \to 3883 \in ℝ$
339	337 338	ax-mp	$⊢ 3883 \in ℝ$
340	2 339	pm3.2i	$⊢ (0 \in ℝ \land 3883 \in ℝ)$
341		dp2cl	$⊢ (0 \in ℝ \land 3883 \in ℝ) \to 03883 \in ℝ$
342	340 341	ax-mp	$⊢ 03883 \in ℝ$
343		dpcl	$⊢ (1 \in ℕ_{0} \land 03883 \in ℝ) \to 1.03883 \in ℝ$
344	1 342 343	mp2an	$⊢ 1.03883 \in ℝ$
345	330 344	remulcli	$⊢ 1.4263 \cdot 1.03883 \in ℝ$
346	317 333	pm3.2i	$⊢ (4 \in ℝ \land 83 \in ℝ)$
347		dp2cl	$⊢ (4 \in ℝ \land 83 \in ℝ) \to 483 \in ℝ$
348	346 347	ax-mp	$⊢ 483 \in ℝ$
349		dpcl	$⊢ (1 \in ℕ_{0} \land 483 \in ℝ) \to 1.483 \in ℝ$
350	1 348 349	mp2an	$⊢ 1.483 \in ℝ$
351	345 350	pm3.2i	$⊢ (1.4263 \cdot 1.03883 \in ℝ \land 1.483 \in ℝ)$
352		3rp	$⊢ 3 \in ℝ^{+}$
353	98 352	rpdp2cl	$⊢ 63 \in ℝ^{+}$
354	181 353	rpdp2cl	$⊢ 263 \in ℝ^{+}$
355	24 354	rpdp2cl	$⊢ 4263 \in ℝ^{+}$
356	1 355	rpdpcl	$⊢ 1.4263 \in ℝ^{+}$
357		rpge0	$⊢ 1.4263 \in ℝ^{+} \to 0 \leq 1.4263$
358	356 357	ax-mp	$⊢ 0 \leq 1.4263$
359	73 352	rpdp2cl	$⊢ 83 \in ℝ^{+}$
360	73 359	rpdp2cl	$⊢ 883 \in ℝ^{+}$
361	182 360	rpdp2cl	$⊢ 3883 \in ℝ^{+}$
362	51 361	rpdp2cl	$⊢ 03883 \in ℝ^{+}$
363	1 362	rpdpcl	$⊢ 1.03883 \in ℝ^{+}$
364		rpge0	$⊢ 1.03883 \in ℝ^{+} \to 0 \leq 1.03883$
365	363 364	ax-mp	$⊢ 0 \leq 1.03883$
366	330 344	mulge0i	$⊢ (0 \leq 1.4263 \land 0 \leq 1.03883) \to 0 \leq 1.4263 \cdot 1.03883$
367	358 365 366	mp2an	$⊢ 0 \leq 1.4263 \cdot 1.03883$
368	318 3	pm3.2i	$⊢ (2 \in ℝ \land 7 \in ℝ)$
369		dp2cl	$⊢ (2 \in ℝ \land 7 \in ℝ) \to 27 \in ℝ$
370	368 369	ax-mp	$⊢ 27 \in ℝ$
371	317 370	pm3.2i	$⊢ (4 \in ℝ \land 27 \in ℝ)$
372		dp2cl	$⊢ (4 \in ℝ \land 27 \in ℝ) \to 427 \in ℝ$
373	371 372	ax-mp	$⊢ 427 \in ℝ$
374		dpcl	$⊢ (1 \in ℕ_{0} \land 427 \in ℝ) \to 1.427 \in ℝ$
375	1 373 374	mp2an	$⊢ 1.427 \in ℝ$
376	330 375	pm3.2i	$⊢ (1.4263 \in ℝ \land 1.427 \in ℝ)$
377		7nn	$⊢ 7 \in ℕ$
378		nnrp	$⊢ 7 \in ℕ \to 7 \in ℝ^{+}$
379	377 378	ax-mp	$⊢ 7 \in ℝ^{+}$
380	181 379	rpdp2cl	$⊢ 27 \in ℝ^{+}$
381	24 380	rpdp2cl	$⊢ 427 \in ℝ^{+}$
382	98 352 184 140	dp2ltsuc	$⊢ 63 < 7$
383	181 353 379 382	dp2lt	$⊢ 263 < 27$
384	24 354 380 383	dp2lt	$⊢ 4263 < 427$
385	1 355 381 384	dplt	$⊢ 1.4263 < 1.427$
386	358 385	pm3.2i	$⊢ (0 \leq 1.4263 \land 1.4263 < 1.427)$
387	376 386	pm3.2i	$⊢ ((1.4263 \in ℝ \land 1.427 \in ℝ) \land (0 \leq 1.4263 \land 1.4263 < 1.427))$
388	319 4	pm3.2i	$⊢ (3 \in ℝ \land 9 \in ℝ)$
389		dp2cl	$⊢ (3 \in ℝ \land 9 \in ℝ) \to 39 \in ℝ$
390	388 389	ax-mp	$⊢ 39 \in ℝ$
391	2 390	pm3.2i	$⊢ (0 \in ℝ \land 39 \in ℝ)$
392		dp2cl	$⊢ (0 \in ℝ \land 39 \in ℝ) \to 039 \in ℝ$
393	391 392	ax-mp	$⊢ 039 \in ℝ$
394		dpcl	$⊢ (1 \in ℕ_{0} \land 039 \in ℝ) \to 1.039 \in ℝ$
395	1 393 394	mp2an	$⊢ 1.039 \in ℝ$
396	344 395	pm3.2i	$⊢ (1.03883 \in ℝ \land 1.039 \in ℝ)$
397		9nn	$⊢ 9 \in ℕ$
398		nnrp	$⊢ 9 \in ℕ \to 9 \in ℝ^{+}$
399	397 398	ax-mp	$⊢ 9 \in ℝ^{+}$
400	182 399	rpdp2cl	$⊢ 39 \in ℝ^{+}$
401	51 400	rpdp2cl	$⊢ 039 \in ℝ^{+}$
402	73 352 185 184	dp2lt10	$⊢ 83 < 10$
403	73 359 402 160	dp2ltsuc	$⊢ 883 < 9$
404	182 360 399 403	dp2lt	$⊢ 3883 < 39$
405	51 361 400 404	dp2lt	$⊢ 03883 < 039$
406	1 362 401 405	dplt	$⊢ 1.03883 < 1.039$
407	365 406	pm3.2i	$⊢ (0 \leq 1.03883 \land 1.03883 < 1.039)$
408	396 407	pm3.2i	$⊢ ((1.03883 \in ℝ \land 1.039 \in ℝ) \land (0 \leq 1.03883 \land 1.03883 < 1.039))$
409		ltmul12a	$⊢ (((1.4263 \in ℝ \land 1.427 \in ℝ) \land (0 \leq 1.4263 \land 1.4263 < 1.427)) \land ((1.03883 \in ℝ \land 1.039 \in ℝ) \land (0 \leq 1.03883 \land 1.03883 < 1.039))) \to 1.4263 \cdot 1.03883 < 1.427 \cdot 1.039$
410	387 408 409	mp2an	$⊢ 1.4263 \cdot 1.03883 < 1.427 \cdot 1.039$
411		6lt10	$⊢ 6 < 10$
412	73 1	deccl	$⊢ 81 \in ℕ_{0}$
413		eqid	$⊢ 816 = 816$
414		eqid	$⊢ 10 = 10$
415		eqid	$⊢ 81 = 81$
416	73 1 269 415	decsuc	$⊢ 81 + 1 = 82$
417	73	dec0h	$⊢ 8 = 08$
418	417	deceq1i	$⊢ 82 = 082$
419	416 418	eqtri	$⊢ 81 + 1 = 082$
420	110	addridi	$⊢ 6 + 0 = 6$
421	412 98 1 51 413 414 419 420	decadd	$⊢ 816 + 10 = 0826$
422	138	mul01i	$⊢ 1 \cdot 0 = 0$
423	113	mul01i	$⊢ 4 \cdot 0 = 0$
424	51	dec0h	$⊢ 0 = 00$
425	423 424	eqtri	$⊢ 4 \cdot 0 = 00$
426	113	addridi	$⊢ 4 + 0 = 4$
427	426	oveq1i	$⊢ 4 + 0 + 0 = 4 + 0$
428	427 426 205	3eqtri	$⊢ 4 + 0 + 0 = 04$
429	1 24 1 51 51 51 24 51 116 422 203 425 428 192	dpmul	$⊢ 1.4 \cdot 1.0 = 1.40$
430		3cn	$⊢ 3 \in ℂ$
431		3t2e6	$⊢ 3 \cdot 2 = 6$
432	430 197 431	mulcomli	$⊢ 2 \cdot 3 = 6$
433		9t2e18	$⊢ 9 \cdot 2 = 18$
434	196 197 433	mulcomli	$⊢ 2 \cdot 9 = 18$
435		7t3e21	$⊢ 7 \cdot 3 = 21$
436		9t7e63	$⊢ 9 \cdot 7 = 63$
437	196 217 436	mulcomli	$⊢ 7 \cdot 9 = 63$
438		eqid	$⊢ 21 = 21$
439		eqid	$⊢ 18 = 18$
440	159 160	eqtri	$⊢ 1 + 8 = 9$
441	181 1 1 73 438 439 224 440	decadd	$⊢ 21 + 18 = 39$
442	441	oveq1i	$⊢ 21 + 18 + 6 = 39 + 6$
443		eqid	$⊢ 39 = 39$
444		3p1e4	$⊢ 3 + 1 = 4$
445		9p6e15	$⊢ 9 + 6 = 15$
446	182 53 98 443 444 54 445	decaddci	$⊢ 39 + 6 = 45$
447	442 446	eqtri	$⊢ 21 + 18 + 6 = 45$
448		6p4e10	$⊢ 6 + 4 = 10$
449	181 52 182 53 98 24 54 182 432 434 435 437 447 448	dpmul	$⊢ 2.7 \cdot 3.9 = 10.53$
450	1 24	deccl	$⊢ 14 \in ℕ_{0}$
451	450 51	deccl	$⊢ 140 \in ℕ_{0}$
452	417 73	eqeltrri	$⊢ 08 \in ℕ_{0}$
453		eqid	$⊢ 1401 = 1401$
454		eqid	$⊢ 082 = 082$
455		eqid	$⊢ 140 = 140$
456	417 158	eqeltrri	$⊢ 08 \in ℂ$
457		0cn	$⊢ 0 \in ℂ$
458	417	oveq1i	$⊢ 8 + 0 = 08 + 0$
459	158	addridi	$⊢ 8 + 0 = 8$
460	458 459	eqtr3i	$⊢ 08 + 0 = 8$
461	456 457 460	addcomli	$⊢ 0 + 08 = 8$
462	450 51 452 455 461	decaddi	$⊢ 140 + 08 = 148$
463	451 1 452 181 453 454 462 230	decadd	$⊢ 1401 + 082 = 1483$
464		4t4e16	$⊢ 4 \cdot 4 = 16$
465		9t4e36	$⊢ 9 \cdot 4 = 36$
466	196 113 465	mulcomli	$⊢ 4 \cdot 9 = 36$
467	196	mulridi	$⊢ 9 \cdot 1 = 9$
468	467 188	eqtri	$⊢ 9 \cdot 1 = 09$
469	196 138 468	mulcomli	$⊢ 1 \cdot 9 = 09$
470	182 98	deccl	$⊢ 36 \in ℕ_{0}$
471	470	nn0cni	$⊢ 36 \in ℂ$
472		eqid	$⊢ 36 = 36$
473	182 98 24 472 444 51 448	decaddci	$⊢ 36 + 4 = 40$
474	471 113 473	addcomli	$⊢ 4 + 36 = 40$
475	474	oveq1i	$⊢ 4 + 36 + 0 = 40 + 0$
476	24 51	deccl	$⊢ 40 \in ℕ_{0}$
477	476	nn0cni	$⊢ 40 \in ℂ$
478	477	addridi	$⊢ 40 + 0 = 40$
479	475 478	eqtri	$⊢ 4 + 36 + 0 = 40$
480	1 98 24 135 269 51 448	decaddci	$⊢ 16 + 4 = 20$
481	24 1 24 53 51 24 51 53 464 466 204 469 479 480	dpmul	$⊢ 4.1 \cdot 4.9 = 20.09$
482		eqid	$⊢ 27 = 27$
483	230	oveq1i	$⊢ 1 + 2 + 1 = 3 + 1$
484	483 444	eqtri	$⊢ 1 + 2 + 1 = 4$
485	1 24 181 52 268 482 484 1 225	decaddc	$⊢ 14 + 27 = 41$
486	1 24 181 52 24 1 485	dpadd	$⊢ 1.4 + 2.7 = 4.1$
487	430 138 444	addcomli	$⊢ 1 + 3 = 4$
488	196	addlidi	$⊢ 0 + 9 = 9$
489	1 51 182 53 414 443 487 488	decadd	$⊢ 10 + 39 = 49$
490	1 51 182 53 24 53 489	dpadd	$⊢ 1.0 + 3.9 = 4.9$
491	486 490	oveq12i	$⊢ (1.4 + 2.7) (1.0 + 3.9) = 4.1 \cdot 4.9$
492	1 24 73 1 268 415 440 210	decadd	$⊢ 14 + 81 = 95$
493	450 51 412 98 455 413 492 111	decadd	$⊢ 140 + 816 = 956$
494	1 24 51 73 1 53 98 54 98 493	dpadd3	$⊢ 1.40 + 8.16 = 9.56$
495	494	oveq1i	$⊢ 1.40 + 8.16 + 10.53 = 9.56 + 10.53$
496	181 51	deccl	$⊢ 20 \in ℕ_{0}$
497	53 54	deccl	$⊢ 95 \in ℕ_{0}$
498	130 54	deccl	$⊢ 105 \in ℕ_{0}$
499		eqid	$⊢ 956 = 956$
500		eqid	$⊢ 1053 = 1053$
501		eqid	$⊢ 95 = 95$
502		eqid	$⊢ 105 = 105$
503		dec10p	$⊢ 10 + 9 = 19$
504	283 196 503	addcomli	$⊢ 9 + 10 = 19$
505	504	oveq1i	$⊢ 9 + 10 + 1 = 19 + 1$
506		eqid	$⊢ 19 = 19$
507	1 53 1 506 269 51 194	decaddci	$⊢ 19 + 1 = 20$
508	505 507	eqtri	$⊢ 9 + 10 + 1 = 20$
509		5p5e10	$⊢ 5 + 5 = 10$
510	53 54 130 54 501 502 508 51 509	decaddc	$⊢ 95 + 105 = 200$
511	497 98 498 182 499 500 510 233	decadd	$⊢ 956 + 1053 = 2009$
512	53 54 98 130 54 496 182 51 53 511	dpadd3	$⊢ 9.56 + 10.53 = 20.09$
513	495 512	eqtri	$⊢ 1.40 + 8.16 + 10.53 = 20.09$
514	481 491 513	3eqtr4i	$⊢ (1.4 + 2.7) (1.0 + 3.9) = 1.40 + 8.16 + 10.53$
515	1 24 181 52 1 182 24 51 51 53 1 73 1 98 130 54 182 51 73 181 98 1 24 73 182 411 67 184 421 429 449 463 514	dpmul4	$⊢ 1.427 \cdot 1.039 < 1.483$
516	375 395	remulcli	$⊢ 1.427 \cdot 1.039 \in ℝ$
517	345 516 350	lttri	$⊢ (1.4263 \cdot 1.03883 < 1.427 \cdot 1.039 \land 1.427 \cdot 1.039 < 1.483) \to 1.4263 \cdot 1.03883 < 1.483$
518	410 515 517	mp2an	$⊢ 1.4263 \cdot 1.03883 < 1.483$
519	367 518	pm3.2i	$⊢ (0 \leq 1.4263 \cdot 1.03883 \land 1.4263 \cdot 1.03883 < 1.483)$
520	351 519	pm3.2i	$⊢ ((1.4263 \cdot 1.03883 \in ℝ \land 1.483 \in ℝ) \land (0 \leq 1.4263 \cdot 1.03883 \land 1.4263 \cdot 1.03883 < 1.483))$
521		ltmul12a	$⊢ ((({1.079955}^{2} \cdot 1.414 \in ℝ \land 1.651 \in ℝ) \land (0 \leq {1.079955}^{2} \cdot 1.414 \land {1.079955}^{2} \cdot 1.414 < 1.651)) \land ((1.4263 \cdot 1.03883 \in ℝ \land 1.483 \in ℝ) \land (0 \leq 1.4263 \cdot 1.03883 \land 1.4263 \cdot 1.03883 < 1.483))) \to {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 < 1.651 \cdot 1.483$
522	316 520 521	mp2an	$⊢ {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 < 1.651 \cdot 1.483$
523	24 181	deccl	$⊢ 42 \in ℕ_{0}$
524	496 24	deccl	$⊢ 204 \in ℕ_{0}$
525		eqid	$⊢ 2042 = 2042$
526		eqid	$⊢ 42 = 42$
527		eqid	$⊢ 204 = 204$
528	496 24 24 527 277	decaddi	$⊢ 204 + 4 = 208$
529		2p2e4	$⊢ 2 + 2 = 4$
530	524 181 24 181 525 526 528 529	decadd	$⊢ 2042 + 42 = 2084$
531	448	oveq1i	$⊢ 6 + 4 + 2 = 10 + 2$
532		dec10p	$⊢ 10 + 2 = 12$
533	531 532	eqtri	$⊢ 6 + 4 + 2 = 12$
534	1 98 1 24 181 1 181 24 116 204 215 216 533 269	dpmul	$⊢ 1.6 \cdot 1.4 = 2.24$
535		8t5e40	$⊢ 8 \cdot 5 = 40$
536	158 256 535	mulcomli	$⊢ 5 \cdot 8 = 40$
537		5t3e15	$⊢ 5 \cdot 3 = 15$
538	158	mullidi	$⊢ 1 \cdot 8 = 8$
539	430	mullidi	$⊢ 1 \cdot 3 = 3$
540	182	dec0h	$⊢ 3 = 03$
541	539 540	eqtri	$⊢ 1 \cdot 3 = 03$
542	235	nn0cni	$⊢ 15 \in ℂ$
543		8p5e13	$⊢ 8 + 5 = 13$
544	158 256 543	addcomli	$⊢ 5 + 8 = 13$
545	1 54 73 245 269 182 544	decaddci	$⊢ 15 + 8 = 23$
546	542 158 545	addcomli	$⊢ 8 + 15 = 23$
547	546	oveq1i	$⊢ 8 + 15 + 0 = 23 + 0$
548	181 182	deccl	$⊢ 23 \in ℕ_{0}$
549	548	nn0cni	$⊢ 23 \in ℂ$
550	549	addridi	$⊢ 23 + 0 = 23$
551	547 550	eqtri	$⊢ 8 + 15 + 0 = 23$
552		eqid	$⊢ 40 = 40$
553	197	addlidi	$⊢ 0 + 2 = 2$
554	24 51 181 552 553	decaddi	$⊢ 40 + 2 = 42$
555	54 1 73 182 51 181 182 182 536 537 538 541 551 554	dpmul	$⊢ 5.1 \cdot 8.3 = 42.33$
556	181 181	deccl	$⊢ 22 \in ℕ_{0}$
557	556 24	deccl	$⊢ 224 \in ℕ_{0}$
558		eqid	$⊢ 2241 = 2241$
559		eqid	$⊢ 208 = 208$
560		eqid	$⊢ 224 = 224$
561		eqid	$⊢ 20 = 20$
562		eqid	$⊢ 22 = 22$
563	181 181 181 562 529	decaddi	$⊢ 22 + 2 = 24$
564	556 24 181 51 560 561 563 426	decadd	$⊢ 224 + 20 = 244$
565	557 1 496 73 558 559 564 440	decadd	$⊢ 2241 + 208 = 2449$
566	556 98	deccl	$⊢ 226 \in ℕ_{0}$
567	523 182	deccl	$⊢ 423 \in ℕ_{0}$
568		eqid	$⊢ 2266 = 2266$
569		eqid	$⊢ 4233 = 4233$
570		eqid	$⊢ 226 = 226$
571		eqid	$⊢ 423 = 423$
572	113 197 289	addcomli	$⊢ 2 + 4 = 6$
573	181 181 24 181 562 526 572 529	decadd	$⊢ 22 + 42 = 64$
574	556 98 523 182 570 571 573 233	decadd	$⊢ 226 + 423 = 649$
575	566 98 567 182 568 569 574 233	decadd	$⊢ 2266 + 4233 = 6499$
576	556 98 98 523 182 100 182 53 53 575	dpadd3	$⊢ 22.66 + 42.33 = 64.99$
577	496	nn0cni	$⊢ 20 \in ℂ$
578	181 51 181 561 553	decaddi	$⊢ 20 + 2 = 22$
579	577 197 578	addcomli	$⊢ 2 + 20 = 22$
580	181 181 496 24 562 527 579 572	decadd	$⊢ 22 + 204 = 226$
581	556 24 524 181 560 525 580 289	decadd	$⊢ 224 + 2042 = 2266$
582	181 181 24 496 24 556 181 98 98 581	dpadd3	$⊢ 2.24 + 20.42 = 22.66$
583	582	oveq1i	$⊢ 2.24 + 20.42 + 42.33 = 22.66 + 42.33$
584		eqid	$⊢ 51 = 51$
585	1 98 54 1 135 584 257 140	decadd	$⊢ 16 + 51 = 67$
586	1 98 54 1 98 52 585	dpadd	$⊢ 1.6 + 5.1 = 6.7$
587		eqid	$⊢ 83 = 83$
588	1 24 73 182 268 587 440 302	decadd	$⊢ 14 + 83 = 97$
589	1 24 73 182 53 52 588	dpadd	$⊢ 1.4 + 8.3 = 9.7$
590	586 589	oveq12i	$⊢ (1.6 + 5.1) (1.4 + 8.3) = 6.7 \cdot 9.7$
591		9t6e54	$⊢ 9 \cdot 6 = 54$
592	196 110 591	mulcomli	$⊢ 6 \cdot 9 = 54$
593		7t6e42	$⊢ 7 \cdot 6 = 42$
594	217 110 593	mulcomli	$⊢ 6 \cdot 7 = 42$
595		7t7e49	$⊢ 7 \cdot 7 = 49$
596		eqid	$⊢ 63 = 63$
597		3p2e5	$⊢ 3 + 2 = 5$
598	98 182 24 181 596 526 448 597	decadd	$⊢ 63 + 42 = 105$
599	598	oveq1i	$⊢ 63 + 42 + 4 = 105 + 4$
600		5p4e9	$⊢ 5 + 4 = 9$
601	130 54 24 502 600	decaddi	$⊢ 105 + 4 = 109$
602	599 601	eqtri	$⊢ 63 + 42 + 4 = 109$
603		eqid	$⊢ 54 = 54$
604	54 24 1 51 603 414 246 426	decadd	$⊢ 54 + 10 = 64$
605	98 52 53 52 24 130 53 53 592 594 437 595 602 604	dpmul	$⊢ 6.7 \cdot 9.7 = 64.99$
606	590 605	eqtri	$⊢ (1.6 + 5.1) (1.4 + 8.3) = 64.99$
607	576 583 606	3eqtr4ri	$⊢ (1.6 + 5.1) (1.4 + 8.3) = 2.24 + 20.42 + 42.33$
608	1 98 54 1 1 73 181 24 24 182 181 496 24 181 523 182 182 181 51 73 24 181 24 24 53 101 184 184 530 534 555 565 607	dpmul4	$⊢ 1.651 \cdot 1.483 < 2.449$
609	33 345	remulcli	$⊢ {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 \in ℝ$
610	43 350	remulcli	$⊢ 1.651 \cdot 1.483 \in ℝ$
611	24 399	rpdp2cl	$⊢ 49 \in ℝ^{+}$
612	24 611	rpdp2cl	$⊢ 449 \in ℝ^{+}$
613	181 612	rpdpcl	$⊢ 2.449 \in ℝ^{+}$
614		rpre	$⊢ 2.449 \in ℝ^{+} \to 2.449 \in ℝ$
615	613 614	ax-mp	$⊢ 2.449 \in ℝ$
616	609 610 615	lttri	$⊢ ({1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 < 1.651 \cdot 1.483 \land 1.651 \cdot 1.483 < 2.449) \to {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 < 2.449$
617	522 608 616	mp2an	$⊢ {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 < 2.449$
618		3pos	$⊢ 0 < 3$
619	609 615 319	ltmul2i	$⊢ 0 < 3 \to ({1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 < 2.449 \leftrightarrow 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 < 3 \cdot 2.449)$
620	618 619	ax-mp	$⊢ {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 < 2.449 \leftrightarrow 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 < 3 \cdot 2.449$
621	617 620	mpbi	$⊢ 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 < 3 \cdot 2.449$
622	119	dp2eq2i	$⊢ 000 = 00$
623	622 119	eqtri	$⊢ 000 = 0$
624	623	oveq2i	$⊢ 3.000 = 3.0$
625	182	dp0u	$⊢ 3.0 = 3$
626	624 625	eqtr2i	$⊢ 3 = 3.000$
627	626	oveq1i	$⊢ 3 \cdot 2.449 = 3.000 \cdot 2.449$
628	450 52	deccl	$⊢ 147 \in ℕ_{0}$
629	628 51	deccl	$⊢ 1470 \in ℕ_{0}$
630	629	nn0cni	$⊢ 1470 \in ℂ$
631	630	addridi	$⊢ 1470 + 0 = 1470$
632		4t3e12	$⊢ 4 \cdot 3 = 12$
633	113 430 632	mulcomli	$⊢ 3 \cdot 4 = 12$
634	197	mul02i	$⊢ 0 \cdot 2 = 0$
635	113 457 425	mulcomli	$⊢ 0 \cdot 4 = 00$
636	51 51 1 181 424 300 153 553	decadd	$⊢ 0 + 12 = 12$
637	636	oveq1i	$⊢ 0 + 12 + 0 = 12 + 0$
638	281	nn0cni	$⊢ 12 \in ℂ$
639	638	addridi	$⊢ 12 + 0 = 12$
640	637 639	eqtri	$⊢ 0 + 12 + 0 = 12$
641	182 51 181 24 51 1 181 51 431 633 634 635 640 140	dpmul	$⊢ 3.0 \cdot 2.4 = 7.20$
642	51	dp0u	$⊢ 0.0 = 0$
643	642	oveq1i	$⊢ 0.0 \cdot 4.9 = 0 \cdot 4.9$
644		dpcl	$⊢ (4 \in ℕ_{0} \land 9 \in ℝ) \to 4.9 \in ℝ$
645	24 4 644	mp2an	$⊢ 4.9 \in ℝ$
646	645	recni	$⊢ 4.9 \in ℂ$
647	646	mul02i	$⊢ 0 \cdot 4.9 = 0$
648	643 647	eqtri	$⊢ 0.0 \cdot 4.9 = 0$
649	119	oveq2i	$⊢ 0.00 = 0.0$
650	649 642	eqtri	$⊢ 0.00 = 0$
651	648 650	eqtr4i	$⊢ 0.0 \cdot 4.9 = 0.00$
652	52 181	deccl	$⊢ 72 \in ℕ_{0}$
653	652 51	deccl	$⊢ 720 \in ℕ_{0}$
654		eqid	$⊢ 7201 = 7201$
655		eqid	$⊢ 147 = 147$
656		eqid	$⊢ 720 = 720$
657	52 181 224 263	decsuc	$⊢ 72 + 1 = 73$
658	652 51 1 24 656 268 657 114	decadd	$⊢ 720 + 14 = 734$
659	653 1 450 52 654 655 658 274	decadd	$⊢ 7201 + 147 = 7348$
660	642	oveq2i	$⊢ 3.0 + 0.0 = 3.0 + 0$
661	625 430	eqeltri	$⊢ 3.0 \in ℂ$
662	661	addridi	$⊢ 3.0 + 0 = 3.0$
663	660 662	eqtri	$⊢ 3.0 + 0.0 = 3.0$
664		eqid	$⊢ 49 = 49$
665	572	oveq1i	$⊢ 2 + 4 + 1 = 6 + 1$
666	665 140	eqtri	$⊢ 2 + 4 + 1 = 7$
667		9p4e13	$⊢ 9 + 4 = 13$
668	196 113 667	addcomli	$⊢ 4 + 9 = 13$
669	181 24 24 53 223 664 666 182 668	decaddc	$⊢ 24 + 49 = 73$
670	181 24 24 53 52 182 669	dpadd	$⊢ 2.4 + 4.9 = 7.3$
671	663 670	oveq12i	$⊢ (3.0 + 0.0) (2.4 + 4.9) = 3.0 \cdot 7.3$
672	217 430 435	mulcomli	$⊢ 3 \cdot 7 = 21$
673		3t3e9	$⊢ 3 \cdot 3 = 9$
674	217	mul01i	$⊢ 7 \cdot 0 = 0$
675	217 457 674	mulcomli	$⊢ 0 \cdot 7 = 0$
676	430	mul01i	$⊢ 3 \cdot 0 = 0$
677	676 424	eqtri	$⊢ 3 \cdot 0 = 00$
678	430 457 677	mulcomli	$⊢ 0 \cdot 3 = 00$
679	196	addridi	$⊢ 9 + 0 = 9$
680	679	oveq1i	$⊢ 9 + 0 + 0 = 9 + 0$
681	680 679 188	3eqtri	$⊢ 9 + 0 + 0 = 09$
682	196 457	addcomi	$⊢ 9 + 0 = 0 + 9$
683	682	oveq1i	$⊢ 9 + 0 + 0 = 0 + 9 + 0$
684	683	eqeq1i	$⊢ 9 + 0 + 0 = 09 \leftrightarrow 0 + 9 + 0 = 09$
685	681 684	mpbi	$⊢ 0 + 9 + 0 = 09$
686	181 1 51 438 192	decaddi	$⊢ 21 + 0 = 21$
687	182 51 52 182 51 51 53 51 672 673 675 678 685 686	dpmul	$⊢ 3.0 \cdot 7.3 = 21.90$
688	671 687	eqtri	$⊢ (3.0 + 0.0) (2.4 + 4.9) = 21.90$
689	650	oveq2i	$⊢ 7.20 + 14.70 + 0.00 = 7.20 + 14.70 + 0$
690	318 2	pm3.2i	$⊢ (2 \in ℝ \land 0 \in ℝ)$
691		dp2cl	$⊢ (2 \in ℝ \land 0 \in ℝ) \to 20 \in ℝ$
692	690 691	ax-mp	$⊢ 20 \in ℝ$
693		dpcl	$⊢ (7 \in ℕ_{0} \land 20 \in ℝ) \to 7.20 \in ℝ$
694	52 692 693	mp2an	$⊢ 7.20 \in ℝ$
695	694	recni	$⊢ 7.20 \in ℂ$
696	3 2	pm3.2i	$⊢ (7 \in ℝ \land 0 \in ℝ)$
697		dp2cl	$⊢ (7 \in ℝ \land 0 \in ℝ) \to 70 \in ℝ$
698	696 697	ax-mp	$⊢ 70 \in ℝ$
699		dpcl	$⊢ (14 \in ℕ_{0} \land 70 \in ℝ) \to 14.70 \in ℝ$
700	450 698 699	mp2an	$⊢ 14.70 \in ℝ$
701	700	recni	$⊢ 14.70 \in ℂ$
702	695 701	addcli	$⊢ 7.20 + 14.70 \in ℂ$
703	702	addridi	$⊢ 7.20 + 14.70 + 0 = 7.20 + 14.70$
704		eqid	$⊢ 1470 = 1470$
705	450	nn0cni	$⊢ 14 \in ℂ$
706	705 217 270	addcomli	$⊢ 7 + 14 = 21$
707		7p2e9	$⊢ 7 + 2 = 9$
708	217 197 707	addcomli	$⊢ 2 + 7 = 9$
709	52 181 450 52 263 655 706 708	decadd	$⊢ 72 + 147 = 219$
710		00id	$⊢ 0 + 0 = 0$
711	652 51 628 51 656 704 709 710	decadd	$⊢ 720 + 1470 = 2190$
712	52 181 51 450 52 293 51 53 51 711	dpadd3	$⊢ 7.20 + 14.70 = 21.90$
713	689 703 712	3eqtri	$⊢ 7.20 + 14.70 + 0.00 = 21.90$
714	688 713	eqtr4i	$⊢ (3.0 + 0.0) (2.4 + 4.9) = 7.20 + 14.70 + 0.00$
715	182 51 51 51 181 24 181 51 24 53 52 450 52 51 51 51 51 1 24 52 51 52 182 24 73 102 102 102 631 641 651 659 714	dpmul4	$⊢ 3.000 \cdot 2.449 < 7.348$
716	627 715	eqbrtri	$⊢ 3 \cdot 2.449 < 7.348$
717	319 609	remulcli	$⊢ 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 \in ℝ$
718	319 615	remulcli	$⊢ 3 \cdot 2.449 \in ℝ$
719		nnrp	$⊢ 8 \in ℕ \to 8 \in ℝ^{+}$
720	63 719	ax-mp	$⊢ 8 \in ℝ^{+}$
721	24 720	rpdp2cl	$⊢ 48 \in ℝ^{+}$
722	182 721	rpdp2cl	$⊢ 348 \in ℝ^{+}$
723	52 722	rpdpcl	$⊢ 7.348 \in ℝ^{+}$
724		rpre	$⊢ 7.348 \in ℝ^{+} \to 7.348 \in ℝ$
725	723 724	ax-mp	$⊢ 7.348 \in ℝ$
726	717 718 725	lttri	$⊢ (3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 < 3 \cdot 2.449 \land 3 \cdot 2.449 < 7.348) \to 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 < 7.348$
727	621 716 726	mp2an	$⊢ 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 < 7.348$

Metamath Proof Explorer

Theorem hgt750lem2

Proof