Step | Hyp | Ref
| Expression |
1 | | eulerth.1 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1)) |
2 | 1 | simp1d 1135 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℕ) |
3 | 2 | phicld 15942 |
. . . . . . . . 9
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℕ) |
4 | 3 | nnred 11507 |
. . . . . . . 8
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℝ) |
5 | 4 | leidd 11060 |
. . . . . . 7
⊢ (𝜑 → (ϕ‘𝑁) ≤ (ϕ‘𝑁)) |
6 | 3 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)) → (ϕ‘𝑁) ∈
ℕ) |
7 | | breq1 4971 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (𝑥 ≤ (ϕ‘𝑁) ↔ 1 ≤ (ϕ‘𝑁))) |
8 | 7 | anbi2d 628 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ 1 ≤ (ϕ‘𝑁)))) |
9 | | oveq2 7031 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → (𝐴↑𝑥) = (𝐴↑1)) |
10 | | fveq2 6545 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → (seq1( · ,
𝐹)‘𝑥) = (seq1( · , 𝐹)‘1)) |
11 | 9, 10 | oveq12d 7041 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑1) · (seq1( · , 𝐹)‘1))) |
12 | 11 | oveq1d 7038 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁)) |
13 | | fveq2 6545 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (seq1( · ,
𝐺)‘𝑥) = (seq1( · , 𝐺)‘1)) |
14 | 13 | oveq1d 7038 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → ((seq1( · ,
𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁)) |
15 | 12, 14 | eqeq12d 2812 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁))) |
16 | 10 | oveq2d 7039 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘1))) |
17 | 16 | eqeq1d 2799 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1)) |
18 | 15, 17 | anbi12d 630 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1))) |
19 | 8, 18 | imbi12d 346 |
. . . . . . . . 9
⊢ (𝑥 = 1 → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ 1 ≤ (ϕ‘𝑁)) → ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1)))) |
20 | | breq1 4971 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝑥 ≤ (ϕ‘𝑁) ↔ 𝑧 ≤ (ϕ‘𝑁))) |
21 | 20 | anbi2d 628 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁)))) |
22 | | oveq2 7031 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝐴↑𝑥) = (𝐴↑𝑧)) |
23 | | fveq2 6545 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑧)) |
24 | 22, 23 | oveq12d 7041 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧))) |
25 | 24 | oveq1d 7038 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁)) |
26 | | fveq2 6545 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘𝑧)) |
27 | 26 | oveq1d 7038 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → ((seq1( · , 𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁)) |
28 | 25, 27 | eqeq12d 2812 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁))) |
29 | 23 | oveq2d 7039 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘𝑧))) |
30 | 29 | eqeq1d 2799 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)) |
31 | 28, 30 | anbi12d 630 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1))) |
32 | 21, 31 | imbi12d 346 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)))) |
33 | | breq1 4971 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑧 + 1) → (𝑥 ≤ (ϕ‘𝑁) ↔ (𝑧 + 1) ≤ (ϕ‘𝑁))) |
34 | 33 | anbi2d 628 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑧 + 1) → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)))) |
35 | | oveq2 7031 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑧 + 1) → (𝐴↑𝑥) = (𝐴↑(𝑧 + 1))) |
36 | | fveq2 6545 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑧 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑧 + 1))) |
37 | 35, 36 | oveq12d 7041 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑧 + 1) → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1)))) |
38 | 37 | oveq1d 7038 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑧 + 1) → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁)) |
39 | | fveq2 6545 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑧 + 1) → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘(𝑧 + 1))) |
40 | 39 | oveq1d 7038 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑧 + 1) → ((seq1( · , 𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁)) |
41 | 38, 40 | eqeq12d 2812 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑧 + 1) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁))) |
42 | 36 | oveq2d 7039 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑧 + 1) → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1)))) |
43 | 42 | eqeq1d 2799 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑧 + 1) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)) |
44 | 41, 43 | anbi12d 630 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑧 + 1) → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))) |
45 | 34, 44 | imbi12d 346 |
. . . . . . . . 9
⊢ (𝑥 = (𝑧 + 1) → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)))) |
46 | | breq1 4971 |
. . . . . . . . . . 11
⊢ (𝑥 = (ϕ‘𝑁) → (𝑥 ≤ (ϕ‘𝑁) ↔ (ϕ‘𝑁) ≤ (ϕ‘𝑁))) |
47 | 46 | anbi2d 628 |
. . . . . . . . . 10
⊢ (𝑥 = (ϕ‘𝑁) → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)))) |
48 | | oveq2 7031 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (ϕ‘𝑁) → (𝐴↑𝑥) = (𝐴↑(ϕ‘𝑁))) |
49 | | fveq2 6545 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (ϕ‘𝑁) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(ϕ‘𝑁))) |
50 | 48, 49 | oveq12d 7041 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (ϕ‘𝑁) → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁)))) |
51 | 50 | oveq1d 7038 |
. . . . . . . . . . . 12
⊢ (𝑥 = (ϕ‘𝑁) → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁)) |
52 | | fveq2 6545 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (ϕ‘𝑁) → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘(ϕ‘𝑁))) |
53 | 52 | oveq1d 7038 |
. . . . . . . . . . . 12
⊢ (𝑥 = (ϕ‘𝑁) → ((seq1( · ,
𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁)) |
54 | 51, 53 | eqeq12d 2812 |
. . . . . . . . . . 11
⊢ (𝑥 = (ϕ‘𝑁) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁))) |
55 | 49 | oveq2d 7039 |
. . . . . . . . . . . 12
⊢ (𝑥 = (ϕ‘𝑁) → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁)))) |
56 | 55 | eqeq1d 2799 |
. . . . . . . . . . 11
⊢ (𝑥 = (ϕ‘𝑁) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1)) |
57 | 54, 56 | anbi12d 630 |
. . . . . . . . . 10
⊢ (𝑥 = (ϕ‘𝑁) → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1))) |
58 | 47, 57 | imbi12d 346 |
. . . . . . . . 9
⊢ (𝑥 = (ϕ‘𝑁) → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)) → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1)))) |
59 | 1 | simp2d 1136 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℤ) |
60 | | eulerth.4 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐹:𝑇–1-1-onto→𝑆) |
61 | | f1of 6490 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝐹:𝑇⟶𝑆) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹:𝑇⟶𝑆) |
63 | | nnuz 12134 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ℕ =
(ℤ≥‘1) |
64 | 3, 63 | syl6eleq 2895 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (ϕ‘𝑁) ∈
(ℤ≥‘1)) |
65 | | eluzfz1 12768 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((ϕ‘𝑁)
∈ (ℤ≥‘1) → 1 ∈
(1...(ϕ‘𝑁))) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 1 ∈
(1...(ϕ‘𝑁))) |
67 | | eulerth.3 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑇 = (1...(ϕ‘𝑁)) |
68 | 66, 67 | syl6eleqr 2896 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 1 ∈ 𝑇) |
69 | 62, 68 | ffvelrnd 6724 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐹‘1) ∈ 𝑆) |
70 | | oveq1 7030 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝐹‘1) → (𝑦 gcd 𝑁) = ((𝐹‘1) gcd 𝑁)) |
71 | 70 | eqeq1d 2799 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (𝐹‘1) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘1) gcd 𝑁) = 1)) |
72 | | eulerth.2 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} |
73 | 71, 72 | elrab2 3624 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘1) ∈ 𝑆 ↔ ((𝐹‘1) ∈ (0..^𝑁) ∧ ((𝐹‘1) gcd 𝑁) = 1)) |
74 | 69, 73 | sylib 219 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐹‘1) ∈ (0..^𝑁) ∧ ((𝐹‘1) gcd 𝑁) = 1)) |
75 | 74 | simpld 495 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹‘1) ∈ (0..^𝑁)) |
76 | | elfzoelz 12892 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘1) ∈ (0..^𝑁) → (𝐹‘1) ∈ ℤ) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹‘1) ∈ ℤ) |
78 | 59, 77 | zmulcld 11947 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℤ) |
79 | 78 | zred 11941 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℝ) |
80 | 2 | nnrpd 12283 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
81 | | modabs2 13127 |
. . . . . . . . . . . . 13
⊢ (((𝐴 · (𝐹‘1)) ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
82 | 79, 80, 81 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
83 | | 1z 11866 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℤ |
84 | | fveq2 6545 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 1 → (𝐹‘𝑥) = (𝐹‘1)) |
85 | 84 | oveq2d 7039 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 1 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘1))) |
86 | 85 | oveq1d 7038 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 1 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
87 | | eulerth.5 |
. . . . . . . . . . . . . . . 16
⊢ 𝐺 = (𝑥 ∈ 𝑇 ↦ ((𝐴 · (𝐹‘𝑥)) mod 𝑁)) |
88 | | ovex 7055 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ V |
89 | 86, 87, 88 | fvmpt 6642 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
𝑇 → (𝐺‘1) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
90 | 68, 89 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐺‘1) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
91 | 83, 90 | seq1i 13237 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (seq1( · , 𝐺)‘1) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
92 | 91 | oveq1d 7038 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((seq1( · , 𝐺)‘1) mod 𝑁) = (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁)) |
93 | 59 | zcnd 11942 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℂ) |
94 | 93 | exp1d 13359 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴↑1) = 𝐴) |
95 | | seq1 13236 |
. . . . . . . . . . . . . . . 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 7041 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴↑1) · (seq1( · , 𝐹)‘1)) = (𝐴 · (𝐹‘1))) |
99 | 98 | oveq1d 7038 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁)) |
100 | 82, 92, 99 | 3eqtr4rd 2844 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁)) |
101 | 96 | oveq2i 7034 |
. . . . . . . . . . . 12
⊢ (𝑁 gcd (seq1( · , 𝐹)‘1)) = (𝑁 gcd (𝐹‘1)) |
102 | 2 | nnzd 11940 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℤ) |
103 | | gcdcom 15699 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℤ ∧ (𝐹‘1) ∈ ℤ) →
(𝑁 gcd (𝐹‘1)) = ((𝐹‘1) gcd 𝑁)) |
104 | 102, 77, 103 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 gcd (𝐹‘1)) = ((𝐹‘1) gcd 𝑁)) |
105 | 74 | simprd 496 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹‘1) gcd 𝑁) = 1) |
106 | 104, 105 | eqtrd 2833 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 gcd (𝐹‘1)) = 1) |
107 | 101, 106 | syl5eq 2845 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1) |
108 | 100, 107 | jca 512 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1)) |
109 | 108 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 1 ≤ (ϕ‘𝑁)) → ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1)) |
110 | | nnre 11499 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℝ) |
111 | 110 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → 𝑧 ∈ ℝ) |
112 | 111 | lep1d 11425 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → 𝑧 ≤ (𝑧 + 1)) |
113 | | peano2re 10666 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℝ → (𝑧 + 1) ∈
ℝ) |
114 | 111, 113 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → (𝑧 + 1) ∈ ℝ) |
115 | 4 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → (ϕ‘𝑁) ∈
ℝ) |
116 | | letr 10587 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℝ ∧ (𝑧 + 1) ∈ ℝ ∧
(ϕ‘𝑁) ∈
ℝ) → ((𝑧 ≤
(𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → 𝑧 ≤ (ϕ‘𝑁))) |
117 | 111, 114,
115, 116 | syl3anc 1364 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → ((𝑧 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → 𝑧 ≤ (ϕ‘𝑁))) |
118 | 112, 117 | mpand 691 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → ((𝑧 + 1) ≤ (ϕ‘𝑁) → 𝑧 ≤ (ϕ‘𝑁))) |
119 | 118 | imdistanda 572 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ → ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → (𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁)))) |
120 | 119 | imim1d 82 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℕ → (((𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)) → ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)))) |
121 | 59 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝐴 ∈ ℤ) |
122 | | nnnn0 11758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℕ0) |
123 | 122 | ad2antrl 724 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℕ0) |
124 | | zexpcl 13298 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℤ ∧ 𝑧 ∈ ℕ0)
→ (𝐴↑𝑧) ∈
ℤ) |
125 | 121, 123,
124 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴↑𝑧) ∈ ℤ) |
126 | | simprl 767 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℕ) |
127 | 126, 63 | syl6eleq 2895 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈
(ℤ≥‘1)) |
128 | 110 | ad2antrl 724 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℝ) |
129 | 128, 113 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ ℝ) |
130 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (ϕ‘𝑁) ∈ ℝ) |
131 | 128 | lep1d 11425 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ≤ (𝑧 + 1)) |
132 | | simprr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ≤ (ϕ‘𝑁)) |
133 | 128, 129,
130, 131, 132 | letrd 10650 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ≤ (ϕ‘𝑁)) |
134 | | nnz 11858 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℤ) |
135 | 134 | ad2antrl 724 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℤ) |
136 | 3 | nnzd 11940 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℤ) |
137 | 136 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (ϕ‘𝑁) ∈ ℤ) |
138 | | eluz 12111 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ ℤ ∧
(ϕ‘𝑁) ∈
ℤ) → ((ϕ‘𝑁) ∈ (ℤ≥‘𝑧) ↔ 𝑧 ≤ (ϕ‘𝑁))) |
139 | 135, 137,
138 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((ϕ‘𝑁) ∈ (ℤ≥‘𝑧) ↔ 𝑧 ≤ (ϕ‘𝑁))) |
140 | 133, 139 | mpbird 258 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (ϕ‘𝑁) ∈ (ℤ≥‘𝑧)) |
141 | | fzss2 12801 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((ϕ‘𝑁)
∈ (ℤ≥‘𝑧) → (1...𝑧) ⊆ (1...(ϕ‘𝑁))) |
142 | 140, 141 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (1...𝑧) ⊆ (1...(ϕ‘𝑁))) |
143 | 142, 67 | syl6sseqr 3945 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (1...𝑧) ⊆ 𝑇) |
144 | 143 | sselda 3895 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑧)) → 𝑥 ∈ 𝑇) |
145 | 62 | ffvelrnda 6723 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ 𝑆) |
146 | | oveq1 7030 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = (𝐹‘𝑥) → (𝑦 gcd 𝑁) = ((𝐹‘𝑥) gcd 𝑁)) |
147 | 146 | eqeq1d 2799 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = (𝐹‘𝑥) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘𝑥) gcd 𝑁) = 1)) |
148 | 147, 72 | elrab2 3624 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹‘𝑥) ∈ 𝑆 ↔ ((𝐹‘𝑥) ∈ (0..^𝑁) ∧ ((𝐹‘𝑥) gcd 𝑁) = 1)) |
149 | 145, 148 | sylib 219 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → ((𝐹‘𝑥) ∈ (0..^𝑁) ∧ ((𝐹‘𝑥) gcd 𝑁) = 1)) |
150 | 149 | simpld 495 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ (0..^𝑁)) |
151 | | elfzoelz 12892 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘𝑥) ∈ (0..^𝑁) → (𝐹‘𝑥) ∈ ℤ) |
152 | 150, 151 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ ℤ) |
153 | 152 | adantlr 711 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ ℤ) |
154 | 144, 153 | syldan 591 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑧)) → (𝐹‘𝑥) ∈ ℤ) |
155 | | zmulcl 11885 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 · 𝑦) ∈ ℤ) |
156 | 155 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 · 𝑦) ∈ ℤ) |
157 | 127, 154,
156 | seqcl 13244 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐹)‘𝑧) ∈ ℤ) |
158 | 125, 157 | zmulcld 11947 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) ∈ ℤ) |
159 | 158 | zred 11941 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) ∈ ℝ) |
160 | 72 | ssrab3 3984 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑆 ⊆ (0..^𝑁) |
161 | 1, 72, 67, 60, 87 | eulerthlem1 15951 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐺:𝑇⟶𝑆) |
162 | 161 | ffvelrnda 6723 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ 𝑆) |
163 | 160, 162 | sseldi 3893 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ (0..^𝑁)) |
164 | | elfzoelz 12892 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺‘𝑥) ∈ (0..^𝑁) → (𝐺‘𝑥) ∈ ℤ) |
165 | 163, 164 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ ℤ) |
166 | 165 | adantlr 711 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ ℤ) |
167 | 144, 166 | syldan 591 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑧)) → (𝐺‘𝑥) ∈ ℤ) |
168 | 127, 167,
156 | seqcl 13244 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘𝑧) ∈ ℤ) |
169 | 168 | zred 11941 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘𝑧) ∈ ℝ) |
170 | 62 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝐹:𝑇⟶𝑆) |
171 | | peano2nn 11504 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ ℕ → (𝑧 + 1) ∈
ℕ) |
172 | 171 | ad2antrl 724 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ ℕ) |
173 | 172 | nnge1d 11539 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 1 ≤ (𝑧 + 1)) |
174 | 172 | nnzd 11940 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ ℤ) |
175 | | elfz 12752 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑧 + 1) ∈ ℤ ∧ 1
∈ ℤ ∧ (ϕ‘𝑁) ∈ ℤ) → ((𝑧 + 1) ∈
(1...(ϕ‘𝑁))
↔ (1 ≤ (𝑧 + 1)
∧ (𝑧 + 1) ≤
(ϕ‘𝑁)))) |
176 | 83, 175 | mp3an2 1441 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑧 + 1) ∈ ℤ ∧
(ϕ‘𝑁) ∈
ℤ) → ((𝑧 + 1)
∈ (1...(ϕ‘𝑁)) ↔ (1 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)))) |
177 | 174, 137,
176 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑧 + 1) ∈ (1...(ϕ‘𝑁)) ↔ (1 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)))) |
178 | 173, 132,
177 | mpbir2and 709 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ (1...(ϕ‘𝑁))) |
179 | 178, 67 | syl6eleqr 2896 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ 𝑇) |
180 | 170, 179 | ffvelrnd 6724 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ 𝑆) |
181 | | oveq1 7030 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (𝐹‘(𝑧 + 1)) → (𝑦 gcd 𝑁) = ((𝐹‘(𝑧 + 1)) gcd 𝑁)) |
182 | 181 | eqeq1d 2799 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = (𝐹‘(𝑧 + 1)) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1)) |
183 | 182, 72 | elrab2 3624 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘(𝑧 + 1)) ∈ 𝑆 ↔ ((𝐹‘(𝑧 + 1)) ∈ (0..^𝑁) ∧ ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1)) |
184 | 180, 183 | sylib 219 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐹‘(𝑧 + 1)) ∈ (0..^𝑁) ∧ ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1)) |
185 | 184 | simpld 495 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ (0..^𝑁)) |
186 | | elfzoelz 12892 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘(𝑧 + 1)) ∈ (0..^𝑁) → (𝐹‘(𝑧 + 1)) ∈ ℤ) |
187 | 185, 186 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ ℤ) |
188 | 121, 187 | zmulcld 11947 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℤ) |
189 | 80 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑁 ∈
ℝ+) |
190 | | modmul1 13146 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴↑𝑧) · (seq1( · ,
𝐹)‘𝑧)) ∈ ℝ ∧ (seq1( · ,
𝐺)‘𝑧) ∈ ℝ) ∧ ((𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℤ ∧ 𝑁 ∈ ℝ+)
∧ (((𝐴↑𝑧) · (seq1( · ,
𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁)) |
191 | 190 | 3expia 1114 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴↑𝑧) · (seq1( · ,
𝐹)‘𝑧)) ∈ ℝ ∧ (seq1( · ,
𝐺)‘𝑧) ∈ ℝ) ∧ ((𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℤ ∧ 𝑁 ∈ ℝ+))
→ ((((𝐴↑𝑧) · (seq1( · ,
𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁))) |
192 | 159, 169,
188, 189, 191 | syl22anc 835 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁))) |
193 | 125 | zcnd 11942 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴↑𝑧) ∈ ℂ) |
194 | 157 | zcnd 11942 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐹)‘𝑧) ∈ ℂ) |
195 | 93 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝐴 ∈ ℂ) |
196 | 187 | zcnd 11942 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ ℂ) |
197 | 193, 194,
195, 196 | mul4d 10705 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) = (((𝐴↑𝑧) · 𝐴) · ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1))))) |
198 | 195, 123 | expp1d 13365 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴↑(𝑧 + 1)) = ((𝐴↑𝑧) · 𝐴)) |
199 | | seqp1 13238 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈
(ℤ≥‘1) → (seq1( · , 𝐹)‘(𝑧 + 1)) = ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) |
200 | 127, 199 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐹)‘(𝑧 + 1)) = ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) |
201 | 198, 200 | oveq12d 7041 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) = (((𝐴↑𝑧) · 𝐴) · ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1))))) |
202 | 197, 201 | eqtr4d 2836 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) = ((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1)))) |
203 | 202 | oveq1d 7038 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁)) |
204 | 188 | zred 11941 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℝ) |
205 | 204, 189 | modcld 13097 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) ∈ ℝ) |
206 | | modabs2 13127 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)) |
207 | 204, 189,
206 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)) |
208 | | modmul1 13146 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ·
(𝐹‘(𝑧 + 1))) mod 𝑁) ∈ ℝ ∧ (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℝ) ∧ ((seq1(
· , 𝐺)‘𝑧) ∈ ℤ ∧ 𝑁 ∈ ℝ+)
∧ (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)) → ((((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁)) |
209 | 205, 204,
168, 189, 207, 208 | syl221anc 1374 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁)) |
210 | | fveq2 6545 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = (𝑧 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑧 + 1))) |
211 | 210 | oveq2d 7039 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = (𝑧 + 1) → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘(𝑧 + 1)))) |
212 | 211 | oveq1d 7038 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = (𝑧 + 1) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)) |
213 | | ovex 7055 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) ∈ V |
214 | 212, 87, 213 | fvmpt 6642 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 + 1) ∈ 𝑇 → (𝐺‘(𝑧 + 1)) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)) |
215 | 179, 214 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐺‘(𝑧 + 1)) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)) |
216 | 215 | oveq2d 7039 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((seq1( · , 𝐺)‘𝑧) · (𝐺‘(𝑧 + 1))) = ((seq1( · , 𝐺)‘𝑧) · ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))) |
217 | | seqp1 13238 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈
(ℤ≥‘1) → (seq1( · , 𝐺)‘(𝑧 + 1)) = ((seq1( · , 𝐺)‘𝑧) · (𝐺‘(𝑧 + 1)))) |
218 | 127, 217 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘(𝑧 + 1)) = ((seq1( · , 𝐺)‘𝑧) · (𝐺‘(𝑧 + 1)))) |
219 | 205 | recnd 10522 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) ∈ ℂ) |
220 | 168 | zcnd 11942 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘𝑧) ∈ ℂ) |
221 | 219, 220 | mulcomd 10515 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) = ((seq1( · , 𝐺)‘𝑧) · ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))) |
222 | 216, 218,
221 | 3eqtr4d 2843 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘(𝑧 + 1)) = (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧))) |
223 | 222 | oveq1d 7038 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) = ((((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁)) |
224 | 188 | zcnd 11942 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℂ) |
225 | 220, 224 | mulcomd 10515 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) = ((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧))) |
226 | 225 | oveq1d 7038 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁)) |
227 | 209, 223,
226 | 3eqtr4rd 2844 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁)) |
228 | 203, 227 | eqeq12d 2812 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) ↔ (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁))) |
229 | 192, 228 | sylibd 240 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) → (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁))) |
230 | 102 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑁 ∈ ℤ) |
231 | | gcdcom 15699 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℤ ∧ (𝐹‘(𝑧 + 1)) ∈ ℤ) → (𝑁 gcd (𝐹‘(𝑧 + 1))) = ((𝐹‘(𝑧 + 1)) gcd 𝑁)) |
232 | 230, 187,
231 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑁 gcd (𝐹‘(𝑧 + 1))) = ((𝐹‘(𝑧 + 1)) gcd 𝑁)) |
233 | 184 | simprd 496 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1) |
234 | 232, 233 | eqtrd 2833 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑁 gcd (𝐹‘(𝑧 + 1))) = 1) |
235 | | rpmul 15836 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧ (seq1(
· , 𝐹)‘𝑧) ∈ ℤ ∧ (𝐹‘(𝑧 + 1)) ∈ ℤ) → (((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 ∧ (𝑁 gcd (𝐹‘(𝑧 + 1))) = 1) → (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1)) |
236 | 230, 157,
187, 235 | syl3anc 1364 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 ∧ (𝑁 gcd (𝐹‘(𝑧 + 1))) = 1) → (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1)) |
237 | 234, 236 | mpan2d 690 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 → (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1)) |
238 | 200 | oveq2d 7039 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1))))) |
239 | 238 | eqeq1d 2799 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1 ↔ (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1)) |
240 | 237, 239 | sylibrd 260 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 → (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)) |
241 | 229, 240 | anim12d 608 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))) |
242 | 241 | an12s 645 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℕ ∧ (𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))) |
243 | 242 | ex 413 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ → ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)))) |
244 | 243 | a2d 29 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℕ → (((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)) → ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)))) |
245 | 120, 244 | syld 47 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℕ → (((𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)) → ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)))) |
246 | 19, 32, 45, 58, 109, 245 | nnind 11510 |
. . . . . . . 8
⊢
((ϕ‘𝑁)
∈ ℕ → ((𝜑
∧ (ϕ‘𝑁) ≤
(ϕ‘𝑁)) →
((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1))) |
247 | 6, 246 | mpcom 38 |
. . . . . . 7
⊢ ((𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)) → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1)) |
248 | 5, 247 | mpdan 683 |
. . . . . 6
⊢ (𝜑 → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1)) |
249 | 248 | simpld 495 |
. . . . 5
⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁)) |
250 | 3 | nnnn0d 11809 |
. . . . . . . 8
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℕ0) |
251 | | zexpcl 13298 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧
(ϕ‘𝑁) ∈
ℕ0) → (𝐴↑(ϕ‘𝑁)) ∈ ℤ) |
252 | 59, 250, 251 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐴↑(ϕ‘𝑁)) ∈ ℤ) |
253 | 67 | eleq2i 2876 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑇 ↔ 𝑥 ∈ (1...(ϕ‘𝑁))) |
254 | 253, 152 | sylan2br 594 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(ϕ‘𝑁))) → (𝐹‘𝑥) ∈ ℤ) |
255 | 155 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 · 𝑦) ∈ ℤ) |
256 | 64, 254, 255 | seqcl 13244 |
. . . . . . 7
⊢ (𝜑 → (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈
ℤ) |
257 | 252, 256 | zmulcld 11947 |
. . . . . 6
⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) ∈
ℤ) |
258 | | mulcl 10474 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
259 | 258 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ) |
260 | | mulcom 10476 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) |
261 | 260 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) |
262 | | mulass 10478 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) |
263 | 262 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) |
264 | | ssidd 3917 |
. . . . . . . 8
⊢ (𝜑 → ℂ ⊆
ℂ) |
265 | | f1ocnv 6502 |
. . . . . . . . . . 11
⊢ (𝐹:𝑇–1-1-onto→𝑆 → ◡𝐹:𝑆–1-1-onto→𝑇) |
266 | 60, 265 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ◡𝐹:𝑆–1-1-onto→𝑇) |
267 | 2 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑁 ∈ ℕ) |
268 | 59 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝐴 ∈ ℤ) |
269 | 62 | ffvelrnda 6723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑇) → (𝐹‘𝑦) ∈ 𝑆) |
270 | 269 | adantrr 713 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ 𝑆) |
271 | 160, 270 | sseldi 3893 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ (0..^𝑁)) |
272 | | elfzoelz 12892 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑦) ∈ (0..^𝑁) → (𝐹‘𝑦) ∈ ℤ) |
273 | 271, 272 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ ℤ) |
274 | 268, 273 | zmulcld 11947 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐴 · (𝐹‘𝑦)) ∈ ℤ) |
275 | 62 | ffvelrnda 6723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑇) → (𝐹‘𝑧) ∈ 𝑆) |
276 | 275 | adantrl 712 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ 𝑆) |
277 | 160, 276 | sseldi 3893 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ (0..^𝑁)) |
278 | | elfzoelz 12892 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑧) ∈ (0..^𝑁) → (𝐹‘𝑧) ∈ ℤ) |
279 | 277, 278 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ ℤ) |
280 | 268, 279 | zmulcld 11947 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐴 · (𝐹‘𝑧)) ∈ ℤ) |
281 | | moddvds 15455 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 · (𝐹‘𝑦)) ∈ ℤ ∧ (𝐴 · (𝐹‘𝑧)) ∈ ℤ) → (((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁) ↔ 𝑁 ∥ ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧))))) |
282 | 267, 274,
280, 281 | syl3anc 1364 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁) ↔ 𝑁 ∥ ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧))))) |
283 | | fveq2 6545 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
284 | 283 | oveq2d 7039 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘𝑦))) |
285 | 284 | oveq1d 7038 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘𝑦)) mod 𝑁)) |
286 | | ovex 7055 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 · (𝐹‘𝑦)) mod 𝑁) ∈ V |
287 | 285, 87, 286 | fvmpt 6642 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝑇 → (𝐺‘𝑦) = ((𝐴 · (𝐹‘𝑦)) mod 𝑁)) |
288 | | fveq2 6545 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
289 | 288 | oveq2d 7039 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑧 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘𝑧))) |
290 | 289 | oveq1d 7038 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑧 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁)) |
291 | | ovex 7055 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 · (𝐹‘𝑧)) mod 𝑁) ∈ V |
292 | 290, 87, 291 | fvmpt 6642 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑇 → (𝐺‘𝑧) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁)) |
293 | 287, 292 | eqeqan12d 2813 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇) → ((𝐺‘𝑦) = (𝐺‘𝑧) ↔ ((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁))) |
294 | 293 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐺‘𝑦) = (𝐺‘𝑧) ↔ ((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁))) |
295 | 93 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝐴 ∈ ℂ) |
296 | 273 | zcnd 11942 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ ℂ) |
297 | 279 | zcnd 11942 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ ℂ) |
298 | 295, 296,
297 | subdid 10950 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) = ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧)))) |
299 | 298 | breq2d 4980 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ↔ 𝑁 ∥ ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧))))) |
300 | 282, 294,
299 | 3bitr4d 312 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐺‘𝑦) = (𝐺‘𝑧) ↔ 𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))))) |
301 | | gcdcom 15699 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑁 gcd 𝐴) = (𝐴 gcd 𝑁)) |
302 | 102, 59, 301 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 gcd 𝐴) = (𝐴 gcd 𝑁)) |
303 | 1 | simp3d 1137 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 gcd 𝑁) = 1) |
304 | 302, 303 | eqtrd 2833 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 gcd 𝐴) = 1) |
305 | 304 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 gcd 𝐴) = 1) |
306 | 102 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑁 ∈ ℤ) |
307 | 273, 279 | zsubcld 11946 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) − (𝐹‘𝑧)) ∈ ℤ) |
308 | | coprmdvds 15830 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ((𝐹‘𝑦) − (𝐹‘𝑧)) ∈ ℤ) → ((𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ∧ (𝑁 gcd 𝐴) = 1) → 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧)))) |
309 | 306, 268,
307, 308 | syl3anc 1364 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ∧ (𝑁 gcd 𝐴) = 1) → 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧)))) |
310 | 273 | zred 11941 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ ℝ) |
311 | 80 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑁 ∈
ℝ+) |
312 | | elfzole1 12900 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑦) ∈ (0..^𝑁) → 0 ≤ (𝐹‘𝑦)) |
313 | 271, 312 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 0 ≤ (𝐹‘𝑦)) |
314 | | elfzolt2 12901 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑦) ∈ (0..^𝑁) → (𝐹‘𝑦) < 𝑁) |
315 | 271, 314 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) < 𝑁) |
316 | | modid 13118 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑦) ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (0 ≤
(𝐹‘𝑦) ∧ (𝐹‘𝑦) < 𝑁)) → ((𝐹‘𝑦) mod 𝑁) = (𝐹‘𝑦)) |
317 | 310, 311,
313, 315, 316 | syl22anc 835 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) mod 𝑁) = (𝐹‘𝑦)) |
318 | 279 | zred 11941 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ ℝ) |
319 | | elfzole1 12900 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑧) ∈ (0..^𝑁) → 0 ≤ (𝐹‘𝑧)) |
320 | 277, 319 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 0 ≤ (𝐹‘𝑧)) |
321 | | elfzolt2 12901 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑧) ∈ (0..^𝑁) → (𝐹‘𝑧) < 𝑁) |
322 | 277, 321 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) < 𝑁) |
323 | | modid 13118 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑧) ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (0 ≤
(𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑁)) → ((𝐹‘𝑧) mod 𝑁) = (𝐹‘𝑧)) |
324 | 318, 311,
320, 322, 323 | syl22anc 835 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑧) mod 𝑁) = (𝐹‘𝑧)) |
325 | 317, 324 | eqeq12d 2812 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((𝐹‘𝑦) mod 𝑁) = ((𝐹‘𝑧) mod 𝑁) ↔ (𝐹‘𝑦) = (𝐹‘𝑧))) |
326 | | moddvds 15455 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ (𝐹‘𝑦) ∈ ℤ ∧ (𝐹‘𝑧) ∈ ℤ) → (((𝐹‘𝑦) mod 𝑁) = ((𝐹‘𝑧) mod 𝑁) ↔ 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧)))) |
327 | 267, 273,
279, 326 | syl3anc 1364 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((𝐹‘𝑦) mod 𝑁) = ((𝐹‘𝑧) mod 𝑁) ↔ 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧)))) |
328 | | f1of1 6489 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝐹:𝑇–1-1→𝑆) |
329 | 60, 328 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹:𝑇–1-1→𝑆) |
330 | | f1fveq 6892 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝑇–1-1→𝑆 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ 𝑦 = 𝑧)) |
331 | 329, 330 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ 𝑦 = 𝑧)) |
332 | 325, 327,
331 | 3bitr3d 310 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧)) ↔ 𝑦 = 𝑧)) |
333 | 309, 332 | sylibd 240 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ∧ (𝑁 gcd 𝐴) = 1) → 𝑦 = 𝑧)) |
334 | 305, 333 | mpan2d 690 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) → 𝑦 = 𝑧)) |
335 | 300, 334 | sylbid 241 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐺‘𝑦) = (𝐺‘𝑧) → 𝑦 = 𝑧)) |
336 | 335 | ralrimivva 3160 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑦 ∈ 𝑇 ∀𝑧 ∈ 𝑇 ((𝐺‘𝑦) = (𝐺‘𝑧) → 𝑦 = 𝑧)) |
337 | | dff13 6885 |
. . . . . . . . . . . 12
⊢ (𝐺:𝑇–1-1→𝑆 ↔ (𝐺:𝑇⟶𝑆 ∧ ∀𝑦 ∈ 𝑇 ∀𝑧 ∈ 𝑇 ((𝐺‘𝑦) = (𝐺‘𝑧) → 𝑦 = 𝑧))) |
338 | 161, 336,
337 | sylanbrc 583 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺:𝑇–1-1→𝑆) |
339 | 67 | ovexi 7056 |
. . . . . . . . . . . . . 14
⊢ 𝑇 ∈ V |
340 | 339 | f1oen 8385 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝑇 ≈ 𝑆) |
341 | 60, 340 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ≈ 𝑆) |
342 | | fzofi 13196 |
. . . . . . . . . . . . 13
⊢
(0..^𝑁) ∈
Fin |
343 | | ssfi 8591 |
. . . . . . . . . . . . 13
⊢
(((0..^𝑁) ∈ Fin
∧ 𝑆 ⊆ (0..^𝑁)) → 𝑆 ∈ Fin) |
344 | 342, 160,
343 | mp2an 688 |
. . . . . . . . . . . 12
⊢ 𝑆 ∈ Fin |
345 | | f1finf1o 8598 |
. . . . . . . . . . . 12
⊢ ((𝑇 ≈ 𝑆 ∧ 𝑆 ∈ Fin) → (𝐺:𝑇–1-1→𝑆 ↔ 𝐺:𝑇–1-1-onto→𝑆)) |
346 | 341, 344,
345 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺:𝑇–1-1→𝑆 ↔ 𝐺:𝑇–1-1-onto→𝑆)) |
347 | 338, 346 | mpbid 233 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:𝑇–1-1-onto→𝑆) |
348 | | f1oco 6512 |
. . . . . . . . . 10
⊢ ((◡𝐹:𝑆–1-1-onto→𝑇 ∧ 𝐺:𝑇–1-1-onto→𝑆) → (◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇) |
349 | 266, 347,
348 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇) |
350 | | f1oeq23 6482 |
. . . . . . . . . 10
⊢ ((𝑇 = (1...(ϕ‘𝑁)) ∧ 𝑇 = (1...(ϕ‘𝑁))) → ((◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇 ↔ (◡𝐹 ∘ 𝐺):(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁)))) |
351 | 67, 67, 350 | mp2an 688 |
. . . . . . . . 9
⊢ ((◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇 ↔ (◡𝐹 ∘ 𝐺):(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁))) |
352 | 349, 351 | sylib 219 |
. . . . . . . 8
⊢ (𝜑 → (◡𝐹 ∘ 𝐺):(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁))) |
353 | 254 | zcnd 11942 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(ϕ‘𝑁))) → (𝐹‘𝑥) ∈ ℂ) |
354 | 67 | eleq2i 2876 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝑇 ↔ 𝑤 ∈ (1...(ϕ‘𝑁))) |
355 | | fvco3 6634 |
. . . . . . . . . . . 12
⊢ ((𝐺:𝑇⟶𝑆 ∧ 𝑤 ∈ 𝑇) → ((◡𝐹 ∘ 𝐺)‘𝑤) = (◡𝐹‘(𝐺‘𝑤))) |
356 | 161, 355 | sylan 580 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((◡𝐹 ∘ 𝐺)‘𝑤) = (◡𝐹‘(𝐺‘𝑤))) |
357 | 356 | fveq2d 6549 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐹‘((◡𝐹 ∘ 𝐺)‘𝑤)) = (𝐹‘(◡𝐹‘(𝐺‘𝑤)))) |
358 | 60 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝐹:𝑇–1-1-onto→𝑆) |
359 | 161 | ffvelrnda 6723 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐺‘𝑤) ∈ 𝑆) |
360 | | f1ocnvfv2 6906 |
. . . . . . . . . . 11
⊢ ((𝐹:𝑇–1-1-onto→𝑆 ∧ (𝐺‘𝑤) ∈ 𝑆) → (𝐹‘(◡𝐹‘(𝐺‘𝑤))) = (𝐺‘𝑤)) |
361 | 358, 359,
360 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐹‘(◡𝐹‘(𝐺‘𝑤))) = (𝐺‘𝑤)) |
362 | 357, 361 | eqtr2d 2834 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐺‘𝑤) = (𝐹‘((◡𝐹 ∘ 𝐺)‘𝑤))) |
363 | 354, 362 | sylan2br 594 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (1...(ϕ‘𝑁))) → (𝐺‘𝑤) = (𝐹‘((◡𝐹 ∘ 𝐺)‘𝑤))) |
364 | 259, 261,
263, 64, 264, 352, 353, 363 | seqf1o 13265 |
. . . . . . 7
⊢ (𝜑 → (seq1( · , 𝐺)‘(ϕ‘𝑁)) = (seq1( · , 𝐹)‘(ϕ‘𝑁))) |
365 | 364, 256 | eqeltrd 2885 |
. . . . . 6
⊢ (𝜑 → (seq1( · , 𝐺)‘(ϕ‘𝑁)) ∈
ℤ) |
366 | | moddvds 15455 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴↑(ϕ‘𝑁)) · (seq1( · ,
𝐹)‘(ϕ‘𝑁))) ∈ ℤ ∧ (seq1( · ,
𝐺)‘(ϕ‘𝑁)) ∈ ℤ) → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · ,
𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ↔ 𝑁 ∥ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · ,
𝐺)‘(ϕ‘𝑁))))) |
367 | 2, 257, 365, 366 | syl3anc 1364 |
. . . . 5
⊢ (𝜑 → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ↔ 𝑁 ∥ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · ,
𝐺)‘(ϕ‘𝑁))))) |
368 | 249, 367 | mpbid 233 |
. . . 4
⊢ (𝜑 → 𝑁 ∥ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · ,
𝐺)‘(ϕ‘𝑁)))) |
369 | 256 | zcnd 11942 |
. . . . . . . 8
⊢ (𝜑 → (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈
ℂ) |
370 | 369 | mulid2d 10512 |
. . . . . . 7
⊢ (𝜑 → (1 · (seq1(
· , 𝐹)‘(ϕ‘𝑁))) = (seq1( · , 𝐹)‘(ϕ‘𝑁))) |
371 | 364, 370 | eqtr4d 2836 |
. . . . . 6
⊢ (𝜑 → (seq1( · , 𝐺)‘(ϕ‘𝑁)) = (1 · (seq1( ·
, 𝐹)‘(ϕ‘𝑁)))) |
372 | 371 | oveq2d 7039 |
. . . . 5
⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · ,
𝐺)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1(
· , 𝐹)‘(ϕ‘𝑁))))) |
373 | 252 | zcnd 11942 |
. . . . . 6
⊢ (𝜑 → (𝐴↑(ϕ‘𝑁)) ∈ ℂ) |
374 | | ax-1cn 10448 |
. . . . . . 7
⊢ 1 ∈
ℂ |
375 | | subdir 10928 |
. . . . . . 7
⊢ (((𝐴↑(ϕ‘𝑁)) ∈ ℂ ∧ 1 ∈
ℂ ∧ (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈ ℂ) → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1(
· , 𝐹)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1(
· , 𝐹)‘(ϕ‘𝑁))))) |
376 | 374, 375 | mp3an2 1441 |
. . . . . 6
⊢ (((𝐴↑(ϕ‘𝑁)) ∈ ℂ ∧ (seq1(
· , 𝐹)‘(ϕ‘𝑁)) ∈ ℂ) → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1(
· , 𝐹)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1(
· , 𝐹)‘(ϕ‘𝑁))))) |
377 | 373, 369,
376 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1( · ,
𝐹)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1(
· , 𝐹)‘(ϕ‘𝑁))))) |
378 | | zsubcl 11878 |
. . . . . . . 8
⊢ (((𝐴↑(ϕ‘𝑁)) ∈ ℤ ∧ 1 ∈
ℤ) → ((𝐴↑(ϕ‘𝑁)) − 1) ∈
ℤ) |
379 | 252, 83, 378 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) − 1) ∈
ℤ) |
380 | 379 | zcnd 11942 |
. . . . . 6
⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) − 1) ∈
ℂ) |
381 | 380, 369 | mulcomd 10515 |
. . . . 5
⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1( · ,
𝐹)‘(ϕ‘𝑁))) = ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1))) |
382 | 372, 377,
381 | 3eqtr2d 2839 |
. . . 4
⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · ,
𝐺)‘(ϕ‘𝑁))) = ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1))) |
383 | 368, 382 | breqtrd 4994 |
. . 3
⊢ (𝜑 → 𝑁 ∥ ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1))) |
384 | 248 | simprd 496 |
. . 3
⊢ (𝜑 → (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1) |
385 | | coprmdvds 15830 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ (seq1(
· , 𝐹)‘(ϕ‘𝑁)) ∈ ℤ ∧ ((𝐴↑(ϕ‘𝑁)) − 1) ∈ ℤ) → ((𝑁 ∥ ((seq1( · ,
𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1) → 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1))) |
386 | 102, 256,
379, 385 | syl3anc 1364 |
. . 3
⊢ (𝜑 → ((𝑁 ∥ ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1) → 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1))) |
387 | 383, 384,
386 | mp2and 695 |
. 2
⊢ (𝜑 → 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1)) |
388 | | moddvds 15455 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑁)) ∈ ℤ ∧ 1 ∈
ℤ) → (((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1))) |
389 | 83, 388 | mp3an3 1442 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑁)) ∈ ℤ) →
(((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1))) |
390 | 2, 252, 389 | syl2anc 584 |
. 2
⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1))) |
391 | 387, 390 | mpbird 258 |
1
⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁)) |