Step | Hyp | Ref
| Expression |
1 | | aks4d1p3.1 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘3)) |
2 | | aks4d1p3.2 |
. . . . . 6
⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) |
3 | | aks4d1p3.3 |
. . . . . 6
⊢ 𝐵 = (⌈‘((2
logb 𝑁)↑5)) |
4 | 1, 2, 3 | aks4d1p1 39847 |
. . . . 5
⊢ (𝜑 → 𝐴 < (2↑𝐵)) |
5 | 4 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → 𝐴 < (2↑𝐵)) |
6 | | 2re 11929 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
7 | 6 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℝ) |
8 | 3 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 = (⌈‘((2 logb 𝑁)↑5))) |
9 | | 2pos 11958 |
. . . . . . . . . . . . . . 15
⊢ 0 <
2 |
10 | 9 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 2) |
11 | | eluzelz 12473 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℤ) |
12 | 1, 11 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℤ) |
13 | 12 | zred 12307 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℝ) |
14 | | 0red 10861 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ∈
ℝ) |
15 | | 3re 11935 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℝ |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 3 ∈
ℝ) |
17 | | 3pos 11960 |
. . . . . . . . . . . . . . . 16
⊢ 0 <
3 |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 < 3) |
19 | | eluzle 12476 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → 3 ≤ 𝑁) |
20 | 1, 19 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 3 ≤ 𝑁) |
21 | 14, 16, 13, 18, 20 | ltletrd 11017 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 𝑁) |
22 | | 1red 10859 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℝ) |
23 | | 1lt2 12026 |
. . . . . . . . . . . . . . . . 17
⊢ 1 <
2 |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 < 2) |
25 | 22, 24 | ltned 10993 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ≠ 2) |
26 | 25 | necomd 2997 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ≠ 1) |
27 | 7, 10, 13, 21, 26 | relogbcld 39744 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 logb 𝑁) ∈
ℝ) |
28 | | 5nn0 12135 |
. . . . . . . . . . . . . 14
⊢ 5 ∈
ℕ0 |
29 | 28 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 5 ∈
ℕ0) |
30 | 27, 29 | reexpcld 13761 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 logb 𝑁)↑5) ∈
ℝ) |
31 | | ceilcl 13442 |
. . . . . . . . . . . 12
⊢ (((2
logb 𝑁)↑5)
∈ ℝ → (⌈‘((2 logb 𝑁)↑5)) ∈ ℤ) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌈‘((2
logb 𝑁)↑5))
∈ ℤ) |
33 | 8, 32 | eqeltrd 2839 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℤ) |
34 | 32 | zred 12307 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⌈‘((2
logb 𝑁)↑5))
∈ ℝ) |
35 | 8, 34 | eqeltrd 2839 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) |
36 | | 7re 11948 |
. . . . . . . . . . . . . . 15
⊢ 7 ∈
ℝ |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 7 ∈
ℝ) |
38 | | 7pos 11966 |
. . . . . . . . . . . . . . 15
⊢ 0 <
7 |
39 | 38 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 7) |
40 | 13, 20 | 3lexlogpow5ineq3 39829 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 7 < ((2 logb
𝑁)↑5)) |
41 | 14, 37, 30, 39, 40 | lttrd 11018 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < ((2 logb
𝑁)↑5)) |
42 | | ceilge 13445 |
. . . . . . . . . . . . . 14
⊢ (((2
logb 𝑁)↑5)
∈ ℝ → ((2 logb 𝑁)↑5) ≤ (⌈‘((2
logb 𝑁)↑5))) |
43 | 30, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 logb 𝑁)↑5) ≤
(⌈‘((2 logb 𝑁)↑5))) |
44 | 14, 30, 34, 41, 43 | ltletrd 11017 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < (⌈‘((2
logb 𝑁)↑5))) |
45 | 44, 8 | breqtrrd 5096 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < 𝐵) |
46 | 14, 35, 45 | ltled 11005 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 𝐵) |
47 | 33, 46 | jca 515 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 ∈ ℤ ∧ 0 ≤ 𝐵)) |
48 | | elnn0z 12214 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℕ0
↔ (𝐵 ∈ ℤ
∧ 0 ≤ 𝐵)) |
49 | 47, 48 | sylibr 237 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℕ0) |
50 | 7, 49 | reexpcld 13761 |
. . . . . . 7
⊢ (𝜑 → (2↑𝐵) ∈ ℝ) |
51 | 50 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (2↑𝐵) ∈ ℝ) |
52 | | elfznn 13166 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ (1...𝐵) → 𝑞 ∈ ℕ) |
53 | 52 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ (1...𝐵)) → 𝑞 ∈ ℕ) |
54 | 53 | nnzd 12306 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ (1...𝐵)) → 𝑞 ∈ ℤ) |
55 | 54 | ex 416 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑞 ∈ (1...𝐵) → 𝑞 ∈ ℤ)) |
56 | 55 | ssrdv 3922 |
. . . . . . . . 9
⊢ (𝜑 → (1...𝐵) ⊆ ℤ) |
57 | | fzfid 13573 |
. . . . . . . . 9
⊢ (𝜑 → (1...𝐵) ∈ Fin) |
58 | | lcmfcl 16213 |
. . . . . . . . 9
⊢
(((1...𝐵) ⊆
ℤ ∧ (1...𝐵)
∈ Fin) → (lcm‘(1...𝐵)) ∈
ℕ0) |
59 | 56, 57, 58 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 →
(lcm‘(1...𝐵))
∈ ℕ0) |
60 | 59 | nn0red 12176 |
. . . . . . 7
⊢ (𝜑 →
(lcm‘(1...𝐵))
∈ ℝ) |
61 | 60 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (lcm‘(1...𝐵)) ∈
ℝ) |
62 | 2 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1))) |
63 | | elnnz 12211 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 <
𝑁)) |
64 | 12, 21, 63 | sylanbrc 586 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℕ) |
65 | 7, 10, 35, 45, 26 | relogbcld 39744 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 logb 𝐵) ∈
ℝ) |
66 | 65 | flcld 13398 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (⌊‘(2
logb 𝐵)) ∈
ℤ) |
67 | 7, 10, 7, 10, 26 | relogbcld 39744 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 logb 2)
∈ ℝ) |
68 | | 0le1 11380 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ≤
1 |
69 | 68 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤ 1) |
70 | 7 | recnd 10886 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 2 ∈
ℂ) |
71 | 14, 10 | gtned 10992 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 2 ≠ 0) |
72 | | logbid1 25678 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 2) =
1) |
73 | 70, 71, 26, 72 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 logb 2) =
1) |
74 | 73 | eqcomd 2744 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 = (2 logb
2)) |
75 | 69, 74 | breqtrd 5094 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ≤ (2 logb
2)) |
76 | | 2z 12234 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℤ |
77 | 76 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 2 ∈
ℤ) |
78 | 7 | leidd 11423 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 2 ≤ 2) |
79 | | 2lt7 12045 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 <
7 |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 2 < 7) |
81 | 7, 37, 80 | ltled 11005 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 ≤ 7) |
82 | 37, 30, 34, 40, 43 | ltletrd 11017 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 7 < (⌈‘((2
logb 𝑁)↑5))) |
83 | 82, 8 | breqtrrd 5096 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 7 < 𝐵) |
84 | 37, 35, 83 | ltled 11005 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 7 ≤ 𝐵) |
85 | 7, 37, 35, 81, 84 | letrd 11014 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 2 ≤ 𝐵) |
86 | 77, 78, 7, 10, 35, 45, 85 | logblebd 39747 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 logb 2) ≤
(2 logb 𝐵)) |
87 | 14, 67, 65, 75, 86 | letrd 11014 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤ (2 logb
𝐵)) |
88 | | 0zd 12213 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ∈
ℤ) |
89 | | flge 13405 |
. . . . . . . . . . . . . . 15
⊢ (((2
logb 𝐵) ∈
ℝ ∧ 0 ∈ ℤ) → (0 ≤ (2 logb 𝐵) ↔ 0 ≤
(⌊‘(2 logb 𝐵)))) |
90 | 65, 88, 89 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0 ≤ (2 logb
𝐵) ↔ 0 ≤
(⌊‘(2 logb 𝐵)))) |
91 | 87, 90 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ (⌊‘(2
logb 𝐵))) |
92 | 66, 91 | jca 515 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((⌊‘(2
logb 𝐵)) ∈
ℤ ∧ 0 ≤ (⌊‘(2 logb 𝐵)))) |
93 | | elnn0z 12214 |
. . . . . . . . . . . 12
⊢
((⌊‘(2 logb 𝐵)) ∈ ℕ0 ↔
((⌊‘(2 logb 𝐵)) ∈ ℤ ∧ 0 ≤
(⌊‘(2 logb 𝐵)))) |
94 | 92, 93 | sylibr 237 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌊‘(2
logb 𝐵)) ∈
ℕ0) |
95 | 64, 94 | nnexpcld 13840 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁↑(⌊‘(2 logb
𝐵))) ∈
ℕ) |
96 | | fzfid 13573 |
. . . . . . . . . . 11
⊢ (𝜑 → (1...(⌊‘((2
logb 𝑁)↑2))) ∈ Fin) |
97 | 12 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑁 ∈ ℤ) |
98 | | elfznn 13166 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) → 𝑘 ∈ ℕ) |
99 | 98 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑘 ∈ ℕ) |
100 | 99 | nnnn0d 12175 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑘 ∈ ℕ0) |
101 | | zexpcl 13677 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈ ℕ0)
→ (𝑁↑𝑘) ∈
ℤ) |
102 | 97, 100, 101 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (𝑁↑𝑘) ∈ ℤ) |
103 | | 1zzd 12233 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 ∈
ℤ) |
104 | 102, 103 | zsubcld 12312 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → ((𝑁↑𝑘) − 1) ∈ ℤ) |
105 | | 1cnd 10853 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 ∈
ℂ) |
106 | 105 | addid1d 11057 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (1 + 0) =
1) |
107 | 22 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 ∈
ℝ) |
108 | | 1nn0 12131 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℕ0 |
109 | 108 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 ∈
ℕ0) |
110 | 13, 109 | reexpcld 13761 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁↑1) ∈ ℝ) |
111 | 110 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (𝑁↑1) ∈ ℝ) |
112 | 102 | zred 12307 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (𝑁↑𝑘) ∈ ℝ) |
113 | | 1lt3 12028 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 <
3 |
114 | 113 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 1 < 3) |
115 | 22, 16, 13, 114, 20 | ltletrd 11017 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 < 𝑁) |
116 | 13 | recnd 10886 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℂ) |
117 | 116 | exp1d 13739 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁↑1) = 𝑁) |
118 | 117 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 = (𝑁↑1)) |
119 | 115, 118 | breqtrd 5094 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 < (𝑁↑1)) |
120 | 119 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 < (𝑁↑1)) |
121 | 13 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑁 ∈ ℝ) |
122 | 64 | nnge1d 11903 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 ≤ 𝑁) |
123 | 122 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 ≤ 𝑁) |
124 | | elfzuz 13133 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) → 𝑘 ∈
(ℤ≥‘1)) |
125 | 124 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑘 ∈
(ℤ≥‘1)) |
126 | 121, 123,
125 | leexp2ad 13851 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (𝑁↑1) ≤ (𝑁↑𝑘)) |
127 | 107, 111,
112, 120, 126 | ltletrd 11017 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 < (𝑁↑𝑘)) |
128 | 106, 127 | eqbrtrd 5090 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (1 + 0) < (𝑁↑𝑘)) |
129 | 14 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 0 ∈
ℝ) |
130 | 107, 129,
112 | ltaddsub2d 11458 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → ((1 + 0) < (𝑁↑𝑘) ↔ 0 < ((𝑁↑𝑘) − 1))) |
131 | 128, 130 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 0 < ((𝑁↑𝑘) − 1)) |
132 | 104, 131 | jca 515 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (((𝑁↑𝑘) − 1) ∈ ℤ ∧ 0 <
((𝑁↑𝑘) − 1))) |
133 | | elnnz 12211 |
. . . . . . . . . . . 12
⊢ (((𝑁↑𝑘) − 1) ∈ ℕ ↔ (((𝑁↑𝑘) − 1) ∈ ℤ ∧ 0 <
((𝑁↑𝑘) − 1))) |
134 | 132, 133 | sylibr 237 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → ((𝑁↑𝑘) − 1) ∈ ℕ) |
135 | 96, 134 | fprodnncl 15545 |
. . . . . . . . . 10
⊢ (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1) ∈ ℕ) |
136 | 95, 135 | nnmulcld 11908 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) ∈
ℕ) |
137 | 62, 136 | eqeltrd 2839 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℕ) |
138 | 137 | nnred 11870 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
139 | 138 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → 𝐴 ∈ ℝ) |
140 | 1, 2, 3 | aks4d1p2 39848 |
. . . . . . 7
⊢ (𝜑 → (2↑𝐵) ≤ (lcm‘(1...𝐵))) |
141 | 140 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (2↑𝐵) ≤ (lcm‘(1...𝐵))) |
142 | 137 | nnzd 12306 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℤ) |
143 | 142 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → 𝐴 ∈ ℤ) |
144 | 56 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (1...𝐵) ⊆ ℤ) |
145 | | fzfid 13573 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (1...𝐵) ∈ Fin) |
146 | | lcmfdvdsb 16228 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (1...𝐵) ⊆ ℤ ∧
(1...𝐵) ∈ Fin) →
(∀𝑟 ∈
(1...𝐵)𝑟 ∥ 𝐴 ↔ (lcm‘(1...𝐵)) ∥ 𝐴)) |
147 | 143, 144,
145, 146 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴 ↔ (lcm‘(1...𝐵)) ∥ 𝐴)) |
148 | 147 | biimpd 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴 → (lcm‘(1...𝐵)) ∥ 𝐴)) |
149 | 148 | syldbl2 841 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (lcm‘(1...𝐵)) ∥ 𝐴) |
150 | 59 | nn0zd 12305 |
. . . . . . . . 9
⊢ (𝜑 →
(lcm‘(1...𝐵))
∈ ℤ) |
151 | 150 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (lcm‘(1...𝐵)) ∈
ℤ) |
152 | 137 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → 𝐴 ∈ ℕ) |
153 | | dvdsle 15899 |
. . . . . . . 8
⊢
(((lcm‘(1...𝐵)) ∈ ℤ ∧ 𝐴 ∈ ℕ) →
((lcm‘(1...𝐵))
∥ 𝐴 →
(lcm‘(1...𝐵))
≤ 𝐴)) |
154 | 151, 152,
153 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → ((lcm‘(1...𝐵)) ∥ 𝐴 → (lcm‘(1...𝐵)) ≤ 𝐴)) |
155 | 149, 154 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (lcm‘(1...𝐵)) ≤ 𝐴) |
156 | 51, 61, 139, 141, 155 | letrd 11014 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (2↑𝐵) ≤ 𝐴) |
157 | 51, 139 | lenltd 11003 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → ((2↑𝐵) ≤ 𝐴 ↔ ¬ 𝐴 < (2↑𝐵))) |
158 | 156, 157 | mpbid 235 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → ¬ 𝐴 < (2↑𝐵)) |
159 | 5, 158 | pm2.21dd 198 |
. . 3
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → ¬ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) |
160 | | simpr 488 |
. . 3
⊢ ((𝜑 ∧ ¬ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → ¬ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) |
161 | 159, 160 | pm2.61dan 813 |
. 2
⊢ (𝜑 → ¬ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) |
162 | | rexnal 3164 |
. 2
⊢
(∃𝑟 ∈
(1...𝐵) ¬ 𝑟 ∥ 𝐴 ↔ ¬ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) |
163 | 161, 162 | sylibr 237 |
1
⊢ (𝜑 → ∃𝑟 ∈ (1...𝐵) ¬ 𝑟 ∥ 𝐴) |