Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  phimullem GIF version

Theorem phimullem 11807
 Description: Lemma for phimul 11808. (Contributed by Mario Carneiro, 24-Feb-2014.)
Hypotheses
Ref Expression
crth.1 𝑆 = (0..^(𝑀 · 𝑁))
crth.2 𝑇 = ((0..^𝑀) × (0..^𝑁))
crth.3 𝐹 = (𝑥𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩)
crth.4 (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1))
phimul.4 𝑈 = {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}
phimul.5 𝑉 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}
phimul.6 𝑊 = {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
Assertion
Ref Expression
phimullem (𝜑 → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁)))
Distinct variable groups:   𝑦,𝐹   𝑥,𝑀   𝑥,𝑁   𝑥,𝑆,𝑦   𝑥,𝑇   𝜑,𝑥,𝑦   𝑦,𝑀   𝑦,𝑁
Allowed substitution hints:   𝑇(𝑦)   𝑈(𝑥,𝑦)   𝐹(𝑥)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem phimullem
Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 5747 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → (𝑦 gcd (𝑀 · 𝑁)) = (𝑤 gcd (𝑀 · 𝑁)))
21eqeq1d 2124 . . . . . . . . . . . . 13 (𝑦 = 𝑤 → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ (𝑤 gcd (𝑀 · 𝑁)) = 1))
3 phimul.6 . . . . . . . . . . . . 13 𝑊 = {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
42, 3elrab2 2814 . . . . . . . . . . . 12 (𝑤𝑊 ↔ (𝑤𝑆 ∧ (𝑤 gcd (𝑀 · 𝑁)) = 1))
54simplbi 270 . . . . . . . . . . 11 (𝑤𝑊𝑤𝑆)
65adantl 273 . . . . . . . . . 10 ((𝜑𝑤𝑊) → 𝑤𝑆)
7 elfzoelz 9875 . . . . . . . . . . . . . . 15 (𝑤 ∈ (0..^(𝑀 · 𝑁)) → 𝑤 ∈ ℤ)
8 crth.1 . . . . . . . . . . . . . . 15 𝑆 = (0..^(𝑀 · 𝑁))
97, 8eleq2s 2210 . . . . . . . . . . . . . 14 (𝑤𝑆𝑤 ∈ ℤ)
106, 9syl 14 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑤 ∈ ℤ)
11 zq 9370 . . . . . . . . . . . . 13 (𝑤 ∈ ℤ → 𝑤 ∈ ℚ)
1210, 11syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑤 ∈ ℚ)
13 crth.4 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1))
1413simp1d 976 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℕ)
1514adantr 272 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑀 ∈ ℕ)
16 nnq 9377 . . . . . . . . . . . . 13 (𝑀 ∈ ℕ → 𝑀 ∈ ℚ)
1715, 16syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑀 ∈ ℚ)
1815nngt0d 8724 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 0 < 𝑀)
1912, 17, 18modqcld 10052 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑀) ∈ ℚ)
2013simp2d 977 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ)
2120adantr 272 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑁 ∈ ℕ)
22 nnq 9377 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 𝑁 ∈ ℚ)
2321, 22syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑁 ∈ ℚ)
2421nngt0d 8724 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 0 < 𝑁)
2512, 23, 24modqcld 10052 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑁) ∈ ℚ)
26 opexg 4118 . . . . . . . . . . 11 (((𝑤 mod 𝑀) ∈ ℚ ∧ (𝑤 mod 𝑁) ∈ ℚ) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ V)
2719, 25, 26syl2anc 406 . . . . . . . . . 10 ((𝜑𝑤𝑊) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ V)
28 oveq1 5747 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝑥 mod 𝑀) = (𝑤 mod 𝑀))
29 oveq1 5747 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝑥 mod 𝑁) = (𝑤 mod 𝑁))
3028, 29opeq12d 3681 . . . . . . . . . . 11 (𝑥 = 𝑤 → ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩ = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
31 crth.3 . . . . . . . . . . 11 𝐹 = (𝑥𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩)
3230, 31fvmptg 5463 . . . . . . . . . 10 ((𝑤𝑆 ∧ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ V) → (𝐹𝑤) = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
336, 27, 32syl2anc 406 . . . . . . . . 9 ((𝜑𝑤𝑊) → (𝐹𝑤) = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
345, 8syl6eleq 2208 . . . . . . . . . . . . . 14 (𝑤𝑊𝑤 ∈ (0..^(𝑀 · 𝑁)))
3534adantl 273 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑤 ∈ (0..^(𝑀 · 𝑁)))
3635, 7syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑤 ∈ ℤ)
37 zmodfzo 10071 . . . . . . . . . . . 12 ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑤 mod 𝑀) ∈ (0..^𝑀))
3836, 15, 37syl2anc 406 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑀) ∈ (0..^𝑀))
39 modgcd 11586 . . . . . . . . . . . . 13 ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀))
4036, 15, 39syl2anc 406 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀))
4115nnzd 9126 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → 𝑀 ∈ ℤ)
42 gcddvds 11559 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
4336, 41, 42syl2anc 406 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
4443simpld 111 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∥ 𝑤)
45 nnne0 8708 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℕ → 𝑀 ≠ 0)
46 simpr 109 . . . . . . . . . . . . . . . . . . . 20 ((𝑤 = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
4746necon3ai 2332 . . . . . . . . . . . . . . . . . . 19 (𝑀 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
4815, 45, 473syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤𝑊) → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
49 gcdn0cl 11558 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑀 = 0)) → (𝑤 gcd 𝑀) ∈ ℕ)
5036, 41, 48, 49syl21anc 1198 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∈ ℕ)
5150nnzd 9126 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∈ ℤ)
5221nnzd 9126 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → 𝑁 ∈ ℤ)
5343simprd 113 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∥ 𝑀)
5451, 41, 52, 53dvdsmultr1d 11439 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁))
5515, 21nnmulcld 8729 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → (𝑀 · 𝑁) ∈ ℕ)
5655nnzd 9126 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑀 · 𝑁) ∈ ℤ)
57 nnne0 8708 . . . . . . . . . . . . . . . . 17 ((𝑀 · 𝑁) ∈ ℕ → (𝑀 · 𝑁) ≠ 0)
58 simpr 109 . . . . . . . . . . . . . . . . . 18 ((𝑤 = 0 ∧ (𝑀 · 𝑁) = 0) → (𝑀 · 𝑁) = 0)
5958necon3ai 2332 . . . . . . . . . . . . . . . . 17 ((𝑀 · 𝑁) ≠ 0 → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0))
6055, 57, 593syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0))
61 dvdslegcd 11560 . . . . . . . . . . . . . . . 16 ((((𝑤 gcd 𝑀) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) → (((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁))))
6251, 36, 56, 60, 61syl31anc 1202 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁))))
6344, 54, 62mp2and 427 . . . . . . . . . . . . . 14 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁)))
644simprbi 271 . . . . . . . . . . . . . . 15 (𝑤𝑊 → (𝑤 gcd (𝑀 · 𝑁)) = 1)
6564adantl 273 . . . . . . . . . . . . . 14 ((𝜑𝑤𝑊) → (𝑤 gcd (𝑀 · 𝑁)) = 1)
6663, 65breqtrd 3922 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ≤ 1)
67 nnle1eq1 8704 . . . . . . . . . . . . . 14 ((𝑤 gcd 𝑀) ∈ ℕ → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1))
6850, 67syl 14 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1))
6966, 68mpbid 146 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) = 1)
7040, 69eqtrd 2148 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = 1)
71 oveq1 5747 . . . . . . . . . . . . 13 (𝑦 = (𝑤 mod 𝑀) → (𝑦 gcd 𝑀) = ((𝑤 mod 𝑀) gcd 𝑀))
7271eqeq1d 2124 . . . . . . . . . . . 12 (𝑦 = (𝑤 mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ ((𝑤 mod 𝑀) gcd 𝑀) = 1))
73 phimul.4 . . . . . . . . . . . 12 𝑈 = {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}
7472, 73elrab2 2814 . . . . . . . . . . 11 ((𝑤 mod 𝑀) ∈ 𝑈 ↔ ((𝑤 mod 𝑀) ∈ (0..^𝑀) ∧ ((𝑤 mod 𝑀) gcd 𝑀) = 1))
7538, 70, 74sylanbrc 411 . . . . . . . . . 10 ((𝜑𝑤𝑊) → (𝑤 mod 𝑀) ∈ 𝑈)
76 zmodfzo 10071 . . . . . . . . . . . 12 ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑤 mod 𝑁) ∈ (0..^𝑁))
7736, 21, 76syl2anc 406 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑁) ∈ (0..^𝑁))
78 modgcd 11586 . . . . . . . . . . . . 13 ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁))
7936, 21, 78syl2anc 406 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁))
80 gcddvds 11559 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
8136, 52, 80syl2anc 406 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
8281simpld 111 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∥ 𝑤)
8381simprd 113 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∥ 𝑁)
84 dvdsmul2 11423 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑀 · 𝑁))
8541, 52, 84syl2anc 406 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → 𝑁 ∥ (𝑀 · 𝑁))
86 nnne0 8708 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
87 simpr 109 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
8887necon3ai 2332 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
8921, 86, 883syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤𝑊) → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
90 gcdn0cl 11558 . . . . . . . . . . . . . . . . . . 19 (((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑁 = 0)) → (𝑤 gcd 𝑁) ∈ ℕ)
9136, 52, 89, 90syl21anc 1198 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∈ ℕ)
9291nnzd 9126 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∈ ℤ)
93 dvdstr 11437 . . . . . . . . . . . . . . . . 17 (((𝑤 gcd 𝑁) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑤 gcd 𝑁) ∥ 𝑁𝑁 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)))
9492, 52, 56, 93syl3anc 1199 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (((𝑤 gcd 𝑁) ∥ 𝑁𝑁 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)))
9583, 85, 94mp2and 427 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁))
96 dvdslegcd 11560 . . . . . . . . . . . . . . . 16 ((((𝑤 gcd 𝑁) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) → (((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁))))
9792, 36, 56, 60, 96syl31anc 1202 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁))))
9882, 95, 97mp2and 427 . . . . . . . . . . . . . 14 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁)))
9998, 65breqtrd 3922 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ≤ 1)
100 nnle1eq1 8704 . . . . . . . . . . . . . 14 ((𝑤 gcd 𝑁) ∈ ℕ → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1))
10191, 100syl 14 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1))
10299, 101mpbid 146 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) = 1)
10379, 102eqtrd 2148 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = 1)
104 oveq1 5747 . . . . . . . . . . . . 13 (𝑦 = (𝑤 mod 𝑁) → (𝑦 gcd 𝑁) = ((𝑤 mod 𝑁) gcd 𝑁))
105104eqeq1d 2124 . . . . . . . . . . . 12 (𝑦 = (𝑤 mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝑤 mod 𝑁) gcd 𝑁) = 1))
106 phimul.5 . . . . . . . . . . . 12 𝑉 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}
107105, 106elrab2 2814 . . . . . . . . . . 11 ((𝑤 mod 𝑁) ∈ 𝑉 ↔ ((𝑤 mod 𝑁) ∈ (0..^𝑁) ∧ ((𝑤 mod 𝑁) gcd 𝑁) = 1))
10877, 103, 107sylanbrc 411 . . . . . . . . . 10 ((𝜑𝑤𝑊) → (𝑤 mod 𝑁) ∈ 𝑉)
109 opelxpi 4539 . . . . . . . . . 10 (((𝑤 mod 𝑀) ∈ 𝑈 ∧ (𝑤 mod 𝑁) ∈ 𝑉) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
11075, 108, 109syl2anc 406 . . . . . . . . 9 ((𝜑𝑤𝑊) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
11133, 110eqeltrd 2192 . . . . . . . 8 ((𝜑𝑤𝑊) → (𝐹𝑤) ∈ (𝑈 × 𝑉))
112111ralrimiva 2480 . . . . . . 7 (𝜑 → ∀𝑤𝑊 (𝐹𝑤) ∈ (𝑈 × 𝑉))
113 crth.2 . . . . . . . . . 10 𝑇 = ((0..^𝑀) × (0..^𝑁))
1148, 113, 31, 13crth 11806 . . . . . . . . 9 (𝜑𝐹:𝑆1-1-onto𝑇)
115 f1ofn 5334 . . . . . . . . 9 (𝐹:𝑆1-1-onto𝑇𝐹 Fn 𝑆)
116 fnfun 5188 . . . . . . . . 9 (𝐹 Fn 𝑆 → Fun 𝐹)
117114, 115, 1163syl 17 . . . . . . . 8 (𝜑 → Fun 𝐹)
118 ssrab2 3150 . . . . . . . . . 10 {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} ⊆ 𝑆
1193, 118eqsstri 3097 . . . . . . . . 9 𝑊𝑆
120 fndm 5190 . . . . . . . . . 10 (𝐹 Fn 𝑆 → dom 𝐹 = 𝑆)
121114, 115, 1203syl 17 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝑆)
122119, 121sseqtrrid 3116 . . . . . . . 8 (𝜑𝑊 ⊆ dom 𝐹)
123 funimass4 5438 . . . . . . . 8 ((Fun 𝐹𝑊 ⊆ dom 𝐹) → ((𝐹𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤𝑊 (𝐹𝑤) ∈ (𝑈 × 𝑉)))
124117, 122, 123syl2anc 406 . . . . . . 7 (𝜑 → ((𝐹𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤𝑊 (𝐹𝑤) ∈ (𝑈 × 𝑉)))
125112, 124mpbird 166 . . . . . 6 (𝜑 → (𝐹𝑊) ⊆ (𝑈 × 𝑉))
126 ssrab2 3150 . . . . . . . . . . . . . 14 {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ⊆ (0..^𝑀)
12773, 126eqsstri 3097 . . . . . . . . . . . . 13 𝑈 ⊆ (0..^𝑀)
128 ssrab2 3150 . . . . . . . . . . . . . 14 {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁)
129106, 128eqsstri 3097 . . . . . . . . . . . . 13 𝑉 ⊆ (0..^𝑁)
130 xpss12 4614 . . . . . . . . . . . . 13 ((𝑈 ⊆ (0..^𝑀) ∧ 𝑉 ⊆ (0..^𝑁)) → (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁)))
131127, 129, 130mp2an 420 . . . . . . . . . . . 12 (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁))
132131, 113sseqtrri 3100 . . . . . . . . . . 11 (𝑈 × 𝑉) ⊆ 𝑇
133132sseli 3061 . . . . . . . . . 10 (𝑧 ∈ (𝑈 × 𝑉) → 𝑧𝑇)
134 f1ocnvfv2 5645 . . . . . . . . . 10 ((𝐹:𝑆1-1-onto𝑇𝑧𝑇) → (𝐹‘(𝐹𝑧)) = 𝑧)
135114, 133, 134syl2an 285 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(𝐹𝑧)) = 𝑧)
136 f1ocnv 5346 . . . . . . . . . . . . 13 (𝐹:𝑆1-1-onto𝑇𝐹:𝑇1-1-onto𝑆)
137 f1of 5333 . . . . . . . . . . . . 13 (𝐹:𝑇1-1-onto𝑆𝐹:𝑇𝑆)
138114, 136, 1373syl 17 . . . . . . . . . . . 12 (𝜑𝐹:𝑇𝑆)
139 ffvelrn 5519 . . . . . . . . . . . 12 ((𝐹:𝑇𝑆𝑧𝑇) → (𝐹𝑧) ∈ 𝑆)
140138, 133, 139syl2an 285 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ 𝑆)
141140, 8syl6eleq 2208 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ (0..^(𝑀 · 𝑁)))
142 elfzoelz 9875 . . . . . . . . . . . . . . 15 ((𝐹𝑧) ∈ (0..^(𝑀 · 𝑁)) → (𝐹𝑧) ∈ ℤ)
143141, 142syl 14 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ ℤ)
14414adantr 272 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℕ)
145 modgcd 11586 . . . . . . . . . . . . . 14 (((𝐹𝑧) ∈ ℤ ∧ 𝑀 ∈ ℕ) → (((𝐹𝑧) mod 𝑀) gcd 𝑀) = ((𝐹𝑧) gcd 𝑀))
146143, 144, 145syl2anc 406 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) gcd 𝑀) = ((𝐹𝑧) gcd 𝑀))
147 zq 9370 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑧) ∈ ℤ → (𝐹𝑧) ∈ ℚ)
148143, 147syl 14 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ ℚ)
149144, 16syl 14 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℚ)
150144nngt0d 8724 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 0 < 𝑀)
151148, 149, 150modqcld 10052 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑀) ∈ ℚ)
15220adantr 272 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℕ)
153152, 22syl 14 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℚ)
154152nngt0d 8724 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 0 < 𝑁)
155148, 153, 154modqcld 10052 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑁) ∈ ℚ)
156 opexg 4118 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑧) mod 𝑀) ∈ ℚ ∧ ((𝐹𝑧) mod 𝑁) ∈ ℚ) → ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ V)
157151, 155, 156syl2anc 406 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ V)
158 oveq1 5747 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = (𝐹𝑧) → (𝑤 mod 𝑀) = ((𝐹𝑧) mod 𝑀))
159 oveq1 5747 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = (𝐹𝑧) → (𝑤 mod 𝑁) = ((𝐹𝑧) mod 𝑁))
160158, 159opeq12d 3681 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = (𝐹𝑧) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
16130cbvmptv 3992 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩) = (𝑤𝑆 ↦ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
16231, 161eqtri 2136 . . . . . . . . . . . . . . . . . . . . 21 𝐹 = (𝑤𝑆 ↦ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
163160, 162fvmptg 5463 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑧) ∈ 𝑆 ∧ ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ V) → (𝐹‘(𝐹𝑧)) = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
164140, 157, 163syl2anc 406 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(𝐹𝑧)) = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
165135, 164eqtr3d 2150 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
166 simpr 109 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝑈 × 𝑉))
167165, 166eqeltrrd 2193 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
168 opelxp 4537 . . . . . . . . . . . . . . . . 17 (⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ (𝑈 × 𝑉) ↔ (((𝐹𝑧) mod 𝑀) ∈ 𝑈 ∧ ((𝐹𝑧) mod 𝑁) ∈ 𝑉))
169167, 168sylib 121 . . . . . . . . . . . . . . . 16 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) ∈ 𝑈 ∧ ((𝐹𝑧) mod 𝑁) ∈ 𝑉))
170169simpld 111 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑀) ∈ 𝑈)
171 oveq1 5747 . . . . . . . . . . . . . . . . 17 (𝑦 = ((𝐹𝑧) mod 𝑀) → (𝑦 gcd 𝑀) = (((𝐹𝑧) mod 𝑀) gcd 𝑀))
172171eqeq1d 2124 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝐹𝑧) mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1))
173172, 73elrab2 2814 . . . . . . . . . . . . . . 15 (((𝐹𝑧) mod 𝑀) ∈ 𝑈 ↔ (((𝐹𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1))
174170, 173sylib 121 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1))
175174simprd 113 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1)
176146, 175eqtr3d 2150 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) gcd 𝑀) = 1)
177 modgcd 11586 . . . . . . . . . . . . . 14 (((𝐹𝑧) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐹𝑧) mod 𝑁) gcd 𝑁) = ((𝐹𝑧) gcd 𝑁))
178143, 152, 177syl2anc 406 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑁) gcd 𝑁) = ((𝐹𝑧) gcd 𝑁))
179169simprd 113 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑁) ∈ 𝑉)
180 oveq1 5747 . . . . . . . . . . . . . . . . 17 (𝑦 = ((𝐹𝑧) mod 𝑁) → (𝑦 gcd 𝑁) = (((𝐹𝑧) mod 𝑁) gcd 𝑁))
181180eqeq1d 2124 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝐹𝑧) mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1))
182181, 106elrab2 2814 . . . . . . . . . . . . . . 15 (((𝐹𝑧) mod 𝑁) ∈ 𝑉 ↔ (((𝐹𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1))
183179, 182sylib 121 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1))
184183simprd 113 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1)
185178, 184eqtr3d 2150 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) gcd 𝑁) = 1)
18614nnzd 9126 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℤ)
187186adantr 272 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℤ)
18820nnzd 9126 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
189188adantr 272 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℤ)
190 rpmul 11686 . . . . . . . . . . . . 13 (((𝐹𝑧) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((((𝐹𝑧) gcd 𝑀) = 1 ∧ ((𝐹𝑧) gcd 𝑁) = 1) → ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
191143, 187, 189, 190syl3anc 1199 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((((𝐹𝑧) gcd 𝑀) = 1 ∧ ((𝐹𝑧) gcd 𝑁) = 1) → ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
192176, 185, 191mp2and 427 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1)
193 oveq1 5747 . . . . . . . . . . . . 13 (𝑦 = (𝐹𝑧) → (𝑦 gcd (𝑀 · 𝑁)) = ((𝐹𝑧) gcd (𝑀 · 𝑁)))
194193eqeq1d 2124 . . . . . . . . . . . 12 (𝑦 = (𝐹𝑧) → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
195194, 3elrab2 2814 . . . . . . . . . . 11 ((𝐹𝑧) ∈ 𝑊 ↔ ((𝐹𝑧) ∈ 𝑆 ∧ ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
196140, 192, 195sylanbrc 411 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ 𝑊)
197 funfvima2 5616 . . . . . . . . . . . 12 ((Fun 𝐹𝑊 ⊆ dom 𝐹) → ((𝐹𝑧) ∈ 𝑊 → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊)))
198117, 122, 197syl2anc 406 . . . . . . . . . . 11 (𝜑 → ((𝐹𝑧) ∈ 𝑊 → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊)))
199198imp 123 . . . . . . . . . 10 ((𝜑 ∧ (𝐹𝑧) ∈ 𝑊) → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊))
200196, 199syldan 278 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊))
201135, 200eqeltrrd 2193 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝐹𝑊))
202201ex 114 . . . . . . 7 (𝜑 → (𝑧 ∈ (𝑈 × 𝑉) → 𝑧 ∈ (𝐹𝑊)))
203202ssrdv 3071 . . . . . 6 (𝜑 → (𝑈 × 𝑉) ⊆ (𝐹𝑊))
204125, 203eqssd 3082 . . . . 5 (𝜑 → (𝐹𝑊) = (𝑈 × 𝑉))
205 f1of1 5332 . . . . . . 7 (𝐹:𝑆1-1-onto𝑇𝐹:𝑆1-1𝑇)
206114, 205syl 14 . . . . . 6 (𝜑𝐹:𝑆1-1𝑇)
207119a1i 9 . . . . . 6 (𝜑𝑊𝑆)
208 0z 9019 . . . . . . . . . 10 0 ∈ ℤ
209186, 188zmulcld 9133 . . . . . . . . . 10 (𝜑 → (𝑀 · 𝑁) ∈ ℤ)
210 fzofig 10156 . . . . . . . . . 10 ((0 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (0..^(𝑀 · 𝑁)) ∈ Fin)
211208, 209, 210sylancr 408 . . . . . . . . 9 (𝜑 → (0..^(𝑀 · 𝑁)) ∈ Fin)
2128, 211eqeltrid 2202 . . . . . . . 8 (𝜑𝑆 ∈ Fin)
213 elfzoelz 9875 . . . . . . . . . . . . . 14 (𝑦 ∈ (0..^(𝑀 · 𝑁)) → 𝑦 ∈ ℤ)
214213, 8eleq2s 2210 . . . . . . . . . . . . 13 (𝑦𝑆𝑦 ∈ ℤ)
215214adantl 273 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → 𝑦 ∈ ℤ)
216209adantr 272 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → (𝑀 · 𝑁) ∈ ℤ)
217215, 216gcdcld 11564 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → (𝑦 gcd (𝑀 · 𝑁)) ∈ ℕ0)
218217nn0zd 9125 . . . . . . . . . 10 ((𝜑𝑦𝑆) → (𝑦 gcd (𝑀 · 𝑁)) ∈ ℤ)
219 1zzd 9035 . . . . . . . . . 10 ((𝜑𝑦𝑆) → 1 ∈ ℤ)
220 zdceq 9080 . . . . . . . . . 10 (((𝑦 gcd (𝑀 · 𝑁)) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝑦 gcd (𝑀 · 𝑁)) = 1)
221218, 219, 220syl2anc 406 . . . . . . . . 9 ((𝜑𝑦𝑆) → DECID (𝑦 gcd (𝑀 · 𝑁)) = 1)
222221ralrimiva 2480 . . . . . . . 8 (𝜑 → ∀𝑦𝑆 DECID (𝑦 gcd (𝑀 · 𝑁)) = 1)
223212, 222ssfirab 6788 . . . . . . 7 (𝜑 → {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} ∈ Fin)
2243, 223eqeltrid 2202 . . . . . 6 (𝜑𝑊 ∈ Fin)
225 f1imaeng 6652 . . . . . 6 ((𝐹:𝑆1-1𝑇𝑊𝑆𝑊 ∈ Fin) → (𝐹𝑊) ≈ 𝑊)
226206, 207, 224, 225syl3anc 1199 . . . . 5 (𝜑 → (𝐹𝑊) ≈ 𝑊)
227204, 226eqbrtrrd 3920 . . . 4 (𝜑 → (𝑈 × 𝑉) ≈ 𝑊)
228 fzofig 10156 . . . . . . . . 9 ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0..^𝑀) ∈ Fin)
229208, 186, 228sylancr 408 . . . . . . . 8 (𝜑 → (0..^𝑀) ∈ Fin)
230 elfzoelz 9875 . . . . . . . . . . . . 13 (𝑦 ∈ (0..^𝑀) → 𝑦 ∈ ℤ)
231230adantl 273 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑀)) → 𝑦 ∈ ℤ)
232186adantr 272 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑀)) → 𝑀 ∈ ℤ)
233231, 232gcdcld 11564 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (0..^𝑀)) → (𝑦 gcd 𝑀) ∈ ℕ0)
234233nn0zd 9125 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0..^𝑀)) → (𝑦 gcd 𝑀) ∈ ℤ)
235 1z 9034 . . . . . . . . . 10 1 ∈ ℤ
236 zdceq 9080 . . . . . . . . . 10 (((𝑦 gcd 𝑀) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝑦 gcd 𝑀) = 1)
237234, 235, 236sylancl 407 . . . . . . . . 9 ((𝜑𝑦 ∈ (0..^𝑀)) → DECID (𝑦 gcd 𝑀) = 1)
238237ralrimiva 2480 . . . . . . . 8 (𝜑 → ∀𝑦 ∈ (0..^𝑀)DECID (𝑦 gcd 𝑀) = 1)
239229, 238ssfirab 6788 . . . . . . 7 (𝜑 → {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ∈ Fin)
24073, 239eqeltrid 2202 . . . . . 6 (𝜑𝑈 ∈ Fin)
241 fzofig 10156 . . . . . . . . 9 ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0..^𝑁) ∈ Fin)
242208, 188, 241sylancr 408 . . . . . . . 8 (𝜑 → (0..^𝑁) ∈ Fin)
243 elfzoelz 9875 . . . . . . . . . . . . 13 (𝑦 ∈ (0..^𝑁) → 𝑦 ∈ ℤ)
244243adantl 273 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑁)) → 𝑦 ∈ ℤ)
245188adantr 272 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑁)) → 𝑁 ∈ ℤ)
246244, 245gcdcld 11564 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (0..^𝑁)) → (𝑦 gcd 𝑁) ∈ ℕ0)
247246nn0zd 9125 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0..^𝑁)) → (𝑦 gcd 𝑁) ∈ ℤ)
248 1zzd 9035 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0..^𝑁)) → 1 ∈ ℤ)
249 zdceq 9080 . . . . . . . . . 10 (((𝑦 gcd 𝑁) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝑦 gcd 𝑁) = 1)
250247, 248, 249syl2anc 406 . . . . . . . . 9 ((𝜑𝑦 ∈ (0..^𝑁)) → DECID (𝑦 gcd 𝑁) = 1)
251250ralrimiva 2480 . . . . . . . 8 (𝜑 → ∀𝑦 ∈ (0..^𝑁)DECID (𝑦 gcd 𝑁) = 1)
252242, 251ssfirab 6788 . . . . . . 7 (𝜑 → {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ∈ Fin)
253106, 252eqeltrid 2202 . . . . . 6 (𝜑𝑉 ∈ Fin)
254 xpfi 6784 . . . . . 6 ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) → (𝑈 × 𝑉) ∈ Fin)
255240, 253, 254syl2anc 406 . . . . 5 (𝜑 → (𝑈 × 𝑉) ∈ Fin)
256 hashen 10481 . . . . 5 (((𝑈 × 𝑉) ∈ Fin ∧ 𝑊 ∈ Fin) → ((♯‘(𝑈 × 𝑉)) = (♯‘𝑊) ↔ (𝑈 × 𝑉) ≈ 𝑊))
257255, 224, 256syl2anc 406 . . . 4 (𝜑 → ((♯‘(𝑈 × 𝑉)) = (♯‘𝑊) ↔ (𝑈 × 𝑉) ≈ 𝑊))
258227, 257mpbird 166 . . 3 (𝜑 → (♯‘(𝑈 × 𝑉)) = (♯‘𝑊))
259 hashxp 10523 . . . 4 ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) → (♯‘(𝑈 × 𝑉)) = ((♯‘𝑈) · (♯‘𝑉)))
260240, 253, 259syl2anc 406 . . 3 (𝜑 → (♯‘(𝑈 × 𝑉)) = ((♯‘𝑈) · (♯‘𝑉)))
261258, 260eqtr3d 2150 . 2 (𝜑 → (♯‘𝑊) = ((♯‘𝑈) · (♯‘𝑉)))
26214, 20nnmulcld 8729 . . 3 (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
263 dfphi2 11802 . . . 4 ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (♯‘{𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}))
2648rabeqi 2651 . . . . . 6 {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
2653, 264eqtri 2136 . . . . 5 𝑊 = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
266265fveq2i 5390 . . . 4 (♯‘𝑊) = (♯‘{𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1})
267263, 266syl6eqr 2166 . . 3 ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (♯‘𝑊))
268262, 267syl 14 . 2 (𝜑 → (ϕ‘(𝑀 · 𝑁)) = (♯‘𝑊))
269 dfphi2 11802 . . . . 5 (𝑀 ∈ ℕ → (ϕ‘𝑀) = (♯‘{𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}))
27073fveq2i 5390 . . . . 5 (♯‘𝑈) = (♯‘{𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1})
271269, 270syl6eqr 2166 . . . 4 (𝑀 ∈ ℕ → (ϕ‘𝑀) = (♯‘𝑈))
27214, 271syl 14 . . 3 (𝜑 → (ϕ‘𝑀) = (♯‘𝑈))
273 dfphi2 11802 . . . . 5 (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘{𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}))
274106fveq2i 5390 . . . . 5 (♯‘𝑉) = (♯‘{𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1})
275273, 274syl6eqr 2166 . . . 4 (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘𝑉))
27620, 275syl 14 . . 3 (𝜑 → (ϕ‘𝑁) = (♯‘𝑉))
277272, 276oveq12d 5758 . 2 (𝜑 → ((ϕ‘𝑀) · (ϕ‘𝑁)) = ((♯‘𝑈) · (♯‘𝑉)))
278261, 268, 2773eqtr4d 2158 1 (𝜑 → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁)))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104  DECID wdc 802   ∧ w3a 945   = wceq 1314   ∈ wcel 1463   ≠ wne 2283  ∀wral 2391  {crab 2395  Vcvv 2658   ⊆ wss 3039  ⟨cop 3498   class class class wbr 3897   ↦ cmpt 3957   × cxp 4505  ◡ccnv 4506  dom cdm 4507   “ cima 4510  Fun wfun 5085   Fn wfn 5086  ⟶wf 5087  –1-1→wf1 5088  –1-1-onto→wf1o 5090  ‘cfv 5091  (class class class)co 5740   ≈ cen 6598  Fincfn 6600  0cc0 7584  1c1 7585   · cmul 7589   ≤ cle 7765  ℕcn 8680  ℤcz 9008  ℚcq 9363  ..^cfzo 9870   mod cmo 10046  ♯chash 10472   ∥ cdvds 11400   gcd cgcd 11542  ϕcphi 11792 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4011  ax-sep 4014  ax-nul 4022  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420  ax-iinf 4470  ax-cnex 7675  ax-resscn 7676  ax-1cn 7677  ax-1re 7678  ax-icn 7679  ax-addcl 7680  ax-addrcl 7681  ax-mulcl 7682  ax-mulrcl 7683  ax-addcom 7684  ax-mulcom 7685  ax-addass 7686  ax-mulass 7687  ax-distr 7688  ax-i2m1 7689  ax-0lt1 7690  ax-1rid 7691  ax-0id 7692  ax-rnegex 7693  ax-precex 7694  ax-cnre 7695  ax-pre-ltirr 7696  ax-pre-ltwlin 7697  ax-pre-lttrn 7698  ax-pre-apti 7699  ax-pre-ltadd 7700  ax-pre-mulgt0 7701  ax-pre-mulext 7702  ax-arch 7703  ax-caucvg 7704 This theorem depends on definitions:  df-bi 116  df-stab 799  df-dc 803  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-nel 2379  df-ral 2396  df-rex 2397  df-reu 2398  df-rmo 2399  df-rab 2400  df-v 2660  df-sbc 2881  df-csb 2974  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-if 3443  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-int 3740  df-iun 3783  df-br 3898  df-opab 3958  df-mpt 3959  df-tr 3995  df-id 4183  df-po 4186  df-iso 4187  df-iord 4256  df-on 4258  df-ilim 4259  df-suc 4261  df-iom 4473  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-f1 5096  df-fo 5097  df-f1o 5098  df-fv 5099  df-riota 5696  df-ov 5743  df-oprab 5744  df-mpo 5745  df-1st 6004  df-2nd 6005  df-recs 6168  df-irdg 6233  df-frec 6254  df-1o 6279  df-oadd 6283  df-er 6395  df-en 6601  df-dom 6602  df-fin 6603  df-sup 6837  df-pnf 7766  df-mnf 7767  df-xr 7768  df-ltxr 7769  df-le 7770  df-sub 7899  df-neg 7900  df-reap 8300  df-ap 8307  df-div 8396  df-inn 8681  df-2 8739  df-3 8740  df-4 8741  df-n0 8932  df-z 9009  df-uz 9279  df-q 9364  df-rp 9394  df-fz 9742  df-fzo 9871  df-fl 9994  df-mod 10047  df-seqfrec 10170  df-exp 10244  df-ihash 10473  df-cj 10565  df-re 10566  df-im 10567  df-rsqrt 10721  df-abs 10722  df-dvds 11401  df-gcd 11543  df-phi 11793 This theorem is referenced by:  phimul  11808
 Copyright terms: Public domain W3C validator