Proof of Theorem eulerthlem1
Step | Hyp | Ref
| Expression |
1 | | eulerth.1 |
. . . . . . 7
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1)) |
2 | 1 | simp2d 1139 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℤ) |
3 | 2 | adantr 483 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → 𝐴 ∈ ℤ) |
4 | | eulerth.4 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑇–1-1-onto→𝑆) |
5 | | f1of 6610 |
. . . . . . . . . 10
⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝐹:𝑇⟶𝑆) |
6 | 4, 5 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑇⟶𝑆) |
7 | 6 | ffvelrnda 6846 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ 𝑆) |
8 | | oveq1 7157 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑥) → (𝑦 gcd 𝑁) = ((𝐹‘𝑥) gcd 𝑁)) |
9 | 8 | eqeq1d 2823 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑥) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘𝑥) gcd 𝑁) = 1)) |
10 | | eulerth.2 |
. . . . . . . . 9
⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} |
11 | 9, 10 | elrab2 3683 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ∈ 𝑆 ↔ ((𝐹‘𝑥) ∈ (0..^𝑁) ∧ ((𝐹‘𝑥) gcd 𝑁) = 1)) |
12 | 7, 11 | sylib 220 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → ((𝐹‘𝑥) ∈ (0..^𝑁) ∧ ((𝐹‘𝑥) gcd 𝑁) = 1)) |
13 | 12 | simpld 497 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ (0..^𝑁)) |
14 | | elfzoelz 13032 |
. . . . . 6
⊢ ((𝐹‘𝑥) ∈ (0..^𝑁) → (𝐹‘𝑥) ∈ ℤ) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ ℤ) |
16 | 3, 15 | zmulcld 12087 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐴 · (𝐹‘𝑥)) ∈ ℤ) |
17 | 1 | simp1d 1138 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
18 | 17 | adantr 483 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → 𝑁 ∈ ℕ) |
19 | | zmodfzo 13256 |
. . . 4
⊢ (((𝐴 · (𝐹‘𝑥)) ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ (0..^𝑁)) |
20 | 16, 18, 19 | syl2anc 586 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ (0..^𝑁)) |
21 | | modgcd 15874 |
. . . . 5
⊢ (((𝐴 · (𝐹‘𝑥)) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴 · (𝐹‘𝑥)) mod 𝑁) gcd 𝑁) = ((𝐴 · (𝐹‘𝑥)) gcd 𝑁)) |
22 | 16, 18, 21 | syl2anc 586 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (((𝐴 · (𝐹‘𝑥)) mod 𝑁) gcd 𝑁) = ((𝐴 · (𝐹‘𝑥)) gcd 𝑁)) |
23 | 17 | nnzd 12080 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℤ) |
24 | 23 | adantr 483 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → 𝑁 ∈ ℤ) |
25 | | gcdcom 15856 |
. . . . 5
⊢ (((𝐴 · (𝐹‘𝑥)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 · (𝐹‘𝑥)) gcd 𝑁) = (𝑁 gcd (𝐴 · (𝐹‘𝑥)))) |
26 | 16, 24, 25 | syl2anc 586 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → ((𝐴 · (𝐹‘𝑥)) gcd 𝑁) = (𝑁 gcd (𝐴 · (𝐹‘𝑥)))) |
27 | | gcdcom 15856 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑁 gcd 𝐴) = (𝐴 gcd 𝑁)) |
28 | 23, 2, 27 | syl2anc 586 |
. . . . . . 7
⊢ (𝜑 → (𝑁 gcd 𝐴) = (𝐴 gcd 𝑁)) |
29 | 1 | simp3d 1140 |
. . . . . . 7
⊢ (𝜑 → (𝐴 gcd 𝑁) = 1) |
30 | 28, 29 | eqtrd 2856 |
. . . . . 6
⊢ (𝜑 → (𝑁 gcd 𝐴) = 1) |
31 | 30 | adantr 483 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝑁 gcd 𝐴) = 1) |
32 | | gcdcom 15856 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ (𝐹‘𝑥) ∈ ℤ) → (𝑁 gcd (𝐹‘𝑥)) = ((𝐹‘𝑥) gcd 𝑁)) |
33 | 24, 15, 32 | syl2anc 586 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝑁 gcd (𝐹‘𝑥)) = ((𝐹‘𝑥) gcd 𝑁)) |
34 | 12 | simprd 498 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → ((𝐹‘𝑥) gcd 𝑁) = 1) |
35 | 33, 34 | eqtrd 2856 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝑁 gcd (𝐹‘𝑥)) = 1) |
36 | | rpmul 15997 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ (𝐹‘𝑥) ∈ ℤ) → (((𝑁 gcd 𝐴) = 1 ∧ (𝑁 gcd (𝐹‘𝑥)) = 1) → (𝑁 gcd (𝐴 · (𝐹‘𝑥))) = 1)) |
37 | 24, 3, 15, 36 | syl3anc 1367 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (((𝑁 gcd 𝐴) = 1 ∧ (𝑁 gcd (𝐹‘𝑥)) = 1) → (𝑁 gcd (𝐴 · (𝐹‘𝑥))) = 1)) |
38 | 31, 35, 37 | mp2and 697 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝑁 gcd (𝐴 · (𝐹‘𝑥))) = 1) |
39 | 22, 26, 38 | 3eqtrd 2860 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (((𝐴 · (𝐹‘𝑥)) mod 𝑁) gcd 𝑁) = 1) |
40 | | oveq1 7157 |
. . . . 5
⊢ (𝑦 = ((𝐴 · (𝐹‘𝑥)) mod 𝑁) → (𝑦 gcd 𝑁) = (((𝐴 · (𝐹‘𝑥)) mod 𝑁) gcd 𝑁)) |
41 | 40 | eqeq1d 2823 |
. . . 4
⊢ (𝑦 = ((𝐴 · (𝐹‘𝑥)) mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ (((𝐴 · (𝐹‘𝑥)) mod 𝑁) gcd 𝑁) = 1)) |
42 | 41, 10 | elrab2 3683 |
. . 3
⊢ (((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ 𝑆 ↔ (((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ (0..^𝑁) ∧ (((𝐴 · (𝐹‘𝑥)) mod 𝑁) gcd 𝑁) = 1)) |
43 | 20, 39, 42 | sylanbrc 585 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ 𝑆) |
44 | | eulerth.5 |
. 2
⊢ 𝐺 = (𝑥 ∈ 𝑇 ↦ ((𝐴 · (𝐹‘𝑥)) mod 𝑁)) |
45 | 43, 44 | fmptd 6873 |
1
⊢ (𝜑 → 𝐺:𝑇⟶𝑆) |