Proof of Theorem 3lexlogpow5ineq1
Step | Hyp | Ref
| Expression |
1 | | 2cn 11700 |
. . . . . . 7
⊢ 2 ∈
ℂ |
2 | | halfcn 11840 |
. . . . . . 7
⊢ (1 / 2)
∈ ℂ |
3 | | 5nn0 11905 |
. . . . . . 7
⊢ 5 ∈
ℕ0 |
4 | 1, 2, 3 | 3pm3.2i 1336 |
. . . . . 6
⊢ (2 ∈
ℂ ∧ (1 / 2) ∈ ℂ ∧ 5 ∈
ℕ0) |
5 | | mulexp 13464 |
. . . . . 6
⊢ ((2
∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ 5 ∈ ℕ0)
→ ((2 · (1 / 2))↑5) = ((2↑5) · ((1 /
2)↑5))) |
6 | 4, 5 | ax-mp 5 |
. . . . 5
⊢ ((2
· (1 / 2))↑5) = ((2↑5) · ((1 /
2)↑5)) |
7 | 6 | oveq2i 7146 |
. . . 4
⊢ (7
· ((2 · (1 / 2))↑5)) = (7 · ((2↑5) · ((1
/ 2)↑5))) |
8 | | 2ne0 11729 |
. . . . . . . . 9
⊢ 2 ≠
0 |
9 | 1, 8 | recidi 11360 |
. . . . . . . 8
⊢ (2
· (1 / 2)) = 1 |
10 | 9 | oveq1i 7145 |
. . . . . . 7
⊢ ((2
· (1 / 2))↑5) = (1↑5) |
11 | | 1nn0 11901 |
. . . . . . . 8
⊢ 1 ∈
ℕ0 |
12 | | 4nn0 11904 |
. . . . . . . 8
⊢ 4 ∈
ℕ0 |
13 | | 4p1e5 11771 |
. . . . . . . 8
⊢ (4 + 1) =
5 |
14 | | 2nn0 11902 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
15 | | 2t2e4 11789 |
. . . . . . . . . . 11
⊢ (2
· 2) = 4 |
16 | | sq1 13554 |
. . . . . . . . . . 11
⊢
(1↑2) = 1 |
17 | | 1t1e1 11787 |
. . . . . . . . . . 11
⊢ (1
· 1) = 1 |
18 | 11, 14, 15, 16, 17 | numexp2x 16405 |
. . . . . . . . . 10
⊢
(1↑4) = 1 |
19 | 18 | oveq1i 7145 |
. . . . . . . . 9
⊢
((1↑4) · 1) = (1 · 1) |
20 | 19, 17 | eqtri 2821 |
. . . . . . . 8
⊢
((1↑4) · 1) = 1 |
21 | 11, 12, 13, 20 | numexpp1 16404 |
. . . . . . 7
⊢
(1↑5) = 1 |
22 | 10, 21 | eqtri 2821 |
. . . . . 6
⊢ ((2
· (1 / 2))↑5) = 1 |
23 | 22 | oveq2i 7146 |
. . . . 5
⊢ (7
· ((2 · (1 / 2))↑5)) = (7 · 1) |
24 | | 7cn 11719 |
. . . . . 6
⊢ 7 ∈
ℂ |
25 | 24 | mulid1i 10634 |
. . . . 5
⊢ (7
· 1) = 7 |
26 | 23, 25 | eqtri 2821 |
. . . 4
⊢ (7
· ((2 · (1 / 2))↑5)) = 7 |
27 | 7, 26 | eqtr3i 2823 |
. . 3
⊢ (7
· ((2↑5) · ((1 / 2)↑5))) = 7 |
28 | | 2exp5 16412 |
. . . . . 6
⊢
(2↑5) = ;32 |
29 | | 3nn0 11903 |
. . . . . . . 8
⊢ 3 ∈
ℕ0 |
30 | 29, 14 | deccl 12101 |
. . . . . . 7
⊢ ;32 ∈
ℕ0 |
31 | 30 | nn0cni 11897 |
. . . . . 6
⊢ ;32 ∈ ℂ |
32 | 28, 31 | eqeltri 2886 |
. . . . 5
⊢
(2↑5) ∈ ℂ |
33 | | halfre 11839 |
. . . . . . . 8
⊢ (1 / 2)
∈ ℝ |
34 | 33, 3 | pm3.2i 474 |
. . . . . . 7
⊢ ((1 / 2)
∈ ℝ ∧ 5 ∈ ℕ0) |
35 | | reexpcl 13442 |
. . . . . . 7
⊢ (((1 / 2)
∈ ℝ ∧ 5 ∈ ℕ0) → ((1 / 2)↑5)
∈ ℝ) |
36 | 34, 35 | ax-mp 5 |
. . . . . 6
⊢ ((1 /
2)↑5) ∈ ℝ |
37 | 36 | recni 10644 |
. . . . 5
⊢ ((1 /
2)↑5) ∈ ℂ |
38 | 24, 32, 37 | mulassi 10641 |
. . . 4
⊢ ((7
· (2↑5)) · ((1 / 2)↑5)) = (7 · ((2↑5)
· ((1 / 2)↑5))) |
39 | 14, 14 | deccl 12101 |
. . . . . . 7
⊢ ;22 ∈
ℕ0 |
40 | 14, 12 | deccl 12101 |
. . . . . . 7
⊢ ;24 ∈
ℕ0 |
41 | | 4lt9 11828 |
. . . . . . . 8
⊢ 4 <
9 |
42 | | 4re 11709 |
. . . . . . . . 9
⊢ 4 ∈
ℝ |
43 | | 9re 11724 |
. . . . . . . . 9
⊢ 9 ∈
ℝ |
44 | 42, 43 | ltlei 10751 |
. . . . . . . 8
⊢ (4 < 9
→ 4 ≤ 9) |
45 | 41, 44 | ax-mp 5 |
. . . . . . 7
⊢ 4 ≤
9 |
46 | | 4nn 11708 |
. . . . . . . 8
⊢ 4 ∈
ℕ |
47 | | 2lt4 11800 |
. . . . . . . 8
⊢ 2 <
4 |
48 | 14, 14, 46, 47 | declt 12114 |
. . . . . . 7
⊢ ;22 < ;24 |
49 | 39, 40, 12, 29, 45, 48 | declth 12116 |
. . . . . 6
⊢ ;;224 < ;;243 |
50 | 31, 24 | mulcomi 10638 |
. . . . . . . . 9
⊢ (;32 · 7) = (7 · ;32) |
51 | 28 | oveq2i 7146 |
. . . . . . . . 9
⊢ (7
· (2↑5)) = (7 · ;32) |
52 | 50, 51 | eqtr4i 2824 |
. . . . . . . 8
⊢ (;32 · 7) = (7 ·
(2↑5)) |
53 | | 7nn0 11907 |
. . . . . . . . 9
⊢ 7 ∈
ℕ0 |
54 | | eqid 2798 |
. . . . . . . . 9
⊢ ;32 = ;32 |
55 | | 1p1e2 11750 |
. . . . . . . . . 10
⊢ (1 + 1) =
2 |
56 | | 3cn 11706 |
. . . . . . . . . . 11
⊢ 3 ∈
ℂ |
57 | | 7t3e21 12196 |
. . . . . . . . . . 11
⊢ (7
· 3) = ;21 |
58 | 24, 56, 57 | mulcomli 10639 |
. . . . . . . . . 10
⊢ (3
· 7) = ;21 |
59 | 14, 11, 55, 58 | decsuc 12117 |
. . . . . . . . 9
⊢ ((3
· 7) + 1) = ;22 |
60 | | 7t2e14 12195 |
. . . . . . . . . 10
⊢ (7
· 2) = ;14 |
61 | 24, 1, 60 | mulcomli 10639 |
. . . . . . . . 9
⊢ (2
· 7) = ;14 |
62 | 53, 29, 14, 54, 12, 11, 59, 61 | decmul1c 12151 |
. . . . . . . 8
⊢ (;32 · 7) = ;;224 |
63 | 52, 62 | eqtr3i 2823 |
. . . . . . 7
⊢ (7
· (2↑5)) = ;;224 |
64 | | 8nn0 11908 |
. . . . . . . . 9
⊢ 8 ∈
ℕ0 |
65 | | sq3 13557 |
. . . . . . . . . 10
⊢
(3↑2) = 9 |
66 | | 9t9e81 12215 |
. . . . . . . . . 10
⊢ (9
· 9) = ;81 |
67 | 29, 14, 15, 65, 66 | numexp2x 16405 |
. . . . . . . . 9
⊢
(3↑4) = ;81 |
68 | | 0nn0 11900 |
. . . . . . . . 9
⊢ 0 ∈
ℕ0 |
69 | | 8t3e24 12202 |
. . . . . . . . . 10
⊢ (8
· 3) = ;24 |
70 | | 4cn 11710 |
. . . . . . . . . . 11
⊢ 4 ∈
ℂ |
71 | 70 | addid1i 10816 |
. . . . . . . . . 10
⊢ (4 + 0) =
4 |
72 | 14, 12, 68, 69, 71 | decaddi 12146 |
. . . . . . . . 9
⊢ ((8
· 3) + 0) = ;24 |
73 | | ax-1cn 10584 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
74 | | 3t1e3 11790 |
. . . . . . . . . . 11
⊢ (3
· 1) = 3 |
75 | 29 | dec0h 12108 |
. . . . . . . . . . . 12
⊢ 3 = ;03 |
76 | 75 | eqcomi 2807 |
. . . . . . . . . . 11
⊢ ;03 = 3 |
77 | 74, 76 | eqtr4i 2824 |
. . . . . . . . . 10
⊢ (3
· 1) = ;03 |
78 | 56, 73, 77 | mulcomli 10639 |
. . . . . . . . 9
⊢ (1
· 3) = ;03 |
79 | 29, 64, 11, 67, 29, 68, 72, 78 | decmul1c 12151 |
. . . . . . . 8
⊢
((3↑4) · 3) = ;;243 |
80 | 29, 12, 13, 79 | numexpp1 16404 |
. . . . . . 7
⊢
(3↑5) = ;;243 |
81 | 63, 80 | breq12i 5039 |
. . . . . 6
⊢ ((7
· (2↑5)) < (3↑5) ↔ ;;224
< ;;243) |
82 | 49, 81 | mpbir 234 |
. . . . 5
⊢ (7
· (2↑5)) < (3↑5) |
83 | 3 | nn0zi 11995 |
. . . . . . . 8
⊢ 5 ∈
ℤ |
84 | | halfgt0 11841 |
. . . . . . . 8
⊢ 0 < (1
/ 2) |
85 | 33, 83, 84 | 3pm3.2i 1336 |
. . . . . . 7
⊢ ((1 / 2)
∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < (1 / 2)) |
86 | | expgt0 13458 |
. . . . . . 7
⊢ (((1 / 2)
∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < (1 / 2)) → 0 < ((1 /
2)↑5)) |
87 | 85, 86 | ax-mp 5 |
. . . . . 6
⊢ 0 <
((1 / 2)↑5) |
88 | | 7re 11718 |
. . . . . . . 8
⊢ 7 ∈
ℝ |
89 | | 2re 11699 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
90 | 89, 3 | pm3.2i 474 |
. . . . . . . . 9
⊢ (2 ∈
ℝ ∧ 5 ∈ ℕ0) |
91 | | reexpcl 13442 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ 5 ∈ ℕ0) → (2↑5) ∈
ℝ) |
92 | 90, 91 | ax-mp 5 |
. . . . . . . 8
⊢
(2↑5) ∈ ℝ |
93 | 88, 92 | remulcli 10646 |
. . . . . . 7
⊢ (7
· (2↑5)) ∈ ℝ |
94 | | 3re 11705 |
. . . . . . . . 9
⊢ 3 ∈
ℝ |
95 | 94, 3 | pm3.2i 474 |
. . . . . . . 8
⊢ (3 ∈
ℝ ∧ 5 ∈ ℕ0) |
96 | | reexpcl 13442 |
. . . . . . . 8
⊢ ((3
∈ ℝ ∧ 5 ∈ ℕ0) → (3↑5) ∈
ℝ) |
97 | 95, 96 | ax-mp 5 |
. . . . . . 7
⊢
(3↑5) ∈ ℝ |
98 | 93, 97, 36 | ltmul1i 11547 |
. . . . . 6
⊢ (0 <
((1 / 2)↑5) → ((7 · (2↑5)) < (3↑5) ↔ ((7
· (2↑5)) · ((1 / 2)↑5)) < ((3↑5) · ((1 /
2)↑5)))) |
99 | 87, 98 | ax-mp 5 |
. . . . 5
⊢ ((7
· (2↑5)) < (3↑5) ↔ ((7 · (2↑5)) ·
((1 / 2)↑5)) < ((3↑5) · ((1 / 2)↑5))) |
100 | 82, 99 | mpbi 233 |
. . . 4
⊢ ((7
· (2↑5)) · ((1 / 2)↑5)) < ((3↑5) · ((1 /
2)↑5)) |
101 | 38, 100 | eqbrtrri 5053 |
. . 3
⊢ (7
· ((2↑5) · ((1 / 2)↑5))) < ((3↑5) · ((1
/ 2)↑5)) |
102 | 27, 101 | eqbrtrri 5053 |
. 2
⊢ 7 <
((3↑5) · ((1 / 2)↑5)) |
103 | 56, 1, 8 | divreci 11374 |
. . . 4
⊢ (3 / 2) =
(3 · (1 / 2)) |
104 | 103 | oveq1i 7145 |
. . 3
⊢ ((3 /
2)↑5) = ((3 · (1 / 2))↑5) |
105 | 56, 2, 3 | 3pm3.2i 1336 |
. . . 4
⊢ (3 ∈
ℂ ∧ (1 / 2) ∈ ℂ ∧ 5 ∈
ℕ0) |
106 | | mulexp 13464 |
. . . 4
⊢ ((3
∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ 5 ∈ ℕ0)
→ ((3 · (1 / 2))↑5) = ((3↑5) · ((1 /
2)↑5))) |
107 | 105, 106 | ax-mp 5 |
. . 3
⊢ ((3
· (1 / 2))↑5) = ((3↑5) · ((1 /
2)↑5)) |
108 | 104, 107 | eqtr2i 2822 |
. 2
⊢
((3↑5) · ((1 / 2)↑5)) = ((3 /
2)↑5) |
109 | 102, 108 | breqtri 5055 |
1
⊢ 7 <
((3 / 2)↑5) |