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		2t3e6	$⊢ 2 \cdot 3 = 6$
431		9t2e18	$⊢ 9 \cdot 2 = 18$
432	196 197 431	mulcomli	$⊢ 2 \cdot 9 = 18$
433		7t3e21	$⊢ 7 \cdot 3 = 21$
434		9t7e63	$⊢ 9 \cdot 7 = 63$
435	196 217 434	mulcomli	$⊢ 7 \cdot 9 = 63$
436		eqid	$⊢ 21 = 21$
437		eqid	$⊢ 18 = 18$
438	159 160	eqtri	$⊢ 1 + 8 = 9$
439	181 1 1 73 436 437 224 438	decadd	$⊢ 21 + 18 = 39$
440	439	oveq1i	$⊢ 21 + 18 + 6 = 39 + 6$
441		eqid	$⊢ 39 = 39$
442		3p1e4	$⊢ 3 + 1 = 4$
443		9p6e15	$⊢ 9 + 6 = 15$
444	182 53 98 441 442 54 443	decaddci	$⊢ 39 + 6 = 45$
445	440 444	eqtri	$⊢ 21 + 18 + 6 = 45$
446		6p4e10	$⊢ 6 + 4 = 10$
447	181 52 182 53 98 24 54 182 430 432 433 435 445 446	dpmul	$⊢ 2.7 \cdot 3.9 = 10.53$
448	1 24	deccl	$⊢ 14 \in ℕ_{0}$
449	448 51	deccl	$⊢ 140 \in ℕ_{0}$
450	417 73	eqeltrri	$⊢ 08 \in ℕ_{0}$
451		eqid	$⊢ 1401 = 1401$
452		eqid	$⊢ 082 = 082$
453		eqid	$⊢ 140 = 140$
454	417 158	eqeltrri	$⊢ 08 \in ℂ$
455		0cn	$⊢ 0 \in ℂ$
456	417	oveq1i	$⊢ 8 + 0 = 08 + 0$
457	158	addridi	$⊢ 8 + 0 = 8$
458	456 457	eqtr3i	$⊢ 08 + 0 = 8$
459	454 455 458	addcomli	$⊢ 0 + 08 = 8$
460	448 51 450 453 459	decaddi	$⊢ 140 + 08 = 148$
461	449 1 450 181 451 452 460 230	decadd	$⊢ 1401 + 082 = 1483$
462		4t4e16	$⊢ 4 \cdot 4 = 16$
463		9t4e36	$⊢ 9 \cdot 4 = 36$
464	196 113 463	mulcomli	$⊢ 4 \cdot 9 = 36$
465	196	mulridi	$⊢ 9 \cdot 1 = 9$
466	465 188	eqtri	$⊢ 9 \cdot 1 = 09$
467	196 138 466	mulcomli	$⊢ 1 \cdot 9 = 09$
468	182 98	deccl	$⊢ 36 \in ℕ_{0}$
469	468	nn0cni	$⊢ 36 \in ℂ$
470		eqid	$⊢ 36 = 36$
471	182 98 24 470 442 51 446	decaddci	$⊢ 36 + 4 = 40$
472	469 113 471	addcomli	$⊢ 4 + 36 = 40$
473	472	oveq1i	$⊢ 4 + 36 + 0 = 40 + 0$
474	24 51	deccl	$⊢ 40 \in ℕ_{0}$
475	474	nn0cni	$⊢ 40 \in ℂ$
476	475	addridi	$⊢ 40 + 0 = 40$
477	473 476	eqtri	$⊢ 4 + 36 + 0 = 40$
478	1 98 24 135 269 51 446	decaddci	$⊢ 16 + 4 = 20$
479	24 1 24 53 51 24 51 53 462 464 204 467 477 478	dpmul	$⊢ 4.1 \cdot 4.9 = 20.09$
480		eqid	$⊢ 27 = 27$
481	230	oveq1i	$⊢ 1 + 2 + 1 = 3 + 1$
482	481 442	eqtri	$⊢ 1 + 2 + 1 = 4$
483	1 24 181 52 268 480 482 1 225	decaddc	$⊢ 14 + 27 = 41$
484	1 24 181 52 24 1 483	dpadd	$⊢ 1.4 + 2.7 = 4.1$
485		3cn	$⊢ 3 \in ℂ$
486	485 138 442	addcomli	$⊢ 1 + 3 = 4$
487	196	addlidi	$⊢ 0 + 9 = 9$
488	1 51 182 53 414 441 486 487	decadd	$⊢ 10 + 39 = 49$
489	1 51 182 53 24 53 488	dpadd	$⊢ 1.0 + 3.9 = 4.9$
490	484 489	oveq12i	$⊢ (1.4 + 2.7) (1.0 + 3.9) = 4.1 \cdot 4.9$
491	1 24 73 1 268 415 438 210	decadd	$⊢ 14 + 81 = 95$
492	448 51 412 98 453 413 491 111	decadd	$⊢ 140 + 816 = 956$
493	1 24 51 73 1 53 98 54 98 492	dpadd3	$⊢ 1.40 + 8.16 = 9.56$
494	493	oveq1i	$⊢ 1.40 + 8.16 + 10.53 = 9.56 + 10.53$
495	181 51	deccl	$⊢ 20 \in ℕ_{0}$
496	53 54	deccl	$⊢ 95 \in ℕ_{0}$
497	130 54	deccl	$⊢ 105 \in ℕ_{0}$
498		eqid	$⊢ 956 = 956$
499		eqid	$⊢ 1053 = 1053$
500		eqid	$⊢ 95 = 95$
501		eqid	$⊢ 105 = 105$
502		dec10p	$⊢ 10 + 9 = 19$
503	283 196 502	addcomli	$⊢ 9 + 10 = 19$
504	503	oveq1i	$⊢ 9 + 10 + 1 = 19 + 1$
505		eqid	$⊢ 19 = 19$
506	1 53 1 505 269 51 194	decaddci	$⊢ 19 + 1 = 20$
507	504 506	eqtri	$⊢ 9 + 10 + 1 = 20$
508		5p5e10	$⊢ 5 + 5 = 10$
509	53 54 130 54 500 501 507 51 508	decaddc	$⊢ 95 + 105 = 200$
510	496 98 497 182 498 499 509 233	decadd	$⊢ 956 + 1053 = 2009$
511	53 54 98 130 54 495 182 51 53 510	dpadd3	$⊢ 9.56 + 10.53 = 20.09$
512	494 511	eqtri	$⊢ 1.40 + 8.16 + 10.53 = 20.09$
513	479 490 512	3eqtr4i	$⊢ (1.4 + 2.7) (1.0 + 3.9) = 1.40 + 8.16 + 10.53$
514	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 447 461 513	dpmul4	$⊢ 1.427 \cdot 1.039 < 1.483$
515	375 395	remulcli	$⊢ 1.427 \cdot 1.039 \in ℝ$
516	345 515 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$
517	410 514 516	mp2an	$⊢ 1.4263 \cdot 1.03883 < 1.483$
518	367 517	pm3.2i	$⊢ (0 \leq 1.4263 \cdot 1.03883 \land 1.4263 \cdot 1.03883 < 1.483)$
519	351 518	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))$
520		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$
521	316 519 520	mp2an	$⊢ {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 < 1.651 \cdot 1.483$
522	24 181	deccl	$⊢ 42 \in ℕ_{0}$
523	495 24	deccl	$⊢ 204 \in ℕ_{0}$
524		eqid	$⊢ 2042 = 2042$
525		eqid	$⊢ 42 = 42$
526		eqid	$⊢ 204 = 204$
527	495 24 24 526 277	decaddi	$⊢ 204 + 4 = 208$
528		2p2e4	$⊢ 2 + 2 = 4$
529	523 181 24 181 524 525 527 528	decadd	$⊢ 2042 + 42 = 2084$
530	446	oveq1i	$⊢ 6 + 4 + 2 = 10 + 2$
531		dec10p	$⊢ 10 + 2 = 12$
532	530 531	eqtri	$⊢ 6 + 4 + 2 = 12$
533	1 98 1 24 181 1 181 24 116 204 215 216 532 269	dpmul	$⊢ 1.6 \cdot 1.4 = 2.24$
534		8t5e40	$⊢ 8 \cdot 5 = 40$
535	158 256 534	mulcomli	$⊢ 5 \cdot 8 = 40$
536		5t3e15	$⊢ 5 \cdot 3 = 15$
537	158	mullidi	$⊢ 1 \cdot 8 = 8$
538	485	mullidi	$⊢ 1 \cdot 3 = 3$
539	182	dec0h	$⊢ 3 = 03$
540	538 539	eqtri	$⊢ 1 \cdot 3 = 03$
541	235	nn0cni	$⊢ 15 \in ℂ$
542		8p5e13	$⊢ 8 + 5 = 13$
543	158 256 542	addcomli	$⊢ 5 + 8 = 13$
544	1 54 73 245 269 182 543	decaddci	$⊢ 15 + 8 = 23$
545	541 158 544	addcomli	$⊢ 8 + 15 = 23$
546	545	oveq1i	$⊢ 8 + 15 + 0 = 23 + 0$
547	181 182	deccl	$⊢ 23 \in ℕ_{0}$
548	547	nn0cni	$⊢ 23 \in ℂ$
549	548	addridi	$⊢ 23 + 0 = 23$
550	546 549	eqtri	$⊢ 8 + 15 + 0 = 23$
551		eqid	$⊢ 40 = 40$
552	197	addlidi	$⊢ 0 + 2 = 2$
553	24 51 181 551 552	decaddi	$⊢ 40 + 2 = 42$
554	54 1 73 182 51 181 182 182 535 536 537 540 550 553	dpmul	$⊢ 5.1 \cdot 8.3 = 42.33$
555	181 181	deccl	$⊢ 22 \in ℕ_{0}$
556	555 24	deccl	$⊢ 224 \in ℕ_{0}$
557		eqid	$⊢ 2241 = 2241$
558		eqid	$⊢ 208 = 208$
559		eqid	$⊢ 224 = 224$
560		eqid	$⊢ 20 = 20$
561		eqid	$⊢ 22 = 22$
562	181 181 181 561 528	decaddi	$⊢ 22 + 2 = 24$
563	555 24 181 51 559 560 562 426	decadd	$⊢ 224 + 20 = 244$
564	556 1 495 73 557 558 563 438	decadd	$⊢ 2241 + 208 = 2449$
565	555 98	deccl	$⊢ 226 \in ℕ_{0}$
566	522 182	deccl	$⊢ 423 \in ℕ_{0}$
567		eqid	$⊢ 2266 = 2266$
568		eqid	$⊢ 4233 = 4233$
569		eqid	$⊢ 226 = 226$
570		eqid	$⊢ 423 = 423$
571	113 197 289	addcomli	$⊢ 2 + 4 = 6$
572	181 181 24 181 561 525 571 528	decadd	$⊢ 22 + 42 = 64$
573	555 98 522 182 569 570 572 233	decadd	$⊢ 226 + 423 = 649$
574	565 98 566 182 567 568 573 233	decadd	$⊢ 2266 + 4233 = 6499$
575	555 98 98 522 182 100 182 53 53 574	dpadd3	$⊢ 22.66 + 42.33 = 64.99$
576	495	nn0cni	$⊢ 20 \in ℂ$
577	181 51 181 560 552	decaddi	$⊢ 20 + 2 = 22$
578	576 197 577	addcomli	$⊢ 2 + 20 = 22$
579	181 181 495 24 561 526 578 571	decadd	$⊢ 22 + 204 = 226$
580	555 24 523 181 559 524 579 289	decadd	$⊢ 224 + 2042 = 2266$
581	181 181 24 495 24 555 181 98 98 580	dpadd3	$⊢ 2.24 + 20.42 = 22.66$
582	581	oveq1i	$⊢ 2.24 + 20.42 + 42.33 = 22.66 + 42.33$
583		eqid	$⊢ 51 = 51$
584	1 98 54 1 135 583 257 140	decadd	$⊢ 16 + 51 = 67$
585	1 98 54 1 98 52 584	dpadd	$⊢ 1.6 + 5.1 = 6.7$
586		eqid	$⊢ 83 = 83$
587	1 24 73 182 268 586 438 302	decadd	$⊢ 14 + 83 = 97$
588	1 24 73 182 53 52 587	dpadd	$⊢ 1.4 + 8.3 = 9.7$
589	585 588	oveq12i	$⊢ (1.6 + 5.1) (1.4 + 8.3) = 6.7 \cdot 9.7$
590		9t6e54	$⊢ 9 \cdot 6 = 54$
591	196 110 590	mulcomli	$⊢ 6 \cdot 9 = 54$
592		7t6e42	$⊢ 7 \cdot 6 = 42$
593	217 110 592	mulcomli	$⊢ 6 \cdot 7 = 42$
594		7t7e49	$⊢ 7 \cdot 7 = 49$
595		eqid	$⊢ 63 = 63$
596		3p2e5	$⊢ 3 + 2 = 5$
597	98 182 24 181 595 525 446 596	decadd	$⊢ 63 + 42 = 105$
598	597	oveq1i	$⊢ 63 + 42 + 4 = 105 + 4$
599		5p4e9	$⊢ 5 + 4 = 9$
600	130 54 24 501 599	decaddi	$⊢ 105 + 4 = 109$
601	598 600	eqtri	$⊢ 63 + 42 + 4 = 109$
602		eqid	$⊢ 54 = 54$
603	54 24 1 51 602 414 246 426	decadd	$⊢ 54 + 10 = 64$
604	98 52 53 52 24 130 53 53 591 593 435 594 601 603	dpmul	$⊢ 6.7 \cdot 9.7 = 64.99$
605	589 604	eqtri	$⊢ (1.6 + 5.1) (1.4 + 8.3) = 64.99$
606	575 582 605	3eqtr4ri	$⊢ (1.6 + 5.1) (1.4 + 8.3) = 2.24 + 20.42 + 42.33$
607	1 98 54 1 1 73 181 24 24 182 181 495 24 181 522 182 182 181 51 73 24 181 24 24 53 101 184 184 529 533 554 564 606	dpmul4	$⊢ 1.651 \cdot 1.483 < 2.449$
608	33 345	remulcli	$⊢ {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 \in ℝ$
609	43 350	remulcli	$⊢ 1.651 \cdot 1.483 \in ℝ$
610	24 399	rpdp2cl	$⊢ 49 \in ℝ^{+}$
611	24 610	rpdp2cl	$⊢ 449 \in ℝ^{+}$
612	181 611	rpdpcl	$⊢ 2.449 \in ℝ^{+}$
613		rpre	$⊢ 2.449 \in ℝ^{+} \to 2.449 \in ℝ$
614	612 613	ax-mp	$⊢ 2.449 \in ℝ$
615	608 609 614	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$
616	521 607 615	mp2an	$⊢ {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 < 2.449$
617		3pos	$⊢ 0 < 3$
618	608 614 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)$
619	617 618	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$
620	616 619	mpbi	$⊢ 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 < 3 \cdot 2.449$
621	119	dp2eq2i	$⊢ 000 = 00$
622	621 119	eqtri	$⊢ 000 = 0$
623	622	oveq2i	$⊢ 3.000 = 3.0$
624	182	dp0u	$⊢ 3.0 = 3$
625	623 624	eqtr2i	$⊢ 3 = 3.000$
626	625	oveq1i	$⊢ 3 \cdot 2.449 = 3.000 \cdot 2.449$
627	448 52	deccl	$⊢ 147 \in ℕ_{0}$
628	627 51	deccl	$⊢ 1470 \in ℕ_{0}$
629	628	nn0cni	$⊢ 1470 \in ℂ$
630	629	addridi	$⊢ 1470 + 0 = 1470$
631		3t2e6	$⊢ 3 \cdot 2 = 6$
632		4t3e12	$⊢ 4 \cdot 3 = 12$
633	113 485 632	mulcomli	$⊢ 3 \cdot 4 = 12$
634	197	mul02i	$⊢ 0 \cdot 2 = 0$
635	113 455 425	mulcomli	$⊢ 0 \cdot 4 = 00$
636	51 51 1 181 424 300 153 552	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 631 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 448 52 654 655 658 274	decadd	$⊢ 7201 + 147 = 7348$
660	642	oveq2i	$⊢ 3.0 + 0.0 = 3.0 + 0$
661	624 485	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	571	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 485 433	mulcomli	$⊢ 3 \cdot 7 = 21$
673		3t3e9	$⊢ 3 \cdot 3 = 9$
674	217	mul01i	$⊢ 7 \cdot 0 = 0$
675	217 455 674	mulcomli	$⊢ 0 \cdot 7 = 0$
676	485	mul01i	$⊢ 3 \cdot 0 = 0$
677	676 424	eqtri	$⊢ 3 \cdot 0 = 00$
678	485 455 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 455	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 436 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	448 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	448	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 448 52 263 655 706 708	decadd	$⊢ 72 + 147 = 219$
710		00id	$⊢ 0 + 0 = 0$
711	652 51 627 51 656 704 709 710	decadd	$⊢ 720 + 1470 = 2190$
712	52 181 51 448 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 448 52 51 51 51 51 1 24 52 51 52 182 24 73 102 102 102 630 641 651 659 714	dpmul4	$⊢ 3.000 \cdot 2.449 < 7.348$
716	626 715	eqbrtri	$⊢ 3 \cdot 2.449 < 7.348$
717	319 608	remulcli	$⊢ 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 \in ℝ$
718	319 614	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	620 716 726	mp2an	$⊢ 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 < 7.348$

Metamath Proof Explorer

Theorem hgt750lem2

Proof