Proof of Theorem 3lexlogpow2ineq2
| Step | Hyp | Ref
| Expression |
| 1 | | tru 1544 |
. 2
⊢
⊤ |
| 2 | | 2re 12340 |
. . . . 5
⊢ 2 ∈
ℝ |
| 3 | 2 | a1i 11 |
. . . 4
⊢ (⊤
→ 2 ∈ ℝ) |
| 4 | | 3re 12346 |
. . . . . . 7
⊢ 3 ∈
ℝ |
| 5 | 4 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 3 ∈ ℝ) |
| 6 | 5 | rehalfcld 12513 |
. . . . 5
⊢ (⊤
→ (3 / 2) ∈ ℝ) |
| 7 | 6 | resqcld 14165 |
. . . 4
⊢ (⊤
→ ((3 / 2)↑2) ∈ ℝ) |
| 8 | | 2pos 12369 |
. . . . . . 7
⊢ 0 <
2 |
| 9 | 8 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 0 < 2) |
| 10 | | 3pos 12371 |
. . . . . . 7
⊢ 0 <
3 |
| 11 | 10 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 0 < 3) |
| 12 | | 1red 11262 |
. . . . . . . 8
⊢ (⊤
→ 1 ∈ ℝ) |
| 13 | | 1lt2 12437 |
. . . . . . . . 9
⊢ 1 <
2 |
| 14 | 13 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ 1 < 2) |
| 15 | 12, 14 | ltned 11397 |
. . . . . . 7
⊢ (⊤
→ 1 ≠ 2) |
| 16 | 15 | necomd 2996 |
. . . . . 6
⊢ (⊤
→ 2 ≠ 1) |
| 17 | 3, 9, 5, 11, 16 | relogbcld 41974 |
. . . . 5
⊢ (⊤
→ (2 logb 3) ∈ ℝ) |
| 18 | 17 | resqcld 14165 |
. . . 4
⊢ (⊤
→ ((2 logb 3)↑2) ∈ ℝ) |
| 19 | | 2cnd 12344 |
. . . . . . . 8
⊢ (⊤
→ 2 ∈ ℂ) |
| 20 | | 4cn 12351 |
. . . . . . . . 9
⊢ 4 ∈
ℂ |
| 21 | 20 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ 4 ∈ ℂ) |
| 22 | | 0red 11264 |
. . . . . . . . . 10
⊢ (⊤
→ 0 ∈ ℝ) |
| 23 | | 4pos 12373 |
. . . . . . . . . . 11
⊢ 0 <
4 |
| 24 | 23 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ 0 < 4) |
| 25 | 22, 24 | ltned 11397 |
. . . . . . . . 9
⊢ (⊤
→ 0 ≠ 4) |
| 26 | 25 | necomd 2996 |
. . . . . . . 8
⊢ (⊤
→ 4 ≠ 0) |
| 27 | 19, 21, 26 | divcan4d 12049 |
. . . . . . 7
⊢ (⊤
→ ((2 · 4) / 4) = 2) |
| 28 | 27 | eqcomd 2743 |
. . . . . 6
⊢ (⊤
→ 2 = ((2 · 4) / 4)) |
| 29 | | 4re 12350 |
. . . . . . . . 9
⊢ 4 ∈
ℝ |
| 30 | 29 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ 4 ∈ ℝ) |
| 31 | 3, 30 | remulcld 11291 |
. . . . . . 7
⊢ (⊤
→ (2 · 4) ∈ ℝ) |
| 32 | | 9re 12365 |
. . . . . . . 8
⊢ 9 ∈
ℝ |
| 33 | 32 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 9 ∈ ℝ) |
| 34 | 30, 24 | elrpd 13074 |
. . . . . . 7
⊢ (⊤
→ 4 ∈ ℝ+) |
| 35 | | 2cn 12341 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
| 36 | | 4t2e8 12434 |
. . . . . . . . . 10
⊢ (4
· 2) = 8 |
| 37 | 20, 35, 36 | mulcomli 11270 |
. . . . . . . . 9
⊢ (2
· 4) = 8 |
| 38 | 37 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ (2 · 4) = 8) |
| 39 | | 8lt9 12465 |
. . . . . . . . 9
⊢ 8 <
9 |
| 40 | 39 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ 8 < 9) |
| 41 | 38, 40 | eqbrtrd 5165 |
. . . . . . 7
⊢ (⊤
→ (2 · 4) < 9) |
| 42 | 31, 33, 34, 41 | ltdiv1dd 13134 |
. . . . . 6
⊢ (⊤
→ ((2 · 4) / 4) < (9 / 4)) |
| 43 | 28, 42 | eqbrtrd 5165 |
. . . . 5
⊢ (⊤
→ 2 < (9 / 4)) |
| 44 | | eqid 2737 |
. . . . . . . . . 10
⊢ 9 =
9 |
| 45 | | 3t3e9 12433 |
. . . . . . . . . 10
⊢ (3
· 3) = 9 |
| 46 | 44, 45 | eqtr4i 2768 |
. . . . . . . . 9
⊢ 9 = (3
· 3) |
| 47 | 46 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ 9 = (3 · 3)) |
| 48 | | eqid 2737 |
. . . . . . . . . 10
⊢ 4 =
4 |
| 49 | | 2t2e4 12430 |
. . . . . . . . . 10
⊢ (2
· 2) = 4 |
| 50 | 48, 49 | eqtr4i 2768 |
. . . . . . . . 9
⊢ 4 = (2
· 2) |
| 51 | 50 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ 4 = (2 · 2)) |
| 52 | 47, 51 | oveq12d 7449 |
. . . . . . 7
⊢ (⊤
→ (9 / 4) = ((3 · 3) / (2 · 2))) |
| 53 | 5 | recnd 11289 |
. . . . . . . . 9
⊢ (⊤
→ 3 ∈ ℂ) |
| 54 | 3 | recnd 11289 |
. . . . . . . . 9
⊢ (⊤
→ 2 ∈ ℂ) |
| 55 | 9 | gt0ne0d 11827 |
. . . . . . . . 9
⊢ (⊤
→ 2 ≠ 0) |
| 56 | 53, 54, 53, 54, 55, 55 | divmuldivd 12084 |
. . . . . . . 8
⊢ (⊤
→ ((3 / 2) · (3 / 2)) = ((3 · 3) / (2 ·
2))) |
| 57 | 56 | eqcomd 2743 |
. . . . . . 7
⊢ (⊤
→ ((3 · 3) / (2 · 2)) = ((3 / 2) · (3 /
2))) |
| 58 | 52, 57 | eqtrd 2777 |
. . . . . 6
⊢ (⊤
→ (9 / 4) = ((3 / 2) · (3 / 2))) |
| 59 | 6 | recnd 11289 |
. . . . . . 7
⊢ (⊤
→ (3 / 2) ∈ ℂ) |
| 60 | | sqval 14155 |
. . . . . . . 8
⊢ ((3 / 2)
∈ ℂ → ((3 / 2)↑2) = ((3 / 2) · (3 /
2))) |
| 61 | 60 | eqcomd 2743 |
. . . . . . 7
⊢ ((3 / 2)
∈ ℂ → ((3 / 2) · (3 / 2)) = ((3 /
2)↑2)) |
| 62 | 59, 61 | syl 17 |
. . . . . 6
⊢ (⊤
→ ((3 / 2) · (3 / 2)) = ((3 / 2)↑2)) |
| 63 | 58, 62 | eqtrd 2777 |
. . . . 5
⊢ (⊤
→ (9 / 4) = ((3 / 2)↑2)) |
| 64 | 43, 63 | breqtrd 5169 |
. . . 4
⊢ (⊤
→ 2 < ((3 / 2)↑2)) |
| 65 | | 3lexlogpow2ineq1 42059 |
. . . . . . 7
⊢ ((3 / 2)
< (2 logb 3) ∧ (2 logb 3) < (5 /
3)) |
| 66 | 65 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ((3 / 2) < (2 logb 3) ∧ (2 logb 3) < (5
/ 3))) |
| 67 | 66 | simpld 494 |
. . . . 5
⊢ (⊤
→ (3 / 2) < (2 logb 3)) |
| 68 | | 2nn 12339 |
. . . . . . 7
⊢ 2 ∈
ℕ |
| 69 | 68 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 2 ∈ ℕ) |
| 70 | | 3rp 13040 |
. . . . . . . 8
⊢ 3 ∈
ℝ+ |
| 71 | 70 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 3 ∈ ℝ+) |
| 72 | 71 | rphalfcld 13089 |
. . . . . 6
⊢ (⊤
→ (3 / 2) ∈ ℝ+) |
| 73 | 5, 3, 11, 9 | divgt0d 12203 |
. . . . . . . 8
⊢ (⊤
→ 0 < (3 / 2)) |
| 74 | 22, 6, 17, 73, 67 | lttrd 11422 |
. . . . . . 7
⊢ (⊤
→ 0 < (2 logb 3)) |
| 75 | 17, 74 | elrpd 13074 |
. . . . . 6
⊢ (⊤
→ (2 logb 3) ∈ ℝ+) |
| 76 | | rpexpmord 14208 |
. . . . . 6
⊢ ((2
∈ ℕ ∧ (3 / 2) ∈ ℝ+ ∧ (2
logb 3) ∈ ℝ+) → ((3 / 2) < (2
logb 3) ↔ ((3 / 2)↑2) < ((2 logb
3)↑2))) |
| 77 | 69, 72, 75, 76 | syl3anc 1373 |
. . . . 5
⊢ (⊤
→ ((3 / 2) < (2 logb 3) ↔ ((3 / 2)↑2) < ((2
logb 3)↑2))) |
| 78 | 67, 77 | mpbid 232 |
. . . 4
⊢ (⊤
→ ((3 / 2)↑2) < ((2 logb 3)↑2)) |
| 79 | 3, 7, 18, 64, 78 | lttrd 11422 |
. . 3
⊢ (⊤
→ 2 < ((2 logb 3)↑2)) |
| 80 | | 5re 12353 |
. . . . . . 7
⊢ 5 ∈
ℝ |
| 81 | 80 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 5 ∈ ℝ) |
| 82 | 22, 11 | gtned 11396 |
. . . . . 6
⊢ (⊤
→ 3 ≠ 0) |
| 83 | 81, 5, 82 | redivcld 12095 |
. . . . 5
⊢ (⊤
→ (5 / 3) ∈ ℝ) |
| 84 | 69 | nnnn0d 12587 |
. . . . 5
⊢ (⊤
→ 2 ∈ ℕ0) |
| 85 | 83, 84 | reexpcld 14203 |
. . . 4
⊢ (⊤
→ ((5 / 3)↑2) ∈ ℝ) |
| 86 | 66 | simprd 495 |
. . . . 5
⊢ (⊤
→ (2 logb 3) < (5 / 3)) |
| 87 | | 5nn 12352 |
. . . . . . . . 9
⊢ 5 ∈
ℕ |
| 88 | 87 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ 5 ∈ ℕ) |
| 89 | 88 | nnrpd 13075 |
. . . . . . 7
⊢ (⊤
→ 5 ∈ ℝ+) |
| 90 | 89, 71 | rpdivcld 13094 |
. . . . . 6
⊢ (⊤
→ (5 / 3) ∈ ℝ+) |
| 91 | | rpexpmord 14208 |
. . . . . 6
⊢ ((2
∈ ℕ ∧ (2 logb 3) ∈ ℝ+ ∧ (5
/ 3) ∈ ℝ+) → ((2 logb 3) < (5 / 3)
↔ ((2 logb 3)↑2) < ((5 / 3)↑2))) |
| 92 | 69, 75, 90, 91 | syl3anc 1373 |
. . . . 5
⊢ (⊤
→ ((2 logb 3) < (5 / 3) ↔ ((2 logb
3)↑2) < ((5 / 3)↑2))) |
| 93 | 86, 92 | mpbid 232 |
. . . 4
⊢ (⊤
→ ((2 logb 3)↑2) < ((5 / 3)↑2)) |
| 94 | 83 | recnd 11289 |
. . . . . 6
⊢ (⊤
→ (5 / 3) ∈ ℂ) |
| 95 | 94 | sqvald 14183 |
. . . . 5
⊢ (⊤
→ ((5 / 3)↑2) = ((5 / 3) · (5 / 3))) |
| 96 | 81 | recnd 11289 |
. . . . . . 7
⊢ (⊤
→ 5 ∈ ℂ) |
| 97 | 96, 53, 96, 53, 82, 82 | divmuldivd 12084 |
. . . . . 6
⊢ (⊤
→ ((5 / 3) · (5 / 3)) = ((5 · 5) / (3 ·
3))) |
| 98 | | 5t5e25 12836 |
. . . . . . . . 9
⊢ (5
· 5) = ;25 |
| 99 | 98 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ (5 · 5) = ;25) |
| 100 | 45 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ (3 · 3) = 9) |
| 101 | 99, 100 | oveq12d 7449 |
. . . . . . 7
⊢ (⊤
→ ((5 · 5) / (3 · 3)) = (;25 / 9)) |
| 102 | | 2nn0 12543 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
| 103 | | 5nn0 12546 |
. . . . . . . . . . 11
⊢ 5 ∈
ℕ0 |
| 104 | | 7nn 12358 |
. . . . . . . . . . 11
⊢ 7 ∈
ℕ |
| 105 | | 5lt7 12453 |
. . . . . . . . . . 11
⊢ 5 <
7 |
| 106 | 102, 103,
104, 105 | declt 12761 |
. . . . . . . . . 10
⊢ ;25 < ;27 |
| 107 | | 9cn 12366 |
. . . . . . . . . . 11
⊢ 9 ∈
ℂ |
| 108 | | 3cn 12347 |
. . . . . . . . . . 11
⊢ 3 ∈
ℂ |
| 109 | | 9t3e27 12856 |
. . . . . . . . . . 11
⊢ (9
· 3) = ;27 |
| 110 | 107, 108,
109 | mulcomli 11270 |
. . . . . . . . . 10
⊢ (3
· 9) = ;27 |
| 111 | 106, 110 | breqtrri 5170 |
. . . . . . . . 9
⊢ ;25 < (3 · 9) |
| 112 | 111 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ ;25 < (3 ·
9)) |
| 113 | 102, 87 | decnncl 12753 |
. . . . . . . . . . 11
⊢ ;25 ∈ ℕ |
| 114 | 113 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ ;25 ∈
ℕ) |
| 115 | 114 | nnred 12281 |
. . . . . . . . 9
⊢ (⊤
→ ;25 ∈
ℝ) |
| 116 | | 9nn 12364 |
. . . . . . . . . . 11
⊢ 9 ∈
ℕ |
| 117 | 116 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ 9 ∈ ℕ) |
| 118 | 117 | nnrpd 13075 |
. . . . . . . . 9
⊢ (⊤
→ 9 ∈ ℝ+) |
| 119 | 115, 5, 118 | ltdivmul2d 13129 |
. . . . . . . 8
⊢ (⊤
→ ((;25 / 9) < 3 ↔
;25 < (3 ·
9))) |
| 120 | 112, 119 | mpbird 257 |
. . . . . . 7
⊢ (⊤
→ (;25 / 9) <
3) |
| 121 | 101, 120 | eqbrtrd 5165 |
. . . . . 6
⊢ (⊤
→ ((5 · 5) / (3 · 3)) < 3) |
| 122 | 97, 121 | eqbrtrd 5165 |
. . . . 5
⊢ (⊤
→ ((5 / 3) · (5 / 3)) < 3) |
| 123 | 95, 122 | eqbrtrd 5165 |
. . . 4
⊢ (⊤
→ ((5 / 3)↑2) < 3) |
| 124 | 18, 85, 5, 93, 123 | lttrd 11422 |
. . 3
⊢ (⊤
→ ((2 logb 3)↑2) < 3) |
| 125 | 79, 124 | jca 511 |
. 2
⊢ (⊤
→ (2 < ((2 logb 3)↑2) ∧ ((2 logb
3)↑2) < 3)) |
| 126 | 1, 125 | ax-mp 5 |
1
⊢ (2 <
((2 logb 3)↑2) ∧ ((2 logb 3)↑2) <
3) |