Proof of Theorem aks4d1p1p2
Step | Hyp | Ref
| Expression |
1 | | aks4d1p1p2.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | 1 | nnred 11733 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℝ) |
3 | | 2re 11792 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
4 | 3 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℝ) |
5 | | 2pos 11821 |
. . . . . . . . . . . 12
⊢ 0 <
2 |
6 | 5 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < 2) |
7 | 1 | nngt0d 11767 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 < 𝑁) |
8 | | 1red 10722 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 ∈
ℝ) |
9 | | 1lt2 11889 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 <
2 |
10 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 < 2) |
11 | 8, 10 | ltned 10856 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ≠ 2) |
12 | 11 | necomd 2989 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 2 ≠ 1) |
13 | 4, 6, 2, 7, 12 | relogbcld 39622 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 logb 𝑁) ∈
ℝ) |
14 | | 5nn0 11998 |
. . . . . . . . . . . . . . . 16
⊢ 5 ∈
ℕ0 |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 5 ∈
ℕ0) |
16 | 13, 15 | reexpcld 13621 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 logb 𝑁)↑5) ∈
ℝ) |
17 | | ceilcl 13305 |
. . . . . . . . . . . . . 14
⊢ (((2
logb 𝑁)↑5)
∈ ℝ → (⌈‘((2 logb 𝑁)↑5)) ∈ ℤ) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (⌈‘((2
logb 𝑁)↑5))
∈ ℤ) |
19 | 18 | zred 12170 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⌈‘((2
logb 𝑁)↑5))
∈ ℝ) |
20 | | aks4d1p1p2.3 |
. . . . . . . . . . . . . 14
⊢ 𝐵 = (⌈‘((2
logb 𝑁)↑5)) |
21 | 20 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 = (⌈‘((2 logb 𝑁)↑5))) |
22 | 21 | eleq1d 2817 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 ∈ ℝ ↔ (⌈‘((2
logb 𝑁)↑5))
∈ ℝ)) |
23 | 19, 22 | mpbird 260 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) |
24 | | 0red 10724 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℝ) |
25 | 15 | nn0zd 12168 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 5 ∈
ℤ) |
26 | | 3re 11798 |
. . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℝ |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 3 ∈
ℝ) |
28 | | 1lt3 11891 |
. . . . . . . . . . . . . . . . 17
⊢ 1 <
3 |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 < 3) |
30 | | aks4d1p1p2.4 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 3 ≤ 𝑁) |
31 | 8, 27, 2, 29, 30 | ltletrd 10880 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 < 𝑁) |
32 | 2, 7 | elrpd 12513 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
33 | | 2rp 12479 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ+ |
34 | 33, 9 | pm3.2i 474 |
. . . . . . . . . . . . . . . . 17
⊢ (2 ∈
ℝ+ ∧ 1 < 2) |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 ∈
ℝ+ ∧ 1 < 2)) |
36 | | logbgt0b 25533 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℝ+
∧ (2 ∈ ℝ+ ∧ 1 < 2)) → (0 < (2
logb 𝑁) ↔ 1
< 𝑁)) |
37 | 32, 35, 36 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0 < (2 logb
𝑁) ↔ 1 < 𝑁)) |
38 | 31, 37 | mpbird 260 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < (2 logb
𝑁)) |
39 | | expgt0 13556 |
. . . . . . . . . . . . . 14
⊢ (((2
logb 𝑁) ∈
ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 logb 𝑁)) → 0 < ((2
logb 𝑁)↑5)) |
40 | 13, 25, 38, 39 | syl3anc 1372 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < ((2 logb
𝑁)↑5)) |
41 | | ceilge 13307 |
. . . . . . . . . . . . . 14
⊢ (((2
logb 𝑁)↑5)
∈ ℝ → ((2 logb 𝑁)↑5) ≤ (⌈‘((2
logb 𝑁)↑5))) |
42 | 16, 41 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 logb 𝑁)↑5) ≤
(⌈‘((2 logb 𝑁)↑5))) |
43 | 24, 16, 19, 40, 42 | ltletrd 10880 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < (⌈‘((2
logb 𝑁)↑5))) |
44 | 21 | breq2d 5042 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 < 𝐵 ↔ 0 < (⌈‘((2
logb 𝑁)↑5)))) |
45 | 43, 44 | mpbird 260 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < 𝐵) |
46 | 4, 6, 23, 45, 12 | relogbcld 39622 |
. . . . . . . . . 10
⊢ (𝜑 → (2 logb 𝐵) ∈
ℝ) |
47 | 46 | flcld 13261 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘(2
logb 𝐵)) ∈
ℤ) |
48 | | 7re 11811 |
. . . . . . . . . . . . . . . 16
⊢ 7 ∈
ℝ |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 7 ∈
ℝ) |
50 | | 1lt7 11909 |
. . . . . . . . . . . . . . . 16
⊢ 1 <
7 |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 < 7) |
52 | 2, 30 | 3lexlogpow5ineq3 39707 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 7 < ((2 logb
𝑁)↑5)) |
53 | 8, 49, 16, 51, 52 | lttrd 10881 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 < ((2 logb
𝑁)↑5)) |
54 | 8, 16, 19, 53, 42 | ltletrd 10880 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 < (⌈‘((2
logb 𝑁)↑5))) |
55 | 21 | breq2d 5042 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 < 𝐵 ↔ 1 < (⌈‘((2
logb 𝑁)↑5)))) |
56 | 54, 55 | mpbird 260 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 < 𝐵) |
57 | 23, 45 | elrpd 12513 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
58 | | logbgt0b 25533 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℝ+
∧ (2 ∈ ℝ+ ∧ 1 < 2)) → (0 < (2
logb 𝐵) ↔ 1
< 𝐵)) |
59 | 57, 35, 58 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 < (2 logb
𝐵) ↔ 1 < 𝐵)) |
60 | 56, 59 | mpbird 260 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < (2 logb
𝐵)) |
61 | 24, 46, 60 | ltled 10868 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ (2 logb
𝐵)) |
62 | | 0zd 12076 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℤ) |
63 | | flge 13268 |
. . . . . . . . . . 11
⊢ (((2
logb 𝐵) ∈
ℝ ∧ 0 ∈ ℤ) → (0 ≤ (2 logb 𝐵) ↔ 0 ≤
(⌊‘(2 logb 𝐵)))) |
64 | 46, 62, 63 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → (0 ≤ (2 logb
𝐵) ↔ 0 ≤
(⌊‘(2 logb 𝐵)))) |
65 | 61, 64 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (⌊‘(2
logb 𝐵))) |
66 | 47, 65 | jca 515 |
. . . . . . . 8
⊢ (𝜑 → ((⌊‘(2
logb 𝐵)) ∈
ℤ ∧ 0 ≤ (⌊‘(2 logb 𝐵)))) |
67 | | elnn0z 12077 |
. . . . . . . 8
⊢
((⌊‘(2 logb 𝐵)) ∈ ℕ0 ↔
((⌊‘(2 logb 𝐵)) ∈ ℤ ∧ 0 ≤
(⌊‘(2 logb 𝐵)))) |
68 | 66, 67 | sylibr 237 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(2
logb 𝐵)) ∈
ℕ0) |
69 | 2, 68 | reexpcld 13621 |
. . . . . 6
⊢ (𝜑 → (𝑁↑(⌊‘(2 logb
𝐵))) ∈
ℝ) |
70 | | fzfid 13434 |
. . . . . . 7
⊢ (𝜑 → (1...(⌊‘((2
logb 𝑁)↑2))) ∈ Fin) |
71 | 2 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑁 ∈ ℝ) |
72 | | elfznn 13029 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) → 𝑘 ∈ ℕ) |
73 | 72 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑘 ∈ ℕ) |
74 | | nnnn0 11985 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
75 | 73, 74 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑘 ∈ ℕ0) |
76 | 71, 75 | reexpcld 13621 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (𝑁↑𝑘) ∈ ℝ) |
77 | | 1red 10722 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 ∈
ℝ) |
78 | 76, 77 | resubcld 11148 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → ((𝑁↑𝑘) − 1) ∈ ℝ) |
79 | 70, 78 | fprodrecl 15401 |
. . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1) ∈ ℝ) |
80 | 69, 79 | remulcld 10751 |
. . . . 5
⊢ (𝜑 → ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) ∈
ℝ) |
81 | | aks4d1p1p2.2 |
. . . . . . 7
⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) |
82 | 81 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐴 = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1))) |
83 | 82 | eleq1d 2817 |
. . . . 5
⊢ (𝜑 → (𝐴 ∈ ℝ ↔ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) ∈
ℝ)) |
84 | 80, 83 | mpbird 260 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℝ) |
85 | 1 | nnnn0d 12038 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
86 | 85 | nn0ge0d 12041 |
. . . . 5
⊢ (𝜑 → 0 ≤ 𝑁) |
87 | 16, 8 | readdcld 10750 |
. . . . . . 7
⊢ (𝜑 → (((2 logb 𝑁)↑5) + 1) ∈
ℝ) |
88 | 16 | ltp1d 11650 |
. . . . . . . 8
⊢ (𝜑 → ((2 logb 𝑁)↑5) < (((2
logb 𝑁)↑5)
+ 1)) |
89 | 24, 16, 87, 40, 88 | lttrd 10881 |
. . . . . . 7
⊢ (𝜑 → 0 < (((2
logb 𝑁)↑5)
+ 1)) |
90 | 4, 6, 87, 89, 12 | relogbcld 39622 |
. . . . . 6
⊢ (𝜑 → (2 logb (((2
logb 𝑁)↑5)
+ 1)) ∈ ℝ) |
91 | 13 | resqcld 13705 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 logb 𝑁)↑2) ∈
ℝ) |
92 | 91 | flcld 13261 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌊‘((2
logb 𝑁)↑2))
∈ ℤ) |
93 | 92 | zred 12170 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⌊‘((2
logb 𝑁)↑2))
∈ ℝ) |
94 | | 0lt1 11242 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
95 | 94 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 1) |
96 | 4, 6, 4, 6, 12 | relogbcld 39622 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 logb 2)
∈ ℝ) |
97 | 96 | resqcld 13705 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 logb
2)↑2) ∈ ℝ) |
98 | | 2nn0 11995 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ0 |
99 | 98 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ∈
ℕ0) |
100 | 8 | leidd 11286 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ≤ 1) |
101 | 4 | recnd 10749 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 ∈
ℂ) |
102 | 24, 6 | gtned 10855 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 ≠ 0) |
103 | | logbid1 25508 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 2) =
1) |
104 | 101, 102,
12, 103 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 logb 2) =
1) |
105 | 104 | eqcomd 2744 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 = (2 logb
2)) |
106 | 100, 105 | breqtrd 5056 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ≤ (2 logb
2)) |
107 | 96, 99, 106 | expge1d 13623 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ≤ ((2 logb
2)↑2)) |
108 | 105 | eqcomd 2744 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 logb 2) =
1) |
109 | 108 | oveq1d 7187 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2 logb
2)↑2) = (1↑2)) |
110 | 99 | nn0zd 12168 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 ∈
ℤ) |
111 | | 1exp 13552 |
. . . . . . . . . . . . . . . . 17
⊢ (2 ∈
ℤ → (1↑2) = 1) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1↑2) =
1) |
113 | 109, 112 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2 logb
2)↑2) = 1) |
114 | 4 | leidd 11286 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 2 ≤ 2) |
115 | | 1nn0 11994 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℕ0 |
116 | 3, 115 | nn0addge1i 12026 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ≤ (2
+ 1) |
117 | | 2p1e3 11860 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2 + 1) =
3 |
118 | 116, 117 | breqtri 5055 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ≤
3 |
119 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 2 ≤ 3) |
120 | 4, 27, 2, 119, 30 | letrd 10877 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 2 ≤ 𝑁) |
121 | 110, 114,
4, 6, 2, 7,
120 | logblebd 39625 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 logb 2) ≤
(2 logb 𝑁)) |
122 | 8, 96, 13, 106, 121 | letrd 10877 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ≤ (2 logb
𝑁)) |
123 | 13, 99, 122 | expge1d 13623 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ≤ ((2 logb
𝑁)↑2)) |
124 | 113, 123 | eqbrtrd 5052 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 logb
2)↑2) ≤ ((2 logb 𝑁)↑2)) |
125 | | 1z 12095 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℤ |
126 | | zsqcl 13588 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 ∈
ℤ → (1↑2) ∈ ℤ) |
127 | 125, 126 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
(1↑2) ∈ ℤ |
128 | 127 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1↑2) ∈
ℤ) |
129 | 109 | eleq1d 2817 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((2 logb
2)↑2) ∈ ℤ ↔ (1↑2) ∈ ℤ)) |
130 | 128, 129 | mpbird 260 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2 logb
2)↑2) ∈ ℤ) |
131 | 91, 130 | jca 515 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2 logb 𝑁)↑2) ∈ ℝ ∧
((2 logb 2)↑2) ∈ ℤ)) |
132 | | flge 13268 |
. . . . . . . . . . . . . . 15
⊢ ((((2
logb 𝑁)↑2)
∈ ℝ ∧ ((2 logb 2)↑2) ∈ ℤ) → (((2
logb 2)↑2) ≤ ((2 logb 𝑁)↑2) ↔ ((2 logb
2)↑2) ≤ (⌊‘((2 logb 𝑁)↑2)))) |
133 | 131, 132 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((2 logb
2)↑2) ≤ ((2 logb 𝑁)↑2) ↔ ((2 logb
2)↑2) ≤ (⌊‘((2 logb 𝑁)↑2)))) |
134 | 124, 133 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 logb
2)↑2) ≤ (⌊‘((2 logb 𝑁)↑2))) |
135 | 8, 97, 93, 107, 134 | letrd 10877 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ≤ (⌊‘((2
logb 𝑁)↑2))) |
136 | 24, 8, 93, 95, 135 | ltletrd 10880 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < (⌊‘((2
logb 𝑁)↑2))) |
137 | 92, 136 | jca 515 |
. . . . . . . . . 10
⊢ (𝜑 → ((⌊‘((2
logb 𝑁)↑2))
∈ ℤ ∧ 0 < (⌊‘((2 logb 𝑁)↑2)))) |
138 | | elnnz 12074 |
. . . . . . . . . . . 12
⊢
((⌊‘((2 logb 𝑁)↑2)) ∈ ℕ ↔
((⌊‘((2 logb 𝑁)↑2)) ∈ ℤ ∧ 0 <
(⌊‘((2 logb 𝑁)↑2)))) |
139 | 138 | bicomi 227 |
. . . . . . . . . . 11
⊢
(((⌊‘((2 logb 𝑁)↑2)) ∈ ℤ ∧ 0 <
(⌊‘((2 logb 𝑁)↑2))) ↔ (⌊‘((2
logb 𝑁)↑2))
∈ ℕ) |
140 | 139 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (((⌊‘((2
logb 𝑁)↑2))
∈ ℤ ∧ 0 < (⌊‘((2 logb 𝑁)↑2))) ↔
(⌊‘((2 logb 𝑁)↑2)) ∈ ℕ)) |
141 | 137, 140 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘((2
logb 𝑁)↑2))
∈ ℕ) |
142 | 141 | nnnn0d 12038 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘((2
logb 𝑁)↑2))
∈ ℕ0) |
143 | | arisum 15310 |
. . . . . . . 8
⊢
((⌊‘((2 logb 𝑁)↑2)) ∈ ℕ0 →
Σ𝑘 ∈
(1...(⌊‘((2 logb 𝑁)↑2)))𝑘 = ((((⌊‘((2 logb
𝑁)↑2))↑2) +
(⌊‘((2 logb 𝑁)↑2))) / 2)) |
144 | 142, 143 | syl 17 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))𝑘 = ((((⌊‘((2 logb
𝑁)↑2))↑2) +
(⌊‘((2 logb 𝑁)↑2))) / 2)) |
145 | 73 | nnred 11733 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑘 ∈ ℝ) |
146 | 70, 145 | fsumrecl 15186 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))𝑘 ∈ ℝ) |
147 | 144, 146 | eqeltrrd 2834 |
. . . . . 6
⊢ (𝜑 → ((((⌊‘((2
logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) / 2) ∈
ℝ) |
148 | 90, 147 | readdcld 10750 |
. . . . 5
⊢ (𝜑 → ((2 logb (((2
logb 𝑁)↑5)
+ 1)) + ((((⌊‘((2 logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) / 2)) ∈
ℝ) |
149 | 2, 86, 148 | recxpcld 25468 |
. . . 4
⊢ (𝜑 → (𝑁↑𝑐((2
logb (((2 logb 𝑁)↑5) + 1)) + ((((⌊‘((2
logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) / 2))) ∈
ℝ) |
150 | | 4nn0 11997 |
. . . . . . . . . 10
⊢ 4 ∈
ℕ0 |
151 | 150 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 4 ∈
ℕ0) |
152 | 13, 151 | reexpcld 13621 |
. . . . . . . 8
⊢ (𝜑 → ((2 logb 𝑁)↑4) ∈
ℝ) |
153 | 152, 91 | readdcld 10750 |
. . . . . . 7
⊢ (𝜑 → (((2 logb 𝑁)↑4) + ((2 logb
𝑁)↑2)) ∈
ℝ) |
154 | 153 | rehalfcld 11965 |
. . . . . 6
⊢ (𝜑 → ((((2 logb
𝑁)↑4) + ((2
logb 𝑁)↑2))
/ 2) ∈ ℝ) |
155 | 90, 154 | readdcld 10750 |
. . . . 5
⊢ (𝜑 → ((2 logb (((2
logb 𝑁)↑5)
+ 1)) + ((((2 logb 𝑁)↑4) + ((2 logb 𝑁)↑2)) / 2)) ∈
ℝ) |
156 | 2, 86, 155 | recxpcld 25468 |
. . . 4
⊢ (𝜑 → (𝑁↑𝑐((2
logb (((2 logb 𝑁)↑5) + 1)) + ((((2 logb
𝑁)↑4) + ((2
logb 𝑁)↑2))
/ 2))) ∈ ℝ) |
157 | | reflcl 13259 |
. . . . . . . . . . 11
⊢ ((2
logb 𝐵) ∈
ℝ → (⌊‘(2 logb 𝐵)) ∈ ℝ) |
158 | 46, 157 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (⌊‘(2
logb 𝐵)) ∈
ℝ) |
159 | 2, 86, 158 | recxpcld 25468 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁↑𝑐(⌊‘(2
logb 𝐵))) ∈
ℝ) |
160 | 32, 146 | rpcxpcld 25477 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁↑𝑐Σ𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))𝑘) ∈
ℝ+) |
161 | 32, 141 | aks4d1p1p1 39712 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑐𝑘) = (𝑁↑𝑐Σ𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))𝑘)) |
162 | 161 | eleq1d 2817 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑐𝑘) ∈ ℝ+ ↔ (𝑁↑𝑐Σ𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))𝑘) ∈
ℝ+)) |
163 | 160, 162 | mpbird 260 |
. . . . . . . . . . 11
⊢ (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑐𝑘) ∈
ℝ+) |
164 | 163 | rpregt0d 12522 |
. . . . . . . . . 10
⊢ (𝜑 → (∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑐𝑘) ∈ ℝ ∧ 0 < ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑐𝑘))) |
165 | 164 | simpld 498 |
. . . . . . . . 9
⊢ (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑐𝑘) ∈ ℝ) |
166 | 159, 165 | remulcld 10751 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁↑𝑐(⌊‘(2
logb 𝐵)))
· ∏𝑘 ∈
(1...(⌊‘((2 logb 𝑁)↑2)))(𝑁↑𝑐𝑘)) ∈ ℝ) |
167 | 2, 86, 90 | recxpcld 25468 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁↑𝑐(2 logb
(((2 logb 𝑁)↑5) + 1))) ∈
ℝ) |
168 | 167, 165 | remulcld 10751 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁↑𝑐(2 logb
(((2 logb 𝑁)↑5) + 1))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑐𝑘)) ∈ ℝ) |
169 | 70, 76 | fprodrecl 15401 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑘) ∈ ℝ) |
170 | 2, 68, 86 | expge0d 13622 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ (𝑁↑(⌊‘(2 logb
𝐵)))) |
171 | | nfv 1921 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘𝜑 |
172 | | 0red 10724 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 0 ∈
ℝ) |
173 | 1 | nnge1d 11766 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ≤ 𝑁) |
174 | 173 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 ≤ 𝑁) |
175 | 71, 75, 174 | expge1d 13623 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 ≤ (𝑁↑𝑘)) |
176 | 76 | recnd 10749 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (𝑁↑𝑘) ∈ ℂ) |
177 | 176 | subid1d 11066 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → ((𝑁↑𝑘) − 0) = (𝑁↑𝑘)) |
178 | 177 | breq2d 5042 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (1 ≤ ((𝑁↑𝑘) − 0) ↔ 1 ≤ (𝑁↑𝑘))) |
179 | 175, 178 | mpbird 260 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 ≤ ((𝑁↑𝑘) − 0)) |
180 | 77, 76, 172, 179 | lesubd 11324 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 0 ≤ ((𝑁↑𝑘) − 1)) |
181 | 76 | lem1d 11653 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → ((𝑁↑𝑘) − 1) ≤ (𝑁↑𝑘)) |
182 | 171, 70, 78, 180, 76, 181 | fprodle 15444 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1) ≤ ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑘)) |
183 | 79, 169, 69, 170, 182 | lemul2ad 11660 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) ≤ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑘))) |
184 | 82 | breq1d 5040 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ≤ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑘)) ↔ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) ≤ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑘)))) |
185 | 183, 184 | mpbird 260 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ≤ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑘))) |
186 | 71 | recnd 10749 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑁 ∈ ℂ) |
187 | | cxpexp 25413 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑁↑𝑐𝑘) = (𝑁↑𝑘)) |
188 | 186, 75, 187 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (𝑁↑𝑐𝑘) = (𝑁↑𝑘)) |
189 | 188 | eqcomd 2744 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (𝑁↑𝑘) = (𝑁↑𝑐𝑘)) |
190 | 189 | prodeq2dv 15371 |
. . . . . . . . . . 11
⊢ (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑘) = ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑐𝑘)) |
191 | 190 | oveq2d 7188 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑘)) = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑐𝑘))) |
192 | 185, 191 | breqtrd 5056 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≤ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑐𝑘))) |
193 | 2 | recnd 10749 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) |
194 | | cxpexp 25413 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℂ ∧
(⌊‘(2 logb 𝐵)) ∈ ℕ0) → (𝑁↑𝑐(⌊‘(2
logb 𝐵))) =
(𝑁↑(⌊‘(2
logb 𝐵)))) |
195 | 193, 68, 194 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁↑𝑐(⌊‘(2
logb 𝐵))) =
(𝑁↑(⌊‘(2
logb 𝐵)))) |
196 | 195 | oveq1d 7187 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁↑𝑐(⌊‘(2
logb 𝐵)))
· ∏𝑘 ∈
(1...(⌊‘((2 logb 𝑁)↑2)))(𝑁↑𝑐𝑘)) = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑐𝑘))) |
197 | 196 | eqcomd 2744 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑐𝑘)) = ((𝑁↑𝑐(⌊‘(2
logb 𝐵)))
· ∏𝑘 ∈
(1...(⌊‘((2 logb 𝑁)↑2)))(𝑁↑𝑐𝑘))) |
198 | 192, 197 | breqtrd 5056 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ≤ ((𝑁↑𝑐(⌊‘(2
logb 𝐵)))
· ∏𝑘 ∈
(1...(⌊‘((2 logb 𝑁)↑2)))(𝑁↑𝑐𝑘))) |
199 | 159, 167,
164 | 3jca 1129 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁↑𝑐(⌊‘(2
logb 𝐵))) ∈
ℝ ∧ (𝑁↑𝑐(2 logb
(((2 logb 𝑁)↑5) + 1))) ∈ ℝ ∧
(∏𝑘 ∈
(1...(⌊‘((2 logb 𝑁)↑2)))(𝑁↑𝑐𝑘) ∈ ℝ ∧ 0 < ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑐𝑘)))) |
200 | 1, 20, 30 | aks4d1p1p3 39718 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁↑𝑐(⌊‘(2
logb 𝐵))) <
(𝑁↑𝑐(2 logb
(((2 logb 𝑁)↑5) + 1)))) |
201 | | ltmul1a 11569 |
. . . . . . . . 9
⊢ ((((𝑁↑𝑐(⌊‘(2
logb 𝐵))) ∈
ℝ ∧ (𝑁↑𝑐(2 logb
(((2 logb 𝑁)↑5) + 1))) ∈ ℝ ∧
(∏𝑘 ∈
(1...(⌊‘((2 logb 𝑁)↑2)))(𝑁↑𝑐𝑘) ∈ ℝ ∧ 0 < ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑐𝑘))) ∧ (𝑁↑𝑐(⌊‘(2
logb 𝐵))) <
(𝑁↑𝑐(2 logb
(((2 logb 𝑁)↑5) + 1)))) → ((𝑁↑𝑐(⌊‘(2
logb 𝐵)))
· ∏𝑘 ∈
(1...(⌊‘((2 logb 𝑁)↑2)))(𝑁↑𝑐𝑘)) < ((𝑁↑𝑐(2 logb
(((2 logb 𝑁)↑5) + 1))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑐𝑘))) |
202 | 199, 200,
201 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁↑𝑐(⌊‘(2
logb 𝐵)))
· ∏𝑘 ∈
(1...(⌊‘((2 logb 𝑁)↑2)))(𝑁↑𝑐𝑘)) < ((𝑁↑𝑐(2 logb
(((2 logb 𝑁)↑5) + 1))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑐𝑘))) |
203 | 84, 166, 168, 198, 202 | lelttrd 10878 |
. . . . . . 7
⊢ (𝜑 → 𝐴 < ((𝑁↑𝑐(2 logb
(((2 logb 𝑁)↑5) + 1))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑐𝑘))) |
204 | 161 | oveq2d 7188 |
. . . . . . 7
⊢ (𝜑 → ((𝑁↑𝑐(2 logb
(((2 logb 𝑁)↑5) + 1))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))(𝑁↑𝑐𝑘)) = ((𝑁↑𝑐(2 logb
(((2 logb 𝑁)↑5) + 1))) · (𝑁↑𝑐Σ𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))𝑘))) |
205 | 203, 204 | breqtrd 5056 |
. . . . . 6
⊢ (𝜑 → 𝐴 < ((𝑁↑𝑐(2 logb
(((2 logb 𝑁)↑5) + 1))) · (𝑁↑𝑐Σ𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))𝑘))) |
206 | 144 | oveq2d 7188 |
. . . . . . 7
⊢ (𝜑 → (𝑁↑𝑐Σ𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))𝑘) = (𝑁↑𝑐((((⌊‘((2
logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) /
2))) |
207 | 206 | oveq2d 7188 |
. . . . . 6
⊢ (𝜑 → ((𝑁↑𝑐(2 logb
(((2 logb 𝑁)↑5) + 1))) · (𝑁↑𝑐Σ𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))𝑘)) = ((𝑁↑𝑐(2 logb
(((2 logb 𝑁)↑5) + 1))) · (𝑁↑𝑐((((⌊‘((2
logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) /
2)))) |
208 | 205, 207 | breqtrd 5056 |
. . . . 5
⊢ (𝜑 → 𝐴 < ((𝑁↑𝑐(2 logb
(((2 logb 𝑁)↑5) + 1))) · (𝑁↑𝑐((((⌊‘((2
logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) /
2)))) |
209 | 24, 7 | gtned 10855 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ≠ 0) |
210 | 90 | recnd 10749 |
. . . . . . 7
⊢ (𝜑 → (2 logb (((2
logb 𝑁)↑5)
+ 1)) ∈ ℂ) |
211 | 141 | nncnd 11734 |
. . . . . . . . . 10
⊢ (𝜑 → (⌊‘((2
logb 𝑁)↑2))
∈ ℂ) |
212 | 211 | sqcld 13602 |
. . . . . . . . 9
⊢ (𝜑 → ((⌊‘((2
logb 𝑁)↑2))↑2) ∈
ℂ) |
213 | 212, 211 | addcld 10740 |
. . . . . . . 8
⊢ (𝜑 → (((⌊‘((2
logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) ∈ ℂ) |
214 | 213 | halfcld 11963 |
. . . . . . 7
⊢ (𝜑 → ((((⌊‘((2
logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) / 2) ∈
ℂ) |
215 | 193, 209,
210, 214 | cxpaddd 25462 |
. . . . . 6
⊢ (𝜑 → (𝑁↑𝑐((2
logb (((2 logb 𝑁)↑5) + 1)) + ((((⌊‘((2
logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) / 2))) = ((𝑁↑𝑐(2 logb
(((2 logb 𝑁)↑5) + 1))) · (𝑁↑𝑐((((⌊‘((2
logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) /
2)))) |
216 | 215 | eqcomd 2744 |
. . . . 5
⊢ (𝜑 → ((𝑁↑𝑐(2 logb
(((2 logb 𝑁)↑5) + 1))) · (𝑁↑𝑐((((⌊‘((2
logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) /
2))) = (𝑁↑𝑐((2 logb
(((2 logb 𝑁)↑5) + 1)) + ((((⌊‘((2
logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) /
2)))) |
217 | 208, 216 | breqtrd 5056 |
. . . 4
⊢ (𝜑 → 𝐴 < (𝑁↑𝑐((2
logb (((2 logb 𝑁)↑5) + 1)) + ((((⌊‘((2
logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) / 2)))) |
218 | | reflcl 13259 |
. . . . . . . . . 10
⊢ (((2
logb 𝑁)↑2)
∈ ℝ → (⌊‘((2 logb 𝑁)↑2)) ∈ ℝ) |
219 | 91, 218 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘((2
logb 𝑁)↑2))
∈ ℝ) |
220 | 219 | resqcld 13705 |
. . . . . . . 8
⊢ (𝜑 → ((⌊‘((2
logb 𝑁)↑2))↑2) ∈
ℝ) |
221 | 220, 219 | readdcld 10750 |
. . . . . . 7
⊢ (𝜑 → (((⌊‘((2
logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) ∈ ℝ) |
222 | 33 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 2 ∈
ℝ+) |
223 | 91, 99 | reexpcld 13621 |
. . . . . . . . 9
⊢ (𝜑 → (((2 logb 𝑁)↑2)↑2) ∈
ℝ) |
224 | | id 22 |
. . . . . . . . . 10
⊢ (𝜑 → 𝜑) |
225 | 142 | nn0ge0d 12041 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ (⌊‘((2
logb 𝑁)↑2))) |
226 | | flle 13262 |
. . . . . . . . . . . 12
⊢ (((2
logb 𝑁)↑2)
∈ ℝ → (⌊‘((2 logb 𝑁)↑2)) ≤ ((2 logb 𝑁)↑2)) |
227 | 91, 226 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌊‘((2
logb 𝑁)↑2))
≤ ((2 logb 𝑁)↑2)) |
228 | 219, 91, 99, 225, 227 | leexp1ad 39621 |
. . . . . . . . . 10
⊢ (𝜑 → ((⌊‘((2
logb 𝑁)↑2))↑2) ≤ (((2 logb
𝑁)↑2)↑2)) |
229 | 224, 228 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((⌊‘((2
logb 𝑁)↑2))↑2) ≤ (((2 logb
𝑁)↑2)↑2)) |
230 | 13 | recnd 10749 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 logb 𝑁) ∈
ℂ) |
231 | 230, 99, 99 | expmuld 13607 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 logb 𝑁)↑(2 · 2)) = (((2
logb 𝑁)↑2)↑2)) |
232 | 231 | eqcomd 2744 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 logb 𝑁)↑2)↑2) = ((2
logb 𝑁)↑(2
· 2))) |
233 | | 2t2e4 11882 |
. . . . . . . . . . . . 13
⊢ (2
· 2) = 4 |
234 | 233 | oveq2i 7183 |
. . . . . . . . . . . 12
⊢ ((2
logb 𝑁)↑(2
· 2)) = ((2 logb 𝑁)↑4) |
235 | 234 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 logb 𝑁)↑(2 · 2)) = ((2
logb 𝑁)↑4)) |
236 | 232, 235 | eqtrd 2773 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 logb 𝑁)↑2)↑2) = ((2
logb 𝑁)↑4)) |
237 | 223, 236 | eqled 10823 |
. . . . . . . . 9
⊢ (𝜑 → (((2 logb 𝑁)↑2)↑2) ≤ ((2
logb 𝑁)↑4)) |
238 | 220, 223,
152, 229, 237 | letrd 10877 |
. . . . . . . 8
⊢ (𝜑 → ((⌊‘((2
logb 𝑁)↑2))↑2) ≤ ((2 logb
𝑁)↑4)) |
239 | 220, 219,
152, 91, 238, 227 | le2addd 11339 |
. . . . . . 7
⊢ (𝜑 → (((⌊‘((2
logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) ≤ (((2 logb 𝑁)↑4) + ((2 logb
𝑁)↑2))) |
240 | 221, 153,
222, 239 | lediv1dd 12574 |
. . . . . 6
⊢ (𝜑 → ((((⌊‘((2
logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) / 2) ≤ ((((2 logb
𝑁)↑4) + ((2
logb 𝑁)↑2))
/ 2)) |
241 | 147, 154,
90, 240 | leadd2dd 11335 |
. . . . 5
⊢ (𝜑 → ((2 logb (((2
logb 𝑁)↑5)
+ 1)) + ((((⌊‘((2 logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) / 2)) ≤ ((2 logb
(((2 logb 𝑁)↑5) + 1)) + ((((2 logb
𝑁)↑4) + ((2
logb 𝑁)↑2))
/ 2))) |
242 | 2, 31, 148, 155 | cxpled 25465 |
. . . . 5
⊢ (𝜑 → (((2 logb (((2
logb 𝑁)↑5)
+ 1)) + ((((⌊‘((2 logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) / 2)) ≤ ((2 logb
(((2 logb 𝑁)↑5) + 1)) + ((((2 logb
𝑁)↑4) + ((2
logb 𝑁)↑2))
/ 2)) ↔ (𝑁↑𝑐((2
logb (((2 logb 𝑁)↑5) + 1)) + ((((⌊‘((2
logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) / 2))) ≤ (𝑁↑𝑐((2
logb (((2 logb 𝑁)↑5) + 1)) + ((((2 logb
𝑁)↑4) + ((2
logb 𝑁)↑2))
/ 2))))) |
243 | 241, 242 | mpbid 235 |
. . . 4
⊢ (𝜑 → (𝑁↑𝑐((2
logb (((2 logb 𝑁)↑5) + 1)) + ((((⌊‘((2
logb 𝑁)↑2))↑2) + (⌊‘((2
logb 𝑁)↑2))) / 2))) ≤ (𝑁↑𝑐((2
logb (((2 logb 𝑁)↑5) + 1)) + ((((2 logb
𝑁)↑4) + ((2
logb 𝑁)↑2))
/ 2)))) |
244 | 84, 149, 156, 217, 243 | ltletrd 10880 |
. . 3
⊢ (𝜑 → 𝐴 < (𝑁↑𝑐((2
logb (((2 logb 𝑁)↑5) + 1)) + ((((2 logb
𝑁)↑4) + ((2
logb 𝑁)↑2))
/ 2)))) |
245 | 152 | recnd 10749 |
. . . . . 6
⊢ (𝜑 → ((2 logb 𝑁)↑4) ∈
ℂ) |
246 | 91 | recnd 10749 |
. . . . . 6
⊢ (𝜑 → ((2 logb 𝑁)↑2) ∈
ℂ) |
247 | 245, 246,
101, 102 | divdird 11534 |
. . . . 5
⊢ (𝜑 → ((((2 logb
𝑁)↑4) + ((2
logb 𝑁)↑2))
/ 2) = ((((2 logb 𝑁)↑4) / 2) + (((2 logb 𝑁)↑2) /
2))) |
248 | 247 | oveq2d 7188 |
. . . 4
⊢ (𝜑 → ((2 logb (((2
logb 𝑁)↑5)
+ 1)) + ((((2 logb 𝑁)↑4) + ((2 logb 𝑁)↑2)) / 2)) = ((2
logb (((2 logb 𝑁)↑5) + 1)) + ((((2 logb
𝑁)↑4) / 2) + (((2
logb 𝑁)↑2)
/ 2)))) |
249 | 248 | oveq2d 7188 |
. . 3
⊢ (𝜑 → (𝑁↑𝑐((2
logb (((2 logb 𝑁)↑5) + 1)) + ((((2 logb
𝑁)↑4) + ((2
logb 𝑁)↑2))
/ 2))) = (𝑁↑𝑐((2
logb (((2 logb 𝑁)↑5) + 1)) + ((((2 logb
𝑁)↑4) / 2) + (((2
logb 𝑁)↑2)
/ 2))))) |
250 | 244, 249 | breqtrd 5056 |
. 2
⊢ (𝜑 → 𝐴 < (𝑁↑𝑐((2
logb (((2 logb 𝑁)↑5) + 1)) + ((((2 logb
𝑁)↑4) / 2) + (((2
logb 𝑁)↑2)
/ 2))))) |
251 | 245, 101,
102 | divcld 11496 |
. . . . . 6
⊢ (𝜑 → (((2 logb 𝑁)↑4) / 2) ∈
ℂ) |
252 | 246, 101,
102 | divcld 11496 |
. . . . . 6
⊢ (𝜑 → (((2 logb 𝑁)↑2) / 2) ∈
ℂ) |
253 | 251, 252 | addcomd 10922 |
. . . . 5
⊢ (𝜑 → ((((2 logb
𝑁)↑4) / 2) + (((2
logb 𝑁)↑2)
/ 2)) = ((((2 logb 𝑁)↑2) / 2) + (((2 logb 𝑁)↑4) /
2))) |
254 | 253 | oveq2d 7188 |
. . . 4
⊢ (𝜑 → ((2 logb (((2
logb 𝑁)↑5)
+ 1)) + ((((2 logb 𝑁)↑4) / 2) + (((2 logb 𝑁)↑2) / 2))) = ((2
logb (((2 logb 𝑁)↑5) + 1)) + ((((2 logb
𝑁)↑2) / 2) + (((2
logb 𝑁)↑4)
/ 2)))) |
255 | 210, 252,
251 | addassd 10743 |
. . . . 5
⊢ (𝜑 → (((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
logb 𝑁)↑4)
/ 2)))) |
256 | 255 | eqcomd 2744 |
. . . 4
⊢ (𝜑 → ((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
logb 𝑁)↑4)
/ 2))) |
257 | 254, 256 | eqtrd 2773 |
. . 3
⊢ (𝜑 → ((2 logb (((2
logb 𝑁)↑5)
+ 1)) + ((((2 logb 𝑁)↑4) / 2) + (((2 logb 𝑁)↑2) / 2))) = (((2
logb (((2 logb 𝑁)↑5) + 1)) + (((2 logb 𝑁)↑2) / 2)) + (((2
logb 𝑁)↑4)
/ 2))) |
258 | 257 | oveq2d 7188 |
. 2
⊢ (𝜑 → (𝑁↑𝑐((2
logb (((2 logb 𝑁)↑5) + 1)) + ((((2 logb
𝑁)↑4) / 2) + (((2
logb 𝑁)↑2)
/ 2)))) = (𝑁↑𝑐(((2
logb (((2 logb 𝑁)↑5) + 1)) + (((2 logb 𝑁)↑2) / 2)) + (((2
logb 𝑁)↑4)
/ 2)))) |
259 | 250, 258 | breqtrd 5056 |
1
⊢ (𝜑 → 𝐴 < (𝑁↑𝑐(((2
logb (((2 logb 𝑁)↑5) + 1)) + (((2 logb 𝑁)↑2) / 2)) + (((2
logb 𝑁)↑4)
/ 2)))) |