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

Theorem phimullem 12208
Description: Lemma for phimul 12209. (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 5876 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → (𝑦 gcd (𝑀 · 𝑁)) = (𝑤 gcd (𝑀 · 𝑁)))
21eqeq1d 2186 . . . . . . . . . . . . 13 (𝑦 = 𝑤 → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ (𝑤 gcd (𝑀 · 𝑁)) = 1))
3 phimul.6 . . . . . . . . . . . . 13 𝑊 = {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
42, 3elrab2 2896 . . . . . . . . . . . 12 (𝑤𝑊 ↔ (𝑤𝑆 ∧ (𝑤 gcd (𝑀 · 𝑁)) = 1))
54simplbi 274 . . . . . . . . . . 11 (𝑤𝑊𝑤𝑆)
65adantl 277 . . . . . . . . . 10 ((𝜑𝑤𝑊) → 𝑤𝑆)
7 elfzoelz 10133 . . . . . . . . . . . . . . 15 (𝑤 ∈ (0..^(𝑀 · 𝑁)) → 𝑤 ∈ ℤ)
8 crth.1 . . . . . . . . . . . . . . 15 𝑆 = (0..^(𝑀 · 𝑁))
97, 8eleq2s 2272 . . . . . . . . . . . . . 14 (𝑤𝑆𝑤 ∈ ℤ)
106, 9syl 14 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑤 ∈ ℤ)
11 zq 9615 . . . . . . . . . . . . 13 (𝑤 ∈ ℤ → 𝑤 ∈ ℚ)
1210, 11syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑤 ∈ ℚ)
13 crth.4 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1))
1413simp1d 1009 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℕ)
1514adantr 276 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑀 ∈ ℕ)
16 nnq 9622 . . . . . . . . . . . . 13 (𝑀 ∈ ℕ → 𝑀 ∈ ℚ)
1715, 16syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑀 ∈ ℚ)
1815nngt0d 8952 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 0 < 𝑀)
1912, 17, 18modqcld 10314 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑀) ∈ ℚ)
2013simp2d 1010 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ)
2120adantr 276 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑁 ∈ ℕ)
22 nnq 9622 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 𝑁 ∈ ℚ)
2321, 22syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑁 ∈ ℚ)
2421nngt0d 8952 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 0 < 𝑁)
2512, 23, 24modqcld 10314 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑁) ∈ ℚ)
26 opexg 4225 . . . . . . . . . . 11 (((𝑤 mod 𝑀) ∈ ℚ ∧ (𝑤 mod 𝑁) ∈ ℚ) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ V)
2719, 25, 26syl2anc 411 . . . . . . . . . 10 ((𝜑𝑤𝑊) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ V)
28 oveq1 5876 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝑥 mod 𝑀) = (𝑤 mod 𝑀))
29 oveq1 5876 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝑥 mod 𝑁) = (𝑤 mod 𝑁))
3028, 29opeq12d 3784 . . . . . . . . . . 11 (𝑥 = 𝑤 → ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩ = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
31 crth.3 . . . . . . . . . . 11 𝐹 = (𝑥𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩)
3230, 31fvmptg 5588 . . . . . . . . . 10 ((𝑤𝑆 ∧ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ V) → (𝐹𝑤) = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
336, 27, 32syl2anc 411 . . . . . . . . 9 ((𝜑𝑤𝑊) → (𝐹𝑤) = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
345, 8eleqtrdi 2270 . . . . . . . . . . . . . 14 (𝑤𝑊𝑤 ∈ (0..^(𝑀 · 𝑁)))
3534adantl 277 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑤 ∈ (0..^(𝑀 · 𝑁)))
3635, 7syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑤 ∈ ℤ)
37 zmodfzo 10333 . . . . . . . . . . . 12 ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑤 mod 𝑀) ∈ (0..^𝑀))
3836, 15, 37syl2anc 411 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑀) ∈ (0..^𝑀))
39 modgcd 11975 . . . . . . . . . . . . 13 ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀))
4036, 15, 39syl2anc 411 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀))
4115nnzd 9363 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → 𝑀 ∈ ℤ)
42 gcddvds 11947 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
4336, 41, 42syl2anc 411 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
4443simpld 112 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∥ 𝑤)
45 nnne0 8936 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℕ → 𝑀 ≠ 0)
46 simpr 110 . . . . . . . . . . . . . . . . . . . 20 ((𝑤 = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
4746necon3ai 2396 . . . . . . . . . . . . . . . . . . 19 (𝑀 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
4815, 45, 473syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤𝑊) → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
49 gcdn0cl 11946 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑀 = 0)) → (𝑤 gcd 𝑀) ∈ ℕ)
5036, 41, 48, 49syl21anc 1237 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∈ ℕ)
5150nnzd 9363 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∈ ℤ)
5221nnzd 9363 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → 𝑁 ∈ ℤ)
5343simprd 114 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∥ 𝑀)
5451, 41, 52, 53dvdsmultr1d 11823 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁))
5515, 21nnmulcld 8957 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → (𝑀 · 𝑁) ∈ ℕ)
5655nnzd 9363 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑀 · 𝑁) ∈ ℤ)
57 nnne0 8936 . . . . . . . . . . . . . . . . 17 ((𝑀 · 𝑁) ∈ ℕ → (𝑀 · 𝑁) ≠ 0)
58 simpr 110 . . . . . . . . . . . . . . . . . 18 ((𝑤 = 0 ∧ (𝑀 · 𝑁) = 0) → (𝑀 · 𝑁) = 0)
5958necon3ai 2396 . . . . . . . . . . . . . . . . 17 ((𝑀 · 𝑁) ≠ 0 → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0))
6055, 57, 593syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0))
61 dvdslegcd 11948 . . . . . . . . . . . . . . . 16 ((((𝑤 gcd 𝑀) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) → (((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁))))
6251, 36, 56, 60, 61syl31anc 1241 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁))))
6344, 54, 62mp2and 433 . . . . . . . . . . . . . 14 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁)))
644simprbi 275 . . . . . . . . . . . . . . 15 (𝑤𝑊 → (𝑤 gcd (𝑀 · 𝑁)) = 1)
6564adantl 277 . . . . . . . . . . . . . 14 ((𝜑𝑤𝑊) → (𝑤 gcd (𝑀 · 𝑁)) = 1)
6663, 65breqtrd 4026 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ≤ 1)
67 nnle1eq1 8932 . . . . . . . . . . . . . 14 ((𝑤 gcd 𝑀) ∈ ℕ → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1))
6850, 67syl 14 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1))
6966, 68mpbid 147 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) = 1)
7040, 69eqtrd 2210 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = 1)
71 oveq1 5876 . . . . . . . . . . . . 13 (𝑦 = (𝑤 mod 𝑀) → (𝑦 gcd 𝑀) = ((𝑤 mod 𝑀) gcd 𝑀))
7271eqeq1d 2186 . . . . . . . . . . . 12 (𝑦 = (𝑤 mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ ((𝑤 mod 𝑀) gcd 𝑀) = 1))
73 phimul.4 . . . . . . . . . . . 12 𝑈 = {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}
7472, 73elrab2 2896 . . . . . . . . . . 11 ((𝑤 mod 𝑀) ∈ 𝑈 ↔ ((𝑤 mod 𝑀) ∈ (0..^𝑀) ∧ ((𝑤 mod 𝑀) gcd 𝑀) = 1))
7538, 70, 74sylanbrc 417 . . . . . . . . . 10 ((𝜑𝑤𝑊) → (𝑤 mod 𝑀) ∈ 𝑈)
76 zmodfzo 10333 . . . . . . . . . . . 12 ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑤 mod 𝑁) ∈ (0..^𝑁))
7736, 21, 76syl2anc 411 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑁) ∈ (0..^𝑁))
78 modgcd 11975 . . . . . . . . . . . . 13 ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁))
7936, 21, 78syl2anc 411 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁))
80 gcddvds 11947 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
8136, 52, 80syl2anc 411 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
8281simpld 112 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∥ 𝑤)
8381simprd 114 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∥ 𝑁)
84 dvdsmul2 11805 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑀 · 𝑁))
8541, 52, 84syl2anc 411 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → 𝑁 ∥ (𝑀 · 𝑁))
86 nnne0 8936 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
87 simpr 110 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
8887necon3ai 2396 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
8921, 86, 883syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤𝑊) → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
90 gcdn0cl 11946 . . . . . . . . . . . . . . . . . . 19 (((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑁 = 0)) → (𝑤 gcd 𝑁) ∈ ℕ)
9136, 52, 89, 90syl21anc 1237 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∈ ℕ)
9291nnzd 9363 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∈ ℤ)
93 dvdstr 11819 . . . . . . . . . . . . . . . . 17 (((𝑤 gcd 𝑁) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑤 gcd 𝑁) ∥ 𝑁𝑁 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)))
9492, 52, 56, 93syl3anc 1238 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (((𝑤 gcd 𝑁) ∥ 𝑁𝑁 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)))
9583, 85, 94mp2and 433 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁))
96 dvdslegcd 11948 . . . . . . . . . . . . . . . 16 ((((𝑤 gcd 𝑁) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) → (((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁))))
9792, 36, 56, 60, 96syl31anc 1241 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁))))
9882, 95, 97mp2and 433 . . . . . . . . . . . . . 14 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁)))
9998, 65breqtrd 4026 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ≤ 1)
100 nnle1eq1 8932 . . . . . . . . . . . . . 14 ((𝑤 gcd 𝑁) ∈ ℕ → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1))
10191, 100syl 14 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1))
10299, 101mpbid 147 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) = 1)
10379, 102eqtrd 2210 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = 1)
104 oveq1 5876 . . . . . . . . . . . . 13 (𝑦 = (𝑤 mod 𝑁) → (𝑦 gcd 𝑁) = ((𝑤 mod 𝑁) gcd 𝑁))
105104eqeq1d 2186 . . . . . . . . . . . 12 (𝑦 = (𝑤 mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝑤 mod 𝑁) gcd 𝑁) = 1))
106 phimul.5 . . . . . . . . . . . 12 𝑉 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}
107105, 106elrab2 2896 . . . . . . . . . . 11 ((𝑤 mod 𝑁) ∈ 𝑉 ↔ ((𝑤 mod 𝑁) ∈ (0..^𝑁) ∧ ((𝑤 mod 𝑁) gcd 𝑁) = 1))
10877, 103, 107sylanbrc 417 . . . . . . . . . 10 ((𝜑𝑤𝑊) → (𝑤 mod 𝑁) ∈ 𝑉)
109 opelxpi 4655 . . . . . . . . . 10 (((𝑤 mod 𝑀) ∈ 𝑈 ∧ (𝑤 mod 𝑁) ∈ 𝑉) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
11075, 108, 109syl2anc 411 . . . . . . . . 9 ((𝜑𝑤𝑊) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
11133, 110eqeltrd 2254 . . . . . . . 8 ((𝜑𝑤𝑊) → (𝐹𝑤) ∈ (𝑈 × 𝑉))
112111ralrimiva 2550 . . . . . . 7 (𝜑 → ∀𝑤𝑊 (𝐹𝑤) ∈ (𝑈 × 𝑉))
113 crth.2 . . . . . . . . . 10 𝑇 = ((0..^𝑀) × (0..^𝑁))
1148, 113, 31, 13crth 12207 . . . . . . . . 9 (𝜑𝐹:𝑆1-1-onto𝑇)
115 f1ofn 5458 . . . . . . . . 9 (𝐹:𝑆1-1-onto𝑇𝐹 Fn 𝑆)
116 fnfun 5309 . . . . . . . . 9 (𝐹 Fn 𝑆 → Fun 𝐹)
117114, 115, 1163syl 17 . . . . . . . 8 (𝜑 → Fun 𝐹)
118 ssrab2 3240 . . . . . . . . . 10 {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} ⊆ 𝑆
1193, 118eqsstri 3187 . . . . . . . . 9 𝑊𝑆
120 fndm 5311 . . . . . . . . . 10 (𝐹 Fn 𝑆 → dom 𝐹 = 𝑆)
121114, 115, 1203syl 17 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝑆)
122119, 121sseqtrrid 3206 . . . . . . . 8 (𝜑𝑊 ⊆ dom 𝐹)
123 funimass4 5562 . . . . . . . 8 ((Fun 𝐹𝑊 ⊆ dom 𝐹) → ((𝐹𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤𝑊 (𝐹𝑤) ∈ (𝑈 × 𝑉)))
124117, 122, 123syl2anc 411 . . . . . . 7 (𝜑 → ((𝐹𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤𝑊 (𝐹𝑤) ∈ (𝑈 × 𝑉)))
125112, 124mpbird 167 . . . . . 6 (𝜑 → (𝐹𝑊) ⊆ (𝑈 × 𝑉))
126 ssrab2 3240 . . . . . . . . . . . . . 14 {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ⊆ (0..^𝑀)
12773, 126eqsstri 3187 . . . . . . . . . . . . 13 𝑈 ⊆ (0..^𝑀)
128 ssrab2 3240 . . . . . . . . . . . . . 14 {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁)
129106, 128eqsstri 3187 . . . . . . . . . . . . 13 𝑉 ⊆ (0..^𝑁)
130 xpss12 4730 . . . . . . . . . . . . 13 ((𝑈 ⊆ (0..^𝑀) ∧ 𝑉 ⊆ (0..^𝑁)) → (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁)))
131127, 129, 130mp2an 426 . . . . . . . . . . . 12 (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁))
132131, 113sseqtrri 3190 . . . . . . . . . . 11 (𝑈 × 𝑉) ⊆ 𝑇
133132sseli 3151 . . . . . . . . . 10 (𝑧 ∈ (𝑈 × 𝑉) → 𝑧𝑇)
134 f1ocnvfv2 5773 . . . . . . . . . 10 ((𝐹:𝑆1-1-onto𝑇𝑧𝑇) → (𝐹‘(𝐹𝑧)) = 𝑧)
135114, 133, 134syl2an 289 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(𝐹𝑧)) = 𝑧)
136 f1ocnv 5470 . . . . . . . . . . . . 13 (𝐹:𝑆1-1-onto𝑇𝐹:𝑇1-1-onto𝑆)
137 f1of 5457 . . . . . . . . . . . . 13 (𝐹:𝑇1-1-onto𝑆𝐹:𝑇𝑆)
138114, 136, 1373syl 17 . . . . . . . . . . . 12 (𝜑𝐹:𝑇𝑆)
139 ffvelcdm 5645 . . . . . . . . . . . 12 ((𝐹:𝑇𝑆𝑧𝑇) → (𝐹𝑧) ∈ 𝑆)
140138, 133, 139syl2an 289 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ 𝑆)
141140, 8eleqtrdi 2270 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ (0..^(𝑀 · 𝑁)))
142 elfzoelz 10133 . . . . . . . . . . . . . . 15 ((𝐹𝑧) ∈ (0..^(𝑀 · 𝑁)) → (𝐹𝑧) ∈ ℤ)
143141, 142syl 14 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ ℤ)
14414adantr 276 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℕ)
145 modgcd 11975 . . . . . . . . . . . . . 14 (((𝐹𝑧) ∈ ℤ ∧ 𝑀 ∈ ℕ) → (((𝐹𝑧) mod 𝑀) gcd 𝑀) = ((𝐹𝑧) gcd 𝑀))
146143, 144, 145syl2anc 411 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) gcd 𝑀) = ((𝐹𝑧) gcd 𝑀))
147 zq 9615 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑧) ∈ ℤ → (𝐹𝑧) ∈ ℚ)
148143, 147syl 14 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ ℚ)
149144, 16syl 14 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℚ)
150144nngt0d 8952 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 0 < 𝑀)
151148, 149, 150modqcld 10314 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑀) ∈ ℚ)
15220adantr 276 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℕ)
153152, 22syl 14 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℚ)
154152nngt0d 8952 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 0 < 𝑁)
155148, 153, 154modqcld 10314 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑁) ∈ ℚ)
156 opexg 4225 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑧) mod 𝑀) ∈ ℚ ∧ ((𝐹𝑧) mod 𝑁) ∈ ℚ) → ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ V)
157151, 155, 156syl2anc 411 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ V)
158 oveq1 5876 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = (𝐹𝑧) → (𝑤 mod 𝑀) = ((𝐹𝑧) mod 𝑀))
159 oveq1 5876 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = (𝐹𝑧) → (𝑤 mod 𝑁) = ((𝐹𝑧) mod 𝑁))
160158, 159opeq12d 3784 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = (𝐹𝑧) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
16130cbvmptv 4096 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩) = (𝑤𝑆 ↦ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
16231, 161eqtri 2198 . . . . . . . . . . . . . . . . . . . . 21 𝐹 = (𝑤𝑆 ↦ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
163160, 162fvmptg 5588 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑧) ∈ 𝑆 ∧ ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ V) → (𝐹‘(𝐹𝑧)) = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
164140, 157, 163syl2anc 411 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(𝐹𝑧)) = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
165135, 164eqtr3d 2212 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
166 simpr 110 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝑈 × 𝑉))
167165, 166eqeltrrd 2255 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
168 opelxp 4653 . . . . . . . . . . . . . . . . 17 (⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ (𝑈 × 𝑉) ↔ (((𝐹𝑧) mod 𝑀) ∈ 𝑈 ∧ ((𝐹𝑧) mod 𝑁) ∈ 𝑉))
169167, 168sylib 122 . . . . . . . . . . . . . . . 16 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) ∈ 𝑈 ∧ ((𝐹𝑧) mod 𝑁) ∈ 𝑉))
170169simpld 112 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑀) ∈ 𝑈)
171 oveq1 5876 . . . . . . . . . . . . . . . . 17 (𝑦 = ((𝐹𝑧) mod 𝑀) → (𝑦 gcd 𝑀) = (((𝐹𝑧) mod 𝑀) gcd 𝑀))
172171eqeq1d 2186 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝐹𝑧) mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1))
173172, 73elrab2 2896 . . . . . . . . . . . . . . 15 (((𝐹𝑧) mod 𝑀) ∈ 𝑈 ↔ (((𝐹𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1))
174170, 173sylib 122 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1))
175174simprd 114 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1)
176146, 175eqtr3d 2212 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) gcd 𝑀) = 1)
177 modgcd 11975 . . . . . . . . . . . . . 14 (((𝐹𝑧) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐹𝑧) mod 𝑁) gcd 𝑁) = ((𝐹𝑧) gcd 𝑁))
178143, 152, 177syl2anc 411 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑁) gcd 𝑁) = ((𝐹𝑧) gcd 𝑁))
179169simprd 114 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑁) ∈ 𝑉)
180 oveq1 5876 . . . . . . . . . . . . . . . . 17 (𝑦 = ((𝐹𝑧) mod 𝑁) → (𝑦 gcd 𝑁) = (((𝐹𝑧) mod 𝑁) gcd 𝑁))
181180eqeq1d 2186 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝐹𝑧) mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1))
182181, 106elrab2 2896 . . . . . . . . . . . . . . 15 (((𝐹𝑧) mod 𝑁) ∈ 𝑉 ↔ (((𝐹𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1))
183179, 182sylib 122 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1))
184183simprd 114 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1)
185178, 184eqtr3d 2212 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) gcd 𝑁) = 1)
18614nnzd 9363 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℤ)
187186adantr 276 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℤ)
18820nnzd 9363 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
189188adantr 276 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℤ)
190 rpmul 12081 . . . . . . . . . . . . 13 (((𝐹𝑧) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((((𝐹𝑧) gcd 𝑀) = 1 ∧ ((𝐹𝑧) gcd 𝑁) = 1) → ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
191143, 187, 189, 190syl3anc 1238 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((((𝐹𝑧) gcd 𝑀) = 1 ∧ ((𝐹𝑧) gcd 𝑁) = 1) → ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
192176, 185, 191mp2and 433 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1)
193 oveq1 5876 . . . . . . . . . . . . 13 (𝑦 = (𝐹𝑧) → (𝑦 gcd (𝑀 · 𝑁)) = ((𝐹𝑧) gcd (𝑀 · 𝑁)))
194193eqeq1d 2186 . . . . . . . . . . . 12 (𝑦 = (𝐹𝑧) → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
195194, 3elrab2 2896 . . . . . . . . . . 11 ((𝐹𝑧) ∈ 𝑊 ↔ ((𝐹𝑧) ∈ 𝑆 ∧ ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
196140, 192, 195sylanbrc 417 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ 𝑊)
197 funfvima2 5744 . . . . . . . . . . . 12 ((Fun 𝐹𝑊 ⊆ dom 𝐹) → ((𝐹𝑧) ∈ 𝑊 → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊)))
198117, 122, 197syl2anc 411 . . . . . . . . . . 11 (𝜑 → ((𝐹𝑧) ∈ 𝑊 → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊)))
199198imp 124 . . . . . . . . . 10 ((𝜑 ∧ (𝐹𝑧) ∈ 𝑊) → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊))
200196, 199syldan 282 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊))
201135, 200eqeltrrd 2255 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝐹𝑊))
202201ex 115 . . . . . . 7 (𝜑 → (𝑧 ∈ (𝑈 × 𝑉) → 𝑧 ∈ (𝐹𝑊)))
203202ssrdv 3161 . . . . . 6 (𝜑 → (𝑈 × 𝑉) ⊆ (𝐹𝑊))
204125, 203eqssd 3172 . . . . 5 (𝜑 → (𝐹𝑊) = (𝑈 × 𝑉))
205 f1of1 5456 . . . . . . 7 (𝐹:𝑆1-1-onto𝑇𝐹:𝑆1-1𝑇)
206114, 205syl 14 . . . . . 6 (𝜑𝐹:𝑆1-1𝑇)
207119a1i 9 . . . . . 6 (𝜑𝑊𝑆)
208 0z 9253 . . . . . . . . . 10 0 ∈ ℤ
209186, 188zmulcld 9370 . . . . . . . . . 10 (𝜑 → (𝑀 · 𝑁) ∈ ℤ)
210 fzofig 10418 . . . . . . . . . 10 ((0 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (0..^(𝑀 · 𝑁)) ∈ Fin)
211208, 209, 210sylancr 414 . . . . . . . . 9 (𝜑 → (0..^(𝑀 · 𝑁)) ∈ Fin)
2128, 211eqeltrid 2264 . . . . . . . 8 (𝜑𝑆 ∈ Fin)
213 elfzoelz 10133 . . . . . . . . . . . . . 14 (𝑦 ∈ (0..^(𝑀 · 𝑁)) → 𝑦 ∈ ℤ)
214213, 8eleq2s 2272 . . . . . . . . . . . . 13 (𝑦𝑆𝑦 ∈ ℤ)
215214adantl 277 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → 𝑦 ∈ ℤ)
216209adantr 276 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → (𝑀 · 𝑁) ∈ ℤ)
217215, 216gcdcld 11952 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → (𝑦 gcd (𝑀 · 𝑁)) ∈ ℕ0)
218217nn0zd 9362 . . . . . . . . . 10 ((𝜑𝑦𝑆) → (𝑦 gcd (𝑀 · 𝑁)) ∈ ℤ)
219 1zzd 9269 . . . . . . . . . 10 ((𝜑𝑦𝑆) → 1 ∈ ℤ)
220 zdceq 9317 . . . . . . . . . 10 (((𝑦 gcd (𝑀 · 𝑁)) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝑦 gcd (𝑀 · 𝑁)) = 1)
221218, 219, 220syl2anc 411 . . . . . . . . 9 ((𝜑𝑦𝑆) → DECID (𝑦 gcd (𝑀 · 𝑁)) = 1)
222221ralrimiva 2550 . . . . . . . 8 (𝜑 → ∀𝑦𝑆 DECID (𝑦 gcd (𝑀 · 𝑁)) = 1)
223212, 222ssfirab 6927 . . . . . . 7 (𝜑 → {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} ∈ Fin)
2243, 223eqeltrid 2264 . . . . . 6 (𝜑𝑊 ∈ Fin)
225 f1imaeng 6786 . . . . . 6 ((𝐹:𝑆1-1𝑇𝑊𝑆𝑊 ∈ Fin) → (𝐹𝑊) ≈ 𝑊)
226206, 207, 224, 225syl3anc 1238 . . . . 5 (𝜑 → (𝐹𝑊) ≈ 𝑊)
227204, 226eqbrtrrd 4024 . . . 4 (𝜑 → (𝑈 × 𝑉) ≈ 𝑊)
228 fzofig 10418 . . . . . . . . 9 ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0..^𝑀) ∈ Fin)
229208, 186, 228sylancr 414 . . . . . . . 8 (𝜑 → (0..^𝑀) ∈ Fin)
230 elfzoelz 10133 . . . . . . . . . . . . 13 (𝑦 ∈ (0..^𝑀) → 𝑦 ∈ ℤ)
231230adantl 277 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑀)) → 𝑦 ∈ ℤ)
232186adantr 276 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑀)) → 𝑀 ∈ ℤ)
233231, 232gcdcld 11952 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (0..^𝑀)) → (𝑦 gcd 𝑀) ∈ ℕ0)
234233nn0zd 9362 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0..^𝑀)) → (𝑦 gcd 𝑀) ∈ ℤ)
235 1z 9268 . . . . . . . . . 10 1 ∈ ℤ
236 zdceq 9317 . . . . . . . . . 10 (((𝑦 gcd 𝑀) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝑦 gcd 𝑀) = 1)
237234, 235, 236sylancl 413 . . . . . . . . 9 ((𝜑𝑦 ∈ (0..^𝑀)) → DECID (𝑦 gcd 𝑀) = 1)
238237ralrimiva 2550 . . . . . . . 8 (𝜑 → ∀𝑦 ∈ (0..^𝑀)DECID (𝑦 gcd 𝑀) = 1)
239229, 238ssfirab 6927 . . . . . . 7 (𝜑 → {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ∈ Fin)
24073, 239eqeltrid 2264 . . . . . 6 (𝜑𝑈 ∈ Fin)
241 fzofig 10418 . . . . . . . . 9 ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0..^𝑁) ∈ Fin)
242208, 188, 241sylancr 414 . . . . . . . 8 (𝜑 → (0..^𝑁) ∈ Fin)
243 elfzoelz 10133 . . . . . . . . . . . . 13 (𝑦 ∈ (0..^𝑁) → 𝑦 ∈ ℤ)
244243adantl 277 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑁)) → 𝑦 ∈ ℤ)
245188adantr 276 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑁)) → 𝑁 ∈ ℤ)
246244, 245gcdcld 11952 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (0..^𝑁)) → (𝑦 gcd 𝑁) ∈ ℕ0)
247246nn0zd 9362 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0..^𝑁)) → (𝑦 gcd 𝑁) ∈ ℤ)
248 1zzd 9269 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0..^𝑁)) → 1 ∈ ℤ)
249 zdceq 9317 . . . . . . . . . 10 (((𝑦 gcd 𝑁) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝑦 gcd 𝑁) = 1)
250247, 248, 249syl2anc 411 . . . . . . . . 9 ((𝜑𝑦 ∈ (0..^𝑁)) → DECID (𝑦 gcd 𝑁) = 1)
251250ralrimiva 2550 . . . . . . . 8 (𝜑 → ∀𝑦 ∈ (0..^𝑁)DECID (𝑦 gcd 𝑁) = 1)
252242, 251ssfirab 6927 . . . . . . 7 (𝜑 → {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ∈ Fin)
253106, 252eqeltrid 2264 . . . . . 6 (𝜑𝑉 ∈ Fin)
254 xpfi 6923 . . . . . 6 ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) → (𝑈 × 𝑉) ∈ Fin)
255240, 253, 254syl2anc 411 . . . . 5 (𝜑 → (𝑈 × 𝑉) ∈ Fin)
256 hashen 10748 . . . . 5 (((𝑈 × 𝑉) ∈ Fin ∧ 𝑊 ∈ Fin) → ((♯‘(𝑈 × 𝑉)) = (♯‘𝑊) ↔ (𝑈 × 𝑉) ≈ 𝑊))
257255, 224, 256syl2anc 411 . . . 4 (𝜑 → ((♯‘(𝑈 × 𝑉)) = (♯‘𝑊) ↔ (𝑈 × 𝑉) ≈ 𝑊))
258227, 257mpbird 167 . . 3 (𝜑 → (♯‘(𝑈 × 𝑉)) = (♯‘𝑊))
259 hashxp 10790 . . . 4 ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) → (♯‘(𝑈 × 𝑉)) = ((♯‘𝑈) · (♯‘𝑉)))
260240, 253, 259syl2anc 411 . . 3 (𝜑 → (♯‘(𝑈 × 𝑉)) = ((♯‘𝑈) · (♯‘𝑉)))
261258, 260eqtr3d 2212 . 2 (𝜑 → (♯‘𝑊) = ((♯‘𝑈) · (♯‘𝑉)))
26214, 20nnmulcld 8957 . . 3 (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
263 dfphi2 12203 . . . 4 ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (♯‘{𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}))
2648rabeqi 2730 . . . . . 6 {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
2653, 264eqtri 2198 . . . . 5 𝑊 = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
266265fveq2i 5514 . . . 4 (♯‘𝑊) = (♯‘{𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1})
267263, 266eqtr4di 2228 . . 3 ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (♯‘𝑊))
268262, 267syl 14 . 2 (𝜑 → (ϕ‘(𝑀 · 𝑁)) = (♯‘𝑊))
269 dfphi2 12203 . . . . 5 (𝑀 ∈ ℕ → (ϕ‘𝑀) = (♯‘{𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}))
27073fveq2i 5514 . . . . 5 (♯‘𝑈) = (♯‘{𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1})
271269, 270eqtr4di 2228 . . . 4 (𝑀 ∈ ℕ → (ϕ‘𝑀) = (♯‘𝑈))
27214, 271syl 14 . . 3 (𝜑 → (ϕ‘𝑀) = (♯‘𝑈))
273 dfphi2 12203 . . . . 5 (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘{𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}))
274106fveq2i 5514 . . . . 5 (♯‘𝑉) = (♯‘{𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1})
275273, 274eqtr4di 2228 . . . 4 (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘𝑉))
27620, 275syl 14 . . 3 (𝜑 → (ϕ‘𝑁) = (♯‘𝑉))
277272, 276oveq12d 5887 . 2 (𝜑 → ((ϕ‘𝑀) · (ϕ‘𝑁)) = ((♯‘𝑈) · (♯‘𝑉)))
278261, 268, 2773eqtr4d 2220 1 (𝜑 → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  DECID wdc 834  w3a 978   = wceq 1353  wcel 2148  wne 2347  wral 2455  {crab 2459  Vcvv 2737  wss 3129  cop 3594   class class class wbr 4000  cmpt 4061   × cxp 4621  ccnv 4622  dom cdm 4623  cima 4626  Fun wfun 5206   Fn wfn 5207  wf 5208  1-1wf1 5209  1-1-ontowf1o 5211  cfv 5212  (class class class)co 5869  cen 6732  Fincfn 6734  0cc0 7802  1c1 7803   · cmul 7807  cle 7983  cn 8908  cz 9242  cq 9608  ..^cfzo 10128   mod cmo 10308  chash 10739  cdvds 11778   gcd cgcd 11926  ϕcphi 12192
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4115  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-iinf 4584  ax-cnex 7893  ax-resscn 7894  ax-1cn 7895  ax-1re 7896  ax-icn 7897  ax-addcl 7898  ax-addrcl 7899  ax-mulcl 7900  ax-mulrcl 7901  ax-addcom 7902  ax-mulcom 7903  ax-addass 7904  ax-mulass 7905  ax-distr 7906  ax-i2m1 7907  ax-0lt1 7908  ax-1rid 7909  ax-0id 7910  ax-rnegex 7911  ax-precex 7912  ax-cnre 7913  ax-pre-ltirr 7914  ax-pre-ltwlin 7915  ax-pre-lttrn 7916  ax-pre-apti 7917  ax-pre-ltadd 7918  ax-pre-mulgt0 7919  ax-pre-mulext 7920  ax-arch 7921  ax-caucvg 7922
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-id 4290  df-po 4293  df-iso 4294  df-iord 4363  df-on 4365  df-ilim 4366  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-riota 5825  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-recs 6300  df-irdg 6365  df-frec 6386  df-1o 6411  df-oadd 6415  df-er 6529  df-en 6735  df-dom 6736  df-fin 6737  df-sup 6977  df-pnf 7984  df-mnf 7985  df-xr 7986  df-ltxr 7987  df-le 7988  df-sub 8120  df-neg 8121  df-reap 8522  df-ap 8529  df-div 8619  df-inn 8909  df-2 8967  df-3 8968  df-4 8969  df-n0 9166  df-z 9243  df-uz 9518  df-q 9609  df-rp 9641  df-fz 9996  df-fzo 10129  df-fl 10256  df-mod 10309  df-seqfrec 10432  df-exp 10506  df-ihash 10740  df-cj 10835  df-re 10836  df-im 10837  df-rsqrt 10991  df-abs 10992  df-dvds 11779  df-gcd 11927  df-phi 12194
This theorem is referenced by:  phimul  12209
  Copyright terms: Public domain W3C validator