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 31052
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 11571 . . . . . . . . . 10 1 ∈ ℕ0
2 0re 10324 . . . . . . . . . . . 12 0 ∈ ℝ
3 7re 11383 . . . . . . . . . . . . . 14 7 ∈ ℝ
4 9re 11387 . . . . . . . . . . . . . . . 16 9 ∈ ℝ
5 5re 11379 . . . . . . . . . . . . . . . . . . . 20 5 ∈ ℝ
65, 5pm3.2i 458 . . . . . . . . . . . . . . . . . . 19 (5 ∈ ℝ ∧ 5 ∈ ℝ)
7 dp2cl 29910 . . . . . . . . . . . . . . . . . . 19 ((5 ∈ ℝ ∧ 5 ∈ ℝ) → 55 ∈ ℝ)
86, 7ax-mp 5 . . . . . . . . . . . . . . . . . 18 55 ∈ ℝ
94, 8pm3.2i 458 . . . . . . . . . . . . . . . . 17 (9 ∈ ℝ ∧ 55 ∈ ℝ)
10 dp2cl 29910 . . . . . . . . . . . . . . . . 17 ((9 ∈ ℝ ∧ 55 ∈ ℝ) → 955 ∈ ℝ)
119, 10ax-mp 5 . . . . . . . . . . . . . . . 16 955 ∈ ℝ
124, 11pm3.2i 458 . . . . . . . . . . . . . . 15 (9 ∈ ℝ ∧ 955 ∈ ℝ)
13 dp2cl 29910 . . . . . . . . . . . . . . 15 ((9 ∈ ℝ ∧ 955 ∈ ℝ) → 9955 ∈ ℝ)
1412, 13ax-mp 5 . . . . . . . . . . . . . 14 9955 ∈ ℝ
153, 14pm3.2i 458 . . . . . . . . . . . . 13 (7 ∈ ℝ ∧ 9955 ∈ ℝ)
16 dp2cl 29910 . . . . . . . . . . . . 13 ((7 ∈ ℝ ∧ 9955 ∈ ℝ) → 79955 ∈ ℝ)
1715, 16ax-mp 5 . . . . . . . . . . . 12 79955 ∈ ℝ
182, 17pm3.2i 458 . . . . . . . . . . 11 (0 ∈ ℝ ∧ 79955 ∈ ℝ)
19 dp2cl 29910 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ 79955 ∈ ℝ) → 079955 ∈ ℝ)
2018, 19ax-mp 5 . . . . . . . . . 10 079955 ∈ ℝ
21 dpcl 29921 . . . . . . . . . 10 ((1 ∈ ℕ0079955 ∈ ℝ) → (1.079955) ∈ ℝ)
221, 20, 21mp2an 675 . . . . . . . . 9 (1.079955) ∈ ℝ
2322resqcli 13168 . . . . . . . 8 ((1.079955)↑2) ∈ ℝ
24 4nn0 11574 . . . . . . . . . . 11 4 ∈ ℕ0
25 4nn 11460 . . . . . . . . . . . . 13 4 ∈ ℕ
26 nnrp 12052 . . . . . . . . . . . . 13 (4 ∈ ℕ → 4 ∈ ℝ+)
2725, 26ax-mp 5 . . . . . . . . . . . 12 4 ∈ ℝ+
281, 27rpdp2cl 29912 . . . . . . . . . . 11 14 ∈ ℝ+
2924, 28rpdp2cl 29912 . . . . . . . . . 10 414 ∈ ℝ+
301, 29rpdpcl 29933 . . . . . . . . 9 (1.414) ∈ ℝ+
31 rpre 12049 . . . . . . . . 9 ((1.414) ∈ ℝ+ → (1.414) ∈ ℝ)
3230, 31ax-mp 5 . . . . . . . 8 (1.414) ∈ ℝ
3323, 32remulcli 10338 . . . . . . 7 (((1.079955)↑2) · (1.414)) ∈ ℝ
34 6re 11381 . . . . . . . . . 10 6 ∈ ℝ
35 1re 10322 . . . . . . . . . . . 12 1 ∈ ℝ
365, 35pm3.2i 458 . . . . . . . . . . 11 (5 ∈ ℝ ∧ 1 ∈ ℝ)
37 dp2cl 29910 . . . . . . . . . . 11 ((5 ∈ ℝ ∧ 1 ∈ ℝ) → 51 ∈ ℝ)
3836, 37ax-mp 5 . . . . . . . . . 10 51 ∈ ℝ
3934, 38pm3.2i 458 . . . . . . . . 9 (6 ∈ ℝ ∧ 51 ∈ ℝ)
40 dp2cl 29910 . . . . . . . . 9 ((6 ∈ ℝ ∧ 51 ∈ ℝ) → 651 ∈ ℝ)
4139, 40ax-mp 5 . . . . . . . 8 651 ∈ ℝ
42 dpcl 29921 . . . . . . . 8 ((1 ∈ ℕ0651 ∈ ℝ) → (1.651) ∈ ℝ)
431, 41, 42mp2an 675 . . . . . . 7 (1.651) ∈ ℝ
4433, 43pm3.2i 458 . . . . . 6 ((((1.079955)↑2) · (1.414)) ∈ ℝ ∧ (1.651) ∈ ℝ)
4522sqge0i 13170 . . . . . . . 8 0 ≤ ((1.079955)↑2)
46 rpgt0 12054 . . . . . . . . . 10 ((1.414) ∈ ℝ+ → 0 < (1.414))
4730, 46ax-mp 5 . . . . . . . . 9 0 < (1.414)
482, 32, 47ltleii 10442 . . . . . . . 8 0 ≤ (1.414)
4923, 32mulge0i 10857 . . . . . . . 8 ((0 ≤ ((1.079955)↑2) ∧ 0 ≤ (1.414)) → 0 ≤ (((1.079955)↑2) · (1.414)))
5045, 48, 49mp2an 675 . . . . . . 7 0 ≤ (((1.079955)↑2) · (1.414))
51 0nn0 11570 . . . . . . . . . . . . 13 0 ∈ ℕ0
52 7nn0 11577 . . . . . . . . . . . . . 14 7 ∈ ℕ0
53 9nn0 11579 . . . . . . . . . . . . . . 15 9 ∈ ℕ0
54 5nn0 11575 . . . . . . . . . . . . . . . . 17 5 ∈ ℕ0
55 5nn 11461 . . . . . . . . . . . . . . . . . 18 5 ∈ ℕ
56 nnrp 12052 . . . . . . . . . . . . . . . . . 18 (5 ∈ ℕ → 5 ∈ ℝ+)
5755, 56ax-mp 5 . . . . . . . . . . . . . . . . 17 5 ∈ ℝ+
5854, 57rpdp2cl 29912 . . . . . . . . . . . . . . . 16 55 ∈ ℝ+
5953, 58rpdp2cl 29912 . . . . . . . . . . . . . . 15 955 ∈ ℝ+
6053, 59rpdp2cl 29912 . . . . . . . . . . . . . 14 9955 ∈ ℝ+
6152, 60rpdp2cl 29912 . . . . . . . . . . . . 13 79955 ∈ ℝ+
6251, 61rpdp2cl 29912 . . . . . . . . . . . 12 079955 ∈ ℝ+
63 8nn 11464 . . . . . . . . . . . . . 14 8 ∈ ℕ
6463rpdp2cl2 29913 . . . . . . . . . . . . 13 80 ∈ ℝ+
6551, 64rpdp2cl 29912 . . . . . . . . . . . 12 080 ∈ ℝ+
66 9lt10 11886 . . . . . . . . . . . . . . . 16 9 < 10
67 5lt10 11890 . . . . . . . . . . . . . . . . . 18 5 < 10
6854, 57, 67, 67dp2lt10 29914 . . . . . . . . . . . . . . . . 17 55 < 10
6953, 58, 66, 68dp2lt10 29914 . . . . . . . . . . . . . . . 16 955 < 10
7053, 59, 66, 69dp2lt10 29914 . . . . . . . . . . . . . . 15 9955 < 10
71 7p1e8 11436 . . . . . . . . . . . . . . 15 (7 + 1) = 8
7252, 60, 70, 71dp2ltsuc 29916 . . . . . . . . . . . . . 14 79955 < 8
73 8nn0 11578 . . . . . . . . . . . . . . 15 8 ∈ ℕ0
7473dp20u 29908 . . . . . . . . . . . . . 14 80 = 8
7572, 74breqtrri 4867 . . . . . . . . . . . . 13 79955 < 80
7651, 61, 64, 75dp2lt 29915 . . . . . . . . . . . 12 079955 < 080
771, 62, 65, 76dplt 29934 . . . . . . . . . . 11 (1.079955) < (1.080)
781, 62rpdpcl 29933 . . . . . . . . . . . . 13 (1.079955) ∈ ℝ+
79 rpge0 12055 . . . . . . . . . . . . 13 ((1.079955) ∈ ℝ+ → 0 ≤ (1.079955))
8078, 79ax-mp 5 . . . . . . . . . . . 12 0 ≤ (1.079955)
811, 65rpdpcl 29933 . . . . . . . . . . . . 13 (1.080) ∈ ℝ+
82 rpge0 12055 . . . . . . . . . . . . 13 ((1.080) ∈ ℝ+ → 0 ≤ (1.080))
8381, 82ax-mp 5 . . . . . . . . . . . 12 0 ≤ (1.080)
84 8re 11385 . . . . . . . . . . . . . . . . . 18 8 ∈ ℝ
8584, 2pm3.2i 458 . . . . . . . . . . . . . . . . 17 (8 ∈ ℝ ∧ 0 ∈ ℝ)
86 dp2cl 29910 . . . . . . . . . . . . . . . . 17 ((8 ∈ ℝ ∧ 0 ∈ ℝ) → 80 ∈ ℝ)
8785, 86ax-mp 5 . . . . . . . . . . . . . . . 16 80 ∈ ℝ
882, 87pm3.2i 458 . . . . . . . . . . . . . . 15 (0 ∈ ℝ ∧ 80 ∈ ℝ)
89 dp2cl 29910 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ 80 ∈ ℝ) → 080 ∈ ℝ)
9088, 89ax-mp 5 . . . . . . . . . . . . . 14 080 ∈ ℝ
91 dpcl 29921 . . . . . . . . . . . . . 14 ((1 ∈ ℕ0080 ∈ ℝ) → (1.080) ∈ ℝ)
921, 90, 91mp2an 675 . . . . . . . . . . . . 13 (1.080) ∈ ℝ
9322, 92lt2sqi 13171 . . . . . . . . . . . 12 ((0 ≤ (1.079955) ∧ 0 ≤ (1.080)) → ((1.079955) < (1.080) ↔ ((1.079955)↑2) < ((1.080)↑2)))
9480, 83, 93mp2an 675 . . . . . . . . . . 11 ((1.079955) < (1.080) ↔ ((1.079955)↑2) < ((1.080)↑2))
9577, 94mpbi 221 . . . . . . . . . 10 ((1.079955)↑2) < ((1.080)↑2)
9692recni 10336 . . . . . . . . . . . 12 (1.080) ∈ ℂ
9796sqvali 13162 . . . . . . . . . . 11 ((1.080)↑2) = ((1.080) · (1.080))
98 6nn0 11576 . . . . . . . . . . . . 13 6 ∈ ℕ0
991, 98deccl 11770 . . . . . . . . . . . 12 16 ∈ ℕ0
10098, 24deccl 11770 . . . . . . . . . . . 12 64 ∈ ℕ0
101 4lt10 11891 . . . . . . . . . . . 12 4 < 10
102 10pos 11772 . . . . . . . . . . . 12 0 < 10
10399, 51deccl 11770 . . . . . . . . . . . . 13 160 ∈ ℕ0
104 eqid 2805 . . . . . . . . . . . . 13 1600 = 1600
105 eqid 2805 . . . . . . . . . . . . 13 64 = 64
106 eqid 2805 . . . . . . . . . . . . . 14 160 = 160
10798dec0h 11777 . . . . . . . . . . . . . 14 6 = 06
10899nn0cni 11567 . . . . . . . . . . . . . . 15 16 ∈ ℂ
109108addid1i 10505 . . . . . . . . . . . . . 14 (16 + 0) = 16
110 6cn 11382 . . . . . . . . . . . . . . 15 6 ∈ ℂ
111110addid2i 10506 . . . . . . . . . . . . . 14 (0 + 6) = 6
11299, 51, 51, 98, 106, 107, 109, 111decadd 11809 . . . . . . . . . . . . 13 (160 + 6) = 166
113 4cn 11378 . . . . . . . . . . . . . 14 4 ∈ ℂ
114113addid2i 10506 . . . . . . . . . . . . 13 (0 + 4) = 4
115103, 51, 98, 24, 104, 105, 112, 114decadd 11809 . . . . . . . . . . . 12 (1600 + 64) = 1664
116 1t1e1 11449 . . . . . . . . . . . . 13 (1 · 1) = 1
1171dp0u 29931 . . . . . . . . . . . . . 14 (1.0) = 1
118117, 117oveq12i 6883 . . . . . . . . . . . . 13 ((1.0) · (1.0)) = (1 · 1)
11951dp20u 29908 . . . . . . . . . . . . . . 15 00 = 0
120119oveq2i 6882 . . . . . . . . . . . . . 14 (1.00) = (1.0)
121120, 117eqtri 2827 . . . . . . . . . . . . 13 (1.00) = 1
122116, 118, 1213eqtr4i 2837 . . . . . . . . . . . 12 ((1.0) · (1.0)) = (1.00)
123 8t8e64 11876 . . . . . . . . . . . . 13 (8 · 8) = 64
12473dp0u 29931 . . . . . . . . . . . . . 14 (8.0) = 8
125124, 124oveq12i 6883 . . . . . . . . . . . . 13 ((8.0) · (8.0)) = (8 · 8)
126119oveq2i 6882 . . . . . . . . . . . . . 14 (64.00) = (64.0)
127100dp0u 29931 . . . . . . . . . . . . . 14 (64.0) = 64
128126, 127eqtri 2827 . . . . . . . . . . . . 13 (64.00) = 64
129123, 125, 1283eqtr4i 2837 . . . . . . . . . . . 12 ((8.0) · (8.0)) = (64.00)
130 10nn0 11773 . . . . . . . . . . . . . 14 10 ∈ ℕ0
131130, 51deccl 11770 . . . . . . . . . . . . 13 100 ∈ ℕ0
132 eqid 2805 . . . . . . . . . . . . 13 1001 = 1001
133 eqid 2805 . . . . . . . . . . . . 13 166 = 166
134 eqid 2805 . . . . . . . . . . . . . 14 100 = 100
135 eqid 2805 . . . . . . . . . . . . . 14 16 = 16
136 dec10p 11798 . . . . . . . . . . . . . 14 (10 + 1) = 11
137130, 51, 1, 98, 134, 135, 136, 111decadd 11809 . . . . . . . . . . . . 13 (100 + 16) = 116
138 ax-1cn 10276 . . . . . . . . . . . . . . 15 1 ∈ ℂ
139138, 110addcomi 10509 . . . . . . . . . . . . . 14 (1 + 6) = (6 + 1)
140 6p1e7 11435 . . . . . . . . . . . . . 14 (6 + 1) = 7
141139, 140eqtri 2827 . . . . . . . . . . . . 13 (1 + 6) = 7
142131, 1, 99, 98, 132, 133, 137, 141decadd 11809 . . . . . . . . . . . 12 (1001 + 166) = 1167
143 eqid 2805 . . . . . . . . . . . . . 14 17 = 17
144141oveq1i 6881 . . . . . . . . . . . . . . 15 ((1 + 6) + 1) = (7 + 1)
145144, 71eqtri 2827 . . . . . . . . . . . . . 14 ((1 + 6) + 1) = 8
146 7p4e11 11831 . . . . . . . . . . . . . 14 (7 + 4) = 11
1471, 52, 98, 24, 143, 105, 145, 1, 146decaddc 11810 . . . . . . . . . . . . 13 (17 + 64) = 81
148119oveq2i 6882 . . . . . . . . . . . . . . . . 17 (16.00) = (16.0)
14999dp0u 29931 . . . . . . . . . . . . . . . . 17 (16.0) = 16
150148, 149eqtri 2827 . . . . . . . . . . . . . . . 16 (16.00) = 16
151121, 150oveq12i 6883 . . . . . . . . . . . . . . 15 ((1.00) + (16.00)) = (1 + 16)
1521dec0h 11777 . . . . . . . . . . . . . . . 16 1 = 01
153138addid2i 10506 . . . . . . . . . . . . . . . 16 (0 + 1) = 1
15451, 1, 1, 98, 152, 135, 153, 141decadd 11809 . . . . . . . . . . . . . . 15 (1 + 16) = 17
155151, 154eqtri 2827 . . . . . . . . . . . . . 14 ((1.00) + (16.00)) = 17
156155, 128oveq12i 6883 . . . . . . . . . . . . 13 (((1.00) + (16.00)) + (64.00)) = (17 + 64)
157117, 124oveq12i 6883 . . . . . . . . . . . . . . . 16 ((1.0) + (8.0)) = (1 + 8)
158 8cn 11386 . . . . . . . . . . . . . . . . 17 8 ∈ ℂ
159138, 158addcomi 10509 . . . . . . . . . . . . . . . 16 (1 + 8) = (8 + 1)
160 8p1e9 11437 . . . . . . . . . . . . . . . 16 (8 + 1) = 9
161157, 159, 1603eqtri 2831 . . . . . . . . . . . . . . 15 ((1.0) + (8.0)) = 9
162161, 161oveq12i 6883 . . . . . . . . . . . . . 14 (((1.0) + (8.0)) · ((1.0) + (8.0))) = (9 · 9)
163 9t9e81 11884 . . . . . . . . . . . . . 14 (9 · 9) = 81
164162, 163eqtri 2827 . . . . . . . . . . . . 13 (((1.0) + (8.0)) · ((1.0) + (8.0))) = 81
165147, 156, 1643eqtr4ri 2838 . . . . . . . . . . . 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 29944 . . . . . . . . . . 11 ((1.080) · (1.080)) < (1.167)
16797, 166eqbrtri 4861 . . . . . . . . . 10 ((1.080)↑2) < (1.167)
16892resqcli 13168 . . . . . . . . . . 11 ((1.080)↑2) ∈ ℝ
16934, 3pm3.2i 458 . . . . . . . . . . . . . . 15 (6 ∈ ℝ ∧ 7 ∈ ℝ)
170 dp2cl 29910 . . . . . . . . . . . . . . 15 ((6 ∈ ℝ ∧ 7 ∈ ℝ) → 67 ∈ ℝ)
171169, 170ax-mp 5 . . . . . . . . . . . . . 14 67 ∈ ℝ
17235, 171pm3.2i 458 . . . . . . . . . . . . 13 (1 ∈ ℝ ∧ 67 ∈ ℝ)
173 dp2cl 29910 . . . . . . . . . . . . 13 ((1 ∈ ℝ ∧ 67 ∈ ℝ) → 167 ∈ ℝ)
174172, 173ax-mp 5 . . . . . . . . . . . 12 167 ∈ ℝ
175 dpcl 29921 . . . . . . . . . . . 12 ((1 ∈ ℕ0167 ∈ ℝ) → (1.167) ∈ ℝ)
1761, 174, 175mp2an 675 . . . . . . . . . . 11 (1.167) ∈ ℝ
17723, 168, 176lttri 10445 . . . . . . . . . 10 ((((1.079955)↑2) < ((1.080)↑2) ∧ ((1.080)↑2) < (1.167)) → ((1.079955)↑2) < (1.167))
17895, 167, 177mp2an 675 . . . . . . . . 9 ((1.079955)↑2) < (1.167)
17923, 176, 32, 47ltmul1ii 11234 . . . . . . . . 9 (((1.079955)↑2) < (1.167) ↔ (((1.079955)↑2) · (1.414)) < ((1.167) · (1.414)))
180178, 179mpbi 221 . . . . . . . 8 (((1.079955)↑2) · (1.414)) < ((1.167) · (1.414))
181 2nn0 11572 . . . . . . . . 9 2 ∈ ℕ0
182 3nn0 11573 . . . . . . . . 9 3 ∈ ℕ0
183 1lt10 11894 . . . . . . . . 9 1 < 10
184 3lt10 11892 . . . . . . . . 9 3 < 10
185 8lt10 11887 . . . . . . . . 9 8 < 10
186130, 53deccl 11770 . . . . . . . . . 10 109 ∈ ℕ0
187 eqid 2805 . . . . . . . . . 10 1092 = 1092
18853dec0h 11777 . . . . . . . . . 10 9 = 09
189186nn0cni 11567 . . . . . . . . . . . 12 109 ∈ ℂ
190189addid1i 10505 . . . . . . . . . . 11 (109 + 0) = 109
191 dec10p 11798 . . . . . . . . . . . 12 (10 + 0) = 10
192138addid1i 10505 . . . . . . . . . . . 12 (1 + 0) = 1
1931, 51, 51, 1, 191, 152, 192, 153decadd 11809 . . . . . . . . . . 11 ((10 + 0) + 1) = 11
194 9p1e10 11757 . . . . . . . . . . 11 (9 + 1) = 10
195130, 53, 51, 1, 190, 152, 193, 51, 194decaddc 11810 . . . . . . . . . 10 ((109 + 0) + 1) = 110
196 9cn 11388 . . . . . . . . . . . 12 9 ∈ ℂ
197 2cn 11371 . . . . . . . . . . . 12 2 ∈ ℂ
198196, 197addcomi 10509 . . . . . . . . . . 11 (9 + 2) = (2 + 9)
199 9p2e11 11842 . . . . . . . . . . 11 (9 + 2) = 11
200198, 199eqtr3i 2829 . . . . . . . . . 10 (2 + 9) = 11
201186, 181, 51, 53, 187, 188, 195, 1, 200decaddc 11810 . . . . . . . . 9 (1092 + 9) = 1101
202113, 138mulcomi 10330 . . . . . . . . . . 11 (4 · 1) = (1 · 4)
203113mulid1i 10326 . . . . . . . . . . 11 (4 · 1) = 4
204202, 203eqtr3i 2829 . . . . . . . . . 10 (1 · 4) = 4
20524dec0h 11777 . . . . . . . . . . 11 4 = 04
206203, 202, 2053eqtr3i 2835 . . . . . . . . . 10 (1 · 4) = 04
207138, 113addcli 10328 . . . . . . . . . . . . 13 (1 + 4) ∈ ℂ
208207addid1i 10505 . . . . . . . . . . . 12 ((1 + 4) + 0) = (1 + 4)
209113, 138addcomi 10509 . . . . . . . . . . . 12 (4 + 1) = (1 + 4)
210 4p1e5 11433 . . . . . . . . . . . 12 (4 + 1) = 5
211208, 209, 2103eqtr2i 2833 . . . . . . . . . . 11 ((1 + 4) + 0) = 5
21254dec0h 11777 . . . . . . . . . . 11 5 = 05
213211, 212eqtri 2827 . . . . . . . . . 10 ((1 + 4) + 0) = 05
2141, 1, 1, 24, 51, 51, 54, 24, 116, 204, 116, 206, 213, 192dpmul 29943 . . . . . . . . 9 ((1.1) · (1.4)) = (1.54)
215110mulid1i 10326 . . . . . . . . . 10 (6 · 1) = 6
216 6t4e24 11861 . . . . . . . . . 10 (6 · 4) = 24
217 7cn 11384 . . . . . . . . . . 11 7 ∈ ℂ
218217mulid1i 10326 . . . . . . . . . 10 (7 · 1) = 7
219 7t4e28 11866 . . . . . . . . . 10 (7 · 4) = 28
220181, 24deccl 11770 . . . . . . . . . . . . . . 15 24 ∈ ℕ0
221220nn0cni 11567 . . . . . . . . . . . . . 14 24 ∈ ℂ
222221, 217addcomi 10509 . . . . . . . . . . . . 13 (24 + 7) = (7 + 24)
223 eqid 2805 . . . . . . . . . . . . . 14 24 = 24
224 2p1e3 11430 . . . . . . . . . . . . . 14 (2 + 1) = 3
225217, 113, 146addcomli 10510 . . . . . . . . . . . . . 14 (4 + 7) = 11
226181, 24, 52, 223, 224, 1, 225decaddci 11816 . . . . . . . . . . . . 13 (24 + 7) = 31
227222, 226eqtr3i 2829 . . . . . . . . . . . 12 (7 + 24) = 31
228227oveq1i 6881 . . . . . . . . . . 11 ((7 + 24) + 2) = (31 + 2)
229 eqid 2805 . . . . . . . . . . . 12 31 = 31
230197, 138, 224addcomli 10510 . . . . . . . . . . . 12 (1 + 2) = 3
231182, 1, 181, 229, 230decaddi 11815 . . . . . . . . . . 11 (31 + 2) = 33
232228, 231eqtri 2827 . . . . . . . . . 10 ((7 + 24) + 2) = 33
233 6p3e9 11447 . . . . . . . . . 10 (6 + 3) = 9
23498, 52, 1, 24, 181, 182, 182, 73, 215, 216, 218, 219, 232, 233dpmul 29943 . . . . . . . . 9 ((6.7) · (1.4)) = (9.38)
2351, 54deccl 11770 . . . . . . . . . . 11 15 ∈ ℕ0
236235, 24deccl 11770 . . . . . . . . . 10 154 ∈ ℕ0
23751, 1deccl 11770 . . . . . . . . . . 11 01 ∈ ℕ0
238237, 1deccl 11770 . . . . . . . . . 10 011 ∈ ℕ0
239 eqid 2805 . . . . . . . . . 10 1541 = 1541
240152deceq1i 11762 . . . . . . . . . . 11 11 = 011
241240deceq1i 11762 . . . . . . . . . 10 110 = 0110
242 eqid 2805 . . . . . . . . . . 11 154 = 154
243 eqid 2805 . . . . . . . . . . 11 011 = 011
244152oveq2i 6882 . . . . . . . . . . . 12 (15 + 1) = (15 + 01)
245 eqid 2805 . . . . . . . . . . . . 13 15 = 15
246 5p1e6 11434 . . . . . . . . . . . . 13 (5 + 1) = 6
2471, 54, 1, 245, 246decaddi 11815 . . . . . . . . . . . 12 (15 + 1) = 16
248244, 247eqtr3i 2829 . . . . . . . . . . 11 (15 + 01) = 16
249235, 24, 237, 1, 242, 243, 248, 210decadd 11809 . . . . . . . . . 10 (154 + 011) = 165
250236, 1, 238, 51, 239, 241, 249, 192decadd 11809 . . . . . . . . 9 (1541 + 110) = 1651
251 7t2e14 11864 . . . . . . . . . . 11 (7 · 2) = 14
252 8t7e56 11875 . . . . . . . . . . . 12 (8 · 7) = 56
253158, 217, 252mulcomli 10331 . . . . . . . . . . 11 (7 · 8) = 56
254 8t2e16 11870 . . . . . . . . . . 11 (8 · 2) = 16
255 eqid 2805 . . . . . . . . . . . . . 14 56 = 56
256 5cn 11380 . . . . . . . . . . . . . . . . 17 5 ∈ ℂ
257256, 138, 246addcomli 10510 . . . . . . . . . . . . . . . 16 (1 + 5) = 6
258257oveq1i 6881 . . . . . . . . . . . . . . 15 ((1 + 5) + 1) = (6 + 1)
259258, 140eqtri 2827 . . . . . . . . . . . . . 14 ((1 + 5) + 1) = 7
260 6p6e12 11829 . . . . . . . . . . . . . 14 (6 + 6) = 12
2611, 98, 54, 98, 135, 255, 259, 181, 260decaddc 11810 . . . . . . . . . . . . 13 (16 + 56) = 72
262261oveq1i 6881 . . . . . . . . . . . 12 ((16 + 56) + 6) = (72 + 6)
263 eqid 2805 . . . . . . . . . . . . 13 72 = 72
264 6p2e8 11446 . . . . . . . . . . . . . 14 (6 + 2) = 8
265110, 197, 264addcomli 10510 . . . . . . . . . . . . 13 (2 + 6) = 8
26652, 181, 98, 263, 265decaddi 11815 . . . . . . . . . . . 12 (72 + 6) = 78
267262, 266eqtri 2827 . . . . . . . . . . 11 ((16 + 56) + 6) = 78
268 eqid 2805 . . . . . . . . . . . 12 14 = 14
269 1p1e2 11413 . . . . . . . . . . . 12 (1 + 1) = 2
2701, 24, 52, 268, 269, 1, 225decaddci 11816 . . . . . . . . . . 11 (14 + 7) = 21
27152, 73, 181, 73, 98, 52, 73, 24, 251, 253, 254, 123, 267, 270dpmul 29943 . . . . . . . . . 10 ((7.8) · (2.8)) = (21.84)
272 eqid 2805 . . . . . . . . . . . . 13 11 = 11
273 eqid 2805 . . . . . . . . . . . . 13 67 = 67
274217, 138, 71addcomli 10510 . . . . . . . . . . . . 13 (1 + 7) = 8
2751, 1, 98, 52, 272, 273, 141, 274decadd 11809 . . . . . . . . . . . 12 (11 + 67) = 78
2761, 1, 98, 52, 52, 73, 275dpadd 29941 . . . . . . . . . . 11 ((1.1) + (6.7)) = (7.8)
277 4p4e8 11442 . . . . . . . . . . . . 13 (4 + 4) = 8
2781, 24, 1, 24, 268, 268, 269, 277decadd 11809 . . . . . . . . . . . 12 (14 + 14) = 28
2791, 24, 1, 24, 181, 73, 278dpadd 29941 . . . . . . . . . . 11 ((1.4) + (1.4)) = (2.8)
280276, 279oveq12i 6883 . . . . . . . . . 10 (((1.1) + (6.7)) · ((1.4) + (1.4))) = ((7.8) · (2.8))
2811, 181deccl 11770 . . . . . . . . . . . . 13 12 ∈ ℕ0
282 eqid 2805 . . . . . . . . . . . . . . 15 109 = 109
283130nn0cni 11567 . . . . . . . . . . . . . . . . 17 10 ∈ ℂ
284283, 138, 136addcomli 10510 . . . . . . . . . . . . . . . 16 (1 + 10) = 11
2851, 1, 269, 284decsuc 11786 . . . . . . . . . . . . . . 15 ((1 + 10) + 1) = 12
286 9p5e14 11845 . . . . . . . . . . . . . . . 16 (9 + 5) = 14
287196, 256, 286addcomli 10510 . . . . . . . . . . . . . . 15 (5 + 9) = 14
2881, 54, 130, 53, 245, 282, 285, 24, 287decaddc 11810 . . . . . . . . . . . . . 14 (15 + 109) = 124
289 4p2e6 11440 . . . . . . . . . . . . . 14 (4 + 2) = 6
290235, 24, 186, 181, 242, 187, 288, 289decadd 11809 . . . . . . . . . . . . 13 (154 + 1092) = 1246
2911, 54, 24, 130, 53, 281, 181, 24, 98, 290dpadd3 29942 . . . . . . . . . . . 12 ((1.54) + (10.92)) = (12.46)
292291oveq1i 6881 . . . . . . . . . . 11 (((1.54) + (10.92)) + (9.38)) = ((12.46) + (9.38))
293181, 1deccl 11770 . . . . . . . . . . . 12 21 ∈ ℕ0
294281, 24deccl 11770 . . . . . . . . . . . . 13 124 ∈ ℕ0
29553, 182deccl 11770 . . . . . . . . . . . . 13 93 ∈ ℕ0
296 eqid 2805 . . . . . . . . . . . . 13 1246 = 1246
297 eqid 2805 . . . . . . . . . . . . 13 938 = 938
298 eqid 2805 . . . . . . . . . . . . . . 15 124 = 124
299 eqid 2805 . . . . . . . . . . . . . . 15 93 = 93
300 eqid 2805 . . . . . . . . . . . . . . . 16 12 = 12
3011, 181, 53, 300, 269, 1, 200decaddci 11816 . . . . . . . . . . . . . . 15 (12 + 9) = 21
302 4p3e7 11441 . . . . . . . . . . . . . . 15 (4 + 3) = 7
303281, 24, 53, 182, 298, 299, 301, 302decadd 11809 . . . . . . . . . . . . . 14 (124 + 93) = 217
304293, 52, 71, 303decsuc 11786 . . . . . . . . . . . . 13 ((124 + 93) + 1) = 218
305 8p6e14 11839 . . . . . . . . . . . . . 14 (8 + 6) = 14
306158, 110, 305addcomli 10510 . . . . . . . . . . . . 13 (6 + 8) = 14
307294, 98, 295, 73, 296, 297, 304, 24, 306decaddc 11810 . . . . . . . . . . . 12 (1246 + 938) = 2184
308281, 24, 98, 53, 182, 293, 73, 73, 24, 307dpadd3 29942 . . . . . . . . . . 11 ((12.46) + (9.38)) = (21.84)
309292, 308eqtri 2827 . . . . . . . . . 10 (((1.54) + (10.92)) + (9.38)) = (21.84)
310271, 280, 3093eqtr4i 2837 . . . . . . . . 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 29944 . . . . . . . 8 ((1.167) · (1.414)) < (1.651)
312176, 32remulcli 10338 . . . . . . . . 9 ((1.167) · (1.414)) ∈ ℝ
31333, 312, 43lttri 10445 . . . . . . . 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 675 . . . . . . 7 (((1.079955)↑2) · (1.414)) < (1.651)
31550, 314pm3.2i 458 . . . . . 6 (0 ≤ (((1.079955)↑2) · (1.414)) ∧ (((1.079955)↑2) · (1.414)) < (1.651))
31644, 315pm3.2i 458 . . . . 5 (((((1.079955)↑2) · (1.414)) ∈ ℝ ∧ (1.651) ∈ ℝ) ∧ (0 ≤ (((1.079955)↑2) · (1.414)) ∧ (((1.079955)↑2) · (1.414)) < (1.651)))
317 4re 11377 . . . . . . . . . . 11 4 ∈ ℝ
318 2re 11370 . . . . . . . . . . . . 13 2 ∈ ℝ
319 3re 11374 . . . . . . . . . . . . . . 15 3 ∈ ℝ
32034, 319pm3.2i 458 . . . . . . . . . . . . . 14 (6 ∈ ℝ ∧ 3 ∈ ℝ)
321 dp2cl 29910 . . . . . . . . . . . . . 14 ((6 ∈ ℝ ∧ 3 ∈ ℝ) → 63 ∈ ℝ)
322320, 321ax-mp 5 . . . . . . . . . . . . 13 63 ∈ ℝ
323318, 322pm3.2i 458 . . . . . . . . . . . 12 (2 ∈ ℝ ∧ 63 ∈ ℝ)
324 dp2cl 29910 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ 63 ∈ ℝ) → 263 ∈ ℝ)
325323, 324ax-mp 5 . . . . . . . . . . 11 263 ∈ ℝ
326317, 325pm3.2i 458 . . . . . . . . . 10 (4 ∈ ℝ ∧ 263 ∈ ℝ)
327 dp2cl 29910 . . . . . . . . . 10 ((4 ∈ ℝ ∧ 263 ∈ ℝ) → 4263 ∈ ℝ)
328326, 327ax-mp 5 . . . . . . . . 9 4263 ∈ ℝ
329 dpcl 29921 . . . . . . . . 9 ((1 ∈ ℕ04263 ∈ ℝ) → (1.4263) ∈ ℝ)
3301, 328, 329mp2an 675 . . . . . . . 8 (1.4263) ∈ ℝ
33184, 319pm3.2i 458 . . . . . . . . . . . . . . . 16 (8 ∈ ℝ ∧ 3 ∈ ℝ)
332 dp2cl 29910 . . . . . . . . . . . . . . . 16 ((8 ∈ ℝ ∧ 3 ∈ ℝ) → 83 ∈ ℝ)
333331, 332ax-mp 5 . . . . . . . . . . . . . . 15 83 ∈ ℝ
33484, 333pm3.2i 458 . . . . . . . . . . . . . 14 (8 ∈ ℝ ∧ 83 ∈ ℝ)
335 dp2cl 29910 . . . . . . . . . . . . . 14 ((8 ∈ ℝ ∧ 83 ∈ ℝ) → 883 ∈ ℝ)
336334, 335ax-mp 5 . . . . . . . . . . . . 13 883 ∈ ℝ
337319, 336pm3.2i 458 . . . . . . . . . . . 12 (3 ∈ ℝ ∧ 883 ∈ ℝ)
338 dp2cl 29910 . . . . . . . . . . . 12 ((3 ∈ ℝ ∧ 883 ∈ ℝ) → 3883 ∈ ℝ)
339337, 338ax-mp 5 . . . . . . . . . . 11 3883 ∈ ℝ
3402, 339pm3.2i 458 . . . . . . . . . 10 (0 ∈ ℝ ∧ 3883 ∈ ℝ)
341 dp2cl 29910 . . . . . . . . . 10 ((0 ∈ ℝ ∧ 3883 ∈ ℝ) → 03883 ∈ ℝ)
342340, 341ax-mp 5 . . . . . . . . 9 03883 ∈ ℝ
343 dpcl 29921 . . . . . . . . 9 ((1 ∈ ℕ003883 ∈ ℝ) → (1.03883) ∈ ℝ)
3441, 342, 343mp2an 675 . . . . . . . 8 (1.03883) ∈ ℝ
345330, 344remulcli 10338 . . . . . . 7 ((1.4263) · (1.03883)) ∈ ℝ
346317, 333pm3.2i 458 . . . . . . . . 9 (4 ∈ ℝ ∧ 83 ∈ ℝ)
347 dp2cl 29910 . . . . . . . . 9 ((4 ∈ ℝ ∧ 83 ∈ ℝ) → 483 ∈ ℝ)
348346, 347ax-mp 5 . . . . . . . 8 483 ∈ ℝ
349 dpcl 29921 . . . . . . . 8 ((1 ∈ ℕ0483 ∈ ℝ) → (1.483) ∈ ℝ)
3501, 348, 349mp2an 675 . . . . . . 7 (1.483) ∈ ℝ
351345, 350pm3.2i 458 . . . . . 6 (((1.4263) · (1.03883)) ∈ ℝ ∧ (1.483) ∈ ℝ)
352 3rp 12048 . . . . . . . . . . . . 13 3 ∈ ℝ+
35398, 352rpdp2cl 29912 . . . . . . . . . . . 12 63 ∈ ℝ+
354181, 353rpdp2cl 29912 . . . . . . . . . . 11 263 ∈ ℝ+
35524, 354rpdp2cl 29912 . . . . . . . . . 10 4263 ∈ ℝ+
3561, 355rpdpcl 29933 . . . . . . . . 9 (1.4263) ∈ ℝ+
357 rpge0 12055 . . . . . . . . 9 ((1.4263) ∈ ℝ+ → 0 ≤ (1.4263))
358356, 357ax-mp 5 . . . . . . . 8 0 ≤ (1.4263)
35973, 352rpdp2cl 29912 . . . . . . . . . . . . 13 83 ∈ ℝ+
36073, 359rpdp2cl 29912 . . . . . . . . . . . 12 883 ∈ ℝ+
361182, 360rpdp2cl 29912 . . . . . . . . . . 11 3883 ∈ ℝ+
36251, 361rpdp2cl 29912 . . . . . . . . . 10 03883 ∈ ℝ+
3631, 362rpdpcl 29933 . . . . . . . . 9 (1.03883) ∈ ℝ+
364 rpge0 12055 . . . . . . . . 9 ((1.03883) ∈ ℝ+ → 0 ≤ (1.03883))
365363, 364ax-mp 5 . . . . . . . 8 0 ≤ (1.03883)
366330, 344mulge0i 10857 . . . . . . . 8 ((0 ≤ (1.4263) ∧ 0 ≤ (1.03883)) → 0 ≤ ((1.4263) · (1.03883)))
367358, 365, 366mp2an 675 . . . . . . 7 0 ≤ ((1.4263) · (1.03883))
368318, 3pm3.2i 458 . . . . . . . . . . . . . . 15 (2 ∈ ℝ ∧ 7 ∈ ℝ)
369 dp2cl 29910 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ ∧ 7 ∈ ℝ) → 27 ∈ ℝ)
370368, 369ax-mp 5 . . . . . . . . . . . . . 14 27 ∈ ℝ
371317, 370pm3.2i 458 . . . . . . . . . . . . 13 (4 ∈ ℝ ∧ 27 ∈ ℝ)
372 dp2cl 29910 . . . . . . . . . . . . 13 ((4 ∈ ℝ ∧ 27 ∈ ℝ) → 427 ∈ ℝ)
373371, 372ax-mp 5 . . . . . . . . . . . 12 427 ∈ ℝ
374 dpcl 29921 . . . . . . . . . . . 12 ((1 ∈ ℕ0427 ∈ ℝ) → (1.427) ∈ ℝ)
3751, 373, 374mp2an 675 . . . . . . . . . . 11 (1.427) ∈ ℝ
376330, 375pm3.2i 458 . . . . . . . . . 10 ((1.4263) ∈ ℝ ∧ (1.427) ∈ ℝ)
377 7nn 11463 . . . . . . . . . . . . . . 15 7 ∈ ℕ
378 nnrp 12052 . . . . . . . . . . . . . . 15 (7 ∈ ℕ → 7 ∈ ℝ+)
379377, 378ax-mp 5 . . . . . . . . . . . . . 14 7 ∈ ℝ+
380181, 379rpdp2cl 29912 . . . . . . . . . . . . 13 27 ∈ ℝ+
38124, 380rpdp2cl 29912 . . . . . . . . . . . 12 427 ∈ ℝ+
38298, 352, 184, 140dp2ltsuc 29916 . . . . . . . . . . . . . 14 63 < 7
383181, 353, 379, 382dp2lt 29915 . . . . . . . . . . . . 13 263 < 27
38424, 354, 380, 383dp2lt 29915 . . . . . . . . . . . 12 4263 < 427
3851, 355, 381, 384dplt 29934 . . . . . . . . . . 11 (1.4263) < (1.427)
386358, 385pm3.2i 458 . . . . . . . . . 10 (0 ≤ (1.4263) ∧ (1.4263) < (1.427))
387376, 386pm3.2i 458 . . . . . . . . 9 (((1.4263) ∈ ℝ ∧ (1.427) ∈ ℝ) ∧ (0 ≤ (1.4263) ∧ (1.4263) < (1.427)))
388319, 4pm3.2i 458 . . . . . . . . . . . . . . 15 (3 ∈ ℝ ∧ 9 ∈ ℝ)
389 dp2cl 29910 . . . . . . . . . . . . . . 15 ((3 ∈ ℝ ∧ 9 ∈ ℝ) → 39 ∈ ℝ)
390388, 389ax-mp 5 . . . . . . . . . . . . . 14 39 ∈ ℝ
3912, 390pm3.2i 458 . . . . . . . . . . . . 13 (0 ∈ ℝ ∧ 39 ∈ ℝ)
392 dp2cl 29910 . . . . . . . . . . . . 13 ((0 ∈ ℝ ∧ 39 ∈ ℝ) → 039 ∈ ℝ)
393391, 392ax-mp 5 . . . . . . . . . . . 12 039 ∈ ℝ
394 dpcl 29921 . . . . . . . . . . . 12 ((1 ∈ ℕ0039 ∈ ℝ) → (1.039) ∈ ℝ)
3951, 393, 394mp2an 675 . . . . . . . . . . 11 (1.039) ∈ ℝ
396344, 395pm3.2i 458 . . . . . . . . . 10 ((1.03883) ∈ ℝ ∧ (1.039) ∈ ℝ)
397 9nn 11465 . . . . . . . . . . . . . . 15 9 ∈ ℕ
398 nnrp 12052 . . . . . . . . . . . . . . 15 (9 ∈ ℕ → 9 ∈ ℝ+)
399397, 398ax-mp 5 . . . . . . . . . . . . . 14 9 ∈ ℝ+
400182, 399rpdp2cl 29912 . . . . . . . . . . . . 13 39 ∈ ℝ+
40151, 400rpdp2cl 29912 . . . . . . . . . . . 12 039 ∈ ℝ+
40273, 352, 185, 184dp2lt10 29914 . . . . . . . . . . . . . . 15 83 < 10
40373, 359, 402, 160dp2ltsuc 29916 . . . . . . . . . . . . . 14 883 < 9
404182, 360, 399, 403dp2lt 29915 . . . . . . . . . . . . 13 3883 < 39
40551, 361, 400, 404dp2lt 29915 . . . . . . . . . . . 12 03883 < 039
4061, 362, 401, 405dplt 29934 . . . . . . . . . . 11 (1.03883) < (1.039)
407365, 406pm3.2i 458 . . . . . . . . . 10 (0 ≤ (1.03883) ∧ (1.03883) < (1.039))
408396, 407pm3.2i 458 . . . . . . . . 9 (((1.03883) ∈ ℝ ∧ (1.039) ∈ ℝ) ∧ (0 ≤ (1.03883) ∧ (1.03883) < (1.039)))
409 ltmul12a 11161 . . . . . . . . 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 675 . . . . . . . 8 ((1.4263) · (1.03883)) < ((1.427) · (1.039))
411 6lt10 11889 . . . . . . . . 9 6 < 10
41273, 1deccl 11770 . . . . . . . . . 10 81 ∈ ℕ0
413 eqid 2805 . . . . . . . . . 10 816 = 816
414 eqid 2805 . . . . . . . . . 10 10 = 10
415 eqid 2805 . . . . . . . . . . . 12 81 = 81
41673, 1, 269, 415decsuc 11786 . . . . . . . . . . 11 (81 + 1) = 82
41773dec0h 11777 . . . . . . . . . . . 12 8 = 08
418417deceq1i 11762 . . . . . . . . . . 11 82 = 082
419416, 418eqtri 2827 . . . . . . . . . 10 (81 + 1) = 082
420110addid1i 10505 . . . . . . . . . 10 (6 + 0) = 6
421412, 98, 1, 51, 413, 414, 419, 420decadd 11809 . . . . . . . . 9 (816 + 10) = 0826
422138mul01i 10508 . . . . . . . . . 10 (1 · 0) = 0
423113mul01i 10508 . . . . . . . . . . 11 (4 · 0) = 0
42451dec0h 11777 . . . . . . . . . . 11 0 = 00
425423, 424eqtri 2827 . . . . . . . . . 10 (4 · 0) = 00
426113addid1i 10505 . . . . . . . . . . . 12 (4 + 0) = 4
427426oveq1i 6881 . . . . . . . . . . 11 ((4 + 0) + 0) = (4 + 0)
428427, 426, 2053eqtri 2831 . . . . . . . . . 10 ((4 + 0) + 0) = 04
4291, 24, 1, 51, 51, 51, 24, 51, 116, 422, 203, 425, 428, 192dpmul 29943 . . . . . . . . 9 ((1.4) · (1.0)) = (1.40)
430 3cn 11375 . . . . . . . . . . 11 3 ∈ ℂ
431 3t2e6 11453 . . . . . . . . . . 11 (3 · 2) = 6
432430, 197, 431mulcomli 10331 . . . . . . . . . 10 (2 · 3) = 6
433 9t2e18 11877 . . . . . . . . . . 11 (9 · 2) = 18
434196, 197, 433mulcomli 10331 . . . . . . . . . 10 (2 · 9) = 18
435 7t3e21 11865 . . . . . . . . . 10 (7 · 3) = 21
436 9t7e63 11882 . . . . . . . . . . 11 (9 · 7) = 63
437196, 217, 436mulcomli 10331 . . . . . . . . . 10 (7 · 9) = 63
438 eqid 2805 . . . . . . . . . . . . 13 21 = 21
439 eqid 2805 . . . . . . . . . . . . 13 18 = 18
440159, 160eqtri 2827 . . . . . . . . . . . . 13 (1 + 8) = 9
441181, 1, 1, 73, 438, 439, 224, 440decadd 11809 . . . . . . . . . . . 12 (21 + 18) = 39
442441oveq1i 6881 . . . . . . . . . . 11 ((21 + 18) + 6) = (39 + 6)
443 eqid 2805 . . . . . . . . . . . 12 39 = 39
444 3p1e4 11432 . . . . . . . . . . . 12 (3 + 1) = 4
445 9p6e15 11846 . . . . . . . . . . . 12 (9 + 6) = 15
446182, 53, 98, 443, 444, 54, 445decaddci 11816 . . . . . . . . . . 11 (39 + 6) = 45
447442, 446eqtri 2827 . . . . . . . . . 10 ((21 + 18) + 6) = 45
448 6p4e10 11827 . . . . . . . . . 10 (6 + 4) = 10
449181, 52, 182, 53, 98, 24, 54, 182, 432, 434, 435, 437, 447, 448dpmul 29943 . . . . . . . . 9 ((2.7) · (3.9)) = (10.53)
4501, 24deccl 11770 . . . . . . . . . . 11 14 ∈ ℕ0
451450, 51deccl 11770 . . . . . . . . . 10 140 ∈ ℕ0
452417, 73eqeltrri 2881 . . . . . . . . . 10 08 ∈ ℕ0
453 eqid 2805 . . . . . . . . . 10 1401 = 1401
454 eqid 2805 . . . . . . . . . 10 082 = 082
455 eqid 2805 . . . . . . . . . . 11 140 = 140
456417, 158eqeltrri 2881 . . . . . . . . . . . 12 08 ∈ ℂ
457 0cn 10314 . . . . . . . . . . . 12 0 ∈ ℂ
458417oveq1i 6881 . . . . . . . . . . . . 13 (8 + 0) = (08 + 0)
459158addid1i 10505 . . . . . . . . . . . . 13 (8 + 0) = 8
460458, 459eqtr3i 2829 . . . . . . . . . . . 12 (08 + 0) = 8
461456, 457, 460addcomli 10510 . . . . . . . . . . 11 (0 + 08) = 8
462450, 51, 452, 455, 461decaddi 11815 . . . . . . . . . 10 (140 + 08) = 148
463451, 1, 452, 181, 453, 454, 462, 230decadd 11809 . . . . . . . . 9 (1401 + 082) = 1483
464 4t4e16 11854 . . . . . . . . . . 11 (4 · 4) = 16
465 9t4e36 11879 . . . . . . . . . . . 12 (9 · 4) = 36
466196, 113, 465mulcomli 10331 . . . . . . . . . . 11 (4 · 9) = 36
467196mulid1i 10326 . . . . . . . . . . . . 13 (9 · 1) = 9
468467, 188eqtri 2827 . . . . . . . . . . . 12 (9 · 1) = 09
469196, 138, 468mulcomli 10331 . . . . . . . . . . 11 (1 · 9) = 09
470182, 98deccl 11770 . . . . . . . . . . . . . . 15 36 ∈ ℕ0
471470nn0cni 11567 . . . . . . . . . . . . . 14 36 ∈ ℂ
472 eqid 2805 . . . . . . . . . . . . . . 15 36 = 36
473182, 98, 24, 472, 444, 51, 448decaddci 11816 . . . . . . . . . . . . . 14 (36 + 4) = 40
474471, 113, 473addcomli 10510 . . . . . . . . . . . . 13 (4 + 36) = 40
475474oveq1i 6881 . . . . . . . . . . . 12 ((4 + 36) + 0) = (40 + 0)
47624, 51deccl 11770 . . . . . . . . . . . . . 14 40 ∈ ℕ0
477476nn0cni 11567 . . . . . . . . . . . . 13 40 ∈ ℂ
478477addid1i 10505 . . . . . . . . . . . 12 (40 + 0) = 40
479475, 478eqtri 2827 . . . . . . . . . . 11 ((4 + 36) + 0) = 40
4801, 98, 24, 135, 269, 51, 448decaddci 11816 . . . . . . . . . . 11 (16 + 4) = 20
48124, 1, 24, 53, 51, 24, 51, 53, 464, 466, 204, 469, 479, 480dpmul 29943 . . . . . . . . . 10 ((4.1) · (4.9)) = (20.09)
482 eqid 2805 . . . . . . . . . . . . 13 27 = 27
483230oveq1i 6881 . . . . . . . . . . . . . 14 ((1 + 2) + 1) = (3 + 1)
484483, 444eqtri 2827 . . . . . . . . . . . . 13 ((1 + 2) + 1) = 4
4851, 24, 181, 52, 268, 482, 484, 1, 225decaddc 11810 . . . . . . . . . . . 12 (14 + 27) = 41
4861, 24, 181, 52, 24, 1, 485dpadd 29941 . . . . . . . . . . 11 ((1.4) + (2.7)) = (4.1)
487430, 138, 444addcomli 10510 . . . . . . . . . . . . 13 (1 + 3) = 4
488196addid2i 10506 . . . . . . . . . . . . 13 (0 + 9) = 9
4891, 51, 182, 53, 414, 443, 487, 488decadd 11809 . . . . . . . . . . . 12 (10 + 39) = 49
4901, 51, 182, 53, 24, 53, 489dpadd 29941 . . . . . . . . . . 11 ((1.0) + (3.9)) = (4.9)
491486, 490oveq12i 6883 . . . . . . . . . 10 (((1.4) + (2.7)) · ((1.0) + (3.9))) = ((4.1) · (4.9))
4921, 24, 73, 1, 268, 415, 440, 210decadd 11809 . . . . . . . . . . . . . 14 (14 + 81) = 95
493450, 51, 412, 98, 455, 413, 492, 111decadd 11809 . . . . . . . . . . . . 13 (140 + 816) = 956
4941, 24, 51, 73, 1, 53, 98, 54, 98, 493dpadd3 29942 . . . . . . . . . . . 12 ((1.40) + (8.16)) = (9.56)
495494oveq1i 6881 . . . . . . . . . . 11 (((1.40) + (8.16)) + (10.53)) = ((9.56) + (10.53))
496181, 51deccl 11770 . . . . . . . . . . . 12 20 ∈ ℕ0
49753, 54deccl 11770 . . . . . . . . . . . . 13 95 ∈ ℕ0
498130, 54deccl 11770 . . . . . . . . . . . . 13 105 ∈ ℕ0
499 eqid 2805 . . . . . . . . . . . . 13 956 = 956
500 eqid 2805 . . . . . . . . . . . . 13 1053 = 1053
501 eqid 2805 . . . . . . . . . . . . . 14 95 = 95
502 eqid 2805 . . . . . . . . . . . . . 14 105 = 105
503 dec10p 11798 . . . . . . . . . . . . . . . . 17 (10 + 9) = 19
504283, 196, 503addcomli 10510 . . . . . . . . . . . . . . . 16 (9 + 10) = 19
505504oveq1i 6881 . . . . . . . . . . . . . . 15 ((9 + 10) + 1) = (19 + 1)
506 eqid 2805 . . . . . . . . . . . . . . . 16 19 = 19
5071, 53, 1, 506, 269, 51, 194decaddci 11816 . . . . . . . . . . . . . . 15 (19 + 1) = 20
508505, 507eqtri 2827 . . . . . . . . . . . . . 14 ((9 + 10) + 1) = 20
509 5p5e10 11826 . . . . . . . . . . . . . 14 (5 + 5) = 10
51053, 54, 130, 54, 501, 502, 508, 51, 509decaddc 11810 . . . . . . . . . . . . 13 (95 + 105) = 200
511497, 98, 498, 182, 499, 500, 510, 233decadd 11809 . . . . . . . . . . . 12 (956 + 1053) = 2009
51253, 54, 98, 130, 54, 496, 182, 51, 53, 511dpadd3 29942 . . . . . . . . . . 11 ((9.56) + (10.53)) = (20.09)
513495, 512eqtri 2827 . . . . . . . . . 10 (((1.40) + (8.16)) + (10.53)) = (20.09)
514481, 491, 5133eqtr4i 2837 . . . . . . . . 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 29944 . . . . . . . 8 ((1.427) · (1.039)) < (1.483)
516375, 395remulcli 10338 . . . . . . . . 9 ((1.427) · (1.039)) ∈ ℝ
517345, 516, 350lttri 10445 . . . . . . . 8 ((((1.4263) · (1.03883)) < ((1.427) · (1.039)) ∧ ((1.427) · (1.039)) < (1.483)) → ((1.4263) · (1.03883)) < (1.483))
518410, 515, 517mp2an 675 . . . . . . 7 ((1.4263) · (1.03883)) < (1.483)
519367, 518pm3.2i 458 . . . . . 6 (0 ≤ ((1.4263) · (1.03883)) ∧ ((1.4263) · (1.03883)) < (1.483))
520351, 519pm3.2i 458 . . . . 5 ((((1.4263) · (1.03883)) ∈ ℝ ∧ (1.483) ∈ ℝ) ∧ (0 ≤ ((1.4263) · (1.03883)) ∧ ((1.4263) · (1.03883)) < (1.483)))
521 ltmul12a 11161 . . . . 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 675 . . . 4 ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) < ((1.651) · (1.483))
52324, 181deccl 11770 . . . . 5 42 ∈ ℕ0
524496, 24deccl 11770 . . . . . 6 204 ∈ ℕ0
525 eqid 2805 . . . . . 6 2042 = 2042
526 eqid 2805 . . . . . 6 42 = 42
527 eqid 2805 . . . . . . 7 204 = 204
528496, 24, 24, 527, 277decaddi 11815 . . . . . 6 (204 + 4) = 208
529 2p2e4 11423 . . . . . 6 (2 + 2) = 4
530524, 181, 24, 181, 525, 526, 528, 529decadd 11809 . . . . 5 (2042 + 42) = 2084
531448oveq1i 6881 . . . . . . 7 ((6 + 4) + 2) = (10 + 2)
532 dec10p 11798 . . . . . . 7 (10 + 2) = 12
533531, 532eqtri 2827 . . . . . 6 ((6 + 4) + 2) = 12
5341, 98, 1, 24, 181, 1, 181, 24, 116, 204, 215, 216, 533, 269dpmul 29943 . . . . 5 ((1.6) · (1.4)) = (2.24)
535 8t5e40 11873 . . . . . . 7 (8 · 5) = 40
536158, 256, 535mulcomli 10331 . . . . . 6 (5 · 8) = 40
537 5t3e15 11856 . . . . . 6 (5 · 3) = 15
538158mulid2i 10327 . . . . . 6 (1 · 8) = 8
539430mulid2i 10327 . . . . . . 7 (1 · 3) = 3
540182dec0h 11777 . . . . . . 7 3 = 03
541539, 540eqtri 2827 . . . . . 6 (1 · 3) = 03
542235nn0cni 11567 . . . . . . . . 9 15 ∈ ℂ
543 8p5e13 11838 . . . . . . . . . . 11 (8 + 5) = 13
544158, 256, 543addcomli 10510 . . . . . . . . . 10 (5 + 8) = 13
5451, 54, 73, 245, 269, 182, 544decaddci 11816 . . . . . . . . 9 (15 + 8) = 23
546542, 158, 545addcomli 10510 . . . . . . . 8 (8 + 15) = 23
547546oveq1i 6881 . . . . . . 7 ((8 + 15) + 0) = (23 + 0)
548181, 182deccl 11770 . . . . . . . . 9 23 ∈ ℕ0
549548nn0cni 11567 . . . . . . . 8 23 ∈ ℂ
550549addid1i 10505 . . . . . . 7 (23 + 0) = 23
551547, 550eqtri 2827 . . . . . 6 ((8 + 15) + 0) = 23
552 eqid 2805 . . . . . . 7 40 = 40
553197addid2i 10506 . . . . . . 7 (0 + 2) = 2
55424, 51, 181, 552, 553decaddi 11815 . . . . . 6 (40 + 2) = 42
55554, 1, 73, 182, 51, 181, 182, 182, 536, 537, 538, 541, 551, 554dpmul 29943 . . . . 5 ((5.1) · (8.3)) = (42.33)
556181, 181deccl 11770 . . . . . . 7 22 ∈ ℕ0
557556, 24deccl 11770 . . . . . 6 224 ∈ ℕ0
558 eqid 2805 . . . . . 6 2241 = 2241
559 eqid 2805 . . . . . 6 208 = 208
560 eqid 2805 . . . . . . 7 224 = 224
561 eqid 2805 . . . . . . 7 20 = 20
562 eqid 2805 . . . . . . . 8 22 = 22
563181, 181, 181, 562, 529decaddi 11815 . . . . . . 7 (22 + 2) = 24
564556, 24, 181, 51, 560, 561, 563, 426decadd 11809 . . . . . 6 (224 + 20) = 244
565557, 1, 496, 73, 558, 559, 564, 440decadd 11809 . . . . 5 (2241 + 208) = 2449
566556, 98deccl 11770 . . . . . . . 8 226 ∈ ℕ0
567523, 182deccl 11770 . . . . . . . 8 423 ∈ ℕ0
568 eqid 2805 . . . . . . . 8 2266 = 2266
569 eqid 2805 . . . . . . . 8 4233 = 4233
570 eqid 2805 . . . . . . . . 9 226 = 226
571 eqid 2805 . . . . . . . . 9 423 = 423
572113, 197, 289addcomli 10510 . . . . . . . . . 10 (2 + 4) = 6
573181, 181, 24, 181, 562, 526, 572, 529decadd 11809 . . . . . . . . 9 (22 + 42) = 64
574556, 98, 523, 182, 570, 571, 573, 233decadd 11809 . . . . . . . 8 (226 + 423) = 649
575566, 98, 567, 182, 568, 569, 574, 233decadd 11809 . . . . . . 7 (2266 + 4233) = 6499
576556, 98, 98, 523, 182, 100, 182, 53, 53, 575dpadd3 29942 . . . . . 6 ((22.66) + (42.33)) = (64.99)
577496nn0cni 11567 . . . . . . . . . . 11 20 ∈ ℂ
578181, 51, 181, 561, 553decaddi 11815 . . . . . . . . . . 11 (20 + 2) = 22
579577, 197, 578addcomli 10510 . . . . . . . . . 10 (2 + 20) = 22
580181, 181, 496, 24, 562, 527, 579, 572decadd 11809 . . . . . . . . 9 (22 + 204) = 226
581556, 24, 524, 181, 560, 525, 580, 289decadd 11809 . . . . . . . 8 (224 + 2042) = 2266
582181, 181, 24, 496, 24, 556, 181, 98, 98, 581dpadd3 29942 . . . . . . 7 ((2.24) + (20.42)) = (22.66)
583582oveq1i 6881 . . . . . 6 (((2.24) + (20.42)) + (42.33)) = ((22.66) + (42.33))
584 eqid 2805 . . . . . . . . . 10 51 = 51
5851, 98, 54, 1, 135, 584, 257, 140decadd 11809 . . . . . . . . 9 (16 + 51) = 67
5861, 98, 54, 1, 98, 52, 585dpadd 29941 . . . . . . . 8 ((1.6) + (5.1)) = (6.7)
587 eqid 2805 . . . . . . . . . 10 83 = 83
5881, 24, 73, 182, 268, 587, 440, 302decadd 11809 . . . . . . . . 9 (14 + 83) = 97
5891, 24, 73, 182, 53, 52, 588dpadd 29941 . . . . . . . 8 ((1.4) + (8.3)) = (9.7)
590586, 589oveq12i 6883 . . . . . . 7 (((1.6) + (5.1)) · ((1.4) + (8.3))) = ((6.7) · (9.7))
591 9t6e54 11881 . . . . . . . . 9 (9 · 6) = 54
592196, 110, 591mulcomli 10331 . . . . . . . 8 (6 · 9) = 54
593 7t6e42 11868 . . . . . . . . 9 (7 · 6) = 42
594217, 110, 593mulcomli 10331 . . . . . . . 8 (6 · 7) = 42
595 7t7e49 11869 . . . . . . . 8 (7 · 7) = 49
596 eqid 2805 . . . . . . . . . . 11 63 = 63
597 3p2e5 11438 . . . . . . . . . . 11 (3 + 2) = 5
59898, 182, 24, 181, 596, 526, 448, 597decadd 11809 . . . . . . . . . 10 (63 + 42) = 105
599598oveq1i 6881 . . . . . . . . 9 ((63 + 42) + 4) = (105 + 4)
600 5p4e9 11445 . . . . . . . . . 10 (5 + 4) = 9
601130, 54, 24, 502, 600decaddi 11815 . . . . . . . . 9 (105 + 4) = 109
602599, 601eqtri 2827 . . . . . . . 8 ((63 + 42) + 4) = 109
603 eqid 2805 . . . . . . . . 9 54 = 54
60454, 24, 1, 51, 603, 414, 246, 426decadd 11809 . . . . . . . 8 (54 + 10) = 64
60598, 52, 53, 52, 24, 130, 53, 53, 592, 594, 437, 595, 602, 604dpmul 29943 . . . . . . 7 ((6.7) · (9.7)) = (64.99)
606590, 605eqtri 2827 . . . . . 6 (((1.6) + (5.1)) · ((1.4) + (8.3))) = (64.99)
607576, 583, 6063eqtr4ri 2838 . . . . 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 29944 . . . 4 ((1.651) · (1.483)) < (2.449)
60933, 345remulcli 10338 . . . . 5 ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) ∈ ℝ
61043, 350remulcli 10338 . . . . 5 ((1.651) · (1.483)) ∈ ℝ
61124, 399rpdp2cl 29912 . . . . . . . 8 49 ∈ ℝ+
61224, 611rpdp2cl 29912 . . . . . . 7 449 ∈ ℝ+
613181, 612rpdpcl 29933 . . . . . 6 (2.449) ∈ ℝ+
614 rpre 12049 . . . . . 6 ((2.449) ∈ ℝ+ → (2.449) ∈ ℝ)
615613, 614ax-mp 5 . . . . 5 (2.449) ∈ ℝ
616609, 610, 615lttri 10445 . . . 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 675 . . 3 ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) < (2.449)
618 3pos 11393 . . . 4 0 < 3
619609, 615, 319ltmul2i 11227 . . . 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 221 . 2 (3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) < (3 · (2.449))
622119dp2eq2i 29906 . . . . . . 7 000 = 00
623622, 119eqtri 2827 . . . . . 6 000 = 0
624623oveq2i 6882 . . . . 5 (3.000) = (3.0)
625182dp0u 29931 . . . . 5 (3.0) = 3
626624, 625eqtr2i 2828 . . . 4 3 = (3.000)
627626oveq1i 6881 . . 3 (3 · (2.449)) = ((3.000) · (2.449))
628450, 52deccl 11770 . . . . . . 7 147 ∈ ℕ0
629628, 51deccl 11770 . . . . . 6 1470 ∈ ℕ0
630629nn0cni 11567 . . . . 5 1470 ∈ ℂ
631630addid1i 10505 . . . 4 (1470 + 0) = 1470
632 4t3e12 11853 . . . . . 6 (4 · 3) = 12
633113, 430, 632mulcomli 10331 . . . . 5 (3 · 4) = 12
634197mul02i 10507 . . . . 5 (0 · 2) = 0
635113, 457, 425mulcomli 10331 . . . . 5 (0 · 4) = 00
63651, 51, 1, 181, 424, 300, 153, 553decadd 11809 . . . . . . 7 (0 + 12) = 12
637636oveq1i 6881 . . . . . 6 ((0 + 12) + 0) = (12 + 0)
638281nn0cni 11567 . . . . . . 7 12 ∈ ℂ
639638addid1i 10505 . . . . . 6 (12 + 0) = 12
640637, 639eqtri 2827 . . . . 5 ((0 + 12) + 0) = 12
641182, 51, 181, 24, 51, 1, 181, 51, 431, 633, 634, 635, 640, 140dpmul 29943 . . . 4 ((3.0) · (2.4)) = (7.20)
64251dp0u 29931 . . . . . . 7 (0.0) = 0
643642oveq1i 6881 . . . . . 6 ((0.0) · (4.9)) = (0 · (4.9))
644 dpcl 29921 . . . . . . . . 9 ((4 ∈ ℕ0 ∧ 9 ∈ ℝ) → (4.9) ∈ ℝ)
64524, 4, 644mp2an 675 . . . . . . . 8 (4.9) ∈ ℝ
646645recni 10336 . . . . . . 7 (4.9) ∈ ℂ
647646mul02i 10507 . . . . . 6 (0 · (4.9)) = 0
648643, 647eqtri 2827 . . . . 5 ((0.0) · (4.9)) = 0
649119oveq2i 6882 . . . . . 6 (0.00) = (0.0)
650649, 642eqtri 2827 . . . . 5 (0.00) = 0
651648, 650eqtr4i 2830 . . . 4 ((0.0) · (4.9)) = (0.00)
65252, 181deccl 11770 . . . . . 6 72 ∈ ℕ0
653652, 51deccl 11770 . . . . 5 720 ∈ ℕ0
654 eqid 2805 . . . . 5 7201 = 7201
655 eqid 2805 . . . . 5 147 = 147
656 eqid 2805 . . . . . 6 720 = 720
65752, 181, 224, 263decsuc 11786 . . . . . 6 (72 + 1) = 73
658652, 51, 1, 24, 656, 268, 657, 114decadd 11809 . . . . 5 (720 + 14) = 734
659653, 1, 450, 52, 654, 655, 658, 274decadd 11809 . . . 4 (7201 + 147) = 7348
660642oveq2i 6882 . . . . . . . 8 ((3.0) + (0.0)) = ((3.0) + 0)
661625, 430eqeltri 2880 . . . . . . . . 9 (3.0) ∈ ℂ
662661addid1i 10505 . . . . . . . 8 ((3.0) + 0) = (3.0)
663660, 662eqtri 2827 . . . . . . 7 ((3.0) + (0.0)) = (3.0)
664 eqid 2805 . . . . . . . . 9 49 = 49
665572oveq1i 6881 . . . . . . . . . 10 ((2 + 4) + 1) = (6 + 1)
666665, 140eqtri 2827 . . . . . . . . 9 ((2 + 4) + 1) = 7
667 9p4e13 11844 . . . . . . . . . 10 (9 + 4) = 13
668196, 113, 667addcomli 10510 . . . . . . . . 9 (4 + 9) = 13
669181, 24, 24, 53, 223, 664, 666, 182, 668decaddc 11810 . . . . . . . 8 (24 + 49) = 73
670181, 24, 24, 53, 52, 182, 669dpadd 29941 . . . . . . 7 ((2.4) + (4.9)) = (7.3)
671663, 670oveq12i 6883 . . . . . 6 (((3.0) + (0.0)) · ((2.4) + (4.9))) = ((3.0) · (7.3))
672217, 430, 435mulcomli 10331 . . . . . . 7 (3 · 7) = 21
673 3t3e9 11454 . . . . . . 7 (3 · 3) = 9
674217mul01i 10508 . . . . . . . 8 (7 · 0) = 0
675217, 457, 674mulcomli 10331 . . . . . . 7 (0 · 7) = 0
676430mul01i 10508 . . . . . . . . 9 (3 · 0) = 0
677676, 424eqtri 2827 . . . . . . . 8 (3 · 0) = 00
678430, 457, 677mulcomli 10331 . . . . . . 7 (0 · 3) = 00
679196addid1i 10505 . . . . . . . . . 10 (9 + 0) = 9
680679oveq1i 6881 . . . . . . . . 9 ((9 + 0) + 0) = (9 + 0)
681680, 679, 1883eqtri 2831 . . . . . . . 8 ((9 + 0) + 0) = 09
682196, 457addcomi 10509 . . . . . . . . . 10 (9 + 0) = (0 + 9)
683682oveq1i 6881 . . . . . . . . 9 ((9 + 0) + 0) = ((0 + 9) + 0)
684683eqeq1i 2810 . . . . . . . 8 (((9 + 0) + 0) = 09 ↔ ((0 + 9) + 0) = 09)
685681, 684mpbi 221 . . . . . . 7 ((0 + 9) + 0) = 09
686181, 1, 51, 438, 192decaddi 11815 . . . . . . 7 (21 + 0) = 21
687182, 51, 52, 182, 51, 51, 53, 51, 672, 673, 675, 678, 685, 686dpmul 29943 . . . . . 6 ((3.0) · (7.3)) = (21.90)
688671, 687eqtri 2827 . . . . 5 (((3.0) + (0.0)) · ((2.4) + (4.9))) = (21.90)
689650oveq2i 6882 . . . . . 6 (((7.20) + (14.70)) + (0.00)) = (((7.20) + (14.70)) + 0)
690318, 2pm3.2i 458 . . . . . . . . . . 11 (2 ∈ ℝ ∧ 0 ∈ ℝ)
691 dp2cl 29910 . . . . . . . . . . 11 ((2 ∈ ℝ ∧ 0 ∈ ℝ) → 20 ∈ ℝ)
692690, 691ax-mp 5 . . . . . . . . . 10 20 ∈ ℝ
693 dpcl 29921 . . . . . . . . . 10 ((7 ∈ ℕ020 ∈ ℝ) → (7.20) ∈ ℝ)
69452, 692, 693mp2an 675 . . . . . . . . 9 (7.20) ∈ ℝ
695694recni 10336 . . . . . . . 8 (7.20) ∈ ℂ
6963, 2pm3.2i 458 . . . . . . . . . . 11 (7 ∈ ℝ ∧ 0 ∈ ℝ)
697 dp2cl 29910 . . . . . . . . . . 11 ((7 ∈ ℝ ∧ 0 ∈ ℝ) → 70 ∈ ℝ)
698696, 697ax-mp 5 . . . . . . . . . 10 70 ∈ ℝ
699 dpcl 29921 . . . . . . . . . 10 ((14 ∈ ℕ070 ∈ ℝ) → (14.70) ∈ ℝ)
700450, 698, 699mp2an 675 . . . . . . . . 9 (14.70) ∈ ℝ
701700recni 10336 . . . . . . . 8 (14.70) ∈ ℂ
702695, 701addcli 10328 . . . . . . 7 ((7.20) + (14.70)) ∈ ℂ
703702addid1i 10505 . . . . . 6 (((7.20) + (14.70)) + 0) = ((7.20) + (14.70))
704 eqid 2805 . . . . . . . 8 1470 = 1470
705450nn0cni 11567 . . . . . . . . . 10 14 ∈ ℂ
706705, 217, 270addcomli 10510 . . . . . . . . 9 (7 + 14) = 21
707 7p2e9 11448 . . . . . . . . . 10 (7 + 2) = 9
708217, 197, 707addcomli 10510 . . . . . . . . 9 (2 + 7) = 9
70952, 181, 450, 52, 263, 655, 706, 708decadd 11809 . . . . . . . 8 (72 + 147) = 219
710 00id 10493 . . . . . . . 8 (0 + 0) = 0
711652, 51, 628, 51, 656, 704, 709, 710decadd 11809 . . . . . . 7 (720 + 1470) = 2190
71252, 181, 51, 450, 52, 293, 51, 53, 51, 711dpadd3 29942 . . . . . 6 ((7.20) + (14.70)) = (21.90)
713689, 703, 7123eqtri 2831 . . . . 5 (((7.20) + (14.70)) + (0.00)) = (21.90)
714688, 713eqtr4i 2830 . . . 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 29944 . . 3 ((3.000) · (2.449)) < (7.348)
716627, 715eqbrtri 4861 . 2 (3 · (2.449)) < (7.348)
717319, 609remulcli 10338 . . 3 (3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) ∈ ℝ
718319, 615remulcli 10338 . . 3 (3 · (2.449)) ∈ ℝ
719 nnrp 12052 . . . . . . . 8 (8 ∈ ℕ → 8 ∈ ℝ+)
72063, 719ax-mp 5 . . . . . . 7 8 ∈ ℝ+
72124, 720rpdp2cl 29912 . . . . . 6 48 ∈ ℝ+
722182, 721rpdp2cl 29912 . . . . 5 348 ∈ ℝ+
72352, 722rpdpcl 29933 . . . 4 (7.348) ∈ ℝ+
724 rpre 12049 . . . 4 ((7.348) ∈ ℝ+ → (7.348) ∈ ℝ)
725723, 724ax-mp 5 . . 3 (7.348) ∈ ℝ
726717, 718, 725lttri 10445 . 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 675 1 (3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) < (7.348)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384   = wceq 1637  wcel 2158   class class class wbr 4840  (class class class)co 6871  cc 10216  cr 10217  0cc0 10218  1c1 10219   + caddc 10221   · cmul 10223   < clt 10356  cle 10357  cn 11302  2c2 11352  3c3 11353  4c4 11354  5c5 11355  6c6 11356  7c7 11357  8c8 11358  9c9 11359  0cn0 11555  cdc 11755  +crp 12042  cexp 13079  cdp2 29901  .cdp 29918
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176  ax-cnex 10274  ax-resscn 10275  ax-1cn 10276  ax-icn 10277  ax-addcl 10278  ax-addrcl 10279  ax-mulcl 10280  ax-mulrcl 10281  ax-mulcom 10282  ax-addass 10283  ax-mulass 10284  ax-distr 10285  ax-i2m1 10286  ax-1ne0 10287  ax-1rid 10288  ax-rnegex 10289  ax-rrecex 10290  ax-cnre 10291  ax-pre-lttri 10292  ax-pre-lttrn 10293  ax-pre-ltadd 10294  ax-pre-mulgt0 10295
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-nel 3081  df-ral 3100  df-rex 3101  df-reu 3102  df-rmo 3103  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-pss 3782  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4627  df-iun 4710  df-br 4841  df-opab 4903  df-mpt 4920  df-tr 4943  df-id 5216  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-we 5269  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-pred 5890  df-ord 5936  df-on 5937  df-lim 5938  df-suc 5939  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-riota 6832  df-ov 6874  df-oprab 6875  df-mpt2 6876  df-om 7293  df-2nd 7396  df-wrecs 7639  df-recs 7701  df-rdg 7739  df-er 7976  df-en 8190  df-dom 8191  df-sdom 8192  df-pnf 10358  df-mnf 10359  df-xr 10360  df-ltxr 10361  df-le 10362  df-sub 10550  df-neg 10551  df-div 10967  df-nn 11303  df-2 11360  df-3 11361  df-4 11362  df-5 11363  df-6 11364  df-7 11365  df-8 11366  df-9 11367  df-n0 11556  df-z 11640  df-dec 11756  df-uz 11901  df-rp 12043  df-seq 13021  df-exp 13080  df-dp2 29902  df-dp 29919
This theorem is referenced by:  hgt750leme  31058
  Copyright terms: Public domain W3C validator