Proof of Theorem aks4d1p6
Step | Hyp | Ref
| Expression |
1 | | aks4d1p6.7 |
. . . . . . 7
⊢ 𝐾 = (𝑃 pCnt 𝑅) |
2 | 1 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐾 = (𝑃 pCnt 𝑅)) |
3 | | aks4d1p6.5 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℙ) |
4 | | aks4d1p6.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘3)) |
5 | | aks4d1p6.2 |
. . . . . . . . . 10
⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) |
6 | | aks4d1p6.3 |
. . . . . . . . . 10
⊢ 𝐵 = (⌈‘((2
logb 𝑁)↑5)) |
7 | | aks4d1p6.4 |
. . . . . . . . . 10
⊢ 𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) |
8 | 4, 5, 6, 7 | aks4d1p4 40084 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 ∈ (1...𝐵) ∧ ¬ 𝑅 ∥ 𝐴)) |
9 | 8 | simpld 495 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ (1...𝐵)) |
10 | | elfznn 13284 |
. . . . . . . 8
⊢ (𝑅 ∈ (1...𝐵) → 𝑅 ∈ ℕ) |
11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ℕ) |
12 | 3, 11 | pccld 16549 |
. . . . . 6
⊢ (𝜑 → (𝑃 pCnt 𝑅) ∈
ℕ0) |
13 | 2, 12 | eqeltrd 2841 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
14 | 13 | nn0zd 12423 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ ℤ) |
15 | 14 | zred 12425 |
. . 3
⊢ (𝜑 → 𝐾 ∈ ℝ) |
16 | | prmnn 16377 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
17 | 3, 16 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ ℕ) |
18 | 17 | nnred 11988 |
. . . 4
⊢ (𝜑 → 𝑃 ∈ ℝ) |
19 | 17 | nngt0d 12022 |
. . . 4
⊢ (𝜑 → 0 < 𝑃) |
20 | 6 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = (⌈‘((2 logb 𝑁)↑5))) |
21 | | 2re 12047 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
22 | 21 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℝ) |
23 | | 2pos 12076 |
. . . . . . . . . . . 12
⊢ 0 <
2 |
24 | 23 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < 2) |
25 | | eluzelz 12591 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℤ) |
26 | 4, 25 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℤ) |
27 | 26 | zred 12425 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℝ) |
28 | | 0red 10979 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈
ℝ) |
29 | | 3re 12053 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℝ |
30 | 29 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 3 ∈
ℝ) |
31 | | 3pos 12078 |
. . . . . . . . . . . . 13
⊢ 0 <
3 |
32 | 31 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 3) |
33 | | eluzle 12594 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘3) → 3 ≤ 𝑁) |
34 | 4, 33 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 3 ≤ 𝑁) |
35 | 28, 30, 27, 32, 34 | ltletrd 11135 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < 𝑁) |
36 | | 1red 10977 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
ℝ) |
37 | | 1lt2 12144 |
. . . . . . . . . . . . . 14
⊢ 1 <
2 |
38 | 37 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 < 2) |
39 | 36, 38 | ltned 11111 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ≠ 2) |
40 | 39 | necomd 3001 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ≠ 1) |
41 | 22, 24, 27, 35, 40 | relogbcld 39977 |
. . . . . . . . . 10
⊢ (𝜑 → (2 logb 𝑁) ∈
ℝ) |
42 | | 5nn0 12253 |
. . . . . . . . . . 11
⊢ 5 ∈
ℕ0 |
43 | 42 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 5 ∈
ℕ0) |
44 | 41, 43 | reexpcld 13879 |
. . . . . . . . 9
⊢ (𝜑 → ((2 logb 𝑁)↑5) ∈
ℝ) |
45 | | ceilcl 13560 |
. . . . . . . . 9
⊢ (((2
logb 𝑁)↑5)
∈ ℝ → (⌈‘((2 logb 𝑁)↑5)) ∈ ℤ) |
46 | 44, 45 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (⌈‘((2
logb 𝑁)↑5))
∈ ℤ) |
47 | 20, 46 | eqeltrd 2841 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℤ) |
48 | 47 | zred 12425 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℝ) |
49 | | 9re 12072 |
. . . . . . . . . 10
⊢ 9 ∈
ℝ |
50 | 49 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 9 ∈
ℝ) |
51 | | 9pos 12086 |
. . . . . . . . . 10
⊢ 0 <
9 |
52 | 51 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 9) |
53 | 27, 34 | 3lexlogpow5ineq4 40061 |
. . . . . . . . 9
⊢ (𝜑 → 9 < ((2 logb
𝑁)↑5)) |
54 | 28, 50, 44, 52, 53 | lttrd 11136 |
. . . . . . . 8
⊢ (𝜑 → 0 < ((2 logb
𝑁)↑5)) |
55 | | ceilge 13563 |
. . . . . . . . . 10
⊢ (((2
logb 𝑁)↑5)
∈ ℝ → ((2 logb 𝑁)↑5) ≤ (⌈‘((2
logb 𝑁)↑5))) |
56 | 44, 55 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((2 logb 𝑁)↑5) ≤
(⌈‘((2 logb 𝑁)↑5))) |
57 | 56, 20 | breqtrrd 5107 |
. . . . . . . 8
⊢ (𝜑 → ((2 logb 𝑁)↑5) ≤ 𝐵) |
58 | 28, 44, 48, 54, 57 | ltletrd 11135 |
. . . . . . 7
⊢ (𝜑 → 0 < 𝐵) |
59 | 47, 58 | jca 512 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∈ ℤ ∧ 0 < 𝐵)) |
60 | | elnnz 12329 |
. . . . . 6
⊢ (𝐵 ∈ ℕ ↔ (𝐵 ∈ ℤ ∧ 0 <
𝐵)) |
61 | 59, 60 | sylibr 233 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℕ) |
62 | 61 | nnred 11988 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℝ) |
63 | 61 | nngt0d 12022 |
. . . 4
⊢ (𝜑 → 0 < 𝐵) |
64 | | 2z 12352 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
65 | 64 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℤ) |
66 | 65 | zred 12425 |
. . . . . . 7
⊢ (𝜑 → 2 ∈
ℝ) |
67 | | prmuz2 16399 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
68 | 3, 67 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈
(ℤ≥‘2)) |
69 | | eluzle 12594 |
. . . . . . . 8
⊢ (𝑃 ∈
(ℤ≥‘2) → 2 ≤ 𝑃) |
70 | 68, 69 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 2 ≤ 𝑃) |
71 | 36, 66, 18, 38, 70 | ltletrd 11135 |
. . . . . 6
⊢ (𝜑 → 1 < 𝑃) |
72 | 36, 71 | ltned 11111 |
. . . . 5
⊢ (𝜑 → 1 ≠ 𝑃) |
73 | 72 | necomd 3001 |
. . . 4
⊢ (𝜑 → 𝑃 ≠ 1) |
74 | 18, 19, 62, 63, 73 | relogbcld 39977 |
. . 3
⊢ (𝜑 → (𝑃 logb 𝐵) ∈ ℝ) |
75 | 66, 24, 62, 63, 40 | relogbcld 39977 |
. . 3
⊢ (𝜑 → (2 logb 𝐵) ∈
ℝ) |
76 | 17 | nnrpd 12769 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈
ℝ+) |
77 | 76 | rpcnd 12773 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℂ) |
78 | 76 | rpne0d 12776 |
. . . . . 6
⊢ (𝜑 → 𝑃 ≠ 0) |
79 | 77, 78, 14 | cxpexpzd 25864 |
. . . . 5
⊢ (𝜑 → (𝑃↑𝑐𝐾) = (𝑃↑𝐾)) |
80 | 18, 13 | reexpcld 13879 |
. . . . . . 7
⊢ (𝜑 → (𝑃↑𝐾) ∈ ℝ) |
81 | 11 | nnred 11988 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ℝ) |
82 | 2 | oveq2d 7287 |
. . . . . . . 8
⊢ (𝜑 → (𝑃↑𝐾) = (𝑃↑(𝑃 pCnt 𝑅))) |
83 | | pcdvds 16563 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝑅)) ∥ 𝑅) |
84 | 3, 11, 83 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝑅)) ∥ 𝑅) |
85 | 17 | nnzd 12424 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ ℤ) |
86 | | zexpcl 13795 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℤ ∧ (𝑃 pCnt 𝑅) ∈ ℕ0) → (𝑃↑(𝑃 pCnt 𝑅)) ∈ ℤ) |
87 | 85, 12, 86 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝑅)) ∈ ℤ) |
88 | | dvdsle 16017 |
. . . . . . . . . 10
⊢ (((𝑃↑(𝑃 pCnt 𝑅)) ∈ ℤ ∧ 𝑅 ∈ ℕ) → ((𝑃↑(𝑃 pCnt 𝑅)) ∥ 𝑅 → (𝑃↑(𝑃 pCnt 𝑅)) ≤ 𝑅)) |
89 | 87, 11, 88 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝑅)) ∥ 𝑅 → (𝑃↑(𝑃 pCnt 𝑅)) ≤ 𝑅)) |
90 | 84, 89 | mpd 15 |
. . . . . . . 8
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝑅)) ≤ 𝑅) |
91 | 82, 90 | eqbrtrd 5101 |
. . . . . . 7
⊢ (𝜑 → (𝑃↑𝐾) ≤ 𝑅) |
92 | | elfzle2 13259 |
. . . . . . . 8
⊢ (𝑅 ∈ (1...𝐵) → 𝑅 ≤ 𝐵) |
93 | 9, 92 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ≤ 𝐵) |
94 | 80, 81, 62, 91, 93 | letrd 11132 |
. . . . . 6
⊢ (𝜑 → (𝑃↑𝐾) ≤ 𝐵) |
95 | 78, 73 | nelprd 4598 |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝑃 ∈ {0, 1}) |
96 | 77, 95 | eldifd 3903 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ (ℂ ∖ {0,
1})) |
97 | 62 | recnd 11004 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℂ) |
98 | 28, 63 | ltned 11111 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≠ 𝐵) |
99 | 98 | necomd 3001 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ≠ 0) |
100 | 99 | neneqd 2950 |
. . . . . . . . 9
⊢ (𝜑 → ¬ 𝐵 = 0) |
101 | | elsng 4581 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℕ → (𝐵 ∈ {0} ↔ 𝐵 = 0)) |
102 | 61, 101 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 ∈ {0} ↔ 𝐵 = 0)) |
103 | 100, 102 | mtbird 325 |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝐵 ∈ {0}) |
104 | 97, 103 | eldifd 3903 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ (ℂ ∖
{0})) |
105 | | cxplogb 25934 |
. . . . . . 7
⊢ ((𝑃 ∈ (ℂ ∖ {0, 1})
∧ 𝐵 ∈ (ℂ
∖ {0})) → (𝑃↑𝑐(𝑃 logb 𝐵)) = 𝐵) |
106 | 96, 104, 105 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝑃↑𝑐(𝑃 logb 𝐵)) = 𝐵) |
107 | 94, 106 | breqtrrd 5107 |
. . . . 5
⊢ (𝜑 → (𝑃↑𝐾) ≤ (𝑃↑𝑐(𝑃 logb 𝐵))) |
108 | 79, 107 | eqbrtrd 5101 |
. . . 4
⊢ (𝜑 → (𝑃↑𝑐𝐾) ≤ (𝑃↑𝑐(𝑃 logb 𝐵))) |
109 | 76 | rpred 12771 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ ℝ) |
110 | 36, 66, 109, 38, 70 | ltletrd 11135 |
. . . . 5
⊢ (𝜑 → 1 < 𝑃) |
111 | 109, 110,
15, 74 | cxpled 25873 |
. . . 4
⊢ (𝜑 → (𝐾 ≤ (𝑃 logb 𝐵) ↔ (𝑃↑𝑐𝐾) ≤ (𝑃↑𝑐(𝑃 logb 𝐵)))) |
112 | 108, 111 | mpbird 256 |
. . 3
⊢ (𝜑 → 𝐾 ≤ (𝑃 logb 𝐵)) |
113 | 22, 38 | rplogcld 25782 |
. . . . 5
⊢ (𝜑 → (log‘2) ∈
ℝ+) |
114 | 109, 110 | rplogcld 25782 |
. . . . 5
⊢ (𝜑 → (log‘𝑃) ∈
ℝ+) |
115 | 61 | nnrpd 12769 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
116 | 115 | relogcld 25776 |
. . . . 5
⊢ (𝜑 → (log‘𝐵) ∈
ℝ) |
117 | 61 | nnge1d 12021 |
. . . . . 6
⊢ (𝜑 → 1 ≤ 𝐵) |
118 | 62, 117 | logge0d 25783 |
. . . . 5
⊢ (𝜑 → 0 ≤ (log‘𝐵)) |
119 | | 2rp 12734 |
. . . . . . . 8
⊢ 2 ∈
ℝ+ |
120 | 119 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 2 ∈
ℝ+) |
121 | 120, 76 | logled 25780 |
. . . . . 6
⊢ (𝜑 → (2 ≤ 𝑃 ↔ (log‘2) ≤ (log‘𝑃))) |
122 | 70, 121 | mpbid 231 |
. . . . 5
⊢ (𝜑 → (log‘2) ≤
(log‘𝑃)) |
123 | 113, 114,
116, 118, 122 | lediv2ad 12793 |
. . . 4
⊢ (𝜑 → ((log‘𝐵) / (log‘𝑃)) ≤ ((log‘𝐵) / (log‘2))) |
124 | | relogbval 25920 |
. . . . . 6
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ ℝ+) → (𝑃 logb 𝐵) = ((log‘𝐵) / (log‘𝑃))) |
125 | 68, 115, 124 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑃 logb 𝐵) = ((log‘𝐵) / (log‘𝑃))) |
126 | 125 | eqcomd 2746 |
. . . 4
⊢ (𝜑 → ((log‘𝐵) / (log‘𝑃)) = (𝑃 logb 𝐵)) |
127 | 65 | uzidd 12597 |
. . . . . 6
⊢ (𝜑 → 2 ∈
(ℤ≥‘2)) |
128 | | relogbval 25920 |
. . . . . 6
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℝ+) → (2
logb 𝐵) =
((log‘𝐵) /
(log‘2))) |
129 | 127, 115,
128 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (2 logb 𝐵) = ((log‘𝐵) /
(log‘2))) |
130 | 129 | eqcomd 2746 |
. . . 4
⊢ (𝜑 → ((log‘𝐵) / (log‘2)) = (2
logb 𝐵)) |
131 | 123, 126,
130 | 3brtr3d 5110 |
. . 3
⊢ (𝜑 → (𝑃 logb 𝐵) ≤ (2 logb 𝐵)) |
132 | 15, 74, 75, 112, 131 | letrd 11132 |
. 2
⊢ (𝜑 → 𝐾 ≤ (2 logb 𝐵)) |
133 | | flge 13523 |
. . 3
⊢ (((2
logb 𝐵) ∈
ℝ ∧ 𝐾 ∈
ℤ) → (𝐾 ≤ (2
logb 𝐵) ↔
𝐾 ≤ (⌊‘(2
logb 𝐵)))) |
134 | 75, 14, 133 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝐾 ≤ (2 logb 𝐵) ↔ 𝐾 ≤ (⌊‘(2 logb
𝐵)))) |
135 | 132, 134 | mpbid 231 |
1
⊢ (𝜑 → 𝐾 ≤ (⌊‘(2 logb
𝐵))) |