Proof of Theorem aks4d1p1p4
Step | Hyp | Ref
| Expression |
1 | | aks4d1p1p4.1 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | 1 | nnred 11732 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℝ) |
3 | | 2re 11791 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
4 | 3 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℝ) |
5 | | 2pos 11820 |
. . . . . . . . . 10
⊢ 0 <
2 |
6 | 5 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 2) |
7 | 1 | nngt0d 11766 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 𝑁) |
8 | | 1red 10721 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℝ) |
9 | | 1lt2 11888 |
. . . . . . . . . . . . . . . . 17
⊢ 1 <
2 |
10 | 9 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 < 2) |
11 | 8, 10 | ltned 10855 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ≠ 2) |
12 | 11 | necomd 2989 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ≠ 1) |
13 | 4, 6, 2, 7, 12 | relogbcld 39597 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 logb 𝑁) ∈
ℝ) |
14 | | 5nn0 11997 |
. . . . . . . . . . . . . 14
⊢ 5 ∈
ℕ0 |
15 | 14 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 5 ∈
ℕ0) |
16 | 13, 15 | reexpcld 13620 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 logb 𝑁)↑5) ∈
ℝ) |
17 | | ceilcl 13304 |
. . . . . . . . . . . 12
⊢ (((2
logb 𝑁)↑5)
∈ ℝ → (⌈‘((2 logb 𝑁)↑5)) ∈ ℤ) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌈‘((2
logb 𝑁)↑5))
∈ ℤ) |
19 | 18 | zred 12169 |
. . . . . . . . . 10
⊢ (𝜑 → (⌈‘((2
logb 𝑁)↑5))
∈ ℝ) |
20 | | aks4d1p1p4.3 |
. . . . . . . . . . . 12
⊢ 𝐵 = (⌈‘((2
logb 𝑁)↑5)) |
21 | 20 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 = (⌈‘((2 logb 𝑁)↑5))) |
22 | 21 | eleq1d 2817 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 ∈ ℝ ↔ (⌈‘((2
logb 𝑁)↑5))
∈ ℝ)) |
23 | 19, 22 | mpbird 260 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℝ) |
24 | | 0red 10723 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℝ) |
25 | | 7re 11810 |
. . . . . . . . . . 11
⊢ 7 ∈
ℝ |
26 | 25 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 7 ∈
ℝ) |
27 | | 7pos 11828 |
. . . . . . . . . . 11
⊢ 0 <
7 |
28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < 7) |
29 | | aks4d1p1p4.4 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 3 ≤ 𝑁) |
30 | 2, 29 | 3lexlogpow5ineq3 39682 |
. . . . . . . . . . . 12
⊢ (𝜑 → 7 < ((2 logb
𝑁)↑5)) |
31 | 26, 16, 30 | ltled 10867 |
. . . . . . . . . . 11
⊢ (𝜑 → 7 ≤ ((2 logb
𝑁)↑5)) |
32 | | ceilge 13306 |
. . . . . . . . . . . . 13
⊢ (((2
logb 𝑁)↑5)
∈ ℝ → ((2 logb 𝑁)↑5) ≤ (⌈‘((2
logb 𝑁)↑5))) |
33 | 16, 32 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 logb 𝑁)↑5) ≤
(⌈‘((2 logb 𝑁)↑5))) |
34 | 33, 21 | breqtrrd 5059 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 logb 𝑁)↑5) ≤ 𝐵) |
35 | 26, 16, 23, 31, 34 | letrd 10876 |
. . . . . . . . . 10
⊢ (𝜑 → 7 ≤ 𝐵) |
36 | 24, 26, 23, 28, 35 | ltletrd 10879 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 𝐵) |
37 | 4, 6, 23, 36, 12 | relogbcld 39597 |
. . . . . . . 8
⊢ (𝜑 → (2 logb 𝐵) ∈
ℝ) |
38 | 37 | flcld 13260 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(2
logb 𝐵)) ∈
ℤ) |
39 | 24, 8 | readdcld 10749 |
. . . . . . . . 9
⊢ (𝜑 → (0 + 1) ∈
ℝ) |
40 | 38 | zred 12169 |
. . . . . . . . . 10
⊢ (𝜑 → (⌊‘(2
logb 𝐵)) ∈
ℝ) |
41 | 40, 8 | readdcld 10749 |
. . . . . . . . 9
⊢ (𝜑 → ((⌊‘(2
logb 𝐵)) + 1)
∈ ℝ) |
42 | 4, 6, 4, 6, 12 | relogbcld 39597 |
. . . . . . . . . 10
⊢ (𝜑 → (2 logb 2)
∈ ℝ) |
43 | 8 | leidd 11285 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ≤ 1) |
44 | | 1cnd 10715 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
ℂ) |
45 | 44 | addid2d 10920 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 + 1) =
1) |
46 | 4 | recnd 10748 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
ℂ) |
47 | 24, 6 | gtned 10854 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ≠ 0) |
48 | | logbid1 25506 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 2) =
1) |
49 | 46, 47, 12, 48 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 logb 2) =
1) |
50 | 49 | eqcomd 2744 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 = (2 logb
2)) |
51 | 50 | eqcomd 2744 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 logb 2) =
1) |
52 | 45, 51 | breq12d 5044 |
. . . . . . . . . . 11
⊢ (𝜑 → ((0 + 1) ≤ (2
logb 2) ↔ 1 ≤ 1)) |
53 | 43, 52 | mpbird 260 |
. . . . . . . . . 10
⊢ (𝜑 → (0 + 1) ≤ (2
logb 2)) |
54 | | 5re 11804 |
. . . . . . . . . . . . . . 15
⊢ 5 ∈
ℝ |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 5 ∈
ℝ) |
56 | 4, 55 | readdcld 10749 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 + 5) ∈
ℝ) |
57 | 3, 14 | nn0addge1i 12025 |
. . . . . . . . . . . . . 14
⊢ 2 ≤ (2
+ 5) |
58 | 57 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 2 ≤ (2 +
5)) |
59 | 3 | recni 10734 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℂ |
60 | | 5cn 11805 |
. . . . . . . . . . . . . . . . 17
⊢ 5 ∈
ℂ |
61 | 59, 60 | addcomi 10910 |
. . . . . . . . . . . . . . . 16
⊢ (2 + 5) =
(5 + 2) |
62 | | 5p2e7 11873 |
. . . . . . . . . . . . . . . 16
⊢ (5 + 2) =
7 |
63 | 61, 62 | eqtri 2761 |
. . . . . . . . . . . . . . 15
⊢ (2 + 5) =
7 |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 + 5) =
7) |
65 | 26 | leidd 11285 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 7 ≤ 7) |
66 | 64, 65 | eqbrtrd 5053 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 + 5) ≤
7) |
67 | 4, 56, 26, 58, 66 | letrd 10876 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ≤ 7) |
68 | 4, 26, 23, 67, 35 | letrd 10876 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ≤ 𝐵) |
69 | | 2z 12096 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
70 | 69 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 2 ∈
ℤ) |
71 | 70 | uzidd 12341 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
(ℤ≥‘2)) |
72 | | 2rp 12478 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ+ |
73 | 72 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℝ+) |
74 | 23, 36 | elrpd 12512 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
75 | | logbleb 25521 |
. . . . . . . . . . . 12
⊢ ((2
∈ (ℤ≥‘2) ∧ 2 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) → (2 ≤ 𝐵 ↔ (2 logb 2) ≤ (2
logb 𝐵))) |
76 | 71, 73, 74, 75 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 ≤ 𝐵 ↔ (2 logb 2) ≤ (2
logb 𝐵))) |
77 | 68, 76 | mpbid 235 |
. . . . . . . . . 10
⊢ (𝜑 → (2 logb 2) ≤
(2 logb 𝐵)) |
78 | 39, 42, 37, 53, 77 | letrd 10876 |
. . . . . . . . 9
⊢ (𝜑 → (0 + 1) ≤ (2
logb 𝐵)) |
79 | | fllep1 13263 |
. . . . . . . . . 10
⊢ ((2
logb 𝐵) ∈
ℝ → (2 logb 𝐵) ≤ ((⌊‘(2 logb
𝐵)) + 1)) |
80 | 37, 79 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (2 logb 𝐵) ≤ ((⌊‘(2
logb 𝐵)) +
1)) |
81 | 39, 37, 41, 78, 80 | letrd 10876 |
. . . . . . . 8
⊢ (𝜑 → (0 + 1) ≤
((⌊‘(2 logb 𝐵)) + 1)) |
82 | 24, 40, 8 | leadd1d 11313 |
. . . . . . . 8
⊢ (𝜑 → (0 ≤ (⌊‘(2
logb 𝐵)) ↔
(0 + 1) ≤ ((⌊‘(2 logb 𝐵)) + 1))) |
83 | 81, 82 | mpbird 260 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (⌊‘(2
logb 𝐵))) |
84 | 38, 83 | jca 515 |
. . . . . 6
⊢ (𝜑 → ((⌊‘(2
logb 𝐵)) ∈
ℤ ∧ 0 ≤ (⌊‘(2 logb 𝐵)))) |
85 | | elnn0z 12076 |
. . . . . 6
⊢
((⌊‘(2 logb 𝐵)) ∈ ℕ0 ↔
((⌊‘(2 logb 𝐵)) ∈ ℤ ∧ 0 ≤
(⌊‘(2 logb 𝐵)))) |
86 | 84, 85 | sylibr 237 |
. . . . 5
⊢ (𝜑 → (⌊‘(2
logb 𝐵)) ∈
ℕ0) |
87 | 2, 86 | reexpcld 13620 |
. . . 4
⊢ (𝜑 → (𝑁↑(⌊‘(2 logb
𝐵))) ∈
ℝ) |
88 | | fzfid 13433 |
. . . . 5
⊢ (𝜑 → (1...(⌊‘((2
logb 𝑁)↑2))) ∈ Fin) |
89 | 2 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑁 ∈ ℝ) |
90 | | elfznn 13028 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) → 𝑘 ∈ ℕ) |
91 | 90 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑘 ∈ ℕ) |
92 | 91 | nnnn0d 12037 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑘 ∈ ℕ0) |
93 | 89, 92 | reexpcld 13620 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (𝑁↑𝑘) ∈ ℝ) |
94 | | 1red 10721 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 ∈
ℝ) |
95 | 93, 94 | resubcld 11147 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → ((𝑁↑𝑘) − 1) ∈ ℝ) |
96 | 88, 95 | fprodrecl 15400 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1) ∈ ℝ) |
97 | 87, 96 | remulcld 10750 |
. . 3
⊢ (𝜑 → ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) ∈
ℝ) |
98 | | aks4d1p1p4.2 |
. . . . 5
⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) |
99 | 98 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐴 = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1))) |
100 | 99 | eleq1d 2817 |
. . 3
⊢ (𝜑 → (𝐴 ∈ ℝ ↔ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) ∈
ℝ)) |
101 | 97, 100 | mpbird 260 |
. 2
⊢ (𝜑 → 𝐴 ∈ ℝ) |
102 | | aks4d1p1p4.7 |
. . . . . . . . 9
⊢ 𝐸 = ((2 logb 𝑁)↑4) |
103 | 102 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 = ((2 logb 𝑁)↑4)) |
104 | 103 | oveq2d 7187 |
. . . . . . 7
⊢ (𝜑 → (𝑁↑𝑐𝐸) = (𝑁↑𝑐((2
logb 𝑁)↑4))) |
105 | | 2cnd 11795 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℂ) |
106 | 73 | rpne0d 12520 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 2 ≠ 0) |
107 | 106, 12 | nelprd 4548 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ 2 ∈ {0,
1}) |
108 | 105, 107 | eldifd 3855 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈ (ℂ ∖
{0, 1})) |
109 | 2 | recnd 10748 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) |
110 | 24, 7 | ltned 10855 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ≠ 𝑁) |
111 | | necom 2987 |
. . . . . . . . . . . . . . . 16
⊢ (0 ≠
𝑁 ↔ 𝑁 ≠ 0) |
112 | 111 | imbi2i 339 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 → 0 ≠ 𝑁) ↔ (𝜑 → 𝑁 ≠ 0)) |
113 | 110, 112 | mpbi 233 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ≠ 0) |
114 | 113 | neneqd 2939 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑁 = 0) |
115 | | c0ex 10714 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
V |
116 | 115 | elsn2 4556 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ {0} ↔ 𝑁 = 0) |
117 | 114, 116 | sylnibr 332 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ 𝑁 ∈ {0}) |
118 | 109, 117 | eldifd 3855 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ (ℂ ∖
{0})) |
119 | | cxplogb 25524 |
. . . . . . . . . . 11
⊢ ((2
∈ (ℂ ∖ {0, 1}) ∧ 𝑁 ∈ (ℂ ∖ {0})) →
(2↑𝑐(2 logb 𝑁)) = 𝑁) |
120 | 108, 118,
119 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 →
(2↑𝑐(2 logb 𝑁)) = 𝑁) |
121 | 120 | eqcomd 2744 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 = (2↑𝑐(2
logb 𝑁))) |
122 | 121 | oveq1d 7186 |
. . . . . . . 8
⊢ (𝜑 → (𝑁↑𝑐((2
logb 𝑁)↑4))
= ((2↑𝑐(2 logb 𝑁))↑𝑐((2
logb 𝑁)↑4))) |
123 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝜑 →
((2↑𝑐(2 logb 𝑁))↑𝑐((2
logb 𝑁)↑4))
= ((2↑𝑐(2 logb 𝑁))↑𝑐((2
logb 𝑁)↑4))) |
124 | 122, 123 | eqtrd 2773 |
. . . . . . 7
⊢ (𝜑 → (𝑁↑𝑐((2
logb 𝑁)↑4))
= ((2↑𝑐(2 logb 𝑁))↑𝑐((2
logb 𝑁)↑4))) |
125 | 104, 124 | eqtrd 2773 |
. . . . . 6
⊢ (𝜑 → (𝑁↑𝑐𝐸) = ((2↑𝑐(2
logb 𝑁))↑𝑐((2
logb 𝑁)↑4))) |
126 | 103 | eqcomd 2744 |
. . . . . . . . 9
⊢ (𝜑 → ((2 logb 𝑁)↑4) = 𝐸) |
127 | | 4nn0 11996 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℕ0 |
128 | 127 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 4 ∈
ℕ0) |
129 | 13, 128 | reexpcld 13620 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 logb 𝑁)↑4) ∈
ℝ) |
130 | 103 | eleq1d 2817 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸 ∈ ℝ ↔ ((2 logb
𝑁)↑4) ∈
ℝ)) |
131 | 129, 130 | mpbird 260 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ ℝ) |
132 | 131 | recnd 10748 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ ℂ) |
133 | 126, 132 | eqeltrd 2833 |
. . . . . . . 8
⊢ (𝜑 → ((2 logb 𝑁)↑4) ∈
ℂ) |
134 | 73, 13, 133 | cxpmuld 25479 |
. . . . . . 7
⊢ (𝜑 →
(2↑𝑐((2 logb 𝑁) · ((2 logb 𝑁)↑4))) =
((2↑𝑐(2 logb 𝑁))↑𝑐((2
logb 𝑁)↑4))) |
135 | 134 | eqcomd 2744 |
. . . . . 6
⊢ (𝜑 →
((2↑𝑐(2 logb 𝑁))↑𝑐((2
logb 𝑁)↑4))
= (2↑𝑐((2 logb 𝑁) · ((2 logb 𝑁)↑4)))) |
136 | 125, 135 | eqtrd 2773 |
. . . . 5
⊢ (𝜑 → (𝑁↑𝑐𝐸) = (2↑𝑐((2
logb 𝑁) ·
((2 logb 𝑁)↑4)))) |
137 | 13 | recnd 10748 |
. . . . . . . . . 10
⊢ (𝜑 → (2 logb 𝑁) ∈
ℂ) |
138 | 137 | exp1d 13598 |
. . . . . . . . 9
⊢ (𝜑 → ((2 logb 𝑁)↑1) = (2 logb
𝑁)) |
139 | 138 | eqcomd 2744 |
. . . . . . . 8
⊢ (𝜑 → (2 logb 𝑁) = ((2 logb 𝑁)↑1)) |
140 | 139 | oveq1d 7186 |
. . . . . . 7
⊢ (𝜑 → ((2 logb 𝑁) · ((2 logb
𝑁)↑4)) = (((2
logb 𝑁)↑1)
· ((2 logb 𝑁)↑4))) |
141 | | 1nn0 11993 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ0 |
142 | 141 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℕ0) |
143 | 137, 128,
142 | expaddd 13605 |
. . . . . . . 8
⊢ (𝜑 → ((2 logb 𝑁)↑(1 + 4)) = (((2
logb 𝑁)↑1)
· ((2 logb 𝑁)↑4))) |
144 | 143 | eqcomd 2744 |
. . . . . . 7
⊢ (𝜑 → (((2 logb 𝑁)↑1) · ((2
logb 𝑁)↑4))
= ((2 logb 𝑁)↑(1 + 4))) |
145 | 140, 144 | eqtrd 2773 |
. . . . . 6
⊢ (𝜑 → ((2 logb 𝑁) · ((2 logb
𝑁)↑4)) = ((2
logb 𝑁)↑(1
+ 4))) |
146 | 145 | oveq2d 7187 |
. . . . 5
⊢ (𝜑 →
(2↑𝑐((2 logb 𝑁) · ((2 logb 𝑁)↑4))) =
(2↑𝑐((2 logb 𝑁)↑(1 + 4)))) |
147 | 136, 146 | eqtrd 2773 |
. . . 4
⊢ (𝜑 → (𝑁↑𝑐𝐸) = (2↑𝑐((2
logb 𝑁)↑(1
+ 4)))) |
148 | | 4cn 11802 |
. . . . . . . 8
⊢ 4 ∈
ℂ |
149 | | ax-1cn 10674 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
150 | | 4p1e5 11863 |
. . . . . . . 8
⊢ (4 + 1) =
5 |
151 | 148, 149,
150 | addcomli 10911 |
. . . . . . 7
⊢ (1 + 4) =
5 |
152 | 151 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (1 + 4) =
5) |
153 | 152 | oveq2d 7187 |
. . . . 5
⊢ (𝜑 → ((2 logb 𝑁)↑(1 + 4)) = ((2
logb 𝑁)↑5)) |
154 | 153 | oveq2d 7187 |
. . . 4
⊢ (𝜑 →
(2↑𝑐((2 logb 𝑁)↑(1 + 4))) =
(2↑𝑐((2 logb 𝑁)↑5))) |
155 | 147, 154 | eqtrd 2773 |
. . 3
⊢ (𝜑 → (𝑁↑𝑐𝐸) = (2↑𝑐((2
logb 𝑁)↑5))) |
156 | | 3re 11797 |
. . . . . 6
⊢ 3 ∈
ℝ |
157 | 156 | a1i 11 |
. . . . 5
⊢ (𝜑 → 3 ∈
ℝ) |
158 | | 0le1 11242 |
. . . . . . 7
⊢ 0 ≤
1 |
159 | 158 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ≤ 1) |
160 | | 1lt3 11890 |
. . . . . . . 8
⊢ 1 <
3 |
161 | 160 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 1 < 3) |
162 | 8, 157, 161 | ltled 10867 |
. . . . . 6
⊢ (𝜑 → 1 ≤ 3) |
163 | 24, 8, 157, 159, 162 | letrd 10876 |
. . . . 5
⊢ (𝜑 → 0 ≤ 3) |
164 | 24, 157, 2, 163, 29 | letrd 10876 |
. . . 4
⊢ (𝜑 → 0 ≤ 𝑁) |
165 | 2, 164, 131 | recxpcld 25466 |
. . 3
⊢ (𝜑 → (𝑁↑𝑐𝐸) ∈ ℝ) |
166 | 155, 165 | eqeltrrd 2834 |
. 2
⊢ (𝜑 →
(2↑𝑐((2 logb 𝑁)↑5)) ∈ ℝ) |
167 | 21 | eleq1d 2817 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∈ ℤ ↔ (⌈‘((2
logb 𝑁)↑5))
∈ ℤ)) |
168 | 18, 167 | mpbird 260 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℤ) |
169 | 24, 23, 36 | ltled 10867 |
. . . . 5
⊢ (𝜑 → 0 ≤ 𝐵) |
170 | 168, 169 | jca 515 |
. . . 4
⊢ (𝜑 → (𝐵 ∈ ℤ ∧ 0 ≤ 𝐵)) |
171 | | elnn0z 12076 |
. . . 4
⊢ (𝐵 ∈ ℕ0
↔ (𝐵 ∈ ℤ
∧ 0 ≤ 𝐵)) |
172 | 170, 171 | sylibr 237 |
. . 3
⊢ (𝜑 → 𝐵 ∈
ℕ0) |
173 | 4, 172 | reexpcld 13620 |
. 2
⊢ (𝜑 → (2↑𝐵) ∈ ℝ) |
174 | 2, 7 | elrpd 12512 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
175 | 16, 8 | readdcld 10749 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 logb 𝑁)↑5) + 1) ∈
ℝ) |
176 | 15 | nn0zd 12167 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 5 ∈
ℤ) |
177 | | logb1 25507 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 1) =
0) |
178 | 46, 47, 12, 177 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 logb 1) =
0) |
179 | 178, 24 | eqeltrd 2833 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 logb 1)
∈ ℝ) |
180 | 24 | leidd 11285 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ≤ 0) |
181 | 178 | eqcomd 2744 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 = (2 logb
1)) |
182 | 180, 181 | breqtrd 5057 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤ (2 logb
1)) |
183 | 8, 157, 2, 161, 29 | ltletrd 10879 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 < 𝑁) |
184 | | 1rp 12477 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ+ |
185 | 184 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℝ+) |
186 | | logblt 25522 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ (ℤ≥‘2) ∧ 1 ∈ ℝ+
∧ 𝑁 ∈
ℝ+) → (1 < 𝑁 ↔ (2 logb 1) < (2
logb 𝑁))) |
187 | 71, 185, 174, 186 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 < 𝑁 ↔ (2 logb 1) < (2
logb 𝑁))) |
188 | 183, 187 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 logb 1) <
(2 logb 𝑁)) |
189 | 24, 179, 13, 182, 188 | lelttrd 10877 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < (2 logb
𝑁)) |
190 | 13, 176, 189 | 3jca 1129 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 logb 𝑁) ∈ ℝ ∧ 5 ∈
ℤ ∧ 0 < (2 logb 𝑁))) |
191 | | expgt0 13555 |
. . . . . . . . . . . 12
⊢ (((2
logb 𝑁) ∈
ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 logb 𝑁)) → 0 < ((2
logb 𝑁)↑5)) |
192 | 190, 191 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < ((2 logb
𝑁)↑5)) |
193 | | ltp1 11559 |
. . . . . . . . . . . 12
⊢ (((2
logb 𝑁)↑5)
∈ ℝ → ((2 logb 𝑁)↑5) < (((2 logb 𝑁)↑5) + 1)) |
194 | 16, 193 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 logb 𝑁)↑5) < (((2
logb 𝑁)↑5)
+ 1)) |
195 | 24, 16, 175, 192, 194 | lttrd 10880 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < (((2
logb 𝑁)↑5)
+ 1)) |
196 | 4, 6, 175, 195, 12 | relogbcld 39597 |
. . . . . . . . 9
⊢ (𝜑 → (2 logb (((2
logb 𝑁)↑5)
+ 1)) ∈ ℝ) |
197 | | aks4d1p1p4.5 |
. . . . . . . . . . 11
⊢ 𝐶 = (2 logb (((2
logb 𝑁)↑5)
+ 1)) |
198 | 197 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 = (2 logb (((2 logb
𝑁)↑5) +
1))) |
199 | 198 | eleq1d 2817 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 ∈ ℝ ↔ (2 logb
(((2 logb 𝑁)↑5) + 1)) ∈
ℝ)) |
200 | 196, 199 | mpbird 260 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℝ) |
201 | 13 | resqcld 13704 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 logb 𝑁)↑2) ∈
ℝ) |
202 | | aks4d1p1p4.6 |
. . . . . . . . . . . 12
⊢ 𝐷 = ((2 logb 𝑁)↑2) |
203 | 202 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 = ((2 logb 𝑁)↑2)) |
204 | 203 | eleq1d 2817 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷 ∈ ℝ ↔ ((2 logb
𝑁)↑2) ∈
ℝ)) |
205 | 201, 204 | mpbird 260 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ ℝ) |
206 | 205 | rehalfcld 11964 |
. . . . . . . 8
⊢ (𝜑 → (𝐷 / 2) ∈ ℝ) |
207 | 200, 206 | readdcld 10749 |
. . . . . . 7
⊢ (𝜑 → (𝐶 + (𝐷 / 2)) ∈ ℝ) |
208 | 131, 4, 106 | redivcld 11547 |
. . . . . . 7
⊢ (𝜑 → (𝐸 / 2) ∈ ℝ) |
209 | 207, 208 | readdcld 10749 |
. . . . . 6
⊢ (𝜑 → ((𝐶 + (𝐷 / 2)) + (𝐸 / 2)) ∈ ℝ) |
210 | 174, 209 | rpcxpcld 25475 |
. . . . 5
⊢ (𝜑 → (𝑁↑𝑐((𝐶 + (𝐷 / 2)) + (𝐸 / 2))) ∈
ℝ+) |
211 | 210 | rpred 12515 |
. . . 4
⊢ (𝜑 → (𝑁↑𝑐((𝐶 + (𝐷 / 2)) + (𝐸 / 2))) ∈ ℝ) |
212 | 1, 98, 20, 29 | aks4d1p1p2 39694 |
. . . . 5
⊢ (𝜑 → 𝐴 < (𝑁↑𝑐(((2
logb (((2 logb 𝑁)↑5) + 1)) + (((2 logb 𝑁)↑2) / 2)) + (((2
logb 𝑁)↑4)
/ 2)))) |
213 | 126 | oveq1d 7186 |
. . . . . . . 8
⊢ (𝜑 → (((2 logb 𝑁)↑4) / 2) = (𝐸 / 2)) |
214 | 213 | oveq2d 7187 |
. . . . . . 7
⊢ (𝜑 → (((2 logb (((2
logb 𝑁)↑5)
+ 1)) + (((2 logb 𝑁)↑2) / 2)) + (((2 logb 𝑁)↑4) / 2)) = (((2
logb (((2 logb 𝑁)↑5) + 1)) + (((2 logb 𝑁)↑2) / 2)) + (𝐸 / 2))) |
215 | 198 | eqcomd 2744 |
. . . . . . . . . 10
⊢ (𝜑 → (2 logb (((2
logb 𝑁)↑5)
+ 1)) = 𝐶) |
216 | 215 | oveq1d 7186 |
. . . . . . . . 9
⊢ (𝜑 → ((2 logb (((2
logb 𝑁)↑5)
+ 1)) + (((2 logb 𝑁)↑2) / 2)) = (𝐶 + (((2 logb 𝑁)↑2) / 2))) |
217 | 203 | eqcomd 2744 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 logb 𝑁)↑2) = 𝐷) |
218 | 217 | oveq1d 7186 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 logb 𝑁)↑2) / 2) = (𝐷 / 2)) |
219 | 218 | oveq2d 7187 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 + (((2 logb 𝑁)↑2) / 2)) = (𝐶 + (𝐷 / 2))) |
220 | 216, 219 | eqtrd 2773 |
. . . . . . . 8
⊢ (𝜑 → ((2 logb (((2
logb 𝑁)↑5)
+ 1)) + (((2 logb 𝑁)↑2) / 2)) = (𝐶 + (𝐷 / 2))) |
221 | 220 | oveq1d 7186 |
. . . . . . 7
⊢ (𝜑 → (((2 logb (((2
logb 𝑁)↑5)
+ 1)) + (((2 logb 𝑁)↑2) / 2)) + (𝐸 / 2)) = ((𝐶 + (𝐷 / 2)) + (𝐸 / 2))) |
222 | 214, 221 | eqtrd 2773 |
. . . . . 6
⊢ (𝜑 → (((2 logb (((2
logb 𝑁)↑5)
+ 1)) + (((2 logb 𝑁)↑2) / 2)) + (((2 logb 𝑁)↑4) / 2)) = ((𝐶 + (𝐷 / 2)) + (𝐸 / 2))) |
223 | 222 | oveq2d 7187 |
. . . . 5
⊢ (𝜑 → (𝑁↑𝑐(((2
logb (((2 logb 𝑁)↑5) + 1)) + (((2 logb 𝑁)↑2) / 2)) + (((2
logb 𝑁)↑4)
/ 2))) = (𝑁↑𝑐((𝐶 + (𝐷 / 2)) + (𝐸 / 2)))) |
224 | 212, 223 | breqtrd 5057 |
. . . 4
⊢ (𝜑 → 𝐴 < (𝑁↑𝑐((𝐶 + (𝐷 / 2)) + (𝐸 / 2)))) |
225 | 200 | recnd 10748 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ ℂ) |
226 | 225, 105,
106 | divcan3d 11500 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 · 𝐶) / 2) = 𝐶) |
227 | 226 | eqcomd 2744 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 = ((2 · 𝐶) / 2)) |
228 | 227 | oveq1d 7186 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 + (𝐷 / 2)) = (((2 · 𝐶) / 2) + (𝐷 / 2))) |
229 | 4, 200 | remulcld 10750 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 · 𝐶) ∈
ℝ) |
230 | 229 | recnd 10748 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · 𝐶) ∈
ℂ) |
231 | 205 | recnd 10748 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ ℂ) |
232 | 230, 231,
46, 106 | divdird 11533 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 · 𝐶) + 𝐷) / 2) = (((2 · 𝐶) / 2) + (𝐷 / 2))) |
233 | 232 | eqcomd 2744 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝐶) / 2) + (𝐷 / 2)) = (((2 · 𝐶) + 𝐷) / 2)) |
234 | 228, 233 | eqtrd 2773 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 + (𝐷 / 2)) = (((2 · 𝐶) + 𝐷) / 2)) |
235 | | aks4d1p1p4.8 |
. . . . . . . . 9
⊢ (𝜑 → ((2 · 𝐶) + 𝐷) ≤ 𝐸) |
236 | 229, 205 | readdcld 10749 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 · 𝐶) + 𝐷) ∈ ℝ) |
237 | 236, 131,
73 | lediv1d 12561 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝐶) + 𝐷) ≤ 𝐸 ↔ (((2 · 𝐶) + 𝐷) / 2) ≤ (𝐸 / 2))) |
238 | 235, 237 | mpbid 235 |
. . . . . . . 8
⊢ (𝜑 → (((2 · 𝐶) + 𝐷) / 2) ≤ (𝐸 / 2)) |
239 | 234, 238 | eqbrtrd 5053 |
. . . . . . 7
⊢ (𝜑 → (𝐶 + (𝐷 / 2)) ≤ (𝐸 / 2)) |
240 | 207, 208,
208, 239 | leadd1dd 11333 |
. . . . . 6
⊢ (𝜑 → ((𝐶 + (𝐷 / 2)) + (𝐸 / 2)) ≤ ((𝐸 / 2) + (𝐸 / 2))) |
241 | 132 | 2halvesd 11963 |
. . . . . 6
⊢ (𝜑 → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸) |
242 | 240, 241 | breqtrd 5057 |
. . . . 5
⊢ (𝜑 → ((𝐶 + (𝐷 / 2)) + (𝐸 / 2)) ≤ 𝐸) |
243 | 2, 183, 209, 131 | cxpled 25463 |
. . . . 5
⊢ (𝜑 → (((𝐶 + (𝐷 / 2)) + (𝐸 / 2)) ≤ 𝐸 ↔ (𝑁↑𝑐((𝐶 + (𝐷 / 2)) + (𝐸 / 2))) ≤ (𝑁↑𝑐𝐸))) |
244 | 242, 243 | mpbid 235 |
. . . 4
⊢ (𝜑 → (𝑁↑𝑐((𝐶 + (𝐷 / 2)) + (𝐸 / 2))) ≤ (𝑁↑𝑐𝐸)) |
245 | 101, 211,
165, 224, 244 | ltletrd 10879 |
. . 3
⊢ (𝜑 → 𝐴 < (𝑁↑𝑐𝐸)) |
246 | 245, 155 | breqtrd 5057 |
. 2
⊢ (𝜑 → 𝐴 < (2↑𝑐((2
logb 𝑁)↑5))) |
247 | | 1le2 11926 |
. . . . 5
⊢ 1 ≤
2 |
248 | 247 | a1i 11 |
. . . 4
⊢ (𝜑 → 1 ≤ 2) |
249 | 172 | nn0red 12038 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℝ) |
250 | 21 | eqcomd 2744 |
. . . . 5
⊢ (𝜑 → (⌈‘((2
logb 𝑁)↑5))
= 𝐵) |
251 | 33, 250 | breqtrd 5057 |
. . . 4
⊢ (𝜑 → ((2 logb 𝑁)↑5) ≤ 𝐵) |
252 | 4, 248, 16, 249, 251 | cxplead 25464 |
. . 3
⊢ (𝜑 →
(2↑𝑐((2 logb 𝑁)↑5)) ≤
(2↑𝑐𝐵)) |
253 | | cxpexp 25411 |
. . . 4
⊢ ((2
∈ ℂ ∧ 𝐵
∈ ℕ0) → (2↑𝑐𝐵) = (2↑𝐵)) |
254 | 105, 172,
253 | syl2anc 587 |
. . 3
⊢ (𝜑 →
(2↑𝑐𝐵) = (2↑𝐵)) |
255 | 252, 254 | breqtrd 5057 |
. 2
⊢ (𝜑 →
(2↑𝑐((2 logb 𝑁)↑5)) ≤ (2↑𝐵)) |
256 | 101, 166,
173, 246, 255 | ltletrd 10879 |
1
⊢ (𝜑 → 𝐴 < (2↑𝐵)) |