Proof of Theorem aks4d1p1
Step | Hyp | Ref
| Expression |
1 | | 3nn 11795 |
. . . . . 6
⊢ 3 ∈
ℕ |
2 | 1 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 3 < 𝑁) → 3 ∈ ℕ) |
3 | | aks4d1p1.1 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘3)) |
4 | 3 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 3 < 𝑁) → 𝑁 ∈
(ℤ≥‘3)) |
5 | | eluznn 12400 |
. . . . 5
⊢ ((3
∈ ℕ ∧ 𝑁
∈ (ℤ≥‘3)) → 𝑁 ∈ ℕ) |
6 | 2, 4, 5 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ 3 < 𝑁) → 𝑁 ∈ ℕ) |
7 | | aks4d1p1.2 |
. . . 4
⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) |
8 | | aks4d1p1.3 |
. . . 4
⊢ 𝐵 = (⌈‘((2
logb 𝑁)↑5)) |
9 | | 3p1e4 11861 |
. . . . 5
⊢ (3 + 1) =
4 |
10 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 3 < 𝑁) → 3 < 𝑁) |
11 | | 3z 12096 |
. . . . . . . 8
⊢ 3 ∈
ℤ |
12 | 11 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 3 < 𝑁) → 3 ∈ ℤ) |
13 | | eluzelz 12334 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℤ) |
14 | 3, 13 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℤ) |
15 | 14 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 3 < 𝑁) → 𝑁 ∈ ℤ) |
16 | 12, 15 | zltp1led 39608 |
. . . . . 6
⊢ ((𝜑 ∧ 3 < 𝑁) → (3 < 𝑁 ↔ (3 + 1) ≤ 𝑁)) |
17 | 10, 16 | mpbid 235 |
. . . . 5
⊢ ((𝜑 ∧ 3 < 𝑁) → (3 + 1) ≤ 𝑁) |
18 | 9, 17 | eqbrtrrid 5066 |
. . . 4
⊢ ((𝜑 ∧ 3 < 𝑁) → 4 ≤ 𝑁) |
19 | | eqid 2738 |
. . . 4
⊢ (2
logb (((2 logb 𝑁)↑5) + 1)) = (2 logb (((2
logb 𝑁)↑5)
+ 1)) |
20 | | eqid 2738 |
. . . 4
⊢ ((2
logb 𝑁)↑2)
= ((2 logb 𝑁)↑2) |
21 | | eqid 2738 |
. . . 4
⊢ ((2
logb 𝑁)↑4)
= ((2 logb 𝑁)↑4) |
22 | 6, 7, 8, 18, 19, 20, 21 | aks4d1p1p5 39702 |
. . 3
⊢ ((𝜑 ∧ 3 < 𝑁) → 𝐴 < (2↑𝐵)) |
23 | 22 | ex 416 |
. 2
⊢ (𝜑 → (3 < 𝑁 → 𝐴 < (2↑𝐵))) |
24 | | simp2 1138 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 3 = 𝑁 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 3)↑2)))) → 3 = 𝑁) |
25 | 24 | eqcomd 2744 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 3 = 𝑁 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 3)↑2)))) → 𝑁 = 3) |
26 | 25 | oveq1d 7185 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 3 = 𝑁 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 3)↑2)))) → (𝑁↑𝑘) = (3↑𝑘)) |
27 | 26 | oveq1d 7185 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 3 = 𝑁 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 3)↑2)))) → ((𝑁↑𝑘) − 1) = ((3↑𝑘) − 1)) |
28 | 27 | 3expa 1119 |
. . . . . . . 8
⊢ (((𝜑 ∧ 3 = 𝑁) ∧ 𝑘 ∈ (1...(⌊‘((2
logb 3)↑2)))) → ((𝑁↑𝑘) − 1) = ((3↑𝑘) − 1)) |
29 | 28 | prodeq2dv 15369 |
. . . . . . 7
⊢ ((𝜑 ∧ 3 = 𝑁) → ∏𝑘 ∈ (1...(⌊‘((2
logb 3)↑2)))((𝑁↑𝑘) − 1) = ∏𝑘 ∈ (1...(⌊‘((2
logb 3)↑2)))((3↑𝑘) − 1)) |
30 | 29 | oveq2d 7186 |
. . . . . 6
⊢ ((𝜑 ∧ 3 = 𝑁) → ((3↑(⌊‘(2
logb (⌈‘((2 logb 3)↑5))))) ·
∏𝑘 ∈
(1...(⌊‘((2 logb 3)↑2)))((𝑁↑𝑘) − 1)) = ((3↑(⌊‘(2
logb (⌈‘((2 logb 3)↑5))))) ·
∏𝑘 ∈
(1...(⌊‘((2 logb 3)↑2)))((3↑𝑘) − 1))) |
31 | | 2rp 12477 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ+ |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 2 ∈
ℝ+) |
33 | | 1red 10720 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 ∈
ℝ) |
34 | | 1lt2 11887 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 <
2 |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 < 2) |
36 | 33, 35 | ltned 10854 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ≠ 2) |
37 | 36 | necomd 2989 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 2 ≠ 1) |
38 | 11 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 3 ∈
ℤ) |
39 | 32, 37, 38 | relogbexpd 39601 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 logb
(2↑3)) = 3) |
40 | 39 | eqcomd 2744 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 3 = (2 logb
(2↑3))) |
41 | | cu2 13655 |
. . . . . . . . . . . . . . . 16
⊢
(2↑3) = 8 |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2↑3) =
8) |
43 | 42 | oveq2d 7186 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 logb
(2↑3)) = (2 logb 8)) |
44 | 40, 43 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 3 = (2 logb
8)) |
45 | | 2z 12095 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ∈
ℤ) |
47 | 46 | zred 12168 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
ℝ) |
48 | 47 | leidd 11284 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ≤ 2) |
49 | | 8re 11812 |
. . . . . . . . . . . . . . 15
⊢ 8 ∈
ℝ |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 8 ∈
ℝ) |
51 | | 8pos 11828 |
. . . . . . . . . . . . . . 15
⊢ 0 <
8 |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 8) |
53 | 32 | rpgt0d 12517 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 0 < 2) |
54 | | 3re 11796 |
. . . . . . . . . . . . . . . . . . 19
⊢ 3 ∈
ℝ |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 3 ∈
ℝ) |
56 | 1 | nngt0i 11755 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 <
3 |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 0 < 3) |
58 | 47, 53, 55, 57, 37 | relogbcld 39600 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 logb 3)
∈ ℝ) |
59 | | 5nn0 11996 |
. . . . . . . . . . . . . . . . . 18
⊢ 5 ∈
ℕ0 |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 5 ∈
ℕ0) |
61 | 58, 60 | reexpcld 13619 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2 logb
3)↑5) ∈ ℝ) |
62 | | ceilcl 13303 |
. . . . . . . . . . . . . . . 16
⊢ (((2
logb 3)↑5) ∈ ℝ → (⌈‘((2
logb 3)↑5)) ∈ ℤ) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (⌈‘((2
logb 3)↑5)) ∈ ℤ) |
64 | 63 | zred 12168 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (⌈‘((2
logb 3)↑5)) ∈ ℝ) |
65 | | 0red 10722 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ∈
ℝ) |
66 | | 9re 11815 |
. . . . . . . . . . . . . . . . 17
⊢ 9 ∈
ℝ |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 9 ∈
ℝ) |
68 | 50 | lep1d 11649 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 8 ≤ (8 +
1)) |
69 | | 8p1e9 11866 |
. . . . . . . . . . . . . . . . . 18
⊢ (8 + 1) =
9 |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (8 + 1) =
9) |
71 | 68, 70 | breqtrd 5056 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 8 ≤ 9) |
72 | | 2re 11790 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 2 ∈
ℝ) |
74 | | 2pos 11819 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 <
2 |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 < 2) |
76 | | 3pos 11821 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 <
3 |
77 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 < 3) |
78 | 73, 75, 55, 77, 37 | relogbcld 39600 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2 logb 3)
∈ ℝ) |
79 | 78, 60 | reexpcld 13619 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2 logb
3)↑5) ∈ ℝ) |
80 | 79, 62 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (⌈‘((2
logb 3)↑5)) ∈ ℤ) |
81 | 80 | zred 12168 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (⌈‘((2
logb 3)↑5)) ∈ ℝ) |
82 | 55 | leidd 11284 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 3 ≤ 3) |
83 | 55, 82 | 3lexlogpow5ineq4 39684 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 9 < ((2 logb
3)↑5)) |
84 | 67, 79, 83 | ltled 10866 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 9 ≤ ((2 logb
3)↑5)) |
85 | | ceilge 13305 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
logb 3)↑5) ∈ ℝ → ((2 logb 3)↑5)
≤ (⌈‘((2 logb 3)↑5))) |
86 | 79, 85 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2 logb
3)↑5) ≤ (⌈‘((2 logb
3)↑5))) |
87 | 67, 79, 81, 84, 86 | letrd 10875 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 9 ≤ (⌈‘((2
logb 3)↑5))) |
88 | 50, 67, 64, 71, 87 | letrd 10875 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 8 ≤ (⌈‘((2
logb 3)↑5))) |
89 | 65, 50, 64, 52, 88 | ltletrd 10878 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < (⌈‘((2
logb 3)↑5))) |
90 | 46, 48, 50, 52, 64, 89, 88 | logblebd 39603 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 logb 8) ≤
(2 logb (⌈‘((2 logb
3)↑5)))) |
91 | 44, 90 | eqbrtrd 5052 |
. . . . . . . . . . . 12
⊢ (𝜑 → 3 ≤ (2 logb
(⌈‘((2 logb 3)↑5)))) |
92 | 79, 33 | readdcld 10748 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((2 logb
3)↑5) + 1) ∈ ℝ) |
93 | | 1nn0 11992 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℕ0 |
94 | | 6nn 11805 |
. . . . . . . . . . . . . . . . . . 19
⊢ 6 ∈
ℕ |
95 | 93, 94 | decnncl 12199 |
. . . . . . . . . . . . . . . . . 18
⊢ ;16 ∈ ℕ |
96 | 95 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ;16 ∈ ℕ) |
97 | 96 | nnred 11731 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ;16 ∈ ℝ) |
98 | | ceilm1lt 13307 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
logb 3)↑5) ∈ ℝ → ((⌈‘((2
logb 3)↑5)) − 1) < ((2 logb
3)↑5)) |
99 | 79, 98 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((⌈‘((2
logb 3)↑5)) − 1) < ((2 logb
3)↑5)) |
100 | 81, 33, 79 | ltsubaddd 11314 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((⌈‘((2
logb 3)↑5)) − 1) < ((2 logb 3)↑5)
↔ (⌈‘((2 logb 3)↑5)) < (((2 logb
3)↑5) + 1))) |
101 | 99, 100 | mpbid 235 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (⌈‘((2
logb 3)↑5)) < (((2 logb 3)↑5) +
1)) |
102 | | 3lexlogpow5ineq5 39688 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
logb 3)↑5) ≤ ;15 |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2 logb
3)↑5) ≤ ;15) |
104 | | 5p1e6 11863 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (5 + 1) =
6 |
105 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ;15 = ;15 |
106 | 93, 59, 104, 105 | decsuc 12210 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (;15 + 1) = ;16 |
107 | 106 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (;15 + 1) = ;16) |
108 | 97 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ;16 ∈ ℂ) |
109 | | 1cnd 10714 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 ∈
ℂ) |
110 | | 5nn 11802 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 5 ∈
ℕ |
111 | 93, 110 | decnncl 12199 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ;15 ∈ ℕ |
112 | 111 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ;15 ∈ ℕ) |
113 | 112 | nncnd 11732 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ;15 ∈ ℂ) |
114 | 108, 109,
113 | subadd2d 11094 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((;16 − 1) = ;15 ↔ (;15 + 1) = ;16)) |
115 | 107, 114 | mpbird 260 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (;16 − 1) = ;15) |
116 | 115 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ;15 = (;16 − 1)) |
117 | 103, 116 | breqtrd 5056 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2 logb
3)↑5) ≤ (;16 −
1)) |
118 | | leaddsub 11194 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((2
logb 3)↑5) ∈ ℝ ∧ 1 ∈ ℝ ∧ ;16 ∈ ℝ) → ((((2
logb 3)↑5) + 1) ≤ ;16 ↔ ((2 logb 3)↑5) ≤ (;16 − 1))) |
119 | 79, 33, 97, 118 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((((2 logb
3)↑5) + 1) ≤ ;16 ↔
((2 logb 3)↑5) ≤ (;16 − 1))) |
120 | 117, 119 | mpbird 260 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((2 logb
3)↑5) + 1) ≤ ;16) |
121 | 81, 92, 97, 101, 120 | ltletrd 10878 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (⌈‘((2
logb 3)↑5)) < ;16) |
122 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢ ;16 = ;16 |
123 | | 2exp4 16521 |
. . . . . . . . . . . . . . . . 17
⊢
(2↑4) = ;16 |
124 | 122, 123 | eqtr4i 2764 |
. . . . . . . . . . . . . . . 16
⊢ ;16 = (2↑4) |
125 | 124 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ;16 = (2↑4)) |
126 | 121, 125 | breqtrd 5056 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (⌈‘((2
logb 3)↑5)) < (2↑4)) |
127 | 46 | uzidd 12340 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
(ℤ≥‘2)) |
128 | 64, 89 | elrpd 12511 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (⌈‘((2
logb 3)↑5)) ∈ ℝ+) |
129 | | 4z 12097 |
. . . . . . . . . . . . . . . . 17
⊢ 4 ∈
ℤ |
130 | 129 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 4 ∈
ℤ) |
131 | 32, 130 | rpexpcld 13700 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2↑4) ∈
ℝ+) |
132 | | logblt 25522 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ (ℤ≥‘2) ∧ (⌈‘((2
logb 3)↑5)) ∈ ℝ+ ∧ (2↑4) ∈
ℝ+) → ((⌈‘((2 logb 3)↑5))
< (2↑4) ↔ (2 logb (⌈‘((2 logb
3)↑5))) < (2 logb (2↑4)))) |
133 | 127, 128,
131, 132 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((⌈‘((2
logb 3)↑5)) < (2↑4) ↔ (2 logb
(⌈‘((2 logb 3)↑5))) < (2 logb
(2↑4)))) |
134 | 126, 133 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 logb
(⌈‘((2 logb 3)↑5))) < (2 logb
(2↑4))) |
135 | 32, 37, 130 | relogbexpd 39601 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 logb
(2↑4)) = 4) |
136 | 9 | eqcomi 2747 |
. . . . . . . . . . . . . . 15
⊢ 4 = (3 +
1) |
137 | 136 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 4 = (3 +
1)) |
138 | 135, 137 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 logb
(2↑4)) = (3 + 1)) |
139 | 134, 138 | breqtrd 5056 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 logb
(⌈‘((2 logb 3)↑5))) < (3 + 1)) |
140 | 91, 139 | jca 515 |
. . . . . . . . . . 11
⊢ (𝜑 → (3 ≤ (2 logb
(⌈‘((2 logb 3)↑5))) ∧ (2 logb
(⌈‘((2 logb 3)↑5))) < (3 + 1))) |
141 | 73, 75, 55, 57, 37 | relogbcld 39600 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 logb 3)
∈ ℝ) |
142 | 141, 60 | reexpcld 13619 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2 logb
3)↑5) ∈ ℝ) |
143 | 142, 62 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (⌈‘((2
logb 3)↑5)) ∈ ℤ) |
144 | 143 | zred 12168 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (⌈‘((2
logb 3)↑5)) ∈ ℝ) |
145 | | 9pos 11829 |
. . . . . . . . . . . . . . 15
⊢ 0 <
9 |
146 | 145 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 9) |
147 | 65, 67, 144, 146, 87 | ltletrd 10878 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < (⌈‘((2
logb 3)↑5))) |
148 | 73, 75, 144, 147, 37 | relogbcld 39600 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 logb
(⌈‘((2 logb 3)↑5))) ∈
ℝ) |
149 | | flbi 13277 |
. . . . . . . . . . . 12
⊢ (((2
logb (⌈‘((2 logb 3)↑5))) ∈ ℝ
∧ 3 ∈ ℤ) → ((⌊‘(2 logb
(⌈‘((2 logb 3)↑5)))) = 3 ↔ (3 ≤ (2
logb (⌈‘((2 logb 3)↑5))) ∧ (2
logb (⌈‘((2 logb 3)↑5))) < (3 +
1)))) |
150 | 148, 38, 149 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → ((⌊‘(2
logb (⌈‘((2 logb 3)↑5)))) = 3 ↔ (3
≤ (2 logb (⌈‘((2 logb 3)↑5))) ∧
(2 logb (⌈‘((2 logb 3)↑5))) < (3 +
1)))) |
151 | 140, 150 | mpbird 260 |
. . . . . . . . . 10
⊢ (𝜑 → (⌊‘(2
logb (⌈‘((2 logb 3)↑5)))) =
3) |
152 | 151 | oveq2d 7186 |
. . . . . . . . 9
⊢ (𝜑 → (3↑(⌊‘(2
logb (⌈‘((2 logb 3)↑5))))) =
(3↑3)) |
153 | 78 | resqcld 13703 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2 logb
3)↑2) ∈ ℝ) |
154 | | 3lexlogpow2ineq2 39687 |
. . . . . . . . . . . . . . . . 17
⊢ (2 <
((2 logb 3)↑2) ∧ ((2 logb 3)↑2) <
3) |
155 | 154 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 < ((2
logb 3)↑2) ∧ ((2 logb 3)↑2) <
3)) |
156 | 155 | simpld 498 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 < ((2 logb
3)↑2)) |
157 | 73, 153, 156 | ltled 10866 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ≤ ((2 logb
3)↑2)) |
158 | 155 | simprd 499 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2 logb
3)↑2) < 3) |
159 | | df-3 11780 |
. . . . . . . . . . . . . . . 16
⊢ 3 = (2 +
1) |
160 | 159 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 3 = (2 +
1)) |
161 | 158, 160 | breqtrd 5056 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 logb
3)↑2) < (2 + 1)) |
162 | 157, 161 | jca 515 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 ≤ ((2
logb 3)↑2) ∧ ((2 logb 3)↑2) < (2 +
1))) |
163 | 141 | resqcld 13703 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 logb
3)↑2) ∈ ℝ) |
164 | | flbi 13277 |
. . . . . . . . . . . . . 14
⊢ ((((2
logb 3)↑2) ∈ ℝ ∧ 2 ∈ ℤ) →
((⌊‘((2 logb 3)↑2)) = 2 ↔ (2 ≤ ((2
logb 3)↑2) ∧ ((2 logb 3)↑2) < (2 +
1)))) |
165 | 163, 46, 164 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((⌊‘((2
logb 3)↑2)) = 2 ↔ (2 ≤ ((2 logb 3)↑2)
∧ ((2 logb 3)↑2) < (2 + 1)))) |
166 | 162, 165 | mpbird 260 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⌊‘((2
logb 3)↑2)) = 2) |
167 | 166 | oveq2d 7186 |
. . . . . . . . . . 11
⊢ (𝜑 → (1...(⌊‘((2
logb 3)↑2))) = (1...2)) |
168 | 167 | prodeq1d 15367 |
. . . . . . . . . 10
⊢ (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2
logb 3)↑2)))((3↑𝑘) − 1) = ∏𝑘 ∈ (1...2)((3↑𝑘) − 1)) |
169 | | 1zzd 12094 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℤ) |
170 | 169, 46 | jca 515 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 ∈ ℤ ∧ 2
∈ ℤ)) |
171 | | 1le2 11925 |
. . . . . . . . . . . . . . 15
⊢ 1 ≤
2 |
172 | 171 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℤ ∧ 2 ∈ ℤ) → 1 ≤ 2) |
173 | | eluz 12338 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℤ ∧ 2 ∈ ℤ) → (2 ∈
(ℤ≥‘1) ↔ 1 ≤ 2)) |
174 | 172, 173 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℤ ∧ 2 ∈ ℤ) → 2 ∈
(ℤ≥‘1)) |
175 | 170, 174 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
(ℤ≥‘1)) |
176 | | 3cn 11797 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℂ |
177 | 176 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → 3 ∈
ℂ) |
178 | | elfznn 13027 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (1...2) → 𝑘 ∈
ℕ) |
179 | 178 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → 𝑘 ∈ ℕ) |
180 | 179 | nnnn0d 12036 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → 𝑘 ∈ ℕ0) |
181 | 177, 180 | expcld 13602 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → (3↑𝑘) ∈
ℂ) |
182 | | 1cnd 10714 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → 1 ∈
ℂ) |
183 | 181, 182 | subcld 11075 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → ((3↑𝑘) − 1) ∈
ℂ) |
184 | | oveq2 7178 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 2 → (3↑𝑘) = (3↑2)) |
185 | 184 | oveq1d 7185 |
. . . . . . . . . . . 12
⊢ (𝑘 = 2 → ((3↑𝑘) − 1) = ((3↑2)
− 1)) |
186 | 175, 183,
185 | fprodm1 15413 |
. . . . . . . . . . 11
⊢ (𝜑 → ∏𝑘 ∈ (1...2)((3↑𝑘) − 1) = (∏𝑘 ∈ (1...(2 − 1))((3↑𝑘) − 1) ·
((3↑2) − 1))) |
187 | | 2m1e1 11842 |
. . . . . . . . . . . . . . . 16
⊢ (2
− 1) = 1 |
188 | 187 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 − 1) =
1) |
189 | 188 | oveq2d 7186 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1...(2 − 1)) =
(1...1)) |
190 | 189 | prodeq1d 15367 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∏𝑘 ∈ (1...(2 − 1))((3↑𝑘) − 1) = ∏𝑘 ∈ (1...1)((3↑𝑘) − 1)) |
191 | 55 | recnd 10747 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 3 ∈
ℂ) |
192 | 93 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈
ℕ0) |
193 | 191, 192 | expcld 13602 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (3↑1) ∈
ℂ) |
194 | 193, 109 | subcld 11075 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((3↑1) − 1)
∈ ℂ) |
195 | 169, 194 | jca 515 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1 ∈ ℤ ∧
((3↑1) − 1) ∈ ℂ)) |
196 | | oveq2 7178 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 1 → (3↑𝑘) = (3↑1)) |
197 | 196 | oveq1d 7185 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 1 → ((3↑𝑘) − 1) = ((3↑1)
− 1)) |
198 | 197 | fprod1 15409 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℤ ∧ ((3↑1) − 1) ∈ ℂ) → ∏𝑘 ∈ (1...1)((3↑𝑘) − 1) = ((3↑1)
− 1)) |
199 | 195, 198 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∏𝑘 ∈ (1...1)((3↑𝑘) − 1) = ((3↑1) −
1)) |
200 | 190, 199 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∏𝑘 ∈ (1...(2 − 1))((3↑𝑘) − 1) = ((3↑1)
− 1)) |
201 | 200 | oveq1d 7185 |
. . . . . . . . . . 11
⊢ (𝜑 → (∏𝑘 ∈ (1...(2 − 1))((3↑𝑘) − 1) ·
((3↑2) − 1)) = (((3↑1) − 1) · ((3↑2) −
1))) |
202 | 186, 201 | eqtrd 2773 |
. . . . . . . . . 10
⊢ (𝜑 → ∏𝑘 ∈ (1...2)((3↑𝑘) − 1) = (((3↑1) − 1)
· ((3↑2) − 1))) |
203 | 168, 202 | eqtrd 2773 |
. . . . . . . . 9
⊢ (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2
logb 3)↑2)))((3↑𝑘) − 1) = (((3↑1) − 1)
· ((3↑2) − 1))) |
204 | 152, 203 | oveq12d 7188 |
. . . . . . . 8
⊢ (𝜑 → ((3↑(⌊‘(2
logb (⌈‘((2 logb 3)↑5))))) ·
∏𝑘 ∈
(1...(⌊‘((2 logb 3)↑2)))((3↑𝑘) − 1)) = ((3↑3) ·
(((3↑1) − 1) · ((3↑2) − 1)))) |
205 | | 3nn0 11994 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℕ0 |
206 | 205 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 3 ∈
ℕ0) |
207 | 55, 206 | reexpcld 13619 |
. . . . . . . . . 10
⊢ (𝜑 → (3↑3) ∈
ℝ) |
208 | 55, 192 | reexpcld 13619 |
. . . . . . . . . . . 12
⊢ (𝜑 → (3↑1) ∈
ℝ) |
209 | 208, 33 | resubcld 11146 |
. . . . . . . . . . 11
⊢ (𝜑 → ((3↑1) − 1)
∈ ℝ) |
210 | 55 | resqcld 13703 |
. . . . . . . . . . . 12
⊢ (𝜑 → (3↑2) ∈
ℝ) |
211 | 210, 33 | resubcld 11146 |
. . . . . . . . . . 11
⊢ (𝜑 → ((3↑2) − 1)
∈ ℝ) |
212 | 209, 211 | remulcld 10749 |
. . . . . . . . . 10
⊢ (𝜑 → (((3↑1) − 1)
· ((3↑2) − 1)) ∈ ℝ) |
213 | 207, 212 | remulcld 10749 |
. . . . . . . . 9
⊢ (𝜑 → ((3↑3) ·
(((3↑1) − 1) · ((3↑2) − 1))) ∈
ℝ) |
214 | | 9nn0 12000 |
. . . . . . . . . . . 12
⊢ 9 ∈
ℕ0 |
215 | 214 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 9 ∈
ℕ0) |
216 | 73, 215 | reexpcld 13619 |
. . . . . . . . . 10
⊢ (𝜑 → (2↑9) ∈
ℝ) |
217 | 216, 33 | resubcld 11146 |
. . . . . . . . 9
⊢ (𝜑 → ((2↑9) − 1)
∈ ℝ) |
218 | | elnnz 12072 |
. . . . . . . . . . . . 13
⊢
((⌈‘((2 logb 3)↑5)) ∈ ℕ ↔
((⌈‘((2 logb 3)↑5)) ∈ ℤ ∧ 0 <
(⌈‘((2 logb 3)↑5)))) |
219 | 143, 147,
218 | sylanbrc 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⌈‘((2
logb 3)↑5)) ∈ ℕ) |
220 | 219 | orcd 872 |
. . . . . . . . . . 11
⊢ (𝜑 → ((⌈‘((2
logb 3)↑5)) ∈ ℕ ∨ (⌈‘((2
logb 3)↑5)) = 0)) |
221 | | elnn0 11978 |
. . . . . . . . . . . 12
⊢
((⌈‘((2 logb 3)↑5)) ∈
ℕ0 ↔ ((⌈‘((2 logb 3)↑5))
∈ ℕ ∨ (⌈‘((2 logb 3)↑5)) =
0)) |
222 | 221 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ((⌈‘((2
logb 3)↑5)) ∈ ℕ0 ↔
((⌈‘((2 logb 3)↑5)) ∈ ℕ ∨
(⌈‘((2 logb 3)↑5)) = 0))) |
223 | 220, 222 | mpbird 260 |
. . . . . . . . . 10
⊢ (𝜑 → (⌈‘((2
logb 3)↑5)) ∈ ℕ0) |
224 | 73, 223 | reexpcld 13619 |
. . . . . . . . 9
⊢ (𝜑 → (2↑(⌈‘((2
logb 3)↑5))) ∈ ℝ) |
225 | | 8cn 11813 |
. . . . . . . . . . . . . . 15
⊢ 8 ∈
ℂ |
226 | | 2cn 11791 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
227 | | 8t2e16 12294 |
. . . . . . . . . . . . . . 15
⊢ (8
· 2) = ;16 |
228 | 225, 226,
227 | mulcomli 10728 |
. . . . . . . . . . . . . 14
⊢ (2
· 8) = ;16 |
229 | 228 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · 8) = ;16) |
230 | 229 | oveq2d 7186 |
. . . . . . . . . . . 12
⊢ (𝜑 → (;27 · (2 · 8)) = (;27 · ;16)) |
231 | | 6nn0 11997 |
. . . . . . . . . . . . . . 15
⊢ 6 ∈
ℕ0 |
232 | 93, 231 | deccl 12194 |
. . . . . . . . . . . . . 14
⊢ ;16 ∈
ℕ0 |
233 | | 2nn0 11993 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ0 |
234 | | 7nn0 11998 |
. . . . . . . . . . . . . 14
⊢ 7 ∈
ℕ0 |
235 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ ;27 = ;27 |
236 | 93, 93 | deccl 12194 |
. . . . . . . . . . . . . 14
⊢ ;11 ∈
ℕ0 |
237 | | 0nn0 11991 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℕ0 |
238 | 233 | dec0h 12201 |
. . . . . . . . . . . . . . 15
⊢ 2 = ;02 |
239 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ ;11 = ;11 |
240 | 232 | nn0cni 11988 |
. . . . . . . . . . . . . . . . . 18
⊢ ;16 ∈ ℂ |
241 | 240 | mul02i 10907 |
. . . . . . . . . . . . . . . . 17
⊢ (0
· ;16) = 0 |
242 | | ax-1cn 10673 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℂ |
243 | 176, 242,
9 | addcomli 10910 |
. . . . . . . . . . . . . . . . 17
⊢ (1 + 3) =
4 |
244 | 241, 243 | oveq12i 7182 |
. . . . . . . . . . . . . . . 16
⊢ ((0
· ;16) + (1 + 3)) = (0 +
4) |
245 | | 4cn 11801 |
. . . . . . . . . . . . . . . . 17
⊢ 4 ∈
ℂ |
246 | 245 | addid2i 10906 |
. . . . . . . . . . . . . . . 16
⊢ (0 + 4) =
4 |
247 | 244, 246 | eqtri 2761 |
. . . . . . . . . . . . . . 15
⊢ ((0
· ;16) + (1 + 3)) =
4 |
248 | 93 | dec0h 12201 |
. . . . . . . . . . . . . . . 16
⊢ 1 = ;01 |
249 | | 2t1e2 11879 |
. . . . . . . . . . . . . . . . . 18
⊢ (2
· 1) = 2 |
250 | | 0p1e1 11838 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 + 1) =
1 |
251 | 249, 250 | oveq12i 7182 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
· 1) + (0 + 1)) = (2 + 1) |
252 | | 2p1e3 11858 |
. . . . . . . . . . . . . . . . 17
⊢ (2 + 1) =
3 |
253 | 251, 252 | eqtri 2761 |
. . . . . . . . . . . . . . . 16
⊢ ((2
· 1) + (0 + 1)) = 3 |
254 | | 6cn 11807 |
. . . . . . . . . . . . . . . . . 18
⊢ 6 ∈
ℂ |
255 | | 6t2e12 12283 |
. . . . . . . . . . . . . . . . . 18
⊢ (6
· 2) = ;12 |
256 | 254, 226,
255 | mulcomli 10728 |
. . . . . . . . . . . . . . . . 17
⊢ (2
· 6) = ;12 |
257 | 93, 233, 252, 256 | decsuc 12210 |
. . . . . . . . . . . . . . . 16
⊢ ((2
· 6) + 1) = ;13 |
258 | 93, 231, 237, 93, 122, 248, 233, 205, 93, 253, 257 | decma2c 12232 |
. . . . . . . . . . . . . . 15
⊢ ((2
· ;16) + 1) = ;33 |
259 | 237, 233,
93, 93, 238, 239, 232, 205, 205, 247, 258 | decmac 12231 |
. . . . . . . . . . . . . 14
⊢ ((2
· ;16) + ;11) = ;43 |
260 | | 4nn0 11995 |
. . . . . . . . . . . . . . 15
⊢ 4 ∈
ℕ0 |
261 | | 7cn 11810 |
. . . . . . . . . . . . . . . . . 18
⊢ 7 ∈
ℂ |
262 | 261 | mulid1i 10723 |
. . . . . . . . . . . . . . . . 17
⊢ (7
· 1) = 7 |
263 | 262 | oveq1i 7180 |
. . . . . . . . . . . . . . . 16
⊢ ((7
· 1) + 4) = (7 + 4) |
264 | | 7p4e11 12255 |
. . . . . . . . . . . . . . . 16
⊢ (7 + 4) =
;11 |
265 | 263, 264 | eqtri 2761 |
. . . . . . . . . . . . . . 15
⊢ ((7
· 1) + 4) = ;11 |
266 | | 7t6e42 12292 |
. . . . . . . . . . . . . . 15
⊢ (7
· 6) = ;42 |
267 | 234, 93, 231, 122, 233, 260, 265, 266 | decmul2c 12245 |
. . . . . . . . . . . . . 14
⊢ (7
· ;16) = ;;112 |
268 | 232, 233,
234, 235, 233, 236, 259, 267 | decmul1c 12244 |
. . . . . . . . . . . . 13
⊢ (;27 · ;16) = ;;432 |
269 | 268 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (;27 · ;16) = ;;432) |
270 | 230, 269 | eqtrd 2773 |
. . . . . . . . . . 11
⊢ (𝜑 → (;27 · (2 · 8)) = ;;432) |
271 | 260, 205 | deccl 12194 |
. . . . . . . . . . . . 13
⊢ ;43 ∈
ℕ0 |
272 | 59, 93 | deccl 12194 |
. . . . . . . . . . . . 13
⊢ ;51 ∈
ℕ0 |
273 | | 2lt10 12317 |
. . . . . . . . . . . . 13
⊢ 2 <
;10 |
274 | | 3lt10 12316 |
. . . . . . . . . . . . . 14
⊢ 3 <
;10 |
275 | | 4lt5 11893 |
. . . . . . . . . . . . . 14
⊢ 4 <
5 |
276 | 260, 59, 205, 93, 274, 275 | decltc 12208 |
. . . . . . . . . . . . 13
⊢ ;43 < ;51 |
277 | 271, 272,
233, 93, 273, 276 | decltc 12208 |
. . . . . . . . . . . 12
⊢ ;;432 < ;;511 |
278 | 277 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ;;432
< ;;511) |
279 | 270, 278 | eqbrtrd 5052 |
. . . . . . . . . 10
⊢ (𝜑 → (;27 · (2 · 8)) < ;;511) |
280 | | 3exp3 16528 |
. . . . . . . . . . . . 13
⊢
(3↑3) = ;27 |
281 | 280 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (3↑3) = ;27) |
282 | 281 | eqcomd 2744 |
. . . . . . . . . . 11
⊢ (𝜑 → ;27 = (3↑3)) |
283 | 191 | exp1d 13597 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (3↑1) =
3) |
284 | 283 | oveq1d 7185 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((3↑1) − 1) =
(3 − 1)) |
285 | | 3m1e2 11844 |
. . . . . . . . . . . . . 14
⊢ (3
− 1) = 2 |
286 | 285 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (3 − 1) =
2) |
287 | 284, 286 | eqtr2d 2774 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 = ((3↑1) −
1)) |
288 | | sq3 13653 |
. . . . . . . . . . . . . . 15
⊢
(3↑2) = 9 |
289 | 288 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (3↑2) =
9) |
290 | 289 | oveq1d 7185 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((3↑2) − 1) =
(9 − 1)) |
291 | | 9m1e8 11850 |
. . . . . . . . . . . . . 14
⊢ (9
− 1) = 8 |
292 | 291 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (9 − 1) =
8) |
293 | 290, 292 | eqtr2d 2774 |
. . . . . . . . . . . 12
⊢ (𝜑 → 8 = ((3↑2) −
1)) |
294 | 287, 293 | oveq12d 7188 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · 8) =
(((3↑1) − 1) · ((3↑2) − 1))) |
295 | 282, 294 | oveq12d 7188 |
. . . . . . . . . 10
⊢ (𝜑 → (;27 · (2 · 8)) = ((3↑3) ·
(((3↑1) − 1) · ((3↑2) − 1)))) |
296 | | df-9 11786 |
. . . . . . . . . . . . . . . 16
⊢ 9 = (8 +
1) |
297 | 296 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 9 = (8 +
1)) |
298 | 297 | oveq2d 7186 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2↑9) = (2↑(8 +
1))) |
299 | 287, 194 | eqeltrd 2833 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
ℂ) |
300 | | 8nn0 11999 |
. . . . . . . . . . . . . . . 16
⊢ 8 ∈
ℕ0 |
301 | 300 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 8 ∈
ℕ0) |
302 | 299, 192,
301 | expaddd 13604 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2↑(8 + 1)) =
((2↑8) · (2↑1))) |
303 | 298, 302 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2↑9) = ((2↑8)
· (2↑1))) |
304 | | 2exp8 16525 |
. . . . . . . . . . . . . . . . 17
⊢
(2↑8) = ;;256 |
305 | 304 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2↑8) = ;;256) |
306 | 305 | oveq1d 7185 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2↑8) ·
(2↑1)) = (;;256 · (2↑1))) |
307 | 299 | exp1d 13597 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2↑1) =
2) |
308 | 307 | oveq2d 7186 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (;;256
· (2↑1)) = (;;256 · 2)) |
309 | 306, 308 | eqtrd 2773 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2↑8) ·
(2↑1)) = (;;256 · 2)) |
310 | 233, 59 | deccl 12194 |
. . . . . . . . . . . . . . . 16
⊢ ;25 ∈
ℕ0 |
311 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢ ;;256 = ;;256 |
312 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢ ;25 = ;25 |
313 | | 2t2e4 11880 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
· 2) = 4 |
314 | 313, 250 | oveq12i 7182 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
· 2) + (0 + 1)) = (4 + 1) |
315 | | 4p1e5 11862 |
. . . . . . . . . . . . . . . . . 18
⊢ (4 + 1) =
5 |
316 | 314, 315 | eqtri 2761 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
· 2) + (0 + 1)) = 5 |
317 | | 5t2e10 12279 |
. . . . . . . . . . . . . . . . . 18
⊢ (5
· 2) = ;10 |
318 | 93, 237, 250, 317 | decsuc 12210 |
. . . . . . . . . . . . . . . . 17
⊢ ((5
· 2) + 1) = ;11 |
319 | 233, 59, 237, 93, 312, 248, 233, 93, 93, 316, 318 | decmac 12231 |
. . . . . . . . . . . . . . . 16
⊢ ((;25 · 2) + 1) = ;51 |
320 | 233, 310,
231, 311, 233, 93, 319, 255 | decmul1c 12244 |
. . . . . . . . . . . . . . 15
⊢ (;;256 · 2) = ;;512 |
321 | 320 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (;;256
· 2) = ;;512) |
322 | 309, 321 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2↑8) ·
(2↑1)) = ;;512) |
323 | 303, 322 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2↑9) = ;;512) |
324 | 323 | oveq1d 7185 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2↑9) − 1) =
(;;512 − 1)) |
325 | | 1p1e2 11841 |
. . . . . . . . . . . . . 14
⊢ (1 + 1) =
2 |
326 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ ;;511 = ;;511 |
327 | 272, 93, 325, 326 | decsuc 12210 |
. . . . . . . . . . . . 13
⊢ (;;511 + 1) = ;;512 |
328 | 272, 233 | deccl 12194 |
. . . . . . . . . . . . . . 15
⊢ ;;512 ∈ ℕ0 |
329 | 328 | nn0cni 11988 |
. . . . . . . . . . . . . 14
⊢ ;;512 ∈ ℂ |
330 | 272, 93 | deccl 12194 |
. . . . . . . . . . . . . . 15
⊢ ;;511 ∈ ℕ0 |
331 | 330 | nn0cni 11988 |
. . . . . . . . . . . . . 14
⊢ ;;511 ∈ ℂ |
332 | 329, 242,
331 | subadd2i 11052 |
. . . . . . . . . . . . 13
⊢ ((;;512 − 1) = ;;511
↔ (;;511 + 1) = ;;512) |
333 | 327, 332 | mpbir 234 |
. . . . . . . . . . . 12
⊢ (;;512 − 1) = ;;511 |
334 | 333 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (;;512
− 1) = ;;511) |
335 | 324, 334 | eqtr2d 2774 |
. . . . . . . . . 10
⊢ (𝜑 → ;;511 =
((2↑9) − 1)) |
336 | 279, 295,
335 | 3brtr3d 5061 |
. . . . . . . . 9
⊢ (𝜑 → ((3↑3) ·
(((3↑1) − 1) · ((3↑2) − 1))) < ((2↑9)
− 1)) |
337 | 216 | ltm1d 11650 |
. . . . . . . . . 10
⊢ (𝜑 → ((2↑9) − 1)
< (2↑9)) |
338 | 215 | nn0zd 12166 |
. . . . . . . . . . . 12
⊢ (𝜑 → 9 ∈
ℤ) |
339 | 73, 338, 143, 35 | leexp2d 13707 |
. . . . . . . . . . 11
⊢ (𝜑 → (9 ≤ (⌈‘((2
logb 3)↑5)) ↔ (2↑9) ≤ (2↑(⌈‘((2
logb 3)↑5))))) |
340 | 87, 339 | mpbid 235 |
. . . . . . . . . 10
⊢ (𝜑 → (2↑9) ≤
(2↑(⌈‘((2 logb 3)↑5)))) |
341 | 217, 216,
224, 337, 340 | ltletrd 10878 |
. . . . . . . . 9
⊢ (𝜑 → ((2↑9) − 1)
< (2↑(⌈‘((2 logb 3)↑5)))) |
342 | 213, 217,
224, 336, 341 | lttrd 10879 |
. . . . . . . 8
⊢ (𝜑 → ((3↑3) ·
(((3↑1) − 1) · ((3↑2) − 1))) <
(2↑(⌈‘((2 logb 3)↑5)))) |
343 | 204, 342 | eqbrtrd 5052 |
. . . . . . 7
⊢ (𝜑 → ((3↑(⌊‘(2
logb (⌈‘((2 logb 3)↑5))))) ·
∏𝑘 ∈
(1...(⌊‘((2 logb 3)↑2)))((3↑𝑘) − 1)) < (2↑(⌈‘((2
logb 3)↑5)))) |
344 | 343 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 3 = 𝑁) → ((3↑(⌊‘(2
logb (⌈‘((2 logb 3)↑5))))) ·
∏𝑘 ∈
(1...(⌊‘((2 logb 3)↑2)))((3↑𝑘) − 1)) < (2↑(⌈‘((2
logb 3)↑5)))) |
345 | 30, 344 | eqbrtrd 5052 |
. . . . 5
⊢ ((𝜑 ∧ 3 = 𝑁) → ((3↑(⌊‘(2
logb (⌈‘((2 logb 3)↑5))))) ·
∏𝑘 ∈
(1...(⌊‘((2 logb 3)↑2)))((𝑁↑𝑘) − 1)) < (2↑(⌈‘((2
logb 3)↑5)))) |
346 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 3 = 𝑁) → 3 = 𝑁) |
347 | | oveq2 7178 |
. . . . . . . . . . . . 13
⊢ (3 =
𝑁 → (2 logb
3) = (2 logb 𝑁)) |
348 | 347 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 3 = 𝑁) → (2 logb 3) = (2
logb 𝑁)) |
349 | 348 | oveq1d 7185 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 3 = 𝑁) → ((2 logb 3)↑5) =
((2 logb 𝑁)↑5)) |
350 | 349 | fveq2d 6678 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 3 = 𝑁) → (⌈‘((2 logb
3)↑5)) = (⌈‘((2 logb 𝑁)↑5))) |
351 | 8 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 3 = 𝑁) → 𝐵 = (⌈‘((2 logb 𝑁)↑5))) |
352 | 351 | eqcomd 2744 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 3 = 𝑁) → (⌈‘((2 logb
𝑁)↑5)) = 𝐵) |
353 | 350, 352 | eqtrd 2773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 3 = 𝑁) → (⌈‘((2 logb
3)↑5)) = 𝐵) |
354 | 353 | oveq2d 7186 |
. . . . . . . 8
⊢ ((𝜑 ∧ 3 = 𝑁) → (2 logb
(⌈‘((2 logb 3)↑5))) = (2 logb 𝐵)) |
355 | 354 | fveq2d 6678 |
. . . . . . 7
⊢ ((𝜑 ∧ 3 = 𝑁) → (⌊‘(2 logb
(⌈‘((2 logb 3)↑5)))) = (⌊‘(2
logb 𝐵))) |
356 | 346, 355 | oveq12d 7188 |
. . . . . 6
⊢ ((𝜑 ∧ 3 = 𝑁) → (3↑(⌊‘(2
logb (⌈‘((2 logb 3)↑5))))) = (𝑁↑(⌊‘(2
logb 𝐵)))) |
357 | 346 | oveq2d 7186 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 3 = 𝑁) → (2 logb 3) = (2
logb 𝑁)) |
358 | 357 | oveq1d 7185 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 3 = 𝑁) → ((2 logb 3)↑2) =
((2 logb 𝑁)↑2)) |
359 | 358 | fveq2d 6678 |
. . . . . . . 8
⊢ ((𝜑 ∧ 3 = 𝑁) → (⌊‘((2 logb
3)↑2)) = (⌊‘((2 logb 𝑁)↑2))) |
360 | 359 | oveq2d 7186 |
. . . . . . 7
⊢ ((𝜑 ∧ 3 = 𝑁) → (1...(⌊‘((2
logb 3)↑2))) = (1...(⌊‘((2 logb 𝑁)↑2)))) |
361 | 360 | prodeq1d 15367 |
. . . . . 6
⊢ ((𝜑 ∧ 3 = 𝑁) → ∏𝑘 ∈ (1...(⌊‘((2
logb 3)↑2)))((𝑁↑𝑘) − 1) = ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) |
362 | 356, 361 | oveq12d 7188 |
. . . . 5
⊢ ((𝜑 ∧ 3 = 𝑁) → ((3↑(⌊‘(2
logb (⌈‘((2 logb 3)↑5))))) ·
∏𝑘 ∈
(1...(⌊‘((2 logb 3)↑2)))((𝑁↑𝑘) − 1)) = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1))) |
363 | 350 | oveq2d 7186 |
. . . . 5
⊢ ((𝜑 ∧ 3 = 𝑁) → (2↑(⌈‘((2
logb 3)↑5))) = (2↑(⌈‘((2 logb 𝑁)↑5)))) |
364 | 345, 362,
363 | 3brtr3d 5061 |
. . . 4
⊢ ((𝜑 ∧ 3 = 𝑁) → ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) < (2↑(⌈‘((2
logb 𝑁)↑5)))) |
365 | 7 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 3 = 𝑁) → 𝐴 = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1))) |
366 | 365 | eqcomd 2744 |
. . . 4
⊢ ((𝜑 ∧ 3 = 𝑁) → ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) = 𝐴) |
367 | 8 | oveq2i 7181 |
. . . . . 6
⊢
(2↑𝐵) =
(2↑(⌈‘((2 logb 𝑁)↑5))) |
368 | 367 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 3 = 𝑁) → (2↑𝐵) = (2↑(⌈‘((2
logb 𝑁)↑5)))) |
369 | 368 | eqcomd 2744 |
. . . 4
⊢ ((𝜑 ∧ 3 = 𝑁) → (2↑(⌈‘((2
logb 𝑁)↑5))) = (2↑𝐵)) |
370 | 364, 366,
369 | 3brtr3d 5061 |
. . 3
⊢ ((𝜑 ∧ 3 = 𝑁) → 𝐴 < (2↑𝐵)) |
371 | 370 | ex 416 |
. 2
⊢ (𝜑 → (3 = 𝑁 → 𝐴 < (2↑𝐵))) |
372 | | eluzle 12337 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘3) → 3 ≤ 𝑁) |
373 | 3, 372 | syl 17 |
. . 3
⊢ (𝜑 → 3 ≤ 𝑁) |
374 | 14 | zred 12168 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℝ) |
375 | 55, 374 | leloed 10861 |
. . 3
⊢ (𝜑 → (3 ≤ 𝑁 ↔ (3 < 𝑁 ∨ 3 = 𝑁))) |
376 | 373, 375 | mpbid 235 |
. 2
⊢ (𝜑 → (3 < 𝑁 ∨ 3 = 𝑁)) |
377 | 23, 371, 376 | mpjaod 859 |
1
⊢ (𝜑 → 𝐴 < (2↑𝐵)) |