Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hgt750lem2 Structured version   Visualization version   GIF version

Theorem hgt750lem2 32031
Description: Decimal multiplication galore! (Contributed by Thierry Arnoux, 26-Dec-2021.)
Assertion
Ref Expression
hgt750lem2 (3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) < (7.348)

Proof of Theorem hgt750lem2
StepHypRef Expression
1 1nn0 11905 . . . . . . . . . 10 1 ∈ ℕ0
2 0re 10636 . . . . . . . . . . . 12 0 ∈ ℝ
3 7re 11722 . . . . . . . . . . . . . 14 7 ∈ ℝ
4 9re 11728 . . . . . . . . . . . . . . . 16 9 ∈ ℝ
5 5re 11716 . . . . . . . . . . . . . . . . . . . 20 5 ∈ ℝ
65, 5pm3.2i 474 . . . . . . . . . . . . . . . . . . 19 (5 ∈ ℝ ∧ 5 ∈ ℝ)
7 dp2cl 30585 . . . . . . . . . . . . . . . . . . 19 ((5 ∈ ℝ ∧ 5 ∈ ℝ) → 55 ∈ ℝ)
86, 7ax-mp 5 . . . . . . . . . . . . . . . . . 18 55 ∈ ℝ
94, 8pm3.2i 474 . . . . . . . . . . . . . . . . 17 (9 ∈ ℝ ∧ 55 ∈ ℝ)
10 dp2cl 30585 . . . . . . . . . . . . . . . . 17 ((9 ∈ ℝ ∧ 55 ∈ ℝ) → 955 ∈ ℝ)
119, 10ax-mp 5 . . . . . . . . . . . . . . . 16 955 ∈ ℝ
124, 11pm3.2i 474 . . . . . . . . . . . . . . 15 (9 ∈ ℝ ∧ 955 ∈ ℝ)
13 dp2cl 30585 . . . . . . . . . . . . . . 15 ((9 ∈ ℝ ∧ 955 ∈ ℝ) → 9955 ∈ ℝ)
1412, 13ax-mp 5 . . . . . . . . . . . . . 14 9955 ∈ ℝ
153, 14pm3.2i 474 . . . . . . . . . . . . 13 (7 ∈ ℝ ∧ 9955 ∈ ℝ)
16 dp2cl 30585 . . . . . . . . . . . . 13 ((7 ∈ ℝ ∧ 9955 ∈ ℝ) → 79955 ∈ ℝ)
1715, 16ax-mp 5 . . . . . . . . . . . 12 79955 ∈ ℝ
182, 17pm3.2i 474 . . . . . . . . . . 11 (0 ∈ ℝ ∧ 79955 ∈ ℝ)
19 dp2cl 30585 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ 79955 ∈ ℝ) → 079955 ∈ ℝ)
2018, 19ax-mp 5 . . . . . . . . . 10 079955 ∈ ℝ
21 dpcl 30596 . . . . . . . . . 10 ((1 ∈ ℕ0079955 ∈ ℝ) → (1.079955) ∈ ℝ)
221, 20, 21mp2an 691 . . . . . . . . 9 (1.079955) ∈ ℝ
2322resqcli 13549 . . . . . . . 8 ((1.079955)↑2) ∈ ℝ
24 4nn0 11908 . . . . . . . . . . 11 4 ∈ ℕ0
25 4nn 11712 . . . . . . . . . . . . 13 4 ∈ ℕ
26 nnrp 12392 . . . . . . . . . . . . 13 (4 ∈ ℕ → 4 ∈ ℝ+)
2725, 26ax-mp 5 . . . . . . . . . . . 12 4 ∈ ℝ+
281, 27rpdp2cl 30587 . . . . . . . . . . 11 14 ∈ ℝ+
2924, 28rpdp2cl 30587 . . . . . . . . . 10 414 ∈ ℝ+
301, 29rpdpcl 30608 . . . . . . . . 9 (1.414) ∈ ℝ+
31 rpre 12389 . . . . . . . . 9 ((1.414) ∈ ℝ+ → (1.414) ∈ ℝ)
3230, 31ax-mp 5 . . . . . . . 8 (1.414) ∈ ℝ
3323, 32remulcli 10650 . . . . . . 7 (((1.079955)↑2) · (1.414)) ∈ ℝ
34 6re 11719 . . . . . . . . . 10 6 ∈ ℝ
35 1re 10634 . . . . . . . . . . . 12 1 ∈ ℝ
365, 35pm3.2i 474 . . . . . . . . . . 11 (5 ∈ ℝ ∧ 1 ∈ ℝ)
37 dp2cl 30585 . . . . . . . . . . 11 ((5 ∈ ℝ ∧ 1 ∈ ℝ) → 51 ∈ ℝ)
3836, 37ax-mp 5 . . . . . . . . . 10 51 ∈ ℝ
3934, 38pm3.2i 474 . . . . . . . . 9 (6 ∈ ℝ ∧ 51 ∈ ℝ)
40 dp2cl 30585 . . . . . . . . 9 ((6 ∈ ℝ ∧ 51 ∈ ℝ) → 651 ∈ ℝ)
4139, 40ax-mp 5 . . . . . . . 8 651 ∈ ℝ
42 dpcl 30596 . . . . . . . 8 ((1 ∈ ℕ0651 ∈ ℝ) → (1.651) ∈ ℝ)
431, 41, 42mp2an 691 . . . . . . 7 (1.651) ∈ ℝ
4433, 43pm3.2i 474 . . . . . 6 ((((1.079955)↑2) · (1.414)) ∈ ℝ ∧ (1.651) ∈ ℝ)
4522sqge0i 13551 . . . . . . . 8 0 ≤ ((1.079955)↑2)
46 rpgt0 12393 . . . . . . . . . 10 ((1.414) ∈ ℝ+ → 0 < (1.414))
4730, 46ax-mp 5 . . . . . . . . 9 0 < (1.414)
482, 32, 47ltleii 10756 . . . . . . . 8 0 ≤ (1.414)
4923, 32mulge0i 11180 . . . . . . . 8 ((0 ≤ ((1.079955)↑2) ∧ 0 ≤ (1.414)) → 0 ≤ (((1.079955)↑2) · (1.414)))
5045, 48, 49mp2an 691 . . . . . . 7 0 ≤ (((1.079955)↑2) · (1.414))
51 0nn0 11904 . . . . . . . . . . . . 13 0 ∈ ℕ0
52 7nn0 11911 . . . . . . . . . . . . . 14 7 ∈ ℕ0
53 9nn0 11913 . . . . . . . . . . . . . . 15 9 ∈ ℕ0
54 5nn0 11909 . . . . . . . . . . . . . . . . 17 5 ∈ ℕ0
55 5nn 11715 . . . . . . . . . . . . . . . . . 18 5 ∈ ℕ
56 nnrp 12392 . . . . . . . . . . . . . . . . . 18 (5 ∈ ℕ → 5 ∈ ℝ+)
5755, 56ax-mp 5 . . . . . . . . . . . . . . . . 17 5 ∈ ℝ+
5854, 57rpdp2cl 30587 . . . . . . . . . . . . . . . 16 55 ∈ ℝ+
5953, 58rpdp2cl 30587 . . . . . . . . . . . . . . 15 955 ∈ ℝ+
6053, 59rpdp2cl 30587 . . . . . . . . . . . . . 14 9955 ∈ ℝ+
6152, 60rpdp2cl 30587 . . . . . . . . . . . . 13 79955 ∈ ℝ+
6251, 61rpdp2cl 30587 . . . . . . . . . . . 12 079955 ∈ ℝ+
63 8nn 11724 . . . . . . . . . . . . . 14 8 ∈ ℕ
6463rpdp2cl2 30588 . . . . . . . . . . . . 13 80 ∈ ℝ+
6551, 64rpdp2cl 30587 . . . . . . . . . . . 12 080 ∈ ℝ+
66 9lt10 12221 . . . . . . . . . . . . . . . 16 9 < 10
67 5lt10 12225 . . . . . . . . . . . . . . . . . 18 5 < 10
6854, 57, 67, 67dp2lt10 30589 . . . . . . . . . . . . . . . . 17 55 < 10
6953, 58, 66, 68dp2lt10 30589 . . . . . . . . . . . . . . . 16 955 < 10
7053, 59, 66, 69dp2lt10 30589 . . . . . . . . . . . . . . 15 9955 < 10
71 7p1e8 11778 . . . . . . . . . . . . . . 15 (7 + 1) = 8
7252, 60, 70, 71dp2ltsuc 30591 . . . . . . . . . . . . . 14 79955 < 8
73 8nn0 11912 . . . . . . . . . . . . . . 15 8 ∈ ℕ0
7473dp20u 30583 . . . . . . . . . . . . . 14 80 = 8
7572, 74breqtrri 5060 . . . . . . . . . . . . 13 79955 < 80
7651, 61, 64, 75dp2lt 30590 . . . . . . . . . . . 12 079955 < 080
771, 62, 65, 76dplt 30609 . . . . . . . . . . 11 (1.079955) < (1.080)
781, 62rpdpcl 30608 . . . . . . . . . . . . 13 (1.079955) ∈ ℝ+
79 rpge0 12394 . . . . . . . . . . . . 13 ((1.079955) ∈ ℝ+ → 0 ≤ (1.079955))
8078, 79ax-mp 5 . . . . . . . . . . . 12 0 ≤ (1.079955)
811, 65rpdpcl 30608 . . . . . . . . . . . . 13 (1.080) ∈ ℝ+
82 rpge0 12394 . . . . . . . . . . . . 13 ((1.080) ∈ ℝ+ → 0 ≤ (1.080))
8381, 82ax-mp 5 . . . . . . . . . . . 12 0 ≤ (1.080)
84 8re 11725 . . . . . . . . . . . . . . . . . 18 8 ∈ ℝ
8584, 2pm3.2i 474 . . . . . . . . . . . . . . . . 17 (8 ∈ ℝ ∧ 0 ∈ ℝ)
86 dp2cl 30585 . . . . . . . . . . . . . . . . 17 ((8 ∈ ℝ ∧ 0 ∈ ℝ) → 80 ∈ ℝ)
8785, 86ax-mp 5 . . . . . . . . . . . . . . . 16 80 ∈ ℝ
882, 87pm3.2i 474 . . . . . . . . . . . . . . 15 (0 ∈ ℝ ∧ 80 ∈ ℝ)
89 dp2cl 30585 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ 80 ∈ ℝ) → 080 ∈ ℝ)
9088, 89ax-mp 5 . . . . . . . . . . . . . 14 080 ∈ ℝ
91 dpcl 30596 . . . . . . . . . . . . . 14 ((1 ∈ ℕ0080 ∈ ℝ) → (1.080) ∈ ℝ)
921, 90, 91mp2an 691 . . . . . . . . . . . . 13 (1.080) ∈ ℝ
9322, 92lt2sqi 13552 . . . . . . . . . . . 12 ((0 ≤ (1.079955) ∧ 0 ≤ (1.080)) → ((1.079955) < (1.080) ↔ ((1.079955)↑2) < ((1.080)↑2)))
9480, 83, 93mp2an 691 . . . . . . . . . . 11 ((1.079955) < (1.080) ↔ ((1.079955)↑2) < ((1.080)↑2))
9577, 94mpbi 233 . . . . . . . . . 10 ((1.079955)↑2) < ((1.080)↑2)
9692recni 10648 . . . . . . . . . . . 12 (1.080) ∈ ℂ
9796sqvali 13543 . . . . . . . . . . 11 ((1.080)↑2) = ((1.080) · (1.080))
98 6nn0 11910 . . . . . . . . . . . . 13 6 ∈ ℕ0
991, 98deccl 12105 . . . . . . . . . . . 12 16 ∈ ℕ0
10098, 24deccl 12105 . . . . . . . . . . . 12 64 ∈ ℕ0
101 4lt10 12226 . . . . . . . . . . . 12 4 < 10
102 10pos 12107 . . . . . . . . . . . 12 0 < 10
10399, 51deccl 12105 . . . . . . . . . . . . 13 160 ∈ ℕ0
104 eqid 2801 . . . . . . . . . . . . 13 1600 = 1600
105 eqid 2801 . . . . . . . . . . . . 13 64 = 64
106 eqid 2801 . . . . . . . . . . . . . 14 160 = 160
10798dec0h 12112 . . . . . . . . . . . . . 14 6 = 06
10899nn0cni 11901 . . . . . . . . . . . . . . 15 16 ∈ ℂ
109108addid1i 10820 . . . . . . . . . . . . . 14 (16 + 0) = 16
110 6cn 11720 . . . . . . . . . . . . . . 15 6 ∈ ℂ
111110addid2i 10821 . . . . . . . . . . . . . 14 (0 + 6) = 6
11299, 51, 51, 98, 106, 107, 109, 111decadd 12144 . . . . . . . . . . . . 13 (160 + 6) = 166
113 4cn 11714 . . . . . . . . . . . . . 14 4 ∈ ℂ
114113addid2i 10821 . . . . . . . . . . . . 13 (0 + 4) = 4
115103, 51, 98, 24, 104, 105, 112, 114decadd 12144 . . . . . . . . . . . 12 (1600 + 64) = 1664
116 1t1e1 11791 . . . . . . . . . . . . 13 (1 · 1) = 1
1171dp0u 30606 . . . . . . . . . . . . . 14 (1.0) = 1
118117, 117oveq12i 7151 . . . . . . . . . . . . 13 ((1.0) · (1.0)) = (1 · 1)
11951dp20u 30583 . . . . . . . . . . . . . . 15 00 = 0
120119oveq2i 7150 . . . . . . . . . . . . . 14 (1.00) = (1.0)
121120, 117eqtri 2824 . . . . . . . . . . . . 13 (1.00) = 1
122116, 118, 1213eqtr4i 2834 . . . . . . . . . . . 12 ((1.0) · (1.0)) = (1.00)
123 8t8e64 12211 . . . . . . . . . . . . 13 (8 · 8) = 64
12473dp0u 30606 . . . . . . . . . . . . . 14 (8.0) = 8
125124, 124oveq12i 7151 . . . . . . . . . . . . 13 ((8.0) · (8.0)) = (8 · 8)
126119oveq2i 7150 . . . . . . . . . . . . . 14 (64.00) = (64.0)
127100dp0u 30606 . . . . . . . . . . . . . 14 (64.0) = 64
128126, 127eqtri 2824 . . . . . . . . . . . . 13 (64.00) = 64
129123, 125, 1283eqtr4i 2834 . . . . . . . . . . . 12 ((8.0) · (8.0)) = (64.00)
130 10nn0 12108 . . . . . . . . . . . . . 14 10 ∈ ℕ0
131130, 51deccl 12105 . . . . . . . . . . . . 13 100 ∈ ℕ0
132 eqid 2801 . . . . . . . . . . . . 13 1001 = 1001
133 eqid 2801 . . . . . . . . . . . . 13 166 = 166
134 eqid 2801 . . . . . . . . . . . . . 14 100 = 100
135 eqid 2801 . . . . . . . . . . . . . 14 16 = 16
136 dec10p 12133 . . . . . . . . . . . . . 14 (10 + 1) = 11
137130, 51, 1, 98, 134, 135, 136, 111decadd 12144 . . . . . . . . . . . . 13 (100 + 16) = 116
138 ax-1cn 10588 . . . . . . . . . . . . . . 15 1 ∈ ℂ
139138, 110addcomi 10824 . . . . . . . . . . . . . 14 (1 + 6) = (6 + 1)
140 6p1e7 11777 . . . . . . . . . . . . . 14 (6 + 1) = 7
141139, 140eqtri 2824 . . . . . . . . . . . . 13 (1 + 6) = 7
142131, 1, 99, 98, 132, 133, 137, 141decadd 12144 . . . . . . . . . . . 12 (1001 + 166) = 1167
143 eqid 2801 . . . . . . . . . . . . . 14 17 = 17
144141oveq1i 7149 . . . . . . . . . . . . . . 15 ((1 + 6) + 1) = (7 + 1)
145144, 71eqtri 2824 . . . . . . . . . . . . . 14 ((1 + 6) + 1) = 8
146 7p4e11 12166 . . . . . . . . . . . . . 14 (7 + 4) = 11
1471, 52, 98, 24, 143, 105, 145, 1, 146decaddc 12145 . . . . . . . . . . . . 13 (17 + 64) = 81
148119oveq2i 7150 . . . . . . . . . . . . . . . . 17 (16.00) = (16.0)
14999dp0u 30606 . . . . . . . . . . . . . . . . 17 (16.0) = 16
150148, 149eqtri 2824 . . . . . . . . . . . . . . . 16 (16.00) = 16
151121, 150oveq12i 7151 . . . . . . . . . . . . . . 15 ((1.00) + (16.00)) = (1 + 16)
1521dec0h 12112 . . . . . . . . . . . . . . . 16 1 = 01
153138addid2i 10821 . . . . . . . . . . . . . . . 16 (0 + 1) = 1
15451, 1, 1, 98, 152, 135, 153, 141decadd 12144 . . . . . . . . . . . . . . 15 (1 + 16) = 17
155151, 154eqtri 2824 . . . . . . . . . . . . . 14 ((1.00) + (16.00)) = 17
156155, 128oveq12i 7151 . . . . . . . . . . . . 13 (((1.00) + (16.00)) + (64.00)) = (17 + 64)
157117, 124oveq12i 7151 . . . . . . . . . . . . . . . 16 ((1.0) + (8.0)) = (1 + 8)
158 8cn 11726 . . . . . . . . . . . . . . . . 17 8 ∈ ℂ
159138, 158addcomi 10824 . . . . . . . . . . . . . . . 16 (1 + 8) = (8 + 1)
160 8p1e9 11779 . . . . . . . . . . . . . . . 16 (8 + 1) = 9
161157, 159, 1603eqtri 2828 . . . . . . . . . . . . . . 15 ((1.0) + (8.0)) = 9
162161, 161oveq12i 7151 . . . . . . . . . . . . . 14 (((1.0) + (8.0)) · ((1.0) + (8.0))) = (9 · 9)
163 9t9e81 12219 . . . . . . . . . . . . . 14 (9 · 9) = 81
164162, 163eqtri 2824 . . . . . . . . . . . . 13 (((1.0) + (8.0)) · ((1.0) + (8.0))) = 81
165147, 156, 1643eqtr4ri 2835 . . . . . . . . . . . 12 (((1.0) + (8.0)) · ((1.0) + (8.0))) = (((1.00) + (16.00)) + (64.00))
1661, 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, 165dpmul4 30619 . . . . . . . . . . 11 ((1.080) · (1.080)) < (1.167)
16797, 166eqbrtri 5054 . . . . . . . . . 10 ((1.080)↑2) < (1.167)
16892resqcli 13549 . . . . . . . . . . 11 ((1.080)↑2) ∈ ℝ
16934, 3pm3.2i 474 . . . . . . . . . . . . . . 15 (6 ∈ ℝ ∧ 7 ∈ ℝ)
170 dp2cl 30585 . . . . . . . . . . . . . . 15 ((6 ∈ ℝ ∧ 7 ∈ ℝ) → 67 ∈ ℝ)
171169, 170ax-mp 5 . . . . . . . . . . . . . 14 67 ∈ ℝ
17235, 171pm3.2i 474 . . . . . . . . . . . . 13 (1 ∈ ℝ ∧ 67 ∈ ℝ)
173 dp2cl 30585 . . . . . . . . . . . . 13 ((1 ∈ ℝ ∧ 67 ∈ ℝ) → 167 ∈ ℝ)
174172, 173ax-mp 5 . . . . . . . . . . . 12 167 ∈ ℝ
175 dpcl 30596 . . . . . . . . . . . 12 ((1 ∈ ℕ0167 ∈ ℝ) → (1.167) ∈ ℝ)
1761, 174, 175mp2an 691 . . . . . . . . . . 11 (1.167) ∈ ℝ
17723, 168, 176lttri 10759 . . . . . . . . . 10 ((((1.079955)↑2) < ((1.080)↑2) ∧ ((1.080)↑2) < (1.167)) → ((1.079955)↑2) < (1.167))
17895, 167, 177mp2an 691 . . . . . . . . 9 ((1.079955)↑2) < (1.167)
17923, 176, 32, 47ltmul1ii 11561 . . . . . . . . 9 (((1.079955)↑2) < (1.167) ↔ (((1.079955)↑2) · (1.414)) < ((1.167) · (1.414)))
180178, 179mpbi 233 . . . . . . . 8 (((1.079955)↑2) · (1.414)) < ((1.167) · (1.414))
181 2nn0 11906 . . . . . . . . 9 2 ∈ ℕ0
182 3nn0 11907 . . . . . . . . 9 3 ∈ ℕ0
183 1lt10 12229 . . . . . . . . 9 1 < 10
184 3lt10 12227 . . . . . . . . 9 3 < 10
185 8lt10 12222 . . . . . . . . 9 8 < 10
186130, 53deccl 12105 . . . . . . . . . 10 109 ∈ ℕ0
187 eqid 2801 . . . . . . . . . 10 1092 = 1092
18853dec0h 12112 . . . . . . . . . 10 9 = 09
189186nn0cni 11901 . . . . . . . . . . . 12 109 ∈ ℂ
190189addid1i 10820 . . . . . . . . . . 11 (109 + 0) = 109
191 dec10p 12133 . . . . . . . . . . . 12 (10 + 0) = 10
192138addid1i 10820 . . . . . . . . . . . 12 (1 + 0) = 1
1931, 51, 51, 1, 191, 152, 192, 153decadd 12144 . . . . . . . . . . 11 ((10 + 0) + 1) = 11
194 9p1e10 12092 . . . . . . . . . . 11 (9 + 1) = 10
195130, 53, 51, 1, 190, 152, 193, 51, 194decaddc 12145 . . . . . . . . . 10 ((109 + 0) + 1) = 110
196 9cn 11729 . . . . . . . . . . . 12 9 ∈ ℂ
197 2cn 11704 . . . . . . . . . . . 12 2 ∈ ℂ
198196, 197addcomi 10824 . . . . . . . . . . 11 (9 + 2) = (2 + 9)
199 9p2e11 12177 . . . . . . . . . . 11 (9 + 2) = 11
200198, 199eqtr3i 2826 . . . . . . . . . 10 (2 + 9) = 11
201186, 181, 51, 53, 187, 188, 195, 1, 200decaddc 12145 . . . . . . . . 9 (1092 + 9) = 1101
202113, 138mulcomi 10642 . . . . . . . . . . 11 (4 · 1) = (1 · 4)
203113mulid1i 10638 . . . . . . . . . . 11 (4 · 1) = 4
204202, 203eqtr3i 2826 . . . . . . . . . 10 (1 · 4) = 4
20524dec0h 12112 . . . . . . . . . . 11 4 = 04
206203, 202, 2053eqtr3i 2832 . . . . . . . . . 10 (1 · 4) = 04
207138, 113addcli 10640 . . . . . . . . . . . . 13 (1 + 4) ∈ ℂ
208207addid1i 10820 . . . . . . . . . . . 12 ((1 + 4) + 0) = (1 + 4)
209113, 138addcomi 10824 . . . . . . . . . . . 12 (4 + 1) = (1 + 4)
210 4p1e5 11775 . . . . . . . . . . . 12 (4 + 1) = 5
211208, 209, 2103eqtr2i 2830 . . . . . . . . . . 11 ((1 + 4) + 0) = 5
21254dec0h 12112 . . . . . . . . . . 11 5 = 05
213211, 212eqtri 2824 . . . . . . . . . 10 ((1 + 4) + 0) = 05
2141, 1, 1, 24, 51, 51, 54, 24, 116, 204, 116, 206, 213, 192dpmul 30618 . . . . . . . . 9 ((1.1) · (1.4)) = (1.54)
215110mulid1i 10638 . . . . . . . . . 10 (6 · 1) = 6
216 6t4e24 12196 . . . . . . . . . 10 (6 · 4) = 24
217 7cn 11723 . . . . . . . . . . 11 7 ∈ ℂ
218217mulid1i 10638 . . . . . . . . . 10 (7 · 1) = 7
219 7t4e28 12201 . . . . . . . . . 10 (7 · 4) = 28
220181, 24deccl 12105 . . . . . . . . . . . . . . 15 24 ∈ ℕ0
221220nn0cni 11901 . . . . . . . . . . . . . 14 24 ∈ ℂ
222221, 217addcomi 10824 . . . . . . . . . . . . 13 (24 + 7) = (7 + 24)
223 eqid 2801 . . . . . . . . . . . . . 14 24 = 24
224 2p1e3 11771 . . . . . . . . . . . . . 14 (2 + 1) = 3
225217, 113, 146addcomli 10825 . . . . . . . . . . . . . 14 (4 + 7) = 11
226181, 24, 52, 223, 224, 1, 225decaddci 12151 . . . . . . . . . . . . 13 (24 + 7) = 31
227222, 226eqtr3i 2826 . . . . . . . . . . . 12 (7 + 24) = 31
228227oveq1i 7149 . . . . . . . . . . 11 ((7 + 24) + 2) = (31 + 2)
229 eqid 2801 . . . . . . . . . . . 12 31 = 31
230197, 138, 224addcomli 10825 . . . . . . . . . . . 12 (1 + 2) = 3
231182, 1, 181, 229, 230decaddi 12150 . . . . . . . . . . 11 (31 + 2) = 33
232228, 231eqtri 2824 . . . . . . . . . 10 ((7 + 24) + 2) = 33
233 6p3e9 11789 . . . . . . . . . 10 (6 + 3) = 9
23498, 52, 1, 24, 181, 182, 182, 73, 215, 216, 218, 219, 232, 233dpmul 30618 . . . . . . . . 9 ((6.7) · (1.4)) = (9.38)
2351, 54deccl 12105 . . . . . . . . . . 11 15 ∈ ℕ0
236235, 24deccl 12105 . . . . . . . . . 10 154 ∈ ℕ0
23751, 1deccl 12105 . . . . . . . . . . 11 01 ∈ ℕ0
238237, 1deccl 12105 . . . . . . . . . 10 011 ∈ ℕ0
239 eqid 2801 . . . . . . . . . 10 1541 = 1541
240152deceq1i 12097 . . . . . . . . . . 11 11 = 011
241240deceq1i 12097 . . . . . . . . . 10 110 = 0110
242 eqid 2801 . . . . . . . . . . 11 154 = 154
243 eqid 2801 . . . . . . . . . . 11 011 = 011
244152oveq2i 7150 . . . . . . . . . . . 12 (15 + 1) = (15 + 01)
245 eqid 2801 . . . . . . . . . . . . 13 15 = 15
246 5p1e6 11776 . . . . . . . . . . . . 13 (5 + 1) = 6
2471, 54, 1, 245, 246decaddi 12150 . . . . . . . . . . . 12 (15 + 1) = 16
248244, 247eqtr3i 2826 . . . . . . . . . . 11 (15 + 01) = 16
249235, 24, 237, 1, 242, 243, 248, 210decadd 12144 . . . . . . . . . 10 (154 + 011) = 165
250236, 1, 238, 51, 239, 241, 249, 192decadd 12144 . . . . . . . . 9 (1541 + 110) = 1651
251 7t2e14 12199 . . . . . . . . . . 11 (7 · 2) = 14
252 8t7e56 12210 . . . . . . . . . . . 12 (8 · 7) = 56
253158, 217, 252mulcomli 10643 . . . . . . . . . . 11 (7 · 8) = 56
254 8t2e16 12205 . . . . . . . . . . 11 (8 · 2) = 16
255 eqid 2801 . . . . . . . . . . . . . 14 56 = 56
256 5cn 11717 . . . . . . . . . . . . . . . . 17 5 ∈ ℂ
257256, 138, 246addcomli 10825 . . . . . . . . . . . . . . . 16 (1 + 5) = 6
258257oveq1i 7149 . . . . . . . . . . . . . . 15 ((1 + 5) + 1) = (6 + 1)
259258, 140eqtri 2824 . . . . . . . . . . . . . 14 ((1 + 5) + 1) = 7
260 6p6e12 12164 . . . . . . . . . . . . . 14 (6 + 6) = 12
2611, 98, 54, 98, 135, 255, 259, 181, 260decaddc 12145 . . . . . . . . . . . . 13 (16 + 56) = 72
262261oveq1i 7149 . . . . . . . . . . . 12 ((16 + 56) + 6) = (72 + 6)
263 eqid 2801 . . . . . . . . . . . . 13 72 = 72
264 6p2e8 11788 . . . . . . . . . . . . . 14 (6 + 2) = 8
265110, 197, 264addcomli 10825 . . . . . . . . . . . . 13 (2 + 6) = 8
26652, 181, 98, 263, 265decaddi 12150 . . . . . . . . . . . 12 (72 + 6) = 78
267262, 266eqtri 2824 . . . . . . . . . . 11 ((16 + 56) + 6) = 78
268 eqid 2801 . . . . . . . . . . . 12 14 = 14
269 1p1e2 11754 . . . . . . . . . . . 12 (1 + 1) = 2
2701, 24, 52, 268, 269, 1, 225decaddci 12151 . . . . . . . . . . 11 (14 + 7) = 21
27152, 73, 181, 73, 98, 52, 73, 24, 251, 253, 254, 123, 267, 270dpmul 30618 . . . . . . . . . 10 ((7.8) · (2.8)) = (21.84)
272 eqid 2801 . . . . . . . . . . . . 13 11 = 11
273 eqid 2801 . . . . . . . . . . . . 13 67 = 67
274217, 138, 71addcomli 10825 . . . . . . . . . . . . 13 (1 + 7) = 8
2751, 1, 98, 52, 272, 273, 141, 274decadd 12144 . . . . . . . . . . . 12 (11 + 67) = 78
2761, 1, 98, 52, 52, 73, 275dpadd 30616 . . . . . . . . . . 11 ((1.1) + (6.7)) = (7.8)
277 4p4e8 11784 . . . . . . . . . . . . 13 (4 + 4) = 8
2781, 24, 1, 24, 268, 268, 269, 277decadd 12144 . . . . . . . . . . . 12 (14 + 14) = 28
2791, 24, 1, 24, 181, 73, 278dpadd 30616 . . . . . . . . . . 11 ((1.4) + (1.4)) = (2.8)
280276, 279oveq12i 7151 . . . . . . . . . 10 (((1.1) + (6.7)) · ((1.4) + (1.4))) = ((7.8) · (2.8))
2811, 181deccl 12105 . . . . . . . . . . . . 13 12 ∈ ℕ0
282 eqid 2801 . . . . . . . . . . . . . . 15 109 = 109
283130nn0cni 11901 . . . . . . . . . . . . . . . . 17 10 ∈ ℂ
284283, 138, 136addcomli 10825 . . . . . . . . . . . . . . . 16 (1 + 10) = 11
2851, 1, 269, 284decsuc 12121 . . . . . . . . . . . . . . 15 ((1 + 10) + 1) = 12
286 9p5e14 12180 . . . . . . . . . . . . . . . 16 (9 + 5) = 14
287196, 256, 286addcomli 10825 . . . . . . . . . . . . . . 15 (5 + 9) = 14
2881, 54, 130, 53, 245, 282, 285, 24, 287decaddc 12145 . . . . . . . . . . . . . 14 (15 + 109) = 124
289 4p2e6 11782 . . . . . . . . . . . . . 14 (4 + 2) = 6
290235, 24, 186, 181, 242, 187, 288, 289decadd 12144 . . . . . . . . . . . . 13 (154 + 1092) = 1246
2911, 54, 24, 130, 53, 281, 181, 24, 98, 290dpadd3 30617 . . . . . . . . . . . 12 ((1.54) + (10.92)) = (12.46)
292291oveq1i 7149 . . . . . . . . . . 11 (((1.54) + (10.92)) + (9.38)) = ((12.46) + (9.38))
293181, 1deccl 12105 . . . . . . . . . . . 12 21 ∈ ℕ0
294281, 24deccl 12105 . . . . . . . . . . . . 13 124 ∈ ℕ0
29553, 182deccl 12105 . . . . . . . . . . . . 13 93 ∈ ℕ0
296 eqid 2801 . . . . . . . . . . . . 13 1246 = 1246
297 eqid 2801 . . . . . . . . . . . . 13 938 = 938
298 eqid 2801 . . . . . . . . . . . . . . 15 124 = 124
299 eqid 2801 . . . . . . . . . . . . . . 15 93 = 93
300 eqid 2801 . . . . . . . . . . . . . . . 16 12 = 12
3011, 181, 53, 300, 269, 1, 200decaddci 12151 . . . . . . . . . . . . . . 15 (12 + 9) = 21
302 4p3e7 11783 . . . . . . . . . . . . . . 15 (4 + 3) = 7
303281, 24, 53, 182, 298, 299, 301, 302decadd 12144 . . . . . . . . . . . . . 14 (124 + 93) = 217
304293, 52, 71, 303decsuc 12121 . . . . . . . . . . . . 13 ((124 + 93) + 1) = 218
305 8p6e14 12174 . . . . . . . . . . . . . 14 (8 + 6) = 14
306158, 110, 305addcomli 10825 . . . . . . . . . . . . 13 (6 + 8) = 14
307294, 98, 295, 73, 296, 297, 304, 24, 306decaddc 12145 . . . . . . . . . . . 12 (1246 + 938) = 2184
308281, 24, 98, 53, 182, 293, 73, 73, 24, 307dpadd3 30617 . . . . . . . . . . 11 ((12.46) + (9.38)) = (21.84)
309292, 308eqtri 2824 . . . . . . . . . 10 (((1.54) + (10.92)) + (9.38)) = (21.84)
310271, 280, 3093eqtr4i 2834 . . . . . . . . 9 (((1.1) + (6.7)) · ((1.4) + (1.4))) = (((1.54) + (10.92)) + (9.38))
3111, 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, 310dpmul4 30619 . . . . . . . 8 ((1.167) · (1.414)) < (1.651)
312176, 32remulcli 10650 . . . . . . . . 9 ((1.167) · (1.414)) ∈ ℝ
31333, 312, 43lttri 10759 . . . . . . . 8 (((((1.079955)↑2) · (1.414)) < ((1.167) · (1.414)) ∧ ((1.167) · (1.414)) < (1.651)) → (((1.079955)↑2) · (1.414)) < (1.651))
314180, 311, 313mp2an 691 . . . . . . 7 (((1.079955)↑2) · (1.414)) < (1.651)
31550, 314pm3.2i 474 . . . . . 6 (0 ≤ (((1.079955)↑2) · (1.414)) ∧ (((1.079955)↑2) · (1.414)) < (1.651))
31644, 315pm3.2i 474 . . . . 5 (((((1.079955)↑2) · (1.414)) ∈ ℝ ∧ (1.651) ∈ ℝ) ∧ (0 ≤ (((1.079955)↑2) · (1.414)) ∧ (((1.079955)↑2) · (1.414)) < (1.651)))
317 4re 11713 . . . . . . . . . . 11 4 ∈ ℝ
318 2re 11703 . . . . . . . . . . . . 13 2 ∈ ℝ
319 3re 11709 . . . . . . . . . . . . . . 15 3 ∈ ℝ
32034, 319pm3.2i 474 . . . . . . . . . . . . . 14 (6 ∈ ℝ ∧ 3 ∈ ℝ)
321 dp2cl 30585 . . . . . . . . . . . . . 14 ((6 ∈ ℝ ∧ 3 ∈ ℝ) → 63 ∈ ℝ)
322320, 321ax-mp 5 . . . . . . . . . . . . 13 63 ∈ ℝ
323318, 322pm3.2i 474 . . . . . . . . . . . 12 (2 ∈ ℝ ∧ 63 ∈ ℝ)
324 dp2cl 30585 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ 63 ∈ ℝ) → 263 ∈ ℝ)
325323, 324ax-mp 5 . . . . . . . . . . 11 263 ∈ ℝ
326317, 325pm3.2i 474 . . . . . . . . . 10 (4 ∈ ℝ ∧ 263 ∈ ℝ)
327 dp2cl 30585 . . . . . . . . . 10 ((4 ∈ ℝ ∧ 263 ∈ ℝ) → 4263 ∈ ℝ)
328326, 327ax-mp 5 . . . . . . . . 9 4263 ∈ ℝ
329 dpcl 30596 . . . . . . . . 9 ((1 ∈ ℕ04263 ∈ ℝ) → (1.4263) ∈ ℝ)
3301, 328, 329mp2an 691 . . . . . . . 8 (1.4263) ∈ ℝ
33184, 319pm3.2i 474 . . . . . . . . . . . . . . . 16 (8 ∈ ℝ ∧ 3 ∈ ℝ)
332 dp2cl 30585 . . . . . . . . . . . . . . . 16 ((8 ∈ ℝ ∧ 3 ∈ ℝ) → 83 ∈ ℝ)
333331, 332ax-mp 5 . . . . . . . . . . . . . . 15 83 ∈ ℝ
33484, 333pm3.2i 474 . . . . . . . . . . . . . 14 (8 ∈ ℝ ∧ 83 ∈ ℝ)
335 dp2cl 30585 . . . . . . . . . . . . . 14 ((8 ∈ ℝ ∧ 83 ∈ ℝ) → 883 ∈ ℝ)
336334, 335ax-mp 5 . . . . . . . . . . . . 13 883 ∈ ℝ
337319, 336pm3.2i 474 . . . . . . . . . . . 12 (3 ∈ ℝ ∧ 883 ∈ ℝ)
338 dp2cl 30585 . . . . . . . . . . . 12 ((3 ∈ ℝ ∧ 883 ∈ ℝ) → 3883 ∈ ℝ)
339337, 338ax-mp 5 . . . . . . . . . . 11 3883 ∈ ℝ
3402, 339pm3.2i 474 . . . . . . . . . 10 (0 ∈ ℝ ∧ 3883 ∈ ℝ)
341 dp2cl 30585 . . . . . . . . . 10 ((0 ∈ ℝ ∧ 3883 ∈ ℝ) → 03883 ∈ ℝ)
342340, 341ax-mp 5 . . . . . . . . 9 03883 ∈ ℝ
343 dpcl 30596 . . . . . . . . 9 ((1 ∈ ℕ003883 ∈ ℝ) → (1.03883) ∈ ℝ)
3441, 342, 343mp2an 691 . . . . . . . 8 (1.03883) ∈ ℝ
345330, 344remulcli 10650 . . . . . . 7 ((1.4263) · (1.03883)) ∈ ℝ
346317, 333pm3.2i 474 . . . . . . . . 9 (4 ∈ ℝ ∧ 83 ∈ ℝ)
347 dp2cl 30585 . . . . . . . . 9 ((4 ∈ ℝ ∧ 83 ∈ ℝ) → 483 ∈ ℝ)
348346, 347ax-mp 5 . . . . . . . 8 483 ∈ ℝ
349 dpcl 30596 . . . . . . . 8 ((1 ∈ ℕ0483 ∈ ℝ) → (1.483) ∈ ℝ)
3501, 348, 349mp2an 691 . . . . . . 7 (1.483) ∈ ℝ
351345, 350pm3.2i 474 . . . . . 6 (((1.4263) · (1.03883)) ∈ ℝ ∧ (1.483) ∈ ℝ)
352 3rp 12387 . . . . . . . . . . . . 13 3 ∈ ℝ+
35398, 352rpdp2cl 30587 . . . . . . . . . . . 12 63 ∈ ℝ+
354181, 353rpdp2cl 30587 . . . . . . . . . . 11 263 ∈ ℝ+
35524, 354rpdp2cl 30587 . . . . . . . . . 10 4263 ∈ ℝ+
3561, 355rpdpcl 30608 . . . . . . . . 9 (1.4263) ∈ ℝ+
357 rpge0 12394 . . . . . . . . 9 ((1.4263) ∈ ℝ+ → 0 ≤ (1.4263))
358356, 357ax-mp 5 . . . . . . . 8 0 ≤ (1.4263)
35973, 352rpdp2cl 30587 . . . . . . . . . . . . 13 83 ∈ ℝ+
36073, 359rpdp2cl 30587 . . . . . . . . . . . 12 883 ∈ ℝ+
361182, 360rpdp2cl 30587 . . . . . . . . . . 11 3883 ∈ ℝ+
36251, 361rpdp2cl 30587 . . . . . . . . . 10 03883 ∈ ℝ+
3631, 362rpdpcl 30608 . . . . . . . . 9 (1.03883) ∈ ℝ+
364 rpge0 12394 . . . . . . . . 9 ((1.03883) ∈ ℝ+ → 0 ≤ (1.03883))
365363, 364ax-mp 5 . . . . . . . 8 0 ≤ (1.03883)
366330, 344mulge0i 11180 . . . . . . . 8 ((0 ≤ (1.4263) ∧ 0 ≤ (1.03883)) → 0 ≤ ((1.4263) · (1.03883)))
367358, 365, 366mp2an 691 . . . . . . 7 0 ≤ ((1.4263) · (1.03883))
368318, 3pm3.2i 474 . . . . . . . . . . . . . . 15 (2 ∈ ℝ ∧ 7 ∈ ℝ)
369 dp2cl 30585 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ ∧ 7 ∈ ℝ) → 27 ∈ ℝ)
370368, 369ax-mp 5 . . . . . . . . . . . . . 14 27 ∈ ℝ
371317, 370pm3.2i 474 . . . . . . . . . . . . 13 (4 ∈ ℝ ∧ 27 ∈ ℝ)
372 dp2cl 30585 . . . . . . . . . . . . 13 ((4 ∈ ℝ ∧ 27 ∈ ℝ) → 427 ∈ ℝ)
373371, 372ax-mp 5 . . . . . . . . . . . 12 427 ∈ ℝ
374 dpcl 30596 . . . . . . . . . . . 12 ((1 ∈ ℕ0427 ∈ ℝ) → (1.427) ∈ ℝ)
3751, 373, 374mp2an 691 . . . . . . . . . . 11 (1.427) ∈ ℝ
376330, 375pm3.2i 474 . . . . . . . . . 10 ((1.4263) ∈ ℝ ∧ (1.427) ∈ ℝ)
377 7nn 11721 . . . . . . . . . . . . . . 15 7 ∈ ℕ
378 nnrp 12392 . . . . . . . . . . . . . . 15 (7 ∈ ℕ → 7 ∈ ℝ+)
379377, 378ax-mp 5 . . . . . . . . . . . . . 14 7 ∈ ℝ+
380181, 379rpdp2cl 30587 . . . . . . . . . . . . 13 27 ∈ ℝ+
38124, 380rpdp2cl 30587 . . . . . . . . . . . 12 427 ∈ ℝ+
38298, 352, 184, 140dp2ltsuc 30591 . . . . . . . . . . . . . 14 63 < 7
383181, 353, 379, 382dp2lt 30590 . . . . . . . . . . . . 13 263 < 27
38424, 354, 380, 383dp2lt 30590 . . . . . . . . . . . 12 4263 < 427
3851, 355, 381, 384dplt 30609 . . . . . . . . . . 11 (1.4263) < (1.427)
386358, 385pm3.2i 474 . . . . . . . . . 10 (0 ≤ (1.4263) ∧ (1.4263) < (1.427))
387376, 386pm3.2i 474 . . . . . . . . 9 (((1.4263) ∈ ℝ ∧ (1.427) ∈ ℝ) ∧ (0 ≤ (1.4263) ∧ (1.4263) < (1.427)))
388319, 4pm3.2i 474 . . . . . . . . . . . . . . 15 (3 ∈ ℝ ∧ 9 ∈ ℝ)
389 dp2cl 30585 . . . . . . . . . . . . . . 15 ((3 ∈ ℝ ∧ 9 ∈ ℝ) → 39 ∈ ℝ)
390388, 389ax-mp 5 . . . . . . . . . . . . . 14 39 ∈ ℝ
3912, 390pm3.2i 474 . . . . . . . . . . . . 13 (0 ∈ ℝ ∧ 39 ∈ ℝ)
392 dp2cl 30585 . . . . . . . . . . . . 13 ((0 ∈ ℝ ∧ 39 ∈ ℝ) → 039 ∈ ℝ)
393391, 392ax-mp 5 . . . . . . . . . . . 12 039 ∈ ℝ
394 dpcl 30596 . . . . . . . . . . . 12 ((1 ∈ ℕ0039 ∈ ℝ) → (1.039) ∈ ℝ)
3951, 393, 394mp2an 691 . . . . . . . . . . 11 (1.039) ∈ ℝ
396344, 395pm3.2i 474 . . . . . . . . . 10 ((1.03883) ∈ ℝ ∧ (1.039) ∈ ℝ)
397 9nn 11727 . . . . . . . . . . . . . . 15 9 ∈ ℕ
398 nnrp 12392 . . . . . . . . . . . . . . 15 (9 ∈ ℕ → 9 ∈ ℝ+)
399397, 398ax-mp 5 . . . . . . . . . . . . . 14 9 ∈ ℝ+
400182, 399rpdp2cl 30587 . . . . . . . . . . . . 13 39 ∈ ℝ+
40151, 400rpdp2cl 30587 . . . . . . . . . . . 12 039 ∈ ℝ+
40273, 352, 185, 184dp2lt10 30589 . . . . . . . . . . . . . . 15 83 < 10
40373, 359, 402, 160dp2ltsuc 30591 . . . . . . . . . . . . . 14 883 < 9
404182, 360, 399, 403dp2lt 30590 . . . . . . . . . . . . 13 3883 < 39
40551, 361, 400, 404dp2lt 30590 . . . . . . . . . . . 12 03883 < 039
4061, 362, 401, 405dplt 30609 . . . . . . . . . . 11 (1.03883) < (1.039)
407365, 406pm3.2i 474 . . . . . . . . . 10 (0 ≤ (1.03883) ∧ (1.03883) < (1.039))
408396, 407pm3.2i 474 . . . . . . . . 9 (((1.03883) ∈ ℝ ∧ (1.039) ∈ ℝ) ∧ (0 ≤ (1.03883) ∧ (1.03883) < (1.039)))
409 ltmul12a 11489 . . . . . . . . 9 (((((1.4263) ∈ ℝ ∧ (1.427) ∈ ℝ) ∧ (0 ≤ (1.4263) ∧ (1.4263) < (1.427))) ∧ (((1.03883) ∈ ℝ ∧ (1.039) ∈ ℝ) ∧ (0 ≤ (1.03883) ∧ (1.03883) < (1.039)))) → ((1.4263) · (1.03883)) < ((1.427) · (1.039)))
410387, 408, 409mp2an 691 . . . . . . . 8 ((1.4263) · (1.03883)) < ((1.427) · (1.039))
411 6lt10 12224 . . . . . . . . 9 6 < 10
41273, 1deccl 12105 . . . . . . . . . 10 81 ∈ ℕ0
413 eqid 2801 . . . . . . . . . 10 816 = 816
414 eqid 2801 . . . . . . . . . 10 10 = 10
415 eqid 2801 . . . . . . . . . . . 12 81 = 81
41673, 1, 269, 415decsuc 12121 . . . . . . . . . . 11 (81 + 1) = 82
41773dec0h 12112 . . . . . . . . . . . 12 8 = 08
418417deceq1i 12097 . . . . . . . . . . 11 82 = 082
419416, 418eqtri 2824 . . . . . . . . . 10 (81 + 1) = 082
420110addid1i 10820 . . . . . . . . . 10 (6 + 0) = 6
421412, 98, 1, 51, 413, 414, 419, 420decadd 12144 . . . . . . . . 9 (816 + 10) = 0826
422138mul01i 10823 . . . . . . . . . 10 (1 · 0) = 0
423113mul01i 10823 . . . . . . . . . . 11 (4 · 0) = 0
42451dec0h 12112 . . . . . . . . . . 11 0 = 00
425423, 424eqtri 2824 . . . . . . . . . 10 (4 · 0) = 00
426113addid1i 10820 . . . . . . . . . . . 12 (4 + 0) = 4
427426oveq1i 7149 . . . . . . . . . . 11 ((4 + 0) + 0) = (4 + 0)
428427, 426, 2053eqtri 2828 . . . . . . . . . 10 ((4 + 0) + 0) = 04
4291, 24, 1, 51, 51, 51, 24, 51, 116, 422, 203, 425, 428, 192dpmul 30618 . . . . . . . . 9 ((1.4) · (1.0)) = (1.40)
430 3cn 11710 . . . . . . . . . . 11 3 ∈ ℂ
431 3t2e6 11795 . . . . . . . . . . 11 (3 · 2) = 6
432430, 197, 431mulcomli 10643 . . . . . . . . . 10 (2 · 3) = 6
433 9t2e18 12212 . . . . . . . . . . 11 (9 · 2) = 18
434196, 197, 433mulcomli 10643 . . . . . . . . . 10 (2 · 9) = 18
435 7t3e21 12200 . . . . . . . . . 10 (7 · 3) = 21
436 9t7e63 12217 . . . . . . . . . . 11 (9 · 7) = 63
437196, 217, 436mulcomli 10643 . . . . . . . . . 10 (7 · 9) = 63
438 eqid 2801 . . . . . . . . . . . . 13 21 = 21
439 eqid 2801 . . . . . . . . . . . . 13 18 = 18
440159, 160eqtri 2824 . . . . . . . . . . . . 13 (1 + 8) = 9
441181, 1, 1, 73, 438, 439, 224, 440decadd 12144 . . . . . . . . . . . 12 (21 + 18) = 39
442441oveq1i 7149 . . . . . . . . . . 11 ((21 + 18) + 6) = (39 + 6)
443 eqid 2801 . . . . . . . . . . . 12 39 = 39
444 3p1e4 11774 . . . . . . . . . . . 12 (3 + 1) = 4
445 9p6e15 12181 . . . . . . . . . . . 12 (9 + 6) = 15
446182, 53, 98, 443, 444, 54, 445decaddci 12151 . . . . . . . . . . 11 (39 + 6) = 45
447442, 446eqtri 2824 . . . . . . . . . 10 ((21 + 18) + 6) = 45
448 6p4e10 12162 . . . . . . . . . 10 (6 + 4) = 10
449181, 52, 182, 53, 98, 24, 54, 182, 432, 434, 435, 437, 447, 448dpmul 30618 . . . . . . . . 9 ((2.7) · (3.9)) = (10.53)
4501, 24deccl 12105 . . . . . . . . . . 11 14 ∈ ℕ0
451450, 51deccl 12105 . . . . . . . . . 10 140 ∈ ℕ0
452417, 73eqeltrri 2890 . . . . . . . . . 10 08 ∈ ℕ0
453 eqid 2801 . . . . . . . . . 10 1401 = 1401
454 eqid 2801 . . . . . . . . . 10 082 = 082
455 eqid 2801 . . . . . . . . . . 11 140 = 140
456417, 158eqeltrri 2890 . . . . . . . . . . . 12 08 ∈ ℂ
457 0cn 10626 . . . . . . . . . . . 12 0 ∈ ℂ
458417oveq1i 7149 . . . . . . . . . . . . 13 (8 + 0) = (08 + 0)
459158addid1i 10820 . . . . . . . . . . . . 13 (8 + 0) = 8
460458, 459eqtr3i 2826 . . . . . . . . . . . 12 (08 + 0) = 8
461456, 457, 460addcomli 10825 . . . . . . . . . . 11 (0 + 08) = 8
462450, 51, 452, 455, 461decaddi 12150 . . . . . . . . . 10 (140 + 08) = 148
463451, 1, 452, 181, 453, 454, 462, 230decadd 12144 . . . . . . . . 9 (1401 + 082) = 1483
464 4t4e16 12189 . . . . . . . . . . 11 (4 · 4) = 16
465 9t4e36 12214 . . . . . . . . . . . 12 (9 · 4) = 36
466196, 113, 465mulcomli 10643 . . . . . . . . . . 11 (4 · 9) = 36
467196mulid1i 10638 . . . . . . . . . . . . 13 (9 · 1) = 9
468467, 188eqtri 2824 . . . . . . . . . . . 12 (9 · 1) = 09
469196, 138, 468mulcomli 10643 . . . . . . . . . . 11 (1 · 9) = 09
470182, 98deccl 12105 . . . . . . . . . . . . . . 15 36 ∈ ℕ0
471470nn0cni 11901 . . . . . . . . . . . . . 14 36 ∈ ℂ
472 eqid 2801 . . . . . . . . . . . . . . 15 36 = 36
473182, 98, 24, 472, 444, 51, 448decaddci 12151 . . . . . . . . . . . . . 14 (36 + 4) = 40
474471, 113, 473addcomli 10825 . . . . . . . . . . . . 13 (4 + 36) = 40
475474oveq1i 7149 . . . . . . . . . . . 12 ((4 + 36) + 0) = (40 + 0)
47624, 51deccl 12105 . . . . . . . . . . . . . 14 40 ∈ ℕ0
477476nn0cni 11901 . . . . . . . . . . . . 13 40 ∈ ℂ
478477addid1i 10820 . . . . . . . . . . . 12 (40 + 0) = 40
479475, 478eqtri 2824 . . . . . . . . . . 11 ((4 + 36) + 0) = 40
4801, 98, 24, 135, 269, 51, 448decaddci 12151 . . . . . . . . . . 11 (16 + 4) = 20
48124, 1, 24, 53, 51, 24, 51, 53, 464, 466, 204, 469, 479, 480dpmul 30618 . . . . . . . . . 10 ((4.1) · (4.9)) = (20.09)
482 eqid 2801 . . . . . . . . . . . . 13 27 = 27
483230oveq1i 7149 . . . . . . . . . . . . . 14 ((1 + 2) + 1) = (3 + 1)
484483, 444eqtri 2824 . . . . . . . . . . . . 13 ((1 + 2) + 1) = 4
4851, 24, 181, 52, 268, 482, 484, 1, 225decaddc 12145 . . . . . . . . . . . 12 (14 + 27) = 41
4861, 24, 181, 52, 24, 1, 485dpadd 30616 . . . . . . . . . . 11 ((1.4) + (2.7)) = (4.1)
487430, 138, 444addcomli 10825 . . . . . . . . . . . . 13 (1 + 3) = 4
488196addid2i 10821 . . . . . . . . . . . . 13 (0 + 9) = 9
4891, 51, 182, 53, 414, 443, 487, 488decadd 12144 . . . . . . . . . . . 12 (10 + 39) = 49
4901, 51, 182, 53, 24, 53, 489dpadd 30616 . . . . . . . . . . 11 ((1.0) + (3.9)) = (4.9)
491486, 490oveq12i 7151 . . . . . . . . . 10 (((1.4) + (2.7)) · ((1.0) + (3.9))) = ((4.1) · (4.9))
4921, 24, 73, 1, 268, 415, 440, 210decadd 12144 . . . . . . . . . . . . . 14 (14 + 81) = 95
493450, 51, 412, 98, 455, 413, 492, 111decadd 12144 . . . . . . . . . . . . 13 (140 + 816) = 956
4941, 24, 51, 73, 1, 53, 98, 54, 98, 493dpadd3 30617 . . . . . . . . . . . 12 ((1.40) + (8.16)) = (9.56)
495494oveq1i 7149 . . . . . . . . . . 11 (((1.40) + (8.16)) + (10.53)) = ((9.56) + (10.53))
496181, 51deccl 12105 . . . . . . . . . . . 12 20 ∈ ℕ0
49753, 54deccl 12105 . . . . . . . . . . . . 13 95 ∈ ℕ0
498130, 54deccl 12105 . . . . . . . . . . . . 13 105 ∈ ℕ0
499 eqid 2801 . . . . . . . . . . . . 13 956 = 956
500 eqid 2801 . . . . . . . . . . . . 13 1053 = 1053
501 eqid 2801 . . . . . . . . . . . . . 14 95 = 95
502 eqid 2801 . . . . . . . . . . . . . 14 105 = 105
503 dec10p 12133 . . . . . . . . . . . . . . . . 17 (10 + 9) = 19
504283, 196, 503addcomli 10825 . . . . . . . . . . . . . . . 16 (9 + 10) = 19
505504oveq1i 7149 . . . . . . . . . . . . . . 15 ((9 + 10) + 1) = (19 + 1)
506 eqid 2801 . . . . . . . . . . . . . . . 16 19 = 19
5071, 53, 1, 506, 269, 51, 194decaddci 12151 . . . . . . . . . . . . . . 15 (19 + 1) = 20
508505, 507eqtri 2824 . . . . . . . . . . . . . 14 ((9 + 10) + 1) = 20
509 5p5e10 12161 . . . . . . . . . . . . . 14 (5 + 5) = 10
51053, 54, 130, 54, 501, 502, 508, 51, 509decaddc 12145 . . . . . . . . . . . . 13 (95 + 105) = 200
511497, 98, 498, 182, 499, 500, 510, 233decadd 12144 . . . . . . . . . . . 12 (956 + 1053) = 2009
51253, 54, 98, 130, 54, 496, 182, 51, 53, 511dpadd3 30617 . . . . . . . . . . 11 ((9.56) + (10.53)) = (20.09)
513495, 512eqtri 2824 . . . . . . . . . 10 (((1.40) + (8.16)) + (10.53)) = (20.09)
514481, 491, 5133eqtr4i 2834 . . . . . . . . 9 (((1.4) + (2.7)) · ((1.0) + (3.9))) = (((1.40) + (8.16)) + (10.53))
5151, 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, 514dpmul4 30619 . . . . . . . 8 ((1.427) · (1.039)) < (1.483)
516375, 395remulcli 10650 . . . . . . . . 9 ((1.427) · (1.039)) ∈ ℝ
517345, 516, 350lttri 10759 . . . . . . . 8 ((((1.4263) · (1.03883)) < ((1.427) · (1.039)) ∧ ((1.427) · (1.039)) < (1.483)) → ((1.4263) · (1.03883)) < (1.483))
518410, 515, 517mp2an 691 . . . . . . 7 ((1.4263) · (1.03883)) < (1.483)
519367, 518pm3.2i 474 . . . . . 6 (0 ≤ ((1.4263) · (1.03883)) ∧ ((1.4263) · (1.03883)) < (1.483))
520351, 519pm3.2i 474 . . . . 5 ((((1.4263) · (1.03883)) ∈ ℝ ∧ (1.483) ∈ ℝ) ∧ (0 ≤ ((1.4263) · (1.03883)) ∧ ((1.4263) · (1.03883)) < (1.483)))
521 ltmul12a 11489 . . . . 5 (((((((1.079955)↑2) · (1.414)) ∈ ℝ ∧ (1.651) ∈ ℝ) ∧ (0 ≤ (((1.079955)↑2) · (1.414)) ∧ (((1.079955)↑2) · (1.414)) < (1.651))) ∧ ((((1.4263) · (1.03883)) ∈ ℝ ∧ (1.483) ∈ ℝ) ∧ (0 ≤ ((1.4263) · (1.03883)) ∧ ((1.4263) · (1.03883)) < (1.483)))) → ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) < ((1.651) · (1.483)))
522316, 520, 521mp2an 691 . . . 4 ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) < ((1.651) · (1.483))
52324, 181deccl 12105 . . . . 5 42 ∈ ℕ0
524496, 24deccl 12105 . . . . . 6 204 ∈ ℕ0
525 eqid 2801 . . . . . 6 2042 = 2042
526 eqid 2801 . . . . . 6 42 = 42
527 eqid 2801 . . . . . . 7 204 = 204
528496, 24, 24, 527, 277decaddi 12150 . . . . . 6 (204 + 4) = 208
529 2p2e4 11764 . . . . . 6 (2 + 2) = 4
530524, 181, 24, 181, 525, 526, 528, 529decadd 12144 . . . . 5 (2042 + 42) = 2084
531448oveq1i 7149 . . . . . . 7 ((6 + 4) + 2) = (10 + 2)
532 dec10p 12133 . . . . . . 7 (10 + 2) = 12
533531, 532eqtri 2824 . . . . . 6 ((6 + 4) + 2) = 12
5341, 98, 1, 24, 181, 1, 181, 24, 116, 204, 215, 216, 533, 269dpmul 30618 . . . . 5 ((1.6) · (1.4)) = (2.24)
535 8t5e40 12208 . . . . . . 7 (8 · 5) = 40
536158, 256, 535mulcomli 10643 . . . . . 6 (5 · 8) = 40
537 5t3e15 12191 . . . . . 6 (5 · 3) = 15
538158mulid2i 10639 . . . . . 6 (1 · 8) = 8
539430mulid2i 10639 . . . . . . 7 (1 · 3) = 3
540182dec0h 12112 . . . . . . 7 3 = 03
541539, 540eqtri 2824 . . . . . 6 (1 · 3) = 03
542235nn0cni 11901 . . . . . . . . 9 15 ∈ ℂ
543 8p5e13 12173 . . . . . . . . . . 11 (8 + 5) = 13
544158, 256, 543addcomli 10825 . . . . . . . . . 10 (5 + 8) = 13
5451, 54, 73, 245, 269, 182, 544decaddci 12151 . . . . . . . . 9 (15 + 8) = 23
546542, 158, 545addcomli 10825 . . . . . . . 8 (8 + 15) = 23
547546oveq1i 7149 . . . . . . 7 ((8 + 15) + 0) = (23 + 0)
548181, 182deccl 12105 . . . . . . . . 9 23 ∈ ℕ0
549548nn0cni 11901 . . . . . . . 8 23 ∈ ℂ
550549addid1i 10820 . . . . . . 7 (23 + 0) = 23
551547, 550eqtri 2824 . . . . . 6 ((8 + 15) + 0) = 23
552 eqid 2801 . . . . . . 7 40 = 40
553197addid2i 10821 . . . . . . 7 (0 + 2) = 2
55424, 51, 181, 552, 553decaddi 12150 . . . . . 6 (40 + 2) = 42
55554, 1, 73, 182, 51, 181, 182, 182, 536, 537, 538, 541, 551, 554dpmul 30618 . . . . 5 ((5.1) · (8.3)) = (42.33)
556181, 181deccl 12105 . . . . . . 7 22 ∈ ℕ0
557556, 24deccl 12105 . . . . . 6 224 ∈ ℕ0
558 eqid 2801 . . . . . 6 2241 = 2241
559 eqid 2801 . . . . . 6 208 = 208
560 eqid 2801 . . . . . . 7 224 = 224
561 eqid 2801 . . . . . . 7 20 = 20
562 eqid 2801 . . . . . . . 8 22 = 22
563181, 181, 181, 562, 529decaddi 12150 . . . . . . 7 (22 + 2) = 24
564556, 24, 181, 51, 560, 561, 563, 426decadd 12144 . . . . . 6 (224 + 20) = 244
565557, 1, 496, 73, 558, 559, 564, 440decadd 12144 . . . . 5 (2241 + 208) = 2449
566556, 98deccl 12105 . . . . . . . 8 226 ∈ ℕ0
567523, 182deccl 12105 . . . . . . . 8 423 ∈ ℕ0
568 eqid 2801 . . . . . . . 8 2266 = 2266
569 eqid 2801 . . . . . . . 8 4233 = 4233
570 eqid 2801 . . . . . . . . 9 226 = 226
571 eqid 2801 . . . . . . . . 9 423 = 423
572113, 197, 289addcomli 10825 . . . . . . . . . 10 (2 + 4) = 6
573181, 181, 24, 181, 562, 526, 572, 529decadd 12144 . . . . . . . . 9 (22 + 42) = 64
574556, 98, 523, 182, 570, 571, 573, 233decadd 12144 . . . . . . . 8 (226 + 423) = 649
575566, 98, 567, 182, 568, 569, 574, 233decadd 12144 . . . . . . 7 (2266 + 4233) = 6499
576556, 98, 98, 523, 182, 100, 182, 53, 53, 575dpadd3 30617 . . . . . 6 ((22.66) + (42.33)) = (64.99)
577496nn0cni 11901 . . . . . . . . . . 11 20 ∈ ℂ
578181, 51, 181, 561, 553decaddi 12150 . . . . . . . . . . 11 (20 + 2) = 22
579577, 197, 578addcomli 10825 . . . . . . . . . 10 (2 + 20) = 22
580181, 181, 496, 24, 562, 527, 579, 572decadd 12144 . . . . . . . . 9 (22 + 204) = 226
581556, 24, 524, 181, 560, 525, 580, 289decadd 12144 . . . . . . . 8 (224 + 2042) = 2266
582181, 181, 24, 496, 24, 556, 181, 98, 98, 581dpadd3 30617 . . . . . . 7 ((2.24) + (20.42)) = (22.66)
583582oveq1i 7149 . . . . . 6 (((2.24) + (20.42)) + (42.33)) = ((22.66) + (42.33))
584 eqid 2801 . . . . . . . . . 10 51 = 51
5851, 98, 54, 1, 135, 584, 257, 140decadd 12144 . . . . . . . . 9 (16 + 51) = 67
5861, 98, 54, 1, 98, 52, 585dpadd 30616 . . . . . . . 8 ((1.6) + (5.1)) = (6.7)
587 eqid 2801 . . . . . . . . . 10 83 = 83
5881, 24, 73, 182, 268, 587, 440, 302decadd 12144 . . . . . . . . 9 (14 + 83) = 97
5891, 24, 73, 182, 53, 52, 588dpadd 30616 . . . . . . . 8 ((1.4) + (8.3)) = (9.7)
590586, 589oveq12i 7151 . . . . . . 7 (((1.6) + (5.1)) · ((1.4) + (8.3))) = ((6.7) · (9.7))
591 9t6e54 12216 . . . . . . . . 9 (9 · 6) = 54
592196, 110, 591mulcomli 10643 . . . . . . . 8 (6 · 9) = 54
593 7t6e42 12203 . . . . . . . . 9 (7 · 6) = 42
594217, 110, 593mulcomli 10643 . . . . . . . 8 (6 · 7) = 42
595 7t7e49 12204 . . . . . . . 8 (7 · 7) = 49
596 eqid 2801 . . . . . . . . . . 11 63 = 63
597 3p2e5 11780 . . . . . . . . . . 11 (3 + 2) = 5
59898, 182, 24, 181, 596, 526, 448, 597decadd 12144 . . . . . . . . . 10 (63 + 42) = 105
599598oveq1i 7149 . . . . . . . . 9 ((63 + 42) + 4) = (105 + 4)
600 5p4e9 11787 . . . . . . . . . 10 (5 + 4) = 9
601130, 54, 24, 502, 600decaddi 12150 . . . . . . . . 9 (105 + 4) = 109
602599, 601eqtri 2824 . . . . . . . 8 ((63 + 42) + 4) = 109
603 eqid 2801 . . . . . . . . 9 54 = 54
60454, 24, 1, 51, 603, 414, 246, 426decadd 12144 . . . . . . . 8 (54 + 10) = 64
60598, 52, 53, 52, 24, 130, 53, 53, 592, 594, 437, 595, 602, 604dpmul 30618 . . . . . . 7 ((6.7) · (9.7)) = (64.99)
606590, 605eqtri 2824 . . . . . 6 (((1.6) + (5.1)) · ((1.4) + (8.3))) = (64.99)
607576, 583, 6063eqtr4ri 2835 . . . . 5 (((1.6) + (5.1)) · ((1.4) + (8.3))) = (((2.24) + (20.42)) + (42.33))
6081, 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, 607dpmul4 30619 . . . 4 ((1.651) · (1.483)) < (2.449)
60933, 345remulcli 10650 . . . . 5 ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) ∈ ℝ
61043, 350remulcli 10650 . . . . 5 ((1.651) · (1.483)) ∈ ℝ
61124, 399rpdp2cl 30587 . . . . . . . 8 49 ∈ ℝ+
61224, 611rpdp2cl 30587 . . . . . . 7 449 ∈ ℝ+
613181, 612rpdpcl 30608 . . . . . 6 (2.449) ∈ ℝ+
614 rpre 12389 . . . . . 6 ((2.449) ∈ ℝ+ → (2.449) ∈ ℝ)
615613, 614ax-mp 5 . . . . 5 (2.449) ∈ ℝ
616609, 610, 615lttri 10759 . . . 4 ((((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) < ((1.651) · (1.483)) ∧ ((1.651) · (1.483)) < (2.449)) → ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) < (2.449))
617522, 608, 616mp2an 691 . . 3 ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) < (2.449)
618 3pos 11734 . . . 4 0 < 3
619609, 615, 319ltmul2i 11554 . . . 4 (0 < 3 → (((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) < (2.449) ↔ (3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) < (3 · (2.449))))
620618, 619ax-mp 5 . . 3 (((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) < (2.449) ↔ (3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) < (3 · (2.449)))
621617, 620mpbi 233 . 2 (3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) < (3 · (2.449))
622119dp2eq2i 30581 . . . . . . 7 000 = 00
623622, 119eqtri 2824 . . . . . 6 000 = 0
624623oveq2i 7150 . . . . 5 (3.000) = (3.0)
625182dp0u 30606 . . . . 5 (3.0) = 3
626624, 625eqtr2i 2825 . . . 4 3 = (3.000)
627626oveq1i 7149 . . 3 (3 · (2.449)) = ((3.000) · (2.449))
628450, 52deccl 12105 . . . . . . 7 147 ∈ ℕ0
629628, 51deccl 12105 . . . . . 6 1470 ∈ ℕ0
630629nn0cni 11901 . . . . 5 1470 ∈ ℂ
631630addid1i 10820 . . . 4 (1470 + 0) = 1470
632 4t3e12 12188 . . . . . 6 (4 · 3) = 12
633113, 430, 632mulcomli 10643 . . . . 5 (3 · 4) = 12
634197mul02i 10822 . . . . 5 (0 · 2) = 0
635113, 457, 425mulcomli 10643 . . . . 5 (0 · 4) = 00
63651, 51, 1, 181, 424, 300, 153, 553decadd 12144 . . . . . . 7 (0 + 12) = 12
637636oveq1i 7149 . . . . . 6 ((0 + 12) + 0) = (12 + 0)
638281nn0cni 11901 . . . . . . 7 12 ∈ ℂ
639638addid1i 10820 . . . . . 6 (12 + 0) = 12
640637, 639eqtri 2824 . . . . 5 ((0 + 12) + 0) = 12
641182, 51, 181, 24, 51, 1, 181, 51, 431, 633, 634, 635, 640, 140dpmul 30618 . . . 4 ((3.0) · (2.4)) = (7.20)
64251dp0u 30606 . . . . . . 7 (0.0) = 0
643642oveq1i 7149 . . . . . 6 ((0.0) · (4.9)) = (0 · (4.9))
644 dpcl 30596 . . . . . . . . 9 ((4 ∈ ℕ0 ∧ 9 ∈ ℝ) → (4.9) ∈ ℝ)
64524, 4, 644mp2an 691 . . . . . . . 8 (4.9) ∈ ℝ
646645recni 10648 . . . . . . 7 (4.9) ∈ ℂ
647646mul02i 10822 . . . . . 6 (0 · (4.9)) = 0
648643, 647eqtri 2824 . . . . 5 ((0.0) · (4.9)) = 0
649119oveq2i 7150 . . . . . 6 (0.00) = (0.0)
650649, 642eqtri 2824 . . . . 5 (0.00) = 0
651648, 650eqtr4i 2827 . . . 4 ((0.0) · (4.9)) = (0.00)
65252, 181deccl 12105 . . . . . 6 72 ∈ ℕ0
653652, 51deccl 12105 . . . . 5 720 ∈ ℕ0
654 eqid 2801 . . . . 5 7201 = 7201
655 eqid 2801 . . . . 5 147 = 147
656 eqid 2801 . . . . . 6 720 = 720
65752, 181, 224, 263decsuc 12121 . . . . . 6 (72 + 1) = 73
658652, 51, 1, 24, 656, 268, 657, 114decadd 12144 . . . . 5 (720 + 14) = 734
659653, 1, 450, 52, 654, 655, 658, 274decadd 12144 . . . 4 (7201 + 147) = 7348
660642oveq2i 7150 . . . . . . . 8 ((3.0) + (0.0)) = ((3.0) + 0)
661625, 430eqeltri 2889 . . . . . . . . 9 (3.0) ∈ ℂ
662661addid1i 10820 . . . . . . . 8 ((3.0) + 0) = (3.0)
663660, 662eqtri 2824 . . . . . . 7 ((3.0) + (0.0)) = (3.0)
664 eqid 2801 . . . . . . . . 9 49 = 49
665572oveq1i 7149 . . . . . . . . . 10 ((2 + 4) + 1) = (6 + 1)
666665, 140eqtri 2824 . . . . . . . . 9 ((2 + 4) + 1) = 7
667 9p4e13 12179 . . . . . . . . . 10 (9 + 4) = 13
668196, 113, 667addcomli 10825 . . . . . . . . 9 (4 + 9) = 13
669181, 24, 24, 53, 223, 664, 666, 182, 668decaddc 12145 . . . . . . . 8 (24 + 49) = 73
670181, 24, 24, 53, 52, 182, 669dpadd 30616 . . . . . . 7 ((2.4) + (4.9)) = (7.3)
671663, 670oveq12i 7151 . . . . . 6 (((3.0) + (0.0)) · ((2.4) + (4.9))) = ((3.0) · (7.3))
672217, 430, 435mulcomli 10643 . . . . . . 7 (3 · 7) = 21
673 3t3e9 11796 . . . . . . 7 (3 · 3) = 9
674217mul01i 10823 . . . . . . . 8 (7 · 0) = 0
675217, 457, 674mulcomli 10643 . . . . . . 7 (0 · 7) = 0
676430mul01i 10823 . . . . . . . . 9 (3 · 0) = 0
677676, 424eqtri 2824 . . . . . . . 8 (3 · 0) = 00
678430, 457, 677mulcomli 10643 . . . . . . 7 (0 · 3) = 00
679196addid1i 10820 . . . . . . . . . 10 (9 + 0) = 9
680679oveq1i 7149 . . . . . . . . 9 ((9 + 0) + 0) = (9 + 0)
681680, 679, 1883eqtri 2828 . . . . . . . 8 ((9 + 0) + 0) = 09
682196, 457addcomi 10824 . . . . . . . . . 10 (9 + 0) = (0 + 9)
683682oveq1i 7149 . . . . . . . . 9 ((9 + 0) + 0) = ((0 + 9) + 0)
684683eqeq1i 2806 . . . . . . . 8 (((9 + 0) + 0) = 09 ↔ ((0 + 9) + 0) = 09)
685681, 684mpbi 233 . . . . . . 7 ((0 + 9) + 0) = 09
686181, 1, 51, 438, 192decaddi 12150 . . . . . . 7 (21 + 0) = 21
687182, 51, 52, 182, 51, 51, 53, 51, 672, 673, 675, 678, 685, 686dpmul 30618 . . . . . 6 ((3.0) · (7.3)) = (21.90)
688671, 687eqtri 2824 . . . . 5 (((3.0) + (0.0)) · ((2.4) + (4.9))) = (21.90)
689650oveq2i 7150 . . . . . 6 (((7.20) + (14.70)) + (0.00)) = (((7.20) + (14.70)) + 0)
690318, 2pm3.2i 474 . . . . . . . . . . 11 (2 ∈ ℝ ∧ 0 ∈ ℝ)
691 dp2cl 30585 . . . . . . . . . . 11 ((2 ∈ ℝ ∧ 0 ∈ ℝ) → 20 ∈ ℝ)
692690, 691ax-mp 5 . . . . . . . . . 10 20 ∈ ℝ
693 dpcl 30596 . . . . . . . . . 10 ((7 ∈ ℕ020 ∈ ℝ) → (7.20) ∈ ℝ)
69452, 692, 693mp2an 691 . . . . . . . . 9 (7.20) ∈ ℝ
695694recni 10648 . . . . . . . 8 (7.20) ∈ ℂ
6963, 2pm3.2i 474 . . . . . . . . . . 11 (7 ∈ ℝ ∧ 0 ∈ ℝ)
697 dp2cl 30585 . . . . . . . . . . 11 ((7 ∈ ℝ ∧ 0 ∈ ℝ) → 70 ∈ ℝ)
698696, 697ax-mp 5 . . . . . . . . . 10 70 ∈ ℝ
699 dpcl 30596 . . . . . . . . . 10 ((14 ∈ ℕ070 ∈ ℝ) → (14.70) ∈ ℝ)
700450, 698, 699mp2an 691 . . . . . . . . 9 (14.70) ∈ ℝ
701700recni 10648 . . . . . . . 8 (14.70) ∈ ℂ
702695, 701addcli 10640 . . . . . . 7 ((7.20) + (14.70)) ∈ ℂ
703702addid1i 10820 . . . . . 6 (((7.20) + (14.70)) + 0) = ((7.20) + (14.70))
704 eqid 2801 . . . . . . . 8 1470 = 1470
705450nn0cni 11901 . . . . . . . . . 10 14 ∈ ℂ
706705, 217, 270addcomli 10825 . . . . . . . . 9 (7 + 14) = 21
707 7p2e9 11790 . . . . . . . . . 10 (7 + 2) = 9
708217, 197, 707addcomli 10825 . . . . . . . . 9 (2 + 7) = 9
70952, 181, 450, 52, 263, 655, 706, 708decadd 12144 . . . . . . . 8 (72 + 147) = 219
710 00id 10808 . . . . . . . 8 (0 + 0) = 0
711652, 51, 628, 51, 656, 704, 709, 710decadd 12144 . . . . . . 7 (720 + 1470) = 2190
71252, 181, 51, 450, 52, 293, 51, 53, 51, 711dpadd3 30617 . . . . . 6 ((7.20) + (14.70)) = (21.90)
713689, 703, 7123eqtri 2828 . . . . 5 (((7.20) + (14.70)) + (0.00)) = (21.90)
714688, 713eqtr4i 2827 . . . 4 (((3.0) + (0.0)) · ((2.4) + (4.9))) = (((7.20) + (14.70)) + (0.00))
715182, 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, 714dpmul4 30619 . . 3 ((3.000) · (2.449)) < (7.348)
716627, 715eqbrtri 5054 . 2 (3 · (2.449)) < (7.348)
717319, 609remulcli 10650 . . 3 (3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) ∈ ℝ
718319, 615remulcli 10650 . . 3 (3 · (2.449)) ∈ ℝ
719 nnrp 12392 . . . . . . . 8 (8 ∈ ℕ → 8 ∈ ℝ+)
72063, 719ax-mp 5 . . . . . . 7 8 ∈ ℝ+
72124, 720rpdp2cl 30587 . . . . . 6 48 ∈ ℝ+
722182, 721rpdp2cl 30587 . . . . 5 348 ∈ ℝ+
72352, 722rpdpcl 30608 . . . 4 (7.348) ∈ ℝ+
724 rpre 12389 . . . 4 ((7.348) ∈ ℝ+ → (7.348) ∈ ℝ)
725723, 724ax-mp 5 . . 3 (7.348) ∈ ℝ
726717, 718, 725lttri 10759 . 2 (((3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) < (3 · (2.449)) ∧ (3 · (2.449)) < (7.348)) → (3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) < (7.348))
727621, 716, 726mp2an 691 1 (3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) < (7.348)
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399   = wceq 1538  wcel 2112   class class class wbr 5033  (class class class)co 7139  cc 10528  cr 10529  0cc0 10530  1c1 10531   + caddc 10533   · cmul 10535   < clt 10668  cle 10669  cn 11629  2c2 11684  3c3 11685  4c4 11686  5c5 11687  6c6 11688  7c7 11689  8c8 11690  9c9 11691  0cn0 11889  cdc 12090  +crp 12381  cexp 13429  cdp2 30576  .cdp 30593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-rp 12382  df-seq 13369  df-exp 13430  df-dp2 30577  df-dp 30594
This theorem is referenced by:  hgt750leme  32037
  Copyright terms: Public domain W3C validator