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

Theorem hgt750lem 34192
Description: Lemma for tgoldbachgtd 34203. (Contributed by Thierry Arnoux, 17-Dec-2021.)
Assertion
Ref Expression
hgt750lem ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ((7.348) ยท ((logโ€˜๐‘) / (โˆšโ€˜๐‘))) < (0.00042248))

Proof of Theorem hgt750lem
StepHypRef Expression
1 7nn0 12498 . . . . 5 7 โˆˆ โ„•0
2 3re 12296 . . . . . . 7 3 โˆˆ โ„
3 4re 12300 . . . . . . . . 9 4 โˆˆ โ„
4 8re 12312 . . . . . . . . 9 8 โˆˆ โ„
53, 4pm3.2i 470 . . . . . . . 8 (4 โˆˆ โ„ โˆง 8 โˆˆ โ„)
6 dp2cl 32551 . . . . . . . 8 ((4 โˆˆ โ„ โˆง 8 โˆˆ โ„) โ†’ 48 โˆˆ โ„)
75, 6ax-mp 5 . . . . . . 7 48 โˆˆ โ„
82, 7pm3.2i 470 . . . . . 6 (3 โˆˆ โ„ โˆง 48 โˆˆ โ„)
9 dp2cl 32551 . . . . . 6 ((3 โˆˆ โ„ โˆง 48 โˆˆ โ„) โ†’ 348 โˆˆ โ„)
108, 9ax-mp 5 . . . . 5 348 โˆˆ โ„
11 dpcl 32562 . . . . 5 ((7 โˆˆ โ„•0 โˆง 348 โˆˆ โ„) โ†’ (7.348) โˆˆ โ„)
121, 10, 11mp2an 689 . . . 4 (7.348) โˆˆ โ„
1312a1i 11 . . 3 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ (7.348) โˆˆ โ„)
14 nn0re 12485 . . . . . . 7 (๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ โ„)
1514adantr 480 . . . . . 6 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ๐‘ โˆˆ โ„)
16 0re 11220 . . . . . . . 8 0 โˆˆ โ„
1716a1i 11 . . . . . . 7 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ 0 โˆˆ โ„)
18 10re 12700 . . . . . . . . 9 10 โˆˆ โ„
19 2nn0 12493 . . . . . . . . . 10 2 โˆˆ โ„•0
2019, 1deccl 12696 . . . . . . . . 9 27 โˆˆ โ„•0
21 reexpcl 14049 . . . . . . . . 9 ((10 โˆˆ โ„ โˆง 27 โˆˆ โ„•0) โ†’ (10โ†‘27) โˆˆ โ„)
2218, 20, 21mp2an 689 . . . . . . . 8 (10โ†‘27) โˆˆ โ„
2322a1i 11 . . . . . . 7 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ (10โ†‘27) โˆˆ โ„)
24 0lt1 11740 . . . . . . . . 9 0 < 1
25 1nn 12227 . . . . . . . . . . 11 1 โˆˆ โ„•
26 0nn0 12491 . . . . . . . . . . 11 0 โˆˆ โ„•0
27 1nn0 12492 . . . . . . . . . . 11 1 โˆˆ โ„•0
28 1re 11218 . . . . . . . . . . . 12 1 โˆˆ โ„
29 9re 12315 . . . . . . . . . . . 12 9 โˆˆ โ„
30 1lt9 12422 . . . . . . . . . . . 12 1 < 9
3128, 29, 30ltleii 11341 . . . . . . . . . . 11 1 โ‰ค 9
3225, 26, 27, 31declei 12717 . . . . . . . . . 10 1 โ‰ค 10
33 expge1 14070 . . . . . . . . . 10 ((10 โˆˆ โ„ โˆง 27 โˆˆ โ„•0 โˆง 1 โ‰ค 10) โ†’ 1 โ‰ค (10โ†‘27))
3418, 20, 32, 33mp3an 1457 . . . . . . . . 9 1 โ‰ค (10โ†‘27)
3516, 28, 22ltletri 11346 . . . . . . . . 9 ((0 < 1 โˆง 1 โ‰ค (10โ†‘27)) โ†’ 0 < (10โ†‘27))
3624, 34, 35mp2an 689 . . . . . . . 8 0 < (10โ†‘27)
3736a1i 11 . . . . . . 7 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ 0 < (10โ†‘27))
38 simpr 484 . . . . . . 7 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ (10โ†‘27) โ‰ค ๐‘)
3917, 23, 15, 37, 38ltletrd 11378 . . . . . 6 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ 0 < ๐‘)
4015, 39elrpd 13019 . . . . 5 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ๐‘ โˆˆ โ„+)
4140relogcld 26512 . . . 4 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ (logโ€˜๐‘) โˆˆ โ„)
4240rpge0d 13026 . . . . 5 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ 0 โ‰ค ๐‘)
4315, 42resqrtcld 15370 . . . 4 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ (โˆšโ€˜๐‘) โˆˆ โ„)
4440sqrtgt0d 15365 . . . . 5 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ 0 < (โˆšโ€˜๐‘))
4517, 44gtned 11353 . . . 4 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ (โˆšโ€˜๐‘) โ‰  0)
4641, 43, 45redivcld 12046 . . 3 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ((logโ€˜๐‘) / (โˆšโ€˜๐‘)) โˆˆ โ„)
4713, 46remulcld 11248 . 2 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ((7.348) ยท ((logโ€˜๐‘) / (โˆšโ€˜๐‘))) โˆˆ โ„)
48 elrp 12982 . . . . . . 7 ((10โ†‘27) โˆˆ โ„+ โ†” ((10โ†‘27) โˆˆ โ„ โˆง 0 < (10โ†‘27)))
4922, 36, 48mpbir2an 708 . . . . . 6 (10โ†‘27) โˆˆ โ„+
50 relogcl 26464 . . . . . 6 ((10โ†‘27) โˆˆ โ„+ โ†’ (logโ€˜(10โ†‘27)) โˆˆ โ„)
5149, 50ax-mp 5 . . . . 5 (logโ€˜(10โ†‘27)) โˆˆ โ„
5222, 36sqrtpclii 15335 . . . . 5 (โˆšโ€˜(10โ†‘27)) โˆˆ โ„
5322, 36sqrtgt0ii 15336 . . . . . 6 0 < (โˆšโ€˜(10โ†‘27))
5416, 53gtneii 11330 . . . . 5 (โˆšโ€˜(10โ†‘27)) โ‰  0
5551, 52, 54redivcli 11985 . . . 4 ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))) โˆˆ โ„
5655a1i 11 . . 3 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))) โˆˆ โ„)
5713, 56remulcld 11248 . 2 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ((7.348) ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))) โˆˆ โ„)
58 qssre 12947 . . . . 5 โ„š โІ โ„
59 4nn0 12495 . . . . . . . . 9 4 โˆˆ โ„•0
60 nn0ssq 12945 . . . . . . . . . . . . 13 โ„•0 โІ โ„š
61 8nn0 12499 . . . . . . . . . . . . 13 8 โˆˆ โ„•0
6260, 61sselii 3974 . . . . . . . . . . . 12 8 โˆˆ โ„š
6359, 62dp2clq 32552 . . . . . . . . . . 11 48 โˆˆ โ„š
6419, 63dp2clq 32552 . . . . . . . . . 10 248 โˆˆ โ„š
6519, 64dp2clq 32552 . . . . . . . . 9 2248 โˆˆ โ„š
6659, 65dp2clq 32552 . . . . . . . 8 42248 โˆˆ โ„š
6726, 66dp2clq 32552 . . . . . . 7 042248 โˆˆ โ„š
6826, 67dp2clq 32552 . . . . . 6 0042248 โˆˆ โ„š
6926, 68dp2clq 32552 . . . . 5 00042248 โˆˆ โ„š
7058, 69sselii 3974 . . . 4 00042248 โˆˆ โ„
71 dpcl 32562 . . . 4 ((0 โˆˆ โ„•0 โˆง 00042248 โˆˆ โ„) โ†’ (0.00042248) โˆˆ โ„)
7226, 70, 71mp2an 689 . . 3 (0.00042248) โˆˆ โ„
7372a1i 11 . 2 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ (0.00042248) โˆˆ โ„)
74 3nn0 12494 . . . . . . . . 9 3 โˆˆ โ„•0
75 8pos 12328 . . . . . . . . . . 11 0 < 8
76 elrp 12982 . . . . . . . . . . 11 (8 โˆˆ โ„+ โ†” (8 โˆˆ โ„ โˆง 0 < 8))
774, 75, 76mpbir2an 708 . . . . . . . . . 10 8 โˆˆ โ„+
7859, 77rpdp2cl 32553 . . . . . . . . 9 48 โˆˆ โ„+
7974, 78rpdp2cl 32553 . . . . . . . 8 348 โˆˆ โ„+
801, 79rpdpcl 32574 . . . . . . 7 (7.348) โˆˆ โ„+
81 elrp 12982 . . . . . . 7 ((7.348) โˆˆ โ„+ โ†” ((7.348) โˆˆ โ„ โˆง 0 < (7.348)))
8280, 81mpbi 229 . . . . . 6 ((7.348) โˆˆ โ„ โˆง 0 < (7.348))
8382simpri 485 . . . . 5 0 < (7.348)
8416, 12, 83ltleii 11341 . . . 4 0 โ‰ค (7.348)
8584a1i 11 . . 3 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ 0 โ‰ค (7.348))
8649a1i 11 . . . 4 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ (10โ†‘27) โˆˆ โ„+)
87 2cn 12291 . . . . . . . . . 10 2 โˆˆ โ„‚
8887mullidi 11223 . . . . . . . . 9 (1 ยท 2) = 2
89 2nn 12289 . . . . . . . . . . 11 2 โˆˆ โ„•
9089, 1, 27, 31declei 12717 . . . . . . . . . 10 1 โ‰ค 27
91 2pos 12319 . . . . . . . . . . 11 0 < 2
9220nn0rei 12487 . . . . . . . . . . . 12 27 โˆˆ โ„
93 2re 12290 . . . . . . . . . . . 12 2 โˆˆ โ„
9428, 92, 93lemul1i 12140 . . . . . . . . . . 11 (0 < 2 โ†’ (1 โ‰ค 27 โ†” (1 ยท 2) โ‰ค (27 ยท 2)))
9591, 94ax-mp 5 . . . . . . . . . 10 (1 โ‰ค 27 โ†” (1 ยท 2) โ‰ค (27 ยท 2))
9690, 95mpbi 229 . . . . . . . . 9 (1 ยท 2) โ‰ค (27 ยท 2)
9788, 96eqbrtrri 5164 . . . . . . . 8 2 โ‰ค (27 ยท 2)
98 1p1e2 12341 . . . . . . . . . . 11 (1 + 1) = 2
99 loge 26475 . . . . . . . . . . . . . 14 (logโ€˜e) = 1
100 egt2lt3 16156 . . . . . . . . . . . . . . . 16 (2 < e โˆง e < 3)
101100simpri 485 . . . . . . . . . . . . . . 15 e < 3
102 epr 16158 . . . . . . . . . . . . . . . 16 e โˆˆ โ„+
103 3rp 12986 . . . . . . . . . . . . . . . 16 3 โˆˆ โ„+
104 logltb 26489 . . . . . . . . . . . . . . . 16 ((e โˆˆ โ„+ โˆง 3 โˆˆ โ„+) โ†’ (e < 3 โ†” (logโ€˜e) < (logโ€˜3)))
105102, 103, 104mp2an 689 . . . . . . . . . . . . . . 15 (e < 3 โ†” (logโ€˜e) < (logโ€˜3))
106101, 105mpbi 229 . . . . . . . . . . . . . 14 (logโ€˜e) < (logโ€˜3)
10799, 106eqbrtrri 5164 . . . . . . . . . . . . 13 1 < (logโ€˜3)
108 relogcl 26464 . . . . . . . . . . . . . . 15 (3 โˆˆ โ„+ โ†’ (logโ€˜3) โˆˆ โ„)
109103, 108ax-mp 5 . . . . . . . . . . . . . 14 (logโ€˜3) โˆˆ โ„
11028, 28, 109, 109lt2addi 11780 . . . . . . . . . . . . 13 ((1 < (logโ€˜3) โˆง 1 < (logโ€˜3)) โ†’ (1 + 1) < ((logโ€˜3) + (logโ€˜3)))
111107, 107, 110mp2an 689 . . . . . . . . . . . 12 (1 + 1) < ((logโ€˜3) + (logโ€˜3))
112 3cn 12297 . . . . . . . . . . . . . 14 3 โˆˆ โ„‚
113 3ne0 12322 . . . . . . . . . . . . . 14 3 โ‰  0
114 logmul2 26505 . . . . . . . . . . . . . 14 ((3 โˆˆ โ„‚ โˆง 3 โ‰  0 โˆง 3 โˆˆ โ„+) โ†’ (logโ€˜(3 ยท 3)) = ((logโ€˜3) + (logโ€˜3)))
115112, 113, 103, 114mp3an 1457 . . . . . . . . . . . . 13 (logโ€˜(3 ยท 3)) = ((logโ€˜3) + (logโ€˜3))
116 3t3e9 12383 . . . . . . . . . . . . . . 15 (3 ยท 3) = 9
117116fveq2i 6888 . . . . . . . . . . . . . 14 (logโ€˜(3 ยท 3)) = (logโ€˜9)
118 9lt10 12812 . . . . . . . . . . . . . . . 16 9 < 10
11929, 18, 118ltleii 11341 . . . . . . . . . . . . . . 15 9 โ‰ค 10
120 9pos 12329 . . . . . . . . . . . . . . . . 17 0 < 9
121 elrp 12982 . . . . . . . . . . . . . . . . 17 (9 โˆˆ โ„+ โ†” (9 โˆˆ โ„ โˆง 0 < 9))
12229, 120, 121mpbir2an 708 . . . . . . . . . . . . . . . 16 9 โˆˆ โ„+
123 10pos 12698 . . . . . . . . . . . . . . . . 17 0 < 10
124 elrp 12982 . . . . . . . . . . . . . . . . 17 (10 โˆˆ โ„+ โ†” (10 โˆˆ โ„ โˆง 0 < 10))
12518, 123, 124mpbir2an 708 . . . . . . . . . . . . . . . 16 10 โˆˆ โ„+
126 logleb 26492 . . . . . . . . . . . . . . . 16 ((9 โˆˆ โ„+ โˆง 10 โˆˆ โ„+) โ†’ (9 โ‰ค 10 โ†” (logโ€˜9) โ‰ค (logโ€˜10)))
127122, 125, 126mp2an 689 . . . . . . . . . . . . . . 15 (9 โ‰ค 10 โ†” (logโ€˜9) โ‰ค (logโ€˜10))
128119, 127mpbi 229 . . . . . . . . . . . . . 14 (logโ€˜9) โ‰ค (logโ€˜10)
129117, 128eqbrtri 5162 . . . . . . . . . . . . 13 (logโ€˜(3 ยท 3)) โ‰ค (logโ€˜10)
130115, 129eqbrtrri 5164 . . . . . . . . . . . 12 ((logโ€˜3) + (logโ€˜3)) โ‰ค (logโ€˜10)
13128, 28readdcli 11233 . . . . . . . . . . . . 13 (1 + 1) โˆˆ โ„
132109, 109readdcli 11233 . . . . . . . . . . . . 13 ((logโ€˜3) + (logโ€˜3)) โˆˆ โ„
133 relogcl 26464 . . . . . . . . . . . . . 14 (10 โˆˆ โ„+ โ†’ (logโ€˜10) โˆˆ โ„)
134125, 133ax-mp 5 . . . . . . . . . . . . 13 (logโ€˜10) โˆˆ โ„
135131, 132, 134ltletri 11346 . . . . . . . . . . . 12 (((1 + 1) < ((logโ€˜3) + (logโ€˜3)) โˆง ((logโ€˜3) + (logโ€˜3)) โ‰ค (logโ€˜10)) โ†’ (1 + 1) < (logโ€˜10))
136111, 130, 135mp2an 689 . . . . . . . . . . 11 (1 + 1) < (logโ€˜10)
13798, 136eqbrtrri 5164 . . . . . . . . . 10 2 < (logโ€˜10)
13893, 134ltlei 11340 . . . . . . . . . 10 (2 < (logโ€˜10) โ†’ 2 โ‰ค (logโ€˜10))
139137, 138ax-mp 5 . . . . . . . . 9 2 โ‰ค (logโ€˜10)
14016, 29, 120ltleii 11341 . . . . . . . . . . 11 0 โ‰ค 9
14189, 1, 26, 140decltdi 12720 . . . . . . . . . 10 0 < 27
14293, 134, 92lemul2i 12141 . . . . . . . . . 10 (0 < 27 โ†’ (2 โ‰ค (logโ€˜10) โ†” (27 ยท 2) โ‰ค (27 ยท (logโ€˜10))))
143141, 142ax-mp 5 . . . . . . . . 9 (2 โ‰ค (logโ€˜10) โ†” (27 ยท 2) โ‰ค (27 ยท (logโ€˜10)))
144139, 143mpbi 229 . . . . . . . 8 (27 ยท 2) โ‰ค (27 ยท (logโ€˜10))
14592, 93remulcli 11234 . . . . . . . . 9 (27 ยท 2) โˆˆ โ„
14620nn0zi 12591 . . . . . . . . . . 11 27 โˆˆ โ„ค
147 relogexp 26485 . . . . . . . . . . 11 ((10 โˆˆ โ„+ โˆง 27 โˆˆ โ„ค) โ†’ (logโ€˜(10โ†‘27)) = (27 ยท (logโ€˜10)))
148125, 146, 147mp2an 689 . . . . . . . . . 10 (logโ€˜(10โ†‘27)) = (27 ยท (logโ€˜10))
149148, 51eqeltrri 2824 . . . . . . . . 9 (27 ยท (logโ€˜10)) โˆˆ โ„
15093, 145, 149letri 11347 . . . . . . . 8 ((2 โ‰ค (27 ยท 2) โˆง (27 ยท 2) โ‰ค (27 ยท (logโ€˜10))) โ†’ 2 โ‰ค (27 ยท (logโ€˜10)))
15197, 144, 150mp2an 689 . . . . . . 7 2 โ‰ค (27 ยท (logโ€˜10))
152 relogef 26471 . . . . . . . 8 (2 โˆˆ โ„ โ†’ (logโ€˜(expโ€˜2)) = 2)
15393, 152ax-mp 5 . . . . . . 7 (logโ€˜(expโ€˜2)) = 2
154151, 153, 1483brtr4i 5171 . . . . . 6 (logโ€˜(expโ€˜2)) โ‰ค (logโ€˜(10โ†‘27))
155 rpefcl 16054 . . . . . . . 8 (2 โˆˆ โ„ โ†’ (expโ€˜2) โˆˆ โ„+)
15693, 155ax-mp 5 . . . . . . 7 (expโ€˜2) โˆˆ โ„+
157 logleb 26492 . . . . . . 7 (((expโ€˜2) โˆˆ โ„+ โˆง (10โ†‘27) โˆˆ โ„+) โ†’ ((expโ€˜2) โ‰ค (10โ†‘27) โ†” (logโ€˜(expโ€˜2)) โ‰ค (logโ€˜(10โ†‘27))))
158156, 49, 157mp2an 689 . . . . . 6 ((expโ€˜2) โ‰ค (10โ†‘27) โ†” (logโ€˜(expโ€˜2)) โ‰ค (logโ€˜(10โ†‘27)))
159154, 158mpbir 230 . . . . 5 (expโ€˜2) โ‰ค (10โ†‘27)
160159a1i 11 . . . 4 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ (expโ€˜2) โ‰ค (10โ†‘27))
16186, 40, 160, 38logdivsqrle 34191 . . 3 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ((logโ€˜๐‘) / (โˆšโ€˜๐‘)) โ‰ค ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))))
16246, 56, 13, 85, 161lemul2ad 12158 . 2 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ((7.348) ยท ((logโ€˜๐‘) / (โˆšโ€˜๐‘))) โ‰ค ((7.348) ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))))
163 3lt10 12818 . . . . . . . 8 3 < 10
164 4lt10 12817 . . . . . . . . 9 4 < 10
165 8lt10 12813 . . . . . . . . 9 8 < 10
16659, 77, 164, 165dp2lt10 32555 . . . . . . . 8 48 < 10
16774, 78, 163, 166dp2lt10 32555 . . . . . . 7 348 < 10
168 7p1e8 12365 . . . . . . 7 (7 + 1) = 8
1691, 79, 61, 167, 168dplti 32576 . . . . . 6 (7.348) < 8
17058, 62sselii 3974 . . . . . . 7 8 โˆˆ โ„
17112, 170, 18lttri 11344 . . . . . 6 (((7.348) < 8 โˆง 8 < 10) โ†’ (7.348) < 10)
172169, 165, 171mp2an 689 . . . . 5 (7.348) < 10
17327, 26deccl 12696 . . . . . . . . . 10 10 โˆˆ โ„•0
174173numexp0 17018 . . . . . . . . 9 (10โ†‘0) = 1
175 0z 12573 . . . . . . . . . . 11 0 โˆˆ โ„ค
17618, 175, 1463pm3.2i 1336 . . . . . . . . . 10 (10 โˆˆ โ„ โˆง 0 โˆˆ โ„ค โˆง 27 โˆˆ โ„ค)
177 1lt10 12820 . . . . . . . . . . 11 1 < 10
178177, 141pm3.2i 470 . . . . . . . . . 10 (1 < 10 โˆง 0 < 27)
179 ltexp2a 14136 . . . . . . . . . 10 (((10 โˆˆ โ„ โˆง 0 โˆˆ โ„ค โˆง 27 โˆˆ โ„ค) โˆง (1 < 10 โˆง 0 < 27)) โ†’ (10โ†‘0) < (10โ†‘27))
180176, 178, 179mp2an 689 . . . . . . . . 9 (10โ†‘0) < (10โ†‘27)
181174, 180eqbrtrri 5164 . . . . . . . 8 1 < (10โ†‘27)
182 loggt0b 26521 . . . . . . . . 9 ((10โ†‘27) โˆˆ โ„+ โ†’ (0 < (logโ€˜(10โ†‘27)) โ†” 1 < (10โ†‘27)))
18349, 182ax-mp 5 . . . . . . . 8 (0 < (logโ€˜(10โ†‘27)) โ†” 1 < (10โ†‘27))
184181, 183mpbir 230 . . . . . . 7 0 < (logโ€˜(10โ†‘27))
18551, 52divgt0i 12126 . . . . . . 7 ((0 < (logโ€˜(10โ†‘27)) โˆง 0 < (โˆšโ€˜(10โ†‘27))) โ†’ 0 < ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))))
186184, 53, 185mp2an 689 . . . . . 6 0 < ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))
18712, 18, 55ltmul1i 12136 . . . . . 6 (0 < ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))) โ†’ ((7.348) < 10 โ†” ((7.348) ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))) < (10 ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))))))
188186, 187ax-mp 5 . . . . 5 ((7.348) < 10 โ†” ((7.348) ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))) < (10 ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))))
189172, 188mpbi 229 . . . 4 ((7.348) ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))) < (10 ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))))
19018recni 11232 . . . . . . . . . . . . 13 10 โˆˆ โ„‚
191 expmul 14078 . . . . . . . . . . . . 13 ((10 โˆˆ โ„‚ โˆง 7 โˆˆ โ„•0 โˆง 2 โˆˆ โ„•0) โ†’ (10โ†‘(7 ยท 2)) = ((10โ†‘7)โ†‘2))
192190, 1, 19, 191mp3an 1457 . . . . . . . . . . . 12 (10โ†‘(7 ยท 2)) = ((10โ†‘7)โ†‘2)
193 7t2e14 12790 . . . . . . . . . . . . 13 (7 ยท 2) = 14
194193oveq2i 7416 . . . . . . . . . . . 12 (10โ†‘(7 ยท 2)) = (10โ†‘14)
195192, 194eqtr3i 2756 . . . . . . . . . . 11 ((10โ†‘7)โ†‘2) = (10โ†‘14)
196195fveq2i 6888 . . . . . . . . . 10 (โˆšโ€˜((10โ†‘7)โ†‘2)) = (โˆšโ€˜(10โ†‘14))
197 reexpcl 14049 . . . . . . . . . . . 12 ((10 โˆˆ โ„ โˆง 7 โˆˆ โ„•0) โ†’ (10โ†‘7) โˆˆ โ„)
19818, 1, 197mp2an 689 . . . . . . . . . . 11 (10โ†‘7) โˆˆ โ„
1991nn0zi 12591 . . . . . . . . . . . . 13 7 โˆˆ โ„ค
200 expgt0 14066 . . . . . . . . . . . . 13 ((10 โˆˆ โ„ โˆง 7 โˆˆ โ„ค โˆง 0 < 10) โ†’ 0 < (10โ†‘7))
20118, 199, 123, 200mp3an 1457 . . . . . . . . . . . 12 0 < (10โ†‘7)
20216, 198, 201ltleii 11341 . . . . . . . . . . 11 0 โ‰ค (10โ†‘7)
203 sqrtsq 15222 . . . . . . . . . . 11 (((10โ†‘7) โˆˆ โ„ โˆง 0 โ‰ค (10โ†‘7)) โ†’ (โˆšโ€˜((10โ†‘7)โ†‘2)) = (10โ†‘7))
204198, 202, 203mp2an 689 . . . . . . . . . 10 (โˆšโ€˜((10โ†‘7)โ†‘2)) = (10โ†‘7)
205196, 204eqtr3i 2756 . . . . . . . . 9 (โˆšโ€˜(10โ†‘14)) = (10โ†‘7)
20627, 59deccl 12696 . . . . . . . . . . . . 13 14 โˆˆ โ„•0
207206nn0zi 12591 . . . . . . . . . . . 12 14 โˆˆ โ„ค
20818, 207, 1463pm3.2i 1336 . . . . . . . . . . 11 (10 โˆˆ โ„ โˆง 14 โˆˆ โ„ค โˆง 27 โˆˆ โ„ค)
209 1lt2 12387 . . . . . . . . . . . . 13 1 < 2
21027, 19, 59, 1, 164, 209decltc 12710 . . . . . . . . . . . 12 14 < 27
211177, 210pm3.2i 470 . . . . . . . . . . 11 (1 < 10 โˆง 14 < 27)
212 ltexp2a 14136 . . . . . . . . . . 11 (((10 โˆˆ โ„ โˆง 14 โˆˆ โ„ค โˆง 27 โˆˆ โ„ค) โˆง (1 < 10 โˆง 14 < 27)) โ†’ (10โ†‘14) < (10โ†‘27))
213208, 211, 212mp2an 689 . . . . . . . . . 10 (10โ†‘14) < (10โ†‘27)
214 reexpcl 14049 . . . . . . . . . . . . 13 ((10 โˆˆ โ„ โˆง 14 โˆˆ โ„•0) โ†’ (10โ†‘14) โˆˆ โ„)
21518, 206, 214mp2an 689 . . . . . . . . . . . 12 (10โ†‘14) โˆˆ โ„
216 expgt0 14066 . . . . . . . . . . . . . 14 ((10 โˆˆ โ„ โˆง 14 โˆˆ โ„ค โˆง 0 < 10) โ†’ 0 < (10โ†‘14))
21718, 207, 123, 216mp3an 1457 . . . . . . . . . . . . 13 0 < (10โ†‘14)
21816, 215, 217ltleii 11341 . . . . . . . . . . . 12 0 โ‰ค (10โ†‘14)
219215, 218pm3.2i 470 . . . . . . . . . . 11 ((10โ†‘14) โˆˆ โ„ โˆง 0 โ‰ค (10โ†‘14))
22016, 22, 36ltleii 11341 . . . . . . . . . . . 12 0 โ‰ค (10โ†‘27)
22122, 220pm3.2i 470 . . . . . . . . . . 11 ((10โ†‘27) โˆˆ โ„ โˆง 0 โ‰ค (10โ†‘27))
222 sqrtlt 15214 . . . . . . . . . . 11 ((((10โ†‘14) โˆˆ โ„ โˆง 0 โ‰ค (10โ†‘14)) โˆง ((10โ†‘27) โˆˆ โ„ โˆง 0 โ‰ค (10โ†‘27))) โ†’ ((10โ†‘14) < (10โ†‘27) โ†” (โˆšโ€˜(10โ†‘14)) < (โˆšโ€˜(10โ†‘27))))
223219, 221, 222mp2an 689 . . . . . . . . . 10 ((10โ†‘14) < (10โ†‘27) โ†” (โˆšโ€˜(10โ†‘14)) < (โˆšโ€˜(10โ†‘27)))
224213, 223mpbi 229 . . . . . . . . 9 (โˆšโ€˜(10โ†‘14)) < (โˆšโ€˜(10โ†‘27))
225205, 224eqbrtrri 5164 . . . . . . . 8 (10โ†‘7) < (โˆšโ€˜(10โ†‘27))
226198, 201pm3.2i 470 . . . . . . . . 9 ((10โ†‘7) โˆˆ โ„ โˆง 0 < (10โ†‘7))
22752, 53pm3.2i 470 . . . . . . . . 9 ((โˆšโ€˜(10โ†‘27)) โˆˆ โ„ โˆง 0 < (โˆšโ€˜(10โ†‘27)))
22851, 184pm3.2i 470 . . . . . . . . 9 ((logโ€˜(10โ†‘27)) โˆˆ โ„ โˆง 0 < (logโ€˜(10โ†‘27)))
229 ltdiv2 12104 . . . . . . . . 9 ((((10โ†‘7) โˆˆ โ„ โˆง 0 < (10โ†‘7)) โˆง ((โˆšโ€˜(10โ†‘27)) โˆˆ โ„ โˆง 0 < (โˆšโ€˜(10โ†‘27))) โˆง ((logโ€˜(10โ†‘27)) โˆˆ โ„ โˆง 0 < (logโ€˜(10โ†‘27)))) โ†’ ((10โ†‘7) < (โˆšโ€˜(10โ†‘27)) โ†” ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))) < ((logโ€˜(10โ†‘27)) / (10โ†‘7))))
230226, 227, 228, 229mp3an 1457 . . . . . . . 8 ((10โ†‘7) < (โˆšโ€˜(10โ†‘27)) โ†” ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))) < ((logโ€˜(10โ†‘27)) / (10โ†‘7)))
231225, 230mpbi 229 . . . . . . 7 ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))) < ((logโ€˜(10โ†‘27)) / (10โ†‘7))
232 6nn 12305 . . . . . . . . . . . . . 14 6 โˆˆ โ„•
233232nngt0i 12255 . . . . . . . . . . . . . 14 0 < 6
23427, 26, 232, 233declt 12709 . . . . . . . . . . . . 13 10 < 16
235 6nn0 12497 . . . . . . . . . . . . . . . . 17 6 โˆˆ โ„•0
23627, 235deccl 12696 . . . . . . . . . . . . . . . 16 16 โˆˆ โ„•0
237236nn0rei 12487 . . . . . . . . . . . . . . 15 16 โˆˆ โ„
23825, 235, 26, 123declti 12719 . . . . . . . . . . . . . . 15 0 < 16
239 elrp 12982 . . . . . . . . . . . . . . 15 (16 โˆˆ โ„+ โ†” (16 โˆˆ โ„ โˆง 0 < 16))
240237, 238, 239mpbir2an 708 . . . . . . . . . . . . . 14 16 โˆˆ โ„+
241 logltb 26489 . . . . . . . . . . . . . 14 ((10 โˆˆ โ„+ โˆง 16 โˆˆ โ„+) โ†’ (10 < 16 โ†” (logโ€˜10) < (logโ€˜16)))
242125, 240, 241mp2an 689 . . . . . . . . . . . . 13 (10 < 16 โ†” (logโ€˜10) < (logโ€˜16))
243234, 242mpbi 229 . . . . . . . . . . . 12 (logโ€˜10) < (logโ€˜16)
244 2exp4 17027 . . . . . . . . . . . . . 14 (2โ†‘4) = 16
245244fveq2i 6888 . . . . . . . . . . . . 13 (logโ€˜(2โ†‘4)) = (logโ€˜16)
246 2rp 12985 . . . . . . . . . . . . . 14 2 โˆˆ โ„+
24759nn0zi 12591 . . . . . . . . . . . . . 14 4 โˆˆ โ„ค
248 relogexp 26485 . . . . . . . . . . . . . 14 ((2 โˆˆ โ„+ โˆง 4 โˆˆ โ„ค) โ†’ (logโ€˜(2โ†‘4)) = (4 ยท (logโ€˜2)))
249246, 247, 248mp2an 689 . . . . . . . . . . . . 13 (logโ€˜(2โ†‘4)) = (4 ยท (logโ€˜2))
250245, 249eqtr3i 2756 . . . . . . . . . . . 12 (logโ€˜16) = (4 ยท (logโ€˜2))
251243, 250breqtri 5166 . . . . . . . . . . 11 (logโ€˜10) < (4 ยท (logโ€˜2))
252100simpli 483 . . . . . . . . . . . . . . 15 2 < e
253 logltb 26489 . . . . . . . . . . . . . . . 16 ((2 โˆˆ โ„+ โˆง e โˆˆ โ„+) โ†’ (2 < e โ†” (logโ€˜2) < (logโ€˜e)))
254246, 102, 253mp2an 689 . . . . . . . . . . . . . . 15 (2 < e โ†” (logโ€˜2) < (logโ€˜e))
255252, 254mpbi 229 . . . . . . . . . . . . . 14 (logโ€˜2) < (logโ€˜e)
256255, 99breqtri 5166 . . . . . . . . . . . . 13 (logโ€˜2) < 1
257 4pos 12323 . . . . . . . . . . . . . 14 0 < 4
258 relogcl 26464 . . . . . . . . . . . . . . . 16 (2 โˆˆ โ„+ โ†’ (logโ€˜2) โˆˆ โ„)
259246, 258ax-mp 5 . . . . . . . . . . . . . . 15 (logโ€˜2) โˆˆ โ„
260259, 28, 3ltmul2i 12139 . . . . . . . . . . . . . 14 (0 < 4 โ†’ ((logโ€˜2) < 1 โ†” (4 ยท (logโ€˜2)) < (4 ยท 1)))
261257, 260ax-mp 5 . . . . . . . . . . . . 13 ((logโ€˜2) < 1 โ†” (4 ยท (logโ€˜2)) < (4 ยท 1))
262256, 261mpbi 229 . . . . . . . . . . . 12 (4 ยท (logโ€˜2)) < (4 ยท 1)
263 4cn 12301 . . . . . . . . . . . . 13 4 โˆˆ โ„‚
264263mulridi 11222 . . . . . . . . . . . 12 (4 ยท 1) = 4
265262, 264breqtri 5166 . . . . . . . . . . 11 (4 ยท (logโ€˜2)) < 4
2663, 259remulcli 11234 . . . . . . . . . . . 12 (4 ยท (logโ€˜2)) โˆˆ โ„
267134, 266, 3lttri 11344 . . . . . . . . . . 11 (((logโ€˜10) < (4 ยท (logโ€˜2)) โˆง (4 ยท (logโ€˜2)) < 4) โ†’ (logโ€˜10) < 4)
268251, 265, 267mp2an 689 . . . . . . . . . 10 (logโ€˜10) < 4
269134, 3, 92ltmul2i 12139 . . . . . . . . . . 11 (0 < 27 โ†’ ((logโ€˜10) < 4 โ†” (27 ยท (logโ€˜10)) < (27 ยท 4)))
270141, 269ax-mp 5 . . . . . . . . . 10 ((logโ€˜10) < 4 โ†” (27 ยท (logโ€˜10)) < (27 ยท 4))
271268, 270mpbi 229 . . . . . . . . 9 (27 ยท (logโ€˜10)) < (27 ยท 4)
272148, 271eqbrtri 5162 . . . . . . . 8 (logโ€˜(10โ†‘27)) < (27 ยท 4)
27392, 3remulcli 11234 . . . . . . . . . 10 (27 ยท 4) โˆˆ โ„
27451, 273, 198ltdiv1i 12137 . . . . . . . . 9 (0 < (10โ†‘7) โ†’ ((logโ€˜(10โ†‘27)) < (27 ยท 4) โ†” ((logโ€˜(10โ†‘27)) / (10โ†‘7)) < ((27 ยท 4) / (10โ†‘7))))
275201, 274ax-mp 5 . . . . . . . 8 ((logโ€˜(10โ†‘27)) < (27 ยท 4) โ†” ((logโ€˜(10โ†‘27)) / (10โ†‘7)) < ((27 ยท 4) / (10โ†‘7)))
276272, 275mpbi 229 . . . . . . 7 ((logโ€˜(10โ†‘27)) / (10โ†‘7)) < ((27 ยท 4) / (10โ†‘7))
27716, 201gtneii 11330 . . . . . . . . 9 (10โ†‘7) โ‰  0
27851, 198, 277redivcli 11985 . . . . . . . 8 ((logโ€˜(10โ†‘27)) / (10โ†‘7)) โˆˆ โ„
279273, 198, 277redivcli 11985 . . . . . . . 8 ((27 ยท 4) / (10โ†‘7)) โˆˆ โ„
28055, 278, 279lttri 11344 . . . . . . 7 ((((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))) < ((logโ€˜(10โ†‘27)) / (10โ†‘7)) โˆง ((logโ€˜(10โ†‘27)) / (10โ†‘7)) < ((27 ยท 4) / (10โ†‘7))) โ†’ ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))) < ((27 ยท 4) / (10โ†‘7)))
281231, 276, 280mp2an 689 . . . . . 6 ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))) < ((27 ยท 4) / (10โ†‘7))
282 7lt10 12814 . . . . . . . . . 10 7 < 10
283 2lt10 12819 . . . . . . . . . 10 2 < 10
28419, 173, 1, 26, 282, 283decltc 12710 . . . . . . . . 9 27 < 100
285 10nn 12697 . . . . . . . . . . . . 13 10 โˆˆ โ„•
286285decnncl2 12705 . . . . . . . . . . . 12 100 โˆˆ โ„•
287286nnrei 12225 . . . . . . . . . . 11 100 โˆˆ โ„
28892, 287, 3ltmul1i 12136 . . . . . . . . . 10 (0 < 4 โ†’ (27 < 100 โ†” (27 ยท 4) < (100 ยท 4)))
289257, 288ax-mp 5 . . . . . . . . 9 (27 < 100 โ†” (27 ยท 4) < (100 ยท 4))
290284, 289mpbi 229 . . . . . . . 8 (27 ยท 4) < (100 ยท 4)
291287, 3remulcli 11234 . . . . . . . . . 10 (100 ยท 4) โˆˆ โ„
292273, 291, 198ltdiv1i 12137 . . . . . . . . 9 (0 < (10โ†‘7) โ†’ ((27 ยท 4) < (100 ยท 4) โ†” ((27 ยท 4) / (10โ†‘7)) < ((100 ยท 4) / (10โ†‘7))))
293201, 292ax-mp 5 . . . . . . . 8 ((27 ยท 4) < (100 ยท 4) โ†” ((27 ยท 4) / (10โ†‘7)) < ((100 ยท 4) / (10โ†‘7)))
294290, 293mpbi 229 . . . . . . 7 ((27 ยท 4) / (10โ†‘7)) < ((100 ยท 4) / (10โ†‘7))
295 8nn 12311 . . . . . . . . . . . . . . 15 8 โˆˆ โ„•
296 nnrp 12991 . . . . . . . . . . . . . . 15 (8 โˆˆ โ„• โ†’ 8 โˆˆ โ„+)
297295, 296ax-mp 5 . . . . . . . . . . . . . 14 8 โˆˆ โ„+
29859, 297rpdp2cl 32553 . . . . . . . . . . . . 13 48 โˆˆ โ„+
29919, 298rpdp2cl 32553 . . . . . . . . . . . 12 248 โˆˆ โ„+
30019, 299rpdp2cl 32553 . . . . . . . . . . 11 2248 โˆˆ โ„+
30159, 300dpgti 32577 . . . . . . . . . 10 4 < (4.2248)
30272recni 11232 . . . . . . . . . . . . 13 (0.00042248) โˆˆ โ„‚
303198recni 11232 . . . . . . . . . . . . 13 (10โ†‘7) โˆˆ โ„‚
304302, 303mulcli 11225 . . . . . . . . . . . 12 ((0.00042248) ยท (10โ†‘7)) โˆˆ โ„‚
30516, 123gtneii 11330 . . . . . . . . . . . . 13 10 โ‰  0
306190, 305pm3.2i 470 . . . . . . . . . . . 12 (10 โˆˆ โ„‚ โˆง 10 โ‰  0)
307287recni 11232 . . . . . . . . . . . . 13 100 โˆˆ โ„‚
308286nnne0i 12256 . . . . . . . . . . . . 13 100 โ‰  0
309307, 308pm3.2i 470 . . . . . . . . . . . 12 (100 โˆˆ โ„‚ โˆง 100 โ‰  0)
310 divdiv1 11929 . . . . . . . . . . . 12 ((((0.00042248) ยท (10โ†‘7)) โˆˆ โ„‚ โˆง (10 โˆˆ โ„‚ โˆง 10 โ‰  0) โˆง (100 โˆˆ โ„‚ โˆง 100 โ‰  0)) โ†’ ((((0.00042248) ยท (10โ†‘7)) / 10) / 100) = (((0.00042248) ยท (10โ†‘7)) / (10 ยท 100)))
311304, 306, 309, 310mp3an 1457 . . . . . . . . . . 11 ((((0.00042248) ยท (10โ†‘7)) / 10) / 100) = (((0.00042248) ยท (10โ†‘7)) / (10 ยท 100))
312302, 303, 190, 305div23i 11976 . . . . . . . . . . . 12 (((0.00042248) ยท (10โ†‘7)) / 10) = (((0.00042248) / 10) ยท (10โ†‘7))
313312oveq1i 7415 . . . . . . . . . . 11 ((((0.00042248) ยท (10โ†‘7)) / 10) / 100) = ((((0.00042248) / 10) ยท (10โ†‘7)) / 100)
314190, 307mulcli 11225 . . . . . . . . . . . . 13 (10 ยท 100) โˆˆ โ„‚
315190, 307, 305, 308mulne0i 11861 . . . . . . . . . . . . 13 (10 ยท 100) โ‰  0
316302, 303, 314, 315divassi 11974 . . . . . . . . . . . 12 (((0.00042248) ยท (10โ†‘7)) / (10 ยท 100)) = ((0.00042248) ยท ((10โ†‘7) / (10 ยท 100)))
317 expp1 14039 . . . . . . . . . . . . . . . . . 18 ((10 โˆˆ โ„‚ โˆง 2 โˆˆ โ„•0) โ†’ (10โ†‘(2 + 1)) = ((10โ†‘2) ยท 10))
318190, 19, 317mp2an 689 . . . . . . . . . . . . . . . . 17 (10โ†‘(2 + 1)) = ((10โ†‘2) ยท 10)
319 sq10 14229 . . . . . . . . . . . . . . . . . 18 (10โ†‘2) = 100
320319oveq1i 7415 . . . . . . . . . . . . . . . . 17 ((10โ†‘2) ยท 10) = (100 ยท 10)
321307, 190mulcomi 11226 . . . . . . . . . . . . . . . . 17 (100 ยท 10) = (10 ยท 100)
322318, 320, 3213eqtrri 2759 . . . . . . . . . . . . . . . 16 (10 ยท 100) = (10โ†‘(2 + 1))
323 2p1e3 12358 . . . . . . . . . . . . . . . . 17 (2 + 1) = 3
324323oveq2i 7416 . . . . . . . . . . . . . . . 16 (10โ†‘(2 + 1)) = (10โ†‘3)
325322, 324eqtri 2754 . . . . . . . . . . . . . . 15 (10 ยท 100) = (10โ†‘3)
326325oveq2i 7416 . . . . . . . . . . . . . 14 ((10โ†‘7) / (10 ยท 100)) = ((10โ†‘7) / (10โ†‘3))
32774nn0zi 12591 . . . . . . . . . . . . . . . 16 3 โˆˆ โ„ค
328199, 327pm3.2i 470 . . . . . . . . . . . . . . 15 (7 โˆˆ โ„ค โˆง 3 โˆˆ โ„ค)
329 expsub 14081 . . . . . . . . . . . . . . 15 (((10 โˆˆ โ„‚ โˆง 10 โ‰  0) โˆง (7 โˆˆ โ„ค โˆง 3 โˆˆ โ„ค)) โ†’ (10โ†‘(7 โˆ’ 3)) = ((10โ†‘7) / (10โ†‘3)))
330306, 328, 329mp2an 689 . . . . . . . . . . . . . 14 (10โ†‘(7 โˆ’ 3)) = ((10โ†‘7) / (10โ†‘3))
331 7cn 12310 . . . . . . . . . . . . . . . 16 7 โˆˆ โ„‚
332 4p3e7 12370 . . . . . . . . . . . . . . . . 17 (4 + 3) = 7
333263, 112, 332addcomli 11410 . . . . . . . . . . . . . . . 16 (3 + 4) = 7
334331, 112, 263, 333subaddrii 11553 . . . . . . . . . . . . . . 15 (7 โˆ’ 3) = 4
335334oveq2i 7416 . . . . . . . . . . . . . 14 (10โ†‘(7 โˆ’ 3)) = (10โ†‘4)
336326, 330, 3353eqtr2i 2760 . . . . . . . . . . . . 13 ((10โ†‘7) / (10 ยท 100)) = (10โ†‘4)
337336oveq2i 7416 . . . . . . . . . . . 12 ((0.00042248) ยท ((10โ†‘7) / (10 ยท 100))) = ((0.00042248) ยท (10โ†‘4))
338173numexp1 17019 . . . . . . . . . . . . . 14 (10โ†‘1) = 10
339338oveq2i 7416 . . . . . . . . . . . . 13 ((0.42248) ยท (10โ†‘1)) = ((0.42248) ยท 10)
34059, 300rpdp2cl 32553 . . . . . . . . . . . . . . 15 42248 โˆˆ โ„+
34125nnzi 12590 . . . . . . . . . . . . . . 15 1 โˆˆ โ„ค
34289nnzi 12590 . . . . . . . . . . . . . . 15 2 โˆˆ โ„ค
34326, 340, 98, 341, 342dpexpp1 32579 . . . . . . . . . . . . . 14 ((0.42248) ยท (10โ†‘1)) = ((0.042248) ยท (10โ†‘2))
34426, 340rpdp2cl 32553 . . . . . . . . . . . . . . 15 042248 โˆˆ โ„+
34526, 344, 323, 342, 327dpexpp1 32579 . . . . . . . . . . . . . 14 ((0.042248) ยท (10โ†‘2)) = ((0.0042248) ยท (10โ†‘3))
34626, 344rpdp2cl 32553 . . . . . . . . . . . . . . 15 0042248 โˆˆ โ„+
347 3p1e4 12361 . . . . . . . . . . . . . . 15 (3 + 1) = 4
34826, 346, 347, 327, 247dpexpp1 32579 . . . . . . . . . . . . . 14 ((0.0042248) ยท (10โ†‘3)) = ((0.00042248) ยท (10โ†‘4))
349343, 345, 3483eqtri 2758 . . . . . . . . . . . . 13 ((0.42248) ยท (10โ†‘1)) = ((0.00042248) ยท (10โ†‘4))
35059, 3000dp2dp 32580 . . . . . . . . . . . . 13 ((0.42248) ยท 10) = (4.2248)
351339, 349, 3503eqtr3i 2762 . . . . . . . . . . . 12 ((0.00042248) ยท (10โ†‘4)) = (4.2248)
352316, 337, 3513eqtri 2758 . . . . . . . . . . 11 (((0.00042248) ยท (10โ†‘7)) / (10 ยท 100)) = (4.2248)
353311, 313, 3523eqtr3i 2762 . . . . . . . . . 10 ((((0.00042248) / 10) ยท (10โ†‘7)) / 100) = (4.2248)
354301, 353breqtrri 5168 . . . . . . . . 9 4 < ((((0.00042248) / 10) ยท (10โ†‘7)) / 100)
35572, 18, 305redivcli 11985 . . . . . . . . . . 11 ((0.00042248) / 10) โˆˆ โ„
356355, 198remulcli 11234 . . . . . . . . . 10 (((0.00042248) / 10) ยท (10โ†‘7)) โˆˆ โ„
357286nngt0i 12255 . . . . . . . . . . 11 0 < 100
358287, 357pm3.2i 470 . . . . . . . . . 10 (100 โˆˆ โ„ โˆง 0 < 100)
359 ltmuldiv2 12092 . . . . . . . . . 10 ((4 โˆˆ โ„ โˆง (((0.00042248) / 10) ยท (10โ†‘7)) โˆˆ โ„ โˆง (100 โˆˆ โ„ โˆง 0 < 100)) โ†’ ((100 ยท 4) < (((0.00042248) / 10) ยท (10โ†‘7)) โ†” 4 < ((((0.00042248) / 10) ยท (10โ†‘7)) / 100)))
3603, 356, 358, 359mp3an 1457 . . . . . . . . 9 ((100 ยท 4) < (((0.00042248) / 10) ยท (10โ†‘7)) โ†” 4 < ((((0.00042248) / 10) ยท (10โ†‘7)) / 100))
361354, 360mpbir 230 . . . . . . . 8 (100 ยท 4) < (((0.00042248) / 10) ยท (10โ†‘7))
362 ltdivmul2 12095 . . . . . . . . 9 (((100 ยท 4) โˆˆ โ„ โˆง ((0.00042248) / 10) โˆˆ โ„ โˆง ((10โ†‘7) โˆˆ โ„ โˆง 0 < (10โ†‘7))) โ†’ (((100 ยท 4) / (10โ†‘7)) < ((0.00042248) / 10) โ†” (100 ยท 4) < (((0.00042248) / 10) ยท (10โ†‘7))))
363291, 355, 226, 362mp3an 1457 . . . . . . . 8 (((100 ยท 4) / (10โ†‘7)) < ((0.00042248) / 10) โ†” (100 ยท 4) < (((0.00042248) / 10) ยท (10โ†‘7)))
364361, 363mpbir 230 . . . . . . 7 ((100 ยท 4) / (10โ†‘7)) < ((0.00042248) / 10)
365291, 198, 277redivcli 11985 . . . . . . . 8 ((100 ยท 4) / (10โ†‘7)) โˆˆ โ„
366279, 365, 355lttri 11344 . . . . . . 7 ((((27 ยท 4) / (10โ†‘7)) < ((100 ยท 4) / (10โ†‘7)) โˆง ((100 ยท 4) / (10โ†‘7)) < ((0.00042248) / 10)) โ†’ ((27 ยท 4) / (10โ†‘7)) < ((0.00042248) / 10))
367294, 364, 366mp2an 689 . . . . . 6 ((27 ยท 4) / (10โ†‘7)) < ((0.00042248) / 10)
368226simpli 483 . . . . . . . 8 (10โ†‘7) โˆˆ โ„
369273, 368, 277redivcli 11985 . . . . . . 7 ((27 ยท 4) / (10โ†‘7)) โˆˆ โ„
37055, 369, 355lttri 11344 . . . . . 6 ((((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))) < ((27 ยท 4) / (10โ†‘7)) โˆง ((27 ยท 4) / (10โ†‘7)) < ((0.00042248) / 10)) โ†’ ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))) < ((0.00042248) / 10))
371281, 367, 370mp2an 689 . . . . 5 ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))) < ((0.00042248) / 10)
372125, 124mpbi 229 . . . . . 6 (10 โˆˆ โ„ โˆง 0 < 10)
373 ltmuldiv2 12092 . . . . . 6 ((((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))) โˆˆ โ„ โˆง (0.00042248) โˆˆ โ„ โˆง (10 โˆˆ โ„ โˆง 0 < 10)) โ†’ ((10 ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))) < (0.00042248) โ†” ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))) < ((0.00042248) / 10)))
37455, 72, 372, 373mp3an 1457 . . . . 5 ((10 ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))) < (0.00042248) โ†” ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))) < ((0.00042248) / 10))
375371, 374mpbir 230 . . . 4 (10 ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))) < (0.00042248)
37612, 55remulcli 11234 . . . . 5 ((7.348) ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))) โˆˆ โ„
37718, 55remulcli 11234 . . . . 5 (10 ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))) โˆˆ โ„
378376, 377, 72lttri 11344 . . . 4 ((((7.348) ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))) < (10 ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))) โˆง (10 ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))) < (0.00042248)) โ†’ ((7.348) ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))) < (0.00042248))
379189, 375, 378mp2an 689 . . 3 ((7.348) ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))) < (0.00042248)
380379a1i 11 . 2 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ((7.348) ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))) < (0.00042248))
38147, 57, 73, 162, 380lelttrd 11376 1 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ((7.348) ยท ((logโ€˜๐‘) / (โˆšโ€˜๐‘))) < (0.00042248))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098   โ‰  wne 2934   class class class wbr 5141  โ€˜cfv 6537  (class class class)co 7405  โ„‚cc 11110  โ„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   ยท cmul 11117   < clt 11252   โ‰ค cle 11253   โˆ’ cmin 11448   / cdiv 11875  โ„•cn 12216  2c2 12271  3c3 12272  4c4 12273  6c6 12275  7c7 12276  8c8 12277  9c9 12278  โ„•0cn0 12476  โ„คcz 12562  cdc 12681  โ„šcq 12936  โ„+crp 12980  โ†‘cexp 14032  โˆšcsqrt 15186  expce 16011  eceu 16012  logclog 26443  cdp2 32542  .cdp 32559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-inf2 9638  ax-cc 10432  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-symdif 4237  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-iin 4993  df-disj 5107  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7667  df-ofr 7668  df-om 7853  df-1st 7974  df-2nd 7975  df-supp 8147  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-2o 8468  df-oadd 8471  df-omul 8472  df-er 8705  df-map 8824  df-pm 8825  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-fi 9408  df-sup 9439  df-inf 9440  df-oi 9507  df-dju 9898  df-card 9936  df-acn 9939  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-q 12937  df-rp 12981  df-xneg 13098  df-xadd 13099  df-xmul 13100  df-ioo 13334  df-ioc 13335  df-ico 13336  df-icc 13337  df-fz 13491  df-fzo 13634  df-fl 13763  df-mod 13841  df-seq 13973  df-exp 14033  df-fac 14239  df-bc 14268  df-hash 14296  df-shft 15020  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-limsup 15421  df-clim 15438  df-rlim 15439  df-sum 15639  df-ef 16017  df-e 16018  df-sin 16019  df-cos 16020  df-tan 16021  df-pi 16022  df-struct 17089  df-sets 17106  df-slot 17124  df-ndx 17136  df-base 17154  df-ress 17183  df-plusg 17219  df-mulr 17220  df-starv 17221  df-sca 17222  df-vsca 17223  df-ip 17224  df-tset 17225  df-ple 17226  df-ds 17228  df-unif 17229  df-hom 17230  df-cco 17231  df-rest 17377  df-topn 17378  df-0g 17396  df-gsum 17397  df-topgen 17398  df-pt 17399  df-prds 17402  df-xrs 17457  df-qtop 17462  df-imas 17463  df-xps 17465  df-mre 17539  df-mrc 17540  df-acs 17542  df-mgm 18573  df-sgrp 18652  df-mnd 18668  df-submnd 18714  df-mulg 18996  df-cntz 19233  df-cmn 19702  df-psmet 21232  df-xmet 21233  df-met 21234  df-bl 21235  df-mopn 21236  df-fbas 21237  df-fg 21238  df-cnfld 21241  df-top 22751  df-topon 22768  df-topsp 22790  df-bases 22804  df-cld 22878  df-ntr 22879  df-cls 22880  df-nei 22957  df-lp 22995  df-perf 22996  df-cn 23086  df-cnp 23087  df-haus 23174  df-cmp 23246  df-tx 23421  df-hmeo 23614  df-fil 23705  df-fm 23797  df-flim 23798  df-flf 23799  df-xms 24181  df-ms 24182  df-tms 24183  df-cncf 24753  df-ovol 25348  df-vol 25349  df-mbf 25503  df-itg1 25504  df-itg2 25505  df-ibl 25506  df-itg 25507  df-0p 25554  df-limc 25750  df-dv 25751  df-log 26445  df-cxp 26446  df-dp2 32543  df-dp 32560
This theorem is referenced by:  tgoldbachgtde  34201
  Copyright terms: Public domain W3C validator