Step | Hyp | Ref
| Expression |
1 | | phimul.4 |
. . . . 5
⊢ 𝑈 = {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} |
2 | | fzofi 12981 |
. . . . . 6
⊢
(0..^𝑀) ∈
Fin |
3 | | ssrab2 3836 |
. . . . . 6
⊢ {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ⊆ (0..^𝑀) |
4 | | ssfi 8336 |
. . . . . 6
⊢
(((0..^𝑀) ∈ Fin
∧ {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ⊆ (0..^𝑀)) → {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ∈ Fin) |
5 | 2, 3, 4 | mp2an 672 |
. . . . 5
⊢ {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ∈ Fin |
6 | 1, 5 | eqeltri 2846 |
. . . 4
⊢ 𝑈 ∈ Fin |
7 | | phimul.5 |
. . . . 5
⊢ 𝑉 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} |
8 | | fzofi 12981 |
. . . . . 6
⊢
(0..^𝑁) ∈
Fin |
9 | | ssrab2 3836 |
. . . . . 6
⊢ {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁) |
10 | | ssfi 8336 |
. . . . . 6
⊢
(((0..^𝑁) ∈ Fin
∧ {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁)) → {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ∈ Fin) |
11 | 8, 9, 10 | mp2an 672 |
. . . . 5
⊢ {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ∈ Fin |
12 | 7, 11 | eqeltri 2846 |
. . . 4
⊢ 𝑉 ∈ Fin |
13 | | hashxp 13423 |
. . . 4
⊢ ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) →
(♯‘(𝑈 ×
𝑉)) = ((♯‘𝑈) · (♯‘𝑉))) |
14 | 6, 12, 13 | mp2an 672 |
. . 3
⊢
(♯‘(𝑈
× 𝑉)) =
((♯‘𝑈) ·
(♯‘𝑉)) |
15 | | oveq1 6800 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑤 → (𝑦 gcd (𝑀 · 𝑁)) = (𝑤 gcd (𝑀 · 𝑁))) |
16 | 15 | eqeq1d 2773 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑤 → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ (𝑤 gcd (𝑀 · 𝑁)) = 1)) |
17 | | phimul.6 |
. . . . . . . . . . . . 13
⊢ 𝑊 = {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} |
18 | 16, 17 | elrab2 3518 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝑊 ↔ (𝑤 ∈ 𝑆 ∧ (𝑤 gcd (𝑀 · 𝑁)) = 1)) |
19 | 18 | simplbi 485 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝑊 → 𝑤 ∈ 𝑆) |
20 | | oveq1 6800 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → (𝑥 mod 𝑀) = (𝑤 mod 𝑀)) |
21 | | oveq1 6800 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → (𝑥 mod 𝑁) = (𝑤 mod 𝑁)) |
22 | 20, 21 | opeq12d 4547 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉 = 〈(𝑤 mod 𝑀), (𝑤 mod 𝑁)〉) |
23 | | crth.3 |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉) |
24 | | opex 5060 |
. . . . . . . . . . . 12
⊢
〈(𝑤 mod 𝑀), (𝑤 mod 𝑁)〉 ∈ V |
25 | 22, 23, 24 | fvmpt 6424 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝑆 → (𝐹‘𝑤) = 〈(𝑤 mod 𝑀), (𝑤 mod 𝑁)〉) |
26 | 19, 25 | syl 17 |
. . . . . . . . . 10
⊢ (𝑤 ∈ 𝑊 → (𝐹‘𝑤) = 〈(𝑤 mod 𝑀), (𝑤 mod 𝑁)〉) |
27 | 26 | adantl 467 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝐹‘𝑤) = 〈(𝑤 mod 𝑀), (𝑤 mod 𝑁)〉) |
28 | | crth.1 |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = (0..^(𝑀 · 𝑁)) |
29 | 19, 28 | syl6eleq 2860 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ 𝑊 → 𝑤 ∈ (0..^(𝑀 · 𝑁))) |
30 | 29 | adantl 467 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑤 ∈ (0..^(𝑀 · 𝑁))) |
31 | | elfzoelz 12678 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (0..^(𝑀 · 𝑁)) → 𝑤 ∈ ℤ) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑤 ∈ ℤ) |
33 | | crth.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1)) |
34 | 33 | simp1d 1136 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℕ) |
35 | 34 | adantr 466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑀 ∈ ℕ) |
36 | | zmodfzo 12901 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑤 mod 𝑀) ∈ (0..^𝑀)) |
37 | 32, 35, 36 | syl2anc 573 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑀) ∈ (0..^𝑀)) |
38 | | modgcd 15461 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀)) |
39 | 32, 35, 38 | syl2anc 573 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀)) |
40 | 35 | nnzd 11683 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑀 ∈ ℤ) |
41 | | gcddvds 15433 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀)) |
42 | 32, 40, 41 | syl2anc 573 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀)) |
43 | 42 | simpld 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∥ 𝑤) |
44 | 42 | simprd 483 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∥ 𝑀) |
45 | 33 | simp2d 1137 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℕ) |
46 | 45 | adantr 466 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑁 ∈ ℕ) |
47 | 46 | nnzd 11683 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑁 ∈ ℤ) |
48 | | dvdsmul1 15212 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∥ (𝑀 · 𝑁)) |
49 | 40, 47, 48 | syl2anc 573 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑀 ∥ (𝑀 · 𝑁)) |
50 | | nnne0 11255 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ℕ → 𝑀 ≠ 0) |
51 | | simpr 471 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤 = 0 ∧ 𝑀 = 0) → 𝑀 = 0) |
52 | 51 | necon3ai 2968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑀 = 0)) |
53 | 35, 50, 52 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ¬ (𝑤 = 0 ∧ 𝑀 = 0)) |
54 | | gcdn0cl 15432 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬
(𝑤 = 0 ∧ 𝑀 = 0)) → (𝑤 gcd 𝑀) ∈ ℕ) |
55 | 32, 40, 53, 54 | syl21anc 1475 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∈ ℕ) |
56 | 55 | nnzd 11683 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∈ ℤ) |
57 | 35, 46 | nnmulcld 11270 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑀 · 𝑁) ∈ ℕ) |
58 | 57 | nnzd 11683 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑀 · 𝑁) ∈ ℤ) |
59 | | dvdstr 15227 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 gcd 𝑀) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑤 gcd 𝑀) ∥ 𝑀 ∧ 𝑀 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁))) |
60 | 56, 40, 58, 59 | syl3anc 1476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (((𝑤 gcd 𝑀) ∥ 𝑀 ∧ 𝑀 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁))) |
61 | 44, 49, 60 | mp2and 679 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) |
62 | | nnne0 11255 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 · 𝑁) ∈ ℕ → (𝑀 · 𝑁) ≠ 0) |
63 | | simpr 471 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 = 0 ∧ (𝑀 · 𝑁) = 0) → (𝑀 · 𝑁) = 0) |
64 | 63 | necon3ai 2968 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 · 𝑁) ≠ 0 → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) |
65 | 57, 62, 64 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) |
66 | | dvdslegcd 15434 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑤 gcd 𝑀) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) → (((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁)))) |
67 | 56, 32, 58, 65, 66 | syl31anc 1479 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁)))) |
68 | 43, 61, 67 | mp2and 679 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁))) |
69 | 18 | simprbi 484 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ 𝑊 → (𝑤 gcd (𝑀 · 𝑁)) = 1) |
70 | 69 | adantl 467 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd (𝑀 · 𝑁)) = 1) |
71 | 68, 70 | breqtrd 4812 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ≤ 1) |
72 | | nnle1eq1 11250 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 gcd 𝑀) ∈ ℕ → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1)) |
73 | 55, 72 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1)) |
74 | 71, 73 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) = 1) |
75 | 39, 74 | eqtrd 2805 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = 1) |
76 | | oveq1 6800 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑤 mod 𝑀) → (𝑦 gcd 𝑀) = ((𝑤 mod 𝑀) gcd 𝑀)) |
77 | 76 | eqeq1d 2773 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑤 mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ ((𝑤 mod 𝑀) gcd 𝑀) = 1)) |
78 | 77, 1 | elrab2 3518 |
. . . . . . . . . . 11
⊢ ((𝑤 mod 𝑀) ∈ 𝑈 ↔ ((𝑤 mod 𝑀) ∈ (0..^𝑀) ∧ ((𝑤 mod 𝑀) gcd 𝑀) = 1)) |
79 | 37, 75, 78 | sylanbrc 572 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑀) ∈ 𝑈) |
80 | | zmodfzo 12901 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑤 mod 𝑁) ∈ (0..^𝑁)) |
81 | 32, 46, 80 | syl2anc 573 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑁) ∈ (0..^𝑁)) |
82 | | modgcd 15461 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁)) |
83 | 32, 46, 82 | syl2anc 573 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁)) |
84 | | gcddvds 15433 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁)) |
85 | 32, 47, 84 | syl2anc 573 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁)) |
86 | 85 | simpld 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∥ 𝑤) |
87 | 85 | simprd 483 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∥ 𝑁) |
88 | | dvdsmul2 15213 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑀 · 𝑁)) |
89 | 40, 47, 88 | syl2anc 573 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑁 ∥ (𝑀 · 𝑁)) |
90 | | nnne0 11255 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
91 | | simpr 471 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤 = 0 ∧ 𝑁 = 0) → 𝑁 = 0) |
92 | 91 | necon3ai 2968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑁 = 0)) |
93 | 46, 90, 92 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ¬ (𝑤 = 0 ∧ 𝑁 = 0)) |
94 | | gcdn0cl 15432 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑤 = 0 ∧ 𝑁 = 0)) → (𝑤 gcd 𝑁) ∈ ℕ) |
95 | 32, 47, 93, 94 | syl21anc 1475 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∈ ℕ) |
96 | 95 | nnzd 11683 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∈ ℤ) |
97 | | dvdstr 15227 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 gcd 𝑁) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑤 gcd 𝑁) ∥ 𝑁 ∧ 𝑁 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁))) |
98 | 96, 47, 58, 97 | syl3anc 1476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (((𝑤 gcd 𝑁) ∥ 𝑁 ∧ 𝑁 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁))) |
99 | 87, 89, 98 | mp2and 679 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) |
100 | | dvdslegcd 15434 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑤 gcd 𝑁) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) → (((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁)))) |
101 | 96, 32, 58, 65, 100 | syl31anc 1479 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁)))) |
102 | 86, 99, 101 | mp2and 679 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁))) |
103 | 102, 70 | breqtrd 4812 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ≤ 1) |
104 | | nnle1eq1 11250 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 gcd 𝑁) ∈ ℕ → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1)) |
105 | 95, 104 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1)) |
106 | 103, 105 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) = 1) |
107 | 83, 106 | eqtrd 2805 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = 1) |
108 | | oveq1 6800 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑤 mod 𝑁) → (𝑦 gcd 𝑁) = ((𝑤 mod 𝑁) gcd 𝑁)) |
109 | 108 | eqeq1d 2773 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑤 mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝑤 mod 𝑁) gcd 𝑁) = 1)) |
110 | 109, 7 | elrab2 3518 |
. . . . . . . . . . 11
⊢ ((𝑤 mod 𝑁) ∈ 𝑉 ↔ ((𝑤 mod 𝑁) ∈ (0..^𝑁) ∧ ((𝑤 mod 𝑁) gcd 𝑁) = 1)) |
111 | 81, 107, 110 | sylanbrc 572 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑁) ∈ 𝑉) |
112 | | opelxpi 5288 |
. . . . . . . . . 10
⊢ (((𝑤 mod 𝑀) ∈ 𝑈 ∧ (𝑤 mod 𝑁) ∈ 𝑉) → 〈(𝑤 mod 𝑀), (𝑤 mod 𝑁)〉 ∈ (𝑈 × 𝑉)) |
113 | 79, 111, 112 | syl2anc 573 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 〈(𝑤 mod 𝑀), (𝑤 mod 𝑁)〉 ∈ (𝑈 × 𝑉)) |
114 | 27, 113 | eqeltrd 2850 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝐹‘𝑤) ∈ (𝑈 × 𝑉)) |
115 | 114 | ralrimiva 3115 |
. . . . . . 7
⊢ (𝜑 → ∀𝑤 ∈ 𝑊 (𝐹‘𝑤) ∈ (𝑈 × 𝑉)) |
116 | | crth.2 |
. . . . . . . . . 10
⊢ 𝑇 = ((0..^𝑀) × (0..^𝑁)) |
117 | 28, 116, 23, 33 | crth 15690 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑆–1-1-onto→𝑇) |
118 | | f1ofn 6279 |
. . . . . . . . 9
⊢ (𝐹:𝑆–1-1-onto→𝑇 → 𝐹 Fn 𝑆) |
119 | | fnfun 6128 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝑆 → Fun 𝐹) |
120 | 117, 118,
119 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → Fun 𝐹) |
121 | | ssrab2 3836 |
. . . . . . . . . 10
⊢ {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} ⊆ 𝑆 |
122 | 17, 121 | eqsstri 3784 |
. . . . . . . . 9
⊢ 𝑊 ⊆ 𝑆 |
123 | | fndm 6130 |
. . . . . . . . . 10
⊢ (𝐹 Fn 𝑆 → dom 𝐹 = 𝑆) |
124 | 117, 118,
123 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = 𝑆) |
125 | 122, 124 | syl5sseqr 3803 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ⊆ dom 𝐹) |
126 | | funimass4 6389 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑊 ⊆ dom 𝐹) → ((𝐹 “ 𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤 ∈ 𝑊 (𝐹‘𝑤) ∈ (𝑈 × 𝑉))) |
127 | 120, 125,
126 | syl2anc 573 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 “ 𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤 ∈ 𝑊 (𝐹‘𝑤) ∈ (𝑈 × 𝑉))) |
128 | 115, 127 | mpbird 247 |
. . . . . 6
⊢ (𝜑 → (𝐹 “ 𝑊) ⊆ (𝑈 × 𝑉)) |
129 | 1, 3 | eqsstri 3784 |
. . . . . . . . . . . . 13
⊢ 𝑈 ⊆ (0..^𝑀) |
130 | 7, 9 | eqsstri 3784 |
. . . . . . . . . . . . 13
⊢ 𝑉 ⊆ (0..^𝑁) |
131 | | xpss12 5264 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ⊆ (0..^𝑀) ∧ 𝑉 ⊆ (0..^𝑁)) → (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁))) |
132 | 129, 130,
131 | mp2an 672 |
. . . . . . . . . . . 12
⊢ (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁)) |
133 | 132, 116 | sseqtr4i 3787 |
. . . . . . . . . . 11
⊢ (𝑈 × 𝑉) ⊆ 𝑇 |
134 | 133 | sseli 3748 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝑈 × 𝑉) → 𝑧 ∈ 𝑇) |
135 | | f1ocnvfv2 6676 |
. . . . . . . . . 10
⊢ ((𝐹:𝑆–1-1-onto→𝑇 ∧ 𝑧 ∈ 𝑇) → (𝐹‘(◡𝐹‘𝑧)) = 𝑧) |
136 | 117, 134,
135 | syl2an 583 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(◡𝐹‘𝑧)) = 𝑧) |
137 | | f1ocnv 6290 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝑆–1-1-onto→𝑇 → ◡𝐹:𝑇–1-1-onto→𝑆) |
138 | | f1of 6278 |
. . . . . . . . . . . . 13
⊢ (◡𝐹:𝑇–1-1-onto→𝑆 → ◡𝐹:𝑇⟶𝑆) |
139 | 117, 137,
138 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ◡𝐹:𝑇⟶𝑆) |
140 | | ffvelrn 6500 |
. . . . . . . . . . . 12
⊢ ((◡𝐹:𝑇⟶𝑆 ∧ 𝑧 ∈ 𝑇) → (◡𝐹‘𝑧) ∈ 𝑆) |
141 | 139, 134,
140 | syl2an 583 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (◡𝐹‘𝑧) ∈ 𝑆) |
142 | 141, 28 | syl6eleq 2860 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (◡𝐹‘𝑧) ∈ (0..^(𝑀 · 𝑁))) |
143 | | elfzoelz 12678 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝐹‘𝑧) ∈ (0..^(𝑀 · 𝑁)) → (◡𝐹‘𝑧) ∈ ℤ) |
144 | 142, 143 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (◡𝐹‘𝑧) ∈ ℤ) |
145 | 34 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℕ) |
146 | | modgcd 15461 |
. . . . . . . . . . . . . 14
⊢ (((◡𝐹‘𝑧) ∈ ℤ ∧ 𝑀 ∈ ℕ) → (((◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = ((◡𝐹‘𝑧) gcd 𝑀)) |
147 | 144, 145,
146 | syl2anc 573 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = ((◡𝐹‘𝑧) gcd 𝑀)) |
148 | | oveq1 6800 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = (◡𝐹‘𝑧) → (𝑤 mod 𝑀) = ((◡𝐹‘𝑧) mod 𝑀)) |
149 | | oveq1 6800 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = (◡𝐹‘𝑧) → (𝑤 mod 𝑁) = ((◡𝐹‘𝑧) mod 𝑁)) |
150 | 148, 149 | opeq12d 4547 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = (◡𝐹‘𝑧) → 〈(𝑤 mod 𝑀), (𝑤 mod 𝑁)〉 = 〈((◡𝐹‘𝑧) mod 𝑀), ((◡𝐹‘𝑧) mod 𝑁)〉) |
151 | 22 | cbvmptv 4884 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ 𝑆 ↦ 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉) = (𝑤 ∈ 𝑆 ↦ 〈(𝑤 mod 𝑀), (𝑤 mod 𝑁)〉) |
152 | 23, 151 | eqtri 2793 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐹 = (𝑤 ∈ 𝑆 ↦ 〈(𝑤 mod 𝑀), (𝑤 mod 𝑁)〉) |
153 | | opex 5060 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
〈((◡𝐹‘𝑧) mod 𝑀), ((◡𝐹‘𝑧) mod 𝑁)〉 ∈ V |
154 | 150, 152,
153 | fvmpt 6424 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((◡𝐹‘𝑧) ∈ 𝑆 → (𝐹‘(◡𝐹‘𝑧)) = 〈((◡𝐹‘𝑧) mod 𝑀), ((◡𝐹‘𝑧) mod 𝑁)〉) |
155 | 141, 154 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(◡𝐹‘𝑧)) = 〈((◡𝐹‘𝑧) mod 𝑀), ((◡𝐹‘𝑧) mod 𝑁)〉) |
156 | 136, 155 | eqtr3d 2807 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 = 〈((◡𝐹‘𝑧) mod 𝑀), ((◡𝐹‘𝑧) mod 𝑁)〉) |
157 | | simpr 471 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝑈 × 𝑉)) |
158 | 156, 157 | eqeltrrd 2851 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 〈((◡𝐹‘𝑧) mod 𝑀), ((◡𝐹‘𝑧) mod 𝑁)〉 ∈ (𝑈 × 𝑉)) |
159 | | opelxp 5286 |
. . . . . . . . . . . . . . . . 17
⊢
(〈((◡𝐹‘𝑧) mod 𝑀), ((◡𝐹‘𝑧) mod 𝑁)〉 ∈ (𝑈 × 𝑉) ↔ (((◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈 ∧ ((◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉)) |
160 | 158, 159 | sylib 208 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈 ∧ ((◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉)) |
161 | 160 | simpld 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈) |
162 | | oveq1 6800 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = ((◡𝐹‘𝑧) mod 𝑀) → (𝑦 gcd 𝑀) = (((◡𝐹‘𝑧) mod 𝑀) gcd 𝑀)) |
163 | 162 | eqeq1d 2773 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ((◡𝐹‘𝑧) mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ (((◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1)) |
164 | 163, 1 | elrab2 3518 |
. . . . . . . . . . . . . . 15
⊢ (((◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈 ↔ (((◡𝐹‘𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1)) |
165 | 161, 164 | sylib 208 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((◡𝐹‘𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1)) |
166 | 165 | simprd 483 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1) |
167 | 147, 166 | eqtr3d 2807 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((◡𝐹‘𝑧) gcd 𝑀) = 1) |
168 | 45 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℕ) |
169 | | modgcd 15461 |
. . . . . . . . . . . . . 14
⊢ (((◡𝐹‘𝑧) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = ((◡𝐹‘𝑧) gcd 𝑁)) |
170 | 144, 168,
169 | syl2anc 573 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = ((◡𝐹‘𝑧) gcd 𝑁)) |
171 | 160 | simprd 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉) |
172 | | oveq1 6800 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = ((◡𝐹‘𝑧) mod 𝑁) → (𝑦 gcd 𝑁) = (((◡𝐹‘𝑧) mod 𝑁) gcd 𝑁)) |
173 | 172 | eqeq1d 2773 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ((◡𝐹‘𝑧) mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ (((◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1)) |
174 | 173, 7 | elrab2 3518 |
. . . . . . . . . . . . . . 15
⊢ (((◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉 ↔ (((◡𝐹‘𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1)) |
175 | 171, 174 | sylib 208 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((◡𝐹‘𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1)) |
176 | 175 | simprd 483 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1) |
177 | 170, 176 | eqtr3d 2807 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((◡𝐹‘𝑧) gcd 𝑁) = 1) |
178 | 34 | nnzd 11683 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ ℤ) |
179 | 178 | adantr 466 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℤ) |
180 | 45 | nnzd 11683 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℤ) |
181 | 180 | adantr 466 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℤ) |
182 | | rpmul 15580 |
. . . . . . . . . . . . 13
⊢ (((◡𝐹‘𝑧) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((((◡𝐹‘𝑧) gcd 𝑀) = 1 ∧ ((◡𝐹‘𝑧) gcd 𝑁) = 1) → ((◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1)) |
183 | 144, 179,
181, 182 | syl3anc 1476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((((◡𝐹‘𝑧) gcd 𝑀) = 1 ∧ ((◡𝐹‘𝑧) gcd 𝑁) = 1) → ((◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1)) |
184 | 167, 177,
183 | mp2and 679 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1) |
185 | | oveq1 6800 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (◡𝐹‘𝑧) → (𝑦 gcd (𝑀 · 𝑁)) = ((◡𝐹‘𝑧) gcd (𝑀 · 𝑁))) |
186 | 185 | eqeq1d 2773 |
. . . . . . . . . . . 12
⊢ (𝑦 = (◡𝐹‘𝑧) → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ ((◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1)) |
187 | 186, 17 | elrab2 3518 |
. . . . . . . . . . 11
⊢ ((◡𝐹‘𝑧) ∈ 𝑊 ↔ ((◡𝐹‘𝑧) ∈ 𝑆 ∧ ((◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1)) |
188 | 141, 184,
187 | sylanbrc 572 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (◡𝐹‘𝑧) ∈ 𝑊) |
189 | | funfvima2 6636 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ 𝑊 ⊆ dom 𝐹) → ((◡𝐹‘𝑧) ∈ 𝑊 → (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊))) |
190 | 120, 125,
189 | syl2anc 573 |
. . . . . . . . . . 11
⊢ (𝜑 → ((◡𝐹‘𝑧) ∈ 𝑊 → (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊))) |
191 | 190 | imp 393 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (◡𝐹‘𝑧) ∈ 𝑊) → (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊)) |
192 | 188, 191 | syldan 579 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊)) |
193 | 136, 192 | eqeltrrd 2851 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝐹 “ 𝑊)) |
194 | 193 | ex 397 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ (𝑈 × 𝑉) → 𝑧 ∈ (𝐹 “ 𝑊))) |
195 | 194 | ssrdv 3758 |
. . . . . 6
⊢ (𝜑 → (𝑈 × 𝑉) ⊆ (𝐹 “ 𝑊)) |
196 | 128, 195 | eqssd 3769 |
. . . . 5
⊢ (𝜑 → (𝐹 “ 𝑊) = (𝑈 × 𝑉)) |
197 | | f1of1 6277 |
. . . . . . 7
⊢ (𝐹:𝑆–1-1-onto→𝑇 → 𝐹:𝑆–1-1→𝑇) |
198 | 117, 197 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑆–1-1→𝑇) |
199 | | fzofi 12981 |
. . . . . . . . . 10
⊢
(0..^(𝑀 ·
𝑁)) ∈
Fin |
200 | 28, 199 | eqeltri 2846 |
. . . . . . . . 9
⊢ 𝑆 ∈ Fin |
201 | | ssfi 8336 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Fin ∧ 𝑊 ⊆ 𝑆) → 𝑊 ∈ Fin) |
202 | 200, 122,
201 | mp2an 672 |
. . . . . . . 8
⊢ 𝑊 ∈ Fin |
203 | 202 | elexi 3365 |
. . . . . . 7
⊢ 𝑊 ∈ V |
204 | 203 | f1imaen 8171 |
. . . . . 6
⊢ ((𝐹:𝑆–1-1→𝑇 ∧ 𝑊 ⊆ 𝑆) → (𝐹 “ 𝑊) ≈ 𝑊) |
205 | 198, 122,
204 | sylancl 574 |
. . . . 5
⊢ (𝜑 → (𝐹 “ 𝑊) ≈ 𝑊) |
206 | 196, 205 | eqbrtrrd 4810 |
. . . 4
⊢ (𝜑 → (𝑈 × 𝑉) ≈ 𝑊) |
207 | | xpfi 8387 |
. . . . . 6
⊢ ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) → (𝑈 × 𝑉) ∈ Fin) |
208 | 6, 12, 207 | mp2an 672 |
. . . . 5
⊢ (𝑈 × 𝑉) ∈ Fin |
209 | | hashen 13339 |
. . . . 5
⊢ (((𝑈 × 𝑉) ∈ Fin ∧ 𝑊 ∈ Fin) → ((♯‘(𝑈 × 𝑉)) = (♯‘𝑊) ↔ (𝑈 × 𝑉) ≈ 𝑊)) |
210 | 208, 202,
209 | mp2an 672 |
. . . 4
⊢
((♯‘(𝑈
× 𝑉)) =
(♯‘𝑊) ↔
(𝑈 × 𝑉) ≈ 𝑊) |
211 | 206, 210 | sylibr 224 |
. . 3
⊢ (𝜑 → (♯‘(𝑈 × 𝑉)) = (♯‘𝑊)) |
212 | 14, 211 | syl5reqr 2820 |
. 2
⊢ (𝜑 → (♯‘𝑊) = ((♯‘𝑈) · (♯‘𝑉))) |
213 | 34, 45 | nnmulcld 11270 |
. . 3
⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ) |
214 | | dfphi2 15686 |
. . . 4
⊢ ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (♯‘{𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1})) |
215 | | rabeq 3342 |
. . . . . . 7
⊢ (𝑆 = (0..^(𝑀 · 𝑁)) → {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}) |
216 | 28, 215 | ax-mp 5 |
. . . . . 6
⊢ {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} |
217 | 17, 216 | eqtri 2793 |
. . . . 5
⊢ 𝑊 = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} |
218 | 217 | fveq2i 6335 |
. . . 4
⊢
(♯‘𝑊) =
(♯‘{𝑦 ∈
(0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}) |
219 | 214, 218 | syl6eqr 2823 |
. . 3
⊢ ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (♯‘𝑊)) |
220 | 213, 219 | syl 17 |
. 2
⊢ (𝜑 → (ϕ‘(𝑀 · 𝑁)) = (♯‘𝑊)) |
221 | | dfphi2 15686 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
(ϕ‘𝑀) =
(♯‘{𝑦 ∈
(0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1})) |
222 | 1 | fveq2i 6335 |
. . . . 5
⊢
(♯‘𝑈) =
(♯‘{𝑦 ∈
(0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}) |
223 | 221, 222 | syl6eqr 2823 |
. . . 4
⊢ (𝑀 ∈ ℕ →
(ϕ‘𝑀) =
(♯‘𝑈)) |
224 | 34, 223 | syl 17 |
. . 3
⊢ (𝜑 → (ϕ‘𝑀) = (♯‘𝑈)) |
225 | | dfphi2 15686 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(ϕ‘𝑁) =
(♯‘{𝑦 ∈
(0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1})) |
226 | 7 | fveq2i 6335 |
. . . . 5
⊢
(♯‘𝑉) =
(♯‘{𝑦 ∈
(0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}) |
227 | 225, 226 | syl6eqr 2823 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(ϕ‘𝑁) =
(♯‘𝑉)) |
228 | 45, 227 | syl 17 |
. . 3
⊢ (𝜑 → (ϕ‘𝑁) = (♯‘𝑉)) |
229 | 224, 228 | oveq12d 6811 |
. 2
⊢ (𝜑 → ((ϕ‘𝑀) · (ϕ‘𝑁)) = ((♯‘𝑈) · (♯‘𝑉))) |
230 | 212, 220,
229 | 3eqtr4d 2815 |
1
⊢ (𝜑 → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁))) |