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 33304
Description: Lemma for tgoldbachgtd 33315. (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 12442 . . . . 5 7 โˆˆ โ„•0
2 3re 12240 . . . . . . 7 3 โˆˆ โ„
3 4re 12244 . . . . . . . . 9 4 โˆˆ โ„
4 8re 12256 . . . . . . . . 9 8 โˆˆ โ„
53, 4pm3.2i 472 . . . . . . . 8 (4 โˆˆ โ„ โˆง 8 โˆˆ โ„)
6 dp2cl 31778 . . . . . . . 8 ((4 โˆˆ โ„ โˆง 8 โˆˆ โ„) โ†’ 48 โˆˆ โ„)
75, 6ax-mp 5 . . . . . . 7 48 โˆˆ โ„
82, 7pm3.2i 472 . . . . . 6 (3 โˆˆ โ„ โˆง 48 โˆˆ โ„)
9 dp2cl 31778 . . . . . 6 ((3 โˆˆ โ„ โˆง 48 โˆˆ โ„) โ†’ 348 โˆˆ โ„)
108, 9ax-mp 5 . . . . 5 348 โˆˆ โ„
11 dpcl 31789 . . . . 5 ((7 โˆˆ โ„•0 โˆง 348 โˆˆ โ„) โ†’ (7.348) โˆˆ โ„)
121, 10, 11mp2an 691 . . . 4 (7.348) โˆˆ โ„
1312a1i 11 . . 3 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ (7.348) โˆˆ โ„)
14 nn0re 12429 . . . . . . 7 (๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ โ„)
1514adantr 482 . . . . . 6 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ๐‘ โˆˆ โ„)
16 0re 11164 . . . . . . . 8 0 โˆˆ โ„
1716a1i 11 . . . . . . 7 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ 0 โˆˆ โ„)
18 10re 12644 . . . . . . . . 9 10 โˆˆ โ„
19 2nn0 12437 . . . . . . . . . 10 2 โˆˆ โ„•0
2019, 1deccl 12640 . . . . . . . . 9 27 โˆˆ โ„•0
21 reexpcl 13991 . . . . . . . . 9 ((10 โˆˆ โ„ โˆง 27 โˆˆ โ„•0) โ†’ (10โ†‘27) โˆˆ โ„)
2218, 20, 21mp2an 691 . . . . . . . 8 (10โ†‘27) โˆˆ โ„
2322a1i 11 . . . . . . 7 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ (10โ†‘27) โˆˆ โ„)
24 0lt1 11684 . . . . . . . . 9 0 < 1
25 1nn 12171 . . . . . . . . . . 11 1 โˆˆ โ„•
26 0nn0 12435 . . . . . . . . . . 11 0 โˆˆ โ„•0
27 1nn0 12436 . . . . . . . . . . 11 1 โˆˆ โ„•0
28 1re 11162 . . . . . . . . . . . 12 1 โˆˆ โ„
29 9re 12259 . . . . . . . . . . . 12 9 โˆˆ โ„
30 1lt9 12366 . . . . . . . . . . . 12 1 < 9
3128, 29, 30ltleii 11285 . . . . . . . . . . 11 1 โ‰ค 9
3225, 26, 27, 31declei 12661 . . . . . . . . . 10 1 โ‰ค 10
33 expge1 14012 . . . . . . . . . 10 ((10 โˆˆ โ„ โˆง 27 โˆˆ โ„•0 โˆง 1 โ‰ค 10) โ†’ 1 โ‰ค (10โ†‘27))
3418, 20, 32, 33mp3an 1462 . . . . . . . . 9 1 โ‰ค (10โ†‘27)
3516, 28, 22ltletri 11290 . . . . . . . . 9 ((0 < 1 โˆง 1 โ‰ค (10โ†‘27)) โ†’ 0 < (10โ†‘27))
3624, 34, 35mp2an 691 . . . . . . . 8 0 < (10โ†‘27)
3736a1i 11 . . . . . . 7 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ 0 < (10โ†‘27))
38 simpr 486 . . . . . . 7 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ (10โ†‘27) โ‰ค ๐‘)
3917, 23, 15, 37, 38ltletrd 11322 . . . . . 6 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ 0 < ๐‘)
4015, 39elrpd 12961 . . . . 5 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ๐‘ โˆˆ โ„+)
4140relogcld 25994 . . . 4 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ (logโ€˜๐‘) โˆˆ โ„)
4240rpge0d 12968 . . . . 5 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ 0 โ‰ค ๐‘)
4315, 42resqrtcld 15309 . . . 4 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ (โˆšโ€˜๐‘) โˆˆ โ„)
4440sqrtgt0d 15304 . . . . 5 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ 0 < (โˆšโ€˜๐‘))
4517, 44gtned 11297 . . . 4 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ (โˆšโ€˜๐‘) โ‰  0)
4641, 43, 45redivcld 11990 . . 3 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ((logโ€˜๐‘) / (โˆšโ€˜๐‘)) โˆˆ โ„)
4713, 46remulcld 11192 . 2 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ((7.348) ยท ((logโ€˜๐‘) / (โˆšโ€˜๐‘))) โˆˆ โ„)
48 elrp 12924 . . . . . . 7 ((10โ†‘27) โˆˆ โ„+ โ†” ((10โ†‘27) โˆˆ โ„ โˆง 0 < (10โ†‘27)))
4922, 36, 48mpbir2an 710 . . . . . 6 (10โ†‘27) โˆˆ โ„+
50 relogcl 25947 . . . . . 6 ((10โ†‘27) โˆˆ โ„+ โ†’ (logโ€˜(10โ†‘27)) โˆˆ โ„)
5149, 50ax-mp 5 . . . . 5 (logโ€˜(10โ†‘27)) โˆˆ โ„
5222, 36sqrtpclii 15274 . . . . 5 (โˆšโ€˜(10โ†‘27)) โˆˆ โ„
5322, 36sqrtgt0ii 15275 . . . . . 6 0 < (โˆšโ€˜(10โ†‘27))
5416, 53gtneii 11274 . . . . 5 (โˆšโ€˜(10โ†‘27)) โ‰  0
5551, 52, 54redivcli 11929 . . . 4 ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))) โˆˆ โ„
5655a1i 11 . . 3 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))) โˆˆ โ„)
5713, 56remulcld 11192 . 2 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ((7.348) ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))) โˆˆ โ„)
58 qssre 12891 . . . . 5 โ„š โŠ† โ„
59 4nn0 12439 . . . . . . . . 9 4 โˆˆ โ„•0
60 nn0ssq 12889 . . . . . . . . . . . . 13 โ„•0 โŠ† โ„š
61 8nn0 12443 . . . . . . . . . . . . 13 8 โˆˆ โ„•0
6260, 61sselii 3946 . . . . . . . . . . . 12 8 โˆˆ โ„š
6359, 62dp2clq 31779 . . . . . . . . . . 11 48 โˆˆ โ„š
6419, 63dp2clq 31779 . . . . . . . . . 10 248 โˆˆ โ„š
6519, 64dp2clq 31779 . . . . . . . . 9 2248 โˆˆ โ„š
6659, 65dp2clq 31779 . . . . . . . 8 42248 โˆˆ โ„š
6726, 66dp2clq 31779 . . . . . . 7 042248 โˆˆ โ„š
6826, 67dp2clq 31779 . . . . . 6 0042248 โˆˆ โ„š
6926, 68dp2clq 31779 . . . . 5 00042248 โˆˆ โ„š
7058, 69sselii 3946 . . . 4 00042248 โˆˆ โ„
71 dpcl 31789 . . . 4 ((0 โˆˆ โ„•0 โˆง 00042248 โˆˆ โ„) โ†’ (0.00042248) โˆˆ โ„)
7226, 70, 71mp2an 691 . . 3 (0.00042248) โˆˆ โ„
7372a1i 11 . 2 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ (0.00042248) โˆˆ โ„)
74 3nn0 12438 . . . . . . . . 9 3 โˆˆ โ„•0
75 8pos 12272 . . . . . . . . . . 11 0 < 8
76 elrp 12924 . . . . . . . . . . 11 (8 โˆˆ โ„+ โ†” (8 โˆˆ โ„ โˆง 0 < 8))
774, 75, 76mpbir2an 710 . . . . . . . . . 10 8 โˆˆ โ„+
7859, 77rpdp2cl 31780 . . . . . . . . 9 48 โˆˆ โ„+
7974, 78rpdp2cl 31780 . . . . . . . 8 348 โˆˆ โ„+
801, 79rpdpcl 31801 . . . . . . 7 (7.348) โˆˆ โ„+
81 elrp 12924 . . . . . . 7 ((7.348) โˆˆ โ„+ โ†” ((7.348) โˆˆ โ„ โˆง 0 < (7.348)))
8280, 81mpbi 229 . . . . . 6 ((7.348) โˆˆ โ„ โˆง 0 < (7.348))
8382simpri 487 . . . . 5 0 < (7.348)
8416, 12, 83ltleii 11285 . . . 4 0 โ‰ค (7.348)
8584a1i 11 . . 3 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ 0 โ‰ค (7.348))
8649a1i 11 . . . 4 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ (10โ†‘27) โˆˆ โ„+)
87 2cn 12235 . . . . . . . . . 10 2 โˆˆ โ„‚
8887mulid2i 11167 . . . . . . . . 9 (1 ยท 2) = 2
89 2nn 12233 . . . . . . . . . . 11 2 โˆˆ โ„•
9089, 1, 27, 31declei 12661 . . . . . . . . . 10 1 โ‰ค 27
91 2pos 12263 . . . . . . . . . . 11 0 < 2
9220nn0rei 12431 . . . . . . . . . . . 12 27 โˆˆ โ„
93 2re 12234 . . . . . . . . . . . 12 2 โˆˆ โ„
9428, 92, 93lemul1i 12084 . . . . . . . . . . 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 5133 . . . . . . . 8 2 โ‰ค (27 ยท 2)
98 1p1e2 12285 . . . . . . . . . . 11 (1 + 1) = 2
99 loge 25958 . . . . . . . . . . . . . 14 (logโ€˜e) = 1
100 egt2lt3 16095 . . . . . . . . . . . . . . . 16 (2 < e โˆง e < 3)
101100simpri 487 . . . . . . . . . . . . . . 15 e < 3
102 epr 16097 . . . . . . . . . . . . . . . 16 e โˆˆ โ„+
103 3rp 12928 . . . . . . . . . . . . . . . 16 3 โˆˆ โ„+
104 logltb 25971 . . . . . . . . . . . . . . . 16 ((e โˆˆ โ„+ โˆง 3 โˆˆ โ„+) โ†’ (e < 3 โ†” (logโ€˜e) < (logโ€˜3)))
105102, 103, 104mp2an 691 . . . . . . . . . . . . . . 15 (e < 3 โ†” (logโ€˜e) < (logโ€˜3))
106101, 105mpbi 229 . . . . . . . . . . . . . 14 (logโ€˜e) < (logโ€˜3)
10799, 106eqbrtrri 5133 . . . . . . . . . . . . 13 1 < (logโ€˜3)
108 relogcl 25947 . . . . . . . . . . . . . . 15 (3 โˆˆ โ„+ โ†’ (logโ€˜3) โˆˆ โ„)
109103, 108ax-mp 5 . . . . . . . . . . . . . 14 (logโ€˜3) โˆˆ โ„
11028, 28, 109, 109lt2addi 11724 . . . . . . . . . . . . 13 ((1 < (logโ€˜3) โˆง 1 < (logโ€˜3)) โ†’ (1 + 1) < ((logโ€˜3) + (logโ€˜3)))
111107, 107, 110mp2an 691 . . . . . . . . . . . 12 (1 + 1) < ((logโ€˜3) + (logโ€˜3))
112 3cn 12241 . . . . . . . . . . . . . 14 3 โˆˆ โ„‚
113 3ne0 12266 . . . . . . . . . . . . . 14 3 โ‰  0
114 logmul2 25987 . . . . . . . . . . . . . 14 ((3 โˆˆ โ„‚ โˆง 3 โ‰  0 โˆง 3 โˆˆ โ„+) โ†’ (logโ€˜(3 ยท 3)) = ((logโ€˜3) + (logโ€˜3)))
115112, 113, 103, 114mp3an 1462 . . . . . . . . . . . . 13 (logโ€˜(3 ยท 3)) = ((logโ€˜3) + (logโ€˜3))
116 3t3e9 12327 . . . . . . . . . . . . . . 15 (3 ยท 3) = 9
117116fveq2i 6850 . . . . . . . . . . . . . 14 (logโ€˜(3 ยท 3)) = (logโ€˜9)
118 9lt10 12756 . . . . . . . . . . . . . . . 16 9 < 10
11929, 18, 118ltleii 11285 . . . . . . . . . . . . . . 15 9 โ‰ค 10
120 9pos 12273 . . . . . . . . . . . . . . . . 17 0 < 9
121 elrp 12924 . . . . . . . . . . . . . . . . 17 (9 โˆˆ โ„+ โ†” (9 โˆˆ โ„ โˆง 0 < 9))
12229, 120, 121mpbir2an 710 . . . . . . . . . . . . . . . 16 9 โˆˆ โ„+
123 10pos 12642 . . . . . . . . . . . . . . . . 17 0 < 10
124 elrp 12924 . . . . . . . . . . . . . . . . 17 (10 โˆˆ โ„+ โ†” (10 โˆˆ โ„ โˆง 0 < 10))
12518, 123, 124mpbir2an 710 . . . . . . . . . . . . . . . 16 10 โˆˆ โ„+
126 logleb 25974 . . . . . . . . . . . . . . . 16 ((9 โˆˆ โ„+ โˆง 10 โˆˆ โ„+) โ†’ (9 โ‰ค 10 โ†” (logโ€˜9) โ‰ค (logโ€˜10)))
127122, 125, 126mp2an 691 . . . . . . . . . . . . . . 15 (9 โ‰ค 10 โ†” (logโ€˜9) โ‰ค (logโ€˜10))
128119, 127mpbi 229 . . . . . . . . . . . . . 14 (logโ€˜9) โ‰ค (logโ€˜10)
129117, 128eqbrtri 5131 . . . . . . . . . . . . 13 (logโ€˜(3 ยท 3)) โ‰ค (logโ€˜10)
130115, 129eqbrtrri 5133 . . . . . . . . . . . 12 ((logโ€˜3) + (logโ€˜3)) โ‰ค (logโ€˜10)
13128, 28readdcli 11177 . . . . . . . . . . . . 13 (1 + 1) โˆˆ โ„
132109, 109readdcli 11177 . . . . . . . . . . . . 13 ((logโ€˜3) + (logโ€˜3)) โˆˆ โ„
133 relogcl 25947 . . . . . . . . . . . . . 14 (10 โˆˆ โ„+ โ†’ (logโ€˜10) โˆˆ โ„)
134125, 133ax-mp 5 . . . . . . . . . . . . 13 (logโ€˜10) โˆˆ โ„
135131, 132, 134ltletri 11290 . . . . . . . . . . . 12 (((1 + 1) < ((logโ€˜3) + (logโ€˜3)) โˆง ((logโ€˜3) + (logโ€˜3)) โ‰ค (logโ€˜10)) โ†’ (1 + 1) < (logโ€˜10))
136111, 130, 135mp2an 691 . . . . . . . . . . 11 (1 + 1) < (logโ€˜10)
13798, 136eqbrtrri 5133 . . . . . . . . . 10 2 < (logโ€˜10)
13893, 134ltlei 11284 . . . . . . . . . 10 (2 < (logโ€˜10) โ†’ 2 โ‰ค (logโ€˜10))
139137, 138ax-mp 5 . . . . . . . . 9 2 โ‰ค (logโ€˜10)
14016, 29, 120ltleii 11285 . . . . . . . . . . 11 0 โ‰ค 9
14189, 1, 26, 140decltdi 12664 . . . . . . . . . 10 0 < 27
14293, 134, 92lemul2i 12085 . . . . . . . . . 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 11178 . . . . . . . . 9 (27 ยท 2) โˆˆ โ„
14620nn0zi 12535 . . . . . . . . . . 11 27 โˆˆ โ„ค
147 relogexp 25967 . . . . . . . . . . 11 ((10 โˆˆ โ„+ โˆง 27 โˆˆ โ„ค) โ†’ (logโ€˜(10โ†‘27)) = (27 ยท (logโ€˜10)))
148125, 146, 147mp2an 691 . . . . . . . . . 10 (logโ€˜(10โ†‘27)) = (27 ยท (logโ€˜10))
149148, 51eqeltrri 2835 . . . . . . . . 9 (27 ยท (logโ€˜10)) โˆˆ โ„
15093, 145, 149letri 11291 . . . . . . . 8 ((2 โ‰ค (27 ยท 2) โˆง (27 ยท 2) โ‰ค (27 ยท (logโ€˜10))) โ†’ 2 โ‰ค (27 ยท (logโ€˜10)))
15197, 144, 150mp2an 691 . . . . . . 7 2 โ‰ค (27 ยท (logโ€˜10))
152 relogef 25954 . . . . . . . 8 (2 โˆˆ โ„ โ†’ (logโ€˜(expโ€˜2)) = 2)
15393, 152ax-mp 5 . . . . . . 7 (logโ€˜(expโ€˜2)) = 2
154151, 153, 1483brtr4i 5140 . . . . . 6 (logโ€˜(expโ€˜2)) โ‰ค (logโ€˜(10โ†‘27))
155 rpefcl 15993 . . . . . . . 8 (2 โˆˆ โ„ โ†’ (expโ€˜2) โˆˆ โ„+)
15693, 155ax-mp 5 . . . . . . 7 (expโ€˜2) โˆˆ โ„+
157 logleb 25974 . . . . . . 7 (((expโ€˜2) โˆˆ โ„+ โˆง (10โ†‘27) โˆˆ โ„+) โ†’ ((expโ€˜2) โ‰ค (10โ†‘27) โ†” (logโ€˜(expโ€˜2)) โ‰ค (logโ€˜(10โ†‘27))))
158156, 49, 157mp2an 691 . . . . . 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 33303 . . 3 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ((logโ€˜๐‘) / (โˆšโ€˜๐‘)) โ‰ค ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))))
16246, 56, 13, 85, 161lemul2ad 12102 . 2 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ((7.348) ยท ((logโ€˜๐‘) / (โˆšโ€˜๐‘))) โ‰ค ((7.348) ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))))
163 3lt10 12762 . . . . . . . 8 3 < 10
164 4lt10 12761 . . . . . . . . 9 4 < 10
165 8lt10 12757 . . . . . . . . 9 8 < 10
16659, 77, 164, 165dp2lt10 31782 . . . . . . . 8 48 < 10
16774, 78, 163, 166dp2lt10 31782 . . . . . . 7 348 < 10
168 7p1e8 12309 . . . . . . 7 (7 + 1) = 8
1691, 79, 61, 167, 168dplti 31803 . . . . . 6 (7.348) < 8
17058, 62sselii 3946 . . . . . . 7 8 โˆˆ โ„
17112, 170, 18lttri 11288 . . . . . 6 (((7.348) < 8 โˆง 8 < 10) โ†’ (7.348) < 10)
172169, 165, 171mp2an 691 . . . . 5 (7.348) < 10
17327, 26deccl 12640 . . . . . . . . . 10 10 โˆˆ โ„•0
174173numexp0 16955 . . . . . . . . 9 (10โ†‘0) = 1
175 0z 12517 . . . . . . . . . . 11 0 โˆˆ โ„ค
17618, 175, 1463pm3.2i 1340 . . . . . . . . . 10 (10 โˆˆ โ„ โˆง 0 โˆˆ โ„ค โˆง 27 โˆˆ โ„ค)
177 1lt10 12764 . . . . . . . . . . 11 1 < 10
178177, 141pm3.2i 472 . . . . . . . . . 10 (1 < 10 โˆง 0 < 27)
179 ltexp2a 14078 . . . . . . . . . 10 (((10 โˆˆ โ„ โˆง 0 โˆˆ โ„ค โˆง 27 โˆˆ โ„ค) โˆง (1 < 10 โˆง 0 < 27)) โ†’ (10โ†‘0) < (10โ†‘27))
180176, 178, 179mp2an 691 . . . . . . . . 9 (10โ†‘0) < (10โ†‘27)
181174, 180eqbrtrri 5133 . . . . . . . 8 1 < (10โ†‘27)
182 loggt0b 26003 . . . . . . . . 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 12070 . . . . . . 7 ((0 < (logโ€˜(10โ†‘27)) โˆง 0 < (โˆšโ€˜(10โ†‘27))) โ†’ 0 < ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))))
186184, 53, 185mp2an 691 . . . . . 6 0 < ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))
18712, 18, 55ltmul1i 12080 . . . . . 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 11176 . . . . . . . . . . . . 13 10 โˆˆ โ„‚
191 expmul 14020 . . . . . . . . . . . . 13 ((10 โˆˆ โ„‚ โˆง 7 โˆˆ โ„•0 โˆง 2 โˆˆ โ„•0) โ†’ (10โ†‘(7 ยท 2)) = ((10โ†‘7)โ†‘2))
192190, 1, 19, 191mp3an 1462 . . . . . . . . . . . 12 (10โ†‘(7 ยท 2)) = ((10โ†‘7)โ†‘2)
193 7t2e14 12734 . . . . . . . . . . . . 13 (7 ยท 2) = 14
194193oveq2i 7373 . . . . . . . . . . . 12 (10โ†‘(7 ยท 2)) = (10โ†‘14)
195192, 194eqtr3i 2767 . . . . . . . . . . 11 ((10โ†‘7)โ†‘2) = (10โ†‘14)
196195fveq2i 6850 . . . . . . . . . 10 (โˆšโ€˜((10โ†‘7)โ†‘2)) = (โˆšโ€˜(10โ†‘14))
197 reexpcl 13991 . . . . . . . . . . . 12 ((10 โˆˆ โ„ โˆง 7 โˆˆ โ„•0) โ†’ (10โ†‘7) โˆˆ โ„)
19818, 1, 197mp2an 691 . . . . . . . . . . 11 (10โ†‘7) โˆˆ โ„
1991nn0zi 12535 . . . . . . . . . . . . 13 7 โˆˆ โ„ค
200 expgt0 14008 . . . . . . . . . . . . 13 ((10 โˆˆ โ„ โˆง 7 โˆˆ โ„ค โˆง 0 < 10) โ†’ 0 < (10โ†‘7))
20118, 199, 123, 200mp3an 1462 . . . . . . . . . . . 12 0 < (10โ†‘7)
20216, 198, 201ltleii 11285 . . . . . . . . . . 11 0 โ‰ค (10โ†‘7)
203 sqrtsq 15161 . . . . . . . . . . 11 (((10โ†‘7) โˆˆ โ„ โˆง 0 โ‰ค (10โ†‘7)) โ†’ (โˆšโ€˜((10โ†‘7)โ†‘2)) = (10โ†‘7))
204198, 202, 203mp2an 691 . . . . . . . . . 10 (โˆšโ€˜((10โ†‘7)โ†‘2)) = (10โ†‘7)
205196, 204eqtr3i 2767 . . . . . . . . 9 (โˆšโ€˜(10โ†‘14)) = (10โ†‘7)
20627, 59deccl 12640 . . . . . . . . . . . . 13 14 โˆˆ โ„•0
207206nn0zi 12535 . . . . . . . . . . . 12 14 โˆˆ โ„ค
20818, 207, 1463pm3.2i 1340 . . . . . . . . . . 11 (10 โˆˆ โ„ โˆง 14 โˆˆ โ„ค โˆง 27 โˆˆ โ„ค)
209 1lt2 12331 . . . . . . . . . . . . 13 1 < 2
21027, 19, 59, 1, 164, 209decltc 12654 . . . . . . . . . . . 12 14 < 27
211177, 210pm3.2i 472 . . . . . . . . . . 11 (1 < 10 โˆง 14 < 27)
212 ltexp2a 14078 . . . . . . . . . . 11 (((10 โˆˆ โ„ โˆง 14 โˆˆ โ„ค โˆง 27 โˆˆ โ„ค) โˆง (1 < 10 โˆง 14 < 27)) โ†’ (10โ†‘14) < (10โ†‘27))
213208, 211, 212mp2an 691 . . . . . . . . . 10 (10โ†‘14) < (10โ†‘27)
214 reexpcl 13991 . . . . . . . . . . . . 13 ((10 โˆˆ โ„ โˆง 14 โˆˆ โ„•0) โ†’ (10โ†‘14) โˆˆ โ„)
21518, 206, 214mp2an 691 . . . . . . . . . . . 12 (10โ†‘14) โˆˆ โ„
216 expgt0 14008 . . . . . . . . . . . . . 14 ((10 โˆˆ โ„ โˆง 14 โˆˆ โ„ค โˆง 0 < 10) โ†’ 0 < (10โ†‘14))
21718, 207, 123, 216mp3an 1462 . . . . . . . . . . . . 13 0 < (10โ†‘14)
21816, 215, 217ltleii 11285 . . . . . . . . . . . 12 0 โ‰ค (10โ†‘14)
219215, 218pm3.2i 472 . . . . . . . . . . 11 ((10โ†‘14) โˆˆ โ„ โˆง 0 โ‰ค (10โ†‘14))
22016, 22, 36ltleii 11285 . . . . . . . . . . . 12 0 โ‰ค (10โ†‘27)
22122, 220pm3.2i 472 . . . . . . . . . . 11 ((10โ†‘27) โˆˆ โ„ โˆง 0 โ‰ค (10โ†‘27))
222 sqrtlt 15153 . . . . . . . . . . 11 ((((10โ†‘14) โˆˆ โ„ โˆง 0 โ‰ค (10โ†‘14)) โˆง ((10โ†‘27) โˆˆ โ„ โˆง 0 โ‰ค (10โ†‘27))) โ†’ ((10โ†‘14) < (10โ†‘27) โ†” (โˆšโ€˜(10โ†‘14)) < (โˆšโ€˜(10โ†‘27))))
223219, 221, 222mp2an 691 . . . . . . . . . 10 ((10โ†‘14) < (10โ†‘27) โ†” (โˆšโ€˜(10โ†‘14)) < (โˆšโ€˜(10โ†‘27)))
224213, 223mpbi 229 . . . . . . . . 9 (โˆšโ€˜(10โ†‘14)) < (โˆšโ€˜(10โ†‘27))
225205, 224eqbrtrri 5133 . . . . . . . 8 (10โ†‘7) < (โˆšโ€˜(10โ†‘27))
226198, 201pm3.2i 472 . . . . . . . . 9 ((10โ†‘7) โˆˆ โ„ โˆง 0 < (10โ†‘7))
22752, 53pm3.2i 472 . . . . . . . . 9 ((โˆšโ€˜(10โ†‘27)) โˆˆ โ„ โˆง 0 < (โˆšโ€˜(10โ†‘27)))
22851, 184pm3.2i 472 . . . . . . . . 9 ((logโ€˜(10โ†‘27)) โˆˆ โ„ โˆง 0 < (logโ€˜(10โ†‘27)))
229 ltdiv2 12048 . . . . . . . . 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 1462 . . . . . . . 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 12249 . . . . . . . . . . . . . 14 6 โˆˆ โ„•
233232nngt0i 12199 . . . . . . . . . . . . . 14 0 < 6
23427, 26, 232, 233declt 12653 . . . . . . . . . . . . 13 10 < 16
235 6nn0 12441 . . . . . . . . . . . . . . . . 17 6 โˆˆ โ„•0
23627, 235deccl 12640 . . . . . . . . . . . . . . . 16 16 โˆˆ โ„•0
237236nn0rei 12431 . . . . . . . . . . . . . . 15 16 โˆˆ โ„
23825, 235, 26, 123declti 12663 . . . . . . . . . . . . . . 15 0 < 16
239 elrp 12924 . . . . . . . . . . . . . . 15 (16 โˆˆ โ„+ โ†” (16 โˆˆ โ„ โˆง 0 < 16))
240237, 238, 239mpbir2an 710 . . . . . . . . . . . . . 14 16 โˆˆ โ„+
241 logltb 25971 . . . . . . . . . . . . . 14 ((10 โˆˆ โ„+ โˆง 16 โˆˆ โ„+) โ†’ (10 < 16 โ†” (logโ€˜10) < (logโ€˜16)))
242125, 240, 241mp2an 691 . . . . . . . . . . . . 13 (10 < 16 โ†” (logโ€˜10) < (logโ€˜16))
243234, 242mpbi 229 . . . . . . . . . . . 12 (logโ€˜10) < (logโ€˜16)
244 2exp4 16964 . . . . . . . . . . . . . 14 (2โ†‘4) = 16
245244fveq2i 6850 . . . . . . . . . . . . 13 (logโ€˜(2โ†‘4)) = (logโ€˜16)
246 2rp 12927 . . . . . . . . . . . . . 14 2 โˆˆ โ„+
24759nn0zi 12535 . . . . . . . . . . . . . 14 4 โˆˆ โ„ค
248 relogexp 25967 . . . . . . . . . . . . . 14 ((2 โˆˆ โ„+ โˆง 4 โˆˆ โ„ค) โ†’ (logโ€˜(2โ†‘4)) = (4 ยท (logโ€˜2)))
249246, 247, 248mp2an 691 . . . . . . . . . . . . 13 (logโ€˜(2โ†‘4)) = (4 ยท (logโ€˜2))
250245, 249eqtr3i 2767 . . . . . . . . . . . 12 (logโ€˜16) = (4 ยท (logโ€˜2))
251243, 250breqtri 5135 . . . . . . . . . . 11 (logโ€˜10) < (4 ยท (logโ€˜2))
252100simpli 485 . . . . . . . . . . . . . . 15 2 < e
253 logltb 25971 . . . . . . . . . . . . . . . 16 ((2 โˆˆ โ„+ โˆง e โˆˆ โ„+) โ†’ (2 < e โ†” (logโ€˜2) < (logโ€˜e)))
254246, 102, 253mp2an 691 . . . . . . . . . . . . . . 15 (2 < e โ†” (logโ€˜2) < (logโ€˜e))
255252, 254mpbi 229 . . . . . . . . . . . . . 14 (logโ€˜2) < (logโ€˜e)
256255, 99breqtri 5135 . . . . . . . . . . . . 13 (logโ€˜2) < 1
257 4pos 12267 . . . . . . . . . . . . . 14 0 < 4
258 relogcl 25947 . . . . . . . . . . . . . . . 16 (2 โˆˆ โ„+ โ†’ (logโ€˜2) โˆˆ โ„)
259246, 258ax-mp 5 . . . . . . . . . . . . . . 15 (logโ€˜2) โˆˆ โ„
260259, 28, 3ltmul2i 12083 . . . . . . . . . . . . . 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 12245 . . . . . . . . . . . . 13 4 โˆˆ โ„‚
264263mulid1i 11166 . . . . . . . . . . . 12 (4 ยท 1) = 4
265262, 264breqtri 5135 . . . . . . . . . . 11 (4 ยท (logโ€˜2)) < 4
2663, 259remulcli 11178 . . . . . . . . . . . 12 (4 ยท (logโ€˜2)) โˆˆ โ„
267134, 266, 3lttri 11288 . . . . . . . . . . 11 (((logโ€˜10) < (4 ยท (logโ€˜2)) โˆง (4 ยท (logโ€˜2)) < 4) โ†’ (logโ€˜10) < 4)
268251, 265, 267mp2an 691 . . . . . . . . . 10 (logโ€˜10) < 4
269134, 3, 92ltmul2i 12083 . . . . . . . . . . 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 5131 . . . . . . . 8 (logโ€˜(10โ†‘27)) < (27 ยท 4)
27392, 3remulcli 11178 . . . . . . . . . 10 (27 ยท 4) โˆˆ โ„
27451, 273, 198ltdiv1i 12081 . . . . . . . . 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 11274 . . . . . . . . 9 (10โ†‘7) โ‰  0
27851, 198, 277redivcli 11929 . . . . . . . 8 ((logโ€˜(10โ†‘27)) / (10โ†‘7)) โˆˆ โ„
279273, 198, 277redivcli 11929 . . . . . . . 8 ((27 ยท 4) / (10โ†‘7)) โˆˆ โ„
28055, 278, 279lttri 11288 . . . . . . 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 691 . . . . . 6 ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))) < ((27 ยท 4) / (10โ†‘7))
282 7lt10 12758 . . . . . . . . . 10 7 < 10
283 2lt10 12763 . . . . . . . . . 10 2 < 10
28419, 173, 1, 26, 282, 283decltc 12654 . . . . . . . . 9 27 < 100
285 10nn 12641 . . . . . . . . . . . . 13 10 โˆˆ โ„•
286285decnncl2 12649 . . . . . . . . . . . 12 100 โˆˆ โ„•
287286nnrei 12169 . . . . . . . . . . 11 100 โˆˆ โ„
28892, 287, 3ltmul1i 12080 . . . . . . . . . 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 11178 . . . . . . . . . 10 (100 ยท 4) โˆˆ โ„
292273, 291, 198ltdiv1i 12081 . . . . . . . . 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 12255 . . . . . . . . . . . . . . 15 8 โˆˆ โ„•
296 nnrp 12933 . . . . . . . . . . . . . . 15 (8 โˆˆ โ„• โ†’ 8 โˆˆ โ„+)
297295, 296ax-mp 5 . . . . . . . . . . . . . 14 8 โˆˆ โ„+
29859, 297rpdp2cl 31780 . . . . . . . . . . . . 13 48 โˆˆ โ„+
29919, 298rpdp2cl 31780 . . . . . . . . . . . 12 248 โˆˆ โ„+
30019, 299rpdp2cl 31780 . . . . . . . . . . 11 2248 โˆˆ โ„+
30159, 300dpgti 31804 . . . . . . . . . 10 4 < (4.2248)
30272recni 11176 . . . . . . . . . . . . 13 (0.00042248) โˆˆ โ„‚
303198recni 11176 . . . . . . . . . . . . 13 (10โ†‘7) โˆˆ โ„‚
304302, 303mulcli 11169 . . . . . . . . . . . 12 ((0.00042248) ยท (10โ†‘7)) โˆˆ โ„‚
30516, 123gtneii 11274 . . . . . . . . . . . . 13 10 โ‰  0
306190, 305pm3.2i 472 . . . . . . . . . . . 12 (10 โˆˆ โ„‚ โˆง 10 โ‰  0)
307287recni 11176 . . . . . . . . . . . . 13 100 โˆˆ โ„‚
308286nnne0i 12200 . . . . . . . . . . . . 13 100 โ‰  0
309307, 308pm3.2i 472 . . . . . . . . . . . 12 (100 โˆˆ โ„‚ โˆง 100 โ‰  0)
310 divdiv1 11873 . . . . . . . . . . . 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 1462 . . . . . . . . . . 11 ((((0.00042248) ยท (10โ†‘7)) / 10) / 100) = (((0.00042248) ยท (10โ†‘7)) / (10 ยท 100))
312302, 303, 190, 305div23i 11920 . . . . . . . . . . . 12 (((0.00042248) ยท (10โ†‘7)) / 10) = (((0.00042248) / 10) ยท (10โ†‘7))
313312oveq1i 7372 . . . . . . . . . . 11 ((((0.00042248) ยท (10โ†‘7)) / 10) / 100) = ((((0.00042248) / 10) ยท (10โ†‘7)) / 100)
314190, 307mulcli 11169 . . . . . . . . . . . . 13 (10 ยท 100) โˆˆ โ„‚
315190, 307, 305, 308mulne0i 11805 . . . . . . . . . . . . 13 (10 ยท 100) โ‰  0
316302, 303, 314, 315divassi 11918 . . . . . . . . . . . 12 (((0.00042248) ยท (10โ†‘7)) / (10 ยท 100)) = ((0.00042248) ยท ((10โ†‘7) / (10 ยท 100)))
317 expp1 13981 . . . . . . . . . . . . . . . . . 18 ((10 โˆˆ โ„‚ โˆง 2 โˆˆ โ„•0) โ†’ (10โ†‘(2 + 1)) = ((10โ†‘2) ยท 10))
318190, 19, 317mp2an 691 . . . . . . . . . . . . . . . . 17 (10โ†‘(2 + 1)) = ((10โ†‘2) ยท 10)
319 sq10 14171 . . . . . . . . . . . . . . . . . 18 (10โ†‘2) = 100
320319oveq1i 7372 . . . . . . . . . . . . . . . . 17 ((10โ†‘2) ยท 10) = (100 ยท 10)
321307, 190mulcomi 11170 . . . . . . . . . . . . . . . . 17 (100 ยท 10) = (10 ยท 100)
322318, 320, 3213eqtrri 2770 . . . . . . . . . . . . . . . 16 (10 ยท 100) = (10โ†‘(2 + 1))
323 2p1e3 12302 . . . . . . . . . . . . . . . . 17 (2 + 1) = 3
324323oveq2i 7373 . . . . . . . . . . . . . . . 16 (10โ†‘(2 + 1)) = (10โ†‘3)
325322, 324eqtri 2765 . . . . . . . . . . . . . . 15 (10 ยท 100) = (10โ†‘3)
326325oveq2i 7373 . . . . . . . . . . . . . 14 ((10โ†‘7) / (10 ยท 100)) = ((10โ†‘7) / (10โ†‘3))
32774nn0zi 12535 . . . . . . . . . . . . . . . 16 3 โˆˆ โ„ค
328199, 327pm3.2i 472 . . . . . . . . . . . . . . 15 (7 โˆˆ โ„ค โˆง 3 โˆˆ โ„ค)
329 expsub 14023 . . . . . . . . . . . . . . 15 (((10 โˆˆ โ„‚ โˆง 10 โ‰  0) โˆง (7 โˆˆ โ„ค โˆง 3 โˆˆ โ„ค)) โ†’ (10โ†‘(7 โˆ’ 3)) = ((10โ†‘7) / (10โ†‘3)))
330306, 328, 329mp2an 691 . . . . . . . . . . . . . 14 (10โ†‘(7 โˆ’ 3)) = ((10โ†‘7) / (10โ†‘3))
331 7cn 12254 . . . . . . . . . . . . . . . 16 7 โˆˆ โ„‚
332 4p3e7 12314 . . . . . . . . . . . . . . . . 17 (4 + 3) = 7
333263, 112, 332addcomli 11354 . . . . . . . . . . . . . . . 16 (3 + 4) = 7
334331, 112, 263, 333subaddrii 11497 . . . . . . . . . . . . . . 15 (7 โˆ’ 3) = 4
335334oveq2i 7373 . . . . . . . . . . . . . 14 (10โ†‘(7 โˆ’ 3)) = (10โ†‘4)
336326, 330, 3353eqtr2i 2771 . . . . . . . . . . . . 13 ((10โ†‘7) / (10 ยท 100)) = (10โ†‘4)
337336oveq2i 7373 . . . . . . . . . . . 12 ((0.00042248) ยท ((10โ†‘7) / (10 ยท 100))) = ((0.00042248) ยท (10โ†‘4))
338173numexp1 16956 . . . . . . . . . . . . . 14 (10โ†‘1) = 10
339338oveq2i 7373 . . . . . . . . . . . . 13 ((0.42248) ยท (10โ†‘1)) = ((0.42248) ยท 10)
34059, 300rpdp2cl 31780 . . . . . . . . . . . . . . 15 42248 โˆˆ โ„+
34125nnzi 12534 . . . . . . . . . . . . . . 15 1 โˆˆ โ„ค
34289nnzi 12534 . . . . . . . . . . . . . . 15 2 โˆˆ โ„ค
34326, 340, 98, 341, 342dpexpp1 31806 . . . . . . . . . . . . . 14 ((0.42248) ยท (10โ†‘1)) = ((0.042248) ยท (10โ†‘2))
34426, 340rpdp2cl 31780 . . . . . . . . . . . . . . 15 042248 โˆˆ โ„+
34526, 344, 323, 342, 327dpexpp1 31806 . . . . . . . . . . . . . 14 ((0.042248) ยท (10โ†‘2)) = ((0.0042248) ยท (10โ†‘3))
34626, 344rpdp2cl 31780 . . . . . . . . . . . . . . 15 0042248 โˆˆ โ„+
347 3p1e4 12305 . . . . . . . . . . . . . . 15 (3 + 1) = 4
34826, 346, 347, 327, 247dpexpp1 31806 . . . . . . . . . . . . . 14 ((0.0042248) ยท (10โ†‘3)) = ((0.00042248) ยท (10โ†‘4))
349343, 345, 3483eqtri 2769 . . . . . . . . . . . . 13 ((0.42248) ยท (10โ†‘1)) = ((0.00042248) ยท (10โ†‘4))
35059, 3000dp2dp 31807 . . . . . . . . . . . . 13 ((0.42248) ยท 10) = (4.2248)
351339, 349, 3503eqtr3i 2773 . . . . . . . . . . . 12 ((0.00042248) ยท (10โ†‘4)) = (4.2248)
352316, 337, 3513eqtri 2769 . . . . . . . . . . 11 (((0.00042248) ยท (10โ†‘7)) / (10 ยท 100)) = (4.2248)
353311, 313, 3523eqtr3i 2773 . . . . . . . . . 10 ((((0.00042248) / 10) ยท (10โ†‘7)) / 100) = (4.2248)
354301, 353breqtrri 5137 . . . . . . . . 9 4 < ((((0.00042248) / 10) ยท (10โ†‘7)) / 100)
35572, 18, 305redivcli 11929 . . . . . . . . . . 11 ((0.00042248) / 10) โˆˆ โ„
356355, 198remulcli 11178 . . . . . . . . . 10 (((0.00042248) / 10) ยท (10โ†‘7)) โˆˆ โ„
357286nngt0i 12199 . . . . . . . . . . 11 0 < 100
358287, 357pm3.2i 472 . . . . . . . . . 10 (100 โˆˆ โ„ โˆง 0 < 100)
359 ltmuldiv2 12036 . . . . . . . . . 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 1462 . . . . . . . . 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 12039 . . . . . . . . 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 1462 . . . . . . . 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 11929 . . . . . . . 8 ((100 ยท 4) / (10โ†‘7)) โˆˆ โ„
366279, 365, 355lttri 11288 . . . . . . 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 691 . . . . . 6 ((27 ยท 4) / (10โ†‘7)) < ((0.00042248) / 10)
368226simpli 485 . . . . . . . 8 (10โ†‘7) โˆˆ โ„
369273, 368, 277redivcli 11929 . . . . . . 7 ((27 ยท 4) / (10โ†‘7)) โˆˆ โ„
37055, 369, 355lttri 11288 . . . . . 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 691 . . . . 5 ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27))) < ((0.00042248) / 10)
372125, 124mpbi 229 . . . . . 6 (10 โˆˆ โ„ โˆง 0 < 10)
373 ltmuldiv2 12036 . . . . . 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 1462 . . . . 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 11178 . . . . 5 ((7.348) ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))) โˆˆ โ„
37718, 55remulcli 11178 . . . . 5 (10 ยท ((logโ€˜(10โ†‘27)) / (โˆšโ€˜(10โ†‘27)))) โˆˆ โ„
378376, 377, 72lttri 11288 . . . 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 691 . . 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 11320 1 ((๐‘ โˆˆ โ„•0 โˆง (10โ†‘27) โ‰ค ๐‘) โ†’ ((7.348) ยท ((logโ€˜๐‘) / (โˆšโ€˜๐‘))) < (0.00042248))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944   class class class wbr 5110  โ€˜cfv 6501  (class class class)co 7362  โ„‚cc 11056  โ„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   ยท cmul 11063   < clt 11196   โ‰ค cle 11197   โˆ’ cmin 11392   / cdiv 11819  โ„•cn 12160  2c2 12215  3c3 12216  4c4 12217  6c6 12219  7c7 12220  8c8 12221  9c9 12222  โ„•0cn0 12420  โ„คcz 12506  cdc 12625  โ„šcq 12880  โ„+crp 12922  โ†‘cexp 13974  โˆšcsqrt 15125  expce 15951  eceu 15952  logclog 25926  cdp2 31769  .cdp 31786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cc 10378  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136  ax-addf 11137  ax-mulf 11138
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-symdif 4207  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-disj 5076  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-ofr 7623  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-oadd 8421  df-omul 8422  df-er 8655  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-fi 9354  df-sup 9385  df-inf 9386  df-oi 9453  df-dju 9844  df-card 9882  df-acn 9885  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-z 12507  df-dec 12626  df-uz 12771  df-q 12881  df-rp 12923  df-xneg 13040  df-xadd 13041  df-xmul 13042  df-ioo 13275  df-ioc 13276  df-ico 13277  df-icc 13278  df-fz 13432  df-fzo 13575  df-fl 13704  df-mod 13782  df-seq 13914  df-exp 13975  df-fac 14181  df-bc 14210  df-hash 14238  df-shft 14959  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-limsup 15360  df-clim 15377  df-rlim 15378  df-sum 15578  df-ef 15957  df-e 15958  df-sin 15959  df-cos 15960  df-tan 15961  df-pi 15962  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-starv 17155  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-unif 17163  df-hom 17164  df-cco 17165  df-rest 17311  df-topn 17312  df-0g 17330  df-gsum 17331  df-topgen 17332  df-pt 17333  df-prds 17336  df-xrs 17391  df-qtop 17396  df-imas 17397  df-xps 17399  df-mre 17473  df-mrc 17474  df-acs 17476  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-submnd 18609  df-mulg 18880  df-cntz 19104  df-cmn 19571  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-cmp 22754  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-ovol 24844  df-vol 24845  df-mbf 24999  df-itg1 25000  df-itg2 25001  df-ibl 25002  df-itg 25003  df-0p 25050  df-limc 25246  df-dv 25247  df-log 25928  df-cxp 25929  df-dp2 31770  df-dp 31787
This theorem is referenced by:  tgoldbachgtde  33313
  Copyright terms: Public domain W3C validator