Proof of Theorem aks4d1p1p4
Step | Hyp | Ref
| Expression |
1 | | aks4d1p1p4.1 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | 1 | nnred 11997 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℝ) |
3 | | 2re 12056 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
4 | 3 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℝ) |
5 | | 2pos 12085 |
. . . . . . . . . 10
⊢ 0 <
2 |
6 | 5 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 2) |
7 | 1 | nngt0d 12031 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 𝑁) |
8 | | 1red 10985 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℝ) |
9 | | 1lt2 12153 |
. . . . . . . . . . . . . . . . 17
⊢ 1 <
2 |
10 | 9 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 < 2) |
11 | 8, 10 | ltned 11120 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ≠ 2) |
12 | 11 | necomd 3000 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ≠ 1) |
13 | 4, 6, 2, 7, 12 | relogbcld 39988 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 logb 𝑁) ∈
ℝ) |
14 | | 5nn0 12262 |
. . . . . . . . . . . . . 14
⊢ 5 ∈
ℕ0 |
15 | 14 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 5 ∈
ℕ0) |
16 | 13, 15 | reexpcld 13890 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 logb 𝑁)↑5) ∈
ℝ) |
17 | | ceilcl 13571 |
. . . . . . . . . . . 12
⊢ (((2
logb 𝑁)↑5)
∈ ℝ → (⌈‘((2 logb 𝑁)↑5)) ∈ ℤ) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌈‘((2
logb 𝑁)↑5))
∈ ℤ) |
19 | 18 | zred 12435 |
. . . . . . . . . 10
⊢ (𝜑 → (⌈‘((2
logb 𝑁)↑5))
∈ ℝ) |
20 | | aks4d1p1p4.3 |
. . . . . . . . . . . 12
⊢ 𝐵 = (⌈‘((2
logb 𝑁)↑5)) |
21 | 20 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 = (⌈‘((2 logb 𝑁)↑5))) |
22 | 21 | eleq1d 2824 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 ∈ ℝ ↔ (⌈‘((2
logb 𝑁)↑5))
∈ ℝ)) |
23 | 19, 22 | mpbird 256 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℝ) |
24 | | 0red 10987 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℝ) |
25 | | 7re 12075 |
. . . . . . . . . . 11
⊢ 7 ∈
ℝ |
26 | 25 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 7 ∈
ℝ) |
27 | | 7pos 12093 |
. . . . . . . . . . 11
⊢ 0 <
7 |
28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < 7) |
29 | | aks4d1p1p4.4 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 3 ≤ 𝑁) |
30 | 2, 29 | 3lexlogpow5ineq3 40072 |
. . . . . . . . . . . 12
⊢ (𝜑 → 7 < ((2 logb
𝑁)↑5)) |
31 | 26, 16, 30 | ltled 11132 |
. . . . . . . . . . 11
⊢ (𝜑 → 7 ≤ ((2 logb
𝑁)↑5)) |
32 | | ceilge 13574 |
. . . . . . . . . . . . 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 5103 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 logb 𝑁)↑5) ≤ 𝐵) |
35 | 26, 16, 23, 31, 34 | letrd 11141 |
. . . . . . . . . 10
⊢ (𝜑 → 7 ≤ 𝐵) |
36 | 24, 26, 23, 28, 35 | ltletrd 11144 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 𝐵) |
37 | 4, 6, 23, 36, 12 | relogbcld 39988 |
. . . . . . . 8
⊢ (𝜑 → (2 logb 𝐵) ∈
ℝ) |
38 | 37 | flcld 13527 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(2
logb 𝐵)) ∈
ℤ) |
39 | 24, 8 | readdcld 11013 |
. . . . . . . . 9
⊢ (𝜑 → (0 + 1) ∈
ℝ) |
40 | 38 | zred 12435 |
. . . . . . . . . 10
⊢ (𝜑 → (⌊‘(2
logb 𝐵)) ∈
ℝ) |
41 | 40, 8 | readdcld 11013 |
. . . . . . . . 9
⊢ (𝜑 → ((⌊‘(2
logb 𝐵)) + 1)
∈ ℝ) |
42 | 4, 6, 4, 6, 12 | relogbcld 39988 |
. . . . . . . . . 10
⊢ (𝜑 → (2 logb 2)
∈ ℝ) |
43 | 8 | leidd 11550 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ≤ 1) |
44 | | 1cnd 10979 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
ℂ) |
45 | 44 | addid2d 11185 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 + 1) =
1) |
46 | 4 | recnd 11012 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
ℂ) |
47 | 24, 6 | gtned 11119 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ≠ 0) |
48 | | logbid1 25927 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 2) =
1) |
49 | 46, 47, 12, 48 | syl3anc 1370 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 logb 2) =
1) |
50 | 49 | eqcomd 2745 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 = (2 logb
2)) |
51 | 50 | eqcomd 2745 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 logb 2) =
1) |
52 | 45, 51 | breq12d 5088 |
. . . . . . . . . . 11
⊢ (𝜑 → ((0 + 1) ≤ (2
logb 2) ↔ 1 ≤ 1)) |
53 | 43, 52 | mpbird 256 |
. . . . . . . . . 10
⊢ (𝜑 → (0 + 1) ≤ (2
logb 2)) |
54 | | 5re 12069 |
. . . . . . . . . . . . . . 15
⊢ 5 ∈
ℝ |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 5 ∈
ℝ) |
56 | 4, 55 | readdcld 11013 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 + 5) ∈
ℝ) |
57 | 3, 14 | nn0addge1i 12290 |
. . . . . . . . . . . . . 14
⊢ 2 ≤ (2
+ 5) |
58 | 57 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 2 ≤ (2 +
5)) |
59 | 3 | recni 10998 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℂ |
60 | | 5cn 12070 |
. . . . . . . . . . . . . . . . 17
⊢ 5 ∈
ℂ |
61 | 59, 60 | addcomi 11175 |
. . . . . . . . . . . . . . . 16
⊢ (2 + 5) =
(5 + 2) |
62 | | 5p2e7 12138 |
. . . . . . . . . . . . . . . 16
⊢ (5 + 2) =
7 |
63 | 61, 62 | eqtri 2767 |
. . . . . . . . . . . . . . 15
⊢ (2 + 5) =
7 |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 + 5) =
7) |
65 | 26 | leidd 11550 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 7 ≤ 7) |
66 | 64, 65 | eqbrtrd 5097 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 + 5) ≤
7) |
67 | 4, 56, 26, 58, 66 | letrd 11141 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ≤ 7) |
68 | 4, 26, 23, 67, 35 | letrd 11141 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ≤ 𝐵) |
69 | | 2z 12361 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
70 | 69 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 2 ∈
ℤ) |
71 | 70 | uzidd 12607 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
(ℤ≥‘2)) |
72 | | 2rp 12744 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ+ |
73 | 72 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℝ+) |
74 | 23, 36 | elrpd 12778 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
75 | | logbleb 25942 |
. . . . . . . . . . . 12
⊢ ((2
∈ (ℤ≥‘2) ∧ 2 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) → (2 ≤ 𝐵 ↔ (2 logb 2) ≤ (2
logb 𝐵))) |
76 | 71, 73, 74, 75 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 ≤ 𝐵 ↔ (2 logb 2) ≤ (2
logb 𝐵))) |
77 | 68, 76 | mpbid 231 |
. . . . . . . . . 10
⊢ (𝜑 → (2 logb 2) ≤
(2 logb 𝐵)) |
78 | 39, 42, 37, 53, 77 | letrd 11141 |
. . . . . . . . 9
⊢ (𝜑 → (0 + 1) ≤ (2
logb 𝐵)) |
79 | | fllep1 13530 |
. . . . . . . . . 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 11141 |
. . . . . . . 8
⊢ (𝜑 → (0 + 1) ≤
((⌊‘(2 logb 𝐵)) + 1)) |
82 | 24, 40, 8 | leadd1d 11578 |
. . . . . . . 8
⊢ (𝜑 → (0 ≤ (⌊‘(2
logb 𝐵)) ↔
(0 + 1) ≤ ((⌊‘(2 logb 𝐵)) + 1))) |
83 | 81, 82 | mpbird 256 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (⌊‘(2
logb 𝐵))) |
84 | 38, 83 | jca 512 |
. . . . . 6
⊢ (𝜑 → ((⌊‘(2
logb 𝐵)) ∈
ℤ ∧ 0 ≤ (⌊‘(2 logb 𝐵)))) |
85 | | elnn0z 12341 |
. . . . . 6
⊢
((⌊‘(2 logb 𝐵)) ∈ ℕ0 ↔
((⌊‘(2 logb 𝐵)) ∈ ℤ ∧ 0 ≤
(⌊‘(2 logb 𝐵)))) |
86 | 84, 85 | sylibr 233 |
. . . . 5
⊢ (𝜑 → (⌊‘(2
logb 𝐵)) ∈
ℕ0) |
87 | 2, 86 | reexpcld 13890 |
. . . 4
⊢ (𝜑 → (𝑁↑(⌊‘(2 logb
𝐵))) ∈
ℝ) |
88 | | fzfid 13702 |
. . . . 5
⊢ (𝜑 → (1...(⌊‘((2
logb 𝑁)↑2))) ∈ Fin) |
89 | 2 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑁 ∈ ℝ) |
90 | | elfznn 13294 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) → 𝑘 ∈ ℕ) |
91 | 90 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑘 ∈ ℕ) |
92 | 91 | nnnn0d 12302 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑘 ∈ ℕ0) |
93 | 89, 92 | reexpcld 13890 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (𝑁↑𝑘) ∈ ℝ) |
94 | | 1red 10985 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 ∈
ℝ) |
95 | 93, 94 | resubcld 11412 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → ((𝑁↑𝑘) − 1) ∈ ℝ) |
96 | 88, 95 | fprodrecl 15672 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1) ∈ ℝ) |
97 | 87, 96 | remulcld 11014 |
. . 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 2824 |
. . 3
⊢ (𝜑 → (𝐴 ∈ ℝ ↔ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) ∈
ℝ)) |
101 | 97, 100 | mpbird 256 |
. 2
⊢ (𝜑 → 𝐴 ∈ ℝ) |
102 | | aks4d1p1p4.7 |
. . . . . . . . 9
⊢ 𝐸 = ((2 logb 𝑁)↑4) |
103 | 102 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 = ((2 logb 𝑁)↑4)) |
104 | 103 | oveq2d 7300 |
. . . . . . 7
⊢ (𝜑 → (𝑁↑𝑐𝐸) = (𝑁↑𝑐((2
logb 𝑁)↑4))) |
105 | | 2cnd 12060 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℂ) |
106 | 73 | rpne0d 12786 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 2 ≠ 0) |
107 | 106, 12 | nelprd 4593 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ 2 ∈ {0,
1}) |
108 | 105, 107 | eldifd 3899 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈ (ℂ ∖
{0, 1})) |
109 | 2 | recnd 11012 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) |
110 | 24, 7 | ltned 11120 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ≠ 𝑁) |
111 | | necom 2998 |
. . . . . . . . . . . . . . . 16
⊢ (0 ≠
𝑁 ↔ 𝑁 ≠ 0) |
112 | 111 | imbi2i 336 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 → 0 ≠ 𝑁) ↔ (𝜑 → 𝑁 ≠ 0)) |
113 | 110, 112 | mpbi 229 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ≠ 0) |
114 | 113 | neneqd 2949 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑁 = 0) |
115 | | c0ex 10978 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
V |
116 | 115 | elsn2 4601 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ {0} ↔ 𝑁 = 0) |
117 | 114, 116 | sylnibr 329 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ 𝑁 ∈ {0}) |
118 | 109, 117 | eldifd 3899 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ (ℂ ∖
{0})) |
119 | | cxplogb 25945 |
. . . . . . . . . . 11
⊢ ((2
∈ (ℂ ∖ {0, 1}) ∧ 𝑁 ∈ (ℂ ∖ {0})) →
(2↑𝑐(2 logb 𝑁)) = 𝑁) |
120 | 108, 118,
119 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 →
(2↑𝑐(2 logb 𝑁)) = 𝑁) |
121 | 120 | eqcomd 2745 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 = (2↑𝑐(2
logb 𝑁))) |
122 | 121 | oveq1d 7299 |
. . . . . . . 8
⊢ (𝜑 → (𝑁↑𝑐((2
logb 𝑁)↑4))
= ((2↑𝑐(2 logb 𝑁))↑𝑐((2
logb 𝑁)↑4))) |
123 | | eqidd 2740 |
. . . . . . . 8
⊢ (𝜑 →
((2↑𝑐(2 logb 𝑁))↑𝑐((2
logb 𝑁)↑4))
= ((2↑𝑐(2 logb 𝑁))↑𝑐((2
logb 𝑁)↑4))) |
124 | 122, 123 | eqtrd 2779 |
. . . . . . 7
⊢ (𝜑 → (𝑁↑𝑐((2
logb 𝑁)↑4))
= ((2↑𝑐(2 logb 𝑁))↑𝑐((2
logb 𝑁)↑4))) |
125 | 104, 124 | eqtrd 2779 |
. . . . . 6
⊢ (𝜑 → (𝑁↑𝑐𝐸) = ((2↑𝑐(2
logb 𝑁))↑𝑐((2
logb 𝑁)↑4))) |
126 | 103 | eqcomd 2745 |
. . . . . . . . 9
⊢ (𝜑 → ((2 logb 𝑁)↑4) = 𝐸) |
127 | | 4nn0 12261 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℕ0 |
128 | 127 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 4 ∈
ℕ0) |
129 | 13, 128 | reexpcld 13890 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 logb 𝑁)↑4) ∈
ℝ) |
130 | 103 | eleq1d 2824 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸 ∈ ℝ ↔ ((2 logb
𝑁)↑4) ∈
ℝ)) |
131 | 129, 130 | mpbird 256 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ ℝ) |
132 | 131 | recnd 11012 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ ℂ) |
133 | 126, 132 | eqeltrd 2840 |
. . . . . . . 8
⊢ (𝜑 → ((2 logb 𝑁)↑4) ∈
ℂ) |
134 | 73, 13, 133 | cxpmuld 25900 |
. . . . . . 7
⊢ (𝜑 →
(2↑𝑐((2 logb 𝑁) · ((2 logb 𝑁)↑4))) =
((2↑𝑐(2 logb 𝑁))↑𝑐((2
logb 𝑁)↑4))) |
135 | 134 | eqcomd 2745 |
. . . . . 6
⊢ (𝜑 →
((2↑𝑐(2 logb 𝑁))↑𝑐((2
logb 𝑁)↑4))
= (2↑𝑐((2 logb 𝑁) · ((2 logb 𝑁)↑4)))) |
136 | 125, 135 | eqtrd 2779 |
. . . . 5
⊢ (𝜑 → (𝑁↑𝑐𝐸) = (2↑𝑐((2
logb 𝑁) ·
((2 logb 𝑁)↑4)))) |
137 | 13 | recnd 11012 |
. . . . . . . . . 10
⊢ (𝜑 → (2 logb 𝑁) ∈
ℂ) |
138 | 137 | exp1d 13868 |
. . . . . . . . 9
⊢ (𝜑 → ((2 logb 𝑁)↑1) = (2 logb
𝑁)) |
139 | 138 | eqcomd 2745 |
. . . . . . . 8
⊢ (𝜑 → (2 logb 𝑁) = ((2 logb 𝑁)↑1)) |
140 | 139 | oveq1d 7299 |
. . . . . . 7
⊢ (𝜑 → ((2 logb 𝑁) · ((2 logb
𝑁)↑4)) = (((2
logb 𝑁)↑1)
· ((2 logb 𝑁)↑4))) |
141 | | 1nn0 12258 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ0 |
142 | 141 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℕ0) |
143 | 137, 128,
142 | expaddd 13875 |
. . . . . . . 8
⊢ (𝜑 → ((2 logb 𝑁)↑(1 + 4)) = (((2
logb 𝑁)↑1)
· ((2 logb 𝑁)↑4))) |
144 | 143 | eqcomd 2745 |
. . . . . . 7
⊢ (𝜑 → (((2 logb 𝑁)↑1) · ((2
logb 𝑁)↑4))
= ((2 logb 𝑁)↑(1 + 4))) |
145 | 140, 144 | eqtrd 2779 |
. . . . . 6
⊢ (𝜑 → ((2 logb 𝑁) · ((2 logb
𝑁)↑4)) = ((2
logb 𝑁)↑(1
+ 4))) |
146 | 145 | oveq2d 7300 |
. . . . 5
⊢ (𝜑 →
(2↑𝑐((2 logb 𝑁) · ((2 logb 𝑁)↑4))) =
(2↑𝑐((2 logb 𝑁)↑(1 + 4)))) |
147 | 136, 146 | eqtrd 2779 |
. . . 4
⊢ (𝜑 → (𝑁↑𝑐𝐸) = (2↑𝑐((2
logb 𝑁)↑(1
+ 4)))) |
148 | | 4cn 12067 |
. . . . . . . 8
⊢ 4 ∈
ℂ |
149 | | ax-1cn 10938 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
150 | | 4p1e5 12128 |
. . . . . . . 8
⊢ (4 + 1) =
5 |
151 | 148, 149,
150 | addcomli 11176 |
. . . . . . 7
⊢ (1 + 4) =
5 |
152 | 151 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (1 + 4) =
5) |
153 | 152 | oveq2d 7300 |
. . . . 5
⊢ (𝜑 → ((2 logb 𝑁)↑(1 + 4)) = ((2
logb 𝑁)↑5)) |
154 | 153 | oveq2d 7300 |
. . . 4
⊢ (𝜑 →
(2↑𝑐((2 logb 𝑁)↑(1 + 4))) =
(2↑𝑐((2 logb 𝑁)↑5))) |
155 | 147, 154 | eqtrd 2779 |
. . 3
⊢ (𝜑 → (𝑁↑𝑐𝐸) = (2↑𝑐((2
logb 𝑁)↑5))) |
156 | | 3re 12062 |
. . . . . 6
⊢ 3 ∈
ℝ |
157 | 156 | a1i 11 |
. . . . 5
⊢ (𝜑 → 3 ∈
ℝ) |
158 | | 0le1 11507 |
. . . . . . 7
⊢ 0 ≤
1 |
159 | 158 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ≤ 1) |
160 | | 1lt3 12155 |
. . . . . . . 8
⊢ 1 <
3 |
161 | 160 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 1 < 3) |
162 | 8, 157, 161 | ltled 11132 |
. . . . . 6
⊢ (𝜑 → 1 ≤ 3) |
163 | 24, 8, 157, 159, 162 | letrd 11141 |
. . . . 5
⊢ (𝜑 → 0 ≤ 3) |
164 | 24, 157, 2, 163, 29 | letrd 11141 |
. . . 4
⊢ (𝜑 → 0 ≤ 𝑁) |
165 | 2, 164, 131 | recxpcld 25887 |
. . 3
⊢ (𝜑 → (𝑁↑𝑐𝐸) ∈ ℝ) |
166 | 155, 165 | eqeltrrd 2841 |
. 2
⊢ (𝜑 →
(2↑𝑐((2 logb 𝑁)↑5)) ∈ ℝ) |
167 | 21 | eleq1d 2824 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∈ ℤ ↔ (⌈‘((2
logb 𝑁)↑5))
∈ ℤ)) |
168 | 18, 167 | mpbird 256 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℤ) |
169 | 24, 23, 36 | ltled 11132 |
. . . . 5
⊢ (𝜑 → 0 ≤ 𝐵) |
170 | 168, 169 | jca 512 |
. . . 4
⊢ (𝜑 → (𝐵 ∈ ℤ ∧ 0 ≤ 𝐵)) |
171 | | elnn0z 12341 |
. . . 4
⊢ (𝐵 ∈ ℕ0
↔ (𝐵 ∈ ℤ
∧ 0 ≤ 𝐵)) |
172 | 170, 171 | sylibr 233 |
. . 3
⊢ (𝜑 → 𝐵 ∈
ℕ0) |
173 | 4, 172 | reexpcld 13890 |
. 2
⊢ (𝜑 → (2↑𝐵) ∈ ℝ) |
174 | 2, 7 | elrpd 12778 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
175 | 16, 8 | readdcld 11013 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 logb 𝑁)↑5) + 1) ∈
ℝ) |
176 | 15 | nn0zd 12433 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 5 ∈
ℤ) |
177 | | logb1 25928 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 1) =
0) |
178 | 46, 47, 12, 177 | syl3anc 1370 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 logb 1) =
0) |
179 | 178, 24 | eqeltrd 2840 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 logb 1)
∈ ℝ) |
180 | 24 | leidd 11550 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ≤ 0) |
181 | 178 | eqcomd 2745 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 = (2 logb
1)) |
182 | 180, 181 | breqtrd 5101 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤ (2 logb
1)) |
183 | 8, 157, 2, 161, 29 | ltletrd 11144 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 < 𝑁) |
184 | | 1rp 12743 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ+ |
185 | 184 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℝ+) |
186 | | logblt 25943 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ (ℤ≥‘2) ∧ 1 ∈ ℝ+
∧ 𝑁 ∈
ℝ+) → (1 < 𝑁 ↔ (2 logb 1) < (2
logb 𝑁))) |
187 | 71, 185, 174, 186 | syl3anc 1370 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 < 𝑁 ↔ (2 logb 1) < (2
logb 𝑁))) |
188 | 183, 187 | mpbid 231 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 logb 1) <
(2 logb 𝑁)) |
189 | 24, 179, 13, 182, 188 | lelttrd 11142 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < (2 logb
𝑁)) |
190 | 13, 176, 189 | 3jca 1127 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 logb 𝑁) ∈ ℝ ∧ 5 ∈
ℤ ∧ 0 < (2 logb 𝑁))) |
191 | | expgt0 13825 |
. . . . . . . . . . . 12
⊢ (((2
logb 𝑁) ∈
ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 logb 𝑁)) → 0 < ((2
logb 𝑁)↑5)) |
192 | 190, 191 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < ((2 logb
𝑁)↑5)) |
193 | | ltp1 11824 |
. . . . . . . . . . . 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 11145 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < (((2
logb 𝑁)↑5)
+ 1)) |
196 | 4, 6, 175, 195, 12 | relogbcld 39988 |
. . . . . . . . 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 2824 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 ∈ ℝ ↔ (2 logb
(((2 logb 𝑁)↑5) + 1)) ∈
ℝ)) |
200 | 196, 199 | mpbird 256 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℝ) |
201 | 13 | resqcld 13974 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 logb 𝑁)↑2) ∈
ℝ) |
202 | | aks4d1p1p4.6 |
. . . . . . . . . . . 12
⊢ 𝐷 = ((2 logb 𝑁)↑2) |
203 | 202 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 = ((2 logb 𝑁)↑2)) |
204 | 203 | eleq1d 2824 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷 ∈ ℝ ↔ ((2 logb
𝑁)↑2) ∈
ℝ)) |
205 | 201, 204 | mpbird 256 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ ℝ) |
206 | 205 | rehalfcld 12229 |
. . . . . . . 8
⊢ (𝜑 → (𝐷 / 2) ∈ ℝ) |
207 | 200, 206 | readdcld 11013 |
. . . . . . 7
⊢ (𝜑 → (𝐶 + (𝐷 / 2)) ∈ ℝ) |
208 | 131, 4, 106 | redivcld 11812 |
. . . . . . 7
⊢ (𝜑 → (𝐸 / 2) ∈ ℝ) |
209 | 207, 208 | readdcld 11013 |
. . . . . 6
⊢ (𝜑 → ((𝐶 + (𝐷 / 2)) + (𝐸 / 2)) ∈ ℝ) |
210 | 174, 209 | rpcxpcld 25896 |
. . . . 5
⊢ (𝜑 → (𝑁↑𝑐((𝐶 + (𝐷 / 2)) + (𝐸 / 2))) ∈
ℝ+) |
211 | 210 | rpred 12781 |
. . . 4
⊢ (𝜑 → (𝑁↑𝑐((𝐶 + (𝐷 / 2)) + (𝐸 / 2))) ∈ ℝ) |
212 | 1, 98, 20, 29 | aks4d1p1p2 40085 |
. . . . 5
⊢ (𝜑 → 𝐴 < (𝑁↑𝑐(((2
logb (((2 logb 𝑁)↑5) + 1)) + (((2 logb 𝑁)↑2) / 2)) + (((2
logb 𝑁)↑4)
/ 2)))) |
213 | 126 | oveq1d 7299 |
. . . . . . . 8
⊢ (𝜑 → (((2 logb 𝑁)↑4) / 2) = (𝐸 / 2)) |
214 | 213 | oveq2d 7300 |
. . . . . . 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 2745 |
. . . . . . . . . 10
⊢ (𝜑 → (2 logb (((2
logb 𝑁)↑5)
+ 1)) = 𝐶) |
216 | 215 | oveq1d 7299 |
. . . . . . . . 9
⊢ (𝜑 → ((2 logb (((2
logb 𝑁)↑5)
+ 1)) + (((2 logb 𝑁)↑2) / 2)) = (𝐶 + (((2 logb 𝑁)↑2) / 2))) |
217 | 203 | eqcomd 2745 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 logb 𝑁)↑2) = 𝐷) |
218 | 217 | oveq1d 7299 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 logb 𝑁)↑2) / 2) = (𝐷 / 2)) |
219 | 218 | oveq2d 7300 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 + (((2 logb 𝑁)↑2) / 2)) = (𝐶 + (𝐷 / 2))) |
220 | 216, 219 | eqtrd 2779 |
. . . . . . . 8
⊢ (𝜑 → ((2 logb (((2
logb 𝑁)↑5)
+ 1)) + (((2 logb 𝑁)↑2) / 2)) = (𝐶 + (𝐷 / 2))) |
221 | 220 | oveq1d 7299 |
. . . . . . 7
⊢ (𝜑 → (((2 logb (((2
logb 𝑁)↑5)
+ 1)) + (((2 logb 𝑁)↑2) / 2)) + (𝐸 / 2)) = ((𝐶 + (𝐷 / 2)) + (𝐸 / 2))) |
222 | 214, 221 | eqtrd 2779 |
. . . . . 6
⊢ (𝜑 → (((2 logb (((2
logb 𝑁)↑5)
+ 1)) + (((2 logb 𝑁)↑2) / 2)) + (((2 logb 𝑁)↑4) / 2)) = ((𝐶 + (𝐷 / 2)) + (𝐸 / 2))) |
223 | 222 | oveq2d 7300 |
. . . . 5
⊢ (𝜑 → (𝑁↑𝑐(((2
logb (((2 logb 𝑁)↑5) + 1)) + (((2 logb 𝑁)↑2) / 2)) + (((2
logb 𝑁)↑4)
/ 2))) = (𝑁↑𝑐((𝐶 + (𝐷 / 2)) + (𝐸 / 2)))) |
224 | 212, 223 | breqtrd 5101 |
. . . 4
⊢ (𝜑 → 𝐴 < (𝑁↑𝑐((𝐶 + (𝐷 / 2)) + (𝐸 / 2)))) |
225 | 200 | recnd 11012 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ ℂ) |
226 | 225, 105,
106 | divcan3d 11765 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 · 𝐶) / 2) = 𝐶) |
227 | 226 | eqcomd 2745 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 = ((2 · 𝐶) / 2)) |
228 | 227 | oveq1d 7299 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 + (𝐷 / 2)) = (((2 · 𝐶) / 2) + (𝐷 / 2))) |
229 | 4, 200 | remulcld 11014 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 · 𝐶) ∈
ℝ) |
230 | 229 | recnd 11012 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · 𝐶) ∈
ℂ) |
231 | 205 | recnd 11012 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ ℂ) |
232 | 230, 231,
46, 106 | divdird 11798 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 · 𝐶) + 𝐷) / 2) = (((2 · 𝐶) / 2) + (𝐷 / 2))) |
233 | 232 | eqcomd 2745 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝐶) / 2) + (𝐷 / 2)) = (((2 · 𝐶) + 𝐷) / 2)) |
234 | 228, 233 | eqtrd 2779 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 + (𝐷 / 2)) = (((2 · 𝐶) + 𝐷) / 2)) |
235 | | aks4d1p1p4.8 |
. . . . . . . . 9
⊢ (𝜑 → ((2 · 𝐶) + 𝐷) ≤ 𝐸) |
236 | 229, 205 | readdcld 11013 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 · 𝐶) + 𝐷) ∈ ℝ) |
237 | 236, 131,
73 | lediv1d 12827 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝐶) + 𝐷) ≤ 𝐸 ↔ (((2 · 𝐶) + 𝐷) / 2) ≤ (𝐸 / 2))) |
238 | 235, 237 | mpbid 231 |
. . . . . . . 8
⊢ (𝜑 → (((2 · 𝐶) + 𝐷) / 2) ≤ (𝐸 / 2)) |
239 | 234, 238 | eqbrtrd 5097 |
. . . . . . 7
⊢ (𝜑 → (𝐶 + (𝐷 / 2)) ≤ (𝐸 / 2)) |
240 | 207, 208,
208, 239 | leadd1dd 11598 |
. . . . . 6
⊢ (𝜑 → ((𝐶 + (𝐷 / 2)) + (𝐸 / 2)) ≤ ((𝐸 / 2) + (𝐸 / 2))) |
241 | 132 | 2halvesd 12228 |
. . . . . 6
⊢ (𝜑 → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸) |
242 | 240, 241 | breqtrd 5101 |
. . . . 5
⊢ (𝜑 → ((𝐶 + (𝐷 / 2)) + (𝐸 / 2)) ≤ 𝐸) |
243 | 2, 183, 209, 131 | cxpled 25884 |
. . . . 5
⊢ (𝜑 → (((𝐶 + (𝐷 / 2)) + (𝐸 / 2)) ≤ 𝐸 ↔ (𝑁↑𝑐((𝐶 + (𝐷 / 2)) + (𝐸 / 2))) ≤ (𝑁↑𝑐𝐸))) |
244 | 242, 243 | mpbid 231 |
. . . 4
⊢ (𝜑 → (𝑁↑𝑐((𝐶 + (𝐷 / 2)) + (𝐸 / 2))) ≤ (𝑁↑𝑐𝐸)) |
245 | 101, 211,
165, 224, 244 | ltletrd 11144 |
. . 3
⊢ (𝜑 → 𝐴 < (𝑁↑𝑐𝐸)) |
246 | 245, 155 | breqtrd 5101 |
. 2
⊢ (𝜑 → 𝐴 < (2↑𝑐((2
logb 𝑁)↑5))) |
247 | | 1le2 12191 |
. . . . 5
⊢ 1 ≤
2 |
248 | 247 | a1i 11 |
. . . 4
⊢ (𝜑 → 1 ≤ 2) |
249 | 172 | nn0red 12303 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℝ) |
250 | 21 | eqcomd 2745 |
. . . . 5
⊢ (𝜑 → (⌈‘((2
logb 𝑁)↑5))
= 𝐵) |
251 | 33, 250 | breqtrd 5101 |
. . . 4
⊢ (𝜑 → ((2 logb 𝑁)↑5) ≤ 𝐵) |
252 | 4, 248, 16, 249, 251 | cxplead 25885 |
. . 3
⊢ (𝜑 →
(2↑𝑐((2 logb 𝑁)↑5)) ≤
(2↑𝑐𝐵)) |
253 | | cxpexp 25832 |
. . . 4
⊢ ((2
∈ ℂ ∧ 𝐵
∈ ℕ0) → (2↑𝑐𝐵) = (2↑𝐵)) |
254 | 105, 172,
253 | syl2anc 584 |
. . 3
⊢ (𝜑 →
(2↑𝑐𝐵) = (2↑𝐵)) |
255 | 252, 254 | breqtrd 5101 |
. 2
⊢ (𝜑 →
(2↑𝑐((2 logb 𝑁)↑5)) ≤ (2↑𝐵)) |
256 | 101, 166,
173, 246, 255 | ltletrd 11144 |
1
⊢ (𝜑 → 𝐴 < (2↑𝐵)) |