Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  3lexlogpow5ineq2 Structured version   Visualization version   GIF version

Theorem 3lexlogpow5ineq2 41228
Description: Second inequality in inequality chain, proposed by Mario Carneiro. (Contributed by metakunt, 22-May-2024.)
Hypotheses
Ref Expression
3lexlogpow5ineq2.1 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„)
3lexlogpow5ineq2.2 (๐œ‘ โ†’ 3 โ‰ค ๐‘‹)
Assertion
Ref Expression
3lexlogpow5ineq2 (๐œ‘ โ†’ ((11 / 7)โ†‘5) โ‰ค ((2 logb ๐‘‹)โ†‘5))

Proof of Theorem 3lexlogpow5ineq2
StepHypRef Expression
1 1nn0 12494 . . . . . 6 1 โˆˆ โ„•0
2 1nn 12229 . . . . . 6 1 โˆˆ โ„•
31, 2decnncl 12703 . . . . 5 11 โˆˆ โ„•
43a1i 11 . . . 4 (๐œ‘ โ†’ 11 โˆˆ โ„•)
54nnred 12233 . . 3 (๐œ‘ โ†’ 11 โˆˆ โ„)
6 7re 12311 . . . 4 7 โˆˆ โ„
76a1i 11 . . 3 (๐œ‘ โ†’ 7 โˆˆ โ„)
8 0red 11223 . . . . 5 (๐œ‘ โ†’ 0 โˆˆ โ„)
9 7pos 12329 . . . . . 6 0 < 7
109a1i 11 . . . . 5 (๐œ‘ โ†’ 0 < 7)
118, 10ltned 11356 . . . 4 (๐œ‘ โ†’ 0 โ‰  7)
1211necomd 2994 . . 3 (๐œ‘ โ†’ 7 โ‰  0)
135, 7, 12redivcld 12048 . 2 (๐œ‘ โ†’ (11 / 7) โˆˆ โ„)
14 2re 12292 . . . 4 2 โˆˆ โ„
1514a1i 11 . . 3 (๐œ‘ โ†’ 2 โˆˆ โ„)
16 2pos 12321 . . . 4 0 < 2
1716a1i 11 . . 3 (๐œ‘ โ†’ 0 < 2)
18 3lexlogpow5ineq2.1 . . 3 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„)
19 3re 12298 . . . . 5 3 โˆˆ โ„
2019a1i 11 . . . 4 (๐œ‘ โ†’ 3 โˆˆ โ„)
21 3pos 12323 . . . . 5 0 < 3
2221a1i 11 . . . 4 (๐œ‘ โ†’ 0 < 3)
23 3lexlogpow5ineq2.2 . . . 4 (๐œ‘ โ†’ 3 โ‰ค ๐‘‹)
248, 20, 18, 22, 23ltletrd 11380 . . 3 (๐œ‘ โ†’ 0 < ๐‘‹)
25 1red 11221 . . . . 5 (๐œ‘ โ†’ 1 โˆˆ โ„)
26 1lt2 12389 . . . . . 6 1 < 2
2726a1i 11 . . . . 5 (๐œ‘ โ†’ 1 < 2)
2825, 27ltned 11356 . . . 4 (๐œ‘ โ†’ 1 โ‰  2)
2928necomd 2994 . . 3 (๐œ‘ โ†’ 2 โ‰  1)
3015, 17, 18, 24, 29relogbcld 41146 . 2 (๐œ‘ โ†’ (2 logb ๐‘‹) โˆˆ โ„)
31 5nn0 12498 . . 3 5 โˆˆ โ„•0
3231a1i 11 . 2 (๐œ‘ โ†’ 5 โˆˆ โ„•0)
33 7nn 12310 . . . . 5 7 โˆˆ โ„•
3433a1i 11 . . . 4 (๐œ‘ โ†’ 7 โˆˆ โ„•)
3534nnrpd 13020 . . 3 (๐œ‘ โ†’ 7 โˆˆ โ„+)
36 0nn0 12493 . . . . 5 0 โˆˆ โ„•0
37 tru 1543 . . . . . 6 โŠค
38 0red 11223 . . . . . . 7 (โŠค โ†’ 0 โˆˆ โ„)
39 9re 12317 . . . . . . . 8 9 โˆˆ โ„
4039a1i 11 . . . . . . 7 (โŠค โ†’ 9 โˆˆ โ„)
41 9pos 12331 . . . . . . . 8 0 < 9
4241a1i 11 . . . . . . 7 (โŠค โ†’ 0 < 9)
4338, 40, 42ltled 11368 . . . . . 6 (โŠค โ†’ 0 โ‰ค 9)
4437, 43ax-mp 5 . . . . 5 0 โ‰ค 9
452, 1, 36, 44declei 12719 . . . 4 0 โ‰ค 11
4645a1i 11 . . 3 (๐œ‘ โ†’ 0 โ‰ค 11)
475, 35, 46divge0d 13062 . 2 (๐œ‘ โ†’ 0 โ‰ค (11 / 7))
4815, 17, 20, 22, 29relogbcld 41146 . . 3 (๐œ‘ โ†’ (2 logb 3) โˆˆ โ„)
49 2exp11 17029 . . . . . . . . . . 11 (2โ†‘11) = 2048
5049eqcomi 2739 . . . . . . . . . 10 2048 = (2โ†‘11)
5150a1i 11 . . . . . . . . 9 (๐œ‘ โ†’ 2048 = (2โ†‘11))
5251oveq2d 7429 . . . . . . . 8 (๐œ‘ โ†’ (2 logb 2048) = (2 logb (2โ†‘11)))
5315, 17elrpd 13019 . . . . . . . . 9 (๐œ‘ โ†’ 2 โˆˆ โ„+)
544nnzd 12591 . . . . . . . . 9 (๐œ‘ โ†’ 11 โˆˆ โ„ค)
5553, 29, 54relogbexpd 41147 . . . . . . . 8 (๐œ‘ โ†’ (2 logb (2โ†‘11)) = 11)
5652, 55eqtrd 2770 . . . . . . 7 (๐œ‘ โ†’ (2 logb 2048) = 11)
5756eqcomd 2736 . . . . . 6 (๐œ‘ โ†’ 11 = (2 logb 2048))
58 2z 12600 . . . . . . . 8 2 โˆˆ โ„ค
5958a1i 11 . . . . . . 7 (๐œ‘ โ†’ 2 โˆˆ โ„ค)
6015leidd 11786 . . . . . . 7 (๐œ‘ โ†’ 2 โ‰ค 2)
61 2nn0 12495 . . . . . . . . . . . 12 2 โˆˆ โ„•0
6261, 36deccl 12698 . . . . . . . . . . 11 20 โˆˆ โ„•0
63 4nn0 12497 . . . . . . . . . . 11 4 โˆˆ โ„•0
6462, 63deccl 12698 . . . . . . . . . 10 204 โˆˆ โ„•0
65 8nn 12313 . . . . . . . . . 10 8 โˆˆ โ„•
6664, 65decnncl 12703 . . . . . . . . 9 2048 โˆˆ โ„•
6766a1i 11 . . . . . . . 8 (๐œ‘ โ†’ 2048 โˆˆ โ„•)
6867nnred 12233 . . . . . . 7 (๐œ‘ โ†’ 2048 โˆˆ โ„)
69 4nn 12301 . . . . . . . . . 10 4 โˆˆ โ„•
7062, 69decnncl 12703 . . . . . . . . 9 204 โˆˆ โ„•
71 8nn0 12501 . . . . . . . . 9 8 โˆˆ โ„•0
7270, 71, 36, 44decltdi 12722 . . . . . . . 8 0 < 2048
7372a1i 11 . . . . . . 7 (๐œ‘ โ†’ 0 < 2048)
7461, 1deccl 12698 . . . . . . . . . . 11 21 โˆˆ โ„•0
7574, 71deccl 12698 . . . . . . . . . 10 218 โˆˆ โ„•0
7675, 33decnncl 12703 . . . . . . . . 9 2187 โˆˆ โ„•
7776a1i 11 . . . . . . . 8 (๐œ‘ โ†’ 2187 โˆˆ โ„•)
7877nnred 12233 . . . . . . 7 (๐œ‘ โ†’ 2187 โˆˆ โ„)
7974, 65decnncl 12703 . . . . . . . . 9 218 โˆˆ โ„•
80 7nn0 12500 . . . . . . . . 9 7 โˆˆ โ„•0
8179, 80, 36, 44decltdi 12722 . . . . . . . 8 0 < 2187
8281a1i 11 . . . . . . 7 (๐œ‘ โ†’ 0 < 2187)
83 8re 12314 . . . . . . . . . . 11 8 โˆˆ โ„
8483, 1nn0addge1i 12526 . . . . . . . . . 10 8 โ‰ค (8 + 1)
85 8p1e9 12368 . . . . . . . . . 10 (8 + 1) = 9
8684, 85breqtri 5174 . . . . . . . . 9 8 โ‰ค 9
87 4lt10 12819 . . . . . . . . . 10 4 < 10
88 0lt1 11742 . . . . . . . . . . 11 0 < 1
8961, 36, 2, 88declt 12711 . . . . . . . . . 10 20 < 21
9062, 74, 63, 71, 87, 89decltc 12712 . . . . . . . . 9 204 < 218
9164, 75, 71, 80, 86, 90decleh 12718 . . . . . . . 8 2048 โ‰ค 2187
9291a1i 11 . . . . . . 7 (๐œ‘ โ†’ 2048 โ‰ค 2187)
9359, 60, 68, 73, 78, 82, 92logblebd 41149 . . . . . 6 (๐œ‘ โ†’ (2 logb 2048) โ‰ค (2 logb 2187))
9457, 93eqbrtrd 5171 . . . . 5 (๐œ‘ โ†’ 11 โ‰ค (2 logb 2187))
955recnd 11248 . . . . . . 7 (๐œ‘ โ†’ 11 โˆˆ โ„‚)
967recnd 11248 . . . . . . 7 (๐œ‘ โ†’ 7 โˆˆ โ„‚)
9795, 96, 12divcan1d 11997 . . . . . 6 (๐œ‘ โ†’ ((11 / 7) ยท 7) = 11)
9897eqcomd 2736 . . . . 5 (๐œ‘ โ†’ 11 = ((11 / 7) ยท 7))
99 3exp7 41226 . . . . . . . . . 10 (3โ†‘7) = 2187
10099eqcomi 2739 . . . . . . . . 9 2187 = (3โ†‘7)
101100a1i 11 . . . . . . . 8 (๐œ‘ โ†’ 2187 = (3โ†‘7))
102101oveq2d 7429 . . . . . . 7 (๐œ‘ โ†’ (2 logb 2187) = (2 logb (3โ†‘7)))
10320, 22elrpd 13019 . . . . . . . 8 (๐œ‘ โ†’ 3 โˆˆ โ„+)
10434nnzd 12591 . . . . . . . 8 (๐œ‘ โ†’ 7 โˆˆ โ„ค)
10553, 29, 103, 104relogbzexpd 41148 . . . . . . 7 (๐œ‘ โ†’ (2 logb (3โ†‘7)) = (7 ยท (2 logb 3)))
106102, 105eqtrd 2770 . . . . . 6 (๐œ‘ โ†’ (2 logb 2187) = (7 ยท (2 logb 3)))
10748recnd 11248 . . . . . . 7 (๐œ‘ โ†’ (2 logb 3) โˆˆ โ„‚)
10896, 107mulcomd 11241 . . . . . 6 (๐œ‘ โ†’ (7 ยท (2 logb 3)) = ((2 logb 3) ยท 7))
109106, 108eqtrd 2770 . . . . 5 (๐œ‘ โ†’ (2 logb 2187) = ((2 logb 3) ยท 7))
11094, 98, 1093brtr3d 5180 . . . 4 (๐œ‘ โ†’ ((11 / 7) ยท 7) โ‰ค ((2 logb 3) ยท 7))
11113, 48, 35lemul1d 13065 . . . 4 (๐œ‘ โ†’ ((11 / 7) โ‰ค (2 logb 3) โ†” ((11 / 7) ยท 7) โ‰ค ((2 logb 3) ยท 7)))
112110, 111mpbird 256 . . 3 (๐œ‘ โ†’ (11 / 7) โ‰ค (2 logb 3))
11359, 60, 20, 22, 18, 24, 23logblebd 41149 . . 3 (๐œ‘ โ†’ (2 logb 3) โ‰ค (2 logb ๐‘‹))
11413, 48, 30, 112, 113letrd 11377 . 2 (๐œ‘ โ†’ (11 / 7) โ‰ค (2 logb ๐‘‹))
11513, 30, 32, 47, 114leexp1ad 41145 1 (๐œ‘ โ†’ ((11 / 7)โ†‘5) โ‰ค ((2 logb ๐‘‹)โ†‘5))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   = wceq 1539  โŠคwtru 1540   โˆˆ wcel 2104   class class class wbr 5149  (class class class)co 7413  โ„cr 11113  0cc0 11114  1c1 11115   + caddc 11117   ยท cmul 11119   < clt 11254   โ‰ค cle 11255   / cdiv 11877  โ„•cn 12218  2c2 12273  3c3 12274  4c4 12275  5c5 12276  7c7 12278  8c8 12279  9c9 12280  โ„•0cn0 12478  โ„คcz 12564  cdc 12683  โ†‘cexp 14033   logb clogb 26503
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7729  ax-inf2 9640  ax-cnex 11170  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-mulcom 11178  ax-addass 11179  ax-mulass 11180  ax-distr 11181  ax-i2m1 11182  ax-1ne0 11183  ax-1rid 11184  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187  ax-pre-lttri 11188  ax-pre-lttrn 11189  ax-pre-ltadd 11190  ax-pre-mulgt0 11191  ax-pre-sup 11192  ax-addf 11193  ax-mulf 11194
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7674  df-om 7860  df-1st 7979  df-2nd 7980  df-supp 8151  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-1o 8470  df-2o 8471  df-er 8707  df-map 8826  df-pm 8827  df-ixp 8896  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-fsupp 9366  df-fi 9410  df-sup 9441  df-inf 9442  df-oi 9509  df-card 9938  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-sub 11452  df-neg 11453  df-div 11878  df-nn 12219  df-2 12281  df-3 12282  df-4 12283  df-5 12284  df-6 12285  df-7 12286  df-8 12287  df-9 12288  df-n0 12479  df-z 12565  df-dec 12684  df-uz 12829  df-q 12939  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 14034  df-fac 14240  df-bc 14269  df-hash 14297  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-sin 16019  df-cos 16020  df-pi 16022  df-struct 17086  df-sets 17103  df-slot 17121  df-ndx 17133  df-base 17151  df-ress 17180  df-plusg 17216  df-mulr 17217  df-starv 17218  df-sca 17219  df-vsca 17220  df-ip 17221  df-tset 17222  df-ple 17223  df-ds 17225  df-unif 17226  df-hom 17227  df-cco 17228  df-rest 17374  df-topn 17375  df-0g 17393  df-gsum 17394  df-topgen 17395  df-pt 17396  df-prds 17399  df-xrs 17454  df-qtop 17459  df-imas 17460  df-xps 17462  df-mre 17536  df-mrc 17537  df-acs 17539  df-mgm 18567  df-sgrp 18646  df-mnd 18662  df-submnd 18708  df-mulg 18989  df-cntz 19224  df-cmn 19693  df-psmet 21138  df-xmet 21139  df-met 21140  df-bl 21141  df-mopn 21142  df-fbas 21143  df-fg 21144  df-cnfld 21147  df-top 22618  df-topon 22635  df-topsp 22657  df-bases 22671  df-cld 22745  df-ntr 22746  df-cls 22747  df-nei 22824  df-lp 22862  df-perf 22863  df-cn 22953  df-cnp 22954  df-haus 23041  df-tx 23288  df-hmeo 23481  df-fil 23572  df-fm 23664  df-flim 23665  df-flf 23666  df-xms 24048  df-ms 24049  df-tms 24050  df-cncf 24620  df-limc 25617  df-dv 25618  df-log 26299  df-cxp 26300  df-logb 26504
This theorem is referenced by:  3lexlogpow5ineq4  41229
  Copyright terms: Public domain W3C validator