| Step | Hyp | Ref
| Expression |
| 1 | | zmodcl 13931 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 mod 𝑁) ∈
ℕ0) |
| 2 | 1 | 3adant3 1133 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → (𝐴 mod 𝑁) ∈
ℕ0) |
| 3 | 2 | nn0zd 12639 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → (𝐴 mod 𝑁) ∈ ℤ) |
| 4 | 3 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → (𝐴 mod 𝑁) ∈ ℤ) |
| 5 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈
ℙ) |
| 6 | 5 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑛 ∈ ℙ) |
| 7 | | simpl3 1194 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) → ¬ 2
∥ 𝑁) |
| 8 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 2 → (𝑛 ∥ 𝑁 ↔ 2 ∥ 𝑁)) |
| 9 | 8 | notbid 318 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 2 → (¬ 𝑛 ∥ 𝑁 ↔ ¬ 2 ∥ 𝑁)) |
| 10 | 7, 9 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) → (𝑛 = 2 → ¬ 𝑛 ∥ 𝑁)) |
| 11 | 10 | necon2ad 2955 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) → (𝑛 ∥ 𝑁 → 𝑛 ≠ 2)) |
| 12 | 11 | imp 406 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑛 ≠ 2) |
| 13 | | eldifsn 4786 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (ℙ ∖ {2})
↔ (𝑛 ∈ ℙ
∧ 𝑛 ≠
2)) |
| 14 | 6, 12, 13 | sylanbrc 583 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑛 ∈ (ℙ ∖
{2})) |
| 15 | | oddprm 16848 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (ℙ ∖ {2})
→ ((𝑛 − 1) / 2)
∈ ℕ) |
| 16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((𝑛 − 1) / 2) ∈
ℕ) |
| 17 | 16 | nnnn0d 12587 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((𝑛 − 1) / 2) ∈
ℕ0) |
| 18 | | zexpcl 14117 |
. . . . . . . . . . . . 13
⊢ (((𝐴 mod 𝑁) ∈ ℤ ∧ ((𝑛 − 1) / 2) ∈ ℕ0)
→ ((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) ∈
ℤ) |
| 19 | 4, 17, 18 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) ∈
ℤ) |
| 20 | 19 | zred 12722 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) ∈
ℝ) |
| 21 | | simpll1 1213 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝐴 ∈ ℤ) |
| 22 | | zexpcl 14117 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ ((𝑛 − 1) / 2) ∈
ℕ0) → (𝐴↑((𝑛 − 1) / 2)) ∈
ℤ) |
| 23 | 21, 17, 22 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → (𝐴↑((𝑛 − 1) / 2)) ∈
ℤ) |
| 24 | 23 | zred 12722 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → (𝐴↑((𝑛 − 1) / 2)) ∈
ℝ) |
| 25 | | 1red 11262 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 1 ∈ ℝ) |
| 26 | | prmnn 16711 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℙ → 𝑛 ∈
ℕ) |
| 27 | 26 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑛 ∈ ℕ) |
| 28 | 27 | nnrpd 13075 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑛 ∈ ℝ+) |
| 29 | | prmz 16712 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℙ → 𝑛 ∈
ℤ) |
| 30 | 29 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑛 ∈ ℤ) |
| 31 | | simp2 1138 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → 𝑁 ∈
ℕ) |
| 32 | 31 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑁 ∈ ℕ) |
| 33 | 32 | nnzd 12640 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑁 ∈ ℤ) |
| 34 | 4, 21 | zsubcld 12727 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((𝐴 mod 𝑁) − 𝐴) ∈ ℤ) |
| 35 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑛 ∥ 𝑁) |
| 36 | 21 | zred 12722 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝐴 ∈ ℝ) |
| 37 | 32 | nnrpd 13075 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑁 ∈
ℝ+) |
| 38 | | modabs2 13945 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ ((𝐴 mod 𝑁) mod 𝑁) = (𝐴 mod 𝑁)) |
| 39 | 36, 37, 38 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((𝐴 mod 𝑁) mod 𝑁) = (𝐴 mod 𝑁)) |
| 40 | | moddvds 16301 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 mod 𝑁) ∈ ℤ ∧ 𝐴 ∈ ℤ) → (((𝐴 mod 𝑁) mod 𝑁) = (𝐴 mod 𝑁) ↔ 𝑁 ∥ ((𝐴 mod 𝑁) − 𝐴))) |
| 41 | 32, 4, 21, 40 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → (((𝐴 mod 𝑁) mod 𝑁) = (𝐴 mod 𝑁) ↔ 𝑁 ∥ ((𝐴 mod 𝑁) − 𝐴))) |
| 42 | 39, 41 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑁 ∥ ((𝐴 mod 𝑁) − 𝐴)) |
| 43 | 30, 33, 34, 35, 42 | dvdstrd 16332 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → 𝑛 ∥ ((𝐴 mod 𝑁) − 𝐴)) |
| 44 | | moddvds 16301 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ (𝐴 mod 𝑁) ∈ ℤ ∧ 𝐴 ∈ ℤ) → (((𝐴 mod 𝑁) mod 𝑛) = (𝐴 mod 𝑛) ↔ 𝑛 ∥ ((𝐴 mod 𝑁) − 𝐴))) |
| 45 | 27, 4, 21, 44 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → (((𝐴 mod 𝑁) mod 𝑛) = (𝐴 mod 𝑛) ↔ 𝑛 ∥ ((𝐴 mod 𝑁) − 𝐴))) |
| 46 | 43, 45 | mpbird 257 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((𝐴 mod 𝑁) mod 𝑛) = (𝐴 mod 𝑛)) |
| 47 | | modexp 14277 |
. . . . . . . . . . . 12
⊢ ((((𝐴 mod 𝑁) ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ (((𝑛 − 1) / 2) ∈ ℕ0
∧ 𝑛 ∈
ℝ+) ∧ ((𝐴 mod 𝑁) mod 𝑛) = (𝐴 mod 𝑛)) → (((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) mod 𝑛) = ((𝐴↑((𝑛 − 1) / 2)) mod 𝑛)) |
| 48 | 4, 21, 17, 28, 46, 47 | syl221anc 1383 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → (((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) mod 𝑛) = ((𝐴↑((𝑛 − 1) / 2)) mod 𝑛)) |
| 49 | | modadd1 13948 |
. . . . . . . . . . 11
⊢
(((((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) ∈ ℝ ∧ (𝐴↑((𝑛 − 1) / 2)) ∈ ℝ) ∧ (1
∈ ℝ ∧ 𝑛
∈ ℝ+) ∧ (((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) mod 𝑛) = ((𝐴↑((𝑛 − 1) / 2)) mod 𝑛)) → ((((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) + 1) mod 𝑛) = (((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛)) |
| 50 | 20, 24, 25, 28, 48, 49 | syl221anc 1383 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) + 1) mod 𝑛) = (((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛)) |
| 51 | 50 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → (((((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1) = ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1)) |
| 52 | | lgsval3 27359 |
. . . . . . . . . 10
⊢ (((𝐴 mod 𝑁) ∈ ℤ ∧ 𝑛 ∈ (ℙ ∖ {2})) → ((𝐴 mod 𝑁) /L 𝑛) = (((((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1)) |
| 53 | 4, 14, 52 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((𝐴 mod 𝑁) /L 𝑛) = (((((𝐴 mod 𝑁)↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1)) |
| 54 | | lgsval3 27359 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (ℙ ∖ {2}))
→ (𝐴
/L 𝑛) =
((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1)) |
| 55 | 21, 14, 54 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → (𝐴 /L 𝑛) = ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1)) |
| 56 | 51, 53, 55 | 3eqtr4d 2787 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → ((𝐴 mod 𝑁) /L 𝑛) = (𝐴 /L 𝑛)) |
| 57 | 56 | oveq1d 7446 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ 𝑛 ∥ 𝑁) → (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁))) |
| 58 | 3 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → (𝐴 mod 𝑁) ∈ ℤ) |
| 59 | 29 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → 𝑛 ∈ ℤ) |
| 60 | | lgscl 27355 |
. . . . . . . . . . . 12
⊢ (((𝐴 mod 𝑁) ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝐴 mod 𝑁) /L 𝑛) ∈ ℤ) |
| 61 | 58, 59, 60 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → ((𝐴 mod 𝑁) /L 𝑛) ∈ ℤ) |
| 62 | 61 | zcnd 12723 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → ((𝐴 mod 𝑁) /L 𝑛) ∈ ℂ) |
| 63 | 62 | exp0d 14180 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → (((𝐴 mod 𝑁) /L 𝑛)↑0) = 1) |
| 64 | | simpll1 1213 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → 𝐴 ∈ ℤ) |
| 65 | | lgscl 27355 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝐴 /L 𝑛) ∈
ℤ) |
| 66 | 64, 59, 65 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → (𝐴 /L 𝑛) ∈ ℤ) |
| 67 | 66 | zcnd 12723 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → (𝐴 /L 𝑛) ∈ ℂ) |
| 68 | 67 | exp0d 14180 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → ((𝐴 /L 𝑛)↑0) = 1) |
| 69 | 63, 68 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → (((𝐴 mod 𝑁) /L 𝑛)↑0) = ((𝐴 /L 𝑛)↑0)) |
| 70 | 31 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) → 𝑁 ∈
ℕ) |
| 71 | | pceq0 16909 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑛 pCnt 𝑁) = 0 ↔ ¬ 𝑛 ∥ 𝑁)) |
| 72 | 5, 70, 71 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑁) = 0 ↔ ¬ 𝑛 ∥ 𝑁)) |
| 73 | 72 | biimpar 477 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → (𝑛 pCnt 𝑁) = 0) |
| 74 | 73 | oveq2d 7447 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)) = (((𝐴 mod 𝑁) /L 𝑛)↑0)) |
| 75 | 73 | oveq2d 7447 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑛)↑0)) |
| 76 | 69, 74, 75 | 3eqtr4d 2787 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) ∧ ¬
𝑛 ∥ 𝑁) → (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁))) |
| 77 | 57, 76 | pm2.61dan 813 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑛 ∈ ℙ) → (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)) = ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁))) |
| 78 | 77 | ifeq1da 4557 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → if(𝑛 ∈ ℙ, (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1) = if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) |
| 79 | 78 | mpteq2dv 5244 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))) |
| 80 | 79 | seqeq3d 14050 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → seq1(
· , (𝑛 ∈
ℕ ↦ if(𝑛 ∈
ℙ, (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))) = seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))) |
| 81 | 80 | fveq1d 6908 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → (seq1(
· , (𝑛 ∈
ℕ ↦ if(𝑛 ∈
ℙ, (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘𝑁) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘𝑁)) |
| 82 | | eqid 2737 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) |
| 83 | 82 | lgsval4a 27363 |
. . 3
⊢ (((𝐴 mod 𝑁) ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod 𝑁) /L 𝑁) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘𝑁)) |
| 84 | 3, 31, 83 | syl2anc 584 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → ((𝐴 mod 𝑁) /L 𝑁) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (((𝐴 mod 𝑁) /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘𝑁)) |
| 85 | | eqid 2737 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) |
| 86 | 85 | lgsval4a 27363 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 /L 𝑁) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘𝑁)) |
| 87 | 86 | 3adant3 1133 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → (𝐴 /L 𝑁) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘𝑁)) |
| 88 | 81, 84, 87 | 3eqtr4d 2787 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → ((𝐴 mod 𝑁) /L 𝑁) = (𝐴 /L 𝑁)) |