Proof of Theorem 3lexlogpow2ineq2
Step | Hyp | Ref
| Expression |
1 | | tru 1543 |
. 2
⊢
⊤ |
2 | | 2re 12047 |
. . . . 5
⊢ 2 ∈
ℝ |
3 | 2 | a1i 11 |
. . . 4
⊢ (⊤
→ 2 ∈ ℝ) |
4 | | 3re 12053 |
. . . . . . 7
⊢ 3 ∈
ℝ |
5 | 4 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 3 ∈ ℝ) |
6 | 5 | rehalfcld 12220 |
. . . . 5
⊢ (⊤
→ (3 / 2) ∈ ℝ) |
7 | 6 | resqcld 13965 |
. . . 4
⊢ (⊤
→ ((3 / 2)↑2) ∈ ℝ) |
8 | | 2pos 12076 |
. . . . . . 7
⊢ 0 <
2 |
9 | 8 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 0 < 2) |
10 | | 3pos 12078 |
. . . . . . 7
⊢ 0 <
3 |
11 | 10 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 0 < 3) |
12 | | 1red 10976 |
. . . . . . . 8
⊢ (⊤
→ 1 ∈ ℝ) |
13 | | 1lt2 12144 |
. . . . . . . . 9
⊢ 1 <
2 |
14 | 13 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ 1 < 2) |
15 | 12, 14 | ltned 11111 |
. . . . . . 7
⊢ (⊤
→ 1 ≠ 2) |
16 | 15 | necomd 2999 |
. . . . . 6
⊢ (⊤
→ 2 ≠ 1) |
17 | 3, 9, 5, 11, 16 | relogbcld 39981 |
. . . . 5
⊢ (⊤
→ (2 logb 3) ∈ ℝ) |
18 | 17 | resqcld 13965 |
. . . 4
⊢ (⊤
→ ((2 logb 3)↑2) ∈ ℝ) |
19 | | 2cnd 12051 |
. . . . . . . 8
⊢ (⊤
→ 2 ∈ ℂ) |
20 | | 4cn 12058 |
. . . . . . . . 9
⊢ 4 ∈
ℂ |
21 | 20 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ 4 ∈ ℂ) |
22 | | 0red 10978 |
. . . . . . . . . 10
⊢ (⊤
→ 0 ∈ ℝ) |
23 | | 4pos 12080 |
. . . . . . . . . . 11
⊢ 0 <
4 |
24 | 23 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ 0 < 4) |
25 | 22, 24 | ltned 11111 |
. . . . . . . . 9
⊢ (⊤
→ 0 ≠ 4) |
26 | 25 | necomd 2999 |
. . . . . . . 8
⊢ (⊤
→ 4 ≠ 0) |
27 | 19, 21, 26 | divcan4d 11757 |
. . . . . . 7
⊢ (⊤
→ ((2 · 4) / 4) = 2) |
28 | 27 | eqcomd 2744 |
. . . . . 6
⊢ (⊤
→ 2 = ((2 · 4) / 4)) |
29 | | 4re 12057 |
. . . . . . . . 9
⊢ 4 ∈
ℝ |
30 | 29 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ 4 ∈ ℝ) |
31 | 3, 30 | remulcld 11005 |
. . . . . . 7
⊢ (⊤
→ (2 · 4) ∈ ℝ) |
32 | | 9re 12072 |
. . . . . . . 8
⊢ 9 ∈
ℝ |
33 | 32 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 9 ∈ ℝ) |
34 | 30, 24 | elrpd 12769 |
. . . . . . 7
⊢ (⊤
→ 4 ∈ ℝ+) |
35 | | 2cn 12048 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
36 | | 4t2e8 12141 |
. . . . . . . . . 10
⊢ (4
· 2) = 8 |
37 | 20, 35, 36 | mulcomli 10984 |
. . . . . . . . 9
⊢ (2
· 4) = 8 |
38 | 37 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ (2 · 4) = 8) |
39 | | 8lt9 12172 |
. . . . . . . . 9
⊢ 8 <
9 |
40 | 39 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ 8 < 9) |
41 | 38, 40 | eqbrtrd 5096 |
. . . . . . 7
⊢ (⊤
→ (2 · 4) < 9) |
42 | 31, 33, 34, 41 | ltdiv1dd 12829 |
. . . . . 6
⊢ (⊤
→ ((2 · 4) / 4) < (9 / 4)) |
43 | 28, 42 | eqbrtrd 5096 |
. . . . 5
⊢ (⊤
→ 2 < (9 / 4)) |
44 | | eqid 2738 |
. . . . . . . . . 10
⊢ 9 =
9 |
45 | | 3t3e9 12140 |
. . . . . . . . . 10
⊢ (3
· 3) = 9 |
46 | 44, 45 | eqtr4i 2769 |
. . . . . . . . 9
⊢ 9 = (3
· 3) |
47 | 46 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ 9 = (3 · 3)) |
48 | | eqid 2738 |
. . . . . . . . . 10
⊢ 4 =
4 |
49 | | 2t2e4 12137 |
. . . . . . . . . 10
⊢ (2
· 2) = 4 |
50 | 48, 49 | eqtr4i 2769 |
. . . . . . . . 9
⊢ 4 = (2
· 2) |
51 | 50 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ 4 = (2 · 2)) |
52 | 47, 51 | oveq12d 7293 |
. . . . . . 7
⊢ (⊤
→ (9 / 4) = ((3 · 3) / (2 · 2))) |
53 | 5 | recnd 11003 |
. . . . . . . . 9
⊢ (⊤
→ 3 ∈ ℂ) |
54 | 3 | recnd 11003 |
. . . . . . . . 9
⊢ (⊤
→ 2 ∈ ℂ) |
55 | 9 | gt0ne0d 11539 |
. . . . . . . . 9
⊢ (⊤
→ 2 ≠ 0) |
56 | 53, 54, 53, 54, 55, 55 | divmuldivd 11792 |
. . . . . . . 8
⊢ (⊤
→ ((3 / 2) · (3 / 2)) = ((3 · 3) / (2 ·
2))) |
57 | 56 | eqcomd 2744 |
. . . . . . 7
⊢ (⊤
→ ((3 · 3) / (2 · 2)) = ((3 / 2) · (3 /
2))) |
58 | 52, 57 | eqtrd 2778 |
. . . . . 6
⊢ (⊤
→ (9 / 4) = ((3 / 2) · (3 / 2))) |
59 | 6 | recnd 11003 |
. . . . . . 7
⊢ (⊤
→ (3 / 2) ∈ ℂ) |
60 | | sqval 13835 |
. . . . . . . 8
⊢ ((3 / 2)
∈ ℂ → ((3 / 2)↑2) = ((3 / 2) · (3 /
2))) |
61 | 60 | eqcomd 2744 |
. . . . . . 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 2778 |
. . . . 5
⊢ (⊤
→ (9 / 4) = ((3 / 2)↑2)) |
64 | 43, 63 | breqtrd 5100 |
. . . 4
⊢ (⊤
→ 2 < ((3 / 2)↑2)) |
65 | | 3lexlogpow2ineq1 40066 |
. . . . . . 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 495 |
. . . . 5
⊢ (⊤
→ (3 / 2) < (2 logb 3)) |
68 | | 2nn 12046 |
. . . . . . 7
⊢ 2 ∈
ℕ |
69 | 68 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 2 ∈ ℕ) |
70 | | 3rp 12736 |
. . . . . . . 8
⊢ 3 ∈
ℝ+ |
71 | 70 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 3 ∈ ℝ+) |
72 | 71 | rphalfcld 12784 |
. . . . . 6
⊢ (⊤
→ (3 / 2) ∈ ℝ+) |
73 | 5, 3, 11, 9 | divgt0d 11910 |
. . . . . . . 8
⊢ (⊤
→ 0 < (3 / 2)) |
74 | 22, 6, 17, 73, 67 | lttrd 11136 |
. . . . . . 7
⊢ (⊤
→ 0 < (2 logb 3)) |
75 | 17, 74 | elrpd 12769 |
. . . . . 6
⊢ (⊤
→ (2 logb 3) ∈ ℝ+) |
76 | | rpexpmord 13886 |
. . . . . 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 1370 |
. . . . 5
⊢ (⊤
→ ((3 / 2) < (2 logb 3) ↔ ((3 / 2)↑2) < ((2
logb 3)↑2))) |
78 | 67, 77 | mpbid 231 |
. . . 4
⊢ (⊤
→ ((3 / 2)↑2) < ((2 logb 3)↑2)) |
79 | 3, 7, 18, 64, 78 | lttrd 11136 |
. . 3
⊢ (⊤
→ 2 < ((2 logb 3)↑2)) |
80 | | 5re 12060 |
. . . . . . 7
⊢ 5 ∈
ℝ |
81 | 80 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 5 ∈ ℝ) |
82 | 22, 11 | gtned 11110 |
. . . . . 6
⊢ (⊤
→ 3 ≠ 0) |
83 | 81, 5, 82 | redivcld 11803 |
. . . . 5
⊢ (⊤
→ (5 / 3) ∈ ℝ) |
84 | 69 | nnnn0d 12293 |
. . . . 5
⊢ (⊤
→ 2 ∈ ℕ0) |
85 | 83, 84 | reexpcld 13881 |
. . . 4
⊢ (⊤
→ ((5 / 3)↑2) ∈ ℝ) |
86 | 66 | simprd 496 |
. . . . 5
⊢ (⊤
→ (2 logb 3) < (5 / 3)) |
87 | | 5nn 12059 |
. . . . . . . . 9
⊢ 5 ∈
ℕ |
88 | 87 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ 5 ∈ ℕ) |
89 | 88 | nnrpd 12770 |
. . . . . . 7
⊢ (⊤
→ 5 ∈ ℝ+) |
90 | 89, 71 | rpdivcld 12789 |
. . . . . 6
⊢ (⊤
→ (5 / 3) ∈ ℝ+) |
91 | | rpexpmord 13886 |
. . . . . 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 1370 |
. . . . 5
⊢ (⊤
→ ((2 logb 3) < (5 / 3) ↔ ((2 logb
3)↑2) < ((5 / 3)↑2))) |
93 | 86, 92 | mpbid 231 |
. . . 4
⊢ (⊤
→ ((2 logb 3)↑2) < ((5 / 3)↑2)) |
94 | 83 | recnd 11003 |
. . . . . 6
⊢ (⊤
→ (5 / 3) ∈ ℂ) |
95 | 94 | sqvald 13861 |
. . . . 5
⊢ (⊤
→ ((5 / 3)↑2) = ((5 / 3) · (5 / 3))) |
96 | 81 | recnd 11003 |
. . . . . . 7
⊢ (⊤
→ 5 ∈ ℂ) |
97 | 96, 53, 96, 53, 82, 82 | divmuldivd 11792 |
. . . . . 6
⊢ (⊤
→ ((5 / 3) · (5 / 3)) = ((5 · 5) / (3 ·
3))) |
98 | | 5t5e25 12540 |
. . . . . . . . 9
⊢ (5
· 5) = ;25 |
99 | 98 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ (5 · 5) = ;25) |
100 | 45 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ (3 · 3) = 9) |
101 | 99, 100 | oveq12d 7293 |
. . . . . . 7
⊢ (⊤
→ ((5 · 5) / (3 · 3)) = (;25 / 9)) |
102 | | 2nn0 12250 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
103 | | 5nn0 12253 |
. . . . . . . . . . 11
⊢ 5 ∈
ℕ0 |
104 | | 7nn 12065 |
. . . . . . . . . . 11
⊢ 7 ∈
ℕ |
105 | | 5lt7 12160 |
. . . . . . . . . . 11
⊢ 5 <
7 |
106 | 102, 103,
104, 105 | declt 12465 |
. . . . . . . . . 10
⊢ ;25 < ;27 |
107 | | 9cn 12073 |
. . . . . . . . . . 11
⊢ 9 ∈
ℂ |
108 | | 3cn 12054 |
. . . . . . . . . . 11
⊢ 3 ∈
ℂ |
109 | | 9t3e27 12560 |
. . . . . . . . . . 11
⊢ (9
· 3) = ;27 |
110 | 107, 108,
109 | mulcomli 10984 |
. . . . . . . . . 10
⊢ (3
· 9) = ;27 |
111 | 106, 110 | breqtrri 5101 |
. . . . . . . . 9
⊢ ;25 < (3 · 9) |
112 | 111 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ ;25 < (3 ·
9)) |
113 | 102, 87 | decnncl 12457 |
. . . . . . . . . . 11
⊢ ;25 ∈ ℕ |
114 | 113 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ ;25 ∈
ℕ) |
115 | 114 | nnred 11988 |
. . . . . . . . 9
⊢ (⊤
→ ;25 ∈
ℝ) |
116 | | 9nn 12071 |
. . . . . . . . . . 11
⊢ 9 ∈
ℕ |
117 | 116 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ 9 ∈ ℕ) |
118 | 117 | nnrpd 12770 |
. . . . . . . . 9
⊢ (⊤
→ 9 ∈ ℝ+) |
119 | 115, 5, 118 | ltdivmul2d 12824 |
. . . . . . . 8
⊢ (⊤
→ ((;25 / 9) < 3 ↔
;25 < (3 ·
9))) |
120 | 112, 119 | mpbird 256 |
. . . . . . 7
⊢ (⊤
→ (;25 / 9) <
3) |
121 | 101, 120 | eqbrtrd 5096 |
. . . . . 6
⊢ (⊤
→ ((5 · 5) / (3 · 3)) < 3) |
122 | 97, 121 | eqbrtrd 5096 |
. . . . 5
⊢ (⊤
→ ((5 / 3) · (5 / 3)) < 3) |
123 | 95, 122 | eqbrtrd 5096 |
. . . 4
⊢ (⊤
→ ((5 / 3)↑2) < 3) |
124 | 18, 85, 5, 93, 123 | lttrd 11136 |
. . 3
⊢ (⊤
→ ((2 logb 3)↑2) < 3) |
125 | 79, 124 | jca 512 |
. 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) |