Nearby theorems
|
|
Mathbox for metakunt |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > Mathboxes > 3lexlogpow5ineq4 | Structured version Visualization version GIF version | ||
| Description: Sharper logarithm inequality chain. (Contributed by metakunt, 21-Aug-2024.) |
| Ref | Expression |
|---|---|
| 3lexlogpow5ineq4.1 | ⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 3lexlogpow5ineq4.2 | ⊢ (𝜑 → 3 ≤ 𝑋) |
| Ref | Expression |
|---|---|
| 3lexlogpow5ineq4 | ⊢ (𝜑 → 9 < ((2 logb 𝑋)↑5)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 9re 11977 | . . 3 ⊢ 9 ∈ ℝ | |
| 2 | 1 | a1i 11 | . 2 ⊢ (𝜑 → 9 ∈ ℝ) |
| 3 | 1nn0 12154 | . . . . . . 7 ⊢ 1 ∈ ℕ0 | |
| 4 | 1nn 11889 | . . . . . . 7 ⊢ 1 ∈ ℕ | |
| 5 | 3, 4 | decnncl 12361 | . . . . . 6 ⊢ ;11 ∈ ℕ |
| 6 | 5 | a1i 11 | . . . . 5 ⊢ (𝜑 → ;11 ∈ ℕ) |
| 7 | 6 | nnred 11893 | . . . 4 ⊢ (𝜑 → ;11 ∈ ℝ) |
| 8 | 7re 11971 | . . . . 5 ⊢ 7 ∈ ℝ | |
| 9 | 8 | a1i 11 | . . . 4 ⊢ (𝜑 → 7 ∈ ℝ) |
| 10 | 0red 10884 | . . . . . 6 ⊢ (𝜑 → 0 ∈ ℝ) | |
| 11 | 7pos 11989 | . . . . . . 7 ⊢ 0 < 7 | |
| 12 | 11 | a1i 11 | . . . . . 6 ⊢ (𝜑 → 0 < 7) |
| 13 | 10, 12 | ltned 11016 | . . . . 5 ⊢ (𝜑 → 0 ≠ 7) |
| 14 | 13 | necomd 2999 | . . . 4 ⊢ (𝜑 → 7 ≠ 0) |
| 15 | 7, 9, 14 | redivcld 11708 | . . 3 ⊢ (𝜑 → (;11 / 7) ∈ ℝ) |
| 16 | 5nn0 12158 | . . . 4 ⊢ 5 ∈ ℕ0 | |
| 17 | 16 | a1i 11 | . . 3 ⊢ (𝜑 → 5 ∈ ℕ0) |
| 18 | 15, 17 | reexpcld 13784 | . 2 ⊢ (𝜑 → ((;11 / 7)↑5) ∈ ℝ) |
| 19 | 2re 11952 | . . . . 5 ⊢ 2 ∈ ℝ | |
| 20 | 19 | a1i 11 | . . . 4 ⊢ (𝜑 → 2 ∈ ℝ) |
| 21 | 2pos 11981 | . . . . 5 ⊢ 0 < 2 | |
| 22 | 21 | a1i 11 | . . . 4 ⊢ (𝜑 → 0 < 2) |
| 23 | 3lexlogpow5ineq4.1 | . . . 4 ⊢ (𝜑 → 𝑋 ∈ ℝ) | |
| 24 | 3re 11958 | . . . . . 6 ⊢ 3 ∈ ℝ | |
| 25 | 24 | a1i 11 | . . . . 5 ⊢ (𝜑 → 3 ∈ ℝ) |
| 26 | 3pos 11983 | . . . . . 6 ⊢ 0 < 3 | |
| 27 | 26 | a1i 11 | . . . . 5 ⊢ (𝜑 → 0 < 3) |
| 28 | 3lexlogpow5ineq4.2 | . . . . 5 ⊢ (𝜑 → 3 ≤ 𝑋) | |
| 29 | 10, 25, 23, 27, 28 | ltletrd 11040 | . . . 4 ⊢ (𝜑 → 0 < 𝑋) |
| 30 | 1red 10882 | . . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ) | |
| 31 | 1lt2 12049 | . . . . . . 7 ⊢ 1 < 2 | |
| 32 | 31 | a1i 11 | . . . . . 6 ⊢ (𝜑 → 1 < 2) |
| 33 | 30, 32 | ltned 11016 | . . . . 5 ⊢ (𝜑 → 1 ≠ 2) |
| 34 | 33 | necomd 2999 | . . . 4 ⊢ (𝜑 → 2 ≠ 1) |
| 35 | 20, 22, 23, 29, 34 | relogbcld 39887 | . . 3 ⊢ (𝜑 → (2 logb 𝑋) ∈ ℝ) |
| 36 | 35, 17 | reexpcld 13784 | . 2 ⊢ (𝜑 → ((2 logb 𝑋)↑5) ∈ ℝ) |
| 37 | 3lexlogpow5ineq1 39969 | . . 3 ⊢ 9 < ((;11 / 7)↑5) | |
| 38 | 37 | a1i 11 | . 2 ⊢ (𝜑 → 9 < ((;11 / 7)↑5)) |
| 39 | 23, 28 | 3lexlogpow5ineq2 39970 | . 2 ⊢ (𝜑 → ((;11 / 7)↑5) ≤ ((2 logb 𝑋)↑5)) |
| 40 | 2, 18, 36, 38, 39 | ltletrd 11040 | 1 ⊢ (𝜑 → 9 < ((2 logb 𝑋)↑5)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2112 class class class wbr 5070 (class class class)co 7252 ℝcr 10776 0cc0 10777 1c1 10778 < clt 10915 ≤ cle 10916 / cdiv 11537 ℕcn 11878 2c2 11933 3c3 11934 5c5 11936 7c7 11938 9c9 11940 ℕ0cn0 12138 ;cdc 12341 ↑cexp 13685 logb clogb 25794 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 ax-rep 5203 ax-sep 5216 ax-nul 5223 ax-pow 5282 ax-pr 5346 ax-un 7563 ax-inf2 9304 ax-cnex 10833 ax-resscn 10834 ax-1cn 10835 ax-icn 10836 ax-addcl 10837 ax-addrcl 10838 ax-mulcl 10839 ax-mulrcl 10840 ax-mulcom 10841 ax-addass 10842 ax-mulass 10843 ax-distr 10844 ax-i2m1 10845 ax-1ne0 10846 ax-1rid 10847 ax-rnegex 10848 ax-rrecex 10849 ax-cnre 10850 ax-pre-lttri 10851 ax-pre-lttrn 10852 ax-pre-ltadd 10853 ax-pre-mulgt0 10854 ax-pre-sup 10855 ax-addf 10856 ax-mulf 10857 |
| This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rmo 3072 df-rab 3073 df-v 3425 df-sbc 3713 df-csb 3830 df-dif 3887 df-un 3889 df-in 3891 df-ss 3901 df-pss 3903 df-nul 4255 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-iin 4924 df-br 5071 df-opab 5133 df-mpt 5153 df-tr 5186 df-id 5479 df-eprel 5485 df-po 5493 df-so 5494 df-fr 5534 df-se 5535 df-we 5536 df-xp 5585 df-rel 5586 df-cnv 5587 df-co 5588 df-dm 5589 df-rn 5590 df-res 5591 df-ima 5592 df-pred 6189 df-ord 6251 df-on 6252 df-lim 6253 df-suc 6254 df-iota 6373 df-fun 6417 df-fn 6418 df-f 6419 df-f1 6420 df-fo 6421 df-f1o 6422 df-fv 6423 df-isom 6424 df-riota 7209 df-ov 7255 df-oprab 7256 df-mpo 7257 df-of 7508 df-om 7685 df-1st 7801 df-2nd 7802 df-supp 7946 df-wrecs 8089 df-recs 8150 df-rdg 8188 df-1o 8244 df-2o 8245 df-er 8433 df-map 8552 df-pm 8553 df-ixp 8621 df-en 8669 df-dom 8670 df-sdom 8671 df-fin 8672 df-fsupp 9034 df-fi 9075 df-sup 9106 df-inf 9107 df-oi 9174 df-card 9603 df-pnf 10917 df-mnf 10918 df-xr 10919 df-ltxr 10920 df-le 10921 df-sub 11112 df-neg 11113 df-div 11538 df-nn 11879 df-2 11941 df-3 11942 df-4 11943 df-5 11944 df-6 11945 df-7 11946 df-8 11947 df-9 11948 df-n0 12139 df-z 12225 df-dec 12342 df-uz 12487 df-q 12593 df-rp 12635 df-xneg 12752 df-xadd 12753 df-xmul 12754 df-ioo 12987 df-ioc 12988 df-ico 12989 df-icc 12990 df-fz 13144 df-fzo 13287 df-fl 13415 df-mod 13493 df-seq 13625 df-exp 13686 df-fac 13891 df-bc 13920 df-hash 13948 df-shft 14681 df-cj 14713 df-re 14714 df-im 14715 df-sqrt 14849 df-abs 14850 df-limsup 15083 df-clim 15100 df-rlim 15101 df-sum 15301 df-ef 15680 df-sin 15682 df-cos 15683 df-pi 15685 df-struct 16751 df-sets 16768 df-slot 16786 df-ndx 16798 df-base 16816 df-ress 16843 df-plusg 16876 df-mulr 16877 df-starv 16878 df-sca 16879 df-vsca 16880 df-ip 16881 df-tset 16882 df-ple 16883 df-ds 16885 df-unif 16886 df-hom 16887 df-cco 16888 df-rest 17025 df-topn 17026 df-0g 17044 df-gsum 17045 df-topgen 17046 df-pt 17047 df-prds 17050 df-xrs 17105 df-qtop 17110 df-imas 17111 df-xps 17113 df-mre 17187 df-mrc 17188 df-acs 17190 df-mgm 18216 df-sgrp 18265 df-mnd 18276 df-submnd 18321 df-mulg 18591 df-cntz 18813 df-cmn 19278 df-psmet 20477 df-xmet 20478 df-met 20479 df-bl 20480 df-mopn 20481 df-fbas 20482 df-fg 20483 df-cnfld 20486 df-top 21926 df-topon 21943 df-topsp 21965 df-bases 21979 df-cld 22053 df-ntr 22054 df-cls 22055 df-nei 22132 df-lp 22170 df-perf 22171 df-cn 22261 df-cnp 22262 df-haus 22349 df-tx 22596 df-hmeo 22789 df-fil 22880 df-fm 22972 df-flim 22973 df-flf 22974 df-xms 23356 df-ms 23357 df-tms 23358 df-cncf 23922 df-limc 24910 df-dv 24911 df-log 25592 df-cxp 25593 df-logb 25795 |
| This theorem is referenced by: 3lexlogpow5ineq3 39972 aks4d1p1 39990 aks4d1p6 39995 aks4d1p7d1 39996 aks4d1p7 39997 |
| Copyright terms: Public domain | W3C validator |