Theorem hgt750lem2 32611

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 12232	. . . . . . . . . 10 ⊢ 1 ∈ ℕ0
2		0re 10961	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
3		7re 12049	. . . . . . . . . . . . . 14 ⊢ 7 ∈ ℝ
4		9re 12055	. . . . . . . . . . . . . . . 16 ⊢ 9 ∈ ℝ
5		5re 12043	. . . . . . . . . . . . . . . . . . . 20 ⊢ 5 ∈ ℝ
6	5, 5	pm3.2i 470	. . . . . . . . . . . . . . . . . . 19 ⊢ (5 ∈ ℝ ∧ 5 ∈ ℝ)
7		dp2cl 31133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((5 ∈ ℝ ∧ 5 ∈ ℝ) → _55 ∈ ℝ)
8	6, 7	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ _55 ∈ ℝ
9	4, 8	pm3.2i 470	. . . . . . . . . . . . . . . . 17 ⊢ (9 ∈ ℝ ∧ _55 ∈ ℝ)
10		dp2cl 31133	. . . . . . . . . . . . . . . . 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 31133	. . . . . . . . . . . . . . 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 31133	. . . . . . . . . . . . 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 31133	. . . . . . . . . . 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 31144	. . . . . . . . . 10 ⊢ ((1 ∈ ℕ0 ∧ _0_7_9_9_55 ∈ ℝ) → (1._0_7_9_9_55) ∈ ℝ)
22	1, 20, 21	mp2an 688	. . . . . . . . 9 ⊢ (1._0_7_9_9_55) ∈ ℝ
23	22	resqcli 13884	. . . . . . . 8 ⊢ ((1._0_7_9_9_55)↑2) ∈ ℝ
24		4nn0 12235	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ0
25		4nn 12039	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℕ
26		nnrp 12723	. . . . . . . . . . . . 13 ⊢ (4 ∈ ℕ → 4 ∈ ℝ+)
27	25, 26	ax-mp 5	. . . . . . . . . . . 12 ⊢ 4 ∈ ℝ+
28	1, 27	rpdp2cl 31135	. . . . . . . . . . 11 ⊢ _14 ∈ ℝ+
29	24, 28	rpdp2cl 31135	. . . . . . . . . 10 ⊢ _4_14 ∈ ℝ+
30	1, 29	rpdpcl 31156	. . . . . . . . 9 ⊢ (1._4_14) ∈ ℝ+
31		rpre 12720	. . . . . . . . 9 ⊢ ((1._4_14) ∈ ℝ+ → (1._4_14) ∈ ℝ)
32	30, 31	ax-mp 5	. . . . . . . 8 ⊢ (1._4_14) ∈ ℝ
33	23, 32	remulcli 10975	. . . . . . 7 ⊢ (((1._0_7_9_9_55)↑2) · (1._4_14)) ∈ ℝ
34		6re 12046	. . . . . . . . . 10 ⊢ 6 ∈ ℝ
35		1re 10959	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
36	5, 35	pm3.2i 470	. . . . . . . . . . 11 ⊢ (5 ∈ ℝ ∧ 1 ∈ ℝ)
37		dp2cl 31133	. . . . . . . . . . 11 ⊢ ((5 ∈ ℝ ∧ 1 ∈ ℝ) → _51 ∈ ℝ)
38	36, 37	ax-mp 5	. . . . . . . . . 10 ⊢ _51 ∈ ℝ
39	34, 38	pm3.2i 470	. . . . . . . . 9 ⊢ (6 ∈ ℝ ∧ _51 ∈ ℝ)
40		dp2cl 31133	. . . . . . . . 9 ⊢ ((6 ∈ ℝ ∧ _51 ∈ ℝ) → _6_51 ∈ ℝ)
41	39, 40	ax-mp 5	. . . . . . . 8 ⊢ _6_51 ∈ ℝ
42		dpcl 31144	. . . . . . . 8 ⊢ ((1 ∈ ℕ0 ∧ _6_51 ∈ ℝ) → (1._6_51) ∈ ℝ)
43	1, 41, 42	mp2an 688	. . . . . . 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 13886	. . . . . . . 8 ⊢ 0 ≤ ((1._0_7_9_9_55)↑2)
46		rpgt0 12724	. . . . . . . . . 10 ⊢ ((1._4_14) ∈ ℝ+ → 0 < (1._4_14))
47	30, 46	ax-mp 5	. . . . . . . . 9 ⊢ 0 < (1._4_14)
48	2, 32, 47	ltleii 11081	. . . . . . . 8 ⊢ 0 ≤ (1._4_14)
49	23, 32	mulge0i 11505	. . . . . . . 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 688	. . . . . . 7 ⊢ 0 ≤ (((1._0_7_9_9_55)↑2) · (1._4_14))
51		0nn0 12231	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
52		7nn0 12238	. . . . . . . . . . . . . 14 ⊢ 7 ∈ ℕ0
53		9nn0 12240	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ ℕ0
54		5nn0 12236	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℕ0
55		5nn 12042	. . . . . . . . . . . . . . . . . 18 ⊢ 5 ∈ ℕ
56		nnrp 12723	. . . . . . . . . . . . . . . . . 18 ⊢ (5 ∈ ℕ → 5 ∈ ℝ+)
57	55, 56	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℝ+
58	54, 57	rpdp2cl 31135	. . . . . . . . . . . . . . . 16 ⊢ _55 ∈ ℝ+
59	53, 58	rpdp2cl 31135	. . . . . . . . . . . . . . 15 ⊢ _9_55 ∈ ℝ+
60	53, 59	rpdp2cl 31135	. . . . . . . . . . . . . 14 ⊢ _9_9_55 ∈ ℝ+
61	52, 60	rpdp2cl 31135	. . . . . . . . . . . . 13 ⊢ _7_9_9_55 ∈ ℝ+
62	51, 61	rpdp2cl 31135	. . . . . . . . . . . 12 ⊢ _0_7_9_9_55 ∈ ℝ+
63		8nn 12051	. . . . . . . . . . . . . 14 ⊢ 8 ∈ ℕ
64	63	rpdp2cl2 31136	. . . . . . . . . . . . 13 ⊢ _80 ∈ ℝ+
65	51, 64	rpdp2cl 31135	. . . . . . . . . . . 12 ⊢ _0_80 ∈ ℝ+
66		9lt10 12550	. . . . . . . . . . . . . . . 16 ⊢ 9 < ;10
67		5lt10 12554	. . . . . . . . . . . . . . . . . 18 ⊢ 5 < ;10
68	54, 57, 67, 67	dp2lt10 31137	. . . . . . . . . . . . . . . . 17 ⊢ _55 < ;10
69	53, 58, 66, 68	dp2lt10 31137	. . . . . . . . . . . . . . . 16 ⊢ _9_55 < ;10
70	53, 59, 66, 69	dp2lt10 31137	. . . . . . . . . . . . . . 15 ⊢ _9_9_55 < ;10
71		7p1e8 12105	. . . . . . . . . . . . . . 15 ⊢ (7 + 1) = 8
72	52, 60, 70, 71	dp2ltsuc 31139	. . . . . . . . . . . . . 14 ⊢ _7_9_9_55 < 8
73		8nn0 12239	. . . . . . . . . . . . . . 15 ⊢ 8 ∈ ℕ0
74	73	dp20u 31131	. . . . . . . . . . . . . 14 ⊢ _80 = 8
75	72, 74	breqtrri 5105	. . . . . . . . . . . . 13 ⊢ _7_9_9_55 < _80
76	51, 61, 64, 75	dp2lt 31138	. . . . . . . . . . . 12 ⊢ _0_7_9_9_55 < _0_80
77	1, 62, 65, 76	dplt 31157	. . . . . . . . . . 11 ⊢ (1._0_7_9_9_55) < (1._0_80)
78	1, 62	rpdpcl 31156	. . . . . . . . . . . . 13 ⊢ (1._0_7_9_9_55) ∈ ℝ+
79		rpge0 12725	. . . . . . . . . . . . 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 31156	. . . . . . . . . . . . 13 ⊢ (1._0_80) ∈ ℝ+
82		rpge0 12725	. . . . . . . . . . . . 13 ⊢ ((1._0_80) ∈ ℝ+ → 0 ≤ (1._0_80))
83	81, 82	ax-mp 5	. . . . . . . . . . . 12 ⊢ 0 ≤ (1._0_80)
84		8re 12052	. . . . . . . . . . . . . . . . . 18 ⊢ 8 ∈ ℝ
85	84, 2	pm3.2i 470	. . . . . . . . . . . . . . . . 17 ⊢ (8 ∈ ℝ ∧ 0 ∈ ℝ)
86		dp2cl 31133	. . . . . . . . . . . . . . . . 17 ⊢ ((8 ∈ ℝ ∧ 0 ∈ ℝ) → _80 ∈ ℝ)
87	85, 86	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ _80 ∈ ℝ
88	2, 87	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ (0 ∈ ℝ ∧ _80 ∈ ℝ)
89		dp2cl 31133	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ ∧ _80 ∈ ℝ) → _0_80 ∈ ℝ)
90	88, 89	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ _0_80 ∈ ℝ
91		dpcl 31144	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℕ0 ∧ _0_80 ∈ ℝ) → (1._0_80) ∈ ℝ)
92	1, 90, 91	mp2an 688	. . . . . . . . . . . . 13 ⊢ (1._0_80) ∈ ℝ
93	22, 92	lt2sqi 13887	. . . . . . . . . . . 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 688	. . . . . . . . . . 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 229	. . . . . . . . . 10 ⊢ ((1._0_7_9_9_55)↑2) < ((1._0_80)↑2)
96	92	recni 10973	. . . . . . . . . . . 12 ⊢ (1._0_80) ∈ ℂ
97	96	sqvali 13878	. . . . . . . . . . 11 ⊢ ((1._0_80)↑2) = ((1._0_80) · (1._0_80))
98		6nn0 12237	. . . . . . . . . . . . 13 ⊢ 6 ∈ ℕ0
99	1, 98	deccl 12434	. . . . . . . . . . . 12 ⊢ ;16 ∈ ℕ0
100	98, 24	deccl 12434	. . . . . . . . . . . 12 ⊢ ;64 ∈ ℕ0
101		4lt10 12555	. . . . . . . . . . . 12 ⊢ 4 < ;10
102		10pos 12436	. . . . . . . . . . . 12 ⊢ 0 < ;10
103	99, 51	deccl 12434	. . . . . . . . . . . . 13 ⊢ ;;160 ∈ ℕ0
104		eqid 2739	. . . . . . . . . . . . 13 ⊢ ;;;1600 = ;;;1600
105		eqid 2739	. . . . . . . . . . . . 13 ⊢ ;64 = ;64
106		eqid 2739	. . . . . . . . . . . . . 14 ⊢ ;;160 = ;;160
107	98	dec0h 12441	. . . . . . . . . . . . . 14 ⊢ 6 = ;06
108	99	nn0cni 12228	. . . . . . . . . . . . . . 15 ⊢ ;16 ∈ ℂ
109	108	addid1i 11145	. . . . . . . . . . . . . 14 ⊢ (;16 + 0) = ;16
110		6cn 12047	. . . . . . . . . . . . . . 15 ⊢ 6 ∈ ℂ
111	110	addid2i 11146	. . . . . . . . . . . . . 14 ⊢ (0 + 6) = 6
112	99, 51, 51, 98, 106, 107, 109, 111	decadd 12473	. . . . . . . . . . . . 13 ⊢ (;;160 + 6) = ;;166
113		4cn 12041	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℂ
114	113	addid2i 11146	. . . . . . . . . . . . 13 ⊢ (0 + 4) = 4
115	103, 51, 98, 24, 104, 105, 112, 114	decadd 12473	. . . . . . . . . . . 12 ⊢ (;;;1600 + ;64) = ;;;1664
116		1t1e1 12118	. . . . . . . . . . . . 13 ⊢ (1 · 1) = 1
117	1	dp0u 31154	. . . . . . . . . . . . . 14 ⊢ (1.0) = 1
118	117, 117	oveq12i 7280	. . . . . . . . . . . . 13 ⊢ ((1.0) · (1.0)) = (1 · 1)
119	51	dp20u 31131	. . . . . . . . . . . . . . 15 ⊢ _00 = 0
120	119	oveq2i 7279	. . . . . . . . . . . . . 14 ⊢ (1._00) = (1.0)
121	120, 117	eqtri 2767	. . . . . . . . . . . . 13 ⊢ (1._00) = 1
122	116, 118, 121	3eqtr4i 2777	. . . . . . . . . . . 12 ⊢ ((1.0) · (1.0)) = (1._00)
123		8t8e64 12540	. . . . . . . . . . . . 13 ⊢ (8 · 8) = ;64
124	73	dp0u 31154	. . . . . . . . . . . . . 14 ⊢ (8.0) = 8
125	124, 124	oveq12i 7280	. . . . . . . . . . . . 13 ⊢ ((8.0) · (8.0)) = (8 · 8)
126	119	oveq2i 7279	. . . . . . . . . . . . . 14 ⊢ (;64._00) = (;64.0)
127	100	dp0u 31154	. . . . . . . . . . . . . 14 ⊢ (;64.0) = ;64
128	126, 127	eqtri 2767	. . . . . . . . . . . . 13 ⊢ (;64._00) = ;64
129	123, 125, 128	3eqtr4i 2777	. . . . . . . . . . . 12 ⊢ ((8.0) · (8.0)) = (;64._00)
130		10nn0 12437	. . . . . . . . . . . . . 14 ⊢ ;10 ∈ ℕ0
131	130, 51	deccl 12434	. . . . . . . . . . . . 13 ⊢ ;;100 ∈ ℕ0
132		eqid 2739	. . . . . . . . . . . . 13 ⊢ ;;;1001 = ;;;1001
133		eqid 2739	. . . . . . . . . . . . 13 ⊢ ;;166 = ;;166
134		eqid 2739	. . . . . . . . . . . . . 14 ⊢ ;;100 = ;;100
135		eqid 2739	. . . . . . . . . . . . . 14 ⊢ ;16 = ;16
136		dec10p 12462	. . . . . . . . . . . . . 14 ⊢ (;10 + 1) = ;11
137	130, 51, 1, 98, 134, 135, 136, 111	decadd 12473	. . . . . . . . . . . . 13 ⊢ (;;100 + ;16) = ;;116
138		ax-1cn 10913	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
139	138, 110	addcomi 11149	. . . . . . . . . . . . . 14 ⊢ (1 + 6) = (6 + 1)
140		6p1e7 12104	. . . . . . . . . . . . . 14 ⊢ (6 + 1) = 7
141	139, 140	eqtri 2767	. . . . . . . . . . . . 13 ⊢ (1 + 6) = 7
142	131, 1, 99, 98, 132, 133, 137, 141	decadd 12473	. . . . . . . . . . . 12 ⊢ (;;;1001 + ;;166) = ;;;1167
143		eqid 2739	. . . . . . . . . . . . . 14 ⊢ ;17 = ;17
144	141	oveq1i 7278	. . . . . . . . . . . . . . 15 ⊢ ((1 + 6) + 1) = (7 + 1)
145	144, 71	eqtri 2767	. . . . . . . . . . . . . 14 ⊢ ((1 + 6) + 1) = 8
146		7p4e11 12495	. . . . . . . . . . . . . 14 ⊢ (7 + 4) = ;11
147	1, 52, 98, 24, 143, 105, 145, 1, 146	decaddc 12474	. . . . . . . . . . . . 13 ⊢ (;17 + ;64) = ;81
148	119	oveq2i 7279	. . . . . . . . . . . . . . . . 17 ⊢ (;16._00) = (;16.0)
149	99	dp0u 31154	. . . . . . . . . . . . . . . . 17 ⊢ (;16.0) = ;16
150	148, 149	eqtri 2767	. . . . . . . . . . . . . . . 16 ⊢ (;16._00) = ;16
151	121, 150	oveq12i 7280	. . . . . . . . . . . . . . 15 ⊢ ((1._00) + (;16._00)) = (1 + ;16)
152	1	dec0h 12441	. . . . . . . . . . . . . . . 16 ⊢ 1 = ;01
153	138	addid2i 11146	. . . . . . . . . . . . . . . 16 ⊢ (0 + 1) = 1
154	51, 1, 1, 98, 152, 135, 153, 141	decadd 12473	. . . . . . . . . . . . . . 15 ⊢ (1 + ;16) = ;17
155	151, 154	eqtri 2767	. . . . . . . . . . . . . 14 ⊢ ((1._00) + (;16._00)) = ;17
156	155, 128	oveq12i 7280	. . . . . . . . . . . . 13 ⊢ (((1._00) + (;16._00)) + (;64._00)) = (;17 + ;64)
157	117, 124	oveq12i 7280	. . . . . . . . . . . . . . . 16 ⊢ ((1.0) + (8.0)) = (1 + 8)
158		8cn 12053	. . . . . . . . . . . . . . . . 17 ⊢ 8 ∈ ℂ
159	138, 158	addcomi 11149	. . . . . . . . . . . . . . . 16 ⊢ (1 + 8) = (8 + 1)
160		8p1e9 12106	. . . . . . . . . . . . . . . 16 ⊢ (8 + 1) = 9
161	157, 159, 160	3eqtri 2771	. . . . . . . . . . . . . . 15 ⊢ ((1.0) + (8.0)) = 9
162	161, 161	oveq12i 7280	. . . . . . . . . . . . . 14 ⊢ (((1.0) + (8.0)) · ((1.0) + (8.0))) = (9 · 9)
163		9t9e81 12548	. . . . . . . . . . . . . 14 ⊢ (9 · 9) = ;81
164	162, 163	eqtri 2767	. . . . . . . . . . . . 13 ⊢ (((1.0) + (8.0)) · ((1.0) + (8.0))) = ;81
165	147, 156, 164	3eqtr4ri 2778	. . . . . . . . . . . 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 31167	. . . . . . . . . . 11 ⊢ ((1._0_80) · (1._0_80)) < (1._1_67)
167	97, 166	eqbrtri 5099	. . . . . . . . . 10 ⊢ ((1._0_80)↑2) < (1._1_67)
168	92	resqcli 13884	. . . . . . . . . . 11 ⊢ ((1._0_80)↑2) ∈ ℝ
169	34, 3	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ (6 ∈ ℝ ∧ 7 ∈ ℝ)
170		dp2cl 31133	. . . . . . . . . . . . . . 15 ⊢ ((6 ∈ ℝ ∧ 7 ∈ ℝ) → _67 ∈ ℝ)
171	169, 170	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ _67 ∈ ℝ
172	35, 171	pm3.2i 470	. . . . . . . . . . . . 13 ⊢ (1 ∈ ℝ ∧ _67 ∈ ℝ)
173		dp2cl 31133	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ ∧ _67 ∈ ℝ) → _1_67 ∈ ℝ)
174	172, 173	ax-mp 5	. . . . . . . . . . . 12 ⊢ _1_67 ∈ ℝ
175		dpcl 31144	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℕ0 ∧ _1_67 ∈ ℝ) → (1._1_67) ∈ ℝ)
176	1, 174, 175	mp2an 688	. . . . . . . . . . 11 ⊢ (1._1_67) ∈ ℝ
177	23, 168, 176	lttri 11084	. . . . . . . . . 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 688	. . . . . . . . 9 ⊢ ((1._0_7_9_9_55)↑2) < (1._1_67)
179	23, 176, 32, 47	ltmul1ii 11886	. . . . . . . . 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 229	. . . . . . . 8 ⊢ (((1._0_7_9_9_55)↑2) · (1._4_14)) < ((1._1_67) · (1._4_14))
181		2nn0 12233	. . . . . . . . 9 ⊢ 2 ∈ ℕ0
182		3nn0 12234	. . . . . . . . 9 ⊢ 3 ∈ ℕ0
183		1lt10 12558	. . . . . . . . 9 ⊢ 1 < ;10
184		3lt10 12556	. . . . . . . . 9 ⊢ 3 < ;10
185		8lt10 12551	. . . . . . . . 9 ⊢ 8 < ;10
186	130, 53	deccl 12434	. . . . . . . . . 10 ⊢ ;;109 ∈ ℕ0
187		eqid 2739	. . . . . . . . . 10 ⊢ ;;;1092 = ;;;1092
188	53	dec0h 12441	. . . . . . . . . 10 ⊢ 9 = ;09
189	186	nn0cni 12228	. . . . . . . . . . . 12 ⊢ ;;109 ∈ ℂ
190	189	addid1i 11145	. . . . . . . . . . 11 ⊢ (;;109 + 0) = ;;109
191		dec10p 12462	. . . . . . . . . . . 12 ⊢ (;10 + 0) = ;10
192	138	addid1i 11145	. . . . . . . . . . . 12 ⊢ (1 + 0) = 1
193	1, 51, 51, 1, 191, 152, 192, 153	decadd 12473	. . . . . . . . . . 11 ⊢ ((;10 + 0) + 1) = ;11
194		9p1e10 12421	. . . . . . . . . . 11 ⊢ (9 + 1) = ;10
195	130, 53, 51, 1, 190, 152, 193, 51, 194	decaddc 12474	. . . . . . . . . 10 ⊢ ((;;109 + 0) + 1) = ;;110
196		9cn 12056	. . . . . . . . . . . 12 ⊢ 9 ∈ ℂ
197		2cn 12031	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
198	196, 197	addcomi 11149	. . . . . . . . . . 11 ⊢ (9 + 2) = (2 + 9)
199		9p2e11 12506	. . . . . . . . . . 11 ⊢ (9 + 2) = ;11
200	198, 199	eqtr3i 2769	. . . . . . . . . 10 ⊢ (2 + 9) = ;11
201	186, 181, 51, 53, 187, 188, 195, 1, 200	decaddc 12474	. . . . . . . . 9 ⊢ (;;;1092 + 9) = ;;;1101
202	113, 138	mulcomi 10967	. . . . . . . . . . 11 ⊢ (4 · 1) = (1 · 4)
203	113	mulid1i 10963	. . . . . . . . . . 11 ⊢ (4 · 1) = 4
204	202, 203	eqtr3i 2769	. . . . . . . . . 10 ⊢ (1 · 4) = 4
205	24	dec0h 12441	. . . . . . . . . . 11 ⊢ 4 = ;04
206	203, 202, 205	3eqtr3i 2775	. . . . . . . . . 10 ⊢ (1 · 4) = ;04
207	138, 113	addcli 10965	. . . . . . . . . . . . 13 ⊢ (1 + 4) ∈ ℂ
208	207	addid1i 11145	. . . . . . . . . . . 12 ⊢ ((1 + 4) + 0) = (1 + 4)
209	113, 138	addcomi 11149	. . . . . . . . . . . 12 ⊢ (4 + 1) = (1 + 4)
210		4p1e5 12102	. . . . . . . . . . . 12 ⊢ (4 + 1) = 5
211	208, 209, 210	3eqtr2i 2773	. . . . . . . . . . 11 ⊢ ((1 + 4) + 0) = 5
212	54	dec0h 12441	. . . . . . . . . . 11 ⊢ 5 = ;05
213	211, 212	eqtri 2767	. . . . . . . . . 10 ⊢ ((1 + 4) + 0) = ;05
214	1, 1, 1, 24, 51, 51, 54, 24, 116, 204, 116, 206, 213, 192	dpmul 31166	. . . . . . . . 9 ⊢ ((1.1) · (1.4)) = (1._54)
215	110	mulid1i 10963	. . . . . . . . . 10 ⊢ (6 · 1) = 6
216		6t4e24 12525	. . . . . . . . . 10 ⊢ (6 · 4) = ;24
217		7cn 12050	. . . . . . . . . . 11 ⊢ 7 ∈ ℂ
218	217	mulid1i 10963	. . . . . . . . . 10 ⊢ (7 · 1) = 7
219		7t4e28 12530	. . . . . . . . . 10 ⊢ (7 · 4) = ;28
220	181, 24	deccl 12434	. . . . . . . . . . . . . . 15 ⊢ ;24 ∈ ℕ0
221	220	nn0cni 12228	. . . . . . . . . . . . . 14 ⊢ ;24 ∈ ℂ
222	221, 217	addcomi 11149	. . . . . . . . . . . . 13 ⊢ (;24 + 7) = (7 + ;24)
223		eqid 2739	. . . . . . . . . . . . . 14 ⊢ ;24 = ;24
224		2p1e3 12098	. . . . . . . . . . . . . 14 ⊢ (2 + 1) = 3
225	217, 113, 146	addcomli 11150	. . . . . . . . . . . . . 14 ⊢ (4 + 7) = ;11
226	181, 24, 52, 223, 224, 1, 225	decaddci 12480	. . . . . . . . . . . . 13 ⊢ (;24 + 7) = ;31
227	222, 226	eqtr3i 2769	. . . . . . . . . . . 12 ⊢ (7 + ;24) = ;31
228	227	oveq1i 7278	. . . . . . . . . . 11 ⊢ ((7 + ;24) + 2) = (;31 + 2)
229		eqid 2739	. . . . . . . . . . . 12 ⊢ ;31 = ;31
230	197, 138, 224	addcomli 11150	. . . . . . . . . . . 12 ⊢ (1 + 2) = 3
231	182, 1, 181, 229, 230	decaddi 12479	. . . . . . . . . . 11 ⊢ (;31 + 2) = ;33
232	228, 231	eqtri 2767	. . . . . . . . . 10 ⊢ ((7 + ;24) + 2) = ;33
233		6p3e9 12116	. . . . . . . . . 10 ⊢ (6 + 3) = 9
234	98, 52, 1, 24, 181, 182, 182, 73, 215, 216, 218, 219, 232, 233	dpmul 31166	. . . . . . . . 9 ⊢ ((6.7) · (1.4)) = (9._38)
235	1, 54	deccl 12434	. . . . . . . . . . 11 ⊢ ;15 ∈ ℕ0
236	235, 24	deccl 12434	. . . . . . . . . 10 ⊢ ;;154 ∈ ℕ0
237	51, 1	deccl 12434	. . . . . . . . . . 11 ⊢ ;01 ∈ ℕ0
238	237, 1	deccl 12434	. . . . . . . . . 10 ⊢ ;;011 ∈ ℕ0
239		eqid 2739	. . . . . . . . . 10 ⊢ ;;;1541 = ;;;1541
240	152	deceq1i 12426	. . . . . . . . . . 11 ⊢ ;11 = ;;011
241	240	deceq1i 12426	. . . . . . . . . 10 ⊢ ;;110 = ;;;0110
242		eqid 2739	. . . . . . . . . . 11 ⊢ ;;154 = ;;154
243		eqid 2739	. . . . . . . . . . 11 ⊢ ;;011 = ;;011
244	152	oveq2i 7279	. . . . . . . . . . . 12 ⊢ (;15 + 1) = (;15 + ;01)
245		eqid 2739	. . . . . . . . . . . . 13 ⊢ ;15 = ;15
246		5p1e6 12103	. . . . . . . . . . . . 13 ⊢ (5 + 1) = 6
247	1, 54, 1, 245, 246	decaddi 12479	. . . . . . . . . . . 12 ⊢ (;15 + 1) = ;16
248	244, 247	eqtr3i 2769	. . . . . . . . . . 11 ⊢ (;15 + ;01) = ;16
249	235, 24, 237, 1, 242, 243, 248, 210	decadd 12473	. . . . . . . . . 10 ⊢ (;;154 + ;;011) = ;;165
250	236, 1, 238, 51, 239, 241, 249, 192	decadd 12473	. . . . . . . . 9 ⊢ (;;;1541 + ;;110) = ;;;1651
251		7t2e14 12528	. . . . . . . . . . 11 ⊢ (7 · 2) = ;14
252		8t7e56 12539	. . . . . . . . . . . 12 ⊢ (8 · 7) = ;56
253	158, 217, 252	mulcomli 10968	. . . . . . . . . . 11 ⊢ (7 · 8) = ;56
254		8t2e16 12534	. . . . . . . . . . 11 ⊢ (8 · 2) = ;16
255		eqid 2739	. . . . . . . . . . . . . 14 ⊢ ;56 = ;56
256		5cn 12044	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℂ
257	256, 138, 246	addcomli 11150	. . . . . . . . . . . . . . . 16 ⊢ (1 + 5) = 6
258	257	oveq1i 7278	. . . . . . . . . . . . . . 15 ⊢ ((1 + 5) + 1) = (6 + 1)
259	258, 140	eqtri 2767	. . . . . . . . . . . . . 14 ⊢ ((1 + 5) + 1) = 7
260		6p6e12 12493	. . . . . . . . . . . . . 14 ⊢ (6 + 6) = ;12
261	1, 98, 54, 98, 135, 255, 259, 181, 260	decaddc 12474	. . . . . . . . . . . . 13 ⊢ (;16 + ;56) = ;72
262	261	oveq1i 7278	. . . . . . . . . . . 12 ⊢ ((;16 + ;56) + 6) = (;72 + 6)
263		eqid 2739	. . . . . . . . . . . . 13 ⊢ ;72 = ;72
264		6p2e8 12115	. . . . . . . . . . . . . 14 ⊢ (6 + 2) = 8
265	110, 197, 264	addcomli 11150	. . . . . . . . . . . . 13 ⊢ (2 + 6) = 8
266	52, 181, 98, 263, 265	decaddi 12479	. . . . . . . . . . . 12 ⊢ (;72 + 6) = ;78
267	262, 266	eqtri 2767	. . . . . . . . . . 11 ⊢ ((;16 + ;56) + 6) = ;78
268		eqid 2739	. . . . . . . . . . . 12 ⊢ ;14 = ;14
269		1p1e2 12081	. . . . . . . . . . . 12 ⊢ (1 + 1) = 2
270	1, 24, 52, 268, 269, 1, 225	decaddci 12480	. . . . . . . . . . 11 ⊢ (;14 + 7) = ;21
271	52, 73, 181, 73, 98, 52, 73, 24, 251, 253, 254, 123, 267, 270	dpmul 31166	. . . . . . . . . 10 ⊢ ((7.8) · (2.8)) = (;21._84)
272		eqid 2739	. . . . . . . . . . . . 13 ⊢ ;11 = ;11
273		eqid 2739	. . . . . . . . . . . . 13 ⊢ ;67 = ;67
274	217, 138, 71	addcomli 11150	. . . . . . . . . . . . 13 ⊢ (1 + 7) = 8
275	1, 1, 98, 52, 272, 273, 141, 274	decadd 12473	. . . . . . . . . . . 12 ⊢ (;11 + ;67) = ;78
276	1, 1, 98, 52, 52, 73, 275	dpadd 31164	. . . . . . . . . . 11 ⊢ ((1.1) + (6.7)) = (7.8)
277		4p4e8 12111	. . . . . . . . . . . . 13 ⊢ (4 + 4) = 8
278	1, 24, 1, 24, 268, 268, 269, 277	decadd 12473	. . . . . . . . . . . 12 ⊢ (;14 + ;14) = ;28
279	1, 24, 1, 24, 181, 73, 278	dpadd 31164	. . . . . . . . . . 11 ⊢ ((1.4) + (1.4)) = (2.8)
280	276, 279	oveq12i 7280	. . . . . . . . . 10 ⊢ (((1.1) + (6.7)) · ((1.4) + (1.4))) = ((7.8) · (2.8))
281	1, 181	deccl 12434	. . . . . . . . . . . . 13 ⊢ ;12 ∈ ℕ0
282		eqid 2739	. . . . . . . . . . . . . . 15 ⊢ ;;109 = ;;109
283	130	nn0cni 12228	. . . . . . . . . . . . . . . . 17 ⊢ ;10 ∈ ℂ
284	283, 138, 136	addcomli 11150	. . . . . . . . . . . . . . . 16 ⊢ (1 + ;10) = ;11
285	1, 1, 269, 284	decsuc 12450	. . . . . . . . . . . . . . 15 ⊢ ((1 + ;10) + 1) = ;12
286		9p5e14 12509	. . . . . . . . . . . . . . . 16 ⊢ (9 + 5) = ;14
287	196, 256, 286	addcomli 11150	. . . . . . . . . . . . . . 15 ⊢ (5 + 9) = ;14
288	1, 54, 130, 53, 245, 282, 285, 24, 287	decaddc 12474	. . . . . . . . . . . . . 14 ⊢ (;15 + ;;109) = ;;124
289		4p2e6 12109	. . . . . . . . . . . . . 14 ⊢ (4 + 2) = 6
290	235, 24, 186, 181, 242, 187, 288, 289	decadd 12473	. . . . . . . . . . . . 13 ⊢ (;;154 + ;;;1092) = ;;;1246
291	1, 54, 24, 130, 53, 281, 181, 24, 98, 290	dpadd3 31165	. . . . . . . . . . . 12 ⊢ ((1._54) + (;10._92)) = (;12._46)
292	291	oveq1i 7278	. . . . . . . . . . 11 ⊢ (((1._54) + (;10._92)) + (9._38)) = ((;12._46) + (9._38))
293	181, 1	deccl 12434	. . . . . . . . . . . 12 ⊢ ;21 ∈ ℕ0
294	281, 24	deccl 12434	. . . . . . . . . . . . 13 ⊢ ;;124 ∈ ℕ0
295	53, 182	deccl 12434	. . . . . . . . . . . . 13 ⊢ ;93 ∈ ℕ0
296		eqid 2739	. . . . . . . . . . . . 13 ⊢ ;;;1246 = ;;;1246
297		eqid 2739	. . . . . . . . . . . . 13 ⊢ ;;938 = ;;938
298		eqid 2739	. . . . . . . . . . . . . . 15 ⊢ ;;124 = ;;124
299		eqid 2739	. . . . . . . . . . . . . . 15 ⊢ ;93 = ;93
300		eqid 2739	. . . . . . . . . . . . . . . 16 ⊢ ;12 = ;12
301	1, 181, 53, 300, 269, 1, 200	decaddci 12480	. . . . . . . . . . . . . . 15 ⊢ (;12 + 9) = ;21
302		4p3e7 12110	. . . . . . . . . . . . . . 15 ⊢ (4 + 3) = 7
303	281, 24, 53, 182, 298, 299, 301, 302	decadd 12473	. . . . . . . . . . . . . 14 ⊢ (;;124 + ;93) = ;;217
304	293, 52, 71, 303	decsuc 12450	. . . . . . . . . . . . 13 ⊢ ((;;124 + ;93) + 1) = ;;218
305		8p6e14 12503	. . . . . . . . . . . . . 14 ⊢ (8 + 6) = ;14
306	158, 110, 305	addcomli 11150	. . . . . . . . . . . . 13 ⊢ (6 + 8) = ;14
307	294, 98, 295, 73, 296, 297, 304, 24, 306	decaddc 12474	. . . . . . . . . . . 12 ⊢ (;;;1246 + ;;938) = ;;;2184
308	281, 24, 98, 53, 182, 293, 73, 73, 24, 307	dpadd3 31165	. . . . . . . . . . 11 ⊢ ((;12._46) + (9._38)) = (;21._84)
309	292, 308	eqtri 2767	. . . . . . . . . 10 ⊢ (((1._54) + (;10._92)) + (9._38)) = (;21._84)
310	271, 280, 309	3eqtr4i 2777	. . . . . . . . 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 31167	. . . . . . . 8 ⊢ ((1._1_67) · (1._4_14)) < (1._6_51)
312	176, 32	remulcli 10975	. . . . . . . . 9 ⊢ ((1._1_67) · (1._4_14)) ∈ ℝ
313	33, 312, 43	lttri 11084	. . . . . . . 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 688	. . . . . . 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 12040	. . . . . . . . . . 11 ⊢ 4 ∈ ℝ
318		2re 12030	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
319		3re 12036	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ ℝ
320	34, 319	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ (6 ∈ ℝ ∧ 3 ∈ ℝ)
321		dp2cl 31133	. . . . . . . . . . . . . 14 ⊢ ((6 ∈ ℝ ∧ 3 ∈ ℝ) → _63 ∈ ℝ)
322	320, 321	ax-mp 5	. . . . . . . . . . . . 13 ⊢ _63 ∈ ℝ
323	318, 322	pm3.2i 470	. . . . . . . . . . . 12 ⊢ (2 ∈ ℝ ∧ _63 ∈ ℝ)
324		dp2cl 31133	. . . . . . . . . . . 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 31133	. . . . . . . . . 10 ⊢ ((4 ∈ ℝ ∧ _2_63 ∈ ℝ) → _4_2_63 ∈ ℝ)
328	326, 327	ax-mp 5	. . . . . . . . 9 ⊢ _4_2_63 ∈ ℝ
329		dpcl 31144	. . . . . . . . 9 ⊢ ((1 ∈ ℕ0 ∧ _4_2_63 ∈ ℝ) → (1._4_2_63) ∈ ℝ)
330	1, 328, 329	mp2an 688	. . . . . . . 8 ⊢ (1._4_2_63) ∈ ℝ
331	84, 319	pm3.2i 470	. . . . . . . . . . . . . . . 16 ⊢ (8 ∈ ℝ ∧ 3 ∈ ℝ)
332		dp2cl 31133	. . . . . . . . . . . . . . . 16 ⊢ ((8 ∈ ℝ ∧ 3 ∈ ℝ) → _83 ∈ ℝ)
333	331, 332	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ _83 ∈ ℝ
334	84, 333	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ (8 ∈ ℝ ∧ _83 ∈ ℝ)
335		dp2cl 31133	. . . . . . . . . . . . . 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 31133	. . . . . . . . . . . 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 31133	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ _3_8_83 ∈ ℝ) → _0_3_8_83 ∈ ℝ)
342	340, 341	ax-mp 5	. . . . . . . . 9 ⊢ _0_3_8_83 ∈ ℝ
343		dpcl 31144	. . . . . . . . 9 ⊢ ((1 ∈ ℕ0 ∧ _0_3_8_83 ∈ ℝ) → (1._0_3_8_83) ∈ ℝ)
344	1, 342, 343	mp2an 688	. . . . . . . 8 ⊢ (1._0_3_8_83) ∈ ℝ
345	330, 344	remulcli 10975	. . . . . . 7 ⊢ ((1._4_2_63) · (1._0_3_8_83)) ∈ ℝ
346	317, 333	pm3.2i 470	. . . . . . . . 9 ⊢ (4 ∈ ℝ ∧ _83 ∈ ℝ)
347		dp2cl 31133	. . . . . . . . 9 ⊢ ((4 ∈ ℝ ∧ _83 ∈ ℝ) → _4_83 ∈ ℝ)
348	346, 347	ax-mp 5	. . . . . . . 8 ⊢ _4_83 ∈ ℝ
349		dpcl 31144	. . . . . . . 8 ⊢ ((1 ∈ ℕ0 ∧ _4_83 ∈ ℝ) → (1._4_83) ∈ ℝ)
350	1, 348, 349	mp2an 688	. . . . . . 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 12718	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℝ+
353	98, 352	rpdp2cl 31135	. . . . . . . . . . . 12 ⊢ _63 ∈ ℝ+
354	181, 353	rpdp2cl 31135	. . . . . . . . . . 11 ⊢ _2_63 ∈ ℝ+
355	24, 354	rpdp2cl 31135	. . . . . . . . . 10 ⊢ _4_2_63 ∈ ℝ+
356	1, 355	rpdpcl 31156	. . . . . . . . 9 ⊢ (1._4_2_63) ∈ ℝ+
357		rpge0 12725	. . . . . . . . 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 31135	. . . . . . . . . . . . 13 ⊢ _83 ∈ ℝ+
360	73, 359	rpdp2cl 31135	. . . . . . . . . . . 12 ⊢ _8_83 ∈ ℝ+
361	182, 360	rpdp2cl 31135	. . . . . . . . . . 11 ⊢ _3_8_83 ∈ ℝ+
362	51, 361	rpdp2cl 31135	. . . . . . . . . 10 ⊢ _0_3_8_83 ∈ ℝ+
363	1, 362	rpdpcl 31156	. . . . . . . . 9 ⊢ (1._0_3_8_83) ∈ ℝ+
364		rpge0 12725	. . . . . . . . 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 11505	. . . . . . . 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 688	. . . . . . 7 ⊢ 0 ≤ ((1._4_2_63) · (1._0_3_8_83))
368	318, 3	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℝ ∧ 7 ∈ ℝ)
369		dp2cl 31133	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℝ ∧ 7 ∈ ℝ) → _27 ∈ ℝ)
370	368, 369	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ _27 ∈ ℝ
371	317, 370	pm3.2i 470	. . . . . . . . . . . . 13 ⊢ (4 ∈ ℝ ∧ _27 ∈ ℝ)
372		dp2cl 31133	. . . . . . . . . . . . 13 ⊢ ((4 ∈ ℝ ∧ _27 ∈ ℝ) → _4_27 ∈ ℝ)
373	371, 372	ax-mp 5	. . . . . . . . . . . 12 ⊢ _4_27 ∈ ℝ
374		dpcl 31144	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℕ0 ∧ _4_27 ∈ ℝ) → (1._4_27) ∈ ℝ)
375	1, 373, 374	mp2an 688	. . . . . . . . . . 11 ⊢ (1._4_27) ∈ ℝ
376	330, 375	pm3.2i 470	. . . . . . . . . 10 ⊢ ((1._4_2_63) ∈ ℝ ∧ (1._4_27) ∈ ℝ)
377		7nn 12048	. . . . . . . . . . . . . . 15 ⊢ 7 ∈ ℕ
378		nnrp 12723	. . . . . . . . . . . . . . 15 ⊢ (7 ∈ ℕ → 7 ∈ ℝ+)
379	377, 378	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 7 ∈ ℝ+
380	181, 379	rpdp2cl 31135	. . . . . . . . . . . . 13 ⊢ _27 ∈ ℝ+
381	24, 380	rpdp2cl 31135	. . . . . . . . . . . 12 ⊢ _4_27 ∈ ℝ+
382	98, 352, 184, 140	dp2ltsuc 31139	. . . . . . . . . . . . . 14 ⊢ _63 < 7
383	181, 353, 379, 382	dp2lt 31138	. . . . . . . . . . . . 13 ⊢ _2_63 < _27
384	24, 354, 380, 383	dp2lt 31138	. . . . . . . . . . . 12 ⊢ _4_2_63 < _4_27
385	1, 355, 381, 384	dplt 31157	. . . . . . . . . . 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 31133	. . . . . . . . . . . . . . 15 ⊢ ((3 ∈ ℝ ∧ 9 ∈ ℝ) → _39 ∈ ℝ)
390	388, 389	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ _39 ∈ ℝ
391	2, 390	pm3.2i 470	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ ∧ _39 ∈ ℝ)
392		dp2cl 31133	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ _39 ∈ ℝ) → _0_39 ∈ ℝ)
393	391, 392	ax-mp 5	. . . . . . . . . . . 12 ⊢ _0_39 ∈ ℝ
394		dpcl 31144	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℕ0 ∧ _0_39 ∈ ℝ) → (1._0_39) ∈ ℝ)
395	1, 393, 394	mp2an 688	. . . . . . . . . . 11 ⊢ (1._0_39) ∈ ℝ
396	344, 395	pm3.2i 470	. . . . . . . . . 10 ⊢ ((1._0_3_8_83) ∈ ℝ ∧ (1._0_39) ∈ ℝ)
397		9nn 12054	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ ℕ
398		nnrp 12723	. . . . . . . . . . . . . . 15 ⊢ (9 ∈ ℕ → 9 ∈ ℝ+)
399	397, 398	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 9 ∈ ℝ+
400	182, 399	rpdp2cl 31135	. . . . . . . . . . . . 13 ⊢ _39 ∈ ℝ+
401	51, 400	rpdp2cl 31135	. . . . . . . . . . . 12 ⊢ _0_39 ∈ ℝ+
402	73, 352, 185, 184	dp2lt10 31137	. . . . . . . . . . . . . . 15 ⊢ _83 < ;10
403	73, 359, 402, 160	dp2ltsuc 31139	. . . . . . . . . . . . . 14 ⊢ _8_83 < 9
404	182, 360, 399, 403	dp2lt 31138	. . . . . . . . . . . . 13 ⊢ _3_8_83 < _39
405	51, 361, 400, 404	dp2lt 31138	. . . . . . . . . . . 12 ⊢ _0_3_8_83 < _0_39
406	1, 362, 401, 405	dplt 31157	. . . . . . . . . . 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 11814	. . . . . . . . 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 688	. . . . . . . 8 ⊢ ((1._4_2_63) · (1._0_3_8_83)) < ((1._4_27) · (1._0_39))
411		6lt10 12553	. . . . . . . . 9 ⊢ 6 < ;10
412	73, 1	deccl 12434	. . . . . . . . . 10 ⊢ ;81 ∈ ℕ0
413		eqid 2739	. . . . . . . . . 10 ⊢ ;;816 = ;;816
414		eqid 2739	. . . . . . . . . 10 ⊢ ;10 = ;10
415		eqid 2739	. . . . . . . . . . . 12 ⊢ ;81 = ;81
416	73, 1, 269, 415	decsuc 12450	. . . . . . . . . . 11 ⊢ (;81 + 1) = ;82
417	73	dec0h 12441	. . . . . . . . . . . 12 ⊢ 8 = ;08
418	417	deceq1i 12426	. . . . . . . . . . 11 ⊢ ;82 = ;;082
419	416, 418	eqtri 2767	. . . . . . . . . 10 ⊢ (;81 + 1) = ;;082
420	110	addid1i 11145	. . . . . . . . . 10 ⊢ (6 + 0) = 6
421	412, 98, 1, 51, 413, 414, 419, 420	decadd 12473	. . . . . . . . 9 ⊢ (;;816 + ;10) = ;;;0826
422	138	mul01i 11148	. . . . . . . . . 10 ⊢ (1 · 0) = 0
423	113	mul01i 11148	. . . . . . . . . . 11 ⊢ (4 · 0) = 0
424	51	dec0h 12441	. . . . . . . . . . 11 ⊢ 0 = ;00
425	423, 424	eqtri 2767	. . . . . . . . . 10 ⊢ (4 · 0) = ;00
426	113	addid1i 11145	. . . . . . . . . . . 12 ⊢ (4 + 0) = 4
427	426	oveq1i 7278	. . . . . . . . . . 11 ⊢ ((4 + 0) + 0) = (4 + 0)
428	427, 426, 205	3eqtri 2771	. . . . . . . . . 10 ⊢ ((4 + 0) + 0) = ;04
429	1, 24, 1, 51, 51, 51, 24, 51, 116, 422, 203, 425, 428, 192	dpmul 31166	. . . . . . . . 9 ⊢ ((1.4) · (1.0)) = (1._40)
430		3cn 12037	. . . . . . . . . . 11 ⊢ 3 ∈ ℂ
431		3t2e6 12122	. . . . . . . . . . 11 ⊢ (3 · 2) = 6
432	430, 197, 431	mulcomli 10968	. . . . . . . . . 10 ⊢ (2 · 3) = 6
433		9t2e18 12541	. . . . . . . . . . 11 ⊢ (9 · 2) = ;18
434	196, 197, 433	mulcomli 10968	. . . . . . . . . 10 ⊢ (2 · 9) = ;18
435		7t3e21 12529	. . . . . . . . . 10 ⊢ (7 · 3) = ;21
436		9t7e63 12546	. . . . . . . . . . 11 ⊢ (9 · 7) = ;63
437	196, 217, 436	mulcomli 10968	. . . . . . . . . 10 ⊢ (7 · 9) = ;63
438		eqid 2739	. . . . . . . . . . . . 13 ⊢ ;21 = ;21
439		eqid 2739	. . . . . . . . . . . . 13 ⊢ ;18 = ;18
440	159, 160	eqtri 2767	. . . . . . . . . . . . 13 ⊢ (1 + 8) = 9
441	181, 1, 1, 73, 438, 439, 224, 440	decadd 12473	. . . . . . . . . . . 12 ⊢ (;21 + ;18) = ;39
442	441	oveq1i 7278	. . . . . . . . . . 11 ⊢ ((;21 + ;18) + 6) = (;39 + 6)
443		eqid 2739	. . . . . . . . . . . 12 ⊢ ;39 = ;39
444		3p1e4 12101	. . . . . . . . . . . 12 ⊢ (3 + 1) = 4
445		9p6e15 12510	. . . . . . . . . . . 12 ⊢ (9 + 6) = ;15
446	182, 53, 98, 443, 444, 54, 445	decaddci 12480	. . . . . . . . . . 11 ⊢ (;39 + 6) = ;45
447	442, 446	eqtri 2767	. . . . . . . . . 10 ⊢ ((;21 + ;18) + 6) = ;45
448		6p4e10 12491	. . . . . . . . . 10 ⊢ (6 + 4) = ;10
449	181, 52, 182, 53, 98, 24, 54, 182, 432, 434, 435, 437, 447, 448	dpmul 31166	. . . . . . . . 9 ⊢ ((2.7) · (3.9)) = (;10._53)
450	1, 24	deccl 12434	. . . . . . . . . . 11 ⊢ ;14 ∈ ℕ0
451	450, 51	deccl 12434	. . . . . . . . . 10 ⊢ ;;140 ∈ ℕ0
452	417, 73	eqeltrri 2837	. . . . . . . . . 10 ⊢ ;08 ∈ ℕ0
453		eqid 2739	. . . . . . . . . 10 ⊢ ;;;1401 = ;;;1401
454		eqid 2739	. . . . . . . . . 10 ⊢ ;;082 = ;;082
455		eqid 2739	. . . . . . . . . . 11 ⊢ ;;140 = ;;140
456	417, 158	eqeltrri 2837	. . . . . . . . . . . 12 ⊢ ;08 ∈ ℂ
457		0cn 10951	. . . . . . . . . . . 12 ⊢ 0 ∈ ℂ
458	417	oveq1i 7278	. . . . . . . . . . . . 13 ⊢ (8 + 0) = (;08 + 0)
459	158	addid1i 11145	. . . . . . . . . . . . 13 ⊢ (8 + 0) = 8
460	458, 459	eqtr3i 2769	. . . . . . . . . . . 12 ⊢ (;08 + 0) = 8
461	456, 457, 460	addcomli 11150	. . . . . . . . . . 11 ⊢ (0 + ;08) = 8
462	450, 51, 452, 455, 461	decaddi 12479	. . . . . . . . . 10 ⊢ (;;140 + ;08) = ;;148
463	451, 1, 452, 181, 453, 454, 462, 230	decadd 12473	. . . . . . . . 9 ⊢ (;;;1401 + ;;082) = ;;;1483
464		4t4e16 12518	. . . . . . . . . . 11 ⊢ (4 · 4) = ;16
465		9t4e36 12543	. . . . . . . . . . . 12 ⊢ (9 · 4) = ;36
466	196, 113, 465	mulcomli 10968	. . . . . . . . . . 11 ⊢ (4 · 9) = ;36
467	196	mulid1i 10963	. . . . . . . . . . . . 13 ⊢ (9 · 1) = 9
468	467, 188	eqtri 2767	. . . . . . . . . . . 12 ⊢ (9 · 1) = ;09
469	196, 138, 468	mulcomli 10968	. . . . . . . . . . 11 ⊢ (1 · 9) = ;09
470	182, 98	deccl 12434	. . . . . . . . . . . . . . 15 ⊢ ;36 ∈ ℕ0
471	470	nn0cni 12228	. . . . . . . . . . . . . 14 ⊢ ;36 ∈ ℂ
472		eqid 2739	. . . . . . . . . . . . . . 15 ⊢ ;36 = ;36
473	182, 98, 24, 472, 444, 51, 448	decaddci 12480	. . . . . . . . . . . . . 14 ⊢ (;36 + 4) = ;40
474	471, 113, 473	addcomli 11150	. . . . . . . . . . . . 13 ⊢ (4 + ;36) = ;40
475	474	oveq1i 7278	. . . . . . . . . . . 12 ⊢ ((4 + ;36) + 0) = (;40 + 0)
476	24, 51	deccl 12434	. . . . . . . . . . . . . 14 ⊢ ;40 ∈ ℕ0
477	476	nn0cni 12228	. . . . . . . . . . . . 13 ⊢ ;40 ∈ ℂ
478	477	addid1i 11145	. . . . . . . . . . . 12 ⊢ (;40 + 0) = ;40
479	475, 478	eqtri 2767	. . . . . . . . . . 11 ⊢ ((4 + ;36) + 0) = ;40
480	1, 98, 24, 135, 269, 51, 448	decaddci 12480	. . . . . . . . . . 11 ⊢ (;16 + 4) = ;20
481	24, 1, 24, 53, 51, 24, 51, 53, 464, 466, 204, 469, 479, 480	dpmul 31166	. . . . . . . . . 10 ⊢ ((4.1) · (4.9)) = (;20._09)
482		eqid 2739	. . . . . . . . . . . . 13 ⊢ ;27 = ;27
483	230	oveq1i 7278	. . . . . . . . . . . . . 14 ⊢ ((1 + 2) + 1) = (3 + 1)
484	483, 444	eqtri 2767	. . . . . . . . . . . . 13 ⊢ ((1 + 2) + 1) = 4
485	1, 24, 181, 52, 268, 482, 484, 1, 225	decaddc 12474	. . . . . . . . . . . 12 ⊢ (;14 + ;27) = ;41
486	1, 24, 181, 52, 24, 1, 485	dpadd 31164	. . . . . . . . . . 11 ⊢ ((1.4) + (2.7)) = (4.1)
487	430, 138, 444	addcomli 11150	. . . . . . . . . . . . 13 ⊢ (1 + 3) = 4
488	196	addid2i 11146	. . . . . . . . . . . . 13 ⊢ (0 + 9) = 9
489	1, 51, 182, 53, 414, 443, 487, 488	decadd 12473	. . . . . . . . . . . 12 ⊢ (;10 + ;39) = ;49
490	1, 51, 182, 53, 24, 53, 489	dpadd 31164	. . . . . . . . . . 11 ⊢ ((1.0) + (3.9)) = (4.9)
491	486, 490	oveq12i 7280	. . . . . . . . . 10 ⊢ (((1.4) + (2.7)) · ((1.0) + (3.9))) = ((4.1) · (4.9))
492	1, 24, 73, 1, 268, 415, 440, 210	decadd 12473	. . . . . . . . . . . . . 14 ⊢ (;14 + ;81) = ;95
493	450, 51, 412, 98, 455, 413, 492, 111	decadd 12473	. . . . . . . . . . . . 13 ⊢ (;;140 + ;;816) = ;;956
494	1, 24, 51, 73, 1, 53, 98, 54, 98, 493	dpadd3 31165	. . . . . . . . . . . 12 ⊢ ((1._40) + (8._16)) = (9._56)
495	494	oveq1i 7278	. . . . . . . . . . 11 ⊢ (((1._40) + (8._16)) + (;10._53)) = ((9._56) + (;10._53))
496	181, 51	deccl 12434	. . . . . . . . . . . 12 ⊢ ;20 ∈ ℕ0
497	53, 54	deccl 12434	. . . . . . . . . . . . 13 ⊢ ;95 ∈ ℕ0
498	130, 54	deccl 12434	. . . . . . . . . . . . 13 ⊢ ;;105 ∈ ℕ0
499		eqid 2739	. . . . . . . . . . . . 13 ⊢ ;;956 = ;;956
500		eqid 2739	. . . . . . . . . . . . 13 ⊢ ;;;1053 = ;;;1053
501		eqid 2739	. . . . . . . . . . . . . 14 ⊢ ;95 = ;95
502		eqid 2739	. . . . . . . . . . . . . 14 ⊢ ;;105 = ;;105
503		dec10p 12462	. . . . . . . . . . . . . . . . 17 ⊢ (;10 + 9) = ;19
504	283, 196, 503	addcomli 11150	. . . . . . . . . . . . . . . 16 ⊢ (9 + ;10) = ;19
505	504	oveq1i 7278	. . . . . . . . . . . . . . 15 ⊢ ((9 + ;10) + 1) = (;19 + 1)
506		eqid 2739	. . . . . . . . . . . . . . . 16 ⊢ ;19 = ;19
507	1, 53, 1, 506, 269, 51, 194	decaddci 12480	. . . . . . . . . . . . . . 15 ⊢ (;19 + 1) = ;20
508	505, 507	eqtri 2767	. . . . . . . . . . . . . 14 ⊢ ((9 + ;10) + 1) = ;20
509		5p5e10 12490	. . . . . . . . . . . . . 14 ⊢ (5 + 5) = ;10
510	53, 54, 130, 54, 501, 502, 508, 51, 509	decaddc 12474	. . . . . . . . . . . . 13 ⊢ (;95 + ;;105) = ;;200
511	497, 98, 498, 182, 499, 500, 510, 233	decadd 12473	. . . . . . . . . . . 12 ⊢ (;;956 + ;;;1053) = ;;;2009
512	53, 54, 98, 130, 54, 496, 182, 51, 53, 511	dpadd3 31165	. . . . . . . . . . 11 ⊢ ((9._56) + (;10._53)) = (;20._09)
513	495, 512	eqtri 2767	. . . . . . . . . 10 ⊢ (((1._40) + (8._16)) + (;10._53)) = (;20._09)
514	481, 491, 513	3eqtr4i 2777	. . . . . . . . 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 31167	. . . . . . . 8 ⊢ ((1._4_27) · (1._0_39)) < (1._4_83)
516	375, 395	remulcli 10975	. . . . . . . . 9 ⊢ ((1._4_27) · (1._0_39)) ∈ ℝ
517	345, 516, 350	lttri 11084	. . . . . . . 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 688	. . . . . . 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 11814	. . . . 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 688	. . . 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 12434	. . . . 5 ⊢ ;42 ∈ ℕ0
524	496, 24	deccl 12434	. . . . . 6 ⊢ ;;204 ∈ ℕ0
525		eqid 2739	. . . . . 6 ⊢ ;;;2042 = ;;;2042
526		eqid 2739	. . . . . 6 ⊢ ;42 = ;42
527		eqid 2739	. . . . . . 7 ⊢ ;;204 = ;;204
528	496, 24, 24, 527, 277	decaddi 12479	. . . . . 6 ⊢ (;;204 + 4) = ;;208
529		2p2e4 12091	. . . . . 6 ⊢ (2 + 2) = 4
530	524, 181, 24, 181, 525, 526, 528, 529	decadd 12473	. . . . 5 ⊢ (;;;2042 + ;42) = ;;;2084
531	448	oveq1i 7278	. . . . . . 7 ⊢ ((6 + 4) + 2) = (;10 + 2)
532		dec10p 12462	. . . . . . 7 ⊢ (;10 + 2) = ;12
533	531, 532	eqtri 2767	. . . . . 6 ⊢ ((6 + 4) + 2) = ;12
534	1, 98, 1, 24, 181, 1, 181, 24, 116, 204, 215, 216, 533, 269	dpmul 31166	. . . . 5 ⊢ ((1.6) · (1.4)) = (2._24)
535		8t5e40 12537	. . . . . . 7 ⊢ (8 · 5) = ;40
536	158, 256, 535	mulcomli 10968	. . . . . 6 ⊢ (5 · 8) = ;40
537		5t3e15 12520	. . . . . 6 ⊢ (5 · 3) = ;15
538	158	mulid2i 10964	. . . . . 6 ⊢ (1 · 8) = 8
539	430	mulid2i 10964	. . . . . . 7 ⊢ (1 · 3) = 3
540	182	dec0h 12441	. . . . . . 7 ⊢ 3 = ;03
541	539, 540	eqtri 2767	. . . . . 6 ⊢ (1 · 3) = ;03
542	235	nn0cni 12228	. . . . . . . . 9 ⊢ ;15 ∈ ℂ
543		8p5e13 12502	. . . . . . . . . . 11 ⊢ (8 + 5) = ;13
544	158, 256, 543	addcomli 11150	. . . . . . . . . 10 ⊢ (5 + 8) = ;13
545	1, 54, 73, 245, 269, 182, 544	decaddci 12480	. . . . . . . . 9 ⊢ (;15 + 8) = ;23
546	542, 158, 545	addcomli 11150	. . . . . . . 8 ⊢ (8 + ;15) = ;23
547	546	oveq1i 7278	. . . . . . 7 ⊢ ((8 + ;15) + 0) = (;23 + 0)
548	181, 182	deccl 12434	. . . . . . . . 9 ⊢ ;23 ∈ ℕ0
549	548	nn0cni 12228	. . . . . . . 8 ⊢ ;23 ∈ ℂ
550	549	addid1i 11145	. . . . . . 7 ⊢ (;23 + 0) = ;23
551	547, 550	eqtri 2767	. . . . . 6 ⊢ ((8 + ;15) + 0) = ;23
552		eqid 2739	. . . . . . 7 ⊢ ;40 = ;40
553	197	addid2i 11146	. . . . . . 7 ⊢ (0 + 2) = 2
554	24, 51, 181, 552, 553	decaddi 12479	. . . . . 6 ⊢ (;40 + 2) = ;42
555	54, 1, 73, 182, 51, 181, 182, 182, 536, 537, 538, 541, 551, 554	dpmul 31166	. . . . 5 ⊢ ((5.1) · (8.3)) = (;42._33)
556	181, 181	deccl 12434	. . . . . . 7 ⊢ ;22 ∈ ℕ0
557	556, 24	deccl 12434	. . . . . 6 ⊢ ;;224 ∈ ℕ0
558		eqid 2739	. . . . . 6 ⊢ ;;;2241 = ;;;2241
559		eqid 2739	. . . . . 6 ⊢ ;;208 = ;;208
560		eqid 2739	. . . . . . 7 ⊢ ;;224 = ;;224
561		eqid 2739	. . . . . . 7 ⊢ ;20 = ;20
562		eqid 2739	. . . . . . . 8 ⊢ ;22 = ;22
563	181, 181, 181, 562, 529	decaddi 12479	. . . . . . 7 ⊢ (;22 + 2) = ;24
564	556, 24, 181, 51, 560, 561, 563, 426	decadd 12473	. . . . . 6 ⊢ (;;224 + ;20) = ;;244
565	557, 1, 496, 73, 558, 559, 564, 440	decadd 12473	. . . . 5 ⊢ (;;;2241 + ;;208) = ;;;2449
566	556, 98	deccl 12434	. . . . . . . 8 ⊢ ;;226 ∈ ℕ0
567	523, 182	deccl 12434	. . . . . . . 8 ⊢ ;;423 ∈ ℕ0
568		eqid 2739	. . . . . . . 8 ⊢ ;;;2266 = ;;;2266
569		eqid 2739	. . . . . . . 8 ⊢ ;;;4233 = ;;;4233
570		eqid 2739	. . . . . . . . 9 ⊢ ;;226 = ;;226
571		eqid 2739	. . . . . . . . 9 ⊢ ;;423 = ;;423
572	113, 197, 289	addcomli 11150	. . . . . . . . . 10 ⊢ (2 + 4) = 6
573	181, 181, 24, 181, 562, 526, 572, 529	decadd 12473	. . . . . . . . 9 ⊢ (;22 + ;42) = ;64
574	556, 98, 523, 182, 570, 571, 573, 233	decadd 12473	. . . . . . . 8 ⊢ (;;226 + ;;423) = ;;649
575	566, 98, 567, 182, 568, 569, 574, 233	decadd 12473	. . . . . . 7 ⊢ (;;;2266 + ;;;4233) = ;;;6499
576	556, 98, 98, 523, 182, 100, 182, 53, 53, 575	dpadd3 31165	. . . . . 6 ⊢ ((;22._66) + (;42._33)) = (;64._99)
577	496	nn0cni 12228	. . . . . . . . . . 11 ⊢ ;20 ∈ ℂ
578	181, 51, 181, 561, 553	decaddi 12479	. . . . . . . . . . 11 ⊢ (;20 + 2) = ;22
579	577, 197, 578	addcomli 11150	. . . . . . . . . 10 ⊢ (2 + ;20) = ;22
580	181, 181, 496, 24, 562, 527, 579, 572	decadd 12473	. . . . . . . . 9 ⊢ (;22 + ;;204) = ;;226
581	556, 24, 524, 181, 560, 525, 580, 289	decadd 12473	. . . . . . . 8 ⊢ (;;224 + ;;;2042) = ;;;2266
582	181, 181, 24, 496, 24, 556, 181, 98, 98, 581	dpadd3 31165	. . . . . . 7 ⊢ ((2._24) + (;20._42)) = (;22._66)
583	582	oveq1i 7278	. . . . . 6 ⊢ (((2._24) + (;20._42)) + (;42._33)) = ((;22._66) + (;42._33))
584		eqid 2739	. . . . . . . . . 10 ⊢ ;51 = ;51
585	1, 98, 54, 1, 135, 584, 257, 140	decadd 12473	. . . . . . . . 9 ⊢ (;16 + ;51) = ;67
586	1, 98, 54, 1, 98, 52, 585	dpadd 31164	. . . . . . . 8 ⊢ ((1.6) + (5.1)) = (6.7)
587		eqid 2739	. . . . . . . . . 10 ⊢ ;83 = ;83
588	1, 24, 73, 182, 268, 587, 440, 302	decadd 12473	. . . . . . . . 9 ⊢ (;14 + ;83) = ;97
589	1, 24, 73, 182, 53, 52, 588	dpadd 31164	. . . . . . . 8 ⊢ ((1.4) + (8.3)) = (9.7)
590	586, 589	oveq12i 7280	. . . . . . 7 ⊢ (((1.6) + (5.1)) · ((1.4) + (8.3))) = ((6.7) · (9.7))
591		9t6e54 12545	. . . . . . . . 9 ⊢ (9 · 6) = ;54
592	196, 110, 591	mulcomli 10968	. . . . . . . 8 ⊢ (6 · 9) = ;54
593		7t6e42 12532	. . . . . . . . 9 ⊢ (7 · 6) = ;42
594	217, 110, 593	mulcomli 10968	. . . . . . . 8 ⊢ (6 · 7) = ;42
595		7t7e49 12533	. . . . . . . 8 ⊢ (7 · 7) = ;49
596		eqid 2739	. . . . . . . . . . 11 ⊢ ;63 = ;63
597		3p2e5 12107	. . . . . . . . . . 11 ⊢ (3 + 2) = 5
598	98, 182, 24, 181, 596, 526, 448, 597	decadd 12473	. . . . . . . . . 10 ⊢ (;63 + ;42) = ;;105
599	598	oveq1i 7278	. . . . . . . . 9 ⊢ ((;63 + ;42) + 4) = (;;105 + 4)
600		5p4e9 12114	. . . . . . . . . 10 ⊢ (5 + 4) = 9
601	130, 54, 24, 502, 600	decaddi 12479	. . . . . . . . 9 ⊢ (;;105 + 4) = ;;109
602	599, 601	eqtri 2767	. . . . . . . 8 ⊢ ((;63 + ;42) + 4) = ;;109
603		eqid 2739	. . . . . . . . 9 ⊢ ;54 = ;54
604	54, 24, 1, 51, 603, 414, 246, 426	decadd 12473	. . . . . . . 8 ⊢ (;54 + ;10) = ;64
605	98, 52, 53, 52, 24, 130, 53, 53, 592, 594, 437, 595, 602, 604	dpmul 31166	. . . . . . 7 ⊢ ((6.7) · (9.7)) = (;64._99)
606	590, 605	eqtri 2767	. . . . . 6 ⊢ (((1.6) + (5.1)) · ((1.4) + (8.3))) = (;64._99)
607	576, 583, 606	3eqtr4ri 2778	. . . . 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 31167	. . . 4 ⊢ ((1._6_51) · (1._4_83)) < (2._4_49)
609	33, 345	remulcli 10975	. . . . 5 ⊢ ((((1._0_7_9_9_55)↑2) · (1._4_14)) · ((1._4_2_63) · (1._0_3_8_83))) ∈ ℝ
610	43, 350	remulcli 10975	. . . . 5 ⊢ ((1._6_51) · (1._4_83)) ∈ ℝ
611	24, 399	rpdp2cl 31135	. . . . . . . 8 ⊢ _49 ∈ ℝ+
612	24, 611	rpdp2cl 31135	. . . . . . 7 ⊢ _4_49 ∈ ℝ+
613	181, 612	rpdpcl 31156	. . . . . 6 ⊢ (2._4_49) ∈ ℝ+
614		rpre 12720	. . . . . 6 ⊢ ((2._4_49) ∈ ℝ+ → (2._4_49) ∈ ℝ)
615	613, 614	ax-mp 5	. . . . 5 ⊢ (2._4_49) ∈ ℝ
616	609, 610, 615	lttri 11084	. . . 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 688	. . 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 12061	. . . 4 ⊢ 0 < 3
619	609, 615, 319	ltmul2i 11879	. . . 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 229	. 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 31129	. . . . . . 7 ⊢ _0_00 = _00
623	622, 119	eqtri 2767	. . . . . 6 ⊢ _0_00 = 0
624	623	oveq2i 7279	. . . . 5 ⊢ (3._0_00) = (3.0)
625	182	dp0u 31154	. . . . 5 ⊢ (3.0) = 3
626	624, 625	eqtr2i 2768	. . . 4 ⊢ 3 = (3._0_00)
627	626	oveq1i 7278	. . 3 ⊢ (3 · (2._4_49)) = ((3._0_00) · (2._4_49))
628	450, 52	deccl 12434	. . . . . . 7 ⊢ ;;147 ∈ ℕ0
629	628, 51	deccl 12434	. . . . . 6 ⊢ ;;;1470 ∈ ℕ0
630	629	nn0cni 12228	. . . . 5 ⊢ ;;;1470 ∈ ℂ
631	630	addid1i 11145	. . . 4 ⊢ (;;;1470 + 0) = ;;;1470
632		4t3e12 12517	. . . . . 6 ⊢ (4 · 3) = ;12
633	113, 430, 632	mulcomli 10968	. . . . 5 ⊢ (3 · 4) = ;12
634	197	mul02i 11147	. . . . 5 ⊢ (0 · 2) = 0
635	113, 457, 425	mulcomli 10968	. . . . 5 ⊢ (0 · 4) = ;00
636	51, 51, 1, 181, 424, 300, 153, 553	decadd 12473	. . . . . . 7 ⊢ (0 + ;12) = ;12
637	636	oveq1i 7278	. . . . . 6 ⊢ ((0 + ;12) + 0) = (;12 + 0)
638	281	nn0cni 12228	. . . . . . 7 ⊢ ;12 ∈ ℂ
639	638	addid1i 11145	. . . . . 6 ⊢ (;12 + 0) = ;12
640	637, 639	eqtri 2767	. . . . 5 ⊢ ((0 + ;12) + 0) = ;12
641	182, 51, 181, 24, 51, 1, 181, 51, 431, 633, 634, 635, 640, 140	dpmul 31166	. . . 4 ⊢ ((3.0) · (2.4)) = (7._20)
642	51	dp0u 31154	. . . . . . 7 ⊢ (0.0) = 0
643	642	oveq1i 7278	. . . . . 6 ⊢ ((0.0) · (4.9)) = (0 · (4.9))
644		dpcl 31144	. . . . . . . . 9 ⊢ ((4 ∈ ℕ0 ∧ 9 ∈ ℝ) → (4.9) ∈ ℝ)
645	24, 4, 644	mp2an 688	. . . . . . . 8 ⊢ (4.9) ∈ ℝ
646	645	recni 10973	. . . . . . 7 ⊢ (4.9) ∈ ℂ
647	646	mul02i 11147	. . . . . 6 ⊢ (0 · (4.9)) = 0
648	643, 647	eqtri 2767	. . . . 5 ⊢ ((0.0) · (4.9)) = 0
649	119	oveq2i 7279	. . . . . 6 ⊢ (0._00) = (0.0)
650	649, 642	eqtri 2767	. . . . 5 ⊢ (0._00) = 0
651	648, 650	eqtr4i 2770	. . . 4 ⊢ ((0.0) · (4.9)) = (0._00)
652	52, 181	deccl 12434	. . . . . 6 ⊢ ;72 ∈ ℕ0
653	652, 51	deccl 12434	. . . . 5 ⊢ ;;720 ∈ ℕ0
654		eqid 2739	. . . . 5 ⊢ ;;;7201 = ;;;7201
655		eqid 2739	. . . . 5 ⊢ ;;147 = ;;147
656		eqid 2739	. . . . . 6 ⊢ ;;720 = ;;720
657	52, 181, 224, 263	decsuc 12450	. . . . . 6 ⊢ (;72 + 1) = ;73
658	652, 51, 1, 24, 656, 268, 657, 114	decadd 12473	. . . . 5 ⊢ (;;720 + ;14) = ;;734
659	653, 1, 450, 52, 654, 655, 658, 274	decadd 12473	. . . 4 ⊢ (;;;7201 + ;;147) = ;;;7348
660	642	oveq2i 7279	. . . . . . . 8 ⊢ ((3.0) + (0.0)) = ((3.0) + 0)
661	625, 430	eqeltri 2836	. . . . . . . . 9 ⊢ (3.0) ∈ ℂ
662	661	addid1i 11145	. . . . . . . 8 ⊢ ((3.0) + 0) = (3.0)
663	660, 662	eqtri 2767	. . . . . . 7 ⊢ ((3.0) + (0.0)) = (3.0)
664		eqid 2739	. . . . . . . . 9 ⊢ ;49 = ;49
665	572	oveq1i 7278	. . . . . . . . . 10 ⊢ ((2 + 4) + 1) = (6 + 1)
666	665, 140	eqtri 2767	. . . . . . . . 9 ⊢ ((2 + 4) + 1) = 7
667		9p4e13 12508	. . . . . . . . . 10 ⊢ (9 + 4) = ;13
668	196, 113, 667	addcomli 11150	. . . . . . . . 9 ⊢ (4 + 9) = ;13
669	181, 24, 24, 53, 223, 664, 666, 182, 668	decaddc 12474	. . . . . . . 8 ⊢ (;24 + ;49) = ;73
670	181, 24, 24, 53, 52, 182, 669	dpadd 31164	. . . . . . 7 ⊢ ((2.4) + (4.9)) = (7.3)
671	663, 670	oveq12i 7280	. . . . . 6 ⊢ (((3.0) + (0.0)) · ((2.4) + (4.9))) = ((3.0) · (7.3))
672	217, 430, 435	mulcomli 10968	. . . . . . 7 ⊢ (3 · 7) = ;21
673		3t3e9 12123	. . . . . . 7 ⊢ (3 · 3) = 9
674	217	mul01i 11148	. . . . . . . 8 ⊢ (7 · 0) = 0
675	217, 457, 674	mulcomli 10968	. . . . . . 7 ⊢ (0 · 7) = 0
676	430	mul01i 11148	. . . . . . . . 9 ⊢ (3 · 0) = 0
677	676, 424	eqtri 2767	. . . . . . . 8 ⊢ (3 · 0) = ;00
678	430, 457, 677	mulcomli 10968	. . . . . . 7 ⊢ (0 · 3) = ;00
679	196	addid1i 11145	. . . . . . . . . 10 ⊢ (9 + 0) = 9
680	679	oveq1i 7278	. . . . . . . . 9 ⊢ ((9 + 0) + 0) = (9 + 0)
681	680, 679, 188	3eqtri 2771	. . . . . . . 8 ⊢ ((9 + 0) + 0) = ;09
682	196, 457	addcomi 11149	. . . . . . . . . 10 ⊢ (9 + 0) = (0 + 9)
683	682	oveq1i 7278	. . . . . . . . 9 ⊢ ((9 + 0) + 0) = ((0 + 9) + 0)
684	683	eqeq1i 2744	. . . . . . . 8 ⊢ (((9 + 0) + 0) = ;09 ↔ ((0 + 9) + 0) = ;09)
685	681, 684	mpbi 229	. . . . . . 7 ⊢ ((0 + 9) + 0) = ;09
686	181, 1, 51, 438, 192	decaddi 12479	. . . . . . 7 ⊢ (;21 + 0) = ;21
687	182, 51, 52, 182, 51, 51, 53, 51, 672, 673, 675, 678, 685, 686	dpmul 31166	. . . . . 6 ⊢ ((3.0) · (7.3)) = (;21._90)
688	671, 687	eqtri 2767	. . . . 5 ⊢ (((3.0) + (0.0)) · ((2.4) + (4.9))) = (;21._90)
689	650	oveq2i 7279	. . . . . 6 ⊢ (((7._20) + (;14._70)) + (0._00)) = (((7._20) + (;14._70)) + 0)
690	318, 2	pm3.2i 470	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ ∧ 0 ∈ ℝ)
691		dp2cl 31133	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ 0 ∈ ℝ) → _20 ∈ ℝ)
692	690, 691	ax-mp 5	. . . . . . . . . 10 ⊢ _20 ∈ ℝ
693		dpcl 31144	. . . . . . . . . 10 ⊢ ((7 ∈ ℕ0 ∧ _20 ∈ ℝ) → (7._20) ∈ ℝ)
694	52, 692, 693	mp2an 688	. . . . . . . . 9 ⊢ (7._20) ∈ ℝ
695	694	recni 10973	. . . . . . . 8 ⊢ (7._20) ∈ ℂ
696	3, 2	pm3.2i 470	. . . . . . . . . . 11 ⊢ (7 ∈ ℝ ∧ 0 ∈ ℝ)
697		dp2cl 31133	. . . . . . . . . . 11 ⊢ ((7 ∈ ℝ ∧ 0 ∈ ℝ) → _70 ∈ ℝ)
698	696, 697	ax-mp 5	. . . . . . . . . 10 ⊢ _70 ∈ ℝ
699		dpcl 31144	. . . . . . . . . 10 ⊢ ((;14 ∈ ℕ0 ∧ _70 ∈ ℝ) → (;14._70) ∈ ℝ)
700	450, 698, 699	mp2an 688	. . . . . . . . 9 ⊢ (;14._70) ∈ ℝ
701	700	recni 10973	. . . . . . . 8 ⊢ (;14._70) ∈ ℂ
702	695, 701	addcli 10965	. . . . . . 7 ⊢ ((7._20) + (;14._70)) ∈ ℂ
703	702	addid1i 11145	. . . . . 6 ⊢ (((7._20) + (;14._70)) + 0) = ((7._20) + (;14._70))
704		eqid 2739	. . . . . . . 8 ⊢ ;;;1470 = ;;;1470
705	450	nn0cni 12228	. . . . . . . . . 10 ⊢ ;14 ∈ ℂ
706	705, 217, 270	addcomli 11150	. . . . . . . . 9 ⊢ (7 + ;14) = ;21
707		7p2e9 12117	. . . . . . . . . 10 ⊢ (7 + 2) = 9
708	217, 197, 707	addcomli 11150	. . . . . . . . 9 ⊢ (2 + 7) = 9
709	52, 181, 450, 52, 263, 655, 706, 708	decadd 12473	. . . . . . . 8 ⊢ (;72 + ;;147) = ;;219
710		00id 11133	. . . . . . . 8 ⊢ (0 + 0) = 0
711	652, 51, 628, 51, 656, 704, 709, 710	decadd 12473	. . . . . . 7 ⊢ (;;720 + ;;;1470) = ;;;2190
712	52, 181, 51, 450, 52, 293, 51, 53, 51, 711	dpadd3 31165	. . . . . 6 ⊢ ((7._20) + (;14._70)) = (;21._90)
713	689, 703, 712	3eqtri 2771	. . . . 5 ⊢ (((7._20) + (;14._70)) + (0._00)) = (;21._90)
714	688, 713	eqtr4i 2770	. . . 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 31167	. . 3 ⊢ ((3._0_00) · (2._4_49)) < (7._3_48)
716	627, 715	eqbrtri 5099	. 2 ⊢ (3 · (2._4_49)) < (7._3_48)
717	319, 609	remulcli 10975	. . 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 10975	. . 3 ⊢ (3 · (2._4_49)) ∈ ℝ
719		nnrp 12723	. . . . . . . 8 ⊢ (8 ∈ ℕ → 8 ∈ ℝ+)
720	63, 719	ax-mp 5	. . . . . . 7 ⊢ 8 ∈ ℝ+
721	24, 720	rpdp2cl 31135	. . . . . 6 ⊢ _48 ∈ ℝ+
722	182, 721	rpdp2cl 31135	. . . . 5 ⊢ _3_48 ∈ ℝ+
723	52, 722	rpdpcl 31156	. . . 4 ⊢ (7._3_48) ∈ ℝ+
724		rpre 12720	. . . 4 ⊢ ((7._3_48) ∈ ℝ+ → (7._3_48) ∈ ℝ)
725	723, 724	ax-mp 5	. . 3 ⊢ (7._3_48) ∈ ℝ
726	717, 718, 725	lttri 11084	. 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 688	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 205   ∧ wa 395   = wceq 1541   ∈ wcel 2109   class class class wbr 5078  (class class class)co 7268  ℂcc 10853  ℝcr 10854  0cc0 10855  1c1 10856   + caddc 10858   · cmul 10860   < clt 10993   ≤ cle 10994  ℕcn 11956  2c2 12011  3c3 12012  4c4 12013  5c5 12014  6c6 12015  7c7 12016  8c8 12017  9c9 12018  ℕ₀cn0 12216  ;cdc 12419  ℝ⁺crp 12712  ↑cexp 13763  _cdp2 31124  .cdp 31141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579  ax-cnex 10911  ax-resscn 10912  ax-1cn 10913  ax-icn 10914  ax-addcl 10915  ax-addrcl 10916  ax-mulcl 10917  ax-mulrcl 10918  ax-mulcom 10919  ax-addass 10920  ax-mulass 10921  ax-distr 10922  ax-i2m1 10923  ax-1ne0 10924  ax-1rid 10925  ax-rnegex 10926  ax-rrecex 10927  ax-cnre 10928  ax-pre-lttri 10929  ax-pre-lttrn 10930  ax-pre-ltadd 10931  ax-pre-mulgt0 10932

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-reu 3072  df-rmo 3073  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-tr 5196  df-id 5488  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-we 5545  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-pred 6199  df-ord 6266  df-on 6267  df-lim 6268  df-suc 6269  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-riota 7225  df-ov 7271  df-oprab 7272  df-mpo 7273  df-om 7701  df-2nd 7818  df-frecs 8081  df-wrecs 8112  df-recs 8186  df-rdg 8225  df-er 8472  df-en 8708  df-dom 8709  df-sdom 8710  df-pnf 10995  df-mnf 10996  df-xr 10997  df-ltxr 10998  df-le 10999  df-sub 11190  df-neg 11191  df-div 11616  df-nn 11957  df-2 12019  df-3 12020  df-4 12021  df-5 12022  df-6 12023  df-7 12024  df-8 12025  df-9 12026  df-n0 12217  df-z 12303  df-dec 12420  df-uz 12565  df-rp 12713  df-seq 13703  df-exp 13764  df-dp2 31125  df-dp 31142

This theorem is referenced by:  hgt750leme  32617