Step | Hyp | Ref
| Expression |
1 | | phimul.4 |
. . . . 5
⊢ 𝑈 = {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} |
2 | | fzofi 13192 |
. . . . . 6
⊢
(0..^𝑀) ∈
Fin |
3 | | ssrab2 3977 |
. . . . . 6
⊢ {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ⊆ (0..^𝑀) |
4 | | ssfi 8584 |
. . . . . 6
⊢
(((0..^𝑀) ∈ Fin
∧ {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ⊆ (0..^𝑀)) → {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ∈ Fin) |
5 | 2, 3, 4 | mp2an 688 |
. . . . 5
⊢ {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ∈ Fin |
6 | 1, 5 | eqeltri 2879 |
. . . 4
⊢ 𝑈 ∈ Fin |
7 | | phimul.5 |
. . . . 5
⊢ 𝑉 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} |
8 | | fzofi 13192 |
. . . . . 6
⊢
(0..^𝑁) ∈
Fin |
9 | | ssrab2 3977 |
. . . . . 6
⊢ {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁) |
10 | | ssfi 8584 |
. . . . . 6
⊢
(((0..^𝑁) ∈ Fin
∧ {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁)) → {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ∈ Fin) |
11 | 8, 9, 10 | mp2an 688 |
. . . . 5
⊢ {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ∈ Fin |
12 | 7, 11 | eqeltri 2879 |
. . . 4
⊢ 𝑉 ∈ Fin |
13 | | hashxp 13643 |
. . . 4
⊢ ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) →
(♯‘(𝑈 ×
𝑉)) = ((♯‘𝑈) · (♯‘𝑉))) |
14 | 6, 12, 13 | mp2an 688 |
. . 3
⊢
(♯‘(𝑈
× 𝑉)) =
((♯‘𝑈) ·
(♯‘𝑉)) |
15 | | oveq1 7023 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑤 → (𝑦 gcd (𝑀 · 𝑁)) = (𝑤 gcd (𝑀 · 𝑁))) |
16 | 15 | eqeq1d 2797 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑤 → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ (𝑤 gcd (𝑀 · 𝑁)) = 1)) |
17 | | phimul.6 |
. . . . . . . . . . . . 13
⊢ 𝑊 = {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} |
18 | 16, 17 | elrab2 3621 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝑊 ↔ (𝑤 ∈ 𝑆 ∧ (𝑤 gcd (𝑀 · 𝑁)) = 1)) |
19 | 18 | simplbi 498 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝑊 → 𝑤 ∈ 𝑆) |
20 | | oveq1 7023 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → (𝑥 mod 𝑀) = (𝑤 mod 𝑀)) |
21 | | oveq1 7023 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → (𝑥 mod 𝑁) = (𝑤 mod 𝑁)) |
22 | 20, 21 | opeq12d 4718 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉 = 〈(𝑤 mod 𝑀), (𝑤 mod 𝑁)〉) |
23 | | crth.3 |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉) |
24 | | opex 5248 |
. . . . . . . . . . . 12
⊢
〈(𝑤 mod 𝑀), (𝑤 mod 𝑁)〉 ∈ V |
25 | 22, 23, 24 | fvmpt 6635 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝑆 → (𝐹‘𝑤) = 〈(𝑤 mod 𝑀), (𝑤 mod 𝑁)〉) |
26 | 19, 25 | syl 17 |
. . . . . . . . . 10
⊢ (𝑤 ∈ 𝑊 → (𝐹‘𝑤) = 〈(𝑤 mod 𝑀), (𝑤 mod 𝑁)〉) |
27 | 26 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝐹‘𝑤) = 〈(𝑤 mod 𝑀), (𝑤 mod 𝑁)〉) |
28 | | crth.1 |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = (0..^(𝑀 · 𝑁)) |
29 | 19, 28 | syl6eleq 2893 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ 𝑊 → 𝑤 ∈ (0..^(𝑀 · 𝑁))) |
30 | 29 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑤 ∈ (0..^(𝑀 · 𝑁))) |
31 | | elfzoelz 12888 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (0..^(𝑀 · 𝑁)) → 𝑤 ∈ ℤ) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑤 ∈ ℤ) |
33 | | crth.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1)) |
34 | 33 | simp1d 1135 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℕ) |
35 | 34 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑀 ∈ ℕ) |
36 | | zmodfzo 13112 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑤 mod 𝑀) ∈ (0..^𝑀)) |
37 | 32, 35, 36 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑀) ∈ (0..^𝑀)) |
38 | | modgcd 15713 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀)) |
39 | 32, 35, 38 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀)) |
40 | 35 | nnzd 11935 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑀 ∈ ℤ) |
41 | | gcddvds 15685 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀)) |
42 | 32, 40, 41 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀)) |
43 | 42 | simpld 495 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∥ 𝑤) |
44 | | nnne0 11519 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℕ → 𝑀 ≠ 0) |
45 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 = 0 ∧ 𝑀 = 0) → 𝑀 = 0) |
46 | 45 | necon3ai 3009 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑀 = 0)) |
47 | 35, 44, 46 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ¬ (𝑤 = 0 ∧ 𝑀 = 0)) |
48 | | gcdn0cl 15684 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬
(𝑤 = 0 ∧ 𝑀 = 0)) → (𝑤 gcd 𝑀) ∈ ℕ) |
49 | 32, 40, 47, 48 | syl21anc 834 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∈ ℕ) |
50 | 49 | nnzd 11935 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∈ ℤ) |
51 | 33 | simp2d 1136 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ ℕ) |
52 | 51 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑁 ∈ ℕ) |
53 | 52 | nnzd 11935 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑁 ∈ ℤ) |
54 | 42 | simprd 496 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∥ 𝑀) |
55 | 50, 40, 53, 54 | dvdsmultr1d 15481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) |
56 | 35, 52 | nnmulcld 11538 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑀 · 𝑁) ∈ ℕ) |
57 | 56 | nnzd 11935 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑀 · 𝑁) ∈ ℤ) |
58 | | nnne0 11519 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 · 𝑁) ∈ ℕ → (𝑀 · 𝑁) ≠ 0) |
59 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 = 0 ∧ (𝑀 · 𝑁) = 0) → (𝑀 · 𝑁) = 0) |
60 | 59 | necon3ai 3009 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 · 𝑁) ≠ 0 → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) |
61 | 56, 58, 60 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) |
62 | | dvdslegcd 15686 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑤 gcd 𝑀) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) → (((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁)))) |
63 | 50, 32, 57, 61, 62 | syl31anc 1366 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁)))) |
64 | 43, 55, 63 | mp2and 695 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁))) |
65 | 18 | simprbi 497 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ 𝑊 → (𝑤 gcd (𝑀 · 𝑁)) = 1) |
66 | 65 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd (𝑀 · 𝑁)) = 1) |
67 | 64, 66 | breqtrd 4988 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ≤ 1) |
68 | | nnle1eq1 11515 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 gcd 𝑀) ∈ ℕ → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1)) |
69 | 49, 68 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1)) |
70 | 67, 69 | mpbid 233 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) = 1) |
71 | 39, 70 | eqtrd 2831 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = 1) |
72 | | oveq1 7023 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑤 mod 𝑀) → (𝑦 gcd 𝑀) = ((𝑤 mod 𝑀) gcd 𝑀)) |
73 | 72 | eqeq1d 2797 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑤 mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ ((𝑤 mod 𝑀) gcd 𝑀) = 1)) |
74 | 73, 1 | elrab2 3621 |
. . . . . . . . . . 11
⊢ ((𝑤 mod 𝑀) ∈ 𝑈 ↔ ((𝑤 mod 𝑀) ∈ (0..^𝑀) ∧ ((𝑤 mod 𝑀) gcd 𝑀) = 1)) |
75 | 37, 71, 74 | sylanbrc 583 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑀) ∈ 𝑈) |
76 | | zmodfzo 13112 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑤 mod 𝑁) ∈ (0..^𝑁)) |
77 | 32, 52, 76 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑁) ∈ (0..^𝑁)) |
78 | | modgcd 15713 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁)) |
79 | 32, 52, 78 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁)) |
80 | | gcddvds 15685 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁)) |
81 | 32, 53, 80 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁)) |
82 | 81 | simpld 495 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∥ 𝑤) |
83 | 81 | simprd 496 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∥ 𝑁) |
84 | | dvdsmul2 15465 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑀 · 𝑁)) |
85 | 40, 53, 84 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑁 ∥ (𝑀 · 𝑁)) |
86 | | nnne0 11519 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
87 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤 = 0 ∧ 𝑁 = 0) → 𝑁 = 0) |
88 | 87 | necon3ai 3009 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑁 = 0)) |
89 | 52, 86, 88 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ¬ (𝑤 = 0 ∧ 𝑁 = 0)) |
90 | | gcdn0cl 15684 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑤 = 0 ∧ 𝑁 = 0)) → (𝑤 gcd 𝑁) ∈ ℕ) |
91 | 32, 53, 89, 90 | syl21anc 834 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∈ ℕ) |
92 | 91 | nnzd 11935 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∈ ℤ) |
93 | | dvdstr 15479 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 gcd 𝑁) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑤 gcd 𝑁) ∥ 𝑁 ∧ 𝑁 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁))) |
94 | 92, 53, 57, 93 | syl3anc 1364 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (((𝑤 gcd 𝑁) ∥ 𝑁 ∧ 𝑁 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁))) |
95 | 83, 85, 94 | mp2and 695 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) |
96 | | dvdslegcd 15686 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑤 gcd 𝑁) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) → (((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁)))) |
97 | 92, 32, 57, 61, 96 | syl31anc 1366 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁)))) |
98 | 82, 95, 97 | mp2and 695 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁))) |
99 | 98, 66 | breqtrd 4988 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ≤ 1) |
100 | | nnle1eq1 11515 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 gcd 𝑁) ∈ ℕ → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1)) |
101 | 91, 100 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1)) |
102 | 99, 101 | mpbid 233 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) = 1) |
103 | 79, 102 | eqtrd 2831 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = 1) |
104 | | oveq1 7023 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑤 mod 𝑁) → (𝑦 gcd 𝑁) = ((𝑤 mod 𝑁) gcd 𝑁)) |
105 | 104 | eqeq1d 2797 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑤 mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝑤 mod 𝑁) gcd 𝑁) = 1)) |
106 | 105, 7 | elrab2 3621 |
. . . . . . . . . . 11
⊢ ((𝑤 mod 𝑁) ∈ 𝑉 ↔ ((𝑤 mod 𝑁) ∈ (0..^𝑁) ∧ ((𝑤 mod 𝑁) gcd 𝑁) = 1)) |
107 | 77, 103, 106 | sylanbrc 583 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑁) ∈ 𝑉) |
108 | 75, 107 | opelxpd 5481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 〈(𝑤 mod 𝑀), (𝑤 mod 𝑁)〉 ∈ (𝑈 × 𝑉)) |
109 | 27, 108 | eqeltrd 2883 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝐹‘𝑤) ∈ (𝑈 × 𝑉)) |
110 | 109 | ralrimiva 3149 |
. . . . . . 7
⊢ (𝜑 → ∀𝑤 ∈ 𝑊 (𝐹‘𝑤) ∈ (𝑈 × 𝑉)) |
111 | | crth.2 |
. . . . . . . . . 10
⊢ 𝑇 = ((0..^𝑀) × (0..^𝑁)) |
112 | 28, 111, 23, 33 | crth 15944 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑆–1-1-onto→𝑇) |
113 | | f1ofn 6484 |
. . . . . . . . 9
⊢ (𝐹:𝑆–1-1-onto→𝑇 → 𝐹 Fn 𝑆) |
114 | | fnfun 6323 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝑆 → Fun 𝐹) |
115 | 112, 113,
114 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → Fun 𝐹) |
116 | 17 | ssrab3 3978 |
. . . . . . . . 9
⊢ 𝑊 ⊆ 𝑆 |
117 | | fndm 6325 |
. . . . . . . . . 10
⊢ (𝐹 Fn 𝑆 → dom 𝐹 = 𝑆) |
118 | 112, 113,
117 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = 𝑆) |
119 | 116, 118 | sseqtrrid 3941 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ⊆ dom 𝐹) |
120 | | funimass4 6598 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑊 ⊆ dom 𝐹) → ((𝐹 “ 𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤 ∈ 𝑊 (𝐹‘𝑤) ∈ (𝑈 × 𝑉))) |
121 | 115, 119,
120 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 “ 𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤 ∈ 𝑊 (𝐹‘𝑤) ∈ (𝑈 × 𝑉))) |
122 | 110, 121 | mpbird 258 |
. . . . . 6
⊢ (𝜑 → (𝐹 “ 𝑊) ⊆ (𝑈 × 𝑉)) |
123 | 1 | ssrab3 3978 |
. . . . . . . . . . 11
⊢ 𝑈 ⊆ (0..^𝑀) |
124 | 7 | ssrab3 3978 |
. . . . . . . . . . 11
⊢ 𝑉 ⊆ (0..^𝑁) |
125 | | xpss12 5458 |
. . . . . . . . . . 11
⊢ ((𝑈 ⊆ (0..^𝑀) ∧ 𝑉 ⊆ (0..^𝑁)) → (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁))) |
126 | 123, 124,
125 | mp2an 688 |
. . . . . . . . . 10
⊢ (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁)) |
127 | 126, 111 | sseqtr4i 3925 |
. . . . . . . . 9
⊢ (𝑈 × 𝑉) ⊆ 𝑇 |
128 | 127 | sseli 3885 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝑈 × 𝑉) → 𝑧 ∈ 𝑇) |
129 | | f1ocnvfv2 6899 |
. . . . . . . 8
⊢ ((𝐹:𝑆–1-1-onto→𝑇 ∧ 𝑧 ∈ 𝑇) → (𝐹‘(◡𝐹‘𝑧)) = 𝑧) |
130 | 112, 128,
129 | syl2an 595 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(◡𝐹‘𝑧)) = 𝑧) |
131 | | f1ocnv 6495 |
. . . . . . . . . . 11
⊢ (𝐹:𝑆–1-1-onto→𝑇 → ◡𝐹:𝑇–1-1-onto→𝑆) |
132 | | f1of 6483 |
. . . . . . . . . . 11
⊢ (◡𝐹:𝑇–1-1-onto→𝑆 → ◡𝐹:𝑇⟶𝑆) |
133 | 112, 131,
132 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → ◡𝐹:𝑇⟶𝑆) |
134 | | ffvelrn 6714 |
. . . . . . . . . 10
⊢ ((◡𝐹:𝑇⟶𝑆 ∧ 𝑧 ∈ 𝑇) → (◡𝐹‘𝑧) ∈ 𝑆) |
135 | 133, 128,
134 | syl2an 595 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (◡𝐹‘𝑧) ∈ 𝑆) |
136 | 135, 28 | syl6eleq 2893 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (◡𝐹‘𝑧) ∈ (0..^(𝑀 · 𝑁))) |
137 | | elfzoelz 12888 |
. . . . . . . . . . . . 13
⊢ ((◡𝐹‘𝑧) ∈ (0..^(𝑀 · 𝑁)) → (◡𝐹‘𝑧) ∈ ℤ) |
138 | 136, 137 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (◡𝐹‘𝑧) ∈ ℤ) |
139 | 34 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℕ) |
140 | | modgcd 15713 |
. . . . . . . . . . . 12
⊢ (((◡𝐹‘𝑧) ∈ ℤ ∧ 𝑀 ∈ ℕ) → (((◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = ((◡𝐹‘𝑧) gcd 𝑀)) |
141 | 138, 139,
140 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = ((◡𝐹‘𝑧) gcd 𝑀)) |
142 | | oveq1 7023 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = (◡𝐹‘𝑧) → (𝑤 mod 𝑀) = ((◡𝐹‘𝑧) mod 𝑀)) |
143 | | oveq1 7023 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = (◡𝐹‘𝑧) → (𝑤 mod 𝑁) = ((◡𝐹‘𝑧) mod 𝑁)) |
144 | 142, 143 | opeq12d 4718 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = (◡𝐹‘𝑧) → 〈(𝑤 mod 𝑀), (𝑤 mod 𝑁)〉 = 〈((◡𝐹‘𝑧) mod 𝑀), ((◡𝐹‘𝑧) mod 𝑁)〉) |
145 | 22 | cbvmptv 5061 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝑆 ↦ 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉) = (𝑤 ∈ 𝑆 ↦ 〈(𝑤 mod 𝑀), (𝑤 mod 𝑁)〉) |
146 | 23, 145 | eqtri 2819 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐹 = (𝑤 ∈ 𝑆 ↦ 〈(𝑤 mod 𝑀), (𝑤 mod 𝑁)〉) |
147 | | opex 5248 |
. . . . . . . . . . . . . . . . . . 19
⊢
〈((◡𝐹‘𝑧) mod 𝑀), ((◡𝐹‘𝑧) mod 𝑁)〉 ∈ V |
148 | 144, 146,
147 | fvmpt 6635 |
. . . . . . . . . . . . . . . . . 18
⊢ ((◡𝐹‘𝑧) ∈ 𝑆 → (𝐹‘(◡𝐹‘𝑧)) = 〈((◡𝐹‘𝑧) mod 𝑀), ((◡𝐹‘𝑧) mod 𝑁)〉) |
149 | 135, 148 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(◡𝐹‘𝑧)) = 〈((◡𝐹‘𝑧) mod 𝑀), ((◡𝐹‘𝑧) mod 𝑁)〉) |
150 | 130, 149 | eqtr3d 2833 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 = 〈((◡𝐹‘𝑧) mod 𝑀), ((◡𝐹‘𝑧) mod 𝑁)〉) |
151 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝑈 × 𝑉)) |
152 | 150, 151 | eqeltrrd 2884 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 〈((◡𝐹‘𝑧) mod 𝑀), ((◡𝐹‘𝑧) mod 𝑁)〉 ∈ (𝑈 × 𝑉)) |
153 | | opelxp 5479 |
. . . . . . . . . . . . . . 15
⊢
(〈((◡𝐹‘𝑧) mod 𝑀), ((◡𝐹‘𝑧) mod 𝑁)〉 ∈ (𝑈 × 𝑉) ↔ (((◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈 ∧ ((◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉)) |
154 | 152, 153 | sylib 219 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈 ∧ ((◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉)) |
155 | 154 | simpld 495 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈) |
156 | | oveq1 7023 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ((◡𝐹‘𝑧) mod 𝑀) → (𝑦 gcd 𝑀) = (((◡𝐹‘𝑧) mod 𝑀) gcd 𝑀)) |
157 | 156 | eqeq1d 2797 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ((◡𝐹‘𝑧) mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ (((◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1)) |
158 | 157, 1 | elrab2 3621 |
. . . . . . . . . . . . 13
⊢ (((◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈 ↔ (((◡𝐹‘𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1)) |
159 | 155, 158 | sylib 219 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((◡𝐹‘𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1)) |
160 | 159 | simprd 496 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1) |
161 | 141, 160 | eqtr3d 2833 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((◡𝐹‘𝑧) gcd 𝑀) = 1) |
162 | 51 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℕ) |
163 | | modgcd 15713 |
. . . . . . . . . . . 12
⊢ (((◡𝐹‘𝑧) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = ((◡𝐹‘𝑧) gcd 𝑁)) |
164 | 138, 162,
163 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = ((◡𝐹‘𝑧) gcd 𝑁)) |
165 | 154 | simprd 496 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉) |
166 | | oveq1 7023 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ((◡𝐹‘𝑧) mod 𝑁) → (𝑦 gcd 𝑁) = (((◡𝐹‘𝑧) mod 𝑁) gcd 𝑁)) |
167 | 166 | eqeq1d 2797 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ((◡𝐹‘𝑧) mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ (((◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1)) |
168 | 167, 7 | elrab2 3621 |
. . . . . . . . . . . . 13
⊢ (((◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉 ↔ (((◡𝐹‘𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1)) |
169 | 165, 168 | sylib 219 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((◡𝐹‘𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1)) |
170 | 169 | simprd 496 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1) |
171 | 164, 170 | eqtr3d 2833 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((◡𝐹‘𝑧) gcd 𝑁) = 1) |
172 | 34 | nnzd 11935 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℤ) |
173 | 172 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℤ) |
174 | 51 | nnzd 11935 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℤ) |
175 | 174 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℤ) |
176 | | rpmul 15832 |
. . . . . . . . . . 11
⊢ (((◡𝐹‘𝑧) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((((◡𝐹‘𝑧) gcd 𝑀) = 1 ∧ ((◡𝐹‘𝑧) gcd 𝑁) = 1) → ((◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1)) |
177 | 138, 173,
175, 176 | syl3anc 1364 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((((◡𝐹‘𝑧) gcd 𝑀) = 1 ∧ ((◡𝐹‘𝑧) gcd 𝑁) = 1) → ((◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1)) |
178 | 161, 171,
177 | mp2and 695 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1) |
179 | | oveq1 7023 |
. . . . . . . . . . 11
⊢ (𝑦 = (◡𝐹‘𝑧) → (𝑦 gcd (𝑀 · 𝑁)) = ((◡𝐹‘𝑧) gcd (𝑀 · 𝑁))) |
180 | 179 | eqeq1d 2797 |
. . . . . . . . . 10
⊢ (𝑦 = (◡𝐹‘𝑧) → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ ((◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1)) |
181 | 180, 17 | elrab2 3621 |
. . . . . . . . 9
⊢ ((◡𝐹‘𝑧) ∈ 𝑊 ↔ ((◡𝐹‘𝑧) ∈ 𝑆 ∧ ((◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1)) |
182 | 135, 178,
181 | sylanbrc 583 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (◡𝐹‘𝑧) ∈ 𝑊) |
183 | | funfvima2 6859 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝑊 ⊆ dom 𝐹) → ((◡𝐹‘𝑧) ∈ 𝑊 → (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊))) |
184 | 115, 119,
183 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ((◡𝐹‘𝑧) ∈ 𝑊 → (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊))) |
185 | 184 | imp 407 |
. . . . . . . 8
⊢ ((𝜑 ∧ (◡𝐹‘𝑧) ∈ 𝑊) → (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊)) |
186 | 182, 185 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊)) |
187 | 130, 186 | eqeltrrd 2884 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝐹 “ 𝑊)) |
188 | 122, 187 | eqelssd 3909 |
. . . . 5
⊢ (𝜑 → (𝐹 “ 𝑊) = (𝑈 × 𝑉)) |
189 | | f1of1 6482 |
. . . . . . 7
⊢ (𝐹:𝑆–1-1-onto→𝑇 → 𝐹:𝑆–1-1→𝑇) |
190 | 112, 189 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑆–1-1→𝑇) |
191 | | fzofi 13192 |
. . . . . . . . . 10
⊢
(0..^(𝑀 ·
𝑁)) ∈
Fin |
192 | 28, 191 | eqeltri 2879 |
. . . . . . . . 9
⊢ 𝑆 ∈ Fin |
193 | | ssfi 8584 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Fin ∧ 𝑊 ⊆ 𝑆) → 𝑊 ∈ Fin) |
194 | 192, 116,
193 | mp2an 688 |
. . . . . . . 8
⊢ 𝑊 ∈ Fin |
195 | 194 | elexi 3456 |
. . . . . . 7
⊢ 𝑊 ∈ V |
196 | 195 | f1imaen 8419 |
. . . . . 6
⊢ ((𝐹:𝑆–1-1→𝑇 ∧ 𝑊 ⊆ 𝑆) → (𝐹 “ 𝑊) ≈ 𝑊) |
197 | 190, 116,
196 | sylancl 586 |
. . . . 5
⊢ (𝜑 → (𝐹 “ 𝑊) ≈ 𝑊) |
198 | 188, 197 | eqbrtrrd 4986 |
. . . 4
⊢ (𝜑 → (𝑈 × 𝑉) ≈ 𝑊) |
199 | | xpfi 8635 |
. . . . . 6
⊢ ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) → (𝑈 × 𝑉) ∈ Fin) |
200 | 6, 12, 199 | mp2an 688 |
. . . . 5
⊢ (𝑈 × 𝑉) ∈ Fin |
201 | | hashen 13557 |
. . . . 5
⊢ (((𝑈 × 𝑉) ∈ Fin ∧ 𝑊 ∈ Fin) → ((♯‘(𝑈 × 𝑉)) = (♯‘𝑊) ↔ (𝑈 × 𝑉) ≈ 𝑊)) |
202 | 200, 194,
201 | mp2an 688 |
. . . 4
⊢
((♯‘(𝑈
× 𝑉)) =
(♯‘𝑊) ↔
(𝑈 × 𝑉) ≈ 𝑊) |
203 | 198, 202 | sylibr 235 |
. . 3
⊢ (𝜑 → (♯‘(𝑈 × 𝑉)) = (♯‘𝑊)) |
204 | 14, 203 | syl5reqr 2846 |
. 2
⊢ (𝜑 → (♯‘𝑊) = ((♯‘𝑈) · (♯‘𝑉))) |
205 | 34, 51 | nnmulcld 11538 |
. . 3
⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ) |
206 | | dfphi2 15940 |
. . . 4
⊢ ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (♯‘{𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1})) |
207 | 28 | rabeqi 3427 |
. . . . . 6
⊢ {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} |
208 | 17, 207 | eqtri 2819 |
. . . . 5
⊢ 𝑊 = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} |
209 | 208 | fveq2i 6541 |
. . . 4
⊢
(♯‘𝑊) =
(♯‘{𝑦 ∈
(0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}) |
210 | 206, 209 | syl6eqr 2849 |
. . 3
⊢ ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (♯‘𝑊)) |
211 | 205, 210 | syl 17 |
. 2
⊢ (𝜑 → (ϕ‘(𝑀 · 𝑁)) = (♯‘𝑊)) |
212 | | dfphi2 15940 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
(ϕ‘𝑀) =
(♯‘{𝑦 ∈
(0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1})) |
213 | 1 | fveq2i 6541 |
. . . . 5
⊢
(♯‘𝑈) =
(♯‘{𝑦 ∈
(0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}) |
214 | 212, 213 | syl6eqr 2849 |
. . . 4
⊢ (𝑀 ∈ ℕ →
(ϕ‘𝑀) =
(♯‘𝑈)) |
215 | 34, 214 | syl 17 |
. . 3
⊢ (𝜑 → (ϕ‘𝑀) = (♯‘𝑈)) |
216 | | dfphi2 15940 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(ϕ‘𝑁) =
(♯‘{𝑦 ∈
(0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1})) |
217 | 7 | fveq2i 6541 |
. . . . 5
⊢
(♯‘𝑉) =
(♯‘{𝑦 ∈
(0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}) |
218 | 216, 217 | syl6eqr 2849 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(ϕ‘𝑁) =
(♯‘𝑉)) |
219 | 51, 218 | syl 17 |
. . 3
⊢ (𝜑 → (ϕ‘𝑁) = (♯‘𝑉)) |
220 | 215, 219 | oveq12d 7034 |
. 2
⊢ (𝜑 → ((ϕ‘𝑀) · (ϕ‘𝑁)) = ((♯‘𝑈) · (♯‘𝑉))) |
221 | 204, 211,
220 | 3eqtr4d 2841 |
1
⊢ (𝜑 → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁))) |