Theorem hgt750lem2 34667

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 12542	. . . . . . . . . 10 ⊢ 1 ∈ ℕ0
2		0re 11263	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
3		7re 12359	. . . . . . . . . . . . . 14 ⊢ 7 ∈ ℝ
4		9re 12365	. . . . . . . . . . . . . . . 16 ⊢ 9 ∈ ℝ
5		5re 12353	. . . . . . . . . . . . . . . . . . . 20 ⊢ 5 ∈ ℝ
6	5, 5	pm3.2i 470	. . . . . . . . . . . . . . . . . . 19 ⊢ (5 ∈ ℝ ∧ 5 ∈ ℝ)
7		dp2cl 32862	. . . . . . . . . . . . . . . . . . 19 ⊢ ((5 ∈ ℝ ∧ 5 ∈ ℝ) → _55 ∈ ℝ)
8	6, 7	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ _55 ∈ ℝ
9	4, 8	pm3.2i 470	. . . . . . . . . . . . . . . . 17 ⊢ (9 ∈ ℝ ∧ _55 ∈ ℝ)
10		dp2cl 32862	. . . . . . . . . . . . . . . . 17 ⊢ ((9 ∈ ℝ ∧ _55 ∈ ℝ) → _9_55 ∈ ℝ)
11	9, 10	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ _9_55 ∈ ℝ
12	4, 11	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ (9 ∈ ℝ ∧ _9_55 ∈ ℝ)
13		dp2cl 32862	. . . . . . . . . . . . . . 15 ⊢ ((9 ∈ ℝ ∧ _9_55 ∈ ℝ) → _9_9_55 ∈ ℝ)
14	12, 13	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ _9_9_55 ∈ ℝ
15	3, 14	pm3.2i 470	. . . . . . . . . . . . 13 ⊢ (7 ∈ ℝ ∧ _9_9_55 ∈ ℝ)
16		dp2cl 32862	. . . . . . . . . . . . 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 470	. . . . . . . . . . 11 ⊢ (0 ∈ ℝ ∧ _7_9_9_55 ∈ ℝ)
19		dp2cl 32862	. . . . . . . . . . 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 32873	. . . . . . . . . 10 ⊢ ((1 ∈ ℕ0 ∧ _0_7_9_9_55 ∈ ℝ) → (1._0_7_9_9_55) ∈ ℝ)
22	1, 20, 21	mp2an 692	. . . . . . . . 9 ⊢ (1._0_7_9_9_55) ∈ ℝ
23	22	resqcli 14225	. . . . . . . 8 ⊢ ((1._0_7_9_9_55)↑2) ∈ ℝ
24		4nn0 12545	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ0
25		4nn 12349	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℕ
26		nnrp 13046	. . . . . . . . . . . . 13 ⊢ (4 ∈ ℕ → 4 ∈ ℝ+)
27	25, 26	ax-mp 5	. . . . . . . . . . . 12 ⊢ 4 ∈ ℝ+
28	1, 27	rpdp2cl 32864	. . . . . . . . . . 11 ⊢ _14 ∈ ℝ+
29	24, 28	rpdp2cl 32864	. . . . . . . . . 10 ⊢ _4_14 ∈ ℝ+
30	1, 29	rpdpcl 32885	. . . . . . . . 9 ⊢ (1._4_14) ∈ ℝ+
31		rpre 13043	. . . . . . . . 9 ⊢ ((1._4_14) ∈ ℝ+ → (1._4_14) ∈ ℝ)
32	30, 31	ax-mp 5	. . . . . . . 8 ⊢ (1._4_14) ∈ ℝ
33	23, 32	remulcli 11277	. . . . . . 7 ⊢ (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ
34		6re 12356	. . . . . . . . . 10 ⊢ 6 ∈ ℝ
35		1re 11261	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
36	5, 35	pm3.2i 470	. . . . . . . . . . 11 ⊢ (5 ∈ ℝ ∧ 1 ∈ ℝ)
37		dp2cl 32862	. . . . . . . . . . 11 ⊢ ((5 ∈ ℝ ∧ 1 ∈ ℝ) → _51 ∈ ℝ)
38	36, 37	ax-mp 5	. . . . . . . . . 10 ⊢ _51 ∈ ℝ
39	34, 38	pm3.2i 470	. . . . . . . . 9 ⊢ (6 ∈ ℝ ∧ _51 ∈ ℝ)
40		dp2cl 32862	. . . . . . . . 9 ⊢ ((6 ∈ ℝ ∧ _51 ∈ ℝ) → _6_51 ∈ ℝ)
41	39, 40	ax-mp 5	. . . . . . . 8 ⊢ _6_51 ∈ ℝ
42		dpcl 32873	. . . . . . . 8 ⊢ ((1 ∈ ℕ0 ∧ _6_51 ∈ ℝ) → (1._6_51) ∈ ℝ)
43	1, 41, 42	mp2an 692	. . . . . . 7 ⊢ (1._6_51) ∈ ℝ
44	33, 43	pm3.2i 470	. . . . . 6 ⊢ ((((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ ∧ (1._6_51) ∈ ℝ)
45	22	sqge0i 14227	. . . . . . . 8 ⊢ 0 ≤ ((1._0_7_9_9_55)↑2)
46		rpgt0 13047	. . . . . . . . . 10 ⊢ ((1._4_14) ∈ ℝ+ → 0 < (1._4_14))
47	30, 46	ax-mp 5	. . . . . . . . 9 ⊢ 0 < (1._4_14)
48	2, 32, 47	ltleii 11384	. . . . . . . 8 ⊢ 0 ≤ (1._4_14)
49	23, 32	mulge0i 11810	. . . . . . . 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 692	. . . . . . 7 ⊢ 0 ≤ (((1._0_7_9_9_55)↑2) · (1._4_14))
51		0nn0 12541	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
52		7nn0 12548	. . . . . . . . . . . . . 14 ⊢ 7 ∈ ℕ0
53		9nn0 12550	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ ℕ0
54		5nn0 12546	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℕ0
55		5nn 12352	. . . . . . . . . . . . . . . . . 18 ⊢ 5 ∈ ℕ
56		nnrp 13046	. . . . . . . . . . . . . . . . . 18 ⊢ (5 ∈ ℕ → 5 ∈ ℝ+)
57	55, 56	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℝ+
58	54, 57	rpdp2cl 32864	. . . . . . . . . . . . . . . 16 ⊢ _55 ∈ ℝ+
59	53, 58	rpdp2cl 32864	. . . . . . . . . . . . . . 15 ⊢ _9_55 ∈ ℝ+
60	53, 59	rpdp2cl 32864	. . . . . . . . . . . . . 14 ⊢ _9_9_55 ∈ ℝ+
61	52, 60	rpdp2cl 32864	. . . . . . . . . . . . 13 ⊢ _7_9_9_55 ∈ ℝ+
62	51, 61	rpdp2cl 32864	. . . . . . . . . . . 12 ⊢ _0_7_9_9_55 ∈ ℝ+
63		8nn 12361	. . . . . . . . . . . . . 14 ⊢ 8 ∈ ℕ
64	63	rpdp2cl2 32865	. . . . . . . . . . . . 13 ⊢ _80 ∈ ℝ+
65	51, 64	rpdp2cl 32864	. . . . . . . . . . . 12 ⊢ _0_80 ∈ ℝ+
66		9lt10 12864	. . . . . . . . . . . . . . . 16 ⊢ 9 < ;10
67		5lt10 12868	. . . . . . . . . . . . . . . . . 18 ⊢ 5 < ;10
68	54, 57, 67, 67	dp2lt10 32866	. . . . . . . . . . . . . . . . 17 ⊢ _55 < ;10
69	53, 58, 66, 68	dp2lt10 32866	. . . . . . . . . . . . . . . 16 ⊢ _9_55 < ;10
70	53, 59, 66, 69	dp2lt10 32866	. . . . . . . . . . . . . . 15 ⊢ _9_9_55 < ;10
71		7p1e8 12415	. . . . . . . . . . . . . . 15 ⊢ (7 + 1) = 8
72	52, 60, 70, 71	dp2ltsuc 32868	. . . . . . . . . . . . . 14 ⊢ _7_9_9_55 < 8
73		8nn0 12549	. . . . . . . . . . . . . . 15 ⊢ 8 ∈ ℕ0
74	73	dp20u 32860	. . . . . . . . . . . . . 14 ⊢ _80 = 8
75	72, 74	breqtrri 5170	. . . . . . . . . . . . 13 ⊢ _7_9_9_55 < _80
76	51, 61, 64, 75	dp2lt 32867	. . . . . . . . . . . 12 ⊢ _0_7_9_9_55 < _0_80
77	1, 62, 65, 76	dplt 32886	. . . . . . . . . . 11 ⊢ (1._0_7_9_9_55) < (1._0_80)
78	1, 62	rpdpcl 32885	. . . . . . . . . . . . 13 ⊢ (1._0_7_9_9_55) ∈ ℝ+
79		rpge0 13048	. . . . . . . . . . . . 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 32885	. . . . . . . . . . . . 13 ⊢ (1._0_80) ∈ ℝ+
82		rpge0 13048	. . . . . . . . . . . . 13 ⊢ ((1._0_80) ∈ ℝ+ → 0 ≤ (1._0_80))
83	81, 82	ax-mp 5	. . . . . . . . . . . 12 ⊢ 0 ≤ (1._0_80)
84		8re 12362	. . . . . . . . . . . . . . . . . 18 ⊢ 8 ∈ ℝ
85	84, 2	pm3.2i 470	. . . . . . . . . . . . . . . . 17 ⊢ (8 ∈ ℝ ∧ 0 ∈ ℝ)
86		dp2cl 32862	. . . . . . . . . . . . . . . . 17 ⊢ ((8 ∈ ℝ ∧ 0 ∈ ℝ) → _80 ∈ ℝ)
87	85, 86	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ _80 ∈ ℝ
88	2, 87	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ (0 ∈ ℝ ∧ _80 ∈ ℝ)
89		dp2cl 32862	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ ∧ _80 ∈ ℝ) → _0_80 ∈ ℝ)
90	88, 89	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ _0_80 ∈ ℝ
91		dpcl 32873	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℕ0 ∧ _0_80 ∈ ℝ) → (1._0_80) ∈ ℝ)
92	1, 90, 91	mp2an 692	. . . . . . . . . . . . 13 ⊢ (1._0_80) ∈ ℝ
93	22, 92	lt2sqi 14228	. . . . . . . . . . . 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 692	. . . . . . . . . . 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 230	. . . . . . . . . 10 ⊢ ((1._0_7_9_9_55)↑2) < ((1._0_80)↑2)
96	92	recni 11275	. . . . . . . . . . . 12 ⊢ (1._0_80) ∈ ℂ
97	96	sqvali 14219	. . . . . . . . . . 11 ⊢ ((1._0_80)↑2) = ((1._0_80) · (1._0_80))
98		6nn0 12547	. . . . . . . . . . . . 13 ⊢ 6 ∈ ℕ0
99	1, 98	deccl 12748	. . . . . . . . . . . 12 ⊢ ;16 ∈ ℕ0
100	98, 24	deccl 12748	. . . . . . . . . . . 12 ⊢ ;64 ∈ ℕ0
101		4lt10 12869	. . . . . . . . . . . 12 ⊢ 4 < ;10
102		10pos 12750	. . . . . . . . . . . 12 ⊢ 0 < ;10
103	99, 51	deccl 12748	. . . . . . . . . . . . 13 ⊢ ;;160 ∈ ℕ0
104		eqid 2737	. . . . . . . . . . . . 13 ⊢ ;;;1600 = ;;;1600
105		eqid 2737	. . . . . . . . . . . . 13 ⊢ ;64 = ;64
106		eqid 2737	. . . . . . . . . . . . . 14 ⊢ ;;160 = ;;160
107	98	dec0h 12755	. . . . . . . . . . . . . 14 ⊢ 6 = ;06
108	99	nn0cni 12538	. . . . . . . . . . . . . . 15 ⊢ ;16 ∈ ℂ
109	108	addridi 11448	. . . . . . . . . . . . . 14 ⊢ (;16 + 0) = ;16
110		6cn 12357	. . . . . . . . . . . . . . 15 ⊢ 6 ∈ ℂ
111	110	addlidi 11449	. . . . . . . . . . . . . 14 ⊢ (0 + 6) = 6
112	99, 51, 51, 98, 106, 107, 109, 111	decadd 12787	. . . . . . . . . . . . 13 ⊢ (;;160 + 6) = ;;166
113		4cn 12351	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℂ
114	113	addlidi 11449	. . . . . . . . . . . . 13 ⊢ (0 + 4) = 4
115	103, 51, 98, 24, 104, 105, 112, 114	decadd 12787	. . . . . . . . . . . 12 ⊢ (;;;1600 + ;64) = ;;;1664
116		1t1e1 12428	. . . . . . . . . . . . 13 ⊢ (1 · 1) = 1
117	1	dp0u 32883	. . . . . . . . . . . . . 14 ⊢ (1.0) = 1
118	117, 117	oveq12i 7443	. . . . . . . . . . . . 13 ⊢ ((1.0) · (1.0)) = (1 · 1)
119	51	dp20u 32860	. . . . . . . . . . . . . . 15 ⊢ _00 = 0
120	119	oveq2i 7442	. . . . . . . . . . . . . 14 ⊢ (1._00) = (1.0)
121	120, 117	eqtri 2765	. . . . . . . . . . . . 13 ⊢ (1._00) = 1
122	116, 118, 121	3eqtr4i 2775	. . . . . . . . . . . 12 ⊢ ((1.0) · (1.0)) = (1._00)
123		8t8e64 12854	. . . . . . . . . . . . 13 ⊢ (8 · 8) = ;64
124	73	dp0u 32883	. . . . . . . . . . . . . 14 ⊢ (8.0) = 8
125	124, 124	oveq12i 7443	. . . . . . . . . . . . 13 ⊢ ((8.0) · (8.0)) = (8 · 8)
126	119	oveq2i 7442	. . . . . . . . . . . . . 14 ⊢ (;64._00) = (;64.0)
127	100	dp0u 32883	. . . . . . . . . . . . . 14 ⊢ (;64.0) = ;64
128	126, 127	eqtri 2765	. . . . . . . . . . . . 13 ⊢ (;64._00) = ;64
129	123, 125, 128	3eqtr4i 2775	. . . . . . . . . . . 12 ⊢ ((8.0) · (8.0)) = (;64._00)
130		10nn0 12751	. . . . . . . . . . . . . 14 ⊢ ;10 ∈ ℕ0
131	130, 51	deccl 12748	. . . . . . . . . . . . 13 ⊢ ;;100 ∈ ℕ0
132		eqid 2737	. . . . . . . . . . . . 13 ⊢ ;;;1001 = ;;;1001
133		eqid 2737	. . . . . . . . . . . . 13 ⊢ ;;166 = ;;166
134		eqid 2737	. . . . . . . . . . . . . 14 ⊢ ;;100 = ;;100
135		eqid 2737	. . . . . . . . . . . . . 14 ⊢ ;16 = ;16
136		dec10p 12776	. . . . . . . . . . . . . 14 ⊢ (;10 + 1) = ;11
137	130, 51, 1, 98, 134, 135, 136, 111	decadd 12787	. . . . . . . . . . . . 13 ⊢ (;;100 + ;16) = ;;116
138		ax-1cn 11213	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
139	138, 110	addcomi 11452	. . . . . . . . . . . . . 14 ⊢ (1 + 6) = (6 + 1)
140		6p1e7 12414	. . . . . . . . . . . . . 14 ⊢ (6 + 1) = 7
141	139, 140	eqtri 2765	. . . . . . . . . . . . 13 ⊢ (1 + 6) = 7
142	131, 1, 99, 98, 132, 133, 137, 141	decadd 12787	. . . . . . . . . . . 12 ⊢ (;;;1001 + ;;166) = ;;;1167
143		eqid 2737	. . . . . . . . . . . . . 14 ⊢ ;17 = ;17
144	141	oveq1i 7441	. . . . . . . . . . . . . . 15 ⊢ ((1 + 6) + 1) = (7 + 1)
145	144, 71	eqtri 2765	. . . . . . . . . . . . . 14 ⊢ ((1 + 6) + 1) = 8
146		7p4e11 12809	. . . . . . . . . . . . . 14 ⊢ (7 + 4) = ;11
147	1, 52, 98, 24, 143, 105, 145, 1, 146	decaddc 12788	. . . . . . . . . . . . 13 ⊢ (;17 + ;64) = ;81
148	119	oveq2i 7442	. . . . . . . . . . . . . . . . 17 ⊢ (;16._00) = (;16.0)
149	99	dp0u 32883	. . . . . . . . . . . . . . . . 17 ⊢ (;16.0) = ;16
150	148, 149	eqtri 2765	. . . . . . . . . . . . . . . 16 ⊢ (;16._00) = ;16
151	121, 150	oveq12i 7443	. . . . . . . . . . . . . . 15 ⊢ ((1._00) + (;16._00)) = (1 + ;16)
152	1	dec0h 12755	. . . . . . . . . . . . . . . 16 ⊢ 1 = ;01
153	138	addlidi 11449	. . . . . . . . . . . . . . . 16 ⊢ (0 + 1) = 1
154	51, 1, 1, 98, 152, 135, 153, 141	decadd 12787	. . . . . . . . . . . . . . 15 ⊢ (1 + ;16) = ;17
155	151, 154	eqtri 2765	. . . . . . . . . . . . . 14 ⊢ ((1._00) + (;16._00)) = ;17
156	155, 128	oveq12i 7443	. . . . . . . . . . . . 13 ⊢ (((1._00) + (;16._00)) + (;64._00)) = (;17 + ;64)
157	117, 124	oveq12i 7443	. . . . . . . . . . . . . . . 16 ⊢ ((1.0) + (8.0)) = (1 + 8)
158		8cn 12363	. . . . . . . . . . . . . . . . 17 ⊢ 8 ∈ ℂ
159	138, 158	addcomi 11452	. . . . . . . . . . . . . . . 16 ⊢ (1 + 8) = (8 + 1)
160		8p1e9 12416	. . . . . . . . . . . . . . . 16 ⊢ (8 + 1) = 9
161	157, 159, 160	3eqtri 2769	. . . . . . . . . . . . . . 15 ⊢ ((1.0) + (8.0)) = 9
162	161, 161	oveq12i 7443	. . . . . . . . . . . . . 14 ⊢ (((1.0) + (8.0)) · ((1.0) + (8.0))) = (9 · 9)
163		9t9e81 12862	. . . . . . . . . . . . . 14 ⊢ (9 · 9) = ;81
164	162, 163	eqtri 2765	. . . . . . . . . . . . 13 ⊢ (((1.0) + (8.0)) · ((1.0) + (8.0))) = ;81
165	147, 156, 164	3eqtr4ri 2776	. . . . . . . . . . . 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 32896	. . . . . . . . . . 11 ⊢ ((1._0_80) · (1._0_80)) < (1._1_67)
167	97, 166	eqbrtri 5164	. . . . . . . . . 10 ⊢ ((1._0_80)↑2) < (1._1_67)
168	92	resqcli 14225	. . . . . . . . . . 11 ⊢ ((1._0_80)↑2) ∈ ℝ
169	34, 3	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ (6 ∈ ℝ ∧ 7 ∈ ℝ)
170		dp2cl 32862	. . . . . . . . . . . . . . 15 ⊢ ((6 ∈ ℝ ∧ 7 ∈ ℝ) → _67 ∈ ℝ)
171	169, 170	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ _67 ∈ ℝ
172	35, 171	pm3.2i 470	. . . . . . . . . . . . 13 ⊢ (1 ∈ ℝ ∧ _67 ∈ ℝ)
173		dp2cl 32862	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ ∧ _67 ∈ ℝ) → _1_67 ∈ ℝ)
174	172, 173	ax-mp 5	. . . . . . . . . . . 12 ⊢ _1_67 ∈ ℝ
175		dpcl 32873	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℕ0 ∧ _1_67 ∈ ℝ) → (1._1_67) ∈ ℝ)
176	1, 174, 175	mp2an 692	. . . . . . . . . . 11 ⊢ (1._1_67) ∈ ℝ
177	23, 168, 176	lttri 11387	. . . . . . . . . 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 692	. . . . . . . . 9 ⊢ ((1._0_7_9_9_55)↑2) < (1._1_67)
179	23, 176, 32, 47	ltmul1ii 12196	. . . . . . . . 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 230	. . . . . . . 8 ⊢ (((1._0_7_9_9_55)↑2) · (1._4_14)) < ((1._1_67) · (1._4_14))
181		2nn0 12543	. . . . . . . . 9 ⊢ 2 ∈ ℕ0
182		3nn0 12544	. . . . . . . . 9 ⊢ 3 ∈ ℕ0
183		1lt10 12872	. . . . . . . . 9 ⊢ 1 < ;10
184		3lt10 12870	. . . . . . . . 9 ⊢ 3 < ;10
185		8lt10 12865	. . . . . . . . 9 ⊢ 8 < ;10
186	130, 53	deccl 12748	. . . . . . . . . 10 ⊢ ;;109 ∈ ℕ0
187		eqid 2737	. . . . . . . . . 10 ⊢ ;;;1092 = ;;;1092
188	53	dec0h 12755	. . . . . . . . . 10 ⊢ 9 = ;09
189	186	nn0cni 12538	. . . . . . . . . . . 12 ⊢ ;;109 ∈ ℂ
190	189	addridi 11448	. . . . . . . . . . 11 ⊢ (;;109 + 0) = ;;109
191		dec10p 12776	. . . . . . . . . . . 12 ⊢ (;10 + 0) = ;10
192	138	addridi 11448	. . . . . . . . . . . 12 ⊢ (1 + 0) = 1
193	1, 51, 51, 1, 191, 152, 192, 153	decadd 12787	. . . . . . . . . . 11 ⊢ ((;10 + 0) + 1) = ;11
194		9p1e10 12735	. . . . . . . . . . 11 ⊢ (9 + 1) = ;10
195	130, 53, 51, 1, 190, 152, 193, 51, 194	decaddc 12788	. . . . . . . . . 10 ⊢ ((;;109 + 0) + 1) = ;;110
196		9cn 12366	. . . . . . . . . . . 12 ⊢ 9 ∈ ℂ
197		2cn 12341	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
198	196, 197	addcomi 11452	. . . . . . . . . . 11 ⊢ (9 + 2) = (2 + 9)
199		9p2e11 12820	. . . . . . . . . . 11 ⊢ (9 + 2) = ;11
200	198, 199	eqtr3i 2767	. . . . . . . . . 10 ⊢ (2 + 9) = ;11
201	186, 181, 51, 53, 187, 188, 195, 1, 200	decaddc 12788	. . . . . . . . 9 ⊢ (;;;1092 + 9) = ;;;1101
202	113, 138	mulcomi 11269	. . . . . . . . . . 11 ⊢ (4 · 1) = (1 · 4)
203	113	mulridi 11265	. . . . . . . . . . 11 ⊢ (4 · 1) = 4
204	202, 203	eqtr3i 2767	. . . . . . . . . 10 ⊢ (1 · 4) = 4
205	24	dec0h 12755	. . . . . . . . . . 11 ⊢ 4 = ;04
206	203, 202, 205	3eqtr3i 2773	. . . . . . . . . 10 ⊢ (1 · 4) = ;04
207	138, 113	addcli 11267	. . . . . . . . . . . . 13 ⊢ (1 + 4) ∈ ℂ
208	207	addridi 11448	. . . . . . . . . . . 12 ⊢ ((1 + 4) + 0) = (1 + 4)
209	113, 138	addcomi 11452	. . . . . . . . . . . 12 ⊢ (4 + 1) = (1 + 4)
210		4p1e5 12412	. . . . . . . . . . . 12 ⊢ (4 + 1) = 5
211	208, 209, 210	3eqtr2i 2771	. . . . . . . . . . 11 ⊢ ((1 + 4) + 0) = 5
212	54	dec0h 12755	. . . . . . . . . . 11 ⊢ 5 = ;05
213	211, 212	eqtri 2765	. . . . . . . . . 10 ⊢ ((1 + 4) + 0) = ;05
214	1, 1, 1, 24, 51, 51, 54, 24, 116, 204, 116, 206, 213, 192	dpmul 32895	. . . . . . . . 9 ⊢ ((1.1) · (1.4)) = (1._54)
215	110	mulridi 11265	. . . . . . . . . 10 ⊢ (6 · 1) = 6
216		6t4e24 12839	. . . . . . . . . 10 ⊢ (6 · 4) = ;24
217		7cn 12360	. . . . . . . . . . 11 ⊢ 7 ∈ ℂ
218	217	mulridi 11265	. . . . . . . . . 10 ⊢ (7 · 1) = 7
219		7t4e28 12844	. . . . . . . . . 10 ⊢ (7 · 4) = ;28
220	181, 24	deccl 12748	. . . . . . . . . . . . . . 15 ⊢ ;24 ∈ ℕ0
221	220	nn0cni 12538	. . . . . . . . . . . . . 14 ⊢ ;24 ∈ ℂ
222	221, 217	addcomi 11452	. . . . . . . . . . . . 13 ⊢ (;24 + 7) = (7 + ;24)
223		eqid 2737	. . . . . . . . . . . . . 14 ⊢ ;24 = ;24
224		2p1e3 12408	. . . . . . . . . . . . . 14 ⊢ (2 + 1) = 3
225	217, 113, 146	addcomli 11453	. . . . . . . . . . . . . 14 ⊢ (4 + 7) = ;11
226	181, 24, 52, 223, 224, 1, 225	decaddci 12794	. . . . . . . . . . . . 13 ⊢ (;24 + 7) = ;31
227	222, 226	eqtr3i 2767	. . . . . . . . . . . 12 ⊢ (7 + ;24) = ;31
228	227	oveq1i 7441	. . . . . . . . . . 11 ⊢ ((7 + ;24) + 2) = (;31 + 2)
229		eqid 2737	. . . . . . . . . . . 12 ⊢ ;31 = ;31
230	197, 138, 224	addcomli 11453	. . . . . . . . . . . 12 ⊢ (1 + 2) = 3
231	182, 1, 181, 229, 230	decaddi 12793	. . . . . . . . . . 11 ⊢ (;31 + 2) = ;33
232	228, 231	eqtri 2765	. . . . . . . . . 10 ⊢ ((7 + ;24) + 2) = ;33
233		6p3e9 12426	. . . . . . . . . 10 ⊢ (6 + 3) = 9
234	98, 52, 1, 24, 181, 182, 182, 73, 215, 216, 218, 219, 232, 233	dpmul 32895	. . . . . . . . 9 ⊢ ((6.7) · (1.4)) = (9._38)
235	1, 54	deccl 12748	. . . . . . . . . . 11 ⊢ ;15 ∈ ℕ0
236	235, 24	deccl 12748	. . . . . . . . . 10 ⊢ ;;154 ∈ ℕ0
237	51, 1	deccl 12748	. . . . . . . . . . 11 ⊢ ;01 ∈ ℕ0
238	237, 1	deccl 12748	. . . . . . . . . 10 ⊢ ;;011 ∈ ℕ0
239		eqid 2737	. . . . . . . . . 10 ⊢ ;;;1541 = ;;;1541
240	152	deceq1i 12740	. . . . . . . . . . 11 ⊢ ;11 = ;;011
241	240	deceq1i 12740	. . . . . . . . . 10 ⊢ ;;110 = ;;;0110
242		eqid 2737	. . . . . . . . . . 11 ⊢ ;;154 = ;;154
243		eqid 2737	. . . . . . . . . . 11 ⊢ ;;011 = ;;011
244	152	oveq2i 7442	. . . . . . . . . . . 12 ⊢ (;15 + 1) = (;15 + ;01)
245		eqid 2737	. . . . . . . . . . . . 13 ⊢ ;15 = ;15
246		5p1e6 12413	. . . . . . . . . . . . 13 ⊢ (5 + 1) = 6
247	1, 54, 1, 245, 246	decaddi 12793	. . . . . . . . . . . 12 ⊢ (;15 + 1) = ;16
248	244, 247	eqtr3i 2767	. . . . . . . . . . 11 ⊢ (;15 + ;01) = ;16
249	235, 24, 237, 1, 242, 243, 248, 210	decadd 12787	. . . . . . . . . 10 ⊢ (;;154 + ;;011) = ;;165
250	236, 1, 238, 51, 239, 241, 249, 192	decadd 12787	. . . . . . . . 9 ⊢ (;;;1541 + ;;110) = ;;;1651
251		7t2e14 12842	. . . . . . . . . . 11 ⊢ (7 · 2) = ;14
252		8t7e56 12853	. . . . . . . . . . . 12 ⊢ (8 · 7) = ;56
253	158, 217, 252	mulcomli 11270	. . . . . . . . . . 11 ⊢ (7 · 8) = ;56
254		8t2e16 12848	. . . . . . . . . . 11 ⊢ (8 · 2) = ;16
255		eqid 2737	. . . . . . . . . . . . . 14 ⊢ ;56 = ;56
256		5cn 12354	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℂ
257	256, 138, 246	addcomli 11453	. . . . . . . . . . . . . . . 16 ⊢ (1 + 5) = 6
258	257	oveq1i 7441	. . . . . . . . . . . . . . 15 ⊢ ((1 + 5) + 1) = (6 + 1)
259	258, 140	eqtri 2765	. . . . . . . . . . . . . 14 ⊢ ((1 + 5) + 1) = 7
260		6p6e12 12807	. . . . . . . . . . . . . 14 ⊢ (6 + 6) = ;12
261	1, 98, 54, 98, 135, 255, 259, 181, 260	decaddc 12788	. . . . . . . . . . . . 13 ⊢ (;16 + ;56) = ;72
262	261	oveq1i 7441	. . . . . . . . . . . 12 ⊢ ((;16 + ;56) + 6) = (;72 + 6)
263		eqid 2737	. . . . . . . . . . . . 13 ⊢ ;72 = ;72
264		6p2e8 12425	. . . . . . . . . . . . . 14 ⊢ (6 + 2) = 8
265	110, 197, 264	addcomli 11453	. . . . . . . . . . . . 13 ⊢ (2 + 6) = 8
266	52, 181, 98, 263, 265	decaddi 12793	. . . . . . . . . . . 12 ⊢ (;72 + 6) = ;78
267	262, 266	eqtri 2765	. . . . . . . . . . 11 ⊢ ((;16 + ;56) + 6) = ;78
268		eqid 2737	. . . . . . . . . . . 12 ⊢ ;14 = ;14
269		1p1e2 12391	. . . . . . . . . . . 12 ⊢ (1 + 1) = 2
270	1, 24, 52, 268, 269, 1, 225	decaddci 12794	. . . . . . . . . . 11 ⊢ (;14 + 7) = ;21
271	52, 73, 181, 73, 98, 52, 73, 24, 251, 253, 254, 123, 267, 270	dpmul 32895	. . . . . . . . . 10 ⊢ ((7.8) · (2.8)) = (;21._84)
272		eqid 2737	. . . . . . . . . . . . 13 ⊢ ;11 = ;11
273		eqid 2737	. . . . . . . . . . . . 13 ⊢ ;67 = ;67
274	217, 138, 71	addcomli 11453	. . . . . . . . . . . . 13 ⊢ (1 + 7) = 8
275	1, 1, 98, 52, 272, 273, 141, 274	decadd 12787	. . . . . . . . . . . 12 ⊢ (;11 + ;67) = ;78
276	1, 1, 98, 52, 52, 73, 275	dpadd 32893	. . . . . . . . . . 11 ⊢ ((1.1) + (6.7)) = (7.8)
277		4p4e8 12421	. . . . . . . . . . . . 13 ⊢ (4 + 4) = 8
278	1, 24, 1, 24, 268, 268, 269, 277	decadd 12787	. . . . . . . . . . . 12 ⊢ (;14 + ;14) = ;28
279	1, 24, 1, 24, 181, 73, 278	dpadd 32893	. . . . . . . . . . 11 ⊢ ((1.4) + (1.4)) = (2.8)
280	276, 279	oveq12i 7443	. . . . . . . . . 10 ⊢ (((1.1) + (6.7)) · ((1.4) + (1.4))) = ((7.8) · (2.8))
281	1, 181	deccl 12748	. . . . . . . . . . . . 13 ⊢ ;12 ∈ ℕ0
282		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ ;;109 = ;;109
283	130	nn0cni 12538	. . . . . . . . . . . . . . . . 17 ⊢ ;10 ∈ ℂ
284	283, 138, 136	addcomli 11453	. . . . . . . . . . . . . . . 16 ⊢ (1 + ;10) = ;11
285	1, 1, 269, 284	decsuc 12764	. . . . . . . . . . . . . . 15 ⊢ ((1 + ;10) + 1) = ;12
286		9p5e14 12823	. . . . . . . . . . . . . . . 16 ⊢ (9 + 5) = ;14
287	196, 256, 286	addcomli 11453	. . . . . . . . . . . . . . 15 ⊢ (5 + 9) = ;14
288	1, 54, 130, 53, 245, 282, 285, 24, 287	decaddc 12788	. . . . . . . . . . . . . 14 ⊢ (;15 + ;;109) = ;;124
289		4p2e6 12419	. . . . . . . . . . . . . 14 ⊢ (4 + 2) = 6
290	235, 24, 186, 181, 242, 187, 288, 289	decadd 12787	. . . . . . . . . . . . 13 ⊢ (;;154 + ;;;1092) = ;;;1246
291	1, 54, 24, 130, 53, 281, 181, 24, 98, 290	dpadd3 32894	. . . . . . . . . . . 12 ⊢ ((1._54) + (;10._92)) = (;12._46)
292	291	oveq1i 7441	. . . . . . . . . . 11 ⊢ (((1._54) + (;10._92)) + (9._38)) = ((;12._46) + (9._38))
293	181, 1	deccl 12748	. . . . . . . . . . . 12 ⊢ ;21 ∈ ℕ0
294	281, 24	deccl 12748	. . . . . . . . . . . . 13 ⊢ ;;124 ∈ ℕ0
295	53, 182	deccl 12748	. . . . . . . . . . . . 13 ⊢ ;93 ∈ ℕ0
296		eqid 2737	. . . . . . . . . . . . 13 ⊢ ;;;1246 = ;;;1246
297		eqid 2737	. . . . . . . . . . . . 13 ⊢ ;;938 = ;;938
298		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ ;;124 = ;;124
299		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ ;93 = ;93
300		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ ;12 = ;12
301	1, 181, 53, 300, 269, 1, 200	decaddci 12794	. . . . . . . . . . . . . . 15 ⊢ (;12 + 9) = ;21
302		4p3e7 12420	. . . . . . . . . . . . . . 15 ⊢ (4 + 3) = 7
303	281, 24, 53, 182, 298, 299, 301, 302	decadd 12787	. . . . . . . . . . . . . 14 ⊢ (;;124 + ;93) = ;;217
304	293, 52, 71, 303	decsuc 12764	. . . . . . . . . . . . 13 ⊢ ((;;124 + ;93) + 1) = ;;218
305		8p6e14 12817	. . . . . . . . . . . . . 14 ⊢ (8 + 6) = ;14
306	158, 110, 305	addcomli 11453	. . . . . . . . . . . . 13 ⊢ (6 + 8) = ;14
307	294, 98, 295, 73, 296, 297, 304, 24, 306	decaddc 12788	. . . . . . . . . . . 12 ⊢ (;;;1246 + ;;938) = ;;;2184
308	281, 24, 98, 53, 182, 293, 73, 73, 24, 307	dpadd3 32894	. . . . . . . . . . 11 ⊢ ((;12._46) + (9._38)) = (;21._84)
309	292, 308	eqtri 2765	. . . . . . . . . 10 ⊢ (((1._54) + (;10._92)) + (9._38)) = (;21._84)
310	271, 280, 309	3eqtr4i 2775	. . . . . . . . 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 32896	. . . . . . . 8 ⊢ ((1._1_67) · (1._4_14)) < (1._6_51)
312	176, 32	remulcli 11277	. . . . . . . . 9 ⊢ ((1._1_67) · (1._4_14)) ∈ ℝ
313	33, 312, 43	lttri 11387	. . . . . . . 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 692	. . . . . . 7 ⊢ (((1._0_7_9_9_55)↑2) · (1._4_14)) < (1._6_51)
315	50, 314	pm3.2i 470	. . . . . 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 470	. . . . 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 12350	. . . . . . . . . . 11 ⊢ 4 ∈ ℝ
318		2re 12340	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
319		3re 12346	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ ℝ
320	34, 319	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ (6 ∈ ℝ ∧ 3 ∈ ℝ)
321		dp2cl 32862	. . . . . . . . . . . . . 14 ⊢ ((6 ∈ ℝ ∧ 3 ∈ ℝ) → _63 ∈ ℝ)
322	320, 321	ax-mp 5	. . . . . . . . . . . . 13 ⊢ _63 ∈ ℝ
323	318, 322	pm3.2i 470	. . . . . . . . . . . 12 ⊢ (2 ∈ ℝ ∧ _63 ∈ ℝ)
324		dp2cl 32862	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ _63 ∈ ℝ) → _2_63 ∈ ℝ)
325	323, 324	ax-mp 5	. . . . . . . . . . 11 ⊢ _2_63 ∈ ℝ
326	317, 325	pm3.2i 470	. . . . . . . . . 10 ⊢ (4 ∈ ℝ ∧ _2_63 ∈ ℝ)
327		dp2cl 32862	. . . . . . . . . 10 ⊢ ((4 ∈ ℝ ∧ _2_63 ∈ ℝ) → _4_2_63 ∈ ℝ)
328	326, 327	ax-mp 5	. . . . . . . . 9 ⊢ _4_2_63 ∈ ℝ
329		dpcl 32873	. . . . . . . . 9 ⊢ ((1 ∈ ℕ0 ∧ _4_2_63 ∈ ℝ) → (1._4_2_63) ∈ ℝ)
330	1, 328, 329	mp2an 692	. . . . . . . 8 ⊢ (1._4_2_63) ∈ ℝ
331	84, 319	pm3.2i 470	. . . . . . . . . . . . . . . 16 ⊢ (8 ∈ ℝ ∧ 3 ∈ ℝ)
332		dp2cl 32862	. . . . . . . . . . . . . . . 16 ⊢ ((8 ∈ ℝ ∧ 3 ∈ ℝ) → _83 ∈ ℝ)
333	331, 332	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ _83 ∈ ℝ
334	84, 333	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ (8 ∈ ℝ ∧ _83 ∈ ℝ)
335		dp2cl 32862	. . . . . . . . . . . . . 14 ⊢ ((8 ∈ ℝ ∧ _83 ∈ ℝ) → _8_83 ∈ ℝ)
336	334, 335	ax-mp 5	. . . . . . . . . . . . 13 ⊢ _8_83 ∈ ℝ
337	319, 336	pm3.2i 470	. . . . . . . . . . . 12 ⊢ (3 ∈ ℝ ∧ _8_83 ∈ ℝ)
338		dp2cl 32862	. . . . . . . . . . . 12 ⊢ ((3 ∈ ℝ ∧ _8_83 ∈ ℝ) → _3_8_83 ∈ ℝ)
339	337, 338	ax-mp 5	. . . . . . . . . . 11 ⊢ _3_8_83 ∈ ℝ
340	2, 339	pm3.2i 470	. . . . . . . . . 10 ⊢ (0 ∈ ℝ ∧ _3_8_83 ∈ ℝ)
341		dp2cl 32862	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ _3_8_83 ∈ ℝ) → _0_3_8_83 ∈ ℝ)
342	340, 341	ax-mp 5	. . . . . . . . 9 ⊢ _0_3_8_83 ∈ ℝ
343		dpcl 32873	. . . . . . . . 9 ⊢ ((1 ∈ ℕ0 ∧ _0_3_8_83 ∈ ℝ) → (1._0_3_8_83) ∈ ℝ)
344	1, 342, 343	mp2an 692	. . . . . . . 8 ⊢ (1._0_3_8_83) ∈ ℝ
345	330, 344	remulcli 11277	. . . . . . 7 ⊢ ((1._4_2_63) · (1._0_3_8_83)) ∈ ℝ
346	317, 333	pm3.2i 470	. . . . . . . . 9 ⊢ (4 ∈ ℝ ∧ _83 ∈ ℝ)
347		dp2cl 32862	. . . . . . . . 9 ⊢ ((4 ∈ ℝ ∧ _83 ∈ ℝ) → _4_83 ∈ ℝ)
348	346, 347	ax-mp 5	. . . . . . . 8 ⊢ _4_83 ∈ ℝ
349		dpcl 32873	. . . . . . . 8 ⊢ ((1 ∈ ℕ0 ∧ _4_83 ∈ ℝ) → (1._4_83) ∈ ℝ)
350	1, 348, 349	mp2an 692	. . . . . . 7 ⊢ (1._4_83) ∈ ℝ
351	345, 350	pm3.2i 470	. . . . . 6 ⊢ (((1._4_2_63) · (1._0_3_8_83)) ∈ ℝ ∧ (1._4_83) ∈ ℝ)
352		3rp 13040	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℝ+
353	98, 352	rpdp2cl 32864	. . . . . . . . . . . 12 ⊢ _63 ∈ ℝ+
354	181, 353	rpdp2cl 32864	. . . . . . . . . . 11 ⊢ _2_63 ∈ ℝ+
355	24, 354	rpdp2cl 32864	. . . . . . . . . 10 ⊢ _4_2_63 ∈ ℝ+
356	1, 355	rpdpcl 32885	. . . . . . . . 9 ⊢ (1._4_2_63) ∈ ℝ+
357		rpge0 13048	. . . . . . . . 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 32864	. . . . . . . . . . . . 13 ⊢ _83 ∈ ℝ+
360	73, 359	rpdp2cl 32864	. . . . . . . . . . . 12 ⊢ _8_83 ∈ ℝ+
361	182, 360	rpdp2cl 32864	. . . . . . . . . . 11 ⊢ _3_8_83 ∈ ℝ+
362	51, 361	rpdp2cl 32864	. . . . . . . . . 10 ⊢ _0_3_8_83 ∈ ℝ+
363	1, 362	rpdpcl 32885	. . . . . . . . 9 ⊢ (1._0_3_8_83) ∈ ℝ+
364		rpge0 13048	. . . . . . . . 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 11810	. . . . . . . 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 692	. . . . . . 7 ⊢ 0 ≤ ((1._4_2_63) · (1._0_3_8_83))
368	318, 3	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℝ ∧ 7 ∈ ℝ)
369		dp2cl 32862	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℝ ∧ 7 ∈ ℝ) → _27 ∈ ℝ)
370	368, 369	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ _27 ∈ ℝ
371	317, 370	pm3.2i 470	. . . . . . . . . . . . 13 ⊢ (4 ∈ ℝ ∧ _27 ∈ ℝ)
372		dp2cl 32862	. . . . . . . . . . . . 13 ⊢ ((4 ∈ ℝ ∧ _27 ∈ ℝ) → _4_27 ∈ ℝ)
373	371, 372	ax-mp 5	. . . . . . . . . . . 12 ⊢ _4_27 ∈ ℝ
374		dpcl 32873	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℕ0 ∧ _4_27 ∈ ℝ) → (1._4_27) ∈ ℝ)
375	1, 373, 374	mp2an 692	. . . . . . . . . . 11 ⊢ (1._4_27) ∈ ℝ
376	330, 375	pm3.2i 470	. . . . . . . . . 10 ⊢ ((1._4_2_63) ∈ ℝ ∧ (1._4_27) ∈ ℝ)
377		7nn 12358	. . . . . . . . . . . . . . 15 ⊢ 7 ∈ ℕ
378		nnrp 13046	. . . . . . . . . . . . . . 15 ⊢ (7 ∈ ℕ → 7 ∈ ℝ+)
379	377, 378	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 7 ∈ ℝ+
380	181, 379	rpdp2cl 32864	. . . . . . . . . . . . 13 ⊢ _27 ∈ ℝ+
381	24, 380	rpdp2cl 32864	. . . . . . . . . . . 12 ⊢ _4_27 ∈ ℝ+
382	98, 352, 184, 140	dp2ltsuc 32868	. . . . . . . . . . . . . 14 ⊢ _63 < 7
383	181, 353, 379, 382	dp2lt 32867	. . . . . . . . . . . . 13 ⊢ _2_63 < _27
384	24, 354, 380, 383	dp2lt 32867	. . . . . . . . . . . 12 ⊢ _4_2_63 < _4_27
385	1, 355, 381, 384	dplt 32886	. . . . . . . . . . 11 ⊢ (1._4_2_63) < (1._4_27)
386	358, 385	pm3.2i 470	. . . . . . . . . 10 ⊢ (0 ≤ (1._4_2_63) ∧ (1._4_2_63) < (1._4_27))
387	376, 386	pm3.2i 470	. . . . . . . . 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 470	. . . . . . . . . . . . . . 15 ⊢ (3 ∈ ℝ ∧ 9 ∈ ℝ)
389		dp2cl 32862	. . . . . . . . . . . . . . 15 ⊢ ((3 ∈ ℝ ∧ 9 ∈ ℝ) → _39 ∈ ℝ)
390	388, 389	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ _39 ∈ ℝ
391	2, 390	pm3.2i 470	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ ∧ _39 ∈ ℝ)
392		dp2cl 32862	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ _39 ∈ ℝ) → _0_39 ∈ ℝ)
393	391, 392	ax-mp 5	. . . . . . . . . . . 12 ⊢ _0_39 ∈ ℝ
394		dpcl 32873	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℕ0 ∧ _0_39 ∈ ℝ) → (1._0_39) ∈ ℝ)
395	1, 393, 394	mp2an 692	. . . . . . . . . . 11 ⊢ (1._0_39) ∈ ℝ
396	344, 395	pm3.2i 470	. . . . . . . . . 10 ⊢ ((1._0_3_8_83) ∈ ℝ ∧ (1._0_39) ∈ ℝ)
397		9nn 12364	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ ℕ
398		nnrp 13046	. . . . . . . . . . . . . . 15 ⊢ (9 ∈ ℕ → 9 ∈ ℝ+)
399	397, 398	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 9 ∈ ℝ+
400	182, 399	rpdp2cl 32864	. . . . . . . . . . . . 13 ⊢ _39 ∈ ℝ+
401	51, 400	rpdp2cl 32864	. . . . . . . . . . . 12 ⊢ _0_39 ∈ ℝ+
402	73, 352, 185, 184	dp2lt10 32866	. . . . . . . . . . . . . . 15 ⊢ _83 < ;10
403	73, 359, 402, 160	dp2ltsuc 32868	. . . . . . . . . . . . . 14 ⊢ _8_83 < 9
404	182, 360, 399, 403	dp2lt 32867	. . . . . . . . . . . . 13 ⊢ _3_8_83 < _39
405	51, 361, 400, 404	dp2lt 32867	. . . . . . . . . . . 12 ⊢ _0_3_8_83 < _0_39
406	1, 362, 401, 405	dplt 32886	. . . . . . . . . . 11 ⊢ (1._0_3_8_83) < (1._0_39)
407	365, 406	pm3.2i 470	. . . . . . . . . 10 ⊢ (0 ≤ (1._0_3_8_83) ∧ (1._0_3_8_83) < (1._0_39))
408	396, 407	pm3.2i 470	. . . . . . . . 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 12123	. . . . . . . . 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 692	. . . . . . . 8 ⊢ ((1._4_2_63) · (1._0_3_8_83)) < ((1._4_27) · (1._0_39))
411		6lt10 12867	. . . . . . . . 9 ⊢ 6 < ;10
412	73, 1	deccl 12748	. . . . . . . . . 10 ⊢ ;81 ∈ ℕ0
413		eqid 2737	. . . . . . . . . 10 ⊢ ;;816 = ;;816
414		eqid 2737	. . . . . . . . . 10 ⊢ ;10 = ;10
415		eqid 2737	. . . . . . . . . . . 12 ⊢ ;81 = ;81
416	73, 1, 269, 415	decsuc 12764	. . . . . . . . . . 11 ⊢ (;81 + 1) = ;82
417	73	dec0h 12755	. . . . . . . . . . . 12 ⊢ 8 = ;08
418	417	deceq1i 12740	. . . . . . . . . . 11 ⊢ ;82 = ;;082
419	416, 418	eqtri 2765	. . . . . . . . . 10 ⊢ (;81 + 1) = ;;082
420	110	addridi 11448	. . . . . . . . . 10 ⊢ (6 + 0) = 6
421	412, 98, 1, 51, 413, 414, 419, 420	decadd 12787	. . . . . . . . 9 ⊢ (;;816 + ;10) = ;;;0826
422	138	mul01i 11451	. . . . . . . . . 10 ⊢ (1 · 0) = 0
423	113	mul01i 11451	. . . . . . . . . . 11 ⊢ (4 · 0) = 0
424	51	dec0h 12755	. . . . . . . . . . 11 ⊢ 0 = ;00
425	423, 424	eqtri 2765	. . . . . . . . . 10 ⊢ (4 · 0) = ;00
426	113	addridi 11448	. . . . . . . . . . . 12 ⊢ (4 + 0) = 4
427	426	oveq1i 7441	. . . . . . . . . . 11 ⊢ ((4 + 0) + 0) = (4 + 0)
428	427, 426, 205	3eqtri 2769	. . . . . . . . . 10 ⊢ ((4 + 0) + 0) = ;04
429	1, 24, 1, 51, 51, 51, 24, 51, 116, 422, 203, 425, 428, 192	dpmul 32895	. . . . . . . . 9 ⊢ ((1.4) · (1.0)) = (1._40)
430		3cn 12347	. . . . . . . . . . 11 ⊢ 3 ∈ ℂ
431		3t2e6 12432	. . . . . . . . . . 11 ⊢ (3 · 2) = 6
432	430, 197, 431	mulcomli 11270	. . . . . . . . . 10 ⊢ (2 · 3) = 6
433		9t2e18 12855	. . . . . . . . . . 11 ⊢ (9 · 2) = ;18
434	196, 197, 433	mulcomli 11270	. . . . . . . . . 10 ⊢ (2 · 9) = ;18
435		7t3e21 12843	. . . . . . . . . 10 ⊢ (7 · 3) = ;21
436		9t7e63 12860	. . . . . . . . . . 11 ⊢ (9 · 7) = ;63
437	196, 217, 436	mulcomli 11270	. . . . . . . . . 10 ⊢ (7 · 9) = ;63
438		eqid 2737	. . . . . . . . . . . . 13 ⊢ ;21 = ;21
439		eqid 2737	. . . . . . . . . . . . 13 ⊢ ;18 = ;18
440	159, 160	eqtri 2765	. . . . . . . . . . . . 13 ⊢ (1 + 8) = 9
441	181, 1, 1, 73, 438, 439, 224, 440	decadd 12787	. . . . . . . . . . . 12 ⊢ (;21 + ;18) = ;39
442	441	oveq1i 7441	. . . . . . . . . . 11 ⊢ ((;21 + ;18) + 6) = (;39 + 6)
443		eqid 2737	. . . . . . . . . . . 12 ⊢ ;39 = ;39
444		3p1e4 12411	. . . . . . . . . . . 12 ⊢ (3 + 1) = 4
445		9p6e15 12824	. . . . . . . . . . . 12 ⊢ (9 + 6) = ;15
446	182, 53, 98, 443, 444, 54, 445	decaddci 12794	. . . . . . . . . . 11 ⊢ (;39 + 6) = ;45
447	442, 446	eqtri 2765	. . . . . . . . . 10 ⊢ ((;21 + ;18) + 6) = ;45
448		6p4e10 12805	. . . . . . . . . 10 ⊢ (6 + 4) = ;10
449	181, 52, 182, 53, 98, 24, 54, 182, 432, 434, 435, 437, 447, 448	dpmul 32895	. . . . . . . . 9 ⊢ ((2.7) · (3.9)) = (;10._53)
450	1, 24	deccl 12748	. . . . . . . . . . 11 ⊢ ;14 ∈ ℕ0
451	450, 51	deccl 12748	. . . . . . . . . 10 ⊢ ;;140 ∈ ℕ0
452	417, 73	eqeltrri 2838	. . . . . . . . . 10 ⊢ ;08 ∈ ℕ0
453		eqid 2737	. . . . . . . . . 10 ⊢ ;;;1401 = ;;;1401
454		eqid 2737	. . . . . . . . . 10 ⊢ ;;082 = ;;082
455		eqid 2737	. . . . . . . . . . 11 ⊢ ;;140 = ;;140
456	417, 158	eqeltrri 2838	. . . . . . . . . . . 12 ⊢ ;08 ∈ ℂ
457		0cn 11253	. . . . . . . . . . . 12 ⊢ 0 ∈ ℂ
458	417	oveq1i 7441	. . . . . . . . . . . . 13 ⊢ (8 + 0) = (;08 + 0)
459	158	addridi 11448	. . . . . . . . . . . . 13 ⊢ (8 + 0) = 8
460	458, 459	eqtr3i 2767	. . . . . . . . . . . 12 ⊢ (;08 + 0) = 8
461	456, 457, 460	addcomli 11453	. . . . . . . . . . 11 ⊢ (0 + ;08) = 8
462	450, 51, 452, 455, 461	decaddi 12793	. . . . . . . . . 10 ⊢ (;;140 + ;08) = ;;148
463	451, 1, 452, 181, 453, 454, 462, 230	decadd 12787	. . . . . . . . 9 ⊢ (;;;1401 + ;;082) = ;;;1483
464		4t4e16 12832	. . . . . . . . . . 11 ⊢ (4 · 4) = ;16
465		9t4e36 12857	. . . . . . . . . . . 12 ⊢ (9 · 4) = ;36
466	196, 113, 465	mulcomli 11270	. . . . . . . . . . 11 ⊢ (4 · 9) = ;36
467	196	mulridi 11265	. . . . . . . . . . . . 13 ⊢ (9 · 1) = 9
468	467, 188	eqtri 2765	. . . . . . . . . . . 12 ⊢ (9 · 1) = ;09
469	196, 138, 468	mulcomli 11270	. . . . . . . . . . 11 ⊢ (1 · 9) = ;09
470	182, 98	deccl 12748	. . . . . . . . . . . . . . 15 ⊢ ;36 ∈ ℕ0
471	470	nn0cni 12538	. . . . . . . . . . . . . 14 ⊢ ;36 ∈ ℂ
472		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ ;36 = ;36
473	182, 98, 24, 472, 444, 51, 448	decaddci 12794	. . . . . . . . . . . . . 14 ⊢ (;36 + 4) = ;40
474	471, 113, 473	addcomli 11453	. . . . . . . . . . . . 13 ⊢ (4 + ;36) = ;40
475	474	oveq1i 7441	. . . . . . . . . . . 12 ⊢ ((4 + ;36) + 0) = (;40 + 0)
476	24, 51	deccl 12748	. . . . . . . . . . . . . 14 ⊢ ;40 ∈ ℕ0
477	476	nn0cni 12538	. . . . . . . . . . . . 13 ⊢ ;40 ∈ ℂ
478	477	addridi 11448	. . . . . . . . . . . 12 ⊢ (;40 + 0) = ;40
479	475, 478	eqtri 2765	. . . . . . . . . . 11 ⊢ ((4 + ;36) + 0) = ;40
480	1, 98, 24, 135, 269, 51, 448	decaddci 12794	. . . . . . . . . . 11 ⊢ (;16 + 4) = ;20
481	24, 1, 24, 53, 51, 24, 51, 53, 464, 466, 204, 469, 479, 480	dpmul 32895	. . . . . . . . . 10 ⊢ ((4.1) · (4.9)) = (;20._09)
482		eqid 2737	. . . . . . . . . . . . 13 ⊢ ;27 = ;27
483	230	oveq1i 7441	. . . . . . . . . . . . . 14 ⊢ ((1 + 2) + 1) = (3 + 1)
484	483, 444	eqtri 2765	. . . . . . . . . . . . 13 ⊢ ((1 + 2) + 1) = 4
485	1, 24, 181, 52, 268, 482, 484, 1, 225	decaddc 12788	. . . . . . . . . . . 12 ⊢ (;14 + ;27) = ;41
486	1, 24, 181, 52, 24, 1, 485	dpadd 32893	. . . . . . . . . . 11 ⊢ ((1.4) + (2.7)) = (4.1)
487	430, 138, 444	addcomli 11453	. . . . . . . . . . . . 13 ⊢ (1 + 3) = 4
488	196	addlidi 11449	. . . . . . . . . . . . 13 ⊢ (0 + 9) = 9
489	1, 51, 182, 53, 414, 443, 487, 488	decadd 12787	. . . . . . . . . . . 12 ⊢ (;10 + ;39) = ;49
490	1, 51, 182, 53, 24, 53, 489	dpadd 32893	. . . . . . . . . . 11 ⊢ ((1.0) + (3.9)) = (4.9)
491	486, 490	oveq12i 7443	. . . . . . . . . 10 ⊢ (((1.4) + (2.7)) · ((1.0) + (3.9))) = ((4.1) · (4.9))
492	1, 24, 73, 1, 268, 415, 440, 210	decadd 12787	. . . . . . . . . . . . . 14 ⊢ (;14 + ;81) = ;95
493	450, 51, 412, 98, 455, 413, 492, 111	decadd 12787	. . . . . . . . . . . . 13 ⊢ (;;140 + ;;816) = ;;956
494	1, 24, 51, 73, 1, 53, 98, 54, 98, 493	dpadd3 32894	. . . . . . . . . . . 12 ⊢ ((1._40) + (8._16)) = (9._56)
495	494	oveq1i 7441	. . . . . . . . . . 11 ⊢ (((1._40) + (8._16)) + (;10._53)) = ((9._56) + (;10._53))
496	181, 51	deccl 12748	. . . . . . . . . . . 12 ⊢ ;20 ∈ ℕ0
497	53, 54	deccl 12748	. . . . . . . . . . . . 13 ⊢ ;95 ∈ ℕ0
498	130, 54	deccl 12748	. . . . . . . . . . . . 13 ⊢ ;;105 ∈ ℕ0
499		eqid 2737	. . . . . . . . . . . . 13 ⊢ ;;956 = ;;956
500		eqid 2737	. . . . . . . . . . . . 13 ⊢ ;;;1053 = ;;;1053
501		eqid 2737	. . . . . . . . . . . . . 14 ⊢ ;95 = ;95
502		eqid 2737	. . . . . . . . . . . . . 14 ⊢ ;;105 = ;;105
503		dec10p 12776	. . . . . . . . . . . . . . . . 17 ⊢ (;10 + 9) = ;19
504	283, 196, 503	addcomli 11453	. . . . . . . . . . . . . . . 16 ⊢ (9 + ;10) = ;19
505	504	oveq1i 7441	. . . . . . . . . . . . . . 15 ⊢ ((9 + ;10) + 1) = (;19 + 1)
506		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ ;19 = ;19
507	1, 53, 1, 506, 269, 51, 194	decaddci 12794	. . . . . . . . . . . . . . 15 ⊢ (;19 + 1) = ;20
508	505, 507	eqtri 2765	. . . . . . . . . . . . . 14 ⊢ ((9 + ;10) + 1) = ;20
509		5p5e10 12804	. . . . . . . . . . . . . 14 ⊢ (5 + 5) = ;10
510	53, 54, 130, 54, 501, 502, 508, 51, 509	decaddc 12788	. . . . . . . . . . . . 13 ⊢ (;95 + ;;105) = ;;200
511	497, 98, 498, 182, 499, 500, 510, 233	decadd 12787	. . . . . . . . . . . 12 ⊢ (;;956 + ;;;1053) = ;;;2009
512	53, 54, 98, 130, 54, 496, 182, 51, 53, 511	dpadd3 32894	. . . . . . . . . . 11 ⊢ ((9._56) + (;10._53)) = (;20._09)
513	495, 512	eqtri 2765	. . . . . . . . . 10 ⊢ (((1._40) + (8._16)) + (;10._53)) = (;20._09)
514	481, 491, 513	3eqtr4i 2775	. . . . . . . . 9 ⊢ (((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 32896	. . . . . . . 8 ⊢ ((1._4_27) · (1._0_39)) < (1._4_83)
516	375, 395	remulcli 11277	. . . . . . . . 9 ⊢ ((1._4_27) · (1._0_39)) ∈ ℝ
517	345, 516, 350	lttri 11387	. . . . . . . 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))
518	410, 515, 517	mp2an 692	. . . . . . 7 ⊢ ((1._4_2_63) · (1._0_3_8_83)) < (1._4_83)
519	367, 518	pm3.2i 470	. . . . . 6 ⊢ (0 ≤ ((1._4_2_63) · (1._0_3_8_83)) ∧ ((1._4_2_63) · (1._0_3_8_83)) < (1._4_83))
520	351, 519	pm3.2i 470	. . . . 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)))
521		ltmul12a 12123	. . . . 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)))
522	316, 520, 521	mp2an 692	. . . 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))
523	24, 181	deccl 12748	. . . . 5 ⊢ ;42 ∈ ℕ0
524	496, 24	deccl 12748	. . . . . 6 ⊢ ;;204 ∈ ℕ0
525		eqid 2737	. . . . . 6 ⊢ ;;;2042 = ;;;2042
526		eqid 2737	. . . . . 6 ⊢ ;42 = ;42
527		eqid 2737	. . . . . . 7 ⊢ ;;204 = ;;204
528	496, 24, 24, 527, 277	decaddi 12793	. . . . . 6 ⊢ (;;204 + 4) = ;;208
529		2p2e4 12401	. . . . . 6 ⊢ (2 + 2) = 4
530	524, 181, 24, 181, 525, 526, 528, 529	decadd 12787	. . . . 5 ⊢ (;;;2042 + ;42) = ;;;2084
531	448	oveq1i 7441	. . . . . . 7 ⊢ ((6 + 4) + 2) = (;10 + 2)
532		dec10p 12776	. . . . . . 7 ⊢ (;10 + 2) = ;12
533	531, 532	eqtri 2765	. . . . . 6 ⊢ ((6 + 4) + 2) = ;12
534	1, 98, 1, 24, 181, 1, 181, 24, 116, 204, 215, 216, 533, 269	dpmul 32895	. . . . 5 ⊢ ((1.6) · (1.4)) = (2._24)
535		8t5e40 12851	. . . . . . 7 ⊢ (8 · 5) = ;40
536	158, 256, 535	mulcomli 11270	. . . . . 6 ⊢ (5 · 8) = ;40
537		5t3e15 12834	. . . . . 6 ⊢ (5 · 3) = ;15
538	158	mullidi 11266	. . . . . 6 ⊢ (1 · 8) = 8
539	430	mullidi 11266	. . . . . . 7 ⊢ (1 · 3) = 3
540	182	dec0h 12755	. . . . . . 7 ⊢ 3 = ;03
541	539, 540	eqtri 2765	. . . . . 6 ⊢ (1 · 3) = ;03
542	235	nn0cni 12538	. . . . . . . . 9 ⊢ ;15 ∈ ℂ
543		8p5e13 12816	. . . . . . . . . . 11 ⊢ (8 + 5) = ;13
544	158, 256, 543	addcomli 11453	. . . . . . . . . 10 ⊢ (5 + 8) = ;13
545	1, 54, 73, 245, 269, 182, 544	decaddci 12794	. . . . . . . . 9 ⊢ (;15 + 8) = ;23
546	542, 158, 545	addcomli 11453	. . . . . . . 8 ⊢ (8 + ;15) = ;23
547	546	oveq1i 7441	. . . . . . 7 ⊢ ((8 + ;15) + 0) = (;23 + 0)
548	181, 182	deccl 12748	. . . . . . . . 9 ⊢ ;23 ∈ ℕ0
549	548	nn0cni 12538	. . . . . . . 8 ⊢ ;23 ∈ ℂ
550	549	addridi 11448	. . . . . . 7 ⊢ (;23 + 0) = ;23
551	547, 550	eqtri 2765	. . . . . 6 ⊢ ((8 + ;15) + 0) = ;23
552		eqid 2737	. . . . . . 7 ⊢ ;40 = ;40
553	197	addlidi 11449	. . . . . . 7 ⊢ (0 + 2) = 2
554	24, 51, 181, 552, 553	decaddi 12793	. . . . . 6 ⊢ (;40 + 2) = ;42
555	54, 1, 73, 182, 51, 181, 182, 182, 536, 537, 538, 541, 551, 554	dpmul 32895	. . . . 5 ⊢ ((5.1) · (8.3)) = (;42._33)
556	181, 181	deccl 12748	. . . . . . 7 ⊢ ;22 ∈ ℕ0
557	556, 24	deccl 12748	. . . . . 6 ⊢ ;;224 ∈ ℕ0
558		eqid 2737	. . . . . 6 ⊢ ;;;2241 = ;;;2241
559		eqid 2737	. . . . . 6 ⊢ ;;208 = ;;208
560		eqid 2737	. . . . . . 7 ⊢ ;;224 = ;;224
561		eqid 2737	. . . . . . 7 ⊢ ;20 = ;20
562		eqid 2737	. . . . . . . 8 ⊢ ;22 = ;22
563	181, 181, 181, 562, 529	decaddi 12793	. . . . . . 7 ⊢ (;22 + 2) = ;24
564	556, 24, 181, 51, 560, 561, 563, 426	decadd 12787	. . . . . 6 ⊢ (;;224 + ;20) = ;;244
565	557, 1, 496, 73, 558, 559, 564, 440	decadd 12787	. . . . 5 ⊢ (;;;2241 + ;;208) = ;;;2449
566	556, 98	deccl 12748	. . . . . . . 8 ⊢ ;;226 ∈ ℕ0
567	523, 182	deccl 12748	. . . . . . . 8 ⊢ ;;423 ∈ ℕ0
568		eqid 2737	. . . . . . . 8 ⊢ ;;;2266 = ;;;2266
569		eqid 2737	. . . . . . . 8 ⊢ ;;;4233 = ;;;4233
570		eqid 2737	. . . . . . . . 9 ⊢ ;;226 = ;;226
571		eqid 2737	. . . . . . . . 9 ⊢ ;;423 = ;;423
572	113, 197, 289	addcomli 11453	. . . . . . . . . 10 ⊢ (2 + 4) = 6
573	181, 181, 24, 181, 562, 526, 572, 529	decadd 12787	. . . . . . . . 9 ⊢ (;22 + ;42) = ;64
574	556, 98, 523, 182, 570, 571, 573, 233	decadd 12787	. . . . . . . 8 ⊢ (;;226 + ;;423) = ;;649
575	566, 98, 567, 182, 568, 569, 574, 233	decadd 12787	. . . . . . 7 ⊢ (;;;2266 + ;;;4233) = ;;;6499
576	556, 98, 98, 523, 182, 100, 182, 53, 53, 575	dpadd3 32894	. . . . . 6 ⊢ ((;22._66) + (;42._33)) = (;64._99)
577	496	nn0cni 12538	. . . . . . . . . . 11 ⊢ ;20 ∈ ℂ
578	181, 51, 181, 561, 553	decaddi 12793	. . . . . . . . . . 11 ⊢ (;20 + 2) = ;22
579	577, 197, 578	addcomli 11453	. . . . . . . . . 10 ⊢ (2 + ;20) = ;22
580	181, 181, 496, 24, 562, 527, 579, 572	decadd 12787	. . . . . . . . 9 ⊢ (;22 + ;;204) = ;;226
581	556, 24, 524, 181, 560, 525, 580, 289	decadd 12787	. . . . . . . 8 ⊢ (;;224 + ;;;2042) = ;;;2266
582	181, 181, 24, 496, 24, 556, 181, 98, 98, 581	dpadd3 32894	. . . . . . 7 ⊢ ((2._24) + (;20._42)) = (;22._66)
583	582	oveq1i 7441	. . . . . 6 ⊢ (((2._24) + (;20._42)) + (;42._33)) = ((;22._66) + (;42._33))
584		eqid 2737	. . . . . . . . . 10 ⊢ ;51 = ;51
585	1, 98, 54, 1, 135, 584, 257, 140	decadd 12787	. . . . . . . . 9 ⊢ (;16 + ;51) = ;67
586	1, 98, 54, 1, 98, 52, 585	dpadd 32893	. . . . . . . 8 ⊢ ((1.6) + (5.1)) = (6.7)
587		eqid 2737	. . . . . . . . . 10 ⊢ ;83 = ;83
588	1, 24, 73, 182, 268, 587, 440, 302	decadd 12787	. . . . . . . . 9 ⊢ (;14 + ;83) = ;97
589	1, 24, 73, 182, 53, 52, 588	dpadd 32893	. . . . . . . 8 ⊢ ((1.4) + (8.3)) = (9.7)
590	586, 589	oveq12i 7443	. . . . . . 7 ⊢ (((1.6) + (5.1)) · ((1.4) + (8.3))) = ((6.7) · (9.7))
591		9t6e54 12859	. . . . . . . . 9 ⊢ (9 · 6) = ;54
592	196, 110, 591	mulcomli 11270	. . . . . . . 8 ⊢ (6 · 9) = ;54
593		7t6e42 12846	. . . . . . . . 9 ⊢ (7 · 6) = ;42
594	217, 110, 593	mulcomli 11270	. . . . . . . 8 ⊢ (6 · 7) = ;42
595		7t7e49 12847	. . . . . . . 8 ⊢ (7 · 7) = ;49
596		eqid 2737	. . . . . . . . . . 11 ⊢ ;63 = ;63
597		3p2e5 12417	. . . . . . . . . . 11 ⊢ (3 + 2) = 5
598	98, 182, 24, 181, 596, 526, 448, 597	decadd 12787	. . . . . . . . . 10 ⊢ (;63 + ;42) = ;;105
599	598	oveq1i 7441	. . . . . . . . 9 ⊢ ((;63 + ;42) + 4) = (;;105 + 4)
600		5p4e9 12424	. . . . . . . . . 10 ⊢ (5 + 4) = 9
601	130, 54, 24, 502, 600	decaddi 12793	. . . . . . . . 9 ⊢ (;;105 + 4) = ;;109
602	599, 601	eqtri 2765	. . . . . . . 8 ⊢ ((;63 + ;42) + 4) = ;;109
603		eqid 2737	. . . . . . . . 9 ⊢ ;54 = ;54
604	54, 24, 1, 51, 603, 414, 246, 426	decadd 12787	. . . . . . . 8 ⊢ (;54 + ;10) = ;64
605	98, 52, 53, 52, 24, 130, 53, 53, 592, 594, 437, 595, 602, 604	dpmul 32895	. . . . . . 7 ⊢ ((6.7) · (9.7)) = (;64._99)
606	590, 605	eqtri 2765	. . . . . 6 ⊢ (((1.6) + (5.1)) · ((1.4) + (8.3))) = (;64._99)
607	576, 583, 606	3eqtr4ri 2776	. . . . 5 ⊢ (((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 32896	. . . 4 ⊢ ((1._6_51) · (1._4_83)) < (2._4_49)
609	33, 345	remulcli 11277	. . . . 5 ⊢ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) ∈ ℝ
610	43, 350	remulcli 11277	. . . . 5 ⊢ ((1._6_51) · (1._4_83)) ∈ ℝ
611	24, 399	rpdp2cl 32864	. . . . . . . 8 ⊢ _49 ∈ ℝ+
612	24, 611	rpdp2cl 32864	. . . . . . 7 ⊢ _4_49 ∈ ℝ+
613	181, 612	rpdpcl 32885	. . . . . 6 ⊢ (2._4_49) ∈ ℝ+
614		rpre 13043	. . . . . 6 ⊢ ((2._4_49) ∈ ℝ+ → (2._4_49) ∈ ℝ)
615	613, 614	ax-mp 5	. . . . 5 ⊢ (2._4_49) ∈ ℝ
616	609, 610, 615	lttri 11387	. . . 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))
617	522, 608, 616	mp2an 692	. . 3 ⊢ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) < (2._4_49)
618		3pos 12371	. . . 4 ⊢ 0 < 3
619	609, 615, 319	ltmul2i 12189	. . . 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))))
620	618, 619	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)))
621	617, 620	mpbi 230	. 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))
622	119	dp2eq2i 32858	. . . . . . 7 ⊢ _0_00 = _00
623	622, 119	eqtri 2765	. . . . . 6 ⊢ _0_00 = 0
624	623	oveq2i 7442	. . . . 5 ⊢ (3._0_00) = (3.0)
625	182	dp0u 32883	. . . . 5 ⊢ (3.0) = 3
626	624, 625	eqtr2i 2766	. . . 4 ⊢ 3 = (3._0_00)
627	626	oveq1i 7441	. . 3 ⊢ (3 · (2._4_49)) = ((3._0_00) · (2._4_49))
628	450, 52	deccl 12748	. . . . . . 7 ⊢ ;;147 ∈ ℕ0
629	628, 51	deccl 12748	. . . . . 6 ⊢ ;;;1470 ∈ ℕ0
630	629	nn0cni 12538	. . . . 5 ⊢ ;;;1470 ∈ ℂ
631	630	addridi 11448	. . . 4 ⊢ (;;;1470 + 0) = ;;;1470
632		4t3e12 12831	. . . . . 6 ⊢ (4 · 3) = ;12
633	113, 430, 632	mulcomli 11270	. . . . 5 ⊢ (3 · 4) = ;12
634	197	mul02i 11450	. . . . 5 ⊢ (0 · 2) = 0
635	113, 457, 425	mulcomli 11270	. . . . 5 ⊢ (0 · 4) = ;00
636	51, 51, 1, 181, 424, 300, 153, 553	decadd 12787	. . . . . . 7 ⊢ (0 + ;12) = ;12
637	636	oveq1i 7441	. . . . . 6 ⊢ ((0 + ;12) + 0) = (;12 + 0)
638	281	nn0cni 12538	. . . . . . 7 ⊢ ;12 ∈ ℂ
639	638	addridi 11448	. . . . . 6 ⊢ (;12 + 0) = ;12
640	637, 639	eqtri 2765	. . . . 5 ⊢ ((0 + ;12) + 0) = ;12
641	182, 51, 181, 24, 51, 1, 181, 51, 431, 633, 634, 635, 640, 140	dpmul 32895	. . . 4 ⊢ ((3.0) · (2.4)) = (7._20)
642	51	dp0u 32883	. . . . . . 7 ⊢ (0.0) = 0
643	642	oveq1i 7441	. . . . . 6 ⊢ ((0.0) · (4.9)) = (0 · (4.9))
644		dpcl 32873	. . . . . . . . 9 ⊢ ((4 ∈ ℕ0 ∧ 9 ∈ ℝ) → (4.9) ∈ ℝ)
645	24, 4, 644	mp2an 692	. . . . . . . 8 ⊢ (4.9) ∈ ℝ
646	645	recni 11275	. . . . . . 7 ⊢ (4.9) ∈ ℂ
647	646	mul02i 11450	. . . . . 6 ⊢ (0 · (4.9)) = 0
648	643, 647	eqtri 2765	. . . . 5 ⊢ ((0.0) · (4.9)) = 0
649	119	oveq2i 7442	. . . . . 6 ⊢ (0._00) = (0.0)
650	649, 642	eqtri 2765	. . . . 5 ⊢ (0._00) = 0
651	648, 650	eqtr4i 2768	. . . 4 ⊢ ((0.0) · (4.9)) = (0._00)
652	52, 181	deccl 12748	. . . . . 6 ⊢ ;72 ∈ ℕ0
653	652, 51	deccl 12748	. . . . 5 ⊢ ;;720 ∈ ℕ0
654		eqid 2737	. . . . 5 ⊢ ;;;7201 = ;;;7201
655		eqid 2737	. . . . 5 ⊢ ;;147 = ;;147
656		eqid 2737	. . . . . 6 ⊢ ;;720 = ;;720
657	52, 181, 224, 263	decsuc 12764	. . . . . 6 ⊢ (;72 + 1) = ;73
658	652, 51, 1, 24, 656, 268, 657, 114	decadd 12787	. . . . 5 ⊢ (;;720 + ;14) = ;;734
659	653, 1, 450, 52, 654, 655, 658, 274	decadd 12787	. . . 4 ⊢ (;;;7201 + ;;147) = ;;;7348
660	642	oveq2i 7442	. . . . . . . 8 ⊢ ((3.0) + (0.0)) = ((3.0) + 0)
661	625, 430	eqeltri 2837	. . . . . . . . 9 ⊢ (3.0) ∈ ℂ
662	661	addridi 11448	. . . . . . . 8 ⊢ ((3.0) + 0) = (3.0)
663	660, 662	eqtri 2765	. . . . . . 7 ⊢ ((3.0) + (0.0)) = (3.0)
664		eqid 2737	. . . . . . . . 9 ⊢ ;49 = ;49
665	572	oveq1i 7441	. . . . . . . . . 10 ⊢ ((2 + 4) + 1) = (6 + 1)
666	665, 140	eqtri 2765	. . . . . . . . 9 ⊢ ((2 + 4) + 1) = 7
667		9p4e13 12822	. . . . . . . . . 10 ⊢ (9 + 4) = ;13
668	196, 113, 667	addcomli 11453	. . . . . . . . 9 ⊢ (4 + 9) = ;13
669	181, 24, 24, 53, 223, 664, 666, 182, 668	decaddc 12788	. . . . . . . 8 ⊢ (;24 + ;49) = ;73
670	181, 24, 24, 53, 52, 182, 669	dpadd 32893	. . . . . . 7 ⊢ ((2.4) + (4.9)) = (7.3)
671	663, 670	oveq12i 7443	. . . . . 6 ⊢ (((3.0) + (0.0)) · ((2.4) + (4.9))) = ((3.0) · (7.3))
672	217, 430, 435	mulcomli 11270	. . . . . . 7 ⊢ (3 · 7) = ;21
673		3t3e9 12433	. . . . . . 7 ⊢ (3 · 3) = 9
674	217	mul01i 11451	. . . . . . . 8 ⊢ (7 · 0) = 0
675	217, 457, 674	mulcomli 11270	. . . . . . 7 ⊢ (0 · 7) = 0
676	430	mul01i 11451	. . . . . . . . 9 ⊢ (3 · 0) = 0
677	676, 424	eqtri 2765	. . . . . . . 8 ⊢ (3 · 0) = ;00
678	430, 457, 677	mulcomli 11270	. . . . . . 7 ⊢ (0 · 3) = ;00
679	196	addridi 11448	. . . . . . . . . 10 ⊢ (9 + 0) = 9
680	679	oveq1i 7441	. . . . . . . . 9 ⊢ ((9 + 0) + 0) = (9 + 0)
681	680, 679, 188	3eqtri 2769	. . . . . . . 8 ⊢ ((9 + 0) + 0) = ;09
682	196, 457	addcomi 11452	. . . . . . . . . 10 ⊢ (9 + 0) = (0 + 9)
683	682	oveq1i 7441	. . . . . . . . 9 ⊢ ((9 + 0) + 0) = ((0 + 9) + 0)
684	683	eqeq1i 2742	. . . . . . . 8 ⊢ (((9 + 0) + 0) = ;09 ↔ ((0 + 9) + 0) = ;09)
685	681, 684	mpbi 230	. . . . . . 7 ⊢ ((0 + 9) + 0) = ;09
686	181, 1, 51, 438, 192	decaddi 12793	. . . . . . 7 ⊢ (;21 + 0) = ;21
687	182, 51, 52, 182, 51, 51, 53, 51, 672, 673, 675, 678, 685, 686	dpmul 32895	. . . . . 6 ⊢ ((3.0) · (7.3)) = (;21._90)
688	671, 687	eqtri 2765	. . . . 5 ⊢ (((3.0) + (0.0)) · ((2.4) + (4.9))) = (;21._90)
689	650	oveq2i 7442	. . . . . 6 ⊢ (((7._20) + (;14._70)) + (0._00)) = (((7._20) + (;14._70)) + 0)
690	318, 2	pm3.2i 470	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ ∧ 0 ∈ ℝ)
691		dp2cl 32862	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ 0 ∈ ℝ) → _20 ∈ ℝ)
692	690, 691	ax-mp 5	. . . . . . . . . 10 ⊢ _20 ∈ ℝ
693		dpcl 32873	. . . . . . . . . 10 ⊢ ((7 ∈ ℕ0 ∧ _20 ∈ ℝ) → (7._20) ∈ ℝ)
694	52, 692, 693	mp2an 692	. . . . . . . . 9 ⊢ (7._20) ∈ ℝ
695	694	recni 11275	. . . . . . . 8 ⊢ (7._20) ∈ ℂ
696	3, 2	pm3.2i 470	. . . . . . . . . . 11 ⊢ (7 ∈ ℝ ∧ 0 ∈ ℝ)
697		dp2cl 32862	. . . . . . . . . . 11 ⊢ ((7 ∈ ℝ ∧ 0 ∈ ℝ) → _70 ∈ ℝ)
698	696, 697	ax-mp 5	. . . . . . . . . 10 ⊢ _70 ∈ ℝ
699		dpcl 32873	. . . . . . . . . 10 ⊢ ((;14 ∈ ℕ0 ∧ _70 ∈ ℝ) → (;14._70) ∈ ℝ)
700	450, 698, 699	mp2an 692	. . . . . . . . 9 ⊢ (;14._70) ∈ ℝ
701	700	recni 11275	. . . . . . . 8 ⊢ (;14._70) ∈ ℂ
702	695, 701	addcli 11267	. . . . . . 7 ⊢ ((7._20) + (;14._70)) ∈ ℂ
703	702	addridi 11448	. . . . . 6 ⊢ (((7._20) + (;14._70)) + 0) = ((7._20) + (;14._70))
704		eqid 2737	. . . . . . . 8 ⊢ ;;;1470 = ;;;1470
705	450	nn0cni 12538	. . . . . . . . . 10 ⊢ ;14 ∈ ℂ
706	705, 217, 270	addcomli 11453	. . . . . . . . 9 ⊢ (7 + ;14) = ;21
707		7p2e9 12427	. . . . . . . . . 10 ⊢ (7 + 2) = 9
708	217, 197, 707	addcomli 11453	. . . . . . . . 9 ⊢ (2 + 7) = 9
709	52, 181, 450, 52, 263, 655, 706, 708	decadd 12787	. . . . . . . 8 ⊢ (;72 + ;;147) = ;;219
710		00id 11436	. . . . . . . 8 ⊢ (0 + 0) = 0
711	652, 51, 628, 51, 656, 704, 709, 710	decadd 12787	. . . . . . 7 ⊢ (;;720 + ;;;1470) = ;;;2190
712	52, 181, 51, 450, 52, 293, 51, 53, 51, 711	dpadd3 32894	. . . . . 6 ⊢ ((7._20) + (;14._70)) = (;21._90)
713	689, 703, 712	3eqtri 2769	. . . . 5 ⊢ (((7._20) + (;14._70)) + (0._00)) = (;21._90)
714	688, 713	eqtr4i 2768	. . . 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, 450, 52, 51, 51, 51, 51, 1, 24, 52, 51, 52, 182, 24, 73, 102, 102, 102, 631, 641, 651, 659, 714	dpmul4 32896	. . 3 ⊢ ((3._0_00) · (2._4_49)) < (7._3_48)
716	627, 715	eqbrtri 5164	. 2 ⊢ (3 · (2._4_49)) < (7._3_48)
717	319, 609	remulcli 11277	. . 3 ⊢ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) ∈ ℝ
718	319, 615	remulcli 11277	. . 3 ⊢ (3 · (2._4_49)) ∈ ℝ
719		nnrp 13046	. . . . . . . 8 ⊢ (8 ∈ ℕ → 8 ∈ ℝ+)
720	63, 719	ax-mp 5	. . . . . . 7 ⊢ 8 ∈ ℝ+
721	24, 720	rpdp2cl 32864	. . . . . 6 ⊢ _48 ∈ ℝ+
722	182, 721	rpdp2cl 32864	. . . . 5 ⊢ _3_48 ∈ ℝ+
723	52, 722	rpdpcl 32885	. . . 4 ⊢ (7._3_48) ∈ ℝ+
724		rpre 13043	. . . 4 ⊢ ((7._3_48) ∈ ℝ+ → (7._3_48) ∈ ℝ)
725	723, 724	ax-mp 5	. . 3 ⊢ (7._3_48) ∈ ℝ
726	717, 718, 725	lttri 11387	. 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	621, 716, 726	mp2an 692	1 ⊢ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83)))) < (7._3_48)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108   class class class wbr 5143  (class class class)co 7431  ℂcc 11153  ℝcr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   < clt 11295   ≤ cle 11296  ℕcn 12266  2c2 12321  3c3 12322  4c4 12323  5c5 12324  6c6 12325  7c7 12326  8c8 12327  9c9 12328  ℕ₀cn0 12526  ;cdc 12733  ℝ⁺crp 13034  ↑cexp 14102  _cdp2 32853  .cdp 32870

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-rp 13035  df-seq 14043  df-exp 14103  df-dp2 32854  df-dp 32871

This theorem is referenced by:  hgt750leme  34673