Theorem hgt750lem2 31923

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 11914	. . . . . . . . . 10 ⊢ 1 ∈ ℕ0
2		0re 10643	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
3		7re 11731	. . . . . . . . . . . . . 14 ⊢ 7 ∈ ℝ
4		9re 11737	. . . . . . . . . . . . . . . 16 ⊢ 9 ∈ ℝ
5		5re 11725	. . . . . . . . . . . . . . . . . . . 20 ⊢ 5 ∈ ℝ
6	5, 5	pm3.2i 473	. . . . . . . . . . . . . . . . . . 19 ⊢ (5 ∈ ℝ ∧ 5 ∈ ℝ)
7		dp2cl 30556	. . . . . . . . . . . . . . . . . . 19 ⊢ ((5 ∈ ℝ ∧ 5 ∈ ℝ) → _55 ∈ ℝ)
8	6, 7	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ _55 ∈ ℝ
9	4, 8	pm3.2i 473	. . . . . . . . . . . . . . . . 17 ⊢ (9 ∈ ℝ ∧ _55 ∈ ℝ)
10		dp2cl 30556	. . . . . . . . . . . . . . . . 17 ⊢ ((9 ∈ ℝ ∧ _55 ∈ ℝ) → _9_55 ∈ ℝ)
11	9, 10	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ _9_55 ∈ ℝ
12	4, 11	pm3.2i 473	. . . . . . . . . . . . . . 15 ⊢ (9 ∈ ℝ ∧ _9_55 ∈ ℝ)
13		dp2cl 30556	. . . . . . . . . . . . . . 15 ⊢ ((9 ∈ ℝ ∧ _9_55 ∈ ℝ) → _9_9_55 ∈ ℝ)
14	12, 13	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ _9_9_55 ∈ ℝ
15	3, 14	pm3.2i 473	. . . . . . . . . . . . 13 ⊢ (7 ∈ ℝ ∧ _9_9_55 ∈ ℝ)
16		dp2cl 30556	. . . . . . . . . . . . 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 473	. . . . . . . . . . 11 ⊢ (0 ∈ ℝ ∧ _7_9_9_55 ∈ ℝ)
19		dp2cl 30556	. . . . . . . . . . 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 30567	. . . . . . . . . 10 ⊢ ((1 ∈ ℕ0 ∧ _0_7_9_9_55 ∈ ℝ) → (1._0_7_9_9_55) ∈ ℝ)
22	1, 20, 21	mp2an 690	. . . . . . . . 9 ⊢ (1._0_7_9_9_55) ∈ ℝ
23	22	resqcli 13550	. . . . . . . 8 ⊢ ((1._0_7_9_9_55)↑2) ∈ ℝ
24		4nn0 11917	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ0
25		4nn 11721	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℕ
26		nnrp 12401	. . . . . . . . . . . . 13 ⊢ (4 ∈ ℕ → 4 ∈ ℝ+)
27	25, 26	ax-mp 5	. . . . . . . . . . . 12 ⊢ 4 ∈ ℝ+
28	1, 27	rpdp2cl 30558	. . . . . . . . . . 11 ⊢ _14 ∈ ℝ+
29	24, 28	rpdp2cl 30558	. . . . . . . . . 10 ⊢ _4_14 ∈ ℝ+
30	1, 29	rpdpcl 30579	. . . . . . . . 9 ⊢ (1._4_14) ∈ ℝ+
31		rpre 12398	. . . . . . . . 9 ⊢ ((1._4_14) ∈ ℝ+ → (1._4_14) ∈ ℝ)
32	30, 31	ax-mp 5	. . . . . . . 8 ⊢ (1._4_14) ∈ ℝ
33	23, 32	remulcli 10657	. . . . . . 7 ⊢ (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ
34		6re 11728	. . . . . . . . . 10 ⊢ 6 ∈ ℝ
35		1re 10641	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
36	5, 35	pm3.2i 473	. . . . . . . . . . 11 ⊢ (5 ∈ ℝ ∧ 1 ∈ ℝ)
37		dp2cl 30556	. . . . . . . . . . 11 ⊢ ((5 ∈ ℝ ∧ 1 ∈ ℝ) → _51 ∈ ℝ)
38	36, 37	ax-mp 5	. . . . . . . . . 10 ⊢ _51 ∈ ℝ
39	34, 38	pm3.2i 473	. . . . . . . . 9 ⊢ (6 ∈ ℝ ∧ _51 ∈ ℝ)
40		dp2cl 30556	. . . . . . . . 9 ⊢ ((6 ∈ ℝ ∧ _51 ∈ ℝ) → _6_51 ∈ ℝ)
41	39, 40	ax-mp 5	. . . . . . . 8 ⊢ _6_51 ∈ ℝ
42		dpcl 30567	. . . . . . . 8 ⊢ ((1 ∈ ℕ0 ∧ _6_51 ∈ ℝ) → (1._6_51) ∈ ℝ)
43	1, 41, 42	mp2an 690	. . . . . . 7 ⊢ (1._6_51) ∈ ℝ
44	33, 43	pm3.2i 473	. . . . . 6 ⊢ ((((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ ∧ (1._6_51) ∈ ℝ)
45	22	sqge0i 13552	. . . . . . . 8 ⊢ 0 ≤ ((1._0_7_9_9_55)↑2)
46		rpgt0 12402	. . . . . . . . . 10 ⊢ ((1._4_14) ∈ ℝ+ → 0 < (1._4_14))
47	30, 46	ax-mp 5	. . . . . . . . 9 ⊢ 0 < (1._4_14)
48	2, 32, 47	ltleii 10763	. . . . . . . 8 ⊢ 0 ≤ (1._4_14)
49	23, 32	mulge0i 11187	. . . . . . . 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 690	. . . . . . 7 ⊢ 0 ≤ (((1._0_7_9_9_55)↑2) · (1._4_14))
51		0nn0 11913	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
52		7nn0 11920	. . . . . . . . . . . . . 14 ⊢ 7 ∈ ℕ0
53		9nn0 11922	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ ℕ0
54		5nn0 11918	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℕ0
55		5nn 11724	. . . . . . . . . . . . . . . . . 18 ⊢ 5 ∈ ℕ
56		nnrp 12401	. . . . . . . . . . . . . . . . . 18 ⊢ (5 ∈ ℕ → 5 ∈ ℝ+)
57	55, 56	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℝ+
58	54, 57	rpdp2cl 30558	. . . . . . . . . . . . . . . 16 ⊢ _55 ∈ ℝ+
59	53, 58	rpdp2cl 30558	. . . . . . . . . . . . . . 15 ⊢ _9_55 ∈ ℝ+
60	53, 59	rpdp2cl 30558	. . . . . . . . . . . . . 14 ⊢ _9_9_55 ∈ ℝ+
61	52, 60	rpdp2cl 30558	. . . . . . . . . . . . 13 ⊢ _7_9_9_55 ∈ ℝ+
62	51, 61	rpdp2cl 30558	. . . . . . . . . . . 12 ⊢ _0_7_9_9_55 ∈ ℝ+
63		8nn 11733	. . . . . . . . . . . . . 14 ⊢ 8 ∈ ℕ
64	63	rpdp2cl2 30559	. . . . . . . . . . . . 13 ⊢ _80 ∈ ℝ+
65	51, 64	rpdp2cl 30558	. . . . . . . . . . . 12 ⊢ _0_80 ∈ ℝ+
66		9lt10 12230	. . . . . . . . . . . . . . . 16 ⊢ 9 < ;10
67		5lt10 12234	. . . . . . . . . . . . . . . . . 18 ⊢ 5 < ;10
68	54, 57, 67, 67	dp2lt10 30560	. . . . . . . . . . . . . . . . 17 ⊢ _55 < ;10
69	53, 58, 66, 68	dp2lt10 30560	. . . . . . . . . . . . . . . 16 ⊢ _9_55 < ;10
70	53, 59, 66, 69	dp2lt10 30560	. . . . . . . . . . . . . . 15 ⊢ _9_9_55 < ;10
71		7p1e8 11787	. . . . . . . . . . . . . . 15 ⊢ (7 + 1) = 8
72	52, 60, 70, 71	dp2ltsuc 30562	. . . . . . . . . . . . . 14 ⊢ _7_9_9_55 < 8
73		8nn0 11921	. . . . . . . . . . . . . . 15 ⊢ 8 ∈ ℕ0
74	73	dp20u 30554	. . . . . . . . . . . . . 14 ⊢ _80 = 8
75	72, 74	breqtrri 5093	. . . . . . . . . . . . 13 ⊢ _7_9_9_55 < _80
76	51, 61, 64, 75	dp2lt 30561	. . . . . . . . . . . 12 ⊢ _0_7_9_9_55 < _0_80
77	1, 62, 65, 76	dplt 30580	. . . . . . . . . . 11 ⊢ (1._0_7_9_9_55) < (1._0_80)
78	1, 62	rpdpcl 30579	. . . . . . . . . . . . 13 ⊢ (1._0_7_9_9_55) ∈ ℝ+
79		rpge0 12403	. . . . . . . . . . . . 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 30579	. . . . . . . . . . . . 13 ⊢ (1._0_80) ∈ ℝ+
82		rpge0 12403	. . . . . . . . . . . . 13 ⊢ ((1._0_80) ∈ ℝ+ → 0 ≤ (1._0_80))
83	81, 82	ax-mp 5	. . . . . . . . . . . 12 ⊢ 0 ≤ (1._0_80)
84		8re 11734	. . . . . . . . . . . . . . . . . 18 ⊢ 8 ∈ ℝ
85	84, 2	pm3.2i 473	. . . . . . . . . . . . . . . . 17 ⊢ (8 ∈ ℝ ∧ 0 ∈ ℝ)
86		dp2cl 30556	. . . . . . . . . . . . . . . . 17 ⊢ ((8 ∈ ℝ ∧ 0 ∈ ℝ) → _80 ∈ ℝ)
87	85, 86	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ _80 ∈ ℝ
88	2, 87	pm3.2i 473	. . . . . . . . . . . . . . 15 ⊢ (0 ∈ ℝ ∧ _80 ∈ ℝ)
89		dp2cl 30556	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ ∧ _80 ∈ ℝ) → _0_80 ∈ ℝ)
90	88, 89	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ _0_80 ∈ ℝ
91		dpcl 30567	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℕ0 ∧ _0_80 ∈ ℝ) → (1._0_80) ∈ ℝ)
92	1, 90, 91	mp2an 690	. . . . . . . . . . . . 13 ⊢ (1._0_80) ∈ ℝ
93	22, 92	lt2sqi 13553	. . . . . . . . . . . 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 690	. . . . . . . . . . 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 232	. . . . . . . . . 10 ⊢ ((1._0_7_9_9_55)↑2) < ((1._0_80)↑2)
96	92	recni 10655	. . . . . . . . . . . 12 ⊢ (1._0_80) ∈ ℂ
97	96	sqvali 13544	. . . . . . . . . . 11 ⊢ ((1._0_80)↑2) = ((1._0_80) · (1._0_80))
98		6nn0 11919	. . . . . . . . . . . . 13 ⊢ 6 ∈ ℕ0
99	1, 98	deccl 12114	. . . . . . . . . . . 12 ⊢ ;16 ∈ ℕ0
100	98, 24	deccl 12114	. . . . . . . . . . . 12 ⊢ ;64 ∈ ℕ0
101		4lt10 12235	. . . . . . . . . . . 12 ⊢ 4 < ;10
102		10pos 12116	. . . . . . . . . . . 12 ⊢ 0 < ;10
103	99, 51	deccl 12114	. . . . . . . . . . . . 13 ⊢ ;;160 ∈ ℕ0
104		eqid 2821	. . . . . . . . . . . . 13 ⊢ ;;;1600 = ;;;1600
105		eqid 2821	. . . . . . . . . . . . 13 ⊢ ;64 = ;64
106		eqid 2821	. . . . . . . . . . . . . 14 ⊢ ;;160 = ;;160
107	98	dec0h 12121	. . . . . . . . . . . . . 14 ⊢ 6 = ;06
108	99	nn0cni 11910	. . . . . . . . . . . . . . 15 ⊢ ;16 ∈ ℂ
109	108	addid1i 10827	. . . . . . . . . . . . . 14 ⊢ (;16 + 0) = ;16
110		6cn 11729	. . . . . . . . . . . . . . 15 ⊢ 6 ∈ ℂ
111	110	addid2i 10828	. . . . . . . . . . . . . 14 ⊢ (0 + 6) = 6
112	99, 51, 51, 98, 106, 107, 109, 111	decadd 12153	. . . . . . . . . . . . 13 ⊢ (;;160 + 6) = ;;166
113		4cn 11723	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℂ
114	113	addid2i 10828	. . . . . . . . . . . . 13 ⊢ (0 + 4) = 4
115	103, 51, 98, 24, 104, 105, 112, 114	decadd 12153	. . . . . . . . . . . 12 ⊢ (;;;1600 + ;64) = ;;;1664
116		1t1e1 11800	. . . . . . . . . . . . 13 ⊢ (1 · 1) = 1
117	1	dp0u 30577	. . . . . . . . . . . . . 14 ⊢ (1.0) = 1
118	117, 117	oveq12i 7168	. . . . . . . . . . . . 13 ⊢ ((1.0) · (1.0)) = (1 · 1)
119	51	dp20u 30554	. . . . . . . . . . . . . . 15 ⊢ _00 = 0
120	119	oveq2i 7167	. . . . . . . . . . . . . 14 ⊢ (1._00) = (1.0)
121	120, 117	eqtri 2844	. . . . . . . . . . . . 13 ⊢ (1._00) = 1
122	116, 118, 121	3eqtr4i 2854	. . . . . . . . . . . 12 ⊢ ((1.0) · (1.0)) = (1._00)
123		8t8e64 12220	. . . . . . . . . . . . 13 ⊢ (8 · 8) = ;64
124	73	dp0u 30577	. . . . . . . . . . . . . 14 ⊢ (8.0) = 8
125	124, 124	oveq12i 7168	. . . . . . . . . . . . 13 ⊢ ((8.0) · (8.0)) = (8 · 8)
126	119	oveq2i 7167	. . . . . . . . . . . . . 14 ⊢ (;64._00) = (;64.0)
127	100	dp0u 30577	. . . . . . . . . . . . . 14 ⊢ (;64.0) = ;64
128	126, 127	eqtri 2844	. . . . . . . . . . . . 13 ⊢ (;64._00) = ;64
129	123, 125, 128	3eqtr4i 2854	. . . . . . . . . . . 12 ⊢ ((8.0) · (8.0)) = (;64._00)
130		10nn0 12117	. . . . . . . . . . . . . 14 ⊢ ;10 ∈ ℕ0
131	130, 51	deccl 12114	. . . . . . . . . . . . 13 ⊢ ;;100 ∈ ℕ0
132		eqid 2821	. . . . . . . . . . . . 13 ⊢ ;;;1001 = ;;;1001
133		eqid 2821	. . . . . . . . . . . . 13 ⊢ ;;166 = ;;166
134		eqid 2821	. . . . . . . . . . . . . 14 ⊢ ;;100 = ;;100
135		eqid 2821	. . . . . . . . . . . . . 14 ⊢ ;16 = ;16
136		dec10p 12142	. . . . . . . . . . . . . 14 ⊢ (;10 + 1) = ;11
137	130, 51, 1, 98, 134, 135, 136, 111	decadd 12153	. . . . . . . . . . . . 13 ⊢ (;;100 + ;16) = ;;116
138		ax-1cn 10595	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
139	138, 110	addcomi 10831	. . . . . . . . . . . . . 14 ⊢ (1 + 6) = (6 + 1)
140		6p1e7 11786	. . . . . . . . . . . . . 14 ⊢ (6 + 1) = 7
141	139, 140	eqtri 2844	. . . . . . . . . . . . 13 ⊢ (1 + 6) = 7
142	131, 1, 99, 98, 132, 133, 137, 141	decadd 12153	. . . . . . . . . . . 12 ⊢ (;;;1001 + ;;166) = ;;;1167
143		eqid 2821	. . . . . . . . . . . . . 14 ⊢ ;17 = ;17
144	141	oveq1i 7166	. . . . . . . . . . . . . . 15 ⊢ ((1 + 6) + 1) = (7 + 1)
145	144, 71	eqtri 2844	. . . . . . . . . . . . . 14 ⊢ ((1 + 6) + 1) = 8
146		7p4e11 12175	. . . . . . . . . . . . . 14 ⊢ (7 + 4) = ;11
147	1, 52, 98, 24, 143, 105, 145, 1, 146	decaddc 12154	. . . . . . . . . . . . 13 ⊢ (;17 + ;64) = ;81
148	119	oveq2i 7167	. . . . . . . . . . . . . . . . 17 ⊢ (;16._00) = (;16.0)
149	99	dp0u 30577	. . . . . . . . . . . . . . . . 17 ⊢ (;16.0) = ;16
150	148, 149	eqtri 2844	. . . . . . . . . . . . . . . 16 ⊢ (;16._00) = ;16
151	121, 150	oveq12i 7168	. . . . . . . . . . . . . . 15 ⊢ ((1._00) + (;16._00)) = (1 + ;16)
152	1	dec0h 12121	. . . . . . . . . . . . . . . 16 ⊢ 1 = ;01
153	138	addid2i 10828	. . . . . . . . . . . . . . . 16 ⊢ (0 + 1) = 1
154	51, 1, 1, 98, 152, 135, 153, 141	decadd 12153	. . . . . . . . . . . . . . 15 ⊢ (1 + ;16) = ;17
155	151, 154	eqtri 2844	. . . . . . . . . . . . . 14 ⊢ ((1._00) + (;16._00)) = ;17
156	155, 128	oveq12i 7168	. . . . . . . . . . . . 13 ⊢ (((1._00) + (;16._00)) + (;64._00)) = (;17 + ;64)
157	117, 124	oveq12i 7168	. . . . . . . . . . . . . . . 16 ⊢ ((1.0) + (8.0)) = (1 + 8)
158		8cn 11735	. . . . . . . . . . . . . . . . 17 ⊢ 8 ∈ ℂ
159	138, 158	addcomi 10831	. . . . . . . . . . . . . . . 16 ⊢ (1 + 8) = (8 + 1)
160		8p1e9 11788	. . . . . . . . . . . . . . . 16 ⊢ (8 + 1) = 9
161	157, 159, 160	3eqtri 2848	. . . . . . . . . . . . . . 15 ⊢ ((1.0) + (8.0)) = 9
162	161, 161	oveq12i 7168	. . . . . . . . . . . . . 14 ⊢ (((1.0) + (8.0)) · ((1.0) + (8.0))) = (9 · 9)
163		9t9e81 12228	. . . . . . . . . . . . . 14 ⊢ (9 · 9) = ;81
164	162, 163	eqtri 2844	. . . . . . . . . . . . 13 ⊢ (((1.0) + (8.0)) · ((1.0) + (8.0))) = ;81
165	147, 156, 164	3eqtr4ri 2855	. . . . . . . . . . . 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 30590	. . . . . . . . . . 11 ⊢ ((1._0_80) · (1._0_80)) < (1._1_67)
167	97, 166	eqbrtri 5087	. . . . . . . . . 10 ⊢ ((1._0_80)↑2) < (1._1_67)
168	92	resqcli 13550	. . . . . . . . . . 11 ⊢ ((1._0_80)↑2) ∈ ℝ
169	34, 3	pm3.2i 473	. . . . . . . . . . . . . . 15 ⊢ (6 ∈ ℝ ∧ 7 ∈ ℝ)
170		dp2cl 30556	. . . . . . . . . . . . . . 15 ⊢ ((6 ∈ ℝ ∧ 7 ∈ ℝ) → _67 ∈ ℝ)
171	169, 170	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ _67 ∈ ℝ
172	35, 171	pm3.2i 473	. . . . . . . . . . . . 13 ⊢ (1 ∈ ℝ ∧ _67 ∈ ℝ)
173		dp2cl 30556	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ ∧ _67 ∈ ℝ) → _1_67 ∈ ℝ)
174	172, 173	ax-mp 5	. . . . . . . . . . . 12 ⊢ _1_67 ∈ ℝ
175		dpcl 30567	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℕ0 ∧ _1_67 ∈ ℝ) → (1._1_67) ∈ ℝ)
176	1, 174, 175	mp2an 690	. . . . . . . . . . 11 ⊢ (1._1_67) ∈ ℝ
177	23, 168, 176	lttri 10766	. . . . . . . . . 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 690	. . . . . . . . 9 ⊢ ((1._0_7_9_9_55)↑2) < (1._1_67)
179	23, 176, 32, 47	ltmul1ii 11568	. . . . . . . . 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 232	. . . . . . . 8 ⊢ (((1._0_7_9_9_55)↑2) · (1._4_14)) < ((1._1_67) · (1._4_14))
181		2nn0 11915	. . . . . . . . 9 ⊢ 2 ∈ ℕ0
182		3nn0 11916	. . . . . . . . 9 ⊢ 3 ∈ ℕ0
183		1lt10 12238	. . . . . . . . 9 ⊢ 1 < ;10
184		3lt10 12236	. . . . . . . . 9 ⊢ 3 < ;10
185		8lt10 12231	. . . . . . . . 9 ⊢ 8 < ;10
186	130, 53	deccl 12114	. . . . . . . . . 10 ⊢ ;;109 ∈ ℕ0
187		eqid 2821	. . . . . . . . . 10 ⊢ ;;;1092 = ;;;1092
188	53	dec0h 12121	. . . . . . . . . 10 ⊢ 9 = ;09
189	186	nn0cni 11910	. . . . . . . . . . . 12 ⊢ ;;109 ∈ ℂ
190	189	addid1i 10827	. . . . . . . . . . 11 ⊢ (;;109 + 0) = ;;109
191		dec10p 12142	. . . . . . . . . . . 12 ⊢ (;10 + 0) = ;10
192	138	addid1i 10827	. . . . . . . . . . . 12 ⊢ (1 + 0) = 1
193	1, 51, 51, 1, 191, 152, 192, 153	decadd 12153	. . . . . . . . . . 11 ⊢ ((;10 + 0) + 1) = ;11
194		9p1e10 12101	. . . . . . . . . . 11 ⊢ (9 + 1) = ;10
195	130, 53, 51, 1, 190, 152, 193, 51, 194	decaddc 12154	. . . . . . . . . 10 ⊢ ((;;109 + 0) + 1) = ;;110
196		9cn 11738	. . . . . . . . . . . 12 ⊢ 9 ∈ ℂ
197		2cn 11713	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
198	196, 197	addcomi 10831	. . . . . . . . . . 11 ⊢ (9 + 2) = (2 + 9)
199		9p2e11 12186	. . . . . . . . . . 11 ⊢ (9 + 2) = ;11
200	198, 199	eqtr3i 2846	. . . . . . . . . 10 ⊢ (2 + 9) = ;11
201	186, 181, 51, 53, 187, 188, 195, 1, 200	decaddc 12154	. . . . . . . . 9 ⊢ (;;;1092 + 9) = ;;;1101
202	113, 138	mulcomi 10649	. . . . . . . . . . 11 ⊢ (4 · 1) = (1 · 4)
203	113	mulid1i 10645	. . . . . . . . . . 11 ⊢ (4 · 1) = 4
204	202, 203	eqtr3i 2846	. . . . . . . . . 10 ⊢ (1 · 4) = 4
205	24	dec0h 12121	. . . . . . . . . . 11 ⊢ 4 = ;04
206	203, 202, 205	3eqtr3i 2852	. . . . . . . . . 10 ⊢ (1 · 4) = ;04
207	138, 113	addcli 10647	. . . . . . . . . . . . 13 ⊢ (1 + 4) ∈ ℂ
208	207	addid1i 10827	. . . . . . . . . . . 12 ⊢ ((1 + 4) + 0) = (1 + 4)
209	113, 138	addcomi 10831	. . . . . . . . . . . 12 ⊢ (4 + 1) = (1 + 4)
210		4p1e5 11784	. . . . . . . . . . . 12 ⊢ (4 + 1) = 5
211	208, 209, 210	3eqtr2i 2850	. . . . . . . . . . 11 ⊢ ((1 + 4) + 0) = 5
212	54	dec0h 12121	. . . . . . . . . . 11 ⊢ 5 = ;05
213	211, 212	eqtri 2844	. . . . . . . . . 10 ⊢ ((1 + 4) + 0) = ;05
214	1, 1, 1, 24, 51, 51, 54, 24, 116, 204, 116, 206, 213, 192	dpmul 30589	. . . . . . . . 9 ⊢ ((1.1) · (1.4)) = (1._54)
215	110	mulid1i 10645	. . . . . . . . . 10 ⊢ (6 · 1) = 6
216		6t4e24 12205	. . . . . . . . . 10 ⊢ (6 · 4) = ;24
217		7cn 11732	. . . . . . . . . . 11 ⊢ 7 ∈ ℂ
218	217	mulid1i 10645	. . . . . . . . . 10 ⊢ (7 · 1) = 7
219		7t4e28 12210	. . . . . . . . . 10 ⊢ (7 · 4) = ;28
220	181, 24	deccl 12114	. . . . . . . . . . . . . . 15 ⊢ ;24 ∈ ℕ0
221	220	nn0cni 11910	. . . . . . . . . . . . . 14 ⊢ ;24 ∈ ℂ
222	221, 217	addcomi 10831	. . . . . . . . . . . . 13 ⊢ (;24 + 7) = (7 + ;24)
223		eqid 2821	. . . . . . . . . . . . . 14 ⊢ ;24 = ;24
224		2p1e3 11780	. . . . . . . . . . . . . 14 ⊢ (2 + 1) = 3
225	217, 113, 146	addcomli 10832	. . . . . . . . . . . . . 14 ⊢ (4 + 7) = ;11
226	181, 24, 52, 223, 224, 1, 225	decaddci 12160	. . . . . . . . . . . . 13 ⊢ (;24 + 7) = ;31
227	222, 226	eqtr3i 2846	. . . . . . . . . . . 12 ⊢ (7 + ;24) = ;31
228	227	oveq1i 7166	. . . . . . . . . . 11 ⊢ ((7 + ;24) + 2) = (;31 + 2)
229		eqid 2821	. . . . . . . . . . . 12 ⊢ ;31 = ;31
230	197, 138, 224	addcomli 10832	. . . . . . . . . . . 12 ⊢ (1 + 2) = 3
231	182, 1, 181, 229, 230	decaddi 12159	. . . . . . . . . . 11 ⊢ (;31 + 2) = ;33
232	228, 231	eqtri 2844	. . . . . . . . . 10 ⊢ ((7 + ;24) + 2) = ;33
233		6p3e9 11798	. . . . . . . . . 10 ⊢ (6 + 3) = 9
234	98, 52, 1, 24, 181, 182, 182, 73, 215, 216, 218, 219, 232, 233	dpmul 30589	. . . . . . . . 9 ⊢ ((6.7) · (1.4)) = (9._38)
235	1, 54	deccl 12114	. . . . . . . . . . 11 ⊢ ;15 ∈ ℕ0
236	235, 24	deccl 12114	. . . . . . . . . 10 ⊢ ;;154 ∈ ℕ0
237	51, 1	deccl 12114	. . . . . . . . . . 11 ⊢ ;01 ∈ ℕ0
238	237, 1	deccl 12114	. . . . . . . . . 10 ⊢ ;;011 ∈ ℕ0
239		eqid 2821	. . . . . . . . . 10 ⊢ ;;;1541 = ;;;1541
240	152	deceq1i 12106	. . . . . . . . . . 11 ⊢ ;11 = ;;011
241	240	deceq1i 12106	. . . . . . . . . 10 ⊢ ;;110 = ;;;0110
242		eqid 2821	. . . . . . . . . . 11 ⊢ ;;154 = ;;154
243		eqid 2821	. . . . . . . . . . 11 ⊢ ;;011 = ;;011
244	152	oveq2i 7167	. . . . . . . . . . . 12 ⊢ (;15 + 1) = (;15 + ;01)
245		eqid 2821	. . . . . . . . . . . . 13 ⊢ ;15 = ;15
246		5p1e6 11785	. . . . . . . . . . . . 13 ⊢ (5 + 1) = 6
247	1, 54, 1, 245, 246	decaddi 12159	. . . . . . . . . . . 12 ⊢ (;15 + 1) = ;16
248	244, 247	eqtr3i 2846	. . . . . . . . . . 11 ⊢ (;15 + ;01) = ;16
249	235, 24, 237, 1, 242, 243, 248, 210	decadd 12153	. . . . . . . . . 10 ⊢ (;;154 + ;;011) = ;;165
250	236, 1, 238, 51, 239, 241, 249, 192	decadd 12153	. . . . . . . . 9 ⊢ (;;;1541 + ;;110) = ;;;1651
251		7t2e14 12208	. . . . . . . . . . 11 ⊢ (7 · 2) = ;14
252		8t7e56 12219	. . . . . . . . . . . 12 ⊢ (8 · 7) = ;56
253	158, 217, 252	mulcomli 10650	. . . . . . . . . . 11 ⊢ (7 · 8) = ;56
254		8t2e16 12214	. . . . . . . . . . 11 ⊢ (8 · 2) = ;16
255		eqid 2821	. . . . . . . . . . . . . 14 ⊢ ;56 = ;56
256		5cn 11726	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℂ
257	256, 138, 246	addcomli 10832	. . . . . . . . . . . . . . . 16 ⊢ (1 + 5) = 6
258	257	oveq1i 7166	. . . . . . . . . . . . . . 15 ⊢ ((1 + 5) + 1) = (6 + 1)
259	258, 140	eqtri 2844	. . . . . . . . . . . . . 14 ⊢ ((1 + 5) + 1) = 7
260		6p6e12 12173	. . . . . . . . . . . . . 14 ⊢ (6 + 6) = ;12
261	1, 98, 54, 98, 135, 255, 259, 181, 260	decaddc 12154	. . . . . . . . . . . . 13 ⊢ (;16 + ;56) = ;72
262	261	oveq1i 7166	. . . . . . . . . . . 12 ⊢ ((;16 + ;56) + 6) = (;72 + 6)
263		eqid 2821	. . . . . . . . . . . . 13 ⊢ ;72 = ;72
264		6p2e8 11797	. . . . . . . . . . . . . 14 ⊢ (6 + 2) = 8
265	110, 197, 264	addcomli 10832	. . . . . . . . . . . . 13 ⊢ (2 + 6) = 8
266	52, 181, 98, 263, 265	decaddi 12159	. . . . . . . . . . . 12 ⊢ (;72 + 6) = ;78
267	262, 266	eqtri 2844	. . . . . . . . . . 11 ⊢ ((;16 + ;56) + 6) = ;78
268		eqid 2821	. . . . . . . . . . . 12 ⊢ ;14 = ;14
269		1p1e2 11763	. . . . . . . . . . . 12 ⊢ (1 + 1) = 2
270	1, 24, 52, 268, 269, 1, 225	decaddci 12160	. . . . . . . . . . 11 ⊢ (;14 + 7) = ;21
271	52, 73, 181, 73, 98, 52, 73, 24, 251, 253, 254, 123, 267, 270	dpmul 30589	. . . . . . . . . 10 ⊢ ((7.8) · (2.8)) = (;21._84)
272		eqid 2821	. . . . . . . . . . . . 13 ⊢ ;11 = ;11
273		eqid 2821	. . . . . . . . . . . . 13 ⊢ ;67 = ;67
274	217, 138, 71	addcomli 10832	. . . . . . . . . . . . 13 ⊢ (1 + 7) = 8
275	1, 1, 98, 52, 272, 273, 141, 274	decadd 12153	. . . . . . . . . . . 12 ⊢ (;11 + ;67) = ;78
276	1, 1, 98, 52, 52, 73, 275	dpadd 30587	. . . . . . . . . . 11 ⊢ ((1.1) + (6.7)) = (7.8)
277		4p4e8 11793	. . . . . . . . . . . . 13 ⊢ (4 + 4) = 8
278	1, 24, 1, 24, 268, 268, 269, 277	decadd 12153	. . . . . . . . . . . 12 ⊢ (;14 + ;14) = ;28
279	1, 24, 1, 24, 181, 73, 278	dpadd 30587	. . . . . . . . . . 11 ⊢ ((1.4) + (1.4)) = (2.8)
280	276, 279	oveq12i 7168	. . . . . . . . . 10 ⊢ (((1.1) + (6.7)) · ((1.4) + (1.4))) = ((7.8) · (2.8))
281	1, 181	deccl 12114	. . . . . . . . . . . . 13 ⊢ ;12 ∈ ℕ0
282		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ ;;109 = ;;109
283	130	nn0cni 11910	. . . . . . . . . . . . . . . . 17 ⊢ ;10 ∈ ℂ
284	283, 138, 136	addcomli 10832	. . . . . . . . . . . . . . . 16 ⊢ (1 + ;10) = ;11
285	1, 1, 269, 284	decsuc 12130	. . . . . . . . . . . . . . 15 ⊢ ((1 + ;10) + 1) = ;12
286		9p5e14 12189	. . . . . . . . . . . . . . . 16 ⊢ (9 + 5) = ;14
287	196, 256, 286	addcomli 10832	. . . . . . . . . . . . . . 15 ⊢ (5 + 9) = ;14
288	1, 54, 130, 53, 245, 282, 285, 24, 287	decaddc 12154	. . . . . . . . . . . . . 14 ⊢ (;15 + ;;109) = ;;124
289		4p2e6 11791	. . . . . . . . . . . . . 14 ⊢ (4 + 2) = 6
290	235, 24, 186, 181, 242, 187, 288, 289	decadd 12153	. . . . . . . . . . . . 13 ⊢ (;;154 + ;;;1092) = ;;;1246
291	1, 54, 24, 130, 53, 281, 181, 24, 98, 290	dpadd3 30588	. . . . . . . . . . . 12 ⊢ ((1._54) + (;10._92)) = (;12._46)
292	291	oveq1i 7166	. . . . . . . . . . 11 ⊢ (((1._54) + (;10._92)) + (9._38)) = ((;12._46) + (9._38))
293	181, 1	deccl 12114	. . . . . . . . . . . 12 ⊢ ;21 ∈ ℕ0
294	281, 24	deccl 12114	. . . . . . . . . . . . 13 ⊢ ;;124 ∈ ℕ0
295	53, 182	deccl 12114	. . . . . . . . . . . . 13 ⊢ ;93 ∈ ℕ0
296		eqid 2821	. . . . . . . . . . . . 13 ⊢ ;;;1246 = ;;;1246
297		eqid 2821	. . . . . . . . . . . . 13 ⊢ ;;938 = ;;938
298		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ ;;124 = ;;124
299		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ ;93 = ;93
300		eqid 2821	. . . . . . . . . . . . . . . 16 ⊢ ;12 = ;12
301	1, 181, 53, 300, 269, 1, 200	decaddci 12160	. . . . . . . . . . . . . . 15 ⊢ (;12 + 9) = ;21
302		4p3e7 11792	. . . . . . . . . . . . . . 15 ⊢ (4 + 3) = 7
303	281, 24, 53, 182, 298, 299, 301, 302	decadd 12153	. . . . . . . . . . . . . 14 ⊢ (;;124 + ;93) = ;;217
304	293, 52, 71, 303	decsuc 12130	. . . . . . . . . . . . 13 ⊢ ((;;124 + ;93) + 1) = ;;218
305		8p6e14 12183	. . . . . . . . . . . . . 14 ⊢ (8 + 6) = ;14
306	158, 110, 305	addcomli 10832	. . . . . . . . . . . . 13 ⊢ (6 + 8) = ;14
307	294, 98, 295, 73, 296, 297, 304, 24, 306	decaddc 12154	. . . . . . . . . . . 12 ⊢ (;;;1246 + ;;938) = ;;;2184
308	281, 24, 98, 53, 182, 293, 73, 73, 24, 307	dpadd3 30588	. . . . . . . . . . 11 ⊢ ((;12._46) + (9._38)) = (;21._84)
309	292, 308	eqtri 2844	. . . . . . . . . 10 ⊢ (((1._54) + (;10._92)) + (9._38)) = (;21._84)
310	271, 280, 309	3eqtr4i 2854	. . . . . . . . 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 30590	. . . . . . . 8 ⊢ ((1._1_67) · (1._4_14)) < (1._6_51)
312	176, 32	remulcli 10657	. . . . . . . . 9 ⊢ ((1._1_67) · (1._4_14)) ∈ ℝ
313	33, 312, 43	lttri 10766	. . . . . . . 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 690	. . . . . . 7 ⊢ (((1._0_7_9_9_55)↑2) · (1._4_14)) < (1._6_51)
315	50, 314	pm3.2i 473	. . . . . 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 473	. . . . 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 11722	. . . . . . . . . . 11 ⊢ 4 ∈ ℝ
318		2re 11712	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
319		3re 11718	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ ℝ
320	34, 319	pm3.2i 473	. . . . . . . . . . . . . 14 ⊢ (6 ∈ ℝ ∧ 3 ∈ ℝ)
321		dp2cl 30556	. . . . . . . . . . . . . 14 ⊢ ((6 ∈ ℝ ∧ 3 ∈ ℝ) → _63 ∈ ℝ)
322	320, 321	ax-mp 5	. . . . . . . . . . . . 13 ⊢ _63 ∈ ℝ
323	318, 322	pm3.2i 473	. . . . . . . . . . . 12 ⊢ (2 ∈ ℝ ∧ _63 ∈ ℝ)
324		dp2cl 30556	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ _63 ∈ ℝ) → _2_63 ∈ ℝ)
325	323, 324	ax-mp 5	. . . . . . . . . . 11 ⊢ _2_63 ∈ ℝ
326	317, 325	pm3.2i 473	. . . . . . . . . 10 ⊢ (4 ∈ ℝ ∧ _2_63 ∈ ℝ)
327		dp2cl 30556	. . . . . . . . . 10 ⊢ ((4 ∈ ℝ ∧ _2_63 ∈ ℝ) → _4_2_63 ∈ ℝ)
328	326, 327	ax-mp 5	. . . . . . . . 9 ⊢ _4_2_63 ∈ ℝ
329		dpcl 30567	. . . . . . . . 9 ⊢ ((1 ∈ ℕ0 ∧ _4_2_63 ∈ ℝ) → (1._4_2_63) ∈ ℝ)
330	1, 328, 329	mp2an 690	. . . . . . . 8 ⊢ (1._4_2_63) ∈ ℝ
331	84, 319	pm3.2i 473	. . . . . . . . . . . . . . . 16 ⊢ (8 ∈ ℝ ∧ 3 ∈ ℝ)
332		dp2cl 30556	. . . . . . . . . . . . . . . 16 ⊢ ((8 ∈ ℝ ∧ 3 ∈ ℝ) → _83 ∈ ℝ)
333	331, 332	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ _83 ∈ ℝ
334	84, 333	pm3.2i 473	. . . . . . . . . . . . . 14 ⊢ (8 ∈ ℝ ∧ _83 ∈ ℝ)
335		dp2cl 30556	. . . . . . . . . . . . . 14 ⊢ ((8 ∈ ℝ ∧ _83 ∈ ℝ) → _8_83 ∈ ℝ)
336	334, 335	ax-mp 5	. . . . . . . . . . . . 13 ⊢ _8_83 ∈ ℝ
337	319, 336	pm3.2i 473	. . . . . . . . . . . 12 ⊢ (3 ∈ ℝ ∧ _8_83 ∈ ℝ)
338		dp2cl 30556	. . . . . . . . . . . 12 ⊢ ((3 ∈ ℝ ∧ _8_83 ∈ ℝ) → _3_8_83 ∈ ℝ)
339	337, 338	ax-mp 5	. . . . . . . . . . 11 ⊢ _3_8_83 ∈ ℝ
340	2, 339	pm3.2i 473	. . . . . . . . . 10 ⊢ (0 ∈ ℝ ∧ _3_8_83 ∈ ℝ)
341		dp2cl 30556	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ _3_8_83 ∈ ℝ) → _0_3_8_83 ∈ ℝ)
342	340, 341	ax-mp 5	. . . . . . . . 9 ⊢ _0_3_8_83 ∈ ℝ
343		dpcl 30567	. . . . . . . . 9 ⊢ ((1 ∈ ℕ0 ∧ _0_3_8_83 ∈ ℝ) → (1._0_3_8_83) ∈ ℝ)
344	1, 342, 343	mp2an 690	. . . . . . . 8 ⊢ (1._0_3_8_83) ∈ ℝ
345	330, 344	remulcli 10657	. . . . . . 7 ⊢ ((1._4_2_63) · (1._0_3_8_83)) ∈ ℝ
346	317, 333	pm3.2i 473	. . . . . . . . 9 ⊢ (4 ∈ ℝ ∧ _83 ∈ ℝ)
347		dp2cl 30556	. . . . . . . . 9 ⊢ ((4 ∈ ℝ ∧ _83 ∈ ℝ) → _4_83 ∈ ℝ)
348	346, 347	ax-mp 5	. . . . . . . 8 ⊢ _4_83 ∈ ℝ
349		dpcl 30567	. . . . . . . 8 ⊢ ((1 ∈ ℕ0 ∧ _4_83 ∈ ℝ) → (1._4_83) ∈ ℝ)
350	1, 348, 349	mp2an 690	. . . . . . 7 ⊢ (1._4_83) ∈ ℝ
351	345, 350	pm3.2i 473	. . . . . 6 ⊢ (((1._4_2_63) · (1._0_3_8_83)) ∈ ℝ ∧ (1._4_83) ∈ ℝ)
352		3rp 12396	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℝ+
353	98, 352	rpdp2cl 30558	. . . . . . . . . . . 12 ⊢ _63 ∈ ℝ+
354	181, 353	rpdp2cl 30558	. . . . . . . . . . 11 ⊢ _2_63 ∈ ℝ+
355	24, 354	rpdp2cl 30558	. . . . . . . . . 10 ⊢ _4_2_63 ∈ ℝ+
356	1, 355	rpdpcl 30579	. . . . . . . . 9 ⊢ (1._4_2_63) ∈ ℝ+
357		rpge0 12403	. . . . . . . . 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 30558	. . . . . . . . . . . . 13 ⊢ _83 ∈ ℝ+
360	73, 359	rpdp2cl 30558	. . . . . . . . . . . 12 ⊢ _8_83 ∈ ℝ+
361	182, 360	rpdp2cl 30558	. . . . . . . . . . 11 ⊢ _3_8_83 ∈ ℝ+
362	51, 361	rpdp2cl 30558	. . . . . . . . . 10 ⊢ _0_3_8_83 ∈ ℝ+
363	1, 362	rpdpcl 30579	. . . . . . . . 9 ⊢ (1._0_3_8_83) ∈ ℝ+
364		rpge0 12403	. . . . . . . . 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 11187	. . . . . . . 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 690	. . . . . . 7 ⊢ 0 ≤ ((1._4_2_63) · (1._0_3_8_83))
368	318, 3	pm3.2i 473	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℝ ∧ 7 ∈ ℝ)
369		dp2cl 30556	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℝ ∧ 7 ∈ ℝ) → _27 ∈ ℝ)
370	368, 369	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ _27 ∈ ℝ
371	317, 370	pm3.2i 473	. . . . . . . . . . . . 13 ⊢ (4 ∈ ℝ ∧ _27 ∈ ℝ)
372		dp2cl 30556	. . . . . . . . . . . . 13 ⊢ ((4 ∈ ℝ ∧ _27 ∈ ℝ) → _4_27 ∈ ℝ)
373	371, 372	ax-mp 5	. . . . . . . . . . . 12 ⊢ _4_27 ∈ ℝ
374		dpcl 30567	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℕ0 ∧ _4_27 ∈ ℝ) → (1._4_27) ∈ ℝ)
375	1, 373, 374	mp2an 690	. . . . . . . . . . 11 ⊢ (1._4_27) ∈ ℝ
376	330, 375	pm3.2i 473	. . . . . . . . . 10 ⊢ ((1._4_2_63) ∈ ℝ ∧ (1._4_27) ∈ ℝ)
377		7nn 11730	. . . . . . . . . . . . . . 15 ⊢ 7 ∈ ℕ
378		nnrp 12401	. . . . . . . . . . . . . . 15 ⊢ (7 ∈ ℕ → 7 ∈ ℝ+)
379	377, 378	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 7 ∈ ℝ+
380	181, 379	rpdp2cl 30558	. . . . . . . . . . . . 13 ⊢ _27 ∈ ℝ+
381	24, 380	rpdp2cl 30558	. . . . . . . . . . . 12 ⊢ _4_27 ∈ ℝ+
382	98, 352, 184, 140	dp2ltsuc 30562	. . . . . . . . . . . . . 14 ⊢ _63 < 7
383	181, 353, 379, 382	dp2lt 30561	. . . . . . . . . . . . 13 ⊢ _2_63 < _27
384	24, 354, 380, 383	dp2lt 30561	. . . . . . . . . . . 12 ⊢ _4_2_63 < _4_27
385	1, 355, 381, 384	dplt 30580	. . . . . . . . . . 11 ⊢ (1._4_2_63) < (1._4_27)
386	358, 385	pm3.2i 473	. . . . . . . . . 10 ⊢ (0 ≤ (1._4_2_63) ∧ (1._4_2_63) < (1._4_27))
387	376, 386	pm3.2i 473	. . . . . . . . 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 473	. . . . . . . . . . . . . . 15 ⊢ (3 ∈ ℝ ∧ 9 ∈ ℝ)
389		dp2cl 30556	. . . . . . . . . . . . . . 15 ⊢ ((3 ∈ ℝ ∧ 9 ∈ ℝ) → _39 ∈ ℝ)
390	388, 389	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ _39 ∈ ℝ
391	2, 390	pm3.2i 473	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ ∧ _39 ∈ ℝ)
392		dp2cl 30556	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ _39 ∈ ℝ) → _0_39 ∈ ℝ)
393	391, 392	ax-mp 5	. . . . . . . . . . . 12 ⊢ _0_39 ∈ ℝ
394		dpcl 30567	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℕ0 ∧ _0_39 ∈ ℝ) → (1._0_39) ∈ ℝ)
395	1, 393, 394	mp2an 690	. . . . . . . . . . 11 ⊢ (1._0_39) ∈ ℝ
396	344, 395	pm3.2i 473	. . . . . . . . . 10 ⊢ ((1._0_3_8_83) ∈ ℝ ∧ (1._0_39) ∈ ℝ)
397		9nn 11736	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ ℕ
398		nnrp 12401	. . . . . . . . . . . . . . 15 ⊢ (9 ∈ ℕ → 9 ∈ ℝ+)
399	397, 398	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 9 ∈ ℝ+
400	182, 399	rpdp2cl 30558	. . . . . . . . . . . . 13 ⊢ _39 ∈ ℝ+
401	51, 400	rpdp2cl 30558	. . . . . . . . . . . 12 ⊢ _0_39 ∈ ℝ+
402	73, 352, 185, 184	dp2lt10 30560	. . . . . . . . . . . . . . 15 ⊢ _83 < ;10
403	73, 359, 402, 160	dp2ltsuc 30562	. . . . . . . . . . . . . 14 ⊢ _8_83 < 9
404	182, 360, 399, 403	dp2lt 30561	. . . . . . . . . . . . 13 ⊢ _3_8_83 < _39
405	51, 361, 400, 404	dp2lt 30561	. . . . . . . . . . . 12 ⊢ _0_3_8_83 < _0_39
406	1, 362, 401, 405	dplt 30580	. . . . . . . . . . 11 ⊢ (1._0_3_8_83) < (1._0_39)
407	365, 406	pm3.2i 473	. . . . . . . . . 10 ⊢ (0 ≤ (1._0_3_8_83) ∧ (1._0_3_8_83) < (1._0_39))
408	396, 407	pm3.2i 473	. . . . . . . . 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 11496	. . . . . . . . 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 690	. . . . . . . 8 ⊢ ((1._4_2_63) · (1._0_3_8_83)) < ((1._4_27) · (1._0_39))
411		6lt10 12233	. . . . . . . . 9 ⊢ 6 < ;10
412	73, 1	deccl 12114	. . . . . . . . . 10 ⊢ ;81 ∈ ℕ0
413		eqid 2821	. . . . . . . . . 10 ⊢ ;;816 = ;;816
414		eqid 2821	. . . . . . . . . 10 ⊢ ;10 = ;10
415		eqid 2821	. . . . . . . . . . . 12 ⊢ ;81 = ;81
416	73, 1, 269, 415	decsuc 12130	. . . . . . . . . . 11 ⊢ (;81 + 1) = ;82
417	73	dec0h 12121	. . . . . . . . . . . 12 ⊢ 8 = ;08
418	417	deceq1i 12106	. . . . . . . . . . 11 ⊢ ;82 = ;;082
419	416, 418	eqtri 2844	. . . . . . . . . 10 ⊢ (;81 + 1) = ;;082
420	110	addid1i 10827	. . . . . . . . . 10 ⊢ (6 + 0) = 6
421	412, 98, 1, 51, 413, 414, 419, 420	decadd 12153	. . . . . . . . 9 ⊢ (;;816 + ;10) = ;;;0826
422	138	mul01i 10830	. . . . . . . . . 10 ⊢ (1 · 0) = 0
423	113	mul01i 10830	. . . . . . . . . . 11 ⊢ (4 · 0) = 0
424	51	dec0h 12121	. . . . . . . . . . 11 ⊢ 0 = ;00
425	423, 424	eqtri 2844	. . . . . . . . . 10 ⊢ (4 · 0) = ;00
426	113	addid1i 10827	. . . . . . . . . . . 12 ⊢ (4 + 0) = 4
427	426	oveq1i 7166	. . . . . . . . . . 11 ⊢ ((4 + 0) + 0) = (4 + 0)
428	427, 426, 205	3eqtri 2848	. . . . . . . . . 10 ⊢ ((4 + 0) + 0) = ;04
429	1, 24, 1, 51, 51, 51, 24, 51, 116, 422, 203, 425, 428, 192	dpmul 30589	. . . . . . . . 9 ⊢ ((1.4) · (1.0)) = (1._40)
430		3cn 11719	. . . . . . . . . . 11 ⊢ 3 ∈ ℂ
431		3t2e6 11804	. . . . . . . . . . 11 ⊢ (3 · 2) = 6
432	430, 197, 431	mulcomli 10650	. . . . . . . . . 10 ⊢ (2 · 3) = 6
433		9t2e18 12221	. . . . . . . . . . 11 ⊢ (9 · 2) = ;18
434	196, 197, 433	mulcomli 10650	. . . . . . . . . 10 ⊢ (2 · 9) = ;18
435		7t3e21 12209	. . . . . . . . . 10 ⊢ (7 · 3) = ;21
436		9t7e63 12226	. . . . . . . . . . 11 ⊢ (9 · 7) = ;63
437	196, 217, 436	mulcomli 10650	. . . . . . . . . 10 ⊢ (7 · 9) = ;63
438		eqid 2821	. . . . . . . . . . . . 13 ⊢ ;21 = ;21
439		eqid 2821	. . . . . . . . . . . . 13 ⊢ ;18 = ;18
440	159, 160	eqtri 2844	. . . . . . . . . . . . 13 ⊢ (1 + 8) = 9
441	181, 1, 1, 73, 438, 439, 224, 440	decadd 12153	. . . . . . . . . . . 12 ⊢ (;21 + ;18) = ;39
442	441	oveq1i 7166	. . . . . . . . . . 11 ⊢ ((;21 + ;18) + 6) = (;39 + 6)
443		eqid 2821	. . . . . . . . . . . 12 ⊢ ;39 = ;39
444		3p1e4 11783	. . . . . . . . . . . 12 ⊢ (3 + 1) = 4
445		9p6e15 12190	. . . . . . . . . . . 12 ⊢ (9 + 6) = ;15
446	182, 53, 98, 443, 444, 54, 445	decaddci 12160	. . . . . . . . . . 11 ⊢ (;39 + 6) = ;45
447	442, 446	eqtri 2844	. . . . . . . . . 10 ⊢ ((;21 + ;18) + 6) = ;45
448		6p4e10 12171	. . . . . . . . . 10 ⊢ (6 + 4) = ;10
449	181, 52, 182, 53, 98, 24, 54, 182, 432, 434, 435, 437, 447, 448	dpmul 30589	. . . . . . . . 9 ⊢ ((2.7) · (3.9)) = (;10._53)
450	1, 24	deccl 12114	. . . . . . . . . . 11 ⊢ ;14 ∈ ℕ0
451	450, 51	deccl 12114	. . . . . . . . . 10 ⊢ ;;140 ∈ ℕ0
452	417, 73	eqeltrri 2910	. . . . . . . . . 10 ⊢ ;08 ∈ ℕ0
453		eqid 2821	. . . . . . . . . 10 ⊢ ;;;1401 = ;;;1401
454		eqid 2821	. . . . . . . . . 10 ⊢ ;;082 = ;;082
455		eqid 2821	. . . . . . . . . . 11 ⊢ ;;140 = ;;140
456	417, 158	eqeltrri 2910	. . . . . . . . . . . 12 ⊢ ;08 ∈ ℂ
457		0cn 10633	. . . . . . . . . . . 12 ⊢ 0 ∈ ℂ
458	417	oveq1i 7166	. . . . . . . . . . . . 13 ⊢ (8 + 0) = (;08 + 0)
459	158	addid1i 10827	. . . . . . . . . . . . 13 ⊢ (8 + 0) = 8
460	458, 459	eqtr3i 2846	. . . . . . . . . . . 12 ⊢ (;08 + 0) = 8
461	456, 457, 460	addcomli 10832	. . . . . . . . . . 11 ⊢ (0 + ;08) = 8
462	450, 51, 452, 455, 461	decaddi 12159	. . . . . . . . . 10 ⊢ (;;140 + ;08) = ;;148
463	451, 1, 452, 181, 453, 454, 462, 230	decadd 12153	. . . . . . . . 9 ⊢ (;;;1401 + ;;082) = ;;;1483
464		4t4e16 12198	. . . . . . . . . . 11 ⊢ (4 · 4) = ;16
465		9t4e36 12223	. . . . . . . . . . . 12 ⊢ (9 · 4) = ;36
466	196, 113, 465	mulcomli 10650	. . . . . . . . . . 11 ⊢ (4 · 9) = ;36
467	196	mulid1i 10645	. . . . . . . . . . . . 13 ⊢ (9 · 1) = 9
468	467, 188	eqtri 2844	. . . . . . . . . . . 12 ⊢ (9 · 1) = ;09
469	196, 138, 468	mulcomli 10650	. . . . . . . . . . 11 ⊢ (1 · 9) = ;09
470	182, 98	deccl 12114	. . . . . . . . . . . . . . 15 ⊢ ;36 ∈ ℕ0
471	470	nn0cni 11910	. . . . . . . . . . . . . 14 ⊢ ;36 ∈ ℂ
472		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ ;36 = ;36
473	182, 98, 24, 472, 444, 51, 448	decaddci 12160	. . . . . . . . . . . . . 14 ⊢ (;36 + 4) = ;40
474	471, 113, 473	addcomli 10832	. . . . . . . . . . . . 13 ⊢ (4 + ;36) = ;40
475	474	oveq1i 7166	. . . . . . . . . . . 12 ⊢ ((4 + ;36) + 0) = (;40 + 0)
476	24, 51	deccl 12114	. . . . . . . . . . . . . 14 ⊢ ;40 ∈ ℕ0
477	476	nn0cni 11910	. . . . . . . . . . . . 13 ⊢ ;40 ∈ ℂ
478	477	addid1i 10827	. . . . . . . . . . . 12 ⊢ (;40 + 0) = ;40
479	475, 478	eqtri 2844	. . . . . . . . . . 11 ⊢ ((4 + ;36) + 0) = ;40
480	1, 98, 24, 135, 269, 51, 448	decaddci 12160	. . . . . . . . . . 11 ⊢ (;16 + 4) = ;20
481	24, 1, 24, 53, 51, 24, 51, 53, 464, 466, 204, 469, 479, 480	dpmul 30589	. . . . . . . . . 10 ⊢ ((4.1) · (4.9)) = (;20._09)
482		eqid 2821	. . . . . . . . . . . . 13 ⊢ ;27 = ;27
483	230	oveq1i 7166	. . . . . . . . . . . . . 14 ⊢ ((1 + 2) + 1) = (3 + 1)
484	483, 444	eqtri 2844	. . . . . . . . . . . . 13 ⊢ ((1 + 2) + 1) = 4
485	1, 24, 181, 52, 268, 482, 484, 1, 225	decaddc 12154	. . . . . . . . . . . 12 ⊢ (;14 + ;27) = ;41
486	1, 24, 181, 52, 24, 1, 485	dpadd 30587	. . . . . . . . . . 11 ⊢ ((1.4) + (2.7)) = (4.1)
487	430, 138, 444	addcomli 10832	. . . . . . . . . . . . 13 ⊢ (1 + 3) = 4
488	196	addid2i 10828	. . . . . . . . . . . . 13 ⊢ (0 + 9) = 9
489	1, 51, 182, 53, 414, 443, 487, 488	decadd 12153	. . . . . . . . . . . 12 ⊢ (;10 + ;39) = ;49
490	1, 51, 182, 53, 24, 53, 489	dpadd 30587	. . . . . . . . . . 11 ⊢ ((1.0) + (3.9)) = (4.9)
491	486, 490	oveq12i 7168	. . . . . . . . . 10 ⊢ (((1.4) + (2.7)) · ((1.0) + (3.9))) = ((4.1) · (4.9))
492	1, 24, 73, 1, 268, 415, 440, 210	decadd 12153	. . . . . . . . . . . . . 14 ⊢ (;14 + ;81) = ;95
493	450, 51, 412, 98, 455, 413, 492, 111	decadd 12153	. . . . . . . . . . . . 13 ⊢ (;;140 + ;;816) = ;;956
494	1, 24, 51, 73, 1, 53, 98, 54, 98, 493	dpadd3 30588	. . . . . . . . . . . 12 ⊢ ((1._40) + (8._16)) = (9._56)
495	494	oveq1i 7166	. . . . . . . . . . 11 ⊢ (((1._40) + (8._16)) + (;10._53)) = ((9._56) + (;10._53))
496	181, 51	deccl 12114	. . . . . . . . . . . 12 ⊢ ;20 ∈ ℕ0
497	53, 54	deccl 12114	. . . . . . . . . . . . 13 ⊢ ;95 ∈ ℕ0
498	130, 54	deccl 12114	. . . . . . . . . . . . 13 ⊢ ;;105 ∈ ℕ0
499		eqid 2821	. . . . . . . . . . . . 13 ⊢ ;;956 = ;;956
500		eqid 2821	. . . . . . . . . . . . 13 ⊢ ;;;1053 = ;;;1053
501		eqid 2821	. . . . . . . . . . . . . 14 ⊢ ;95 = ;95
502		eqid 2821	. . . . . . . . . . . . . 14 ⊢ ;;105 = ;;105
503		dec10p 12142	. . . . . . . . . . . . . . . . 17 ⊢ (;10 + 9) = ;19
504	283, 196, 503	addcomli 10832	. . . . . . . . . . . . . . . 16 ⊢ (9 + ;10) = ;19
505	504	oveq1i 7166	. . . . . . . . . . . . . . 15 ⊢ ((9 + ;10) + 1) = (;19 + 1)
506		eqid 2821	. . . . . . . . . . . . . . . 16 ⊢ ;19 = ;19
507	1, 53, 1, 506, 269, 51, 194	decaddci 12160	. . . . . . . . . . . . . . 15 ⊢ (;19 + 1) = ;20
508	505, 507	eqtri 2844	. . . . . . . . . . . . . 14 ⊢ ((9 + ;10) + 1) = ;20
509		5p5e10 12170	. . . . . . . . . . . . . 14 ⊢ (5 + 5) = ;10
510	53, 54, 130, 54, 501, 502, 508, 51, 509	decaddc 12154	. . . . . . . . . . . . 13 ⊢ (;95 + ;;105) = ;;200
511	497, 98, 498, 182, 499, 500, 510, 233	decadd 12153	. . . . . . . . . . . 12 ⊢ (;;956 + ;;;1053) = ;;;2009
512	53, 54, 98, 130, 54, 496, 182, 51, 53, 511	dpadd3 30588	. . . . . . . . . . 11 ⊢ ((9._56) + (;10._53)) = (;20._09)
513	495, 512	eqtri 2844	. . . . . . . . . 10 ⊢ (((1._40) + (8._16)) + (;10._53)) = (;20._09)
514	481, 491, 513	3eqtr4i 2854	. . . . . . . . 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 30590	. . . . . . . 8 ⊢ ((1._4_27) · (1._0_39)) < (1._4_83)
516	375, 395	remulcli 10657	. . . . . . . . 9 ⊢ ((1._4_27) · (1._0_39)) ∈ ℝ
517	345, 516, 350	lttri 10766	. . . . . . . 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 690	. . . . . . 7 ⊢ ((1._4_2_63) · (1._0_3_8_83)) < (1._4_83)
519	367, 518	pm3.2i 473	. . . . . 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 473	. . . . 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 11496	. . . . 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 690	. . . 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 12114	. . . . 5 ⊢ ;42 ∈ ℕ0
524	496, 24	deccl 12114	. . . . . 6 ⊢ ;;204 ∈ ℕ0
525		eqid 2821	. . . . . 6 ⊢ ;;;2042 = ;;;2042
526		eqid 2821	. . . . . 6 ⊢ ;42 = ;42
527		eqid 2821	. . . . . . 7 ⊢ ;;204 = ;;204
528	496, 24, 24, 527, 277	decaddi 12159	. . . . . 6 ⊢ (;;204 + 4) = ;;208
529		2p2e4 11773	. . . . . 6 ⊢ (2 + 2) = 4
530	524, 181, 24, 181, 525, 526, 528, 529	decadd 12153	. . . . 5 ⊢ (;;;2042 + ;42) = ;;;2084
531	448	oveq1i 7166	. . . . . . 7 ⊢ ((6 + 4) + 2) = (;10 + 2)
532		dec10p 12142	. . . . . . 7 ⊢ (;10 + 2) = ;12
533	531, 532	eqtri 2844	. . . . . 6 ⊢ ((6 + 4) + 2) = ;12
534	1, 98, 1, 24, 181, 1, 181, 24, 116, 204, 215, 216, 533, 269	dpmul 30589	. . . . 5 ⊢ ((1.6) · (1.4)) = (2._24)
535		8t5e40 12217	. . . . . . 7 ⊢ (8 · 5) = ;40
536	158, 256, 535	mulcomli 10650	. . . . . 6 ⊢ (5 · 8) = ;40
537		5t3e15 12200	. . . . . 6 ⊢ (5 · 3) = ;15
538	158	mulid2i 10646	. . . . . 6 ⊢ (1 · 8) = 8
539	430	mulid2i 10646	. . . . . . 7 ⊢ (1 · 3) = 3
540	182	dec0h 12121	. . . . . . 7 ⊢ 3 = ;03
541	539, 540	eqtri 2844	. . . . . 6 ⊢ (1 · 3) = ;03
542	235	nn0cni 11910	. . . . . . . . 9 ⊢ ;15 ∈ ℂ
543		8p5e13 12182	. . . . . . . . . . 11 ⊢ (8 + 5) = ;13
544	158, 256, 543	addcomli 10832	. . . . . . . . . 10 ⊢ (5 + 8) = ;13
545	1, 54, 73, 245, 269, 182, 544	decaddci 12160	. . . . . . . . 9 ⊢ (;15 + 8) = ;23
546	542, 158, 545	addcomli 10832	. . . . . . . 8 ⊢ (8 + ;15) = ;23
547	546	oveq1i 7166	. . . . . . 7 ⊢ ((8 + ;15) + 0) = (;23 + 0)
548	181, 182	deccl 12114	. . . . . . . . 9 ⊢ ;23 ∈ ℕ0
549	548	nn0cni 11910	. . . . . . . 8 ⊢ ;23 ∈ ℂ
550	549	addid1i 10827	. . . . . . 7 ⊢ (;23 + 0) = ;23
551	547, 550	eqtri 2844	. . . . . 6 ⊢ ((8 + ;15) + 0) = ;23
552		eqid 2821	. . . . . . 7 ⊢ ;40 = ;40
553	197	addid2i 10828	. . . . . . 7 ⊢ (0 + 2) = 2
554	24, 51, 181, 552, 553	decaddi 12159	. . . . . 6 ⊢ (;40 + 2) = ;42
555	54, 1, 73, 182, 51, 181, 182, 182, 536, 537, 538, 541, 551, 554	dpmul 30589	. . . . 5 ⊢ ((5.1) · (8.3)) = (;42._33)
556	181, 181	deccl 12114	. . . . . . 7 ⊢ ;22 ∈ ℕ0
557	556, 24	deccl 12114	. . . . . 6 ⊢ ;;224 ∈ ℕ0
558		eqid 2821	. . . . . 6 ⊢ ;;;2241 = ;;;2241
559		eqid 2821	. . . . . 6 ⊢ ;;208 = ;;208
560		eqid 2821	. . . . . . 7 ⊢ ;;224 = ;;224
561		eqid 2821	. . . . . . 7 ⊢ ;20 = ;20
562		eqid 2821	. . . . . . . 8 ⊢ ;22 = ;22
563	181, 181, 181, 562, 529	decaddi 12159	. . . . . . 7 ⊢ (;22 + 2) = ;24
564	556, 24, 181, 51, 560, 561, 563, 426	decadd 12153	. . . . . 6 ⊢ (;;224 + ;20) = ;;244
565	557, 1, 496, 73, 558, 559, 564, 440	decadd 12153	. . . . 5 ⊢ (;;;2241 + ;;208) = ;;;2449
566	556, 98	deccl 12114	. . . . . . . 8 ⊢ ;;226 ∈ ℕ0
567	523, 182	deccl 12114	. . . . . . . 8 ⊢ ;;423 ∈ ℕ0
568		eqid 2821	. . . . . . . 8 ⊢ ;;;2266 = ;;;2266
569		eqid 2821	. . . . . . . 8 ⊢ ;;;4233 = ;;;4233
570		eqid 2821	. . . . . . . . 9 ⊢ ;;226 = ;;226
571		eqid 2821	. . . . . . . . 9 ⊢ ;;423 = ;;423
572	113, 197, 289	addcomli 10832	. . . . . . . . . 10 ⊢ (2 + 4) = 6
573	181, 181, 24, 181, 562, 526, 572, 529	decadd 12153	. . . . . . . . 9 ⊢ (;22 + ;42) = ;64
574	556, 98, 523, 182, 570, 571, 573, 233	decadd 12153	. . . . . . . 8 ⊢ (;;226 + ;;423) = ;;649
575	566, 98, 567, 182, 568, 569, 574, 233	decadd 12153	. . . . . . 7 ⊢ (;;;2266 + ;;;4233) = ;;;6499
576	556, 98, 98, 523, 182, 100, 182, 53, 53, 575	dpadd3 30588	. . . . . 6 ⊢ ((;22._66) + (;42._33)) = (;64._99)
577	496	nn0cni 11910	. . . . . . . . . . 11 ⊢ ;20 ∈ ℂ
578	181, 51, 181, 561, 553	decaddi 12159	. . . . . . . . . . 11 ⊢ (;20 + 2) = ;22
579	577, 197, 578	addcomli 10832	. . . . . . . . . 10 ⊢ (2 + ;20) = ;22
580	181, 181, 496, 24, 562, 527, 579, 572	decadd 12153	. . . . . . . . 9 ⊢ (;22 + ;;204) = ;;226
581	556, 24, 524, 181, 560, 525, 580, 289	decadd 12153	. . . . . . . 8 ⊢ (;;224 + ;;;2042) = ;;;2266
582	181, 181, 24, 496, 24, 556, 181, 98, 98, 581	dpadd3 30588	. . . . . . 7 ⊢ ((2._24) + (;20._42)) = (;22._66)
583	582	oveq1i 7166	. . . . . 6 ⊢ (((2._24) + (;20._42)) + (;42._33)) = ((;22._66) + (;42._33))
584		eqid 2821	. . . . . . . . . 10 ⊢ ;51 = ;51
585	1, 98, 54, 1, 135, 584, 257, 140	decadd 12153	. . . . . . . . 9 ⊢ (;16 + ;51) = ;67
586	1, 98, 54, 1, 98, 52, 585	dpadd 30587	. . . . . . . 8 ⊢ ((1.6) + (5.1)) = (6.7)
587		eqid 2821	. . . . . . . . . 10 ⊢ ;83 = ;83
588	1, 24, 73, 182, 268, 587, 440, 302	decadd 12153	. . . . . . . . 9 ⊢ (;14 + ;83) = ;97
589	1, 24, 73, 182, 53, 52, 588	dpadd 30587	. . . . . . . 8 ⊢ ((1.4) + (8.3)) = (9.7)
590	586, 589	oveq12i 7168	. . . . . . 7 ⊢ (((1.6) + (5.1)) · ((1.4) + (8.3))) = ((6.7) · (9.7))
591		9t6e54 12225	. . . . . . . . 9 ⊢ (9 · 6) = ;54
592	196, 110, 591	mulcomli 10650	. . . . . . . 8 ⊢ (6 · 9) = ;54
593		7t6e42 12212	. . . . . . . . 9 ⊢ (7 · 6) = ;42
594	217, 110, 593	mulcomli 10650	. . . . . . . 8 ⊢ (6 · 7) = ;42
595		7t7e49 12213	. . . . . . . 8 ⊢ (7 · 7) = ;49
596		eqid 2821	. . . . . . . . . . 11 ⊢ ;63 = ;63
597		3p2e5 11789	. . . . . . . . . . 11 ⊢ (3 + 2) = 5
598	98, 182, 24, 181, 596, 526, 448, 597	decadd 12153	. . . . . . . . . 10 ⊢ (;63 + ;42) = ;;105
599	598	oveq1i 7166	. . . . . . . . 9 ⊢ ((;63 + ;42) + 4) = (;;105 + 4)
600		5p4e9 11796	. . . . . . . . . 10 ⊢ (5 + 4) = 9
601	130, 54, 24, 502, 600	decaddi 12159	. . . . . . . . 9 ⊢ (;;105 + 4) = ;;109
602	599, 601	eqtri 2844	. . . . . . . 8 ⊢ ((;63 + ;42) + 4) = ;;109
603		eqid 2821	. . . . . . . . 9 ⊢ ;54 = ;54
604	54, 24, 1, 51, 603, 414, 246, 426	decadd 12153	. . . . . . . 8 ⊢ (;54 + ;10) = ;64
605	98, 52, 53, 52, 24, 130, 53, 53, 592, 594, 437, 595, 602, 604	dpmul 30589	. . . . . . 7 ⊢ ((6.7) · (9.7)) = (;64._99)
606	590, 605	eqtri 2844	. . . . . 6 ⊢ (((1.6) + (5.1)) · ((1.4) + (8.3))) = (;64._99)
607	576, 583, 606	3eqtr4ri 2855	. . . . 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 30590	. . . 4 ⊢ ((1._6_51) · (1._4_83)) < (2._4_49)
609	33, 345	remulcli 10657	. . . . 5 ⊢ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) ∈ ℝ
610	43, 350	remulcli 10657	. . . . 5 ⊢ ((1._6_51) · (1._4_83)) ∈ ℝ
611	24, 399	rpdp2cl 30558	. . . . . . . 8 ⊢ _49 ∈ ℝ+
612	24, 611	rpdp2cl 30558	. . . . . . 7 ⊢ _4_49 ∈ ℝ+
613	181, 612	rpdpcl 30579	. . . . . 6 ⊢ (2._4_49) ∈ ℝ+
614		rpre 12398	. . . . . 6 ⊢ ((2._4_49) ∈ ℝ+ → (2._4_49) ∈ ℝ)
615	613, 614	ax-mp 5	. . . . 5 ⊢ (2._4_49) ∈ ℝ
616	609, 610, 615	lttri 10766	. . . 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 690	. . 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 11743	. . . 4 ⊢ 0 < 3
619	609, 615, 319	ltmul2i 11561	. . . 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 232	. 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 30552	. . . . . . 7 ⊢ _0_00 = _00
623	622, 119	eqtri 2844	. . . . . 6 ⊢ _0_00 = 0
624	623	oveq2i 7167	. . . . 5 ⊢ (3._0_00) = (3.0)
625	182	dp0u 30577	. . . . 5 ⊢ (3.0) = 3
626	624, 625	eqtr2i 2845	. . . 4 ⊢ 3 = (3._0_00)
627	626	oveq1i 7166	. . 3 ⊢ (3 · (2._4_49)) = ((3._0_00) · (2._4_49))
628	450, 52	deccl 12114	. . . . . . 7 ⊢ ;;147 ∈ ℕ0
629	628, 51	deccl 12114	. . . . . 6 ⊢ ;;;1470 ∈ ℕ0
630	629	nn0cni 11910	. . . . 5 ⊢ ;;;1470 ∈ ℂ
631	630	addid1i 10827	. . . 4 ⊢ (;;;1470 + 0) = ;;;1470
632		4t3e12 12197	. . . . . 6 ⊢ (4 · 3) = ;12
633	113, 430, 632	mulcomli 10650	. . . . 5 ⊢ (3 · 4) = ;12
634	197	mul02i 10829	. . . . 5 ⊢ (0 · 2) = 0
635	113, 457, 425	mulcomli 10650	. . . . 5 ⊢ (0 · 4) = ;00
636	51, 51, 1, 181, 424, 300, 153, 553	decadd 12153	. . . . . . 7 ⊢ (0 + ;12) = ;12
637	636	oveq1i 7166	. . . . . 6 ⊢ ((0 + ;12) + 0) = (;12 + 0)
638	281	nn0cni 11910	. . . . . . 7 ⊢ ;12 ∈ ℂ
639	638	addid1i 10827	. . . . . 6 ⊢ (;12 + 0) = ;12
640	637, 639	eqtri 2844	. . . . 5 ⊢ ((0 + ;12) + 0) = ;12
641	182, 51, 181, 24, 51, 1, 181, 51, 431, 633, 634, 635, 640, 140	dpmul 30589	. . . 4 ⊢ ((3.0) · (2.4)) = (7._20)
642	51	dp0u 30577	. . . . . . 7 ⊢ (0.0) = 0
643	642	oveq1i 7166	. . . . . 6 ⊢ ((0.0) · (4.9)) = (0 · (4.9))
644		dpcl 30567	. . . . . . . . 9 ⊢ ((4 ∈ ℕ0 ∧ 9 ∈ ℝ) → (4.9) ∈ ℝ)
645	24, 4, 644	mp2an 690	. . . . . . . 8 ⊢ (4.9) ∈ ℝ
646	645	recni 10655	. . . . . . 7 ⊢ (4.9) ∈ ℂ
647	646	mul02i 10829	. . . . . 6 ⊢ (0 · (4.9)) = 0
648	643, 647	eqtri 2844	. . . . 5 ⊢ ((0.0) · (4.9)) = 0
649	119	oveq2i 7167	. . . . . 6 ⊢ (0._00) = (0.0)
650	649, 642	eqtri 2844	. . . . 5 ⊢ (0._00) = 0
651	648, 650	eqtr4i 2847	. . . 4 ⊢ ((0.0) · (4.9)) = (0._00)
652	52, 181	deccl 12114	. . . . . 6 ⊢ ;72 ∈ ℕ0
653	652, 51	deccl 12114	. . . . 5 ⊢ ;;720 ∈ ℕ0
654		eqid 2821	. . . . 5 ⊢ ;;;7201 = ;;;7201
655		eqid 2821	. . . . 5 ⊢ ;;147 = ;;147
656		eqid 2821	. . . . . 6 ⊢ ;;720 = ;;720
657	52, 181, 224, 263	decsuc 12130	. . . . . 6 ⊢ (;72 + 1) = ;73
658	652, 51, 1, 24, 656, 268, 657, 114	decadd 12153	. . . . 5 ⊢ (;;720 + ;14) = ;;734
659	653, 1, 450, 52, 654, 655, 658, 274	decadd 12153	. . . 4 ⊢ (;;;7201 + ;;147) = ;;;7348
660	642	oveq2i 7167	. . . . . . . 8 ⊢ ((3.0) + (0.0)) = ((3.0) + 0)
661	625, 430	eqeltri 2909	. . . . . . . . 9 ⊢ (3.0) ∈ ℂ
662	661	addid1i 10827	. . . . . . . 8 ⊢ ((3.0) + 0) = (3.0)
663	660, 662	eqtri 2844	. . . . . . 7 ⊢ ((3.0) + (0.0)) = (3.0)
664		eqid 2821	. . . . . . . . 9 ⊢ ;49 = ;49
665	572	oveq1i 7166	. . . . . . . . . 10 ⊢ ((2 + 4) + 1) = (6 + 1)
666	665, 140	eqtri 2844	. . . . . . . . 9 ⊢ ((2 + 4) + 1) = 7
667		9p4e13 12188	. . . . . . . . . 10 ⊢ (9 + 4) = ;13
668	196, 113, 667	addcomli 10832	. . . . . . . . 9 ⊢ (4 + 9) = ;13
669	181, 24, 24, 53, 223, 664, 666, 182, 668	decaddc 12154	. . . . . . . 8 ⊢ (;24 + ;49) = ;73
670	181, 24, 24, 53, 52, 182, 669	dpadd 30587	. . . . . . 7 ⊢ ((2.4) + (4.9)) = (7.3)
671	663, 670	oveq12i 7168	. . . . . 6 ⊢ (((3.0) + (0.0)) · ((2.4) + (4.9))) = ((3.0) · (7.3))
672	217, 430, 435	mulcomli 10650	. . . . . . 7 ⊢ (3 · 7) = ;21
673		3t3e9 11805	. . . . . . 7 ⊢ (3 · 3) = 9
674	217	mul01i 10830	. . . . . . . 8 ⊢ (7 · 0) = 0
675	217, 457, 674	mulcomli 10650	. . . . . . 7 ⊢ (0 · 7) = 0
676	430	mul01i 10830	. . . . . . . . 9 ⊢ (3 · 0) = 0
677	676, 424	eqtri 2844	. . . . . . . 8 ⊢ (3 · 0) = ;00
678	430, 457, 677	mulcomli 10650	. . . . . . 7 ⊢ (0 · 3) = ;00
679	196	addid1i 10827	. . . . . . . . . 10 ⊢ (9 + 0) = 9
680	679	oveq1i 7166	. . . . . . . . 9 ⊢ ((9 + 0) + 0) = (9 + 0)
681	680, 679, 188	3eqtri 2848	. . . . . . . 8 ⊢ ((9 + 0) + 0) = ;09
682	196, 457	addcomi 10831	. . . . . . . . . 10 ⊢ (9 + 0) = (0 + 9)
683	682	oveq1i 7166	. . . . . . . . 9 ⊢ ((9 + 0) + 0) = ((0 + 9) + 0)
684	683	eqeq1i 2826	. . . . . . . 8 ⊢ (((9 + 0) + 0) = ;09 ↔ ((0 + 9) + 0) = ;09)
685	681, 684	mpbi 232	. . . . . . 7 ⊢ ((0 + 9) + 0) = ;09
686	181, 1, 51, 438, 192	decaddi 12159	. . . . . . 7 ⊢ (;21 + 0) = ;21
687	182, 51, 52, 182, 51, 51, 53, 51, 672, 673, 675, 678, 685, 686	dpmul 30589	. . . . . 6 ⊢ ((3.0) · (7.3)) = (;21._90)
688	671, 687	eqtri 2844	. . . . 5 ⊢ (((3.0) + (0.0)) · ((2.4) + (4.9))) = (;21._90)
689	650	oveq2i 7167	. . . . . 6 ⊢ (((7._20) + (;14._70)) + (0._00)) = (((7._20) + (;14._70)) + 0)
690	318, 2	pm3.2i 473	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ ∧ 0 ∈ ℝ)
691		dp2cl 30556	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ 0 ∈ ℝ) → _20 ∈ ℝ)
692	690, 691	ax-mp 5	. . . . . . . . . 10 ⊢ _20 ∈ ℝ
693		dpcl 30567	. . . . . . . . . 10 ⊢ ((7 ∈ ℕ0 ∧ _20 ∈ ℝ) → (7._20) ∈ ℝ)
694	52, 692, 693	mp2an 690	. . . . . . . . 9 ⊢ (7._20) ∈ ℝ
695	694	recni 10655	. . . . . . . 8 ⊢ (7._20) ∈ ℂ
696	3, 2	pm3.2i 473	. . . . . . . . . . 11 ⊢ (7 ∈ ℝ ∧ 0 ∈ ℝ)
697		dp2cl 30556	. . . . . . . . . . 11 ⊢ ((7 ∈ ℝ ∧ 0 ∈ ℝ) → _70 ∈ ℝ)
698	696, 697	ax-mp 5	. . . . . . . . . 10 ⊢ _70 ∈ ℝ
699		dpcl 30567	. . . . . . . . . 10 ⊢ ((;14 ∈ ℕ0 ∧ _70 ∈ ℝ) → (;14._70) ∈ ℝ)
700	450, 698, 699	mp2an 690	. . . . . . . . 9 ⊢ (;14._70) ∈ ℝ
701	700	recni 10655	. . . . . . . 8 ⊢ (;14._70) ∈ ℂ
702	695, 701	addcli 10647	. . . . . . 7 ⊢ ((7._20) + (;14._70)) ∈ ℂ
703	702	addid1i 10827	. . . . . 6 ⊢ (((7._20) + (;14._70)) + 0) = ((7._20) + (;14._70))
704		eqid 2821	. . . . . . . 8 ⊢ ;;;1470 = ;;;1470
705	450	nn0cni 11910	. . . . . . . . . 10 ⊢ ;14 ∈ ℂ
706	705, 217, 270	addcomli 10832	. . . . . . . . 9 ⊢ (7 + ;14) = ;21
707		7p2e9 11799	. . . . . . . . . 10 ⊢ (7 + 2) = 9
708	217, 197, 707	addcomli 10832	. . . . . . . . 9 ⊢ (2 + 7) = 9
709	52, 181, 450, 52, 263, 655, 706, 708	decadd 12153	. . . . . . . 8 ⊢ (;72 + ;;147) = ;;219
710		00id 10815	. . . . . . . 8 ⊢ (0 + 0) = 0
711	652, 51, 628, 51, 656, 704, 709, 710	decadd 12153	. . . . . . 7 ⊢ (;;720 + ;;;1470) = ;;;2190
712	52, 181, 51, 450, 52, 293, 51, 53, 51, 711	dpadd3 30588	. . . . . 6 ⊢ ((7._20) + (;14._70)) = (;21._90)
713	689, 703, 712	3eqtri 2848	. . . . 5 ⊢ (((7._20) + (;14._70)) + (0._00)) = (;21._90)
714	688, 713	eqtr4i 2847	. . . 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 30590	. . 3 ⊢ ((3._0_00) · (2._4_49)) < (7._3_48)
716	627, 715	eqbrtri 5087	. 2 ⊢ (3 · (2._4_49)) < (7._3_48)
717	319, 609	remulcli 10657	. . 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 10657	. . 3 ⊢ (3 · (2._4_49)) ∈ ℝ
719		nnrp 12401	. . . . . . . 8 ⊢ (8 ∈ ℕ → 8 ∈ ℝ+)
720	63, 719	ax-mp 5	. . . . . . 7 ⊢ 8 ∈ ℝ+
721	24, 720	rpdp2cl 30558	. . . . . 6 ⊢ _48 ∈ ℝ+
722	182, 721	rpdp2cl 30558	. . . . 5 ⊢ _3_48 ∈ ℝ+
723	52, 722	rpdpcl 30579	. . . 4 ⊢ (7._3_48) ∈ ℝ+
724		rpre 12398	. . . 4 ⊢ ((7._3_48) ∈ ℝ+ → (7._3_48) ∈ ℝ)
725	723, 724	ax-mp 5	. . 3 ⊢ (7._3_48) ∈ ℝ
726	717, 718, 725	lttri 10766	. 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 690	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 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114   class class class wbr 5066  (class class class)co 7156  ℂcc 10535  ℝcr 10536  0cc0 10537  1c1 10538   + caddc 10540   · cmul 10542   < clt 10675   ≤ cle 10676  ℕcn 11638  2c2 11693  3c3 11694  4c4 11695  5c5 11696  6c6 11697  7c7 11698  8c8 11699  9c9 11700  ℕ₀cn0 11898  ;cdc 12099  ℝ⁺crp 12390  ↑cexp 13430  _cdp2 30547  .cdp 30564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-2nd 7690  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-div 11298  df-nn 11639  df-2 11701  df-3 11702  df-4 11703  df-5 11704  df-6 11705  df-7 11706  df-8 11707  df-9 11708  df-n0 11899  df-z 11983  df-dec 12100  df-uz 12245  df-rp 12391  df-seq 13371  df-exp 13431  df-dp2 30548  df-dp 30565

This theorem is referenced by:  hgt750leme  31929