Proof of Theorem 3lexlogpow2ineq1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | tru 1544 | . 2
⊢
⊤ | 
| 2 |  | 8lt9 12465 | . . . . . . . 8
⊢ 8 <
9 | 
| 3 |  | 2z 12649 | . . . . . . . . . . 11
⊢ 2 ∈
ℤ | 
| 4 |  | uzid 12893 | . . . . . . . . . . 11
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) | 
| 5 | 3, 4 | ax-mp 5 | . . . . . . . . . 10
⊢ 2 ∈
(ℤ≥‘2) | 
| 6 |  | 8nn 12361 | . . . . . . . . . . 11
⊢ 8 ∈
ℕ | 
| 7 |  | nnrp 13046 | . . . . . . . . . . 11
⊢ (8 ∈
ℕ → 8 ∈ ℝ+) | 
| 8 | 6, 7 | ax-mp 5 | . . . . . . . . . 10
⊢ 8 ∈
ℝ+ | 
| 9 |  | 9nn 12364 | . . . . . . . . . . 11
⊢ 9 ∈
ℕ | 
| 10 |  | nnrp 13046 | . . . . . . . . . . 11
⊢ (9 ∈
ℕ → 9 ∈ ℝ+) | 
| 11 | 9, 10 | ax-mp 5 | . . . . . . . . . 10
⊢ 9 ∈
ℝ+ | 
| 12 | 5, 8, 11 | 3pm3.2i 1340 | . . . . . . . . 9
⊢ (2 ∈
(ℤ≥‘2) ∧ 8 ∈ ℝ+ ∧ 9
∈ ℝ+) | 
| 13 |  | logblt 26827 | . . . . . . . . 9
⊢ ((2
∈ (ℤ≥‘2) ∧ 8 ∈ ℝ+
∧ 9 ∈ ℝ+) → (8 < 9 ↔ (2 logb
8) < (2 logb 9))) | 
| 14 | 12, 13 | ax-mp 5 | . . . . . . . 8
⊢ (8 < 9
↔ (2 logb 8) < (2 logb 9)) | 
| 15 | 2, 14 | mpbi 230 | . . . . . . 7
⊢ (2
logb 8) < (2 logb 9) | 
| 16 | 15 | a1i 11 | . . . . . 6
⊢ (⊤
→ (2 logb 8) < (2 logb 9)) | 
| 17 |  | eqid 2737 | . . . . . . . . . 10
⊢ 8 =
8 | 
| 18 |  | cu2 14239 | . . . . . . . . . 10
⊢
(2↑3) = 8 | 
| 19 | 17, 18 | eqtr4i 2768 | . . . . . . . . 9
⊢ 8 =
(2↑3) | 
| 20 | 19 | a1i 11 | . . . . . . . 8
⊢ (⊤
→ 8 = (2↑3)) | 
| 21 | 20 | oveq2d 7447 | . . . . . . 7
⊢ (⊤
→ (2 logb 8) = (2 logb (2↑3))) | 
| 22 |  | 2rp 13039 | . . . . . . . . 9
⊢ 2 ∈
ℝ+ | 
| 23 | 22 | a1i 11 | . . . . . . . 8
⊢ (⊤
→ 2 ∈ ℝ+) | 
| 24 |  | 1red 11262 | . . . . . . . . . 10
⊢ (⊤
→ 1 ∈ ℝ) | 
| 25 |  | 1lt2 12437 | . . . . . . . . . . 11
⊢ 1 <
2 | 
| 26 | 25 | a1i 11 | . . . . . . . . . 10
⊢ (⊤
→ 1 < 2) | 
| 27 | 24, 26 | ltned 11397 | . . . . . . . . 9
⊢ (⊤
→ 1 ≠ 2) | 
| 28 | 27 | necomd 2996 | . . . . . . . 8
⊢ (⊤
→ 2 ≠ 1) | 
| 29 |  | 3z 12650 | . . . . . . . . 9
⊢ 3 ∈
ℤ | 
| 30 | 29 | a1i 11 | . . . . . . . 8
⊢ (⊤
→ 3 ∈ ℤ) | 
| 31 | 23, 28, 30 | relogbexpd 41975 | . . . . . . 7
⊢ (⊤
→ (2 logb (2↑3)) = 3) | 
| 32 | 21, 31 | eqtrd 2777 | . . . . . 6
⊢ (⊤
→ (2 logb 8) = 3) | 
| 33 |  | eqid 2737 | . . . . . . . . 9
⊢ 9 =
9 | 
| 34 |  | sq3 14237 | . . . . . . . . 9
⊢
(3↑2) = 9 | 
| 35 | 33, 34 | eqtr4i 2768 | . . . . . . . 8
⊢ 9 =
(3↑2) | 
| 36 | 35 | a1i 11 | . . . . . . 7
⊢ (⊤
→ 9 = (3↑2)) | 
| 37 | 36 | oveq2d 7447 | . . . . . 6
⊢ (⊤
→ (2 logb 9) = (2 logb (3↑2))) | 
| 38 | 16, 32, 37 | 3brtr3d 5174 | . . . . 5
⊢ (⊤
→ 3 < (2 logb (3↑2))) | 
| 39 |  | 3re 12346 | . . . . . . . . 9
⊢ 3 ∈
ℝ | 
| 40 | 39 | a1i 11 | . . . . . . . 8
⊢ (⊤
→ 3 ∈ ℝ) | 
| 41 | 40 | recnd 11289 | . . . . . . 7
⊢ (⊤
→ 3 ∈ ℂ) | 
| 42 |  | 2re 12340 | . . . . . . . . 9
⊢ 2 ∈
ℝ | 
| 43 | 42 | a1i 11 | . . . . . . . 8
⊢ (⊤
→ 2 ∈ ℝ) | 
| 44 | 43 | recnd 11289 | . . . . . . 7
⊢ (⊤
→ 2 ∈ ℂ) | 
| 45 |  | 2pos 12369 | . . . . . . . . 9
⊢ 0 <
2 | 
| 46 | 45 | a1i 11 | . . . . . . . 8
⊢ (⊤
→ 0 < 2) | 
| 47 | 46 | gt0ne0d 11827 | . . . . . . 7
⊢ (⊤
→ 2 ≠ 0) | 
| 48 | 41, 44, 47 | divcan1d 12044 | . . . . . 6
⊢ (⊤
→ ((3 / 2) · 2) = 3) | 
| 49 | 48 | eqcomd 2743 | . . . . 5
⊢ (⊤
→ 3 = ((3 / 2) · 2)) | 
| 50 |  | 3pos 12371 | . . . . . . . . 9
⊢ 0 <
3 | 
| 51 | 50 | a1i 11 | . . . . . . . 8
⊢ (⊤
→ 0 < 3) | 
| 52 | 40, 51 | elrpd 13074 | . . . . . . 7
⊢ (⊤
→ 3 ∈ ℝ+) | 
| 53 | 3 | a1i 11 | . . . . . . 7
⊢ (⊤
→ 2 ∈ ℤ) | 
| 54 | 23, 28, 52, 53 | relogbzexpd 41976 | . . . . . 6
⊢ (⊤
→ (2 logb (3↑2)) = (2 · (2 logb
3))) | 
| 55 | 43, 46, 40, 51, 28 | relogbcld 41974 | . . . . . . . 8
⊢ (⊤
→ (2 logb 3) ∈ ℝ) | 
| 56 | 55 | recnd 11289 | . . . . . . 7
⊢ (⊤
→ (2 logb 3) ∈ ℂ) | 
| 57 | 44, 56 | mulcomd 11282 | . . . . . 6
⊢ (⊤
→ (2 · (2 logb 3)) = ((2 logb 3) ·
2)) | 
| 58 | 54, 57 | eqtrd 2777 | . . . . 5
⊢ (⊤
→ (2 logb (3↑2)) = ((2 logb 3) ·
2)) | 
| 59 | 38, 49, 58 | 3brtr3d 5174 | . . . 4
⊢ (⊤
→ ((3 / 2) · 2) < ((2 logb 3) ·
2)) | 
| 60 | 40 | rehalfcld 12513 | . . . . 5
⊢ (⊤
→ (3 / 2) ∈ ℝ) | 
| 61 | 60, 55, 23 | ltmul1d 13118 | . . . 4
⊢ (⊤
→ ((3 / 2) < (2 logb 3) ↔ ((3 / 2) · 2) < ((2
logb 3) · 2))) | 
| 62 | 59, 61 | mpbird 257 | . . 3
⊢ (⊤
→ (3 / 2) < (2 logb 3)) | 
| 63 |  | 2nn0 12543 | . . . . . . . . 9
⊢ 2 ∈
ℕ0 | 
| 64 |  | 3nn0 12544 | . . . . . . . . 9
⊢ 3 ∈
ℕ0 | 
| 65 |  | 7nn0 12548 | . . . . . . . . 9
⊢ 7 ∈
ℕ0 | 
| 66 |  | 7lt10 12866 | . . . . . . . . 9
⊢ 7 <
;10 | 
| 67 |  | 2lt3 12438 | . . . . . . . . 9
⊢ 2 <
3 | 
| 68 | 63, 64, 65, 63, 66, 67 | decltc 12762 | . . . . . . . 8
⊢ ;27 < ;32 | 
| 69 |  | 7nn 12358 | . . . . . . . . . . . 12
⊢ 7 ∈
ℕ | 
| 70 | 63, 69 | decnncl 12753 | . . . . . . . . . . 11
⊢ ;27 ∈ ℕ | 
| 71 |  | nnrp 13046 | . . . . . . . . . . 11
⊢ (;27 ∈ ℕ → ;27 ∈
ℝ+) | 
| 72 | 70, 71 | ax-mp 5 | . . . . . . . . . 10
⊢ ;27 ∈
ℝ+ | 
| 73 |  | 2nn 12339 | . . . . . . . . . . . 12
⊢ 2 ∈
ℕ | 
| 74 | 64, 73 | decnncl 12753 | . . . . . . . . . . 11
⊢ ;32 ∈ ℕ | 
| 75 |  | nnrp 13046 | . . . . . . . . . . 11
⊢ (;32 ∈ ℕ → ;32 ∈
ℝ+) | 
| 76 | 74, 75 | ax-mp 5 | . . . . . . . . . 10
⊢ ;32 ∈
ℝ+ | 
| 77 | 5, 72, 76 | 3pm3.2i 1340 | . . . . . . . . 9
⊢ (2 ∈
(ℤ≥‘2) ∧ ;27 ∈ ℝ+ ∧ ;32 ∈
ℝ+) | 
| 78 |  | logblt 26827 | . . . . . . . . 9
⊢ ((2
∈ (ℤ≥‘2) ∧ ;27 ∈ ℝ+ ∧ ;32 ∈ ℝ+) →
(;27 < ;32 ↔ (2 logb ;27) < (2 logb ;32))) | 
| 79 | 77, 78 | ax-mp 5 | . . . . . . . 8
⊢ (;27 < ;32 ↔ (2 logb ;27) < (2 logb ;32)) | 
| 80 | 68, 79 | mpbi 230 | . . . . . . 7
⊢ (2
logb ;27) < (2
logb ;32) | 
| 81 | 80 | a1i 11 | . . . . . 6
⊢ (⊤
→ (2 logb ;27)
< (2 logb ;32)) | 
| 82 |  | eqid 2737 | . . . . . . . . 9
⊢ ;32 = ;32 | 
| 83 |  | 2exp5 17123 | . . . . . . . . 9
⊢
(2↑5) = ;32 | 
| 84 | 82, 83 | eqtr4i 2768 | . . . . . . . 8
⊢ ;32 = (2↑5) | 
| 85 | 84 | a1i 11 | . . . . . . 7
⊢ (⊤
→ ;32 =
(2↑5)) | 
| 86 | 85 | oveq2d 7447 | . . . . . 6
⊢ (⊤
→ (2 logb ;32) =
(2 logb (2↑5))) | 
| 87 | 81, 86 | breqtrd 5169 | . . . . 5
⊢ (⊤
→ (2 logb ;27)
< (2 logb (2↑5))) | 
| 88 |  | eqid 2737 | . . . . . . . . . 10
⊢ ;27 = ;27 | 
| 89 |  | 3exp3 17129 | . . . . . . . . . 10
⊢
(3↑3) = ;27 | 
| 90 | 88, 89 | eqtr4i 2768 | . . . . . . . . 9
⊢ ;27 = (3↑3) | 
| 91 | 90 | a1i 11 | . . . . . . . 8
⊢ (⊤
→ ;27 =
(3↑3)) | 
| 92 | 91 | oveq2d 7447 | . . . . . . 7
⊢ (⊤
→ (2 logb ;27) =
(2 logb (3↑3))) | 
| 93 | 23, 28, 52, 30 | relogbzexpd 41976 | . . . . . . 7
⊢ (⊤
→ (2 logb (3↑3)) = (3 · (2 logb
3))) | 
| 94 | 92, 93 | eqtrd 2777 | . . . . . 6
⊢ (⊤
→ (2 logb ;27) =
(3 · (2 logb 3))) | 
| 95 | 41, 56 | mulcomd 11282 | . . . . . 6
⊢ (⊤
→ (3 · (2 logb 3)) = ((2 logb 3) ·
3)) | 
| 96 | 94, 95 | eqtrd 2777 | . . . . 5
⊢ (⊤
→ (2 logb ;27) =
((2 logb 3) · 3)) | 
| 97 |  | 5re 12353 | . . . . . . . . . 10
⊢ 5 ∈
ℝ | 
| 98 | 97 | a1i 11 | . . . . . . . . 9
⊢ (⊤
→ 5 ∈ ℝ) | 
| 99 | 98 | recnd 11289 | . . . . . . . 8
⊢ (⊤
→ 5 ∈ ℂ) | 
| 100 | 51 | gt0ne0d 11827 | . . . . . . . 8
⊢ (⊤
→ 3 ≠ 0) | 
| 101 | 99, 41, 100 | divcan1d 12044 | . . . . . . 7
⊢ (⊤
→ ((5 / 3) · 3) = 5) | 
| 102 |  | 5nn 12352 | . . . . . . . . . . 11
⊢ 5 ∈
ℕ | 
| 103 | 102 | a1i 11 | . . . . . . . . . 10
⊢ (⊤
→ 5 ∈ ℕ) | 
| 104 | 103 | nnzd 12640 | . . . . . . . . 9
⊢ (⊤
→ 5 ∈ ℤ) | 
| 105 | 23, 28, 104 | relogbexpd 41975 | . . . . . . . 8
⊢ (⊤
→ (2 logb (2↑5)) = 5) | 
| 106 | 105 | eqcomd 2743 | . . . . . . 7
⊢ (⊤
→ 5 = (2 logb (2↑5))) | 
| 107 | 101, 106 | eqtrd 2777 | . . . . . 6
⊢ (⊤
→ ((5 / 3) · 3) = (2 logb (2↑5))) | 
| 108 | 107 | eqcomd 2743 | . . . . 5
⊢ (⊤
→ (2 logb (2↑5)) = ((5 / 3) · 3)) | 
| 109 | 87, 96, 108 | 3brtr3d 5174 | . . . 4
⊢ (⊤
→ ((2 logb 3) · 3) < ((5 / 3) ·
3)) | 
| 110 | 98, 40, 100 | redivcld 12095 | . . . . 5
⊢ (⊤
→ (5 / 3) ∈ ℝ) | 
| 111 | 55, 110, 52 | ltmul1d 13118 | . . . 4
⊢ (⊤
→ ((2 logb 3) < (5 / 3) ↔ ((2 logb 3)
· 3) < ((5 / 3) · 3))) | 
| 112 | 109, 111 | mpbird 257 | . . 3
⊢ (⊤
→ (2 logb 3) < (5 / 3)) | 
| 113 | 62, 112 | jca 511 | . 2
⊢ (⊤
→ ((3 / 2) < (2 logb 3) ∧ (2 logb 3) < (5
/ 3))) | 
| 114 | 1, 113 | ax-mp 5 | 1
⊢ ((3 / 2)
< (2 logb 3) ∧ (2 logb 3) < (5 /
3)) |