Step | Hyp | Ref
| Expression |
1 | | aks4d1.1 |
. . . 4
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘3)) |
2 | | oveq2 7280 |
. . . . . . 7
⊢ (𝑏 = 𝑎 → (𝑁↑𝑏) = (𝑁↑𝑎)) |
3 | 2 | oveq1d 7287 |
. . . . . 6
⊢ (𝑏 = 𝑎 → ((𝑁↑𝑏) − 1) = ((𝑁↑𝑎) − 1)) |
4 | 3 | cbvprodv 15637 |
. . . . 5
⊢
∏𝑏 ∈
(1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑏) − 1) = ∏𝑎 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑎) − 1) |
5 | 4 | oveq2i 7283 |
. . . 4
⊢ ((𝑁↑(⌊‘(2
logb 𝐵)))
· ∏𝑏 ∈
(1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑏) − 1)) = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑎 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑎) − 1)) |
6 | | aks4d1.2 |
. . . 4
⊢ 𝐵 = (⌈‘((2
logb 𝑁)↑5)) |
7 | | id 22 |
. . . . . . . 8
⊢ (ℎ = 𝑘 → ℎ = 𝑘) |
8 | | oveq2 7280 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑏 → (𝑁↑𝑐) = (𝑁↑𝑏)) |
9 | 8 | oveq1d 7287 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑏 → ((𝑁↑𝑐) − 1) = ((𝑁↑𝑏) − 1)) |
10 | 9 | cbvprodv 15637 |
. . . . . . . . . 10
⊢
∏𝑐 ∈
(1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑐) − 1) = ∏𝑏 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑏) − 1) |
11 | 10 | oveq2i 7283 |
. . . . . . . . 9
⊢ ((𝑁↑(⌊‘(2
logb 𝐵)))
· ∏𝑐 ∈
(1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑐) − 1)) = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑏 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑏) − 1)) |
12 | 11 | a1i 11 |
. . . . . . . 8
⊢ (ℎ = 𝑘 → ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1)) = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑏 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑏) − 1))) |
13 | 7, 12 | breq12d 5092 |
. . . . . . 7
⊢ (ℎ = 𝑘 → (ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1)) ↔ 𝑘 ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑏 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑏) − 1)))) |
14 | 13 | notbid 318 |
. . . . . 6
⊢ (ℎ = 𝑘 → (¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1)) ↔ ¬ 𝑘 ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑏 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑏) − 1)))) |
15 | 14 | cbvrabv 3425 |
. . . . 5
⊢ {ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))} = {𝑘 ∈ (1...𝐵) ∣ ¬ 𝑘 ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑏 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑏) − 1))} |
16 | 15 | infeq1i 9225 |
. . . 4
⊢
inf({ℎ ∈
(1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < ) = inf({𝑘 ∈ (1...𝐵) ∣ ¬ 𝑘 ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑏 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑏) − 1))}, ℝ, <
) |
17 | 1, 5, 6, 16 | aks4d1p4 40096 |
. . 3
⊢ (𝜑 → (inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < ) ∈
(1...𝐵) ∧ ¬
inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < ) ∥
((𝑁↑(⌊‘(2
logb 𝐵)))
· ∏𝑏 ∈
(1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑏) − 1)))) |
18 | 17 | simpld 495 |
. 2
⊢ (𝜑 → inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < ) ∈
(1...𝐵)) |
19 | | oveq2 7280 |
. . . . 5
⊢ (𝑟 = inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < ) → (𝑁 gcd 𝑟) = (𝑁 gcd inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, <
))) |
20 | 19 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 = inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < )) →
(𝑁 gcd 𝑟) = (𝑁 gcd inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, <
))) |
21 | 20 | eqeq1d 2742 |
. . 3
⊢ ((𝜑 ∧ 𝑟 = inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < )) →
((𝑁 gcd 𝑟) = 1 ↔ (𝑁 gcd inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < )) =
1)) |
22 | | fveq2 6771 |
. . . . . 6
⊢ (𝑟 = inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < ) →
(odℤ‘𝑟) = (odℤ‘inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, <
))) |
23 | 22 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 = inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < )) →
(odℤ‘𝑟) = (odℤ‘inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, <
))) |
24 | 23 | fveq1d 6773 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 = inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < )) →
((odℤ‘𝑟)‘𝑁) = ((odℤ‘inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < ))‘𝑁)) |
25 | 24 | breq2d 5091 |
. . 3
⊢ ((𝜑 ∧ 𝑟 = inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < )) → (((2
logb 𝑁)↑2)
< ((odℤ‘𝑟)‘𝑁) ↔ ((2 logb 𝑁)↑2) <
((odℤ‘inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < ))‘𝑁))) |
26 | 21, 25 | anbi12d 631 |
. 2
⊢ ((𝜑 ∧ 𝑟 = inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < )) →
(((𝑁 gcd 𝑟) = 1 ∧ ((2 logb 𝑁)↑2) <
((odℤ‘𝑟)‘𝑁)) ↔ ((𝑁 gcd inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < )) = 1 ∧
((2 logb 𝑁)↑2) <
((odℤ‘inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < ))‘𝑁)))) |
27 | 1, 5, 6, 16 | aks4d1p8 40104 |
. . 3
⊢ (𝜑 → (𝑁 gcd inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < )) =
1) |
28 | 1, 5, 6, 16 | aks4d1p9 40105 |
. . 3
⊢ (𝜑 → ((2 logb 𝑁)↑2) <
((odℤ‘inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < ))‘𝑁)) |
29 | 27, 28 | jca 512 |
. 2
⊢ (𝜑 → ((𝑁 gcd inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < )) = 1 ∧
((2 logb 𝑁)↑2) <
((odℤ‘inf({ℎ ∈ (1...𝐵) ∣ ¬ ℎ ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑐 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑐) − 1))}, ℝ, < ))‘𝑁))) |
30 | 18, 26, 29 | rspcedvd 3564 |
1
⊢ (𝜑 → ∃𝑟 ∈ (1...𝐵)((𝑁 gcd 𝑟) = 1 ∧ ((2 logb 𝑁)↑2) <
((odℤ‘𝑟)‘𝑁))) |