Step | Hyp | Ref
| Expression |
1 | | eulerth.1 |
. . . . . 6
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1)) |
2 | 1 | simp1d 994 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
3 | 2 | phicld 12093 |
. . . 4
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℕ) |
4 | | elnnuz 9475 |
. . . 4
⊢
((ϕ‘𝑁)
∈ ℕ ↔ (ϕ‘𝑁) ∈
(ℤ≥‘1)) |
5 | 3, 4 | sylib 121 |
. . 3
⊢ (𝜑 → (ϕ‘𝑁) ∈
(ℤ≥‘1)) |
6 | | eluzfz2 9934 |
. . 3
⊢
((ϕ‘𝑁)
∈ (ℤ≥‘1) → (ϕ‘𝑁) ∈ (1...(ϕ‘𝑁))) |
7 | 5, 6 | syl 14 |
. 2
⊢ (𝜑 → (ϕ‘𝑁) ∈
(1...(ϕ‘𝑁))) |
8 | | oveq2 5832 |
. . . . . . 7
⊢ (𝑤 = 1 → (𝐴↑𝑤) = (𝐴↑1)) |
9 | | oveq2 5832 |
. . . . . . . 8
⊢ (𝑤 = 1 → (1...𝑤) = (1...1)) |
10 | 9 | prodeq1d 11461 |
. . . . . . 7
⊢ (𝑤 = 1 → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) |
11 | 8, 10 | oveq12d 5842 |
. . . . . 6
⊢ (𝑤 = 1 → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥))) |
12 | 11 | oveq1d 5839 |
. . . . 5
⊢ (𝑤 = 1 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁)) |
13 | 9 | prodeq1d 11461 |
. . . . . 6
⊢ (𝑤 = 1 → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) |
14 | 13 | oveq1d 5839 |
. . . . 5
⊢ (𝑤 = 1 → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) |
15 | 12, 14 | eqeq12d 2172 |
. . . 4
⊢ (𝑤 = 1 → ((((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) ↔ (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))) |
16 | 15 | imbi2d 229 |
. . 3
⊢ (𝑤 = 1 → ((𝜑 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) ↔ (𝜑 → (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))) |
17 | | oveq2 5832 |
. . . . . . 7
⊢ (𝑤 = 𝑘 → (𝐴↑𝑤) = (𝐴↑𝑘)) |
18 | | oveq2 5832 |
. . . . . . . 8
⊢ (𝑤 = 𝑘 → (1...𝑤) = (1...𝑘)) |
19 | 18 | prodeq1d 11461 |
. . . . . . 7
⊢ (𝑤 = 𝑘 → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) |
20 | 17, 19 | oveq12d 5842 |
. . . . . 6
⊢ (𝑤 = 𝑘 → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥))) |
21 | 20 | oveq1d 5839 |
. . . . 5
⊢ (𝑤 = 𝑘 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁)) |
22 | 18 | prodeq1d 11461 |
. . . . . 6
⊢ (𝑤 = 𝑘 → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) |
23 | 22 | oveq1d 5839 |
. . . . 5
⊢ (𝑤 = 𝑘 → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) |
24 | 21, 23 | eqeq12d 2172 |
. . . 4
⊢ (𝑤 = 𝑘 → ((((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) ↔ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))) |
25 | 24 | imbi2d 229 |
. . 3
⊢ (𝑤 = 𝑘 → ((𝜑 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) ↔ (𝜑 → (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))) |
26 | | oveq2 5832 |
. . . . . . 7
⊢ (𝑤 = (𝑘 + 1) → (𝐴↑𝑤) = (𝐴↑(𝑘 + 1))) |
27 | | oveq2 5832 |
. . . . . . . 8
⊢ (𝑤 = (𝑘 + 1) → (1...𝑤) = (1...(𝑘 + 1))) |
28 | 27 | prodeq1d 11461 |
. . . . . . 7
⊢ (𝑤 = (𝑘 + 1) → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) |
29 | 26, 28 | oveq12d 5842 |
. . . . . 6
⊢ (𝑤 = (𝑘 + 1) → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥))) |
30 | 29 | oveq1d 5839 |
. . . . 5
⊢ (𝑤 = (𝑘 + 1) → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁)) |
31 | 27 | prodeq1d 11461 |
. . . . . 6
⊢ (𝑤 = (𝑘 + 1) → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁)) |
32 | 31 | oveq1d 5839 |
. . . . 5
⊢ (𝑤 = (𝑘 + 1) → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) |
33 | 30, 32 | eqeq12d 2172 |
. . . 4
⊢ (𝑤 = (𝑘 + 1) → ((((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) ↔ (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))) |
34 | 33 | imbi2d 229 |
. . 3
⊢ (𝑤 = (𝑘 + 1) → ((𝜑 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) ↔ (𝜑 → (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))) |
35 | | oveq2 5832 |
. . . . . . 7
⊢ (𝑤 = (ϕ‘𝑁) → (𝐴↑𝑤) = (𝐴↑(ϕ‘𝑁))) |
36 | | oveq2 5832 |
. . . . . . . 8
⊢ (𝑤 = (ϕ‘𝑁) → (1...𝑤) = (1...(ϕ‘𝑁))) |
37 | 36 | prodeq1d 11461 |
. . . . . . 7
⊢ (𝑤 = (ϕ‘𝑁) → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) |
38 | 35, 37 | oveq12d 5842 |
. . . . . 6
⊢ (𝑤 = (ϕ‘𝑁) → ((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = ((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥))) |
39 | 38 | oveq1d 5839 |
. . . . 5
⊢ (𝑤 = (ϕ‘𝑁) → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) mod 𝑁)) |
40 | 36 | prodeq1d 11461 |
. . . . . 6
⊢ (𝑤 = (ϕ‘𝑁) → ∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁)) |
41 | 40 | oveq1d 5839 |
. . . . 5
⊢ (𝑤 = (ϕ‘𝑁) → (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) |
42 | 39, 41 | eqeq12d 2172 |
. . . 4
⊢ (𝑤 = (ϕ‘𝑁) → ((((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) ↔ (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))) |
43 | 42 | imbi2d 229 |
. . 3
⊢ (𝑤 = (ϕ‘𝑁) → ((𝜑 → (((𝐴↑𝑤) · ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑤)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) ↔ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))) |
44 | 1 | simp2d 995 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℤ) |
45 | | eulerth.2 |
. . . . . . . . . . . 12
⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} |
46 | | ssrab2 3213 |
. . . . . . . . . . . 12
⊢ {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁) |
47 | 45, 46 | eqsstri 3160 |
. . . . . . . . . . 11
⊢ 𝑆 ⊆ (0..^𝑁) |
48 | | fzo0ssnn0 10114 |
. . . . . . . . . . 11
⊢
(0..^𝑁) ⊆
ℕ0 |
49 | 47, 48 | sstri 3137 |
. . . . . . . . . 10
⊢ 𝑆 ⊆
ℕ0 |
50 | | nn0ssz 9185 |
. . . . . . . . . 10
⊢
ℕ0 ⊆ ℤ |
51 | 49, 50 | sstri 3137 |
. . . . . . . . 9
⊢ 𝑆 ⊆
ℤ |
52 | | eulerth.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆) |
53 | | f1of 5414 |
. . . . . . . . . . 11
⊢ (𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆 → 𝐹:(1...(ϕ‘𝑁))⟶𝑆) |
54 | 52, 53 | syl 14 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:(1...(ϕ‘𝑁))⟶𝑆) |
55 | | 1nn 8844 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
56 | 55 | a1i 9 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℕ) |
57 | 3 | nnge1d 8876 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ≤ (ϕ‘𝑁)) |
58 | | elfz1b 9992 |
. . . . . . . . . . 11
⊢ (1 ∈
(1...(ϕ‘𝑁))
↔ (1 ∈ ℕ ∧ (ϕ‘𝑁) ∈ ℕ ∧ 1 ≤
(ϕ‘𝑁))) |
59 | 56, 3, 57, 58 | syl3anbrc 1166 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
(1...(ϕ‘𝑁))) |
60 | 54, 59 | ffvelrnd 5603 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘1) ∈ 𝑆) |
61 | 51, 60 | sseldi 3126 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘1) ∈ ℤ) |
62 | 44, 61 | zmulcld 9292 |
. . . . . . 7
⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℤ) |
63 | | zq 9535 |
. . . . . . 7
⊢ ((𝐴 · (𝐹‘1)) ∈ ℤ → (𝐴 · (𝐹‘1)) ∈ ℚ) |
64 | 62, 63 | syl 14 |
. . . . . 6
⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℚ) |
65 | | nnq 9542 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℚ) |
66 | 2, 65 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℚ) |
67 | 2 | nngt0d 8877 |
. . . . . 6
⊢ (𝜑 → 0 < 𝑁) |
68 | | modqabs2 10257 |
. . . . . 6
⊢ (((𝐴 · (𝐹‘1)) ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 0 <
𝑁) → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
69 | 64, 66, 67, 68 | syl3anc 1220 |
. . . . 5
⊢ (𝜑 → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
70 | | 1z 9193 |
. . . . . . 7
⊢ 1 ∈
ℤ |
71 | 62, 2 | zmodcld 10244 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 · (𝐹‘1)) mod 𝑁) ∈
ℕ0) |
72 | 71 | nn0cnd 9145 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ ℂ) |
73 | | fveq2 5468 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → (𝐹‘𝑥) = (𝐹‘1)) |
74 | 73 | oveq2d 5840 |
. . . . . . . . 9
⊢ (𝑥 = 1 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘1))) |
75 | 74 | oveq1d 5839 |
. . . . . . . 8
⊢ (𝑥 = 1 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
76 | 75 | fprod1 11491 |
. . . . . . 7
⊢ ((1
∈ ℤ ∧ ((𝐴
· (𝐹‘1)) mod
𝑁) ∈ ℂ) →
∏𝑥 ∈
(1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
77 | 70, 72, 76 | sylancr 411 |
. . . . . 6
⊢ (𝜑 → ∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
78 | 77 | oveq1d 5839 |
. . . . 5
⊢ (𝜑 → (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁)) |
79 | 44 | zcnd 9287 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
80 | 79 | exp1d 10546 |
. . . . . . 7
⊢ (𝜑 → (𝐴↑1) = 𝐴) |
81 | | nn0sscn 9095 |
. . . . . . . . . 10
⊢
ℕ0 ⊆ ℂ |
82 | 49, 81 | sstri 3137 |
. . . . . . . . 9
⊢ 𝑆 ⊆
ℂ |
83 | 82, 60 | sseldi 3126 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘1) ∈ ℂ) |
84 | 73 | fprod1 11491 |
. . . . . . . 8
⊢ ((1
∈ ℤ ∧ (𝐹‘1) ∈ ℂ) →
∏𝑥 ∈
(1...1)(𝐹‘𝑥) = (𝐹‘1)) |
85 | 70, 83, 84 | sylancr 411 |
. . . . . . 7
⊢ (𝜑 → ∏𝑥 ∈ (1...1)(𝐹‘𝑥) = (𝐹‘1)) |
86 | 80, 85 | oveq12d 5842 |
. . . . . 6
⊢ (𝜑 → ((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) = (𝐴 · (𝐹‘1))) |
87 | 86 | oveq1d 5839 |
. . . . 5
⊢ (𝜑 → (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
88 | 69, 78, 87 | 3eqtr4rd 2201 |
. . . 4
⊢ (𝜑 → (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) |
89 | 88 | a1i 9 |
. . 3
⊢
((ϕ‘𝑁)
∈ (ℤ≥‘1) → (𝜑 → (((𝐴↑1) · ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...1)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))) |
90 | 44 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝐴 ∈ ℤ) |
91 | | elfzo1 10089 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) ↔ (𝑘 ∈ ℕ ∧ (ϕ‘𝑁) ∈ ℕ ∧ 𝑘 < (ϕ‘𝑁))) |
92 | 91 | simp1bi 997 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 ∈ ℕ) |
93 | 92 | adantl 275 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℕ) |
94 | 93 | nnnn0d 9143 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℕ0) |
95 | | zexpcl 10434 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℤ) |
96 | 90, 94, 95 | syl2anc 409 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴↑𝑘) ∈ ℤ) |
97 | 70 | a1i 9 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 1 ∈
ℤ) |
98 | 93 | nnzd 9285 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℤ) |
99 | 97, 98 | fzfigd 10330 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (1...𝑘) ∈ Fin) |
100 | 54 | ad2antrr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆) |
101 | | elfzelz 9928 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℤ) |
102 | 101 | zred 9286 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℝ) |
103 | 102 | adantl 275 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ∈ ℝ) |
104 | 3 | nnzd 9285 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℤ) |
105 | 104 | ad2antrr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (ϕ‘𝑁) ∈ ℤ) |
106 | 105 | zred 9286 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (ϕ‘𝑁) ∈ ℝ) |
107 | 93 | nnred 8846 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℝ) |
108 | 107 | adantr 274 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑘 ∈ ℝ) |
109 | | elfzle2 9930 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ≤ 𝑘) |
110 | 109 | adantl 275 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ≤ 𝑘) |
111 | | elfzolt2 10055 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 < (ϕ‘𝑁)) |
112 | 111 | ad2antlr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑘 < (ϕ‘𝑁)) |
113 | 103, 108,
106, 110, 112 | lelttrd 8000 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 < (ϕ‘𝑁)) |
114 | 103, 106,
113 | ltled 7994 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ≤ (ϕ‘𝑁)) |
115 | | elfzuz 9924 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈
(ℤ≥‘1)) |
116 | | elfz5 9920 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈
(ℤ≥‘1) ∧ (ϕ‘𝑁) ∈ ℤ) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁))) |
117 | 115, 105,
116 | syl2an2 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁))) |
118 | 114, 117 | mpbird 166 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ∈ (1...(ϕ‘𝑁))) |
119 | 100, 118 | ffvelrnd 5603 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐹‘𝑥) ∈ 𝑆) |
120 | 51, 119 | sseldi 3126 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐹‘𝑥) ∈ ℤ) |
121 | 99, 120 | fprodzcl 11506 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) ∈ ℤ) |
122 | 96, 121 | zmulcld 9292 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) ∈ ℤ) |
123 | | zq 9535 |
. . . . . . . . . 10
⊢ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) ∈ ℤ → ((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) ∈ ℚ) |
124 | 122, 123 | syl 14 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) ∈ ℚ) |
125 | 124 | adantr 274 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → ((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) ∈ ℚ) |
126 | 90 | adantr 274 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝐴 ∈ ℤ) |
127 | 126, 120 | zmulcld 9292 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐴 · (𝐹‘𝑥)) ∈ ℤ) |
128 | 2 | ad2antrr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑁 ∈ ℕ) |
129 | 127, 128 | zmodcld 10244 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈
ℕ0) |
130 | 129 | nn0zd 9284 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℤ) |
131 | 99, 130 | fprodzcl 11506 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℤ) |
132 | | zq 9535 |
. . . . . . . . . 10
⊢
(∏𝑥 ∈
(1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℤ → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℚ) |
133 | 131, 132 | syl 14 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℚ) |
134 | 133 | adantr 274 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℚ) |
135 | 44 | ad2antrr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → 𝐴 ∈ ℤ) |
136 | 54 | ad2antrr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆) |
137 | | fzofzp1 10126 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁))) |
138 | 137 | ad2antlr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁))) |
139 | 136, 138 | ffvelrnd 5603 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝐹‘(𝑘 + 1)) ∈ 𝑆) |
140 | 51, 139 | sseldi 3126 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝐹‘(𝑘 + 1)) ∈ ℤ) |
141 | 135, 140 | zmulcld 9292 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℤ) |
142 | 66 | ad2antrr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → 𝑁 ∈ ℚ) |
143 | 67 | ad2antrr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → 0 < 𝑁) |
144 | | simpr 109 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) |
145 | 125, 134,
141, 142, 143, 144 | modqmul1 10276 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → ((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁)) |
146 | 145 | ex 114 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) → ((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁))) |
147 | 96 | zcnd 9287 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴↑𝑘) ∈ ℂ) |
148 | 121 | zcnd 9287 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) ∈ ℂ) |
149 | 79 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝐴 ∈ ℂ) |
150 | 54 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆) |
151 | 137 | adantl 275 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁))) |
152 | 150, 151 | ffvelrnd 5603 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ 𝑆) |
153 | 82, 152 | sseldi 3126 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ ℂ) |
154 | 147, 148,
149, 153 | mul4d 8030 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) = (((𝐴↑𝑘) · 𝐴) · (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1))))) |
155 | 149, 94 | expp1d 10552 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) |
156 | | elfzouz 10050 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 ∈
(ℤ≥‘1)) |
157 | 156 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈
(ℤ≥‘1)) |
158 | 150 | adantr 274 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆) |
159 | | elfzelz 9928 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈ ℤ) |
160 | 159 | zred 9286 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈ ℝ) |
161 | 160 | adantl 275 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ∈ ℝ) |
162 | | peano2re 8011 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈
ℝ) |
163 | 107, 162 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝑘 + 1) ∈ ℝ) |
164 | 163 | adantr 274 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑘 + 1) ∈ ℝ) |
165 | 104 | ad2antrr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (ϕ‘𝑁) ∈
ℤ) |
166 | 165 | zred 9286 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (ϕ‘𝑁) ∈
ℝ) |
167 | | elfzle2 9930 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ≤ (𝑘 + 1)) |
168 | 167 | adantl 275 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ≤ (𝑘 + 1)) |
169 | 137 | ad2antlr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁))) |
170 | | elfzle2 9930 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 + 1) ∈
(1...(ϕ‘𝑁))
→ (𝑘 + 1) ≤
(ϕ‘𝑁)) |
171 | 169, 170 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑘 + 1) ≤ (ϕ‘𝑁)) |
172 | 161, 164,
166, 168, 171 | letrd 7999 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ≤ (ϕ‘𝑁)) |
173 | | elfzuz 9924 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈
(ℤ≥‘1)) |
174 | 173, 165,
116 | syl2an2 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁))) |
175 | 172, 174 | mpbird 166 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ∈ (1...(ϕ‘𝑁))) |
176 | 158, 175 | ffvelrnd 5603 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹‘𝑥) ∈ 𝑆) |
177 | 82, 176 | sseldi 3126 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹‘𝑥) ∈ ℂ) |
178 | | fveq2 5468 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑘 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑘 + 1))) |
179 | 157, 177,
178 | fprodp1 11497 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥) = (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1)))) |
180 | 155, 179 | oveq12d 5842 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) = (((𝐴↑𝑘) · 𝐴) · (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1))))) |
181 | 154, 180 | eqtr4d 2193 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) = ((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥))) |
182 | 181 | oveq1d 5839 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁)) |
183 | 51, 152 | sseldi 3126 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ ℤ) |
184 | 90, 183 | zmulcld 9292 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℤ) |
185 | 2 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑁 ∈ ℕ) |
186 | 184, 185 | zmodcld 10244 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈
ℕ0) |
187 | 186 | nn0zd 9284 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℤ) |
188 | | zq 9535 |
. . . . . . . . . 10
⊢ (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℤ → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℚ) |
189 | 187, 188 | syl 14 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℚ) |
190 | | zq 9535 |
. . . . . . . . . 10
⊢ ((𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℤ → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℚ) |
191 | 184, 190 | syl 14 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℚ) |
192 | 66 | adantr 274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑁 ∈ ℚ) |
193 | 67 | adantr 274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 0 < 𝑁) |
194 | | modqabs2 10257 |
. . . . . . . . . 10
⊢ (((𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 0 <
𝑁) → (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁)) |
195 | 191, 192,
193, 194 | syl3anc 1220 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁)) |
196 | 189, 191,
131, 192, 193, 195 | modqmul1 10276 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑘 + 1))) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁)) |
197 | 90 | adantr 274 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝐴 ∈ ℤ) |
198 | 51, 176 | sseldi 3126 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹‘𝑥) ∈ ℤ) |
199 | 197, 198 | zmulcld 9292 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐴 · (𝐹‘𝑥)) ∈ ℤ) |
200 | 185 | adantr 274 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑁 ∈ ℕ) |
201 | 199, 200 | zmodcld 10244 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈
ℕ0) |
202 | 201 | nn0cnd 9145 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℂ) |
203 | 178 | oveq2d 5840 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑘 + 1) → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘(𝑘 + 1)))) |
204 | 203 | oveq1d 5839 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑘 + 1) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁)) |
205 | 157, 202,
204 | fprodp1 11497 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁))) |
206 | 186 | nn0cnd 9145 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) ∈ ℂ) |
207 | 131 | zcnd 9287 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ ℂ) |
208 | 206, 207 | mulcomd 7899 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · ((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁))) |
209 | 205, 208 | eqtr4d 2193 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁))) |
210 | 209 | oveq1d 5839 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) = ((((𝐴 · (𝐹‘(𝑘 + 1))) mod 𝑁) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁)) |
211 | 149, 153 | mulcld 7898 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑘 + 1))) ∈ ℂ) |
212 | 207, 211 | mulcomd 7899 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) = ((𝐴 · (𝐹‘(𝑘 + 1))) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁))) |
213 | 212 | oveq1d 5839 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = (((𝐴 · (𝐹‘(𝑘 + 1))) · ∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁)) mod 𝑁)) |
214 | 196, 210,
213 | 3eqtr4rd 2201 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) |
215 | 182, 214 | eqeq12d 2172 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) = ((∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) · (𝐴 · (𝐹‘(𝑘 + 1)))) mod 𝑁) ↔ (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))) |
216 | 146, 215 | sylibd 148 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) → (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))) |
217 | 216 | expcom 115 |
. . . 4
⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → (𝜑 → ((((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁) → (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))) |
218 | 217 | a2d 26 |
. . 3
⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → ((𝜑 → (((𝐴↑𝑘) · ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...𝑘)((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) → (𝜑 → (((𝐴↑(𝑘 + 1)) · ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(𝑘 + 1))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)))) |
219 | 16, 25, 34, 43, 89, 218 | fzind2 10138 |
. 2
⊢
((ϕ‘𝑁)
∈ (1...(ϕ‘𝑁)) → (𝜑 → (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))) |
220 | 7, 219 | mpcom 36 |
1
⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁)) |