Proof of Theorem eulerthlem1
| Step | Hyp | Ref
| Expression |
| 1 | | eulerth.1 |
. . . . . . 7
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1)) |
| 2 | 1 | simp2d 1144 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℤ) |
| 3 | 2 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → 𝐴 ∈ ℤ) |
| 4 | | eulerth.4 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑇–1-1-onto→𝑆) |
| 5 | | f1of 6848 |
. . . . . . . . . 10
⊢ (𝐹:𝑇–1-1-onto→𝑆 → 𝐹:𝑇⟶𝑆) |
| 6 | 4, 5 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑇⟶𝑆) |
| 7 | 6 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ 𝑆) |
| 8 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑥) → (𝑦 gcd 𝑁) = ((𝐹‘𝑥) gcd 𝑁)) |
| 9 | 8 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑥) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘𝑥) gcd 𝑁) = 1)) |
| 10 | | eulerth.2 |
. . . . . . . . 9
⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} |
| 11 | 9, 10 | elrab2 3695 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ∈ 𝑆 ↔ ((𝐹‘𝑥) ∈ (0..^𝑁) ∧ ((𝐹‘𝑥) gcd 𝑁) = 1)) |
| 12 | 7, 11 | sylib 218 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → ((𝐹‘𝑥) ∈ (0..^𝑁) ∧ ((𝐹‘𝑥) gcd 𝑁) = 1)) |
| 13 | 12 | simpld 494 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ (0..^𝑁)) |
| 14 | | elfzoelz 13699 |
. . . . . 6
⊢ ((𝐹‘𝑥) ∈ (0..^𝑁) → (𝐹‘𝑥) ∈ ℤ) |
| 15 | 13, 14 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐹‘𝑥) ∈ ℤ) |
| 16 | 3, 15 | zmulcld 12728 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝐴 · (𝐹‘𝑥)) ∈ ℤ) |
| 17 | 1 | simp1d 1143 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 18 | 17 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → 𝑁 ∈ ℕ) |
| 19 | | zmodfzo 13934 |
. . . 4
⊢ (((𝐴 · (𝐹‘𝑥)) ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ (0..^𝑁)) |
| 20 | 16, 18, 19 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ (0..^𝑁)) |
| 21 | | modgcd 16569 |
. . . . 5
⊢ (((𝐴 · (𝐹‘𝑥)) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴 · (𝐹‘𝑥)) mod 𝑁) gcd 𝑁) = ((𝐴 · (𝐹‘𝑥)) gcd 𝑁)) |
| 22 | 16, 18, 21 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (((𝐴 · (𝐹‘𝑥)) mod 𝑁) gcd 𝑁) = ((𝐴 · (𝐹‘𝑥)) gcd 𝑁)) |
| 23 | 17 | nnzd 12640 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 24 | 23 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → 𝑁 ∈ ℤ) |
| 25 | 16, 24 | gcdcomd 16551 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → ((𝐴 · (𝐹‘𝑥)) gcd 𝑁) = (𝑁 gcd (𝐴 · (𝐹‘𝑥)))) |
| 26 | 23, 2 | gcdcomd 16551 |
. . . . . . 7
⊢ (𝜑 → (𝑁 gcd 𝐴) = (𝐴 gcd 𝑁)) |
| 27 | 1 | simp3d 1145 |
. . . . . . 7
⊢ (𝜑 → (𝐴 gcd 𝑁) = 1) |
| 28 | 26, 27 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → (𝑁 gcd 𝐴) = 1) |
| 29 | 28 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝑁 gcd 𝐴) = 1) |
| 30 | 24, 15 | gcdcomd 16551 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝑁 gcd (𝐹‘𝑥)) = ((𝐹‘𝑥) gcd 𝑁)) |
| 31 | 12 | simprd 495 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → ((𝐹‘𝑥) gcd 𝑁) = 1) |
| 32 | 30, 31 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝑁 gcd (𝐹‘𝑥)) = 1) |
| 33 | | rpmul 16696 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ (𝐹‘𝑥) ∈ ℤ) → (((𝑁 gcd 𝐴) = 1 ∧ (𝑁 gcd (𝐹‘𝑥)) = 1) → (𝑁 gcd (𝐴 · (𝐹‘𝑥))) = 1)) |
| 34 | 24, 3, 15, 33 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (((𝑁 gcd 𝐴) = 1 ∧ (𝑁 gcd (𝐹‘𝑥)) = 1) → (𝑁 gcd (𝐴 · (𝐹‘𝑥))) = 1)) |
| 35 | 29, 32, 34 | mp2and 699 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝑁 gcd (𝐴 · (𝐹‘𝑥))) = 1) |
| 36 | 22, 25, 35 | 3eqtrd 2781 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (((𝐴 · (𝐹‘𝑥)) mod 𝑁) gcd 𝑁) = 1) |
| 37 | | oveq1 7438 |
. . . . 5
⊢ (𝑦 = ((𝐴 · (𝐹‘𝑥)) mod 𝑁) → (𝑦 gcd 𝑁) = (((𝐴 · (𝐹‘𝑥)) mod 𝑁) gcd 𝑁)) |
| 38 | 37 | eqeq1d 2739 |
. . . 4
⊢ (𝑦 = ((𝐴 · (𝐹‘𝑥)) mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ (((𝐴 · (𝐹‘𝑥)) mod 𝑁) gcd 𝑁) = 1)) |
| 39 | 38, 10 | elrab2 3695 |
. . 3
⊢ (((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ 𝑆 ↔ (((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ (0..^𝑁) ∧ (((𝐴 · (𝐹‘𝑥)) mod 𝑁) gcd 𝑁) = 1)) |
| 40 | 20, 36, 39 | sylanbrc 583 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → ((𝐴 · (𝐹‘𝑥)) mod 𝑁) ∈ 𝑆) |
| 41 | | eulerth.5 |
. 2
⊢ 𝐺 = (𝑥 ∈ 𝑇 ↦ ((𝐴 · (𝐹‘𝑥)) mod 𝑁)) |
| 42 | 40, 41 | fmptd 7134 |
1
⊢ (𝜑 → 𝐺:𝑇⟶𝑆) |