| Step | Hyp | Ref
| Expression |
| 1 | | 2re 12340 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
| 2 | 1 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℝ) |
| 3 | | 2pos 12369 |
. . . . . . . . . 10
⊢ 0 <
2 |
| 4 | 3 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 2) |
| 5 | | aks4d1p9.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘3)) |
| 6 | | eluzelz 12888 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℤ) |
| 7 | 5, 6 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 8 | 7 | zred 12722 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 9 | | 0red 11264 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℝ) |
| 10 | | 3re 12346 |
. . . . . . . . . . 11
⊢ 3 ∈
ℝ |
| 11 | 10 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 3 ∈
ℝ) |
| 12 | | 3pos 12371 |
. . . . . . . . . . 11
⊢ 0 <
3 |
| 13 | 12 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < 3) |
| 14 | | eluzle 12891 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → 3 ≤ 𝑁) |
| 15 | 5, 14 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 3 ≤ 𝑁) |
| 16 | 9, 11, 8, 13, 15 | ltletrd 11421 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 𝑁) |
| 17 | | 1red 11262 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℝ) |
| 18 | | 1lt2 12437 |
. . . . . . . . . . . 12
⊢ 1 <
2 |
| 19 | 18 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 < 2) |
| 20 | 17, 19 | ltned 11397 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ≠ 2) |
| 21 | 20 | necomd 2996 |
. . . . . . . . 9
⊢ (𝜑 → 2 ≠ 1) |
| 22 | 2, 4, 8, 16, 21 | relogbcld 41974 |
. . . . . . . 8
⊢ (𝜑 → (2 logb 𝑁) ∈
ℝ) |
| 23 | 22 | resqcld 14165 |
. . . . . . 7
⊢ (𝜑 → ((2 logb 𝑁)↑2) ∈
ℝ) |
| 24 | | aks4d1p9.2 |
. . . . . . . . . . . . 13
⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) |
| 25 | | aks4d1p9.3 |
. . . . . . . . . . . . 13
⊢ 𝐵 = (⌈‘((2
logb 𝑁)↑5)) |
| 26 | | aks4d1p9.4 |
. . . . . . . . . . . . 13
⊢ 𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) |
| 27 | 5, 24, 25, 26 | aks4d1p4 42080 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑅 ∈ (1...𝐵) ∧ ¬ 𝑅 ∥ 𝐴)) |
| 28 | 27 | simpld 494 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ (1...𝐵)) |
| 29 | | elfznn 13593 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ (1...𝐵) → 𝑅 ∈ ℕ) |
| 30 | 28, 29 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ ℕ) |
| 31 | 5, 24, 25, 26 | aks4d1p8 42088 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) |
| 32 | 30, 7, 31 | 3jca 1129 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 ∈ ℕ ∧ 𝑁 ∈ ℤ ∧ (𝑁 gcd 𝑅) = 1)) |
| 33 | | odzcl 16831 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℕ ∧ 𝑁 ∈ ℤ ∧ (𝑁 gcd 𝑅) = 1) →
((odℤ‘𝑅)‘𝑁) ∈ ℕ) |
| 34 | 32, 33 | syl 17 |
. . . . . . . 8
⊢ (𝜑 →
((odℤ‘𝑅)‘𝑁) ∈ ℕ) |
| 35 | 34 | nnzd 12640 |
. . . . . . 7
⊢ (𝜑 →
((odℤ‘𝑅)‘𝑁) ∈ ℤ) |
| 36 | | flge 13845 |
. . . . . . 7
⊢ ((((2
logb 𝑁)↑2)
∈ ℝ ∧ ((odℤ‘𝑅)‘𝑁) ∈ ℤ) →
(((odℤ‘𝑅)‘𝑁) ≤ ((2 logb 𝑁)↑2) ↔
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2)))) |
| 37 | 23, 35, 36 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 →
(((odℤ‘𝑅)‘𝑁) ≤ ((2 logb 𝑁)↑2) ↔
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2)))) |
| 38 | 37 | biimpd 229 |
. . . . 5
⊢ (𝜑 →
(((odℤ‘𝑅)‘𝑁) ≤ ((2 logb 𝑁)↑2) →
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2)))) |
| 39 | 38 | imp 406 |
. . . 4
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ ((2 logb 𝑁)↑2)) →
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) |
| 40 | 30 | nnzd 12640 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ ℤ) |
| 41 | 40 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → 𝑅 ∈
ℤ) |
| 42 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → 𝑁 ∈
ℤ) |
| 43 | 34 | nnnn0d 12587 |
. . . . . . . . . . 11
⊢ (𝜑 →
((odℤ‘𝑅)‘𝑁) ∈
ℕ0) |
| 44 | 43 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) →
((odℤ‘𝑅)‘𝑁) ∈
ℕ0) |
| 45 | 42, 44 | zexpcld 14128 |
. . . . . . . . 9
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → (𝑁↑((odℤ‘𝑅)‘𝑁)) ∈ ℤ) |
| 46 | | 1zzd 12648 |
. . . . . . . . 9
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → 1
∈ ℤ) |
| 47 | 45, 46 | zsubcld 12727 |
. . . . . . . 8
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → ((𝑁↑((odℤ‘𝑅)‘𝑁)) − 1) ∈
ℤ) |
| 48 | 5, 25 | aks4d1lem1 42063 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐵 ∈ ℕ ∧ 9 < 𝐵)) |
| 49 | 48 | simpld 494 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ ℕ) |
| 50 | 49 | nnred 12281 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 51 | 49 | nngt0d 12315 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 < 𝐵) |
| 52 | 2, 4, 50, 51, 21 | relogbcld 41974 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 logb 𝐵) ∈
ℝ) |
| 53 | 52 | flcld 13838 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (⌊‘(2
logb 𝐵)) ∈
ℤ) |
| 54 | | 2cnd 12344 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 2 ∈
ℂ) |
| 55 | 9, 4 | gtned 11396 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 2 ≠ 0) |
| 56 | 54, 55, 21 | 3jca 1129 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 ∈ ℂ ∧ 2
≠ 0 ∧ 2 ≠ 1)) |
| 57 | | logb1 26812 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 1) =
0) |
| 58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 logb 1) =
0) |
| 59 | | 2z 12649 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℤ |
| 60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 ∈
ℤ) |
| 61 | 2 | leidd 11829 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 ≤ 2) |
| 62 | | 0lt1 11785 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 <
1 |
| 63 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 < 1) |
| 64 | 49 | nnge1d 12314 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ≤ 𝐵) |
| 65 | 60, 61, 17, 63, 50, 51, 64 | logblebd 41977 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 logb 1) ≤
(2 logb 𝐵)) |
| 66 | 58, 65 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ≤ (2 logb
𝐵)) |
| 67 | | 0zd 12625 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ∈
ℤ) |
| 68 | | flge 13845 |
. . . . . . . . . . . . . . . 16
⊢ (((2
logb 𝐵) ∈
ℝ ∧ 0 ∈ ℤ) → (0 ≤ (2 logb 𝐵) ↔ 0 ≤
(⌊‘(2 logb 𝐵)))) |
| 69 | 52, 67, 68 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0 ≤ (2 logb
𝐵) ↔ 0 ≤
(⌊‘(2 logb 𝐵)))) |
| 70 | 66, 69 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤ (⌊‘(2
logb 𝐵))) |
| 71 | 53, 70 | jca 511 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((⌊‘(2
logb 𝐵)) ∈
ℤ ∧ 0 ≤ (⌊‘(2 logb 𝐵)))) |
| 72 | | elnn0z 12626 |
. . . . . . . . . . . . 13
⊢
((⌊‘(2 logb 𝐵)) ∈ ℕ0 ↔
((⌊‘(2 logb 𝐵)) ∈ ℤ ∧ 0 ≤
(⌊‘(2 logb 𝐵)))) |
| 73 | 71, 72 | sylibr 234 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⌊‘(2
logb 𝐵)) ∈
ℕ0) |
| 74 | 7, 73 | zexpcld 14128 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁↑(⌊‘(2 logb
𝐵))) ∈
ℤ) |
| 75 | | fzfid 14014 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...(⌊‘((2
logb 𝑁)↑2))) ∈ Fin) |
| 76 | 7 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑁 ∈ ℤ) |
| 77 | | elfznn 13593 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) → 𝑘 ∈ ℕ) |
| 78 | 77 | nnnn0d 12587 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) → 𝑘 ∈ ℕ0) |
| 79 | 78 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑘 ∈ ℕ0) |
| 80 | 76, 79 | zexpcld 14128 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (𝑁↑𝑘) ∈ ℤ) |
| 81 | | 1zzd 12648 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 ∈
ℤ) |
| 82 | 80, 81 | zsubcld 12727 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → ((𝑁↑𝑘) − 1) ∈ ℤ) |
| 83 | 75, 82 | fprodzcl 15990 |
. . . . . . . . . . 11
⊢ (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1) ∈ ℤ) |
| 84 | 74, 83 | zmulcld 12728 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) ∈
ℤ) |
| 85 | 24 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1))) |
| 86 | 85 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∈ ℤ ↔ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) ∈
ℤ)) |
| 87 | 84, 86 | mpbird 257 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℤ) |
| 88 | 87 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → 𝐴 ∈
ℤ) |
| 89 | | iddvds 16307 |
. . . . . . . . . . 11
⊢
(((odℤ‘𝑅)‘𝑁) ∈ ℤ →
((odℤ‘𝑅)‘𝑁) ∥ ((odℤ‘𝑅)‘𝑁)) |
| 90 | 35, 89 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
((odℤ‘𝑅)‘𝑁) ∥ ((odℤ‘𝑅)‘𝑁)) |
| 91 | | odzdvds 16833 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ ℕ ∧ 𝑁 ∈ ℤ ∧ (𝑁 gcd 𝑅) = 1) ∧
((odℤ‘𝑅)‘𝑁) ∈ ℕ0) → (𝑅 ∥ ((𝑁↑((odℤ‘𝑅)‘𝑁)) − 1) ↔
((odℤ‘𝑅)‘𝑁) ∥ ((odℤ‘𝑅)‘𝑁))) |
| 92 | 32, 43, 91 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅 ∥ ((𝑁↑((odℤ‘𝑅)‘𝑁)) − 1) ↔
((odℤ‘𝑅)‘𝑁) ∥ ((odℤ‘𝑅)‘𝑁))) |
| 93 | 90, 92 | mpbird 257 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∥ ((𝑁↑((odℤ‘𝑅)‘𝑁)) − 1)) |
| 94 | 93 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → 𝑅 ∥ ((𝑁↑((odℤ‘𝑅)‘𝑁)) − 1)) |
| 95 | 73 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) →
(⌊‘(2 logb 𝐵)) ∈
ℕ0) |
| 96 | 42, 95 | zexpcld 14128 |
. . . . . . . . . 10
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → (𝑁↑(⌊‘(2
logb 𝐵))) ∈
ℤ) |
| 97 | | fzfid 14014 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) →
(1...(⌊‘((2 logb 𝑁)↑2))) ∈ Fin) |
| 98 | 42 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑁 ∈ ℤ) |
| 99 | 77 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑘 ∈ ℕ) |
| 100 | 99 | nnnn0d 12587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑘 ∈ ℕ0) |
| 101 | 98, 100 | zexpcld 14128 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (𝑁↑𝑘) ∈ ℤ) |
| 102 | | 1zzd 12648 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 ∈
ℤ) |
| 103 | 101, 102 | zsubcld 12727 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → ((𝑁↑𝑘) − 1) ∈ ℤ) |
| 104 | 97, 103 | fprodzcl 15990 |
. . . . . . . . . 10
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) →
∏𝑘 ∈
(1...(⌊‘((2 logb 𝑁)↑2)))((𝑁↑𝑘) − 1) ∈ ℤ) |
| 105 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑧 =
((odℤ‘𝑅)‘𝑁) → ((𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) − 1))‘𝑧) = ((𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) −
1))‘((odℤ‘𝑅)‘𝑁))) |
| 106 | 105 | breq1d 5153 |
. . . . . . . . . . . 12
⊢ (𝑧 =
((odℤ‘𝑅)‘𝑁) → (((𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) − 1))‘𝑧) ∥ ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) − 1))‘𝑘) ↔ ((𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) −
1))‘((odℤ‘𝑅)‘𝑁)) ∥ ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) − 1))‘𝑘))) |
| 107 | | ssidd 4007 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1...(⌊‘((2
logb 𝑁)↑2))) ⊆ (1...(⌊‘((2
logb 𝑁)↑2)))) |
| 108 | 7 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑁 ∈ ℤ) |
| 109 | | elfznn 13593 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) → 𝑥 ∈ ℕ) |
| 110 | 109 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑥 ∈ ℕ) |
| 111 | 110 | nnnn0d 12587 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑥 ∈ ℕ0) |
| 112 | 108, 111 | zexpcld 14128 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (𝑁↑𝑥) ∈ ℤ) |
| 113 | | 1zzd 12648 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 ∈
ℤ) |
| 114 | 112, 113 | zsubcld 12727 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → ((𝑁↑𝑥) − 1) ∈ ℤ) |
| 115 | 114 | fmpttd 7135 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) − 1)):(1...(⌊‘((2
logb 𝑁)↑2)))⟶ℤ) |
| 116 | 75, 107, 115 | fprodfvdvdsd 16371 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑧 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) − 1))‘𝑧) ∥ ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) − 1))‘𝑘)) |
| 117 | 116 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) →
∀𝑧 ∈
(1...(⌊‘((2 logb 𝑁)↑2)))((𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) − 1))‘𝑧) ∥ ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) − 1))‘𝑘)) |
| 118 | 22 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → (2
logb 𝑁) ∈
ℝ) |
| 119 | 118 | resqcld 14165 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → ((2
logb 𝑁)↑2)
∈ ℝ) |
| 120 | 119 | flcld 13838 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) →
(⌊‘((2 logb 𝑁)↑2)) ∈ ℤ) |
| 121 | 35 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) →
((odℤ‘𝑅)‘𝑁) ∈ ℤ) |
| 122 | 34 | nnge1d 12314 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ≤
((odℤ‘𝑅)‘𝑁)) |
| 123 | 122 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → 1 ≤
((odℤ‘𝑅)‘𝑁)) |
| 124 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) →
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) |
| 125 | 46, 120, 121, 123, 124 | elfzd 13555 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) →
((odℤ‘𝑅)‘𝑁) ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) |
| 126 | 106, 117,
125 | rspcdva 3623 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → ((𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) −
1))‘((odℤ‘𝑅)‘𝑁)) ∥ ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) − 1))‘𝑘)) |
| 127 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → (𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) − 1)) = (𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) − 1))) |
| 128 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) ∧ 𝑥 =
((odℤ‘𝑅)‘𝑁)) → 𝑥 = ((odℤ‘𝑅)‘𝑁)) |
| 129 | 128 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) ∧ 𝑥 =
((odℤ‘𝑅)‘𝑁)) → (𝑁↑𝑥) = (𝑁↑((odℤ‘𝑅)‘𝑁))) |
| 130 | 129 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) ∧ 𝑥 =
((odℤ‘𝑅)‘𝑁)) → ((𝑁↑𝑥) − 1) = ((𝑁↑((odℤ‘𝑅)‘𝑁)) − 1)) |
| 131 | 127, 130,
125, 47 | fvmptd 7023 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → ((𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) −
1))‘((odℤ‘𝑅)‘𝑁)) = ((𝑁↑((odℤ‘𝑅)‘𝑁)) − 1)) |
| 132 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) − 1)) = (𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) − 1))) |
| 133 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) ∧ 𝑥 = 𝑘) → 𝑥 = 𝑘) |
| 134 | 133 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) ∧ 𝑥 = 𝑘) → (𝑁↑𝑥) = (𝑁↑𝑘)) |
| 135 | 134 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) ∧ 𝑥 = 𝑘) → ((𝑁↑𝑥) − 1) = ((𝑁↑𝑘) − 1)) |
| 136 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) |
| 137 | 132, 135,
136, 103 | fvmptd 7023 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → ((𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) − 1))‘𝑘) = ((𝑁↑𝑘) − 1)) |
| 138 | 137 | prodeq2dv 15958 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) →
∏𝑘 ∈
(1...(⌊‘((2 logb 𝑁)↑2)))((𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) − 1))‘𝑘) = ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) |
| 139 | 131, 138 | breq12d 5156 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) →
(((𝑥 ∈
(1...(⌊‘((2 logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) −
1))‘((odℤ‘𝑅)‘𝑁)) ∥ ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑥 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) ↦ ((𝑁↑𝑥) − 1))‘𝑘) ↔ ((𝑁↑((odℤ‘𝑅)‘𝑁)) − 1) ∥ ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1))) |
| 140 | 126, 139 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → ((𝑁↑((odℤ‘𝑅)‘𝑁)) − 1) ∥ ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) |
| 141 | 47, 96, 104, 140 | dvdsmultr2d 16336 |
. . . . . . . . 9
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → ((𝑁↑((odℤ‘𝑅)‘𝑁)) − 1) ∥ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1))) |
| 142 | 24 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → 𝐴 = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1))) |
| 143 | 141, 142 | breqtrrd 5171 |
. . . . . . . 8
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → ((𝑁↑((odℤ‘𝑅)‘𝑁)) − 1) ∥ 𝐴) |
| 144 | 41, 47, 88, 94, 143 | dvdstrd 16332 |
. . . . . . 7
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → 𝑅 ∥ 𝐴) |
| 145 | 144 | ex 412 |
. . . . . 6
⊢ (𝜑 →
(((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2)) → 𝑅 ∥ 𝐴)) |
| 146 | 145 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ ((2 logb 𝑁)↑2)) →
(((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2)) → 𝑅 ∥ 𝐴)) |
| 147 | 146 | imp 406 |
. . . 4
⊢ (((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ ((2 logb 𝑁)↑2)) ∧
((odℤ‘𝑅)‘𝑁) ≤ (⌊‘((2 logb
𝑁)↑2))) → 𝑅 ∥ 𝐴) |
| 148 | 39, 147 | mpdan 687 |
. . 3
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ ((2 logb 𝑁)↑2)) → 𝑅 ∥ 𝐴) |
| 149 | 27 | simprd 495 |
. . . 4
⊢ (𝜑 → ¬ 𝑅 ∥ 𝐴) |
| 150 | 149 | adantr 480 |
. . 3
⊢ ((𝜑 ∧
((odℤ‘𝑅)‘𝑁) ≤ ((2 logb 𝑁)↑2)) → ¬ 𝑅 ∥ 𝐴) |
| 151 | 148, 150 | pm2.65da 817 |
. 2
⊢ (𝜑 → ¬
((odℤ‘𝑅)‘𝑁) ≤ ((2 logb 𝑁)↑2)) |
| 152 | 34 | nnred 12281 |
. . 3
⊢ (𝜑 →
((odℤ‘𝑅)‘𝑁) ∈ ℝ) |
| 153 | 23, 152 | ltnled 11408 |
. 2
⊢ (𝜑 → (((2 logb 𝑁)↑2) <
((odℤ‘𝑅)‘𝑁) ↔ ¬
((odℤ‘𝑅)‘𝑁) ≤ ((2 logb 𝑁)↑2))) |
| 154 | 151, 153 | mpbird 257 |
1
⊢ (𝜑 → ((2 logb 𝑁)↑2) <
((odℤ‘𝑅)‘𝑁)) |