Step | Hyp | Ref
| Expression |
1 | | zmodcl 12552 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 mod 𝑁) ∈
ℕ0) |
2 | 1 | 3adant3 1074 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → (𝐴 mod 𝑁) ∈
ℕ0) |
3 | 2 | nn0zd 11356 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → (𝐴 mod 𝑁) ∈ ℤ) |
4 | 3 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → (𝐴 mod 𝑁) ∈ ℤ) |
5 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈
ℙ) |
6 | 5 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑛 ∈ ℙ) |
7 | | simpl3 1059 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) → ¬ 2
∥ 𝑁) |
8 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 2 → (𝑛 ∥ 𝑁 ↔ 2 ∥ 𝑁)) |
9 | 8 | notbid 307 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 2 → (¬ 𝑛 ∥ 𝑁 ↔ ¬ 2 ∥ 𝑁)) |
10 | 7, 9 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) → (𝑛 = 2 → ¬ 𝑛 ∥ 𝑁)) |
11 | 10 | necon2ad 2797 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) → (𝑛 ∥ 𝑁 → 𝑛 ≠ 2)) |
12 | 11 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑛 ≠ 2) |
13 | | eldifsn 4260 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (ℙ ∖ {2})
↔ (𝑛 ∈ ℙ
∧ 𝑛 ≠
2)) |
14 | 6, 12, 13 | sylanbrc 695 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑛 ∈ (ℙ ∖
{2})) |
15 | | oddprm 15353 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (ℙ ∖ {2})
→ ((𝑛 − 1) / 2)
∈ ℕ) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((𝑛 − 1) / 2) ∈
ℕ) |
17 | 16 | nnnn0d 11228 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((𝑛 − 1) / 2) ∈
ℕ0) |
18 | | zexpcl 12737 |
. . . . . . . . . . . . 13
⊢ (((𝐴 mod 𝑁) ∈ ℤ ∧ ((𝑛 − 1) / 2) ∈ ℕ0)
→ ((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) ∈
ℤ) |
19 | 4, 17, 18 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) ∈
ℤ) |
20 | 19 | zred 11358 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) ∈
ℝ) |
21 | | simpll1 1093 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝐴 ∈ ℤ) |
22 | | zexpcl 12737 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ ((𝑛 − 1) / 2) ∈
ℕ0) → (𝐴↑((𝑛 − 1) / 2)) ∈
ℤ) |
23 | 21, 17, 22 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → (𝐴↑((𝑛 − 1) / 2)) ∈
ℤ) |
24 | 23 | zred 11358 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → (𝐴↑((𝑛 − 1) / 2)) ∈
ℝ) |
25 | | 1red 9934 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 1 ∈ ℝ) |
26 | | prmnn 15226 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℙ → 𝑛 ∈
ℕ) |
27 | 26 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑛 ∈ ℕ) |
28 | 27 | nnrpd 11746 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑛 ∈ ℝ+) |
29 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑛 ∥ 𝑁) |
30 | 21 | zred 11358 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝐴 ∈ ℝ) |
31 | | simp2 1055 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → 𝑁 ∈
ℕ) |
32 | 31 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑁 ∈ ℕ) |
33 | 32 | nnrpd 11746 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑁 ∈
ℝ+) |
34 | | modabs2 12566 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ ((𝐴 mod 𝑁) mod 𝑁) = (𝐴 mod 𝑁)) |
35 | 30, 33, 34 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((𝐴 mod 𝑁) mod 𝑁) = (𝐴 mod 𝑁)) |
36 | | moddvds 14829 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 mod 𝑁) ∈ ℤ ∧ 𝐴 ∈ ℤ) → (((𝐴 mod 𝑁) mod 𝑁) = (𝐴 mod 𝑁) ↔ 𝑁 ∥ ((𝐴 mod 𝑁) − 𝐴))) |
37 | 32, 4, 21, 36 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → (((𝐴 mod 𝑁) mod 𝑁) = (𝐴 mod 𝑁) ↔ 𝑁 ∥ ((𝐴 mod 𝑁) − 𝐴))) |
38 | 35, 37 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑁 ∥ ((𝐴 mod 𝑁) − 𝐴)) |
39 | | prmz 15227 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℙ → 𝑛 ∈
ℤ) |
40 | 39 | ad2antlr 759 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑛 ∈ ℤ) |
41 | 32 | nnzd 11357 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑁 ∈ ℤ) |
42 | 4, 21 | zsubcld 11363 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((𝐴 mod 𝑁) − 𝐴) ∈ ℤ) |
43 | | dvdstr 14856 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝐴 mod 𝑁) − 𝐴) ∈ ℤ) → ((𝑛 ∥ 𝑁 ∧ 𝑁 ∥ ((𝐴 mod 𝑁) − 𝐴)) → 𝑛 ∥ ((𝐴 mod 𝑁) − 𝐴))) |
44 | 40, 41, 42, 43 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((𝑛 ∥ 𝑁 ∧ 𝑁 ∥ ((𝐴 mod 𝑁) − 𝐴)) → 𝑛 ∥ ((𝐴 mod 𝑁) − 𝐴))) |
45 | 29, 38, 44 | mp2and 711 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑛 ∥ ((𝐴 mod 𝑁) − 𝐴)) |
46 | | moddvds 14829 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ (𝐴 mod 𝑁) ∈ ℤ ∧ 𝐴 ∈ ℤ) → (((𝐴 mod 𝑁) mod 𝑛) = (𝐴 mod 𝑛) ↔ 𝑛 ∥ ((𝐴 mod 𝑁) − 𝐴))) |
47 | 27, 4, 21, 46 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → (((𝐴 mod 𝑁) mod 𝑛) = (𝐴 mod 𝑛) ↔ 𝑛 ∥ ((𝐴 mod 𝑁) − 𝐴))) |
48 | 45, 47 | mpbird 246 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((𝐴 mod 𝑁) mod 𝑛) = (𝐴 mod 𝑛)) |
49 | | modexp 12861 |
. . . . . . . . . . . 12
⊢ ((((𝐴 mod 𝑁) ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ (((𝑛 − 1) / 2) ∈ ℕ0
∧ 𝑛 ∈
ℝ+) ∧ ((𝐴 mod 𝑁) mod 𝑛) = (𝐴 mod 𝑛)) → (((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) mod 𝑛) = ((𝐴↑((𝑛 − 1) / 2)) mod 𝑛)) |
50 | 4, 21, 17, 28, 48, 49 | syl221anc 1329 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → (((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) mod 𝑛) = ((𝐴↑((𝑛 − 1) / 2)) mod 𝑛)) |
51 | | modadd1 12569 |
. . . . . . . . . . 11
⊢
(((((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) ∈ ℝ ∧ (𝐴↑((𝑛 − 1) / 2)) ∈ ℝ) ∧ (1
∈ ℝ ∧ 𝑛
∈ ℝ+) ∧ (((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) mod 𝑛) = ((𝐴↑((𝑛 − 1) / 2)) mod 𝑛)) → ((((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) + 1) mod 𝑛) = (((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛)) |
52 | 20, 24, 25, 28, 50, 51 | syl221anc 1329 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) + 1) mod 𝑛) = (((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛)) |
53 | 52 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → (((((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1) = ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1)) |
54 | | lgsval3 24840 |
. . . . . . . . . 10
⊢ (((𝐴 mod 𝑁) ∈ ℤ ∧ 𝑛 ∈ (ℙ ∖ {2})) → ((𝐴 mod 𝑁) /L 𝑛) = (((((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1)) |
55 | 4, 14, 54 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((𝐴 mod 𝑁) /L 𝑛) = (((((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1)) |
56 | | lgsval3 24840 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (ℙ ∖ {2}))
→ (𝐴
/L 𝑛) =
((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1)) |
57 | 21, 14, 56 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → (𝐴 /L 𝑛) = ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1)) |
58 | 53, 55, 57 | 3eqtr4d 2654 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((𝐴 mod 𝑁) /L 𝑛) = (𝐴 /L 𝑛)) |
59 | 58 | oveq1d 6564 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁))) |
60 | 3 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → (𝐴 mod 𝑁) ∈ ℤ) |
61 | 39 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → 𝑛 ∈ ℤ) |
62 | | lgscl 24836 |
. . . . . . . . . . . 12
⊢ (((𝐴 mod 𝑁) ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝐴 mod 𝑁) /L 𝑛) ∈ ℤ) |
63 | 60, 61, 62 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → ((𝐴 mod 𝑁) /L 𝑛) ∈ ℤ) |
64 | 63 | zcnd 11359 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → ((𝐴 mod 𝑁) /L 𝑛) ∈ ℂ) |
65 | 64 | exp0d 12864 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → (((𝐴 mod 𝑁) /L 𝑛)↑0) = 1) |
66 | | simpll1 1093 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → 𝐴 ∈ ℤ) |
67 | | lgscl 24836 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝐴 /L 𝑛) ∈
ℤ) |
68 | 66, 61, 67 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → (𝐴 /L 𝑛) ∈ ℤ) |
69 | 68 | zcnd 11359 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → (𝐴 /L 𝑛) ∈ ℂ) |
70 | 69 | exp0d 12864 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → ((𝐴 /L 𝑛)↑0) = 1) |
71 | 65, 70 | eqtr4d 2647 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → (((𝐴 mod 𝑁) /L 𝑛)↑0) = ((𝐴 /L 𝑛)↑0)) |
72 | 31 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) → 𝑁 ∈
ℕ) |
73 | | pceq0 15413 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑛 pCnt 𝑁) = 0 ↔ ¬ 𝑛 ∥ 𝑁)) |
74 | 5, 72, 73 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑁) = 0 ↔ ¬ 𝑛 ∥ 𝑁)) |
75 | 74 | biimpar 501 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → (𝑛 pCnt 𝑁) = 0) |
76 | 75 | oveq2d 6565 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)) = (((𝐴 mod 𝑁) /L 𝑛)↑0)) |
77 | 75 | oveq2d 6565 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑛)↑0)) |
78 | 71, 76, 77 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁))) |
79 | 59, 78 | pm2.61dan 828 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) → (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁))) |
80 | 79 | ifeq1da 4066 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → if(𝑛 ∈ ℙ, (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) |
81 | 80 | mpteq2dv 4673 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))) |
82 | 81 | seqeq3d 12671 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → seq1(
· , (𝑛 ∈
ℕ ↦ if(𝑛 ∈
ℙ, (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))) = seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))) |
83 | 82 | fveq1d 6105 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → (seq1(
· , (𝑛 ∈
ℕ ↦ if(𝑛 ∈
ℙ, (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘𝑁) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘𝑁)) |
84 | | eqid 2610 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) |
85 | 84 | lgsval4a 24844 |
. . 3
⊢ (((𝐴 mod 𝑁) ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod 𝑁) /L 𝑁) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘𝑁)) |
86 | 3, 31, 85 | syl2anc 691 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → ((𝐴 mod 𝑁) /L 𝑁) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘𝑁)) |
87 | | eqid 2610 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) |
88 | 87 | lgsval4a 24844 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 /L 𝑁) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘𝑁)) |
89 | 88 | 3adant3 1074 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → (𝐴 /L 𝑁) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘𝑁)) |
90 | 83, 86, 89 | 3eqtr4d 2654 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → ((𝐴 mod 𝑁) /L 𝑁) = (𝐴 /L 𝑁)) |