Theorem hgt750lem2 35048

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

Assertion

Ref	Expression
hgt750lem2	⊢ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) < (7._3_48)

Proof of Theorem hgt750lem2

Step	Hyp	Ref	Expression
1		1nn0 12526	. . . . . . . . . 10 ⊢ 1 ∈ ℕ0
2		0re 11216	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
3		7re 12340	. . . . . . . . . . . . . 14 ⊢ 7 ∈ ℝ
4		9re 12346	. . . . . . . . . . . . . . . 16 ⊢ 9 ∈ ℝ
5		5re 12334	. . . . . . . . . . . . . . . . . . . 20 ⊢ 5 ∈ ℝ
6	5, 5	pm3.2i 475	. . . . . . . . . . . . . . . . . . 19 ⊢ (5 ∈ ℝ ∧ 5 ∈ ℝ)
7		dp2cl 33210	. . . . . . . . . . . . . . . . . . 19 ⊢ ((5 ∈ ℝ ∧ 5 ∈ ℝ) → _55 ∈ ℝ)
8	6, 7	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ _55 ∈ ℝ
9	4, 8	pm3.2i 475	. . . . . . . . . . . . . . . . 17 ⊢ (9 ∈ ℝ ∧ _55 ∈ ℝ)
10		dp2cl 33210	. . . . . . . . . . . . . . . . 17 ⊢ ((9 ∈ ℝ ∧ _55 ∈ ℝ) → _9_55 ∈ ℝ)
11	9, 10	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ _9_55 ∈ ℝ
12	4, 11	pm3.2i 475	. . . . . . . . . . . . . . 15 ⊢ (9 ∈ ℝ ∧ _9_55 ∈ ℝ)
13		dp2cl 33210	. . . . . . . . . . . . . . 15 ⊢ ((9 ∈ ℝ ∧ _9_55 ∈ ℝ) → _9_9_55 ∈ ℝ)
14	12, 13	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ _9_9_55 ∈ ℝ
15	3, 14	pm3.2i 475	. . . . . . . . . . . . 13 ⊢ (7 ∈ ℝ ∧ _9_9_55 ∈ ℝ)
16		dp2cl 33210	. . . . . . . . . . . . 13 ⊢ ((7 ∈ ℝ ∧ _9_9_55 ∈ ℝ) → _7_9_9_55 ∈ ℝ)
17	15, 16	ax-mp 5	. . . . . . . . . . . 12 ⊢ _7_9_9_55 ∈ ℝ
18	2, 17	pm3.2i 475	. . . . . . . . . . 11 ⊢ (0 ∈ ℝ ∧ _7_9_9_55 ∈ ℝ)
19		dp2cl 33210	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ _7_9_9_55 ∈ ℝ) → _0_7_9_9_55 ∈ ℝ)
20	18, 19	ax-mp 5	. . . . . . . . . 10 ⊢ _0_7_9_9_55 ∈ ℝ
21		dpcl 33221	. . . . . . . . . 10 ⊢ ((1 ∈ ℕ0 ∧ _0_7_9_9_55 ∈ ℝ) → (1._0_7_9_9_55) ∈ ℝ)
22	1, 20, 21	mp2an 704	. . . . . . . . 9 ⊢ (1._0_7_9_9_55) ∈ ℝ
23	22	resqcli 14229	. . . . . . . 8 ⊢ ((1._0_7_9_9_55)↑2) ∈ ℝ
24		4nn0 12529	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ0
25		4nn 12330	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℕ
26		nnrp 13034	. . . . . . . . . . . . 13 ⊢ (4 ∈ ℕ → 4 ∈ ℝ+)
27	25, 26	ax-mp 5	. . . . . . . . . . . 12 ⊢ 4 ∈ ℝ+
28	1, 27	rpdp2cl 33212	. . . . . . . . . . 11 ⊢ _14 ∈ ℝ+
29	24, 28	rpdp2cl 33212	. . . . . . . . . 10 ⊢ _4_14 ∈ ℝ+
30	1, 29	rpdpcl 33233	. . . . . . . . 9 ⊢ (1._4_14) ∈ ℝ+
31		rpre 13031	. . . . . . . . 9 ⊢ ((1._4_14) ∈ ℝ+ → (1._4_14) ∈ ℝ)
32	30, 31	ax-mp 5	. . . . . . . 8 ⊢ (1._4_14) ∈ ℝ
33	23, 32	remulcli 11231	. . . . . . 7 ⊢ (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ
34		6re 12337	. . . . . . . . . 10 ⊢ 6 ∈ ℝ
35		1re 11214	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
36	5, 35	pm3.2i 475	. . . . . . . . . . 11 ⊢ (5 ∈ ℝ ∧ 1 ∈ ℝ)
37		dp2cl 33210	. . . . . . . . . . 11 ⊢ ((5 ∈ ℝ ∧ 1 ∈ ℝ) → _51 ∈ ℝ)
38	36, 37	ax-mp 5	. . . . . . . . . 10 ⊢ _51 ∈ ℝ
39	34, 38	pm3.2i 475	. . . . . . . . 9 ⊢ (6 ∈ ℝ ∧ _51 ∈ ℝ)
40		dp2cl 33210	. . . . . . . . 9 ⊢ ((6 ∈ ℝ ∧ _51 ∈ ℝ) → _6_51 ∈ ℝ)
41	39, 40	ax-mp 5	. . . . . . . 8 ⊢ _6_51 ∈ ℝ
42		dpcl 33221	. . . . . . . 8 ⊢ ((1 ∈ ℕ0 ∧ _6_51 ∈ ℝ) → (1._6_51) ∈ ℝ)
43	1, 41, 42	mp2an 704	. . . . . . 7 ⊢ (1._6_51) ∈ ℝ
44	33, 43	pm3.2i 475	. . . . . 6 ⊢ ((((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ ∧ (1._6_51) ∈ ℝ)
45	22	sqge0i 14231	. . . . . . . 8 ⊢ 0 ≤ ((1._0_7_9_9_55)↑2)
46		rpgt0 13035	. . . . . . . . . 10 ⊢ ((1._4_14) ∈ ℝ+ → 0 < (1._4_14))
47	30, 46	ax-mp 5	. . . . . . . . 9 ⊢ 0 < (1._4_14)
48	2, 32, 47	ltleii 11339	. . . . . . . 8 ⊢ 0 ≤ (1._4_14)
49	23, 32	mulge0i 11767	. . . . . . . 8 ⊢ ((0 ≤ ((1._0_7_9_9_55)↑2) ∧ 0 ≤ (1._4_14)) → 0 ≤ (((1._0_7_9_9_55)↑2) · (1._4_14)))
50	45, 48, 49	mp2an 704	. . . . . . 7 ⊢ 0 ≤ (((1._0_7_9_9_55)↑2) · (1._4_14))
51		0nn0 12525	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
52		7nn0 12532	. . . . . . . . . . . . . 14 ⊢ 7 ∈ ℕ0
53		9nn0 12534	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ ℕ0
54		5nn0 12530	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℕ0
55		5nn 12333	. . . . . . . . . . . . . . . . . 18 ⊢ 5 ∈ ℕ
56		nnrp 13034	. . . . . . . . . . . . . . . . . 18 ⊢ (5 ∈ ℕ → 5 ∈ ℝ+)
57	55, 56	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℝ+
58	54, 57	rpdp2cl 33212	. . . . . . . . . . . . . . . 16 ⊢ _55 ∈ ℝ+
59	53, 58	rpdp2cl 33212	. . . . . . . . . . . . . . 15 ⊢ _9_55 ∈ ℝ+
60	53, 59	rpdp2cl 33212	. . . . . . . . . . . . . 14 ⊢ _9_9_55 ∈ ℝ+
61	52, 60	rpdp2cl 33212	. . . . . . . . . . . . 13 ⊢ _7_9_9_55 ∈ ℝ+
62	51, 61	rpdp2cl 33212	. . . . . . . . . . . 12 ⊢ _0_7_9_9_55 ∈ ℝ+
63		8nn 12342	. . . . . . . . . . . . . 14 ⊢ 8 ∈ ℕ
64	63	rpdp2cl2 33213	. . . . . . . . . . . . 13 ⊢ _80 ∈ ℝ+
65	51, 64	rpdp2cl 33212	. . . . . . . . . . . 12 ⊢ _0_80 ∈ ℝ+
66		9lt10 12854	. . . . . . . . . . . . . . . 16 ⊢ 9 < ;10
67		5lt10 12858	. . . . . . . . . . . . . . . . . 18 ⊢ 5 < ;10
68	54, 57, 67, 67	dp2lt10 33214	. . . . . . . . . . . . . . . . 17 ⊢ _55 < ;10
69	53, 58, 66, 68	dp2lt10 33214	. . . . . . . . . . . . . . . 16 ⊢ _9_55 < ;10
70	53, 59, 66, 69	dp2lt10 33214	. . . . . . . . . . . . . . 15 ⊢ _9_9_55 < ;10
71		7p1e8 12395	. . . . . . . . . . . . . . 15 ⊢ (7 + 1) = 8
72	52, 60, 70, 71	dp2ltsuc 33216	. . . . . . . . . . . . . 14 ⊢ _7_9_9_55 < 8
73		8nn0 12533	. . . . . . . . . . . . . . 15 ⊢ 8 ∈ ℕ0
74	73	dp20u 33208	. . . . . . . . . . . . . 14 ⊢ _80 = 8
75	72, 74	breqtrri 5137	. . . . . . . . . . . . 13 ⊢ _7_9_9_55 < _80
76	51, 61, 64, 75	dp2lt 33215	. . . . . . . . . . . 12 ⊢ _0_7_9_9_55 < _0_80
77	1, 62, 65, 76	dplt 33234	. . . . . . . . . . 11 ⊢ (1._0_7_9_9_55) < (1._0_80)
78	1, 62	rpdpcl 33233	. . . . . . . . . . . . 13 ⊢ (1._0_7_9_9_55) ∈ ℝ+
79		rpge0 13036	. . . . . . . . . . . . 13 ⊢ ((1._0_7_9_9_55) ∈ ℝ+ → 0 ≤ (1._0_7_9_9_55))
80	78, 79	ax-mp 5	. . . . . . . . . . . 12 ⊢ 0 ≤ (1._0_7_9_9_55)
81	1, 65	rpdpcl 33233	. . . . . . . . . . . . 13 ⊢ (1._0_80) ∈ ℝ+
82		rpge0 13036	. . . . . . . . . . . . 13 ⊢ ((1._0_80) ∈ ℝ+ → 0 ≤ (1._0_80))
83	81, 82	ax-mp 5	. . . . . . . . . . . 12 ⊢ 0 ≤ (1._0_80)
84		8re 12343	. . . . . . . . . . . . . . . . . 18 ⊢ 8 ∈ ℝ
85	84, 2	pm3.2i 475	. . . . . . . . . . . . . . . . 17 ⊢ (8 ∈ ℝ ∧ 0 ∈ ℝ)
86		dp2cl 33210	. . . . . . . . . . . . . . . . 17 ⊢ ((8 ∈ ℝ ∧ 0 ∈ ℝ) → _80 ∈ ℝ)
87	85, 86	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ _80 ∈ ℝ
88	2, 87	pm3.2i 475	. . . . . . . . . . . . . . 15 ⊢ (0 ∈ ℝ ∧ _80 ∈ ℝ)
89		dp2cl 33210	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ ∧ _80 ∈ ℝ) → _0_80 ∈ ℝ)
90	88, 89	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ _0_80 ∈ ℝ
91		dpcl 33221	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℕ0 ∧ _0_80 ∈ ℝ) → (1._0_80) ∈ ℝ)
92	1, 90, 91	mp2an 704	. . . . . . . . . . . . 13 ⊢ (1._0_80) ∈ ℝ
93	22, 92	lt2sqi 14232	. . . . . . . . . . . 12 ⊢ ((0 ≤ (1._0_7_9_9_55) ∧ 0 ≤ (1._0_80)) → ((1._0_7_9_9_55) < (1._0_80) ↔ ((1._0_7_9_9_55)↑2) < ((1._0_80)↑2)))
94	80, 83, 93	mp2an 704	. . . . . . . . . . 11 ⊢ ((1._0_7_9_9_55) < (1._0_80) ↔ ((1._0_7_9_9_55)↑2) < ((1._0_80)↑2))
95	77, 94	mpbi 233	. . . . . . . . . 10 ⊢ ((1._0_7_9_9_55)↑2) < ((1._0_80)↑2)
96	92	recni 11229	. . . . . . . . . . . 12 ⊢ (1._0_80) ∈ ℂ
97	96	sqvali 14223	. . . . . . . . . . 11 ⊢ ((1._0_80)↑2) = ((1._0_80) · (1._0_80))
98		6nn0 12531	. . . . . . . . . . . . 13 ⊢ 6 ∈ ℕ0
99	1, 98	deccl 12732	. . . . . . . . . . . 12 ⊢ ;16 ∈ ℕ0
100	98, 24	deccl 12732	. . . . . . . . . . . 12 ⊢ ;64 ∈ ℕ0
101		4lt10 12859	. . . . . . . . . . . 12 ⊢ 4 < ;10
102		10pos 12738	. . . . . . . . . . . 12 ⊢ 0 < ;10
103	99, 51	deccl 12732	. . . . . . . . . . . . 13 ⊢ ;;160 ∈ ℕ0
104		eqid 2762	. . . . . . . . . . . . 13 ⊢ ;;;1600 = ;;;1600
105		eqid 2762	. . . . . . . . . . . . 13 ⊢ ;64 = ;64
106		eqid 2762	. . . . . . . . . . . . . 14 ⊢ ;;160 = ;;160
107	98	dec0h 12744	. . . . . . . . . . . . . 14 ⊢ 6 = ;06
108	99	nn0cni 12522	. . . . . . . . . . . . . . 15 ⊢ ;16 ∈ ℂ
109	108	addridi 11403	. . . . . . . . . . . . . 14 ⊢ (;16 + 0) = ;16
110		6cn 12338	. . . . . . . . . . . . . . 15 ⊢ 6 ∈ ℂ
111	110	addlidi 11404	. . . . . . . . . . . . . 14 ⊢ (0 + 6) = 6
112	99, 51, 51, 98, 106, 107, 109, 111	decadd 12776	. . . . . . . . . . . . 13 ⊢ (;;160 + 6) = ;;166
113		4cn 12332	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℂ
114	113	addlidi 11404	. . . . . . . . . . . . 13 ⊢ (0 + 4) = 4
115	103, 51, 98, 24, 104, 105, 112, 114	decadd 12776	. . . . . . . . . . . 12 ⊢ (;;;1600 + ;64) = ;;;1664
116		1t1e1 12408	. . . . . . . . . . . . 13 ⊢ (1 · 1) = 1
117	1	dp0u 33231	. . . . . . . . . . . . . 14 ⊢ (1.0) = 1
118	117, 117	oveq12i 7424	. . . . . . . . . . . . 13 ⊢ ((1.0) · (1.0)) = (1 · 1)
119	51	dp20u 33208	. . . . . . . . . . . . . . 15 ⊢ _00 = 0
120	119	oveq2i 7423	. . . . . . . . . . . . . 14 ⊢ (1._00) = (1.0)
121	120, 117	eqtri 2785	. . . . . . . . . . . . 13 ⊢ (1._00) = 1
122	116, 118, 121	3eqtr4i 2795	. . . . . . . . . . . 12 ⊢ ((1.0) · (1.0)) = (1._00)
123		8t8e64 12843	. . . . . . . . . . . . 13 ⊢ (8 · 8) = ;64
124	73	dp0u 33231	. . . . . . . . . . . . . 14 ⊢ (8.0) = 8
125	124, 124	oveq12i 7424	. . . . . . . . . . . . 13 ⊢ ((8.0) · (8.0)) = (8 · 8)
126	119	oveq2i 7423	. . . . . . . . . . . . . 14 ⊢ (;64._00) = (;64.0)
127	100	dp0u 33231	. . . . . . . . . . . . . 14 ⊢ (;64.0) = ;64
128	126, 127	eqtri 2785	. . . . . . . . . . . . 13 ⊢ (;64._00) = ;64
129	123, 125, 128	3eqtr4i 2795	. . . . . . . . . . . 12 ⊢ ((8.0) · (8.0)) = (;64._00)
130		10nn0 12739	. . . . . . . . . . . . . 14 ⊢ ;10 ∈ ℕ0
131	130, 51	deccl 12732	. . . . . . . . . . . . 13 ⊢ ;;100 ∈ ℕ0
132		eqid 2762	. . . . . . . . . . . . 13 ⊢ ;;;1001 = ;;;1001
133		eqid 2762	. . . . . . . . . . . . 13 ⊢ ;;166 = ;;166
134		eqid 2762	. . . . . . . . . . . . . 14 ⊢ ;;100 = ;;100
135		eqid 2762	. . . . . . . . . . . . . 14 ⊢ ;16 = ;16
136		dec10p 12765	. . . . . . . . . . . . . 14 ⊢ (;10 + 1) = ;11
137	130, 51, 1, 98, 134, 135, 136, 111	decadd 12776	. . . . . . . . . . . . 13 ⊢ (;;100 + ;16) = ;;116
138		ax-1cn 11164	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
139	138, 110	addcomi 11407	. . . . . . . . . . . . . 14 ⊢ (1 + 6) = (6 + 1)
140		6p1e7 12394	. . . . . . . . . . . . . 14 ⊢ (6 + 1) = 7
141	139, 140	eqtri 2785	. . . . . . . . . . . . 13 ⊢ (1 + 6) = 7
142	131, 1, 99, 98, 132, 133, 137, 141	decadd 12776	. . . . . . . . . . . 12 ⊢ (;;;1001 + ;;166) = ;;;1167
143		eqid 2762	. . . . . . . . . . . . . 14 ⊢ ;17 = ;17
144	141	oveq1i 7422	. . . . . . . . . . . . . . 15 ⊢ ((1 + 6) + 1) = (7 + 1)
145	144, 71	eqtri 2785	. . . . . . . . . . . . . 14 ⊢ ((1 + 6) + 1) = 8
146		7p4e11 12798	. . . . . . . . . . . . . 14 ⊢ (7 + 4) = ;11
147	1, 52, 98, 24, 143, 105, 145, 1, 146	decaddc 12777	. . . . . . . . . . . . 13 ⊢ (;17 + ;64) = ;81
148	119	oveq2i 7423	. . . . . . . . . . . . . . . . 17 ⊢ (;16._00) = (;16.0)
149	99	dp0u 33231	. . . . . . . . . . . . . . . . 17 ⊢ (;16.0) = ;16
150	148, 149	eqtri 2785	. . . . . . . . . . . . . . . 16 ⊢ (;16._00) = ;16
151	121, 150	oveq12i 7424	. . . . . . . . . . . . . . 15 ⊢ ((1._00) + (;16._00)) = (1 + ;16)
152	1	dec0h 12744	. . . . . . . . . . . . . . . 16 ⊢ 1 = ;01
153	138	addlidi 11404	. . . . . . . . . . . . . . . 16 ⊢ (0 + 1) = 1
154	51, 1, 1, 98, 152, 135, 153, 141	decadd 12776	. . . . . . . . . . . . . . 15 ⊢ (1 + ;16) = ;17
155	151, 154	eqtri 2785	. . . . . . . . . . . . . 14 ⊢ ((1._00) + (;16._00)) = ;17
156	155, 128	oveq12i 7424	. . . . . . . . . . . . 13 ⊢ (((1._00) + (;16._00)) + (;64._00)) = (;17 + ;64)
157	117, 124	oveq12i 7424	. . . . . . . . . . . . . . . 16 ⊢ ((1.0) + (8.0)) = (1 + 8)
158		8cn 12344	. . . . . . . . . . . . . . . . 17 ⊢ 8 ∈ ℂ
159	138, 158	addcomi 11407	. . . . . . . . . . . . . . . 16 ⊢ (1 + 8) = (8 + 1)
160		8p1e9 12396	. . . . . . . . . . . . . . . 16 ⊢ (8 + 1) = 9
161	157, 159, 160	3eqtri 2789	. . . . . . . . . . . . . . 15 ⊢ ((1.0) + (8.0)) = 9
162	161, 161	oveq12i 7424	. . . . . . . . . . . . . 14 ⊢ (((1.0) + (8.0)) · ((1.0) + (8.0))) = (9 · 9)
163		9t9e81 12851	. . . . . . . . . . . . . 14 ⊢ (9 · 9) = ;81
164	162, 163	eqtri 2785	. . . . . . . . . . . . 13 ⊢ (((1.0) + (8.0)) · ((1.0) + (8.0))) = ;81
165	147, 156, 164	3eqtr4ri 2796	. . . . . . . . . . . 12 ⊢ (((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 33244	. . . . . . . . . . 11 ⊢ ((1._0_80) · (1._0_80)) < (1._1_67)
167	97, 166	eqbrtri 5131	. . . . . . . . . 10 ⊢ ((1._0_80)↑2) < (1._1_67)
168	92	resqcli 14229	. . . . . . . . . . 11 ⊢ ((1._0_80)↑2) ∈ ℝ
169	34, 3	pm3.2i 475	. . . . . . . . . . . . . . 15 ⊢ (6 ∈ ℝ ∧ 7 ∈ ℝ)
170		dp2cl 33210	. . . . . . . . . . . . . . 15 ⊢ ((6 ∈ ℝ ∧ 7 ∈ ℝ) → _67 ∈ ℝ)
171	169, 170	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ _67 ∈ ℝ
172	35, 171	pm3.2i 475	. . . . . . . . . . . . 13 ⊢ (1 ∈ ℝ ∧ _67 ∈ ℝ)
173		dp2cl 33210	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ ∧ _67 ∈ ℝ) → _1_67 ∈ ℝ)
174	172, 173	ax-mp 5	. . . . . . . . . . . 12 ⊢ _1_67 ∈ ℝ
175		dpcl 33221	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℕ0 ∧ _1_67 ∈ ℝ) → (1._1_67) ∈ ℝ)
176	1, 174, 175	mp2an 704	. . . . . . . . . . 11 ⊢ (1._1_67) ∈ ℝ
177	23, 168, 176	lttri 11342	. . . . . . . . . 10 ⊢ ((((1._0_7_9_9_55)↑2) < ((1._0_80)↑2) ∧ ((1._0_80)↑2) < (1._1_67)) → ((1._0_7_9_9_55)↑2) < (1._1_67))
178	95, 167, 177	mp2an 704	. . . . . . . . 9 ⊢ ((1._0_7_9_9_55)↑2) < (1._1_67)
179	23, 176, 32, 47	ltmul1ii 12149	. . . . . . . . 9 ⊢ (((1._0_7_9_9_55)↑2) < (1._1_67) ↔ (((1._0_7_9_9_55)↑2) · (1._4_14)) < ((1._1_67) · (1._4_14)))
180	178, 179	mpbi 233	. . . . . . . 8 ⊢ (((1._0_7_9_9_55)↑2) · (1._4_14)) < ((1._1_67) · (1._4_14))
181		2nn0 12527	. . . . . . . . 9 ⊢ 2 ∈ ℕ0
182		3nn0 12528	. . . . . . . . 9 ⊢ 3 ∈ ℕ0
183		1lt10 12862	. . . . . . . . 9 ⊢ 1 < ;10
184		3lt10 12860	. . . . . . . . 9 ⊢ 3 < ;10
185		8lt10 12855	. . . . . . . . 9 ⊢ 8 < ;10
186	130, 53	deccl 12732	. . . . . . . . . 10 ⊢ ;;109 ∈ ℕ0
187		eqid 2762	. . . . . . . . . 10 ⊢ ;;;1092 = ;;;1092
188	53	dec0h 12744	. . . . . . . . . 10 ⊢ 9 = ;09
189	186	nn0cni 12522	. . . . . . . . . . . 12 ⊢ ;;109 ∈ ℂ
190	189	addridi 11403	. . . . . . . . . . 11 ⊢ (;;109 + 0) = ;;109
191		dec10p 12765	. . . . . . . . . . . 12 ⊢ (;10 + 0) = ;10
192	138	addridi 11403	. . . . . . . . . . . 12 ⊢ (1 + 0) = 1
193	1, 51, 51, 1, 191, 152, 192, 153	decadd 12776	. . . . . . . . . . 11 ⊢ ((;10 + 0) + 1) = ;11
194		9p1e10 12719	. . . . . . . . . . 11 ⊢ (9 + 1) = ;10
195	130, 53, 51, 1, 190, 152, 193, 51, 194	decaddc 12777	. . . . . . . . . 10 ⊢ ((;;109 + 0) + 1) = ;;110
196		9cn 12347	. . . . . . . . . . . 12 ⊢ 9 ∈ ℂ
197		2cn 12322	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
198	196, 197	addcomi 11407	. . . . . . . . . . 11 ⊢ (9 + 2) = (2 + 9)
199		9p2e11 12809	. . . . . . . . . . 11 ⊢ (9 + 2) = ;11
200	198, 199	eqtr3i 2787	. . . . . . . . . 10 ⊢ (2 + 9) = ;11
201	186, 181, 51, 53, 187, 188, 195, 1, 200	decaddc 12777	. . . . . . . . 9 ⊢ (;;;1092 + 9) = ;;;1101
202	113, 138	mulcomi 11223	. . . . . . . . . . 11 ⊢ (4 · 1) = (1 · 4)
203	113	mulridi 11219	. . . . . . . . . . 11 ⊢ (4 · 1) = 4
204	202, 203	eqtr3i 2787	. . . . . . . . . 10 ⊢ (1 · 4) = 4
205	24	dec0h 12744	. . . . . . . . . . 11 ⊢ 4 = ;04
206	203, 202, 205	3eqtr3i 2793	. . . . . . . . . 10 ⊢ (1 · 4) = ;04
207	138, 113	addcli 11221	. . . . . . . . . . . . 13 ⊢ (1 + 4) ∈ ℂ
208	207	addridi 11403	. . . . . . . . . . . 12 ⊢ ((1 + 4) + 0) = (1 + 4)
209	113, 138	addcomi 11407	. . . . . . . . . . . 12 ⊢ (4 + 1) = (1 + 4)
210		4p1e5 12392	. . . . . . . . . . . 12 ⊢ (4 + 1) = 5
211	208, 209, 210	3eqtr2i 2791	. . . . . . . . . . 11 ⊢ ((1 + 4) + 0) = 5
212	54	dec0h 12744	. . . . . . . . . . 11 ⊢ 5 = ;05
213	211, 212	eqtri 2785	. . . . . . . . . 10 ⊢ ((1 + 4) + 0) = ;05
214	1, 1, 1, 24, 51, 51, 54, 24, 116, 204, 116, 206, 213, 192	dpmul 33243	. . . . . . . . 9 ⊢ ((1.1) · (1.4)) = (1._54)
215	110	mulridi 11219	. . . . . . . . . 10 ⊢ (6 · 1) = 6
216		6t4e24 12828	. . . . . . . . . 10 ⊢ (6 · 4) = ;24
217		7cn 12341	. . . . . . . . . . 11 ⊢ 7 ∈ ℂ
218	217	mulridi 11219	. . . . . . . . . 10 ⊢ (7 · 1) = 7
219		7t4e28 12833	. . . . . . . . . 10 ⊢ (7 · 4) = ;28
220	181, 24	deccl 12732	. . . . . . . . . . . . . . 15 ⊢ ;24 ∈ ℕ0
221	220	nn0cni 12522	. . . . . . . . . . . . . 14 ⊢ ;24 ∈ ℂ
222	221, 217	addcomi 11407	. . . . . . . . . . . . 13 ⊢ (;24 + 7) = (7 + ;24)
223		eqid 2762	. . . . . . . . . . . . . 14 ⊢ ;24 = ;24
224		2p1e3 12388	. . . . . . . . . . . . . 14 ⊢ (2 + 1) = 3
225	217, 113, 146	addcomli 11408	. . . . . . . . . . . . . 14 ⊢ (4 + 7) = ;11
226	181, 24, 52, 223, 224, 1, 225	decaddci 12783	. . . . . . . . . . . . 13 ⊢ (;24 + 7) = ;31
227	222, 226	eqtr3i 2787	. . . . . . . . . . . 12 ⊢ (7 + ;24) = ;31
228	227	oveq1i 7422	. . . . . . . . . . 11 ⊢ ((7 + ;24) + 2) = (;31 + 2)
229		eqid 2762	. . . . . . . . . . . 12 ⊢ ;31 = ;31
230	197, 138, 224	addcomli 11408	. . . . . . . . . . . 12 ⊢ (1 + 2) = 3
231	182, 1, 181, 229, 230	decaddi 12782	. . . . . . . . . . 11 ⊢ (;31 + 2) = ;33
232	228, 231	eqtri 2785	. . . . . . . . . 10 ⊢ ((7 + ;24) + 2) = ;33
233		6p3e9 12406	. . . . . . . . . 10 ⊢ (6 + 3) = 9
234	98, 52, 1, 24, 181, 182, 182, 73, 215, 216, 218, 219, 232, 233	dpmul 33243	. . . . . . . . 9 ⊢ ((6.7) · (1.4)) = (9._38)
235	1, 54	deccl 12732	. . . . . . . . . . 11 ⊢ ;15 ∈ ℕ0
236	235, 24	deccl 12732	. . . . . . . . . 10 ⊢ ;;154 ∈ ℕ0
237	51, 1	deccl 12732	. . . . . . . . . . 11 ⊢ ;01 ∈ ℕ0
238	237, 1	deccl 12732	. . . . . . . . . 10 ⊢ ;;011 ∈ ℕ0
239		eqid 2762	. . . . . . . . . 10 ⊢ ;;;1541 = ;;;1541
240	152	deceq1i 12724	. . . . . . . . . . 11 ⊢ ;11 = ;;011
241	240	deceq1i 12724	. . . . . . . . . 10 ⊢ ;;110 = ;;;0110
242		eqid 2762	. . . . . . . . . . 11 ⊢ ;;154 = ;;154
243		eqid 2762	. . . . . . . . . . 11 ⊢ ;;011 = ;;011
244	152	oveq2i 7423	. . . . . . . . . . . 12 ⊢ (;15 + 1) = (;15 + ;01)
245		eqid 2762	. . . . . . . . . . . . 13 ⊢ ;15 = ;15
246		5p1e6 12393	. . . . . . . . . . . . 13 ⊢ (5 + 1) = 6
247	1, 54, 1, 245, 246	decaddi 12782	. . . . . . . . . . . 12 ⊢ (;15 + 1) = ;16
248	244, 247	eqtr3i 2787	. . . . . . . . . . 11 ⊢ (;15 + ;01) = ;16
249	235, 24, 237, 1, 242, 243, 248, 210	decadd 12776	. . . . . . . . . 10 ⊢ (;;154 + ;;011) = ;;165
250	236, 1, 238, 51, 239, 241, 249, 192	decadd 12776	. . . . . . . . 9 ⊢ (;;;1541 + ;;110) = ;;;1651
251		7t2e14 12831	. . . . . . . . . . 11 ⊢ (7 · 2) = ;14
252		8t7e56 12842	. . . . . . . . . . . 12 ⊢ (8 · 7) = ;56
253	158, 217, 252	mulcomli 11224	. . . . . . . . . . 11 ⊢ (7 · 8) = ;56
254		8t2e16 12837	. . . . . . . . . . 11 ⊢ (8 · 2) = ;16
255		eqid 2762	. . . . . . . . . . . . . 14 ⊢ ;56 = ;56
256		5cn 12335	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℂ
257	256, 138, 246	addcomli 11408	. . . . . . . . . . . . . . . 16 ⊢ (1 + 5) = 6
258	257	oveq1i 7422	. . . . . . . . . . . . . . 15 ⊢ ((1 + 5) + 1) = (6 + 1)
259	258, 140	eqtri 2785	. . . . . . . . . . . . . 14 ⊢ ((1 + 5) + 1) = 7
260		6p6e12 12796	. . . . . . . . . . . . . 14 ⊢ (6 + 6) = ;12
261	1, 98, 54, 98, 135, 255, 259, 181, 260	decaddc 12777	. . . . . . . . . . . . 13 ⊢ (;16 + ;56) = ;72
262	261	oveq1i 7422	. . . . . . . . . . . 12 ⊢ ((;16 + ;56) + 6) = (;72 + 6)
263		eqid 2762	. . . . . . . . . . . . 13 ⊢ ;72 = ;72
264		6p2e8 12405	. . . . . . . . . . . . . 14 ⊢ (6 + 2) = 8
265	110, 197, 264	addcomli 11408	. . . . . . . . . . . . 13 ⊢ (2 + 6) = 8
266	52, 181, 98, 263, 265	decaddi 12782	. . . . . . . . . . . 12 ⊢ (;72 + 6) = ;78
267	262, 266	eqtri 2785	. . . . . . . . . . 11 ⊢ ((;16 + ;56) + 6) = ;78
268		eqid 2762	. . . . . . . . . . . 12 ⊢ ;14 = ;14
269		1p1e2 12370	. . . . . . . . . . . 12 ⊢ (1 + 1) = 2
270	1, 24, 52, 268, 269, 1, 225	decaddci 12783	. . . . . . . . . . 11 ⊢ (;14 + 7) = ;21
271	52, 73, 181, 73, 98, 52, 73, 24, 251, 253, 254, 123, 267, 270	dpmul 33243	. . . . . . . . . 10 ⊢ ((7.8) · (2.8)) = (;21._84)
272		eqid 2762	. . . . . . . . . . . . 13 ⊢ ;11 = ;11
273		eqid 2762	. . . . . . . . . . . . 13 ⊢ ;67 = ;67
274	217, 138, 71	addcomli 11408	. . . . . . . . . . . . 13 ⊢ (1 + 7) = 8
275	1, 1, 98, 52, 272, 273, 141, 274	decadd 12776	. . . . . . . . . . . 12 ⊢ (;11 + ;67) = ;78
276	1, 1, 98, 52, 52, 73, 275	dpadd 33241	. . . . . . . . . . 11 ⊢ ((1.1) + (6.7)) = (7.8)
277		4p4e8 12401	. . . . . . . . . . . . 13 ⊢ (4 + 4) = 8
278	1, 24, 1, 24, 268, 268, 269, 277	decadd 12776	. . . . . . . . . . . 12 ⊢ (;14 + ;14) = ;28
279	1, 24, 1, 24, 181, 73, 278	dpadd 33241	. . . . . . . . . . 11 ⊢ ((1.4) + (1.4)) = (2.8)
280	276, 279	oveq12i 7424	. . . . . . . . . 10 ⊢ (((1.1) + (6.7)) · ((1.4) + (1.4))) = ((7.8) · (2.8))
281	1, 181	deccl 12732	. . . . . . . . . . . . 13 ⊢ ;12 ∈ ℕ0
282		eqid 2762	. . . . . . . . . . . . . . 15 ⊢ ;;109 = ;;109
283	130	nn0cni 12522	. . . . . . . . . . . . . . . . 17 ⊢ ;10 ∈ ℂ
284	283, 138, 136	addcomli 11408	. . . . . . . . . . . . . . . 16 ⊢ (1 + ;10) = ;11
285	1, 1, 269, 284	decsuc 12753	. . . . . . . . . . . . . . 15 ⊢ ((1 + ;10) + 1) = ;12
286		9p5e14 12812	. . . . . . . . . . . . . . . 16 ⊢ (9 + 5) = ;14
287	196, 256, 286	addcomli 11408	. . . . . . . . . . . . . . 15 ⊢ (5 + 9) = ;14
288	1, 54, 130, 53, 245, 282, 285, 24, 287	decaddc 12777	. . . . . . . . . . . . . 14 ⊢ (;15 + ;;109) = ;;124
289		4p2e6 12399	. . . . . . . . . . . . . 14 ⊢ (4 + 2) = 6
290	235, 24, 186, 181, 242, 187, 288, 289	decadd 12776	. . . . . . . . . . . . 13 ⊢ (;;154 + ;;;1092) = ;;;1246
291	1, 54, 24, 130, 53, 281, 181, 24, 98, 290	dpadd3 33242	. . . . . . . . . . . 12 ⊢ ((1._54) + (;10._92)) = (;12._46)
292	291	oveq1i 7422	. . . . . . . . . . 11 ⊢ (((1._54) + (;10._92)) + (9._38)) = ((;12._46) + (9._38))
293	181, 1	deccl 12732	. . . . . . . . . . . 12 ⊢ ;21 ∈ ℕ0
294	281, 24	deccl 12732	. . . . . . . . . . . . 13 ⊢ ;;124 ∈ ℕ0
295	53, 182	deccl 12732	. . . . . . . . . . . . 13 ⊢ ;93 ∈ ℕ0
296		eqid 2762	. . . . . . . . . . . . 13 ⊢ ;;;1246 = ;;;1246
297		eqid 2762	. . . . . . . . . . . . 13 ⊢ ;;938 = ;;938
298		eqid 2762	. . . . . . . . . . . . . . 15 ⊢ ;;124 = ;;124
299		eqid 2762	. . . . . . . . . . . . . . 15 ⊢ ;93 = ;93
300		eqid 2762	. . . . . . . . . . . . . . . 16 ⊢ ;12 = ;12
301	1, 181, 53, 300, 269, 1, 200	decaddci 12783	. . . . . . . . . . . . . . 15 ⊢ (;12 + 9) = ;21
302		4p3e7 12400	. . . . . . . . . . . . . . 15 ⊢ (4 + 3) = 7
303	281, 24, 53, 182, 298, 299, 301, 302	decadd 12776	. . . . . . . . . . . . . 14 ⊢ (;;124 + ;93) = ;;217
304	293, 52, 71, 303	decsuc 12753	. . . . . . . . . . . . 13 ⊢ ((;;124 + ;93) + 1) = ;;218
305		8p6e14 12806	. . . . . . . . . . . . . 14 ⊢ (8 + 6) = ;14
306	158, 110, 305	addcomli 11408	. . . . . . . . . . . . 13 ⊢ (6 + 8) = ;14
307	294, 98, 295, 73, 296, 297, 304, 24, 306	decaddc 12777	. . . . . . . . . . . 12 ⊢ (;;;1246 + ;;938) = ;;;2184
308	281, 24, 98, 53, 182, 293, 73, 73, 24, 307	dpadd3 33242	. . . . . . . . . . 11 ⊢ ((;12._46) + (9._38)) = (;21._84)
309	292, 308	eqtri 2785	. . . . . . . . . 10 ⊢ (((1._54) + (;10._92)) + (9._38)) = (;21._84)
310	271, 280, 309	3eqtr4i 2795	. . . . . . . . 9 ⊢ (((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 33244	. . . . . . . 8 ⊢ ((1._1_67) · (1._4_14)) < (1._6_51)
312	176, 32	remulcli 11231	. . . . . . . . 9 ⊢ ((1._1_67) · (1._4_14)) ∈ ℝ
313	33, 312, 43	lttri 11342	. . . . . . . 8 ⊢ (((((1._0_7_9_9_55)↑2) · (1._4_14)) < ((1._1_67) · (1._4_14)) ∧ ((1._1_67) · (1._4_14)) < (1._6_51)) → (((1._0_7_9_9_55)↑2) · (1._4_14)) < (1._6_51))
314	180, 311, 313	mp2an 704	. . . . . . 7 ⊢ (((1._0_7_9_9_55)↑2) · (1._4_14)) < (1._6_51)
315	50, 314	pm3.2i 475	. . . . . 6 ⊢ (0 ≤ (((1._0_7_9_9_55)↑2) · (1._4_14)) ∧ (((1._0_7_9_9_55)↑2) · (1._4_14)) < (1._6_51))
316	44, 315	pm3.2i 475	. . . . 5 ⊢ (((((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ ∧ (1._6_51) ∈ ℝ) ∧ (0 ≤ (((1._0_7_9_9_55)↑2) · (1._4_14)) ∧ (((1._0_7_9_9_55)↑2) · (1._4_14)) < (1._6_51)))
317		4re 12331	. . . . . . . . . . 11 ⊢ 4 ∈ ℝ
318		2re 12321	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
319		3re 12327	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ ℝ
320	34, 319	pm3.2i 475	. . . . . . . . . . . . . 14 ⊢ (6 ∈ ℝ ∧ 3 ∈ ℝ)
321		dp2cl 33210	. . . . . . . . . . . . . 14 ⊢ ((6 ∈ ℝ ∧ 3 ∈ ℝ) → _63 ∈ ℝ)
322	320, 321	ax-mp 5	. . . . . . . . . . . . 13 ⊢ _63 ∈ ℝ
323	318, 322	pm3.2i 475	. . . . . . . . . . . 12 ⊢ (2 ∈ ℝ ∧ _63 ∈ ℝ)
324		dp2cl 33210	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ _63 ∈ ℝ) → _2_63 ∈ ℝ)
325	323, 324	ax-mp 5	. . . . . . . . . . 11 ⊢ _2_63 ∈ ℝ
326	317, 325	pm3.2i 475	. . . . . . . . . 10 ⊢ (4 ∈ ℝ ∧ _2_63 ∈ ℝ)
327		dp2cl 33210	. . . . . . . . . 10 ⊢ ((4 ∈ ℝ ∧ _2_63 ∈ ℝ) → _4_2_63 ∈ ℝ)
328	326, 327	ax-mp 5	. . . . . . . . 9 ⊢ _4_2_63 ∈ ℝ
329		dpcl 33221	. . . . . . . . 9 ⊢ ((1 ∈ ℕ0 ∧ _4_2_63 ∈ ℝ) → (1._4_2_63) ∈ ℝ)
330	1, 328, 329	mp2an 704	. . . . . . . 8 ⊢ (1._4_2_63) ∈ ℝ
331	84, 319	pm3.2i 475	. . . . . . . . . . . . . . . 16 ⊢ (8 ∈ ℝ ∧ 3 ∈ ℝ)
332		dp2cl 33210	. . . . . . . . . . . . . . . 16 ⊢ ((8 ∈ ℝ ∧ 3 ∈ ℝ) → _83 ∈ ℝ)
333	331, 332	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ _83 ∈ ℝ
334	84, 333	pm3.2i 475	. . . . . . . . . . . . . 14 ⊢ (8 ∈ ℝ ∧ _83 ∈ ℝ)
335		dp2cl 33210	. . . . . . . . . . . . . 14 ⊢ ((8 ∈ ℝ ∧ _83 ∈ ℝ) → _8_83 ∈ ℝ)
336	334, 335	ax-mp 5	. . . . . . . . . . . . 13 ⊢ _8_83 ∈ ℝ
337	319, 336	pm3.2i 475	. . . . . . . . . . . 12 ⊢ (3 ∈ ℝ ∧ _8_83 ∈ ℝ)
338		dp2cl 33210	. . . . . . . . . . . 12 ⊢ ((3 ∈ ℝ ∧ _8_83 ∈ ℝ) → _3_8_83 ∈ ℝ)
339	337, 338	ax-mp 5	. . . . . . . . . . 11 ⊢ _3_8_83 ∈ ℝ
340	2, 339	pm3.2i 475	. . . . . . . . . 10 ⊢ (0 ∈ ℝ ∧ _3_8_83 ∈ ℝ)
341		dp2cl 33210	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ _3_8_83 ∈ ℝ) → _0_3_8_83 ∈ ℝ)
342	340, 341	ax-mp 5	. . . . . . . . 9 ⊢ _0_3_8_83 ∈ ℝ
343		dpcl 33221	. . . . . . . . 9 ⊢ ((1 ∈ ℕ0 ∧ _0_3_8_83 ∈ ℝ) → (1._0_3_8_83) ∈ ℝ)
344	1, 342, 343	mp2an 704	. . . . . . . 8 ⊢ (1._0_3_8_83) ∈ ℝ
345	330, 344	remulcli 11231	. . . . . . 7 ⊢ ((1._4_2_63) · (1._0_3_8_83)) ∈ ℝ
346	317, 333	pm3.2i 475	. . . . . . . . 9 ⊢ (4 ∈ ℝ ∧ _83 ∈ ℝ)
347		dp2cl 33210	. . . . . . . . 9 ⊢ ((4 ∈ ℝ ∧ _83 ∈ ℝ) → _4_83 ∈ ℝ)
348	346, 347	ax-mp 5	. . . . . . . 8 ⊢ _4_83 ∈ ℝ
349		dpcl 33221	. . . . . . . 8 ⊢ ((1 ∈ ℕ0 ∧ _4_83 ∈ ℝ) → (1._4_83) ∈ ℝ)
350	1, 348, 349	mp2an 704	. . . . . . 7 ⊢ (1._4_83) ∈ ℝ
351	345, 350	pm3.2i 475	. . . . . 6 ⊢ (((1._4_2_63) · (1._0_3_8_83)) ∈ ℝ ∧ (1._4_83) ∈ ℝ)
352		3rp 13028	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℝ+
353	98, 352	rpdp2cl 33212	. . . . . . . . . . . 12 ⊢ _63 ∈ ℝ+
354	181, 353	rpdp2cl 33212	. . . . . . . . . . 11 ⊢ _2_63 ∈ ℝ+
355	24, 354	rpdp2cl 33212	. . . . . . . . . 10 ⊢ _4_2_63 ∈ ℝ+
356	1, 355	rpdpcl 33233	. . . . . . . . 9 ⊢ (1._4_2_63) ∈ ℝ+
357		rpge0 13036	. . . . . . . . 9 ⊢ ((1._4_2_63) ∈ ℝ+ → 0 ≤ (1._4_2_63))
358	356, 357	ax-mp 5	. . . . . . . 8 ⊢ 0 ≤ (1._4_2_63)
359	73, 352	rpdp2cl 33212	. . . . . . . . . . . . 13 ⊢ _83 ∈ ℝ+
360	73, 359	rpdp2cl 33212	. . . . . . . . . . . 12 ⊢ _8_83 ∈ ℝ+
361	182, 360	rpdp2cl 33212	. . . . . . . . . . 11 ⊢ _3_8_83 ∈ ℝ+
362	51, 361	rpdp2cl 33212	. . . . . . . . . 10 ⊢ _0_3_8_83 ∈ ℝ+
363	1, 362	rpdpcl 33233	. . . . . . . . 9 ⊢ (1._0_3_8_83) ∈ ℝ+
364		rpge0 13036	. . . . . . . . 9 ⊢ ((1._0_3_8_83) ∈ ℝ+ → 0 ≤ (1._0_3_8_83))
365	363, 364	ax-mp 5	. . . . . . . 8 ⊢ 0 ≤ (1._0_3_8_83)
366	330, 344	mulge0i 11767	. . . . . . . 8 ⊢ ((0 ≤ (1._4_2_63) ∧ 0 ≤ (1._0_3_8_83)) → 0 ≤ ((1._4_2_63) · (1._0_3_8_83)))
367	358, 365, 366	mp2an 704	. . . . . . 7 ⊢ 0 ≤ ((1._4_2_63) · (1._0_3_8_83))
368	318, 3	pm3.2i 475	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℝ ∧ 7 ∈ ℝ)
369		dp2cl 33210	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℝ ∧ 7 ∈ ℝ) → _27 ∈ ℝ)
370	368, 369	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ _27 ∈ ℝ
371	317, 370	pm3.2i 475	. . . . . . . . . . . . 13 ⊢ (4 ∈ ℝ ∧ _27 ∈ ℝ)
372		dp2cl 33210	. . . . . . . . . . . . 13 ⊢ ((4 ∈ ℝ ∧ _27 ∈ ℝ) → _4_27 ∈ ℝ)
373	371, 372	ax-mp 5	. . . . . . . . . . . 12 ⊢ _4_27 ∈ ℝ
374		dpcl 33221	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℕ0 ∧ _4_27 ∈ ℝ) → (1._4_27) ∈ ℝ)
375	1, 373, 374	mp2an 704	. . . . . . . . . . 11 ⊢ (1._4_27) ∈ ℝ
376	330, 375	pm3.2i 475	. . . . . . . . . 10 ⊢ ((1._4_2_63) ∈ ℝ ∧ (1._4_27) ∈ ℝ)
377		7nn 12339	. . . . . . . . . . . . . . 15 ⊢ 7 ∈ ℕ
378		nnrp 13034	. . . . . . . . . . . . . . 15 ⊢ (7 ∈ ℕ → 7 ∈ ℝ+)
379	377, 378	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 7 ∈ ℝ+
380	181, 379	rpdp2cl 33212	. . . . . . . . . . . . 13 ⊢ _27 ∈ ℝ+
381	24, 380	rpdp2cl 33212	. . . . . . . . . . . 12 ⊢ _4_27 ∈ ℝ+
382	98, 352, 184, 140	dp2ltsuc 33216	. . . . . . . . . . . . . 14 ⊢ _63 < 7
383	181, 353, 379, 382	dp2lt 33215	. . . . . . . . . . . . 13 ⊢ _2_63 < _27
384	24, 354, 380, 383	dp2lt 33215	. . . . . . . . . . . 12 ⊢ _4_2_63 < _4_27
385	1, 355, 381, 384	dplt 33234	. . . . . . . . . . 11 ⊢ (1._4_2_63) < (1._4_27)
386	358, 385	pm3.2i 475	. . . . . . . . . 10 ⊢ (0 ≤ (1._4_2_63) ∧ (1._4_2_63) < (1._4_27))
387	376, 386	pm3.2i 475	. . . . . . . . 9 ⊢ (((1._4_2_63) ∈ ℝ ∧ (1._4_27) ∈ ℝ) ∧ (0 ≤ (1._4_2_63) ∧ (1._4_2_63) < (1._4_27)))
388	319, 4	pm3.2i 475	. . . . . . . . . . . . . . 15 ⊢ (3 ∈ ℝ ∧ 9 ∈ ℝ)
389		dp2cl 33210	. . . . . . . . . . . . . . 15 ⊢ ((3 ∈ ℝ ∧ 9 ∈ ℝ) → _39 ∈ ℝ)
390	388, 389	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ _39 ∈ ℝ
391	2, 390	pm3.2i 475	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ ∧ _39 ∈ ℝ)
392		dp2cl 33210	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ _39 ∈ ℝ) → _0_39 ∈ ℝ)
393	391, 392	ax-mp 5	. . . . . . . . . . . 12 ⊢ _0_39 ∈ ℝ
394		dpcl 33221	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℕ0 ∧ _0_39 ∈ ℝ) → (1._0_39) ∈ ℝ)
395	1, 393, 394	mp2an 704	. . . . . . . . . . 11 ⊢ (1._0_39) ∈ ℝ
396	344, 395	pm3.2i 475	. . . . . . . . . 10 ⊢ ((1._0_3_8_83) ∈ ℝ ∧ (1._0_39) ∈ ℝ)
397		9nn 12345	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ ℕ
398		nnrp 13034	. . . . . . . . . . . . . . 15 ⊢ (9 ∈ ℕ → 9 ∈ ℝ+)
399	397, 398	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 9 ∈ ℝ+
400	182, 399	rpdp2cl 33212	. . . . . . . . . . . . 13 ⊢ _39 ∈ ℝ+
401	51, 400	rpdp2cl 33212	. . . . . . . . . . . 12 ⊢ _0_39 ∈ ℝ+
402	73, 352, 185, 184	dp2lt10 33214	. . . . . . . . . . . . . . 15 ⊢ _83 < ;10
403	73, 359, 402, 160	dp2ltsuc 33216	. . . . . . . . . . . . . 14 ⊢ _8_83 < 9
404	182, 360, 399, 403	dp2lt 33215	. . . . . . . . . . . . 13 ⊢ _3_8_83 < _39
405	51, 361, 400, 404	dp2lt 33215	. . . . . . . . . . . 12 ⊢ _0_3_8_83 < _0_39
406	1, 362, 401, 405	dplt 33234	. . . . . . . . . . 11 ⊢ (1._0_3_8_83) < (1._0_39)
407	365, 406	pm3.2i 475	. . . . . . . . . 10 ⊢ (0 ≤ (1._0_3_8_83) ∧ (1._0_3_8_83) < (1._0_39))
408	396, 407	pm3.2i 475	. . . . . . . . 9 ⊢ (((1._0_3_8_83) ∈ ℝ ∧ (1._0_39) ∈ ℝ) ∧ (0 ≤ (1._0_3_8_83) ∧ (1._0_3_8_83) < (1._0_39)))
409		ltmul12a 12077	. . . . . . . . 9 ⊢ (((((1._4_2_63) ∈ ℝ ∧ (1._4_27) ∈ ℝ) ∧ (0 ≤ (1._4_2_63) ∧ (1._4_2_63) < (1._4_27))) ∧ (((1._0_3_8_83) ∈ ℝ ∧ (1._0_39) ∈ ℝ) ∧ (0 ≤ (1._0_3_8_83) ∧ (1._0_3_8_83) < (1._0_39)))) → ((1._4_2_63) · (1._0_3_8_83)) < ((1._4_27) · (1._0_39)))
410	387, 408, 409	mp2an 704	. . . . . . . 8 ⊢ ((1._4_2_63) · (1._0_3_8_83)) < ((1._4_27) · (1._0_39))
411		6lt10 12857	. . . . . . . . 9 ⊢ 6 < ;10
412	73, 1	deccl 12732	. . . . . . . . . 10 ⊢ ;81 ∈ ℕ0
413		eqid 2762	. . . . . . . . . 10 ⊢ ;;816 = ;;816
414		eqid 2762	. . . . . . . . . 10 ⊢ ;10 = ;10
415		eqid 2762	. . . . . . . . . . . 12 ⊢ ;81 = ;81
416	73, 1, 269, 415	decsuc 12753	. . . . . . . . . . 11 ⊢ (;81 + 1) = ;82
417	73	dec0h 12744	. . . . . . . . . . . 12 ⊢ 8 = ;08
418	417	deceq1i 12724	. . . . . . . . . . 11 ⊢ ;82 = ;;082
419	416, 418	eqtri 2785	. . . . . . . . . 10 ⊢ (;81 + 1) = ;;082
420	110	addridi 11403	. . . . . . . . . 10 ⊢ (6 + 0) = 6
421	412, 98, 1, 51, 413, 414, 419, 420	decadd 12776	. . . . . . . . 9 ⊢ (;;816 + ;10) = ;;;0826
422	138	mul01i 11406	. . . . . . . . . 10 ⊢ (1 · 0) = 0
423	113	mul01i 11406	. . . . . . . . . . 11 ⊢ (4 · 0) = 0
424	51	dec0h 12744	. . . . . . . . . . 11 ⊢ 0 = ;00
425	423, 424	eqtri 2785	. . . . . . . . . 10 ⊢ (4 · 0) = ;00
426	113	addridi 11403	. . . . . . . . . . . 12 ⊢ (4 + 0) = 4
427	426	oveq1i 7422	. . . . . . . . . . 11 ⊢ ((4 + 0) + 0) = (4 + 0)
428	427, 426, 205	3eqtri 2789	. . . . . . . . . 10 ⊢ ((4 + 0) + 0) = ;04
429	1, 24, 1, 51, 51, 51, 24, 51, 116, 422, 203, 425, 428, 192	dpmul 33243	. . . . . . . . 9 ⊢ ((1.4) · (1.0)) = (1._40)
430		2t3e6 12413	. . . . . . . . . 10 ⊢ (2 · 3) = 6
431		9t2e18 12844	. . . . . . . . . . 11 ⊢ (9 · 2) = ;18
432	196, 197, 431	mulcomli 11224	. . . . . . . . . 10 ⊢ (2 · 9) = ;18
433		7t3e21 12832	. . . . . . . . . 10 ⊢ (7 · 3) = ;21
434		9t7e63 12849	. . . . . . . . . . 11 ⊢ (9 · 7) = ;63
435	196, 217, 434	mulcomli 11224	. . . . . . . . . 10 ⊢ (7 · 9) = ;63
436		eqid 2762	. . . . . . . . . . . . 13 ⊢ ;21 = ;21
437		eqid 2762	. . . . . . . . . . . . 13 ⊢ ;18 = ;18
438	159, 160	eqtri 2785	. . . . . . . . . . . . 13 ⊢ (1 + 8) = 9
439	181, 1, 1, 73, 436, 437, 224, 438	decadd 12776	. . . . . . . . . . . 12 ⊢ (;21 + ;18) = ;39
440	439	oveq1i 7422	. . . . . . . . . . 11 ⊢ ((;21 + ;18) + 6) = (;39 + 6)
441		eqid 2762	. . . . . . . . . . . 12 ⊢ ;39 = ;39
442		3p1e4 12391	. . . . . . . . . . . 12 ⊢ (3 + 1) = 4
443		9p6e15 12813	. . . . . . . . . . . 12 ⊢ (9 + 6) = ;15
444	182, 53, 98, 441, 442, 54, 443	decaddci 12783	. . . . . . . . . . 11 ⊢ (;39 + 6) = ;45
445	440, 444	eqtri 2785	. . . . . . . . . 10 ⊢ ((;21 + ;18) + 6) = ;45
446		6p4e10 12794	. . . . . . . . . 10 ⊢ (6 + 4) = ;10
447	181, 52, 182, 53, 98, 24, 54, 182, 430, 432, 433, 435, 445, 446	dpmul 33243	. . . . . . . . 9 ⊢ ((2.7) · (3.9)) = (;10._53)
448	1, 24	deccl 12732	. . . . . . . . . . 11 ⊢ ;14 ∈ ℕ0
449	448, 51	deccl 12732	. . . . . . . . . 10 ⊢ ;;140 ∈ ℕ0
450	417, 73	eqeltrri 2859	. . . . . . . . . 10 ⊢ ;08 ∈ ℕ0
451		eqid 2762	. . . . . . . . . 10 ⊢ ;;;1401 = ;;;1401
452		eqid 2762	. . . . . . . . . 10 ⊢ ;;082 = ;;082
453		eqid 2762	. . . . . . . . . . 11 ⊢ ;;140 = ;;140
454	417, 158	eqeltrri 2859	. . . . . . . . . . . 12 ⊢ ;08 ∈ ℂ
455		0cn 11204	. . . . . . . . . . . 12 ⊢ 0 ∈ ℂ
456	417	oveq1i 7422	. . . . . . . . . . . . 13 ⊢ (8 + 0) = (;08 + 0)
457	158	addridi 11403	. . . . . . . . . . . . 13 ⊢ (8 + 0) = 8
458	456, 457	eqtr3i 2787	. . . . . . . . . . . 12 ⊢ (;08 + 0) = 8
459	454, 455, 458	addcomli 11408	. . . . . . . . . . 11 ⊢ (0 + ;08) = 8
460	448, 51, 450, 453, 459	decaddi 12782	. . . . . . . . . 10 ⊢ (;;140 + ;08) = ;;148
461	449, 1, 450, 181, 451, 452, 460, 230	decadd 12776	. . . . . . . . 9 ⊢ (;;;1401 + ;;082) = ;;;1483
462		4t4e16 12821	. . . . . . . . . . 11 ⊢ (4 · 4) = ;16
463		9t4e36 12846	. . . . . . . . . . . 12 ⊢ (9 · 4) = ;36
464	196, 113, 463	mulcomli 11224	. . . . . . . . . . 11 ⊢ (4 · 9) = ;36
465	196	mulridi 11219	. . . . . . . . . . . . 13 ⊢ (9 · 1) = 9
466	465, 188	eqtri 2785	. . . . . . . . . . . 12 ⊢ (9 · 1) = ;09
467	196, 138, 466	mulcomli 11224	. . . . . . . . . . 11 ⊢ (1 · 9) = ;09
468	182, 98	deccl 12732	. . . . . . . . . . . . . . 15 ⊢ ;36 ∈ ℕ0
469	468	nn0cni 12522	. . . . . . . . . . . . . 14 ⊢ ;36 ∈ ℂ
470		eqid 2762	. . . . . . . . . . . . . . 15 ⊢ ;36 = ;36
471	182, 98, 24, 470, 442, 51, 446	decaddci 12783	. . . . . . . . . . . . . 14 ⊢ (;36 + 4) = ;40
472	469, 113, 471	addcomli 11408	. . . . . . . . . . . . 13 ⊢ (4 + ;36) = ;40
473	472	oveq1i 7422	. . . . . . . . . . . 12 ⊢ ((4 + ;36) + 0) = (;40 + 0)
474	24, 51	deccl 12732	. . . . . . . . . . . . . 14 ⊢ ;40 ∈ ℕ0
475	474	nn0cni 12522	. . . . . . . . . . . . 13 ⊢ ;40 ∈ ℂ
476	475	addridi 11403	. . . . . . . . . . . 12 ⊢ (;40 + 0) = ;40
477	473, 476	eqtri 2785	. . . . . . . . . . 11 ⊢ ((4 + ;36) + 0) = ;40
478	1, 98, 24, 135, 269, 51, 446	decaddci 12783	. . . . . . . . . . 11 ⊢ (;16 + 4) = ;20
479	24, 1, 24, 53, 51, 24, 51, 53, 462, 464, 204, 467, 477, 478	dpmul 33243	. . . . . . . . . 10 ⊢ ((4.1) · (4.9)) = (;20._09)
480		eqid 2762	. . . . . . . . . . . . 13 ⊢ ;27 = ;27
481	230	oveq1i 7422	. . . . . . . . . . . . . 14 ⊢ ((1 + 2) + 1) = (3 + 1)
482	481, 442	eqtri 2785	. . . . . . . . . . . . 13 ⊢ ((1 + 2) + 1) = 4
483	1, 24, 181, 52, 268, 480, 482, 1, 225	decaddc 12777	. . . . . . . . . . . 12 ⊢ (;14 + ;27) = ;41
484	1, 24, 181, 52, 24, 1, 483	dpadd 33241	. . . . . . . . . . 11 ⊢ ((1.4) + (2.7)) = (4.1)
485		3cn 12328	. . . . . . . . . . . . . 14 ⊢ 3 ∈ ℂ
486	485, 138, 442	addcomli 11408	. . . . . . . . . . . . 13 ⊢ (1 + 3) = 4
487	196	addlidi 11404	. . . . . . . . . . . . 13 ⊢ (0 + 9) = 9
488	1, 51, 182, 53, 414, 441, 486, 487	decadd 12776	. . . . . . . . . . . 12 ⊢ (;10 + ;39) = ;49
489	1, 51, 182, 53, 24, 53, 488	dpadd 33241	. . . . . . . . . . 11 ⊢ ((1.0) + (3.9)) = (4.9)
490	484, 489	oveq12i 7424	. . . . . . . . . 10 ⊢ (((1.4) + (2.7)) · ((1.0) + (3.9))) = ((4.1) · (4.9))
491	1, 24, 73, 1, 268, 415, 438, 210	decadd 12776	. . . . . . . . . . . . . 14 ⊢ (;14 + ;81) = ;95
492	448, 51, 412, 98, 453, 413, 491, 111	decadd 12776	. . . . . . . . . . . . 13 ⊢ (;;140 + ;;816) = ;;956
493	1, 24, 51, 73, 1, 53, 98, 54, 98, 492	dpadd3 33242	. . . . . . . . . . . 12 ⊢ ((1._40) + (8._16)) = (9._56)
494	493	oveq1i 7422	. . . . . . . . . . 11 ⊢ (((1._40) + (8._16)) + (;10._53)) = ((9._56) + (;10._53))
495	181, 51	deccl 12732	. . . . . . . . . . . 12 ⊢ ;20 ∈ ℕ0
496	53, 54	deccl 12732	. . . . . . . . . . . . 13 ⊢ ;95 ∈ ℕ0
497	130, 54	deccl 12732	. . . . . . . . . . . . 13 ⊢ ;;105 ∈ ℕ0
498		eqid 2762	. . . . . . . . . . . . 13 ⊢ ;;956 = ;;956
499		eqid 2762	. . . . . . . . . . . . 13 ⊢ ;;;1053 = ;;;1053
500		eqid 2762	. . . . . . . . . . . . . 14 ⊢ ;95 = ;95
501		eqid 2762	. . . . . . . . . . . . . 14 ⊢ ;;105 = ;;105
502		dec10p 12765	. . . . . . . . . . . . . . . . 17 ⊢ (;10 + 9) = ;19
503	283, 196, 502	addcomli 11408	. . . . . . . . . . . . . . . 16 ⊢ (9 + ;10) = ;19
504	503	oveq1i 7422	. . . . . . . . . . . . . . 15 ⊢ ((9 + ;10) + 1) = (;19 + 1)
505		eqid 2762	. . . . . . . . . . . . . . . 16 ⊢ ;19 = ;19
506	1, 53, 1, 505, 269, 51, 194	decaddci 12783	. . . . . . . . . . . . . . 15 ⊢ (;19 + 1) = ;20
507	504, 506	eqtri 2785	. . . . . . . . . . . . . 14 ⊢ ((9 + ;10) + 1) = ;20
508		5p5e10 12793	. . . . . . . . . . . . . 14 ⊢ (5 + 5) = ;10
509	53, 54, 130, 54, 500, 501, 507, 51, 508	decaddc 12777	. . . . . . . . . . . . 13 ⊢ (;95 + ;;105) = ;;200
510	496, 98, 497, 182, 498, 499, 509, 233	decadd 12776	. . . . . . . . . . . 12 ⊢ (;;956 + ;;;1053) = ;;;2009
511	53, 54, 98, 130, 54, 495, 182, 51, 53, 510	dpadd3 33242	. . . . . . . . . . 11 ⊢ ((9._56) + (;10._53)) = (;20._09)
512	494, 511	eqtri 2785	. . . . . . . . . 10 ⊢ (((1._40) + (8._16)) + (;10._53)) = (;20._09)
513	479, 490, 512	3eqtr4i 2795	. . . . . . . . 9 ⊢ (((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 33244	. . . . . . . 8 ⊢ ((1._4_27) · (1._0_39)) < (1._4_83)
515	375, 395	remulcli 11231	. . . . . . . . 9 ⊢ ((1._4_27) · (1._0_39)) ∈ ℝ
516	345, 515, 350	lttri 11342	. . . . . . . 8 ⊢ ((((1._4_2_63) · (1._0_3_8_83)) < ((1._4_27) · (1._0_39)) ∧ ((1._4_27) · (1._0_39)) < (1._4_83)) → ((1._4_2_63) · (1._0_3_8_83)) < (1._4_83))
517	410, 514, 516	mp2an 704	. . . . . . 7 ⊢ ((1._4_2_63) · (1._0_3_8_83)) < (1._4_83)
518	367, 517	pm3.2i 475	. . . . . 6 ⊢ (0 ≤ ((1._4_2_63) · (1._0_3_8_83)) ∧ ((1._4_2_63) · (1._0_3_8_83)) < (1._4_83))
519	351, 518	pm3.2i 475	. . . . 5 ⊢ ((((1._4_2_63) · (1._0_3_8_83)) ∈ ℝ ∧ (1._4_83) ∈ ℝ) ∧ (0 ≤ ((1._4_2_63) · (1._0_3_8_83)) ∧ ((1._4_2_63) · (1._0_3_8_83)) < (1._4_83)))
520		ltmul12a 12077	. . . . 5 ⊢ (((((((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ ∧ (1._6_51) ∈ ℝ) ∧ (0 ≤ (((1._0_7_9_9_55)↑2) · (1._4_14)) ∧ (((1._0_7_9_9_55)↑2) · (1._4_14)) < (1._6_51))) ∧ ((((1._4_2_63) · (1._0_3_8_83)) ∈ ℝ ∧ (1._4_83) ∈ ℝ) ∧ (0 ≤ ((1._4_2_63) · (1._0_3_8_83)) ∧ ((1._4_2_63) · (1._0_3_8_83)) < (1._4_83)))) → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) < ((1._6_51) · (1._4_83)))
521	316, 519, 520	mp2an 704	. . . 4 ⊢ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) < ((1._6_51) · (1._4_83))
522	24, 181	deccl 12732	. . . . 5 ⊢ ;42 ∈ ℕ0
523	495, 24	deccl 12732	. . . . . 6 ⊢ ;;204 ∈ ℕ0
524		eqid 2762	. . . . . 6 ⊢ ;;;2042 = ;;;2042
525		eqid 2762	. . . . . 6 ⊢ ;42 = ;42
526		eqid 2762	. . . . . . 7 ⊢ ;;204 = ;;204
527	495, 24, 24, 526, 277	decaddi 12782	. . . . . 6 ⊢ (;;204 + 4) = ;;208
528		2p2e4 12381	. . . . . 6 ⊢ (2 + 2) = 4
529	523, 181, 24, 181, 524, 525, 527, 528	decadd 12776	. . . . 5 ⊢ (;;;2042 + ;42) = ;;;2084
530	446	oveq1i 7422	. . . . . . 7 ⊢ ((6 + 4) + 2) = (;10 + 2)
531		dec10p 12765	. . . . . . 7 ⊢ (;10 + 2) = ;12
532	530, 531	eqtri 2785	. . . . . 6 ⊢ ((6 + 4) + 2) = ;12
533	1, 98, 1, 24, 181, 1, 181, 24, 116, 204, 215, 216, 532, 269	dpmul 33243	. . . . 5 ⊢ ((1.6) · (1.4)) = (2._24)
534		8t5e40 12840	. . . . . . 7 ⊢ (8 · 5) = ;40
535	158, 256, 534	mulcomli 11224	. . . . . 6 ⊢ (5 · 8) = ;40
536		5t3e15 12823	. . . . . 6 ⊢ (5 · 3) = ;15
537	158	mullidi 11220	. . . . . 6 ⊢ (1 · 8) = 8
538	485	mullidi 11220	. . . . . . 7 ⊢ (1 · 3) = 3
539	182	dec0h 12744	. . . . . . 7 ⊢ 3 = ;03
540	538, 539	eqtri 2785	. . . . . 6 ⊢ (1 · 3) = ;03
541	235	nn0cni 12522	. . . . . . . . 9 ⊢ ;15 ∈ ℂ
542		8p5e13 12805	. . . . . . . . . . 11 ⊢ (8 + 5) = ;13
543	158, 256, 542	addcomli 11408	. . . . . . . . . 10 ⊢ (5 + 8) = ;13
544	1, 54, 73, 245, 269, 182, 543	decaddci 12783	. . . . . . . . 9 ⊢ (;15 + 8) = ;23
545	541, 158, 544	addcomli 11408	. . . . . . . 8 ⊢ (8 + ;15) = ;23
546	545	oveq1i 7422	. . . . . . 7 ⊢ ((8 + ;15) + 0) = (;23 + 0)
547	181, 182	deccl 12732	. . . . . . . . 9 ⊢ ;23 ∈ ℕ0
548	547	nn0cni 12522	. . . . . . . 8 ⊢ ;23 ∈ ℂ
549	548	addridi 11403	. . . . . . 7 ⊢ (;23 + 0) = ;23
550	546, 549	eqtri 2785	. . . . . 6 ⊢ ((8 + ;15) + 0) = ;23
551		eqid 2762	. . . . . . 7 ⊢ ;40 = ;40
552	197	addlidi 11404	. . . . . . 7 ⊢ (0 + 2) = 2
553	24, 51, 181, 551, 552	decaddi 12782	. . . . . 6 ⊢ (;40 + 2) = ;42
554	54, 1, 73, 182, 51, 181, 182, 182, 535, 536, 537, 540, 550, 553	dpmul 33243	. . . . 5 ⊢ ((5.1) · (8.3)) = (;42._33)
555	181, 181	deccl 12732	. . . . . . 7 ⊢ ;22 ∈ ℕ0
556	555, 24	deccl 12732	. . . . . 6 ⊢ ;;224 ∈ ℕ0
557		eqid 2762	. . . . . 6 ⊢ ;;;2241 = ;;;2241
558		eqid 2762	. . . . . 6 ⊢ ;;208 = ;;208
559		eqid 2762	. . . . . . 7 ⊢ ;;224 = ;;224
560		eqid 2762	. . . . . . 7 ⊢ ;20 = ;20
561		eqid 2762	. . . . . . . 8 ⊢ ;22 = ;22
562	181, 181, 181, 561, 528	decaddi 12782	. . . . . . 7 ⊢ (;22 + 2) = ;24
563	555, 24, 181, 51, 559, 560, 562, 426	decadd 12776	. . . . . 6 ⊢ (;;224 + ;20) = ;;244
564	556, 1, 495, 73, 557, 558, 563, 438	decadd 12776	. . . . 5 ⊢ (;;;2241 + ;;208) = ;;;2449
565	555, 98	deccl 12732	. . . . . . . 8 ⊢ ;;226 ∈ ℕ0
566	522, 182	deccl 12732	. . . . . . . 8 ⊢ ;;423 ∈ ℕ0
567		eqid 2762	. . . . . . . 8 ⊢ ;;;2266 = ;;;2266
568		eqid 2762	. . . . . . . 8 ⊢ ;;;4233 = ;;;4233
569		eqid 2762	. . . . . . . . 9 ⊢ ;;226 = ;;226
570		eqid 2762	. . . . . . . . 9 ⊢ ;;423 = ;;423
571	113, 197, 289	addcomli 11408	. . . . . . . . . 10 ⊢ (2 + 4) = 6
572	181, 181, 24, 181, 561, 525, 571, 528	decadd 12776	. . . . . . . . 9 ⊢ (;22 + ;42) = ;64
573	555, 98, 522, 182, 569, 570, 572, 233	decadd 12776	. . . . . . . 8 ⊢ (;;226 + ;;423) = ;;649
574	565, 98, 566, 182, 567, 568, 573, 233	decadd 12776	. . . . . . 7 ⊢ (;;;2266 + ;;;4233) = ;;;6499
575	555, 98, 98, 522, 182, 100, 182, 53, 53, 574	dpadd3 33242	. . . . . 6 ⊢ ((;22._66) + (;42._33)) = (;64._99)
576	495	nn0cni 12522	. . . . . . . . . . 11 ⊢ ;20 ∈ ℂ
577	181, 51, 181, 560, 552	decaddi 12782	. . . . . . . . . . 11 ⊢ (;20 + 2) = ;22
578	576, 197, 577	addcomli 11408	. . . . . . . . . 10 ⊢ (2 + ;20) = ;22
579	181, 181, 495, 24, 561, 526, 578, 571	decadd 12776	. . . . . . . . 9 ⊢ (;22 + ;;204) = ;;226
580	555, 24, 523, 181, 559, 524, 579, 289	decadd 12776	. . . . . . . 8 ⊢ (;;224 + ;;;2042) = ;;;2266
581	181, 181, 24, 495, 24, 555, 181, 98, 98, 580	dpadd3 33242	. . . . . . 7 ⊢ ((2._24) + (;20._42)) = (;22._66)
582	581	oveq1i 7422	. . . . . 6 ⊢ (((2._24) + (;20._42)) + (;42._33)) = ((;22._66) + (;42._33))
583		eqid 2762	. . . . . . . . . 10 ⊢ ;51 = ;51
584	1, 98, 54, 1, 135, 583, 257, 140	decadd 12776	. . . . . . . . 9 ⊢ (;16 + ;51) = ;67
585	1, 98, 54, 1, 98, 52, 584	dpadd 33241	. . . . . . . 8 ⊢ ((1.6) + (5.1)) = (6.7)
586		eqid 2762	. . . . . . . . . 10 ⊢ ;83 = ;83
587	1, 24, 73, 182, 268, 586, 438, 302	decadd 12776	. . . . . . . . 9 ⊢ (;14 + ;83) = ;97
588	1, 24, 73, 182, 53, 52, 587	dpadd 33241	. . . . . . . 8 ⊢ ((1.4) + (8.3)) = (9.7)
589	585, 588	oveq12i 7424	. . . . . . 7 ⊢ (((1.6) + (5.1)) · ((1.4) + (8.3))) = ((6.7) · (9.7))
590		9t6e54 12848	. . . . . . . . 9 ⊢ (9 · 6) = ;54
591	196, 110, 590	mulcomli 11224	. . . . . . . 8 ⊢ (6 · 9) = ;54
592		7t6e42 12835	. . . . . . . . 9 ⊢ (7 · 6) = ;42
593	217, 110, 592	mulcomli 11224	. . . . . . . 8 ⊢ (6 · 7) = ;42
594		7t7e49 12836	. . . . . . . 8 ⊢ (7 · 7) = ;49
595		eqid 2762	. . . . . . . . . . 11 ⊢ ;63 = ;63
596		3p2e5 12397	. . . . . . . . . . 11 ⊢ (3 + 2) = 5
597	98, 182, 24, 181, 595, 525, 446, 596	decadd 12776	. . . . . . . . . 10 ⊢ (;63 + ;42) = ;;105
598	597	oveq1i 7422	. . . . . . . . 9 ⊢ ((;63 + ;42) + 4) = (;;105 + 4)
599		5p4e9 12404	. . . . . . . . . 10 ⊢ (5 + 4) = 9
600	130, 54, 24, 501, 599	decaddi 12782	. . . . . . . . 9 ⊢ (;;105 + 4) = ;;109
601	598, 600	eqtri 2785	. . . . . . . 8 ⊢ ((;63 + ;42) + 4) = ;;109
602		eqid 2762	. . . . . . . . 9 ⊢ ;54 = ;54
603	54, 24, 1, 51, 602, 414, 246, 426	decadd 12776	. . . . . . . 8 ⊢ (;54 + ;10) = ;64
604	98, 52, 53, 52, 24, 130, 53, 53, 591, 593, 435, 594, 601, 603	dpmul 33243	. . . . . . 7 ⊢ ((6.7) · (9.7)) = (;64._99)
605	589, 604	eqtri 2785	. . . . . 6 ⊢ (((1.6) + (5.1)) · ((1.4) + (8.3))) = (;64._99)
606	575, 582, 605	3eqtr4ri 2796	. . . . 5 ⊢ (((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 33244	. . . 4 ⊢ ((1._6_51) · (1._4_83)) < (2._4_49)
608	33, 345	remulcli 11231	. . . . 5 ⊢ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) ∈ ℝ
609	43, 350	remulcli 11231	. . . . 5 ⊢ ((1._6_51) · (1._4_83)) ∈ ℝ
610	24, 399	rpdp2cl 33212	. . . . . . . 8 ⊢ _49 ∈ ℝ+
611	24, 610	rpdp2cl 33212	. . . . . . 7 ⊢ _4_49 ∈ ℝ+
612	181, 611	rpdpcl 33233	. . . . . 6 ⊢ (2._4_49) ∈ ℝ+
613		rpre 13031	. . . . . 6 ⊢ ((2._4_49) ∈ ℝ+ → (2._4_49) ∈ ℝ)
614	612, 613	ax-mp 5	. . . . 5 ⊢ (2._4_49) ∈ ℝ
615	608, 609, 614	lttri 11342	. . . 4 ⊢ ((((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) < ((1._6_51) · (1._4_83)) ∧ ((1._6_51) · (1._4_83)) < (2._4_49)) → ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) < (2._4_49))
616	521, 607, 615	mp2an 704	. . 3 ⊢ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) < (2._4_49)
617		3pos 12355	. . . 4 ⊢ 0 < 3
618	608, 614, 319	ltmul2i 12142	. . . 4 ⊢ (0 < 3 → (((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) < (2._4_49) ↔ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) < (3 · (2._4_49))))
619	617, 618	ax-mp 5	. . 3 ⊢ (((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) < (2._4_49) ↔ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) < (3 · (2._4_49)))
620	616, 619	mpbi 233	. 2 ⊢ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) < (3 · (2._4_49))
621	119	dp2eq2i 33206	. . . . . . 7 ⊢ _0_00 = _00
622	621, 119	eqtri 2785	. . . . . 6 ⊢ _0_00 = 0
623	622	oveq2i 7423	. . . . 5 ⊢ (3._0_00) = (3.0)
624	182	dp0u 33231	. . . . 5 ⊢ (3.0) = 3
625	623, 624	eqtr2i 2786	. . . 4 ⊢ 3 = (3._0_00)
626	625	oveq1i 7422	. . 3 ⊢ (3 · (2._4_49)) = ((3._0_00) · (2._4_49))
627	448, 52	deccl 12732	. . . . . . 7 ⊢ ;;147 ∈ ℕ0
628	627, 51	deccl 12732	. . . . . 6 ⊢ ;;;1470 ∈ ℕ0
629	628	nn0cni 12522	. . . . 5 ⊢ ;;;1470 ∈ ℂ
630	629	addridi 11403	. . . 4 ⊢ (;;;1470 + 0) = ;;;1470
631		3t2e6 12412	. . . . 5 ⊢ (3 · 2) = 6
632		4t3e12 12820	. . . . . 6 ⊢ (4 · 3) = ;12
633	113, 485, 632	mulcomli 11224	. . . . 5 ⊢ (3 · 4) = ;12
634	197	mul02i 11405	. . . . 5 ⊢ (0 · 2) = 0
635	113, 455, 425	mulcomli 11224	. . . . 5 ⊢ (0 · 4) = ;00
636	51, 51, 1, 181, 424, 300, 153, 552	decadd 12776	. . . . . . 7 ⊢ (0 + ;12) = ;12
637	636	oveq1i 7422	. . . . . 6 ⊢ ((0 + ;12) + 0) = (;12 + 0)
638	281	nn0cni 12522	. . . . . . 7 ⊢ ;12 ∈ ℂ
639	638	addridi 11403	. . . . . 6 ⊢ (;12 + 0) = ;12
640	637, 639	eqtri 2785	. . . . 5 ⊢ ((0 + ;12) + 0) = ;12
641	182, 51, 181, 24, 51, 1, 181, 51, 631, 633, 634, 635, 640, 140	dpmul 33243	. . . 4 ⊢ ((3.0) · (2.4)) = (7._20)
642	51	dp0u 33231	. . . . . . 7 ⊢ (0.0) = 0
643	642	oveq1i 7422	. . . . . 6 ⊢ ((0.0) · (4.9)) = (0 · (4.9))
644		dpcl 33221	. . . . . . . . 9 ⊢ ((4 ∈ ℕ0 ∧ 9 ∈ ℝ) → (4.9) ∈ ℝ)
645	24, 4, 644	mp2an 704	. . . . . . . 8 ⊢ (4.9) ∈ ℝ
646	645	recni 11229	. . . . . . 7 ⊢ (4.9) ∈ ℂ
647	646	mul02i 11405	. . . . . 6 ⊢ (0 · (4.9)) = 0
648	643, 647	eqtri 2785	. . . . 5 ⊢ ((0.0) · (4.9)) = 0
649	119	oveq2i 7423	. . . . . 6 ⊢ (0._00) = (0.0)
650	649, 642	eqtri 2785	. . . . 5 ⊢ (0._00) = 0
651	648, 650	eqtr4i 2788	. . . 4 ⊢ ((0.0) · (4.9)) = (0._00)
652	52, 181	deccl 12732	. . . . . 6 ⊢ ;72 ∈ ℕ0
653	652, 51	deccl 12732	. . . . 5 ⊢ ;;720 ∈ ℕ0
654		eqid 2762	. . . . 5 ⊢ ;;;7201 = ;;;7201
655		eqid 2762	. . . . 5 ⊢ ;;147 = ;;147
656		eqid 2762	. . . . . 6 ⊢ ;;720 = ;;720
657	52, 181, 224, 263	decsuc 12753	. . . . . 6 ⊢ (;72 + 1) = ;73
658	652, 51, 1, 24, 656, 268, 657, 114	decadd 12776	. . . . 5 ⊢ (;;720 + ;14) = ;;734
659	653, 1, 448, 52, 654, 655, 658, 274	decadd 12776	. . . 4 ⊢ (;;;7201 + ;;147) = ;;;7348
660	642	oveq2i 7423	. . . . . . . 8 ⊢ ((3.0) + (0.0)) = ((3.0) + 0)
661	624, 485	eqeltri 2858	. . . . . . . . 9 ⊢ (3.0) ∈ ℂ
662	661	addridi 11403	. . . . . . . 8 ⊢ ((3.0) + 0) = (3.0)
663	660, 662	eqtri 2785	. . . . . . 7 ⊢ ((3.0) + (0.0)) = (3.0)
664		eqid 2762	. . . . . . . . 9 ⊢ ;49 = ;49
665	571	oveq1i 7422	. . . . . . . . . 10 ⊢ ((2 + 4) + 1) = (6 + 1)
666	665, 140	eqtri 2785	. . . . . . . . 9 ⊢ ((2 + 4) + 1) = 7
667		9p4e13 12811	. . . . . . . . . 10 ⊢ (9 + 4) = ;13
668	196, 113, 667	addcomli 11408	. . . . . . . . 9 ⊢ (4 + 9) = ;13
669	181, 24, 24, 53, 223, 664, 666, 182, 668	decaddc 12777	. . . . . . . 8 ⊢ (;24 + ;49) = ;73
670	181, 24, 24, 53, 52, 182, 669	dpadd 33241	. . . . . . 7 ⊢ ((2.4) + (4.9)) = (7.3)
671	663, 670	oveq12i 7424	. . . . . 6 ⊢ (((3.0) + (0.0)) · ((2.4) + (4.9))) = ((3.0) · (7.3))
672	217, 485, 433	mulcomli 11224	. . . . . . 7 ⊢ (3 · 7) = ;21
673		3t3e9 12414	. . . . . . 7 ⊢ (3 · 3) = 9
674	217	mul01i 11406	. . . . . . . 8 ⊢ (7 · 0) = 0
675	217, 455, 674	mulcomli 11224	. . . . . . 7 ⊢ (0 · 7) = 0
676	485	mul01i 11406	. . . . . . . . 9 ⊢ (3 · 0) = 0
677	676, 424	eqtri 2785	. . . . . . . 8 ⊢ (3 · 0) = ;00
678	485, 455, 677	mulcomli 11224	. . . . . . 7 ⊢ (0 · 3) = ;00
679	196	addridi 11403	. . . . . . . . . 10 ⊢ (9 + 0) = 9
680	679	oveq1i 7422	. . . . . . . . 9 ⊢ ((9 + 0) + 0) = (9 + 0)
681	680, 679, 188	3eqtri 2789	. . . . . . . 8 ⊢ ((9 + 0) + 0) = ;09
682	196, 455	addcomi 11407	. . . . . . . . . 10 ⊢ (9 + 0) = (0 + 9)
683	682	oveq1i 7422	. . . . . . . . 9 ⊢ ((9 + 0) + 0) = ((0 + 9) + 0)
684	683	eqeq1i 2767	. . . . . . . 8 ⊢ (((9 + 0) + 0) = ;09 ↔ ((0 + 9) + 0) = ;09)
685	681, 684	mpbi 233	. . . . . . 7 ⊢ ((0 + 9) + 0) = ;09
686	181, 1, 51, 436, 192	decaddi 12782	. . . . . . 7 ⊢ (;21 + 0) = ;21
687	182, 51, 52, 182, 51, 51, 53, 51, 672, 673, 675, 678, 685, 686	dpmul 33243	. . . . . 6 ⊢ ((3.0) · (7.3)) = (;21._90)
688	671, 687	eqtri 2785	. . . . 5 ⊢ (((3.0) + (0.0)) · ((2.4) + (4.9))) = (;21._90)
689	650	oveq2i 7423	. . . . . 6 ⊢ (((7._20) + (;14._70)) + (0._00)) = (((7._20) + (;14._70)) + 0)
690	318, 2	pm3.2i 475	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ ∧ 0 ∈ ℝ)
691		dp2cl 33210	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ 0 ∈ ℝ) → _20 ∈ ℝ)
692	690, 691	ax-mp 5	. . . . . . . . . 10 ⊢ _20 ∈ ℝ
693		dpcl 33221	. . . . . . . . . 10 ⊢ ((7 ∈ ℕ0 ∧ _20 ∈ ℝ) → (7._20) ∈ ℝ)
694	52, 692, 693	mp2an 704	. . . . . . . . 9 ⊢ (7._20) ∈ ℝ
695	694	recni 11229	. . . . . . . 8 ⊢ (7._20) ∈ ℂ
696	3, 2	pm3.2i 475	. . . . . . . . . . 11 ⊢ (7 ∈ ℝ ∧ 0 ∈ ℝ)
697		dp2cl 33210	. . . . . . . . . . 11 ⊢ ((7 ∈ ℝ ∧ 0 ∈ ℝ) → _70 ∈ ℝ)
698	696, 697	ax-mp 5	. . . . . . . . . 10 ⊢ _70 ∈ ℝ
699		dpcl 33221	. . . . . . . . . 10 ⊢ ((;14 ∈ ℕ0 ∧ _70 ∈ ℝ) → (;14._70) ∈ ℝ)
700	448, 698, 699	mp2an 704	. . . . . . . . 9 ⊢ (;14._70) ∈ ℝ
701	700	recni 11229	. . . . . . . 8 ⊢ (;14._70) ∈ ℂ
702	695, 701	addcli 11221	. . . . . . 7 ⊢ ((7._20) + (;14._70)) ∈ ℂ
703	702	addridi 11403	. . . . . 6 ⊢ (((7._20) + (;14._70)) + 0) = ((7._20) + (;14._70))
704		eqid 2762	. . . . . . . 8 ⊢ ;;;1470 = ;;;1470
705	448	nn0cni 12522	. . . . . . . . . 10 ⊢ ;14 ∈ ℂ
706	705, 217, 270	addcomli 11408	. . . . . . . . 9 ⊢ (7 + ;14) = ;21
707		7p2e9 12407	. . . . . . . . . 10 ⊢ (7 + 2) = 9
708	217, 197, 707	addcomli 11408	. . . . . . . . 9 ⊢ (2 + 7) = 9
709	52, 181, 448, 52, 263, 655, 706, 708	decadd 12776	. . . . . . . 8 ⊢ (;72 + ;;147) = ;;219
710		00id 11391	. . . . . . . 8 ⊢ (0 + 0) = 0
711	652, 51, 627, 51, 656, 704, 709, 710	decadd 12776	. . . . . . 7 ⊢ (;;720 + ;;;1470) = ;;;2190
712	52, 181, 51, 448, 52, 293, 51, 53, 51, 711	dpadd3 33242	. . . . . 6 ⊢ ((7._20) + (;14._70)) = (;21._90)
713	689, 703, 712	3eqtri 2789	. . . . 5 ⊢ (((7._20) + (;14._70)) + (0._00)) = (;21._90)
714	688, 713	eqtr4i 2788	. . . 4 ⊢ (((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 33244	. . 3 ⊢ ((3._0_00) · (2._4_49)) < (7._3_48)
716	626, 715	eqbrtri 5131	. 2 ⊢ (3 · (2._4_49)) < (7._3_48)
717	319, 608	remulcli 11231	. . 3 ⊢ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) ∈ ℝ
718	319, 614	remulcli 11231	. . 3 ⊢ (3 · (2._4_49)) ∈ ℝ
719		nnrp 13034	. . . . . . . 8 ⊢ (8 ∈ ℕ → 8 ∈ ℝ+)
720	63, 719	ax-mp 5	. . . . . . 7 ⊢ 8 ∈ ℝ+
721	24, 720	rpdp2cl 33212	. . . . . 6 ⊢ _48 ∈ ℝ+
722	182, 721	rpdp2cl 33212	. . . . 5 ⊢ _3_48 ∈ ℝ+
723	52, 722	rpdpcl 33233	. . . 4 ⊢ (7._3_48) ∈ ℝ+
724		rpre 13031	. . . 4 ⊢ ((7._3_48) ∈ ℝ+ → (7._3_48) ∈ ℝ)
725	723, 724	ax-mp 5	. . 3 ⊢ (7._3_48) ∈ ℝ
726	717, 718, 725	lttri 11342	. 2 ⊢ (((3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) < (3 · (2._4_49)) ∧ (3 · (2._4_49)) < (7._3_48)) → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) < (7._3_48))
727	620, 716, 726	mp2an 704	1 ⊢ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) < (7._3_48)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 400   = wceq 1569   ∈ wcel 2142   class class class wbr 5108  (class class class)co 7412  ℂcc 11104  ℝcr 11105  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111   < clt 11249   ≤ cle 11250  ℕcn 12239  2c2 12301  3c3 12302  4c4 12303  5c5 12304  6c6 12305  7c7 12306  8c8 12307  9c9 12308  ℕ₀cn0 12510  ;cdc 12717  ℝ⁺crp 13022  ↑cexp 14104  _cdp2 33201  .cdp 33218

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5555  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-we 5615  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7861  df-2nd 7985  df-frecs 8276  df-wrecs 8307  df-recs 8356  df-rdg 8395  df-er 8692  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-sub 11449  df-neg 11450  df-div 11878  df-nn 12240  df-2 12309  df-3 12310  df-4 12311  df-5 12312  df-6 12313  df-7 12314  df-8 12315  df-9 12316  df-n0 12511  df-z 12598  df-dec 12718  df-uz 12869  df-rp 13023  df-seq 14045  df-exp 14105  df-dp2 33202  df-dp 33219

This theorem is used by:  hgt750leme  35054