| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eulerth.1 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1)) | 
| 2 | 1 | simp1d 1143 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 3 | 2 | phicld 16809 | . . . . . . . . 9
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℕ) | 
| 4 | 3 | nnred 12281 | . . . . . . . 8
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℝ) | 
| 5 | 4 | leidd 11829 | . . . . . . 7
⊢ (𝜑 → (ϕ‘𝑁) ≤ (ϕ‘𝑁)) | 
| 6 | 3 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)) → (ϕ‘𝑁) ∈
ℕ) | 
| 7 |  | breq1 5146 | . . . . . . . . . . 11
⊢ (𝑥 = 1 → (𝑥 ≤ (ϕ‘𝑁) ↔ 1 ≤ (ϕ‘𝑁))) | 
| 8 | 7 | anbi2d 630 | . . . . . . . . . 10
⊢ (𝑥 = 1 → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ 1 ≤ (ϕ‘𝑁)))) | 
| 9 |  | oveq2 7439 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → (𝐴↑𝑥) = (𝐴↑1)) | 
| 10 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → (seq1( · ,
𝐹)‘𝑥) = (seq1( · , 𝐹)‘1)) | 
| 11 | 9, 10 | oveq12d 7449 | . . . . . . . . . . . . 13
⊢ (𝑥 = 1 → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑1) · (seq1( · , 𝐹)‘1))) | 
| 12 | 11 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝑥 = 1 → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁)) | 
| 13 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (seq1( · ,
𝐺)‘𝑥) = (seq1( · , 𝐺)‘1)) | 
| 14 | 13 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝑥 = 1 → ((seq1( · ,
𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁)) | 
| 15 | 12, 14 | eqeq12d 2753 | . . . . . . . . . . 11
⊢ (𝑥 = 1 → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁))) | 
| 16 | 10 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝑥 = 1 → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘1))) | 
| 17 | 16 | eqeq1d 2739 | . . . . . . . . . . 11
⊢ (𝑥 = 1 → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1)) | 
| 18 | 15, 17 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑥 = 1 → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1))) | 
| 19 | 8, 18 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑥 = 1 → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ 1 ≤ (ϕ‘𝑁)) → ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1)))) | 
| 20 |  | breq1 5146 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝑥 ≤ (ϕ‘𝑁) ↔ 𝑧 ≤ (ϕ‘𝑁))) | 
| 21 | 20 | anbi2d 630 | . . . . . . . . . 10
⊢ (𝑥 = 𝑧 → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁)))) | 
| 22 |  | oveq2 7439 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝐴↑𝑥) = (𝐴↑𝑧)) | 
| 23 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑧)) | 
| 24 | 22, 23 | oveq12d 7449 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧))) | 
| 25 | 24 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁)) | 
| 26 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘𝑧)) | 
| 27 | 26 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → ((seq1( · , 𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁)) | 
| 28 | 25, 27 | eqeq12d 2753 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁))) | 
| 29 | 23 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘𝑧))) | 
| 30 | 29 | eqeq1d 2739 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)) | 
| 31 | 28, 30 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1))) | 
| 32 | 21, 31 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑥 = 𝑧 → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ 𝑧 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1)))) | 
| 33 |  | breq1 5146 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑧 + 1) → (𝑥 ≤ (ϕ‘𝑁) ↔ (𝑧 + 1) ≤ (ϕ‘𝑁))) | 
| 34 | 33 | anbi2d 630 | . . . . . . . . . 10
⊢ (𝑥 = (𝑧 + 1) → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)))) | 
| 35 |  | oveq2 7439 | . . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑧 + 1) → (𝐴↑𝑥) = (𝐴↑(𝑧 + 1))) | 
| 36 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑧 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑧 + 1))) | 
| 37 | 35, 36 | oveq12d 7449 | . . . . . . . . . . . . 13
⊢ (𝑥 = (𝑧 + 1) → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1)))) | 
| 38 | 37 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝑥 = (𝑧 + 1) → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁)) | 
| 39 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑥 = (𝑧 + 1) → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘(𝑧 + 1))) | 
| 40 | 39 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝑥 = (𝑧 + 1) → ((seq1( · , 𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁)) | 
| 41 | 38, 40 | eqeq12d 2753 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑧 + 1) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁))) | 
| 42 | 36 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝑥 = (𝑧 + 1) → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1)))) | 
| 43 | 42 | eqeq1d 2739 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑧 + 1) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)) | 
| 44 | 41, 43 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑥 = (𝑧 + 1) → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))) | 
| 45 | 34, 44 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑥 = (𝑧 + 1) → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1)))) | 
| 46 |  | breq1 5146 | . . . . . . . . . . 11
⊢ (𝑥 = (ϕ‘𝑁) → (𝑥 ≤ (ϕ‘𝑁) ↔ (ϕ‘𝑁) ≤ (ϕ‘𝑁))) | 
| 47 | 46 | anbi2d 630 | . . . . . . . . . 10
⊢ (𝑥 = (ϕ‘𝑁) → ((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) ↔ (𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)))) | 
| 48 |  | oveq2 7439 | . . . . . . . . . . . . . 14
⊢ (𝑥 = (ϕ‘𝑁) → (𝐴↑𝑥) = (𝐴↑(ϕ‘𝑁))) | 
| 49 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑥 = (ϕ‘𝑁) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(ϕ‘𝑁))) | 
| 50 | 48, 49 | oveq12d 7449 | . . . . . . . . . . . . 13
⊢ (𝑥 = (ϕ‘𝑁) → ((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) = ((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁)))) | 
| 51 | 50 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝑥 = (ϕ‘𝑁) → (((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁)) | 
| 52 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑥 = (ϕ‘𝑁) → (seq1( · , 𝐺)‘𝑥) = (seq1( · , 𝐺)‘(ϕ‘𝑁))) | 
| 53 | 52 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝑥 = (ϕ‘𝑁) → ((seq1( · ,
𝐺)‘𝑥) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁)) | 
| 54 | 51, 53 | eqeq12d 2753 | . . . . . . . . . . 11
⊢ (𝑥 = (ϕ‘𝑁) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ↔ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁))) | 
| 55 | 49 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝑥 = (ϕ‘𝑁) → (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁)))) | 
| 56 | 55 | eqeq1d 2739 | . . . . . . . . . . 11
⊢ (𝑥 = (ϕ‘𝑁) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1 ↔ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1)) | 
| 57 | 54, 56 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑥 = (ϕ‘𝑁) → (((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1) ↔ ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1))) | 
| 58 | 47, 57 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑥 = (ϕ‘𝑁) → (((𝜑 ∧ 𝑥 ≤ (ϕ‘𝑁)) → ((((𝐴↑𝑥) · (seq1( · , 𝐹)‘𝑥)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑥) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑥)) = 1)) ↔ ((𝜑 ∧ (ϕ‘𝑁) ≤ (ϕ‘𝑁)) → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1)))) | 
| 59 | 1 | simp2d 1144 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℤ) | 
| 60 |  | eulerth.4 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐹:𝑇–1-1-onto→𝑆) | 
| 61 |  | f1of 6848 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝐹:𝑇⟶𝑆) | 
| 62 | 60, 61 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹:𝑇⟶𝑆) | 
| 63 |  | nnuz 12921 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ℕ =
(ℤ≥‘1) | 
| 64 | 3, 63 | eleqtrdi 2851 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (ϕ‘𝑁) ∈
(ℤ≥‘1)) | 
| 65 |  | eluzfz1 13571 | . . . . . . . . . . . . . . . . . . . . 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 | ffvelcdmd 7105 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐹‘1) ∈ 𝑆) | 
| 70 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝐹‘1) → (𝑦 gcd 𝑁) = ((𝐹‘1) gcd 𝑁)) | 
| 71 | 70 | eqeq1d 2739 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (𝐹‘1) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘1) gcd 𝑁) = 1)) | 
| 72 |  | eulerth.2 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} | 
| 73 | 71, 72 | elrab2 3695 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘1) ∈ 𝑆 ↔ ((𝐹‘1) ∈ (0..^𝑁) ∧ ((𝐹‘1) gcd 𝑁) = 1)) | 
| 74 | 69, 73 | sylib 218 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐹‘1) ∈ (0..^𝑁) ∧ ((𝐹‘1) gcd 𝑁) = 1)) | 
| 75 | 74 | simpld 494 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹‘1) ∈ (0..^𝑁)) | 
| 76 |  | elfzoelz 13699 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹‘1) ∈ (0..^𝑁) → (𝐹‘1) ∈ ℤ) | 
| 77 | 75, 76 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹‘1) ∈ ℤ) | 
| 78 | 59, 77 | zmulcld 12728 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℤ) | 
| 79 | 78 | zred 12722 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 · (𝐹‘1)) ∈ ℝ) | 
| 80 | 2 | nnrpd 13075 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈
ℝ+) | 
| 81 |  | modabs2 13945 | . . . . . . . . . . . . 13
⊢ (((𝐴 · (𝐹‘1)) ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁)) | 
| 82 | 79, 80, 81 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁)) | 
| 83 |  | 1z 12647 | . . . . . . . . . . . . . 14
⊢ 1 ∈
ℤ | 
| 84 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 1 → (𝐹‘𝑥) = (𝐹‘1)) | 
| 85 | 84 | oveq2d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 1 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘1))) | 
| 86 | 85 | oveq1d 7446 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 1 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁)) | 
| 87 |  | eulerth.5 | . . . . . . . . . . . . . . . 16
⊢ 𝐺 = (𝑥 ∈ 𝑇 ↦ ((𝐴 · (𝐹‘𝑥)) mod 𝑁)) | 
| 88 |  | ovex 7464 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 · (𝐹‘1)) mod 𝑁) ∈ V | 
| 89 | 86, 87, 88 | fvmpt 7016 | . . . . . . . . . . . . . . 15
⊢ (1 ∈
𝑇 → (𝐺‘1) = ((𝐴 · (𝐹‘1)) mod 𝑁)) | 
| 90 | 68, 89 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐺‘1) = ((𝐴 · (𝐹‘1)) mod 𝑁)) | 
| 91 | 83, 90 | seq1i 14056 | . . . . . . . . . . . . 13
⊢ (𝜑 → (seq1( · , 𝐺)‘1) = ((𝐴 · (𝐹‘1)) mod 𝑁)) | 
| 92 | 91 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝜑 → ((seq1( · , 𝐺)‘1) mod 𝑁) = (((𝐴 · (𝐹‘1)) mod 𝑁) mod 𝑁)) | 
| 93 | 59 | zcnd 12723 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 94 | 93 | exp1d 14181 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴↑1) = 𝐴) | 
| 95 |  | seq1 14055 | . . . . . . . . . . . . . . . 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 7449 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴↑1) · (seq1( · , 𝐹)‘1)) = (𝐴 · (𝐹‘1))) | 
| 99 | 98 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((𝐴 · (𝐹‘1)) mod 𝑁)) | 
| 100 | 82, 92, 99 | 3eqtr4rd 2788 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁)) | 
| 101 | 96 | oveq2i 7442 | . . . . . . . . . . . 12
⊢ (𝑁 gcd (seq1( · , 𝐹)‘1)) = (𝑁 gcd (𝐹‘1)) | 
| 102 | 2 | nnzd 12640 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 103 | 102, 77 | gcdcomd 16551 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 gcd (𝐹‘1)) = ((𝐹‘1) gcd 𝑁)) | 
| 104 | 74 | simprd 495 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹‘1) gcd 𝑁) = 1) | 
| 105 | 103, 104 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 gcd (𝐹‘1)) = 1) | 
| 106 | 101, 105 | eqtrid 2789 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1) | 
| 107 | 100, 106 | jca 511 | . . . . . . . . . 10
⊢ (𝜑 → ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1)) | 
| 108 | 107 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 1 ≤ (ϕ‘𝑁)) → ((((𝐴↑1) · (seq1( · , 𝐹)‘1)) mod 𝑁) = ((seq1( · , 𝐺)‘1) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘1)) = 1)) | 
| 109 |  | nnre 12273 | . . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℝ) | 
| 110 | 109 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → 𝑧 ∈ ℝ) | 
| 111 | 110 | lep1d 12199 | . . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → 𝑧 ≤ (𝑧 + 1)) | 
| 112 |  | peano2re 11434 | . . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℝ → (𝑧 + 1) ∈
ℝ) | 
| 113 | 110, 112 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → (𝑧 + 1) ∈ ℝ) | 
| 114 | 4 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → (ϕ‘𝑁) ∈
ℝ) | 
| 115 |  | letr 11355 | . . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℝ ∧ (𝑧 + 1) ∈ ℝ ∧
(ϕ‘𝑁) ∈
ℝ) → ((𝑧 ≤
(𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → 𝑧 ≤ (ϕ‘𝑁))) | 
| 116 | 110, 113,
114, 115 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → ((𝑧 ≤ (𝑧 + 1) ∧ (𝑧 + 1) ≤ (ϕ‘𝑁)) → 𝑧 ≤ (ϕ‘𝑁))) | 
| 117 | 111, 116 | mpand 695 | . . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℕ ∧ 𝜑) → ((𝑧 + 1) ≤ (ϕ‘𝑁) → 𝑧 ≤ (ϕ‘𝑁))) | 
| 118 | 117 | imdistanda 571 | . . . . . . . . . . 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 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝐴 ∈ ℤ) | 
| 121 |  | nnnn0 12533 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℕ0) | 
| 122 | 121 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℕ0) | 
| 123 |  | zexpcl 14117 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℤ ∧ 𝑧 ∈ ℕ0)
→ (𝐴↑𝑧) ∈
ℤ) | 
| 124 | 120, 122,
123 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴↑𝑧) ∈ ℤ) | 
| 125 |  | simprl 771 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℕ) | 
| 126 | 125, 63 | eleqtrdi 2851 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈
(ℤ≥‘1)) | 
| 127 | 109 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℝ) | 
| 128 | 127, 112 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ ℝ) | 
| 129 | 4 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (ϕ‘𝑁) ∈ ℝ) | 
| 130 | 127 | lep1d 12199 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ≤ (𝑧 + 1)) | 
| 131 |  | simprr 773 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ≤ (ϕ‘𝑁)) | 
| 132 | 127, 128,
129, 130, 131 | letrd 11418 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ≤ (ϕ‘𝑁)) | 
| 133 |  | nnz 12634 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℤ) | 
| 134 | 133 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑧 ∈ ℤ) | 
| 135 | 3 | nnzd 12640 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℤ) | 
| 136 | 135 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (ϕ‘𝑁) ∈ ℤ) | 
| 137 |  | eluz 12892 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ ℤ ∧
(ϕ‘𝑁) ∈
ℤ) → ((ϕ‘𝑁) ∈ (ℤ≥‘𝑧) ↔ 𝑧 ≤ (ϕ‘𝑁))) | 
| 138 | 134, 136,
137 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((ϕ‘𝑁) ∈ (ℤ≥‘𝑧) ↔ 𝑧 ≤ (ϕ‘𝑁))) | 
| 139 | 132, 138 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (ϕ‘𝑁) ∈ (ℤ≥‘𝑧)) | 
| 140 |  | fzss2 13604 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((ϕ‘𝑁)
∈ (ℤ≥‘𝑧) → (1...𝑧) ⊆ (1...(ϕ‘𝑁))) | 
| 141 | 139, 140 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (1...𝑧) ⊆ (1...(ϕ‘𝑁))) | 
| 142 | 141, 67 | sseqtrrdi 4025 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (1...𝑧) ⊆ 𝑇) | 
| 143 | 142 | sselda 3983 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑧)) → 𝑥 ∈ 𝑇) | 
| 144 | 62 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ 𝑆) | 
| 145 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = (𝐹‘𝑥) → (𝑦 gcd 𝑁) = ((𝐹‘𝑥) gcd 𝑁)) | 
| 146 | 145 | eqeq1d 2739 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = (𝐹‘𝑥) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘𝑥) gcd 𝑁) = 1)) | 
| 147 | 146, 72 | elrab2 3695 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹‘𝑥) ∈ 𝑆 ↔ ((𝐹‘𝑥) ∈ (0..^𝑁) ∧ ((𝐹‘𝑥) gcd 𝑁) = 1)) | 
| 148 | 144, 147 | sylib 218 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → ((𝐹‘𝑥) ∈ (0..^𝑁) ∧ ((𝐹‘𝑥) gcd 𝑁) = 1)) | 
| 149 | 148 | simpld 494 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ (0..^𝑁)) | 
| 150 |  | elfzoelz 13699 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘𝑥) ∈ (0..^𝑁) → (𝐹‘𝑥) ∈ ℤ) | 
| 151 | 149, 150 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ ℤ) | 
| 152 | 151 | adantlr 715 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ ℤ) | 
| 153 | 143, 152 | syldan 591 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑧)) → (𝐹‘𝑥) ∈ ℤ) | 
| 154 |  | zmulcl 12666 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 · 𝑦) ∈ ℤ) | 
| 155 | 154 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 · 𝑦) ∈ ℤ) | 
| 156 | 126, 153,
155 | seqcl 14063 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐹)‘𝑧) ∈ ℤ) | 
| 157 | 124, 156 | zmulcld 12728 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) ∈ ℤ) | 
| 158 | 157 | zred 12722 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) ∈ ℝ) | 
| 159 | 72 | ssrab3 4082 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑆 ⊆ (0..^𝑁) | 
| 160 | 1, 72, 67, 60, 87 | eulerthlem1 16818 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐺:𝑇⟶𝑆) | 
| 161 | 160 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ 𝑆) | 
| 162 | 159, 161 | sselid 3981 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ (0..^𝑁)) | 
| 163 |  | elfzoelz 13699 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺‘𝑥) ∈ (0..^𝑁) → (𝐺‘𝑥) ∈ ℤ) | 
| 164 | 162, 163 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ ℤ) | 
| 165 | 164 | adantlr 715 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ 𝑇) → (𝐺‘𝑥) ∈ ℤ) | 
| 166 | 143, 165 | syldan 591 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑧)) → (𝐺‘𝑥) ∈ ℤ) | 
| 167 | 126, 166,
155 | seqcl 14063 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘𝑧) ∈ ℤ) | 
| 168 | 167 | zred 12722 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘𝑧) ∈ ℝ) | 
| 169 | 62 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝐹:𝑇⟶𝑆) | 
| 170 |  | peano2nn 12278 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ ℕ → (𝑧 + 1) ∈
ℕ) | 
| 171 | 170 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ ℕ) | 
| 172 | 171 | nnge1d 12314 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 1 ≤ (𝑧 + 1)) | 
| 173 | 171 | nnzd 12640 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ ℤ) | 
| 174 |  | elfz 13553 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑧 + 1) ∈ ℤ ∧ 1
∈ ℤ ∧ (ϕ‘𝑁) ∈ ℤ) → ((𝑧 + 1) ∈
(1...(ϕ‘𝑁))
↔ (1 ≤ (𝑧 + 1)
∧ (𝑧 + 1) ≤
(ϕ‘𝑁)))) | 
| 175 | 83, 174 | mp3an2 1451 | . . . . . . . . . . . . . . . . . . . . . . . 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 713 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ (1...(ϕ‘𝑁))) | 
| 178 | 177, 67 | eleqtrrdi 2852 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑧 + 1) ∈ 𝑇) | 
| 179 | 169, 178 | ffvelcdmd 7105 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ 𝑆) | 
| 180 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (𝐹‘(𝑧 + 1)) → (𝑦 gcd 𝑁) = ((𝐹‘(𝑧 + 1)) gcd 𝑁)) | 
| 181 | 180 | eqeq1d 2739 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = (𝐹‘(𝑧 + 1)) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1)) | 
| 182 | 181, 72 | elrab2 3695 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘(𝑧 + 1)) ∈ 𝑆 ↔ ((𝐹‘(𝑧 + 1)) ∈ (0..^𝑁) ∧ ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1)) | 
| 183 | 179, 182 | sylib 218 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐹‘(𝑧 + 1)) ∈ (0..^𝑁) ∧ ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1)) | 
| 184 | 183 | simpld 494 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ (0..^𝑁)) | 
| 185 |  | elfzoelz 13699 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘(𝑧 + 1)) ∈ (0..^𝑁) → (𝐹‘(𝑧 + 1)) ∈ ℤ) | 
| 186 | 184, 185 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ ℤ) | 
| 187 | 120, 186 | zmulcld 12728 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℤ) | 
| 188 | 80 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑁 ∈
ℝ+) | 
| 189 |  | modmul1 13965 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝐴↑𝑧) · (seq1( · ,
𝐹)‘𝑧)) ∈ ℝ ∧ (seq1( · ,
𝐺)‘𝑧) ∈ ℝ) ∧ ((𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℤ ∧ 𝑁 ∈ ℝ+)
∧ (((𝐴↑𝑧) · (seq1( · ,
𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁)) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁)) | 
| 190 | 189 | 3expia 1122 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐴↑𝑧) · (seq1( · ,
𝐹)‘𝑧)) ∈ ℝ ∧ (seq1( · ,
𝐺)‘𝑧) ∈ ℝ) ∧ ((𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℤ ∧ 𝑁 ∈ ℝ+))
→ ((((𝐴↑𝑧) · (seq1( · ,
𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁))) | 
| 191 | 158, 168,
187, 188, 190 | syl22anc 839 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁))) | 
| 192 | 124 | zcnd 12723 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴↑𝑧) ∈ ℂ) | 
| 193 | 156 | zcnd 12723 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐹)‘𝑧) ∈ ℂ) | 
| 194 | 93 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝐴 ∈ ℂ) | 
| 195 | 186 | zcnd 12723 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐹‘(𝑧 + 1)) ∈ ℂ) | 
| 196 | 192, 193,
194, 195 | mul4d 11473 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) = (((𝐴↑𝑧) · 𝐴) · ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1))))) | 
| 197 | 194, 122 | expp1d 14187 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴↑(𝑧 + 1)) = ((𝐴↑𝑧) · 𝐴)) | 
| 198 |  | seqp1 14057 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈
(ℤ≥‘1) → (seq1( · , 𝐹)‘(𝑧 + 1)) = ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) | 
| 199 | 126, 198 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐹)‘(𝑧 + 1)) = ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) | 
| 200 | 197, 199 | oveq12d 7449 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) = (((𝐴↑𝑧) · 𝐴) · ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1))))) | 
| 201 | 196, 200 | eqtr4d 2780 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) = ((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1)))) | 
| 202 | 201 | oveq1d 7446 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁)) | 
| 203 | 187 | zred 12722 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℝ) | 
| 204 | 203, 188 | modcld 13915 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) ∈ ℝ) | 
| 205 |  | modabs2 13945 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)) | 
| 206 | 203, 188,
205 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)) | 
| 207 |  | modmul1 13965 | . . . . . . . . . . . . . . . . . 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 1383 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁) = (((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁)) | 
| 209 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = (𝑧 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑧 + 1))) | 
| 210 | 209 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = (𝑧 + 1) → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘(𝑧 + 1)))) | 
| 211 | 210 | oveq1d 7446 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = (𝑧 + 1) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)) | 
| 212 |  | ovex 7464 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) ∈ V | 
| 213 | 211, 87, 212 | fvmpt 7016 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 + 1) ∈ 𝑇 → (𝐺‘(𝑧 + 1)) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)) | 
| 214 | 178, 213 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐺‘(𝑧 + 1)) = ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁)) | 
| 215 | 214 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((seq1( · , 𝐺)‘𝑧) · (𝐺‘(𝑧 + 1))) = ((seq1( · , 𝐺)‘𝑧) · ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))) | 
| 216 |  | seqp1 14057 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈
(ℤ≥‘1) → (seq1( · , 𝐺)‘(𝑧 + 1)) = ((seq1( · , 𝐺)‘𝑧) · (𝐺‘(𝑧 + 1)))) | 
| 217 | 126, 216 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘(𝑧 + 1)) = ((seq1( · , 𝐺)‘𝑧) · (𝐺‘(𝑧 + 1)))) | 
| 218 | 204 | recnd 11289 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) ∈ ℂ) | 
| 219 | 167 | zcnd 12723 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘𝑧) ∈ ℂ) | 
| 220 | 218, 219 | mulcomd 11282 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) = ((seq1( · , 𝐺)‘𝑧) · ((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁))) | 
| 221 | 215, 217,
220 | 3eqtr4d 2787 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (seq1( · , 𝐺)‘(𝑧 + 1)) = (((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧))) | 
| 222 | 221 | oveq1d 7446 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) = ((((𝐴 · (𝐹‘(𝑧 + 1))) mod 𝑁) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁)) | 
| 223 | 187 | zcnd 12723 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝐴 · (𝐹‘(𝑧 + 1))) ∈ ℂ) | 
| 224 | 219, 223 | mulcomd 11282 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) = ((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧))) | 
| 225 | 224 | oveq1d 7446 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((𝐴 · (𝐹‘(𝑧 + 1))) · (seq1( · , 𝐺)‘𝑧)) mod 𝑁)) | 
| 226 | 208, 222,
225 | 3eqtr4rd 2788 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁)) | 
| 227 | 202, 226 | eqeq12d 2753 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) = (((seq1( · , 𝐺)‘𝑧) · (𝐴 · (𝐹‘(𝑧 + 1)))) mod 𝑁) ↔ (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁))) | 
| 228 | 191, 227 | sylibd 239 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) → (((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁))) | 
| 229 | 102 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → 𝑁 ∈ ℤ) | 
| 230 | 229, 186 | gcdcomd 16551 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑁 gcd (𝐹‘(𝑧 + 1))) = ((𝐹‘(𝑧 + 1)) gcd 𝑁)) | 
| 231 | 183 | simprd 495 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝐹‘(𝑧 + 1)) gcd 𝑁) = 1) | 
| 232 | 230, 231 | eqtrd 2777 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑁 gcd (𝐹‘(𝑧 + 1))) = 1) | 
| 233 |  | rpmul 16696 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧ (seq1(
· , 𝐹)‘𝑧) ∈ ℤ ∧ (𝐹‘(𝑧 + 1)) ∈ ℤ) → (((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 ∧ (𝑁 gcd (𝐹‘(𝑧 + 1))) = 1) → (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1)) | 
| 234 | 229, 156,
186, 233 | syl3anc 1373 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 ∧ (𝑁 gcd (𝐹‘(𝑧 + 1))) = 1) → (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1)) | 
| 235 | 232, 234 | mpan2d 694 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1 → (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1)) | 
| 236 | 199 | oveq2d 7447 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1))))) | 
| 237 | 236 | eqeq1d 2739 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → ((𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1 ↔ (𝑁 gcd ((seq1( · , 𝐹)‘𝑧) · (𝐹‘(𝑧 + 1)))) = 1)) | 
| 238 | 235, 237 | sylibrd 259 | . . . . . . . . . . . . . 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 649 | . . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℕ ∧ (𝜑 ∧ (𝑧 + 1) ≤ (ϕ‘𝑁))) → (((((𝐴↑𝑧) · (seq1( · , 𝐹)‘𝑧)) mod 𝑁) = ((seq1( · , 𝐺)‘𝑧) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘𝑧)) = 1) → ((((𝐴↑(𝑧 + 1)) · (seq1( · , 𝐹)‘(𝑧 + 1))) mod 𝑁) = ((seq1( · , 𝐺)‘(𝑧 + 1)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(𝑧 + 1))) = 1))) | 
| 241 | 240 | ex 412 | . . . . . . . . . . 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 12284 | . . . . . . . 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 687 | . . . . . 6
⊢ (𝜑 → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1)) | 
| 247 | 246 | simpld 494 | . . . . 5
⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁)) | 
| 248 | 3 | nnnn0d 12587 | . . . . . . . 8
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℕ0) | 
| 249 |  | zexpcl 14117 | . . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧
(ϕ‘𝑁) ∈
ℕ0) → (𝐴↑(ϕ‘𝑁)) ∈ ℤ) | 
| 250 | 59, 248, 249 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (𝐴↑(ϕ‘𝑁)) ∈ ℤ) | 
| 251 | 67 | eleq2i 2833 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝑇 ↔ 𝑥 ∈ (1...(ϕ‘𝑁))) | 
| 252 | 251, 151 | sylan2br 595 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(ϕ‘𝑁))) → (𝐹‘𝑥) ∈ ℤ) | 
| 253 | 154 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 · 𝑦) ∈ ℤ) | 
| 254 | 64, 252, 253 | seqcl 14063 | . . . . . . 7
⊢ (𝜑 → (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈
ℤ) | 
| 255 | 250, 254 | zmulcld 12728 | . . . . . 6
⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) ∈
ℤ) | 
| 256 |  | mulcl 11239 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) | 
| 257 | 256 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ) | 
| 258 |  | mulcom 11241 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) | 
| 259 | 258 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) | 
| 260 |  | mulass 11243 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) | 
| 261 | 260 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) | 
| 262 |  | ssidd 4007 | . . . . . . . 8
⊢ (𝜑 → ℂ ⊆
ℂ) | 
| 263 |  | f1ocnv 6860 | . . . . . . . . . . 11
⊢ (𝐹:𝑇–1-1-onto→𝑆 → ◡𝐹:𝑆–1-1-onto→𝑇) | 
| 264 | 60, 263 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → ◡𝐹:𝑆–1-1-onto→𝑇) | 
| 265 | 2 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑁 ∈ ℕ) | 
| 266 | 59 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝐴 ∈ ℤ) | 
| 267 | 62 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑇) → (𝐹‘𝑦) ∈ 𝑆) | 
| 268 | 267 | adantrr 717 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ 𝑆) | 
| 269 | 159, 268 | sselid 3981 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ (0..^𝑁)) | 
| 270 |  | elfzoelz 13699 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑦) ∈ (0..^𝑁) → (𝐹‘𝑦) ∈ ℤ) | 
| 271 | 269, 270 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ ℤ) | 
| 272 | 266, 271 | zmulcld 12728 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐴 · (𝐹‘𝑦)) ∈ ℤ) | 
| 273 | 62 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑇) → (𝐹‘𝑧) ∈ 𝑆) | 
| 274 | 273 | adantrl 716 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ 𝑆) | 
| 275 | 159, 274 | sselid 3981 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ (0..^𝑁)) | 
| 276 |  | elfzoelz 13699 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑧) ∈ (0..^𝑁) → (𝐹‘𝑧) ∈ ℤ) | 
| 277 | 275, 276 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ ℤ) | 
| 278 | 266, 277 | zmulcld 12728 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐴 · (𝐹‘𝑧)) ∈ ℤ) | 
| 279 |  | moddvds 16301 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 · (𝐹‘𝑦)) ∈ ℤ ∧ (𝐴 · (𝐹‘𝑧)) ∈ ℤ) → (((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁) ↔ 𝑁 ∥ ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧))))) | 
| 280 | 265, 272,
278, 279 | syl3anc 1373 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁) ↔ 𝑁 ∥ ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧))))) | 
| 281 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) | 
| 282 | 281 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘𝑦))) | 
| 283 | 282 | oveq1d 7446 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘𝑦)) mod 𝑁)) | 
| 284 |  | ovex 7464 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 · (𝐹‘𝑦)) mod 𝑁) ∈ V | 
| 285 | 283, 87, 284 | fvmpt 7016 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝑇 → (𝐺‘𝑦) = ((𝐴 · (𝐹‘𝑦)) mod 𝑁)) | 
| 286 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) | 
| 287 | 286 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑧 → (𝐴 · (𝐹‘𝑥)) = (𝐴 · (𝐹‘𝑧))) | 
| 288 | 287 | oveq1d 7446 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑧 → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁)) | 
| 289 |  | ovex 7464 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 · (𝐹‘𝑧)) mod 𝑁) ∈ V | 
| 290 | 288, 87, 289 | fvmpt 7016 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑇 → (𝐺‘𝑧) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁)) | 
| 291 | 285, 290 | eqeqan12d 2751 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇) → ((𝐺‘𝑦) = (𝐺‘𝑧) ↔ ((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁))) | 
| 292 | 291 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐺‘𝑦) = (𝐺‘𝑧) ↔ ((𝐴 · (𝐹‘𝑦)) mod 𝑁) = ((𝐴 · (𝐹‘𝑧)) mod 𝑁))) | 
| 293 | 93 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝐴 ∈ ℂ) | 
| 294 | 271 | zcnd 12723 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ ℂ) | 
| 295 | 277 | zcnd 12723 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ ℂ) | 
| 296 | 293, 294,
295 | subdid 11719 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) = ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧)))) | 
| 297 | 296 | breq2d 5155 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ↔ 𝑁 ∥ ((𝐴 · (𝐹‘𝑦)) − (𝐴 · (𝐹‘𝑧))))) | 
| 298 | 280, 292,
297 | 3bitr4d 311 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐺‘𝑦) = (𝐺‘𝑧) ↔ 𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))))) | 
| 299 | 102, 59 | gcdcomd 16551 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 gcd 𝐴) = (𝐴 gcd 𝑁)) | 
| 300 | 1 | simp3d 1145 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 gcd 𝑁) = 1) | 
| 301 | 299, 300 | eqtrd 2777 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 gcd 𝐴) = 1) | 
| 302 | 301 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 gcd 𝐴) = 1) | 
| 303 | 102 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑁 ∈ ℤ) | 
| 304 | 271, 277 | zsubcld 12727 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) − (𝐹‘𝑧)) ∈ ℤ) | 
| 305 |  | coprmdvds 16690 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ((𝐹‘𝑦) − (𝐹‘𝑧)) ∈ ℤ) → ((𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ∧ (𝑁 gcd 𝐴) = 1) → 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧)))) | 
| 306 | 303, 266,
304, 305 | syl3anc 1373 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ∧ (𝑁 gcd 𝐴) = 1) → 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧)))) | 
| 307 | 271 | zred 12722 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) ∈ ℝ) | 
| 308 | 80 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑁 ∈
ℝ+) | 
| 309 |  | elfzole1 13707 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑦) ∈ (0..^𝑁) → 0 ≤ (𝐹‘𝑦)) | 
| 310 | 269, 309 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 0 ≤ (𝐹‘𝑦)) | 
| 311 |  | elfzolt2 13708 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑦) ∈ (0..^𝑁) → (𝐹‘𝑦) < 𝑁) | 
| 312 | 269, 311 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑦) < 𝑁) | 
| 313 |  | modid 13936 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑦) ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (0 ≤
(𝐹‘𝑦) ∧ (𝐹‘𝑦) < 𝑁)) → ((𝐹‘𝑦) mod 𝑁) = (𝐹‘𝑦)) | 
| 314 | 307, 308,
310, 312, 313 | syl22anc 839 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) mod 𝑁) = (𝐹‘𝑦)) | 
| 315 | 277 | zred 12722 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) ∈ ℝ) | 
| 316 |  | elfzole1 13707 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑧) ∈ (0..^𝑁) → 0 ≤ (𝐹‘𝑧)) | 
| 317 | 275, 316 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 0 ≤ (𝐹‘𝑧)) | 
| 318 |  | elfzolt2 13708 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑧) ∈ (0..^𝑁) → (𝐹‘𝑧) < 𝑁) | 
| 319 | 275, 318 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝐹‘𝑧) < 𝑁) | 
| 320 |  | modid 13936 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑧) ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (0 ≤
(𝐹‘𝑧) ∧ (𝐹‘𝑧) < 𝑁)) → ((𝐹‘𝑧) mod 𝑁) = (𝐹‘𝑧)) | 
| 321 | 315, 308,
317, 319, 320 | syl22anc 839 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑧) mod 𝑁) = (𝐹‘𝑧)) | 
| 322 | 314, 321 | eqeq12d 2753 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((𝐹‘𝑦) mod 𝑁) = ((𝐹‘𝑧) mod 𝑁) ↔ (𝐹‘𝑦) = (𝐹‘𝑧))) | 
| 323 |  | moddvds 16301 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ (𝐹‘𝑦) ∈ ℤ ∧ (𝐹‘𝑧) ∈ ℤ) → (((𝐹‘𝑦) mod 𝑁) = ((𝐹‘𝑧) mod 𝑁) ↔ 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧)))) | 
| 324 | 265, 271,
277, 323 | syl3anc 1373 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((𝐹‘𝑦) mod 𝑁) = ((𝐹‘𝑧) mod 𝑁) ↔ 𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧)))) | 
| 325 |  | f1of1 6847 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝐹:𝑇–1-1→𝑆) | 
| 326 | 60, 325 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹:𝑇–1-1→𝑆) | 
| 327 |  | f1fveq 7282 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝑇–1-1→𝑆 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ 𝑦 = 𝑧)) | 
| 328 | 326, 327 | sylan 580 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ 𝑦 = 𝑧)) | 
| 329 | 322, 324,
328 | 3bitr3d 309 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 ∥ ((𝐹‘𝑦) − (𝐹‘𝑧)) ↔ 𝑦 = 𝑧)) | 
| 330 | 306, 329 | sylibd 239 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) ∧ (𝑁 gcd 𝐴) = 1) → 𝑦 = 𝑧)) | 
| 331 | 302, 330 | mpan2d 694 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑁 ∥ (𝐴 · ((𝐹‘𝑦) − (𝐹‘𝑧))) → 𝑦 = 𝑧)) | 
| 332 | 298, 331 | sylbid 240 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐺‘𝑦) = (𝐺‘𝑧) → 𝑦 = 𝑧)) | 
| 333 | 332 | ralrimivva 3202 | . . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑦 ∈ 𝑇 ∀𝑧 ∈ 𝑇 ((𝐺‘𝑦) = (𝐺‘𝑧) → 𝑦 = 𝑧)) | 
| 334 |  | dff13 7275 | . . . . . . . . . . . 12
⊢ (𝐺:𝑇–1-1→𝑆 ↔ (𝐺:𝑇⟶𝑆 ∧ ∀𝑦 ∈ 𝑇 ∀𝑧 ∈ 𝑇 ((𝐺‘𝑦) = (𝐺‘𝑧) → 𝑦 = 𝑧))) | 
| 335 | 160, 333,
334 | sylanbrc 583 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐺:𝑇–1-1→𝑆) | 
| 336 | 67 | ovexi 7465 | . . . . . . . . . . . . . 14
⊢ 𝑇 ∈ V | 
| 337 | 336 | f1oen 9013 | . . . . . . . . . . . . 13
⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝑇 ≈ 𝑆) | 
| 338 | 60, 337 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ≈ 𝑆) | 
| 339 |  | fzofi 14015 | . . . . . . . . . . . . 13
⊢
(0..^𝑁) ∈
Fin | 
| 340 |  | ssfi 9213 | . . . . . . . . . . . . 13
⊢
(((0..^𝑁) ∈ Fin
∧ 𝑆 ⊆ (0..^𝑁)) → 𝑆 ∈ Fin) | 
| 341 | 339, 159,
340 | mp2an 692 | . . . . . . . . . . . 12
⊢ 𝑆 ∈ Fin | 
| 342 |  | f1finf1o 9305 | . . . . . . . . . . . 12
⊢ ((𝑇 ≈ 𝑆 ∧ 𝑆 ∈ Fin) → (𝐺:𝑇–1-1→𝑆 ↔ 𝐺:𝑇–1-1-onto→𝑆)) | 
| 343 | 338, 341,
342 | sylancl 586 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐺:𝑇–1-1→𝑆 ↔ 𝐺:𝑇–1-1-onto→𝑆)) | 
| 344 | 335, 343 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → 𝐺:𝑇–1-1-onto→𝑆) | 
| 345 |  | f1oco 6871 | . . . . . . . . . 10
⊢ ((◡𝐹:𝑆–1-1-onto→𝑇 ∧ 𝐺:𝑇–1-1-onto→𝑆) → (◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇) | 
| 346 | 264, 344,
345 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇) | 
| 347 |  | f1oeq23 6839 | . . . . . . . . . 10
⊢ ((𝑇 = (1...(ϕ‘𝑁)) ∧ 𝑇 = (1...(ϕ‘𝑁))) → ((◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇 ↔ (◡𝐹 ∘ 𝐺):(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁)))) | 
| 348 | 67, 67, 347 | mp2an 692 | . . . . . . . . 9
⊢ ((◡𝐹 ∘ 𝐺):𝑇–1-1-onto→𝑇 ↔ (◡𝐹 ∘ 𝐺):(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁))) | 
| 349 | 346, 348 | sylib 218 | . . . . . . . 8
⊢ (𝜑 → (◡𝐹 ∘ 𝐺):(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁))) | 
| 350 | 252 | zcnd 12723 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(ϕ‘𝑁))) → (𝐹‘𝑥) ∈ ℂ) | 
| 351 | 67 | eleq2i 2833 | . . . . . . . . 9
⊢ (𝑤 ∈ 𝑇 ↔ 𝑤 ∈ (1...(ϕ‘𝑁))) | 
| 352 |  | fvco3 7008 | . . . . . . . . . . . 12
⊢ ((𝐺:𝑇⟶𝑆 ∧ 𝑤 ∈ 𝑇) → ((◡𝐹 ∘ 𝐺)‘𝑤) = (◡𝐹‘(𝐺‘𝑤))) | 
| 353 | 160, 352 | sylan 580 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((◡𝐹 ∘ 𝐺)‘𝑤) = (◡𝐹‘(𝐺‘𝑤))) | 
| 354 | 353 | fveq2d 6910 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐹‘((◡𝐹 ∘ 𝐺)‘𝑤)) = (𝐹‘(◡𝐹‘(𝐺‘𝑤)))) | 
| 355 | 60 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝐹:𝑇–1-1-onto→𝑆) | 
| 356 | 160 | ffvelcdmda 7104 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐺‘𝑤) ∈ 𝑆) | 
| 357 |  | f1ocnvfv2 7297 | . . . . . . . . . . 11
⊢ ((𝐹:𝑇–1-1-onto→𝑆 ∧ (𝐺‘𝑤) ∈ 𝑆) → (𝐹‘(◡𝐹‘(𝐺‘𝑤))) = (𝐺‘𝑤)) | 
| 358 | 355, 356,
357 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐹‘(◡𝐹‘(𝐺‘𝑤))) = (𝐺‘𝑤)) | 
| 359 | 354, 358 | eqtr2d 2778 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝐺‘𝑤) = (𝐹‘((◡𝐹 ∘ 𝐺)‘𝑤))) | 
| 360 | 351, 359 | sylan2br 595 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (1...(ϕ‘𝑁))) → (𝐺‘𝑤) = (𝐹‘((◡𝐹 ∘ 𝐺)‘𝑤))) | 
| 361 | 257, 259,
261, 64, 262, 349, 350, 360 | seqf1o 14084 | . . . . . . 7
⊢ (𝜑 → (seq1( · , 𝐺)‘(ϕ‘𝑁)) = (seq1( · , 𝐹)‘(ϕ‘𝑁))) | 
| 362 | 361, 254 | eqeltrd 2841 | . . . . . 6
⊢ (𝜑 → (seq1( · , 𝐺)‘(ϕ‘𝑁)) ∈
ℤ) | 
| 363 |  | moddvds 16301 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴↑(ϕ‘𝑁)) · (seq1( · ,
𝐹)‘(ϕ‘𝑁))) ∈ ℤ ∧ (seq1( · ,
𝐺)‘(ϕ‘𝑁)) ∈ ℤ) → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · ,
𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ↔ 𝑁 ∥ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · ,
𝐺)‘(ϕ‘𝑁))))) | 
| 364 | 2, 255, 362, 363 | syl3anc 1373 | . . . . 5
⊢ (𝜑 → ((((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) mod 𝑁) = ((seq1( · , 𝐺)‘(ϕ‘𝑁)) mod 𝑁) ↔ 𝑁 ∥ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · ,
𝐺)‘(ϕ‘𝑁))))) | 
| 365 | 247, 364 | mpbid 232 | . . . 4
⊢ (𝜑 → 𝑁 ∥ (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · ,
𝐺)‘(ϕ‘𝑁)))) | 
| 366 | 254 | zcnd 12723 | . . . . . . . 8
⊢ (𝜑 → (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈
ℂ) | 
| 367 | 366 | mullidd 11279 | . . . . . . 7
⊢ (𝜑 → (1 · (seq1(
· , 𝐹)‘(ϕ‘𝑁))) = (seq1( · , 𝐹)‘(ϕ‘𝑁))) | 
| 368 | 361, 367 | eqtr4d 2780 | . . . . . 6
⊢ (𝜑 → (seq1( · , 𝐺)‘(ϕ‘𝑁)) = (1 · (seq1( ·
, 𝐹)‘(ϕ‘𝑁)))) | 
| 369 | 368 | oveq2d 7447 | . . . . 5
⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · ,
𝐺)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1(
· , 𝐹)‘(ϕ‘𝑁))))) | 
| 370 | 250 | zcnd 12723 | . . . . . 6
⊢ (𝜑 → (𝐴↑(ϕ‘𝑁)) ∈ ℂ) | 
| 371 |  | ax-1cn 11213 | . . . . . . 7
⊢ 1 ∈
ℂ | 
| 372 |  | subdir 11697 | . . . . . . 7
⊢ (((𝐴↑(ϕ‘𝑁)) ∈ ℂ ∧ 1 ∈
ℂ ∧ (seq1( · , 𝐹)‘(ϕ‘𝑁)) ∈ ℂ) → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1(
· , 𝐹)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1(
· , 𝐹)‘(ϕ‘𝑁))))) | 
| 373 | 371, 372 | mp3an2 1451 | . . . . . 6
⊢ (((𝐴↑(ϕ‘𝑁)) ∈ ℂ ∧ (seq1(
· , 𝐹)‘(ϕ‘𝑁)) ∈ ℂ) → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1(
· , 𝐹)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1(
· , 𝐹)‘(ϕ‘𝑁))))) | 
| 374 | 370, 366,
373 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1( · ,
𝐹)‘(ϕ‘𝑁))) = (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (1 · (seq1(
· , 𝐹)‘(ϕ‘𝑁))))) | 
| 375 |  | zsubcl 12659 | . . . . . . . 8
⊢ (((𝐴↑(ϕ‘𝑁)) ∈ ℤ ∧ 1 ∈
ℤ) → ((𝐴↑(ϕ‘𝑁)) − 1) ∈
ℤ) | 
| 376 | 250, 83, 375 | sylancl 586 | . . . . . . 7
⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) − 1) ∈
ℤ) | 
| 377 | 376 | zcnd 12723 | . . . . . 6
⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) − 1) ∈
ℂ) | 
| 378 | 377, 366 | mulcomd 11282 | . . . . 5
⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) − 1) · (seq1( · ,
𝐹)‘(ϕ‘𝑁))) = ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1))) | 
| 379 | 369, 374,
378 | 3eqtr2d 2783 | . . . 4
⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) · (seq1( · , 𝐹)‘(ϕ‘𝑁))) − (seq1( · ,
𝐺)‘(ϕ‘𝑁))) = ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1))) | 
| 380 | 365, 379 | breqtrd 5169 | . . 3
⊢ (𝜑 → 𝑁 ∥ ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1))) | 
| 381 | 246 | simprd 495 | . . 3
⊢ (𝜑 → (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1) | 
| 382 |  | coprmdvds 16690 | . . . 4
⊢ ((𝑁 ∈ ℤ ∧ (seq1(
· , 𝐹)‘(ϕ‘𝑁)) ∈ ℤ ∧ ((𝐴↑(ϕ‘𝑁)) − 1) ∈ ℤ) → ((𝑁 ∥ ((seq1( · ,
𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1) → 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1))) | 
| 383 | 102, 254,
376, 382 | syl3anc 1373 | . . 3
⊢ (𝜑 → ((𝑁 ∥ ((seq1( · , 𝐹)‘(ϕ‘𝑁)) · ((𝐴↑(ϕ‘𝑁)) − 1)) ∧ (𝑁 gcd (seq1( · , 𝐹)‘(ϕ‘𝑁))) = 1) → 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1))) | 
| 384 | 380, 381,
383 | mp2and 699 | . 2
⊢ (𝜑 → 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1)) | 
| 385 |  | moddvds 16301 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑁)) ∈ ℤ ∧ 1 ∈
ℤ) → (((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1))) | 
| 386 | 83, 385 | mp3an3 1452 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑁)) ∈ ℤ) →
(((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1))) | 
| 387 | 2, 250, 386 | syl2anc 584 | . 2
⊢ (𝜑 → (((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(ϕ‘𝑁)) − 1))) | 
| 388 | 384, 387 | mpbird 257 | 1
⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁)) |