Step | Hyp | Ref
| Expression |
1 | | eulerth.1 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1)) |
2 | 1 | simp1d 1141 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℕ) |
3 | 2 | phicld 16471 |
. . . . . . . . 9
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℕ) |
4 | 3 | nnred 11988 |
. . . . . . . 8
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℝ) |
5 | 4 | leidd 11541 |
. . . . . . 7
⊢ (𝜑 → (ϕ‘𝑁) ≤ (ϕ‘𝑁)) |
6 | 3 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)) → (ϕ‘𝑁) ∈
ℕ) |
7 | | breq1 5082 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (𝑥 ≤ (ϕ‘𝑁) ↔ 1 ≤ (ϕ‘𝑁))) |
8 | 7 | anbi2d 629 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ 1 ≤ (ϕ‘𝑁)))) |
9 | | oveq2 7279 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → (𝐴↑𝑥) = (𝐴↑1)) |
10 | | fveq2 6771 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → (seq1( · ,
𝐹)‘𝑥) = (seq1( · , 𝐹)‘1)) |
11 | 9, 10 | oveq12d 7289 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑1) · (seq1( · , 𝐹)‘1))) |
12 | 11 | oveq1d 7286 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁)) |
13 | | fveq2 6771 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (seq1( · ,
𝐺)‘𝑥) = (seq1( · , 𝐺)‘1)) |
14 | 13 | oveq1d 7286 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → ((seq1( · ,
𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁)) |
15 | 12, 14 | eqeq12d 2756 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁))) |
16 | 10 | oveq2d 7287 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘1))) |
17 | 16 | eqeq1d 2742 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1)) |
18 | 15, 17 | anbi12d 631 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1))) |
19 | 8, 18 | imbi12d 345 |
. . . . . . . . 9
⊢ (𝑥 = 1 → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ 1 ≤ (ϕ‘𝑁)) → ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1)))) |
20 | | breq1 5082 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝑥 ≤ (ϕ‘𝑁) ↔ 𝑧 ≤ (ϕ‘𝑁))) |
21 | 20 | anbi2d 629 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁)))) |
22 | | oveq2 7279 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝐴↑𝑥) = (𝐴↑𝑧)) |
23 | | fveq2 6771 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑧)) |
24 | 22, 23 | oveq12d 7289 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧))) |
25 | 24 | oveq1d 7286 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁)) |
26 | | fveq2 6771 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘𝑧)) |
27 | 26 | oveq1d 7286 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → ((seq1( · , 𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁)) |
28 | 25, 27 | eqeq12d 2756 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁))) |
29 | 23 | oveq2d 7287 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘𝑧))) |
30 | 29 | eqeq1d 2742 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)) |
31 | 28, 30 | anbi12d 631 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1))) |
32 | 21, 31 | imbi12d 345 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)))) |
33 | | breq1 5082 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑧 + 1) → (𝑥 ≤ (ϕ‘𝑁) ↔ (𝑧 + 1) ≤ (ϕ‘𝑁))) |
34 | 33 | anbi2d 629 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑧 + 1) → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)))) |
35 | | oveq2 7279 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑧 + 1) → (𝐴↑𝑥) = (𝐴↑(𝑧 + 1))) |
36 | | fveq2 6771 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑧 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑧 + 1))) |
37 | 35, 36 | oveq12d 7289 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑧 + 1) → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1)))) |
38 | 37 | oveq1d 7286 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑧 + 1) → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁)) |
39 | | fveq2 6771 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑧 + 1) → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘(𝑧 + 1))) |
40 | 39 | oveq1d 7286 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑧 + 1) → ((seq1( · , 𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁)) |
41 | 38, 40 | eqeq12d 2756 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑧 + 1) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁))) |
42 | 36 | oveq2d 7287 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑧 + 1) → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1)))) |
43 | 42 | eqeq1d 2742 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑧 + 1) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)) |
44 | 41, 43 | anbi12d 631 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑧 + 1) → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))) |
45 | 34, 44 | imbi12d 345 |
. . . . . . . . 9
⊢ (𝑥 = (𝑧 + 1) → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)))) |
46 | | breq1 5082 |
. . . . . . . . . . 11
⊢ (𝑥 = (ϕ‘𝑁) → (𝑥 ≤ (ϕ‘𝑁) ↔ (ϕ‘𝑁) ≤ (ϕ‘𝑁))) |
47 | 46 | anbi2d 629 |
. . . . . . . . . 10
⊢ (𝑥 = (ϕ‘𝑁) → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)))) |
48 | | oveq2 7279 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (ϕ‘𝑁) → (𝐴↑𝑥) = (𝐴↑(ϕ‘𝑁))) |
49 | | fveq2 6771 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (ϕ‘𝑁) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(ϕ‘𝑁))) |
50 | 48, 49 | oveq12d 7289 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (ϕ‘𝑁) → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁)))) |
51 | 50 | oveq1d 7286 |
. . . . . . . . . . . 12
⊢ (𝑥 = (ϕ‘𝑁) → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁)) |
52 | | fveq2 6771 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (ϕ‘𝑁) → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘(ϕ‘𝑁))) |
53 | 52 | oveq1d 7286 |
. . . . . . . . . . . 12
⊢ (𝑥 = (ϕ‘𝑁) → ((seq1( · ,
𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁)) |
54 | 51, 53 | eqeq12d 2756 |
. . . . . . . . . . 11
⊢ (𝑥 = (ϕ‘𝑁) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁))) |
55 | 49 | oveq2d 7287 |
. . . . . . . . . . . 12
⊢ (𝑥 = (ϕ‘𝑁) → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁)))) |
56 | 55 | eqeq1d 2742 |
. . . . . . . . . . 11
⊢ (𝑥 = (ϕ‘𝑁) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1)) |
57 | 54, 56 | anbi12d 631 |
. . . . . . . . . 10
⊢ (𝑥 = (ϕ‘𝑁) → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1))) |
58 | 47, 57 | imbi12d 345 |
. . . . . . . . 9
⊢ (𝑥 = (ϕ‘𝑁) → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)) → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1)))) |
59 | 1 | simp2d 1142 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℤ) |
60 | | eulerth.4 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐹:𝑇–1-1-onto→𝑆) |
61 | | f1of 6714 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝐹:𝑇⟶𝑆) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹:𝑇⟶𝑆) |
63 | | nnuz 12620 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ℕ =
(ℤ≥‘1) |
64 | 3, 63 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (ϕ‘𝑁) ∈
(ℤ≥‘1)) |
65 | | eluzfz1 13262 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((ϕ‘𝑁)
∈ (ℤ≥‘1) → 1 ∈
(1...(ϕ‘𝑁))) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 1 ∈
(1...(ϕ‘𝑁))) |
67 | | eulerth.3 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑇 = (1...(ϕ‘𝑁)) |
68 | 66, 67 | eleqtrrdi 2852 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 1 ∈ 𝑇) |
69 | 62, 68 | ffvelrnd 6959 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐹‘1) ∈ 𝑆) |
70 | | oveq1 7278 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝐹‘1) → (𝑦 gcd 𝑁) = ((𝐹‘1) gcd 𝑁)) |
71 | 70 | eqeq1d 2742 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (𝐹‘1) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘1) gcd 𝑁) = 1)) |
72 | | eulerth.2 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} |
73 | 71, 72 | elrab2 3629 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘1) ∈ 𝑆 ↔ ((𝐹‘1) ∈ (0..^𝑁) ∧ ((𝐹‘1) gcd 𝑁) = 1)) |
74 | 69, 73 | sylib 217 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐹‘1) ∈ (0..^𝑁) ∧ ((𝐹‘1) gcd 𝑁) = 1)) |
75 | 74 | simpld 495 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹‘1) ∈ (0..^𝑁)) |
76 | | elfzoelz 13386 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘1) ∈ (0..^𝑁) → (𝐹‘1) ∈ ℤ) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹‘1) ∈ ℤ) |
78 | 59, 77 | zmulcld 12431 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℤ) |
79 | 78 | zred 12425 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℝ) |
80 | 2 | nnrpd 12769 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
81 | | modabs2 13623 |
. . . . . . . . . . . . 13
⊢ (((𝐴 · (𝐹‘1)) ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
82 | 79, 80, 81 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
83 | | 1z 12350 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℤ |
84 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 1 → (𝐹‘𝑥) = (𝐹‘1)) |
85 | 84 | oveq2d 7287 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 1 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘1))) |
86 | 85 | oveq1d 7286 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 1 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
87 | | eulerth.5 |
. . . . . . . . . . . . . . . 16
⊢ 𝐺 = (𝑥 ∈ 𝑇 ↦ ((𝐴 · (𝐹‘𝑥)) mod 𝑁)) |
88 | | ovex 7304 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ V |
89 | 86, 87, 88 | fvmpt 6872 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
𝑇 → (𝐺‘1) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
90 | 68, 89 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐺‘1) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
91 | 83, 90 | seq1i 13733 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (seq1( · , 𝐺)‘1) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
92 | 91 | oveq1d 7286 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((seq1( · , 𝐺)‘1) mod 𝑁) = (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁)) |
93 | 59 | zcnd 12426 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℂ) |
94 | 93 | exp1d 13857 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴↑1) = 𝐴) |
95 | | seq1 13732 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℤ → (seq1( · , 𝐹)‘1) = (𝐹‘1)) |
96 | 83, 95 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (seq1(
· , 𝐹)‘1) =
(𝐹‘1) |
97 | 96 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (seq1( · , 𝐹)‘1) = (𝐹‘1)) |
98 | 94, 97 | oveq12d 7289 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴↑1) · (seq1( · , 𝐹)‘1)) = (𝐴 · (𝐹‘1))) |
99 | 98 | oveq1d 7286 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
100 | 82, 92, 99 | 3eqtr4rd 2791 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁)) |
101 | 96 | oveq2i 7282 |
. . . . . . . . . . . 12
⊢ (𝑁 gcd (seq1( · , 𝐹)‘1)) = (𝑁 gcd (𝐹‘1)) |
102 | 2 | nnzd 12424 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℤ) |
103 | 102, 77 | gcdcomd 16219 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 gcd (𝐹‘1)) = ((𝐹‘1) gcd 𝑁)) |
104 | 74 | simprd 496 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹‘1) gcd 𝑁) = 1) |
105 | 103, 104 | eqtrd 2780 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 gcd (𝐹‘1)) = 1) |
106 | 101, 105 | eqtrid 2792 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1) |
107 | 100, 106 | jca 512 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1)) |
108 | 107 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 1 ≤ (ϕ‘𝑁)) → ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1)) |
109 | | nnre 11980 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℝ) |
110 | 109 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → 𝑧 ∈ ℝ) |
111 | 110 | lep1d 11906 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → 𝑧 ≤ (𝑧 + 1)) |
112 | | peano2re 11148 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℝ → (𝑧 + 1) ∈
ℝ) |
113 | 110, 112 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → (𝑧 + 1) ∈ ℝ) |
114 | 4 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → (ϕ‘𝑁) ∈
ℝ) |
115 | | letr 11069 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℝ ∧ (𝑧 + 1) ∈ ℝ ∧
(ϕ‘𝑁) ∈
ℝ) → ((𝑧 ≤
(𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → 𝑧 ≤ (ϕ‘𝑁))) |
116 | 110, 113,
114, 115 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → ((𝑧 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → 𝑧 ≤ (ϕ‘𝑁))) |
117 | 111, 116 | mpand 692 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → ((𝑧 + 1) ≤ (ϕ‘𝑁) → 𝑧 ≤ (ϕ‘𝑁))) |
118 | 117 | imdistanda 572 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ → ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → (𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁)))) |
119 | 118 | imim1d 82 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℕ → (((𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)) → ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)))) |
120 | 59 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝐴 ∈ ℤ) |
121 | | nnnn0 12240 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℕ0) |
122 | 121 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℕ0) |
123 | | zexpcl 13795 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℤ ∧ 𝑧 ∈ ℕ0)
→ (𝐴↑𝑧) ∈
ℤ) |
124 | 120, 122,
123 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴↑𝑧) ∈ ℤ) |
125 | | simprl 768 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℕ) |
126 | 125, 63 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈
(ℤ≥‘1)) |
127 | 109 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℝ) |
128 | 127, 112 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ ℝ) |
129 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (ϕ‘𝑁) ∈ ℝ) |
130 | 127 | lep1d 11906 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ≤ (𝑧 + 1)) |
131 | | simprr 770 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ≤ (ϕ‘𝑁)) |
132 | 127, 128,
129, 130, 131 | letrd 11132 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ≤ (ϕ‘𝑁)) |
133 | | nnz 12342 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℤ) |
134 | 133 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℤ) |
135 | 3 | nnzd 12424 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℤ) |
136 | 135 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (ϕ‘𝑁) ∈ ℤ) |
137 | | eluz 12595 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ ℤ ∧
(ϕ‘𝑁) ∈
ℤ) → ((ϕ‘𝑁) ∈ (ℤ≥‘𝑧) ↔ 𝑧 ≤ (ϕ‘𝑁))) |
138 | 134, 136,
137 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((ϕ‘𝑁) ∈ (ℤ≥‘𝑧) ↔ 𝑧 ≤ (ϕ‘𝑁))) |
139 | 132, 138 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (ϕ‘𝑁) ∈ (ℤ≥‘𝑧)) |
140 | | fzss2 13295 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((ϕ‘𝑁)
∈ (ℤ≥‘𝑧) → (1...𝑧) ⊆ (1...(ϕ‘𝑁))) |
141 | 139, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (1...𝑧) ⊆ (1...(ϕ‘𝑁))) |
142 | 141, 67 | sseqtrrdi 3977 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (1...𝑧) ⊆ 𝑇) |
143 | 142 | sselda 3926 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑧)) → 𝑥 ∈ 𝑇) |
144 | 62 | ffvelrnda 6958 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ 𝑆) |
145 | | oveq1 7278 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = (𝐹‘𝑥) → (𝑦 gcd 𝑁) = ((𝐹‘𝑥) gcd 𝑁)) |
146 | 145 | eqeq1d 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = (𝐹‘𝑥) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘𝑥) gcd 𝑁) = 1)) |
147 | 146, 72 | elrab2 3629 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹‘𝑥) ∈ 𝑆 ↔ ((𝐹‘𝑥) ∈ (0..^𝑁) ∧ ((𝐹‘𝑥) gcd 𝑁) = 1)) |
148 | 144, 147 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → ((𝐹‘𝑥) ∈ (0..^𝑁) ∧ ((𝐹‘𝑥) gcd 𝑁) = 1)) |
149 | 148 | simpld 495 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ (0..^𝑁)) |
150 | | elfzoelz 13386 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘𝑥) ∈ (0..^𝑁) → (𝐹‘𝑥) ∈ ℤ) |
151 | 149, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ ℤ) |
152 | 151 | adantlr 712 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ ℤ) |
153 | 143, 152 | syldan 591 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑧)) → (𝐹‘𝑥) ∈ ℤ) |
154 | | zmulcl 12369 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 · 𝑦) ∈ ℤ) |
155 | 154 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 · 𝑦) ∈ ℤ) |
156 | 126, 153,
155 | seqcl 13741 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐹)‘𝑧) ∈ ℤ) |
157 | 124, 156 | zmulcld 12431 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) ∈ ℤ) |
158 | 157 | zred 12425 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) ∈ ℝ) |
159 | 72 | ssrab3 4020 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑆 ⊆ (0..^𝑁) |
160 | 1, 72, 67, 60, 87 | eulerthlem1 16480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐺:𝑇⟶𝑆) |
161 | 160 | ffvelrnda 6958 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ 𝑆) |
162 | 159, 161 | sselid 3924 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ (0..^𝑁)) |
163 | | elfzoelz 13386 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺‘𝑥) ∈ (0..^𝑁) → (𝐺‘𝑥) ∈ ℤ) |
164 | 162, 163 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ ℤ) |
165 | 164 | adantlr 712 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ ℤ) |
166 | 143, 165 | syldan 591 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑧)) → (𝐺‘𝑥) ∈ ℤ) |
167 | 126, 166,
155 | seqcl 13741 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘𝑧) ∈ ℤ) |
168 | 167 | zred 12425 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘𝑧) ∈ ℝ) |
169 | 62 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝐹:𝑇⟶𝑆) |
170 | | peano2nn 11985 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ ℕ → (𝑧 + 1) ∈
ℕ) |
171 | 170 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ ℕ) |
172 | 171 | nnge1d 12021 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 1 ≤ (𝑧 + 1)) |
173 | 171 | nnzd 12424 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ ℤ) |
174 | | elfz 13244 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑧 + 1) ∈ ℤ ∧ 1
∈ ℤ ∧ (ϕ‘𝑁) ∈ ℤ) → ((𝑧 + 1) ∈
(1...(ϕ‘𝑁))
↔ (1 ≤ (𝑧 + 1)
∧ (𝑧 + 1) ≤
(ϕ‘𝑁)))) |
175 | 83, 174 | mp3an2 1448 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑧 + 1) ∈ ℤ ∧
(ϕ‘𝑁) ∈
ℤ) → ((𝑧 + 1)
∈ (1...(ϕ‘𝑁)) ↔ (1 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)))) |
176 | 173, 136,
175 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑧 + 1) ∈ (1...(ϕ‘𝑁)) ↔ (1 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)))) |
177 | 172, 131,
176 | mpbir2and 710 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ (1...(ϕ‘𝑁))) |
178 | 177, 67 | eleqtrrdi 2852 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ 𝑇) |
179 | 169, 178 | ffvelrnd 6959 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ 𝑆) |
180 | | oveq1 7278 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (𝐹‘(𝑧 + 1)) → (𝑦 gcd 𝑁) = ((𝐹‘(𝑧 + 1)) gcd 𝑁)) |
181 | 180 | eqeq1d 2742 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = (𝐹‘(𝑧 + 1)) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1)) |
182 | 181, 72 | elrab2 3629 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘(𝑧 + 1)) ∈ 𝑆 ↔ ((𝐹‘(𝑧 + 1)) ∈ (0..^𝑁) ∧ ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1)) |
183 | 179, 182 | sylib 217 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐹‘(𝑧 + 1)) ∈ (0..^𝑁) ∧ ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1)) |
184 | 183 | simpld 495 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ (0..^𝑁)) |
185 | | elfzoelz 13386 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘(𝑧 + 1)) ∈ (0..^𝑁) → (𝐹‘(𝑧 + 1)) ∈ ℤ) |
186 | 184, 185 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ ℤ) |
187 | 120, 186 | zmulcld 12431 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℤ) |
188 | 80 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑁 ∈
ℝ+) |
189 | | modmul1 13642 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴↑𝑧) · (seq1( · ,
𝐹)‘𝑧)) ∈ ℝ ∧ (seq1( · ,
𝐺)‘𝑧) ∈ ℝ) ∧ ((𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℤ ∧ 𝑁 ∈ ℝ+)
∧ (((𝐴↑𝑧) · (seq1( · ,
𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁)) |
190 | 189 | 3expia 1120 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴↑𝑧) · (seq1( · ,
𝐹)‘𝑧)) ∈ ℝ ∧ (seq1( · ,
𝐺)‘𝑧) ∈ ℝ) ∧ ((𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℤ ∧ 𝑁 ∈ ℝ+))
→ ((((𝐴↑𝑧) · (seq1( · ,
𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁))) |
191 | 158, 168,
187, 188, 190 | syl22anc 836 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁))) |
192 | 124 | zcnd 12426 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴↑𝑧) ∈ ℂ) |
193 | 156 | zcnd 12426 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐹)‘𝑧) ∈ ℂ) |
194 | 93 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝐴 ∈ ℂ) |
195 | 186 | zcnd 12426 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ ℂ) |
196 | 192, 193,
194, 195 | mul4d 11187 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) = (((𝐴↑𝑧) · 𝐴) · ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1))))) |
197 | 194, 122 | expp1d 13863 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴↑(𝑧 + 1)) = ((𝐴↑𝑧) · 𝐴)) |
198 | | seqp1 13734 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈
(ℤ≥‘1) → (seq1( · , 𝐹)‘(𝑧 + 1)) = ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) |
199 | 126, 198 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐹)‘(𝑧 + 1)) = ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) |
200 | 197, 199 | oveq12d 7289 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) = (((𝐴↑𝑧) · 𝐴) · ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1))))) |
201 | 196, 200 | eqtr4d 2783 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) = ((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1)))) |
202 | 201 | oveq1d 7286 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁)) |
203 | 187 | zred 12425 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℝ) |
204 | 203, 188 | modcld 13593 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) ∈ ℝ) |
205 | | modabs2 13623 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)) |
206 | 203, 188,
205 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)) |
207 | | modmul1 13642 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ·
(𝐹‘(𝑧 + 1))) mod 𝑁) ∈ ℝ ∧ (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℝ) ∧ ((seq1(
· , 𝐺)‘𝑧) ∈ ℤ ∧ 𝑁 ∈ ℝ+)
∧ (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)) → ((((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁)) |
208 | 204, 203,
167, 188, 206, 207 | syl221anc 1380 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁)) |
209 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = (𝑧 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑧 + 1))) |
210 | 209 | oveq2d 7287 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = (𝑧 + 1) → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘(𝑧 + 1)))) |
211 | 210 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = (𝑧 + 1) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)) |
212 | | ovex 7304 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) ∈ V |
213 | 211, 87, 212 | fvmpt 6872 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 + 1) ∈ 𝑇 → (𝐺‘(𝑧 + 1)) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)) |
214 | 178, 213 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐺‘(𝑧 + 1)) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)) |
215 | 214 | oveq2d 7287 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((seq1( · , 𝐺)‘𝑧) · (𝐺‘(𝑧 + 1))) = ((seq1( · , 𝐺)‘𝑧) · ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))) |
216 | | seqp1 13734 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈
(ℤ≥‘1) → (seq1( · , 𝐺)‘(𝑧 + 1)) = ((seq1( · , 𝐺)‘𝑧) · (𝐺‘(𝑧 + 1)))) |
217 | 126, 216 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘(𝑧 + 1)) = ((seq1( · , 𝐺)‘𝑧) · (𝐺‘(𝑧 + 1)))) |
218 | 204 | recnd 11004 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) ∈ ℂ) |
219 | 167 | zcnd 12426 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘𝑧) ∈ ℂ) |
220 | 218, 219 | mulcomd 10997 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) = ((seq1( · , 𝐺)‘𝑧) · ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))) |
221 | 215, 217,
220 | 3eqtr4d 2790 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘(𝑧 + 1)) = (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧))) |
222 | 221 | oveq1d 7286 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) = ((((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁)) |
223 | 187 | zcnd 12426 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℂ) |
224 | 219, 223 | mulcomd 10997 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) = ((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧))) |
225 | 224 | oveq1d 7286 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁)) |
226 | 208, 222,
225 | 3eqtr4rd 2791 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁)) |
227 | 202, 226 | eqeq12d 2756 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) ↔ (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁))) |
228 | 191, 227 | sylibd 238 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) → (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁))) |
229 | 102 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑁 ∈ ℤ) |
230 | 229, 186 | gcdcomd 16219 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑁 gcd (𝐹‘(𝑧 + 1))) = ((𝐹‘(𝑧 + 1)) gcd 𝑁)) |
231 | 183 | simprd 496 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1) |
232 | 230, 231 | eqtrd 2780 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑁 gcd (𝐹‘(𝑧 + 1))) = 1) |
233 | | rpmul 16362 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧ (seq1(
· , 𝐹)‘𝑧) ∈ ℤ ∧ (𝐹‘(𝑧 + 1)) ∈ ℤ) → (((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 ∧ (𝑁 gcd (𝐹‘(𝑧 + 1))) = 1) → (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1)) |
234 | 229, 156,
186, 233 | syl3anc 1370 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 ∧ (𝑁 gcd (𝐹‘(𝑧 + 1))) = 1) → (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1)) |
235 | 232, 234 | mpan2d 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 → (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1)) |
236 | 199 | oveq2d 7287 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1))))) |
237 | 236 | eqeq1d 2742 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1 ↔ (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1)) |
238 | 235, 237 | sylibrd 258 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 → (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)) |
239 | 228, 238 | anim12d 609 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))) |
240 | 239 | an12s 646 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℕ ∧ (𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))) |
241 | 240 | ex 413 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ → ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)))) |
242 | 241 | a2d 29 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℕ → (((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)) → ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)))) |
243 | 119, 242 | syld 47 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℕ → (((𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)) → ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)))) |
244 | 19, 32, 45, 58, 108, 243 | nnind 11991 |
. . . . . . . 8
⊢
((ϕ‘𝑁)
∈ ℕ → ((𝜑
∧ (ϕ‘𝑁) ≤
(ϕ‘𝑁)) →
((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1))) |
245 | 6, 244 | mpcom 38 |
. . . . . . 7
⊢ ((𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)) → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1)) |
246 | 5, 245 | mpdan 684 |
. . . . . 6
⊢ (𝜑 → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1)) |
247 | 246 | simpld 495 |
. . . . 5
⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁)) |
248 | 3 | nnnn0d 12293 |
. . . . . . . 8
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℕ0) |
249 | | zexpcl 13795 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧
(ϕ‘𝑁) ∈
ℕ0) → (𝐴↑(ϕ‘𝑁)) ∈ ℤ) |
250 | 59, 248, 249 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐴↑(ϕ‘𝑁)) ∈ ℤ) |
251 | 67 | eleq2i 2832 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑇 ↔ 𝑥 ∈ (1...(ϕ‘𝑁))) |
252 | 251, 151 | sylan2br 595 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(ϕ‘𝑁))) → (𝐹‘𝑥) ∈ ℤ) |
253 | 154 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 · 𝑦) ∈ ℤ) |
254 | 64, 252, 253 | seqcl 13741 |
. . . . . . 7
⊢ (𝜑 → (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈
ℤ) |
255 | 250, 254 | zmulcld 12431 |
. . . . . 6
⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) ∈
ℤ) |
256 | | mulcl 10956 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
257 | 256 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ) |
258 | | mulcom 10958 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) |
259 | 258 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) |
260 | | mulass 10960 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) |
261 | 260 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) |
262 | | ssidd 3949 |
. . . . . . . 8
⊢ (𝜑 → ℂ ⊆
ℂ) |
263 | | f1ocnv 6726 |
. . . . . . . . . . 11
⊢ (𝐹:𝑇–1-1-onto→𝑆 → ◡𝐹:𝑆–1-1-onto→𝑇) |
264 | 60, 263 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ◡𝐹:𝑆–1-1-onto→𝑇) |
265 | 2 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑁 ∈ ℕ) |
266 | 59 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝐴 ∈ ℤ) |
267 | 62 | ffvelrnda 6958 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑇) → (𝐹‘𝑦) ∈ 𝑆) |
268 | 267 | adantrr 714 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ 𝑆) |
269 | 159, 268 | sselid 3924 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ (0..^𝑁)) |
270 | | elfzoelz 13386 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑦) ∈ (0..^𝑁) → (𝐹‘𝑦) ∈ ℤ) |
271 | 269, 270 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ ℤ) |
272 | 266, 271 | zmulcld 12431 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐴 · (𝐹‘𝑦)) ∈ ℤ) |
273 | 62 | ffvelrnda 6958 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑇) → (𝐹‘𝑧) ∈ 𝑆) |
274 | 273 | adantrl 713 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ 𝑆) |
275 | 159, 274 | sselid 3924 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ (0..^𝑁)) |
276 | | elfzoelz 13386 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑧) ∈ (0..^𝑁) → (𝐹‘𝑧) ∈ ℤ) |
277 | 275, 276 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ ℤ) |
278 | 266, 277 | zmulcld 12431 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐴 · (𝐹‘𝑧)) ∈ ℤ) |
279 | | moddvds 15972 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 · (𝐹‘𝑦)) ∈ ℤ ∧ (𝐴 · (𝐹‘𝑧)) ∈ ℤ) → (((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁) ↔ 𝑁 ∥ ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧))))) |
280 | 265, 272,
278, 279 | syl3anc 1370 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁) ↔ 𝑁 ∥ ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧))))) |
281 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
282 | 281 | oveq2d 7287 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘𝑦))) |
283 | 282 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘𝑦)) mod 𝑁)) |
284 | | ovex 7304 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 · (𝐹‘𝑦)) mod 𝑁) ∈ V |
285 | 283, 87, 284 | fvmpt 6872 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝑇 → (𝐺‘𝑦) = ((𝐴 · (𝐹‘𝑦)) mod 𝑁)) |
286 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
287 | 286 | oveq2d 7287 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑧 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘𝑧))) |
288 | 287 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑧 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁)) |
289 | | ovex 7304 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 · (𝐹‘𝑧)) mod 𝑁) ∈ V |
290 | 288, 87, 289 | fvmpt 6872 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑇 → (𝐺‘𝑧) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁)) |
291 | 285, 290 | eqeqan12d 2754 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇) → ((𝐺‘𝑦) = (𝐺‘𝑧) ↔ ((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁))) |
292 | 291 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐺‘𝑦) = (𝐺‘𝑧) ↔ ((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁))) |
293 | 93 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝐴 ∈ ℂ) |
294 | 271 | zcnd 12426 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ ℂ) |
295 | 277 | zcnd 12426 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ ℂ) |
296 | 293, 294,
295 | subdid 11431 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) = ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧)))) |
297 | 296 | breq2d 5091 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ↔ 𝑁 ∥ ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧))))) |
298 | 280, 292,
297 | 3bitr4d 311 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐺‘𝑦) = (𝐺‘𝑧) ↔ 𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))))) |
299 | 102, 59 | gcdcomd 16219 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 gcd 𝐴) = (𝐴 gcd 𝑁)) |
300 | 1 | simp3d 1143 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 gcd 𝑁) = 1) |
301 | 299, 300 | eqtrd 2780 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 gcd 𝐴) = 1) |
302 | 301 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 gcd 𝐴) = 1) |
303 | 102 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑁 ∈ ℤ) |
304 | 271, 277 | zsubcld 12430 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) − (𝐹‘𝑧)) ∈ ℤ) |
305 | | coprmdvds 16356 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ((𝐹‘𝑦) − (𝐹‘𝑧)) ∈ ℤ) → ((𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ∧ (𝑁 gcd 𝐴) = 1) → 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧)))) |
306 | 303, 266,
304, 305 | syl3anc 1370 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ∧ (𝑁 gcd 𝐴) = 1) → 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧)))) |
307 | 271 | zred 12425 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ ℝ) |
308 | 80 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑁 ∈
ℝ+) |
309 | | elfzole1 13394 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑦) ∈ (0..^𝑁) → 0 ≤ (𝐹‘𝑦)) |
310 | 269, 309 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 0 ≤ (𝐹‘𝑦)) |
311 | | elfzolt2 13395 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑦) ∈ (0..^𝑁) → (𝐹‘𝑦) < 𝑁) |
312 | 269, 311 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) < 𝑁) |
313 | | modid 13614 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑦) ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (0 ≤
(𝐹‘𝑦) ∧ (𝐹‘𝑦) < 𝑁)) → ((𝐹‘𝑦) mod 𝑁) = (𝐹‘𝑦)) |
314 | 307, 308,
310, 312, 313 | syl22anc 836 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) mod 𝑁) = (𝐹‘𝑦)) |
315 | 277 | zred 12425 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ ℝ) |
316 | | elfzole1 13394 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑧) ∈ (0..^𝑁) → 0 ≤ (𝐹‘𝑧)) |
317 | 275, 316 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 0 ≤ (𝐹‘𝑧)) |
318 | | elfzolt2 13395 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑧) ∈ (0..^𝑁) → (𝐹‘𝑧) < 𝑁) |
319 | 275, 318 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) < 𝑁) |
320 | | modid 13614 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑧) ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (0 ≤
(𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑁)) → ((𝐹‘𝑧) mod 𝑁) = (𝐹‘𝑧)) |
321 | 315, 308,
317, 319, 320 | syl22anc 836 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑧) mod 𝑁) = (𝐹‘𝑧)) |
322 | 314, 321 | eqeq12d 2756 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((𝐹‘𝑦) mod 𝑁) = ((𝐹‘𝑧) mod 𝑁) ↔ (𝐹‘𝑦) = (𝐹‘𝑧))) |
323 | | moddvds 15972 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ (𝐹‘𝑦) ∈ ℤ ∧ (𝐹‘𝑧) ∈ ℤ) → (((𝐹‘𝑦) mod 𝑁) = ((𝐹‘𝑧) mod 𝑁) ↔ 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧)))) |
324 | 265, 271,
277, 323 | syl3anc 1370 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((𝐹‘𝑦) mod 𝑁) = ((𝐹‘𝑧) mod 𝑁) ↔ 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧)))) |
325 | | f1of1 6713 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝐹:𝑇–1-1→𝑆) |
326 | 60, 325 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹:𝑇–1-1→𝑆) |
327 | | f1fveq 7132 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝑇–1-1→𝑆 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ 𝑦 = 𝑧)) |
328 | 326, 327 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ 𝑦 = 𝑧)) |
329 | 322, 324,
328 | 3bitr3d 309 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧)) ↔ 𝑦 = 𝑧)) |
330 | 306, 329 | sylibd 238 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ∧ (𝑁 gcd 𝐴) = 1) → 𝑦 = 𝑧)) |
331 | 302, 330 | mpan2d 691 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) → 𝑦 = 𝑧)) |
332 | 298, 331 | sylbid 239 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐺‘𝑦) = (𝐺‘𝑧) → 𝑦 = 𝑧)) |
333 | 332 | ralrimivva 3117 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑦 ∈ 𝑇 ∀𝑧 ∈ 𝑇 ((𝐺‘𝑦) = (𝐺‘𝑧) → 𝑦 = 𝑧)) |
334 | | dff13 7125 |
. . . . . . . . . . . 12
⊢ (𝐺:𝑇–1-1→𝑆 ↔ (𝐺:𝑇⟶𝑆 ∧ ∀𝑦 ∈ 𝑇 ∀𝑧 ∈ 𝑇 ((𝐺‘𝑦) = (𝐺‘𝑧) → 𝑦 = 𝑧))) |
335 | 160, 333,
334 | sylanbrc 583 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺:𝑇–1-1→𝑆) |
336 | 67 | ovexi 7305 |
. . . . . . . . . . . . . 14
⊢ 𝑇 ∈ V |
337 | 336 | f1oen 8744 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝑇 ≈ 𝑆) |
338 | 60, 337 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ≈ 𝑆) |
339 | | fzofi 13692 |
. . . . . . . . . . . . 13
⊢
(0..^𝑁) ∈
Fin |
340 | | ssfi 8938 |
. . . . . . . . . . . . 13
⊢
(((0..^𝑁) ∈ Fin
∧ 𝑆 ⊆ (0..^𝑁)) → 𝑆 ∈ Fin) |
341 | 339, 159,
340 | mp2an 689 |
. . . . . . . . . . . 12
⊢ 𝑆 ∈ Fin |
342 | | f1finf1o 9024 |
. . . . . . . . . . . 12
⊢ ((𝑇 ≈ 𝑆 ∧ 𝑆 ∈ Fin) → (𝐺:𝑇–1-1→𝑆 ↔ 𝐺:𝑇–1-1-onto→𝑆)) |
343 | 338, 341,
342 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺:𝑇–1-1→𝑆 ↔ 𝐺:𝑇–1-1-onto→𝑆)) |
344 | 335, 343 | mpbid 231 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:𝑇–1-1-onto→𝑆) |
345 | | f1oco 6736 |
. . . . . . . . . 10
⊢ ((◡𝐹:𝑆–1-1-onto→𝑇 ∧ 𝐺:𝑇–1-1-onto→𝑆) → (◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇) |
346 | 264, 344,
345 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇) |
347 | | f1oeq23 6705 |
. . . . . . . . . 10
⊢ ((𝑇 = (1...(ϕ‘𝑁)) ∧ 𝑇 = (1...(ϕ‘𝑁))) → ((◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇 ↔ (◡𝐹 ∘ 𝐺):(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁)))) |
348 | 67, 67, 347 | mp2an 689 |
. . . . . . . . 9
⊢ ((◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇 ↔ (◡𝐹 ∘ 𝐺):(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁))) |
349 | 346, 348 | sylib 217 |
. . . . . . . 8
⊢ (𝜑 → (◡𝐹 ∘ 𝐺):(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁))) |
350 | 252 | zcnd 12426 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(ϕ‘𝑁))) → (𝐹‘𝑥) ∈ ℂ) |
351 | 67 | eleq2i 2832 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝑇 ↔ 𝑤 ∈ (1...(ϕ‘𝑁))) |
352 | | fvco3 6864 |
. . . . . . . . . . . 12
⊢ ((𝐺:𝑇⟶𝑆 ∧ 𝑤 ∈ 𝑇) → ((◡𝐹 ∘ 𝐺)‘𝑤) = (◡𝐹‘(𝐺‘𝑤))) |
353 | 160, 352 | sylan 580 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((◡𝐹 ∘ 𝐺)‘𝑤) = (◡𝐹‘(𝐺‘𝑤))) |
354 | 353 | fveq2d 6775 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐹‘((◡𝐹 ∘ 𝐺)‘𝑤)) = (𝐹‘(◡𝐹‘(𝐺‘𝑤)))) |
355 | 60 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝐹:𝑇–1-1-onto→𝑆) |
356 | 160 | ffvelrnda 6958 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐺‘𝑤) ∈ 𝑆) |
357 | | f1ocnvfv2 7146 |
. . . . . . . . . . 11
⊢ ((𝐹:𝑇–1-1-onto→𝑆 ∧ (𝐺‘𝑤) ∈ 𝑆) → (𝐹‘(◡𝐹‘(𝐺‘𝑤))) = (𝐺‘𝑤)) |
358 | 355, 356,
357 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐹‘(◡𝐹‘(𝐺‘𝑤))) = (𝐺‘𝑤)) |
359 | 354, 358 | eqtr2d 2781 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐺‘𝑤) = (𝐹‘((◡𝐹 ∘ 𝐺)‘𝑤))) |
360 | 351, 359 | sylan2br 595 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (1...(ϕ‘𝑁))) → (𝐺‘𝑤) = (𝐹‘((◡𝐹 ∘ 𝐺)‘𝑤))) |
361 | 257, 259,
261, 64, 262, 349, 350, 360 | seqf1o 13762 |
. . . . . . 7
⊢ (𝜑 → (seq1( · , 𝐺)‘(ϕ‘𝑁)) = (seq1( · , 𝐹)‘(ϕ‘𝑁))) |
362 | 361, 254 | eqeltrd 2841 |
. . . . . 6
⊢ (𝜑 → (seq1( · , 𝐺)‘(ϕ‘𝑁)) ∈
ℤ) |
363 | | moddvds 15972 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴↑(ϕ‘𝑁)) · (seq1( · ,
𝐹)‘(ϕ‘𝑁))) ∈ ℤ ∧ (seq1( · ,
𝐺)‘(ϕ‘𝑁)) ∈ ℤ) → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · ,
𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ↔ 𝑁 ∥ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · ,
𝐺)‘(ϕ‘𝑁))))) |
364 | 2, 255, 362, 363 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ↔ 𝑁 ∥ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · ,
𝐺)‘(ϕ‘𝑁))))) |
365 | 247, 364 | mpbid 231 |
. . . 4
⊢ (𝜑 → 𝑁 ∥ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · ,
𝐺)‘(ϕ‘𝑁)))) |
366 | 254 | zcnd 12426 |
. . . . . . . 8
⊢ (𝜑 → (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈
ℂ) |
367 | 366 | mulid2d 10994 |
. . . . . . 7
⊢ (𝜑 → (1 · (seq1(
· , 𝐹)‘(ϕ‘𝑁))) = (seq1( · , 𝐹)‘(ϕ‘𝑁))) |
368 | 361, 367 | eqtr4d 2783 |
. . . . . 6
⊢ (𝜑 → (seq1( · , 𝐺)‘(ϕ‘𝑁)) = (1 · (seq1( ·
, 𝐹)‘(ϕ‘𝑁)))) |
369 | 368 | oveq2d 7287 |
. . . . 5
⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · ,
𝐺)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1(
· , 𝐹)‘(ϕ‘𝑁))))) |
370 | 250 | zcnd 12426 |
. . . . . 6
⊢ (𝜑 → (𝐴↑(ϕ‘𝑁)) ∈ ℂ) |
371 | | ax-1cn 10930 |
. . . . . . 7
⊢ 1 ∈
ℂ |
372 | | subdir 11409 |
. . . . . . 7
⊢ (((𝐴↑(ϕ‘𝑁)) ∈ ℂ ∧ 1 ∈
ℂ ∧ (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈ ℂ) → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1(
· , 𝐹)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1(
· , 𝐹)‘(ϕ‘𝑁))))) |
373 | 371, 372 | mp3an2 1448 |
. . . . . 6
⊢ (((𝐴↑(ϕ‘𝑁)) ∈ ℂ ∧ (seq1(
· , 𝐹)‘(ϕ‘𝑁)) ∈ ℂ) → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1(
· , 𝐹)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1(
· , 𝐹)‘(ϕ‘𝑁))))) |
374 | 370, 366,
373 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1( · ,
𝐹)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1(
· , 𝐹)‘(ϕ‘𝑁))))) |
375 | | zsubcl 12362 |
. . . . . . . 8
⊢ (((𝐴↑(ϕ‘𝑁)) ∈ ℤ ∧ 1 ∈
ℤ) → ((𝐴↑(ϕ‘𝑁)) − 1) ∈
ℤ) |
376 | 250, 83, 375 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) − 1) ∈
ℤ) |
377 | 376 | zcnd 12426 |
. . . . . 6
⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) − 1) ∈
ℂ) |
378 | 377, 366 | mulcomd 10997 |
. . . . 5
⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1( · ,
𝐹)‘(ϕ‘𝑁))) = ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1))) |
379 | 369, 374,
378 | 3eqtr2d 2786 |
. . . 4
⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · ,
𝐺)‘(ϕ‘𝑁))) = ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1))) |
380 | 365, 379 | breqtrd 5105 |
. . 3
⊢ (𝜑 → 𝑁 ∥ ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1))) |
381 | 246 | simprd 496 |
. . 3
⊢ (𝜑 → (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1) |
382 | | coprmdvds 16356 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ (seq1(
· , 𝐹)‘(ϕ‘𝑁)) ∈ ℤ ∧ ((𝐴↑(ϕ‘𝑁)) − 1) ∈ ℤ) → ((𝑁 ∥ ((seq1( · ,
𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1) → 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1))) |
383 | 102, 254,
376, 382 | syl3anc 1370 |
. . 3
⊢ (𝜑 → ((𝑁 ∥ ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1) → 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1))) |
384 | 380, 381,
383 | mp2and 696 |
. 2
⊢ (𝜑 → 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1)) |
385 | | moddvds 15972 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑁)) ∈ ℤ ∧ 1 ∈
ℤ) → (((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1))) |
386 | 83, 385 | mp3an3 1449 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑁)) ∈ ℤ) →
(((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1))) |
387 | 2, 250, 386 | syl2anc 584 |
. 2
⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1))) |
388 | 384, 387 | mpbird 256 |
1
⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁)) |