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

Theorem phimullem 11107
Description: Lemma for phimul 11108. (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 5622 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → (𝑦 gcd (𝑀 · 𝑁)) = (𝑤 gcd (𝑀 · 𝑁)))
21eqeq1d 2093 . . . . . . . . . . . . 13 (𝑦 = 𝑤 → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ (𝑤 gcd (𝑀 · 𝑁)) = 1))
3 phimul.6 . . . . . . . . . . . . 13 𝑊 = {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
42, 3elrab2 2765 . . . . . . . . . . . 12 (𝑤𝑊 ↔ (𝑤𝑆 ∧ (𝑤 gcd (𝑀 · 𝑁)) = 1))
54simplbi 268 . . . . . . . . . . 11 (𝑤𝑊𝑤𝑆)
65adantl 271 . . . . . . . . . 10 ((𝜑𝑤𝑊) → 𝑤𝑆)
7 elfzoelz 9489 . . . . . . . . . . . . . . 15 (𝑤 ∈ (0..^(𝑀 · 𝑁)) → 𝑤 ∈ ℤ)
8 crth.1 . . . . . . . . . . . . . . 15 𝑆 = (0..^(𝑀 · 𝑁))
97, 8eleq2s 2179 . . . . . . . . . . . . . 14 (𝑤𝑆𝑤 ∈ ℤ)
106, 9syl 14 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑤 ∈ ℤ)
11 zq 9046 . . . . . . . . . . . . 13 (𝑤 ∈ ℤ → 𝑤 ∈ ℚ)
1210, 11syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑤 ∈ ℚ)
13 crth.4 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1))
1413simp1d 953 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℕ)
1514adantr 270 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑀 ∈ ℕ)
16 nnq 9053 . . . . . . . . . . . . 13 (𝑀 ∈ ℕ → 𝑀 ∈ ℚ)
1715, 16syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑀 ∈ ℚ)
1815nngt0d 8403 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 0 < 𝑀)
1912, 17, 18modqcld 9666 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑀) ∈ ℚ)
2013simp2d 954 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ)
2120adantr 270 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑁 ∈ ℕ)
22 nnq 9053 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 𝑁 ∈ ℚ)
2321, 22syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑁 ∈ ℚ)
2421nngt0d 8403 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 0 < 𝑁)
2512, 23, 24modqcld 9666 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑁) ∈ ℚ)
26 opexg 4031 . . . . . . . . . . 11 (((𝑤 mod 𝑀) ∈ ℚ ∧ (𝑤 mod 𝑁) ∈ ℚ) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ V)
2719, 25, 26syl2anc 403 . . . . . . . . . 10 ((𝜑𝑤𝑊) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ V)
28 oveq1 5622 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝑥 mod 𝑀) = (𝑤 mod 𝑀))
29 oveq1 5622 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝑥 mod 𝑁) = (𝑤 mod 𝑁))
3028, 29opeq12d 3615 . . . . . . . . . . 11 (𝑥 = 𝑤 → ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩ = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
31 crth.3 . . . . . . . . . . 11 𝐹 = (𝑥𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩)
3230, 31fvmptg 5345 . . . . . . . . . 10 ((𝑤𝑆 ∧ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ V) → (𝐹𝑤) = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
336, 27, 32syl2anc 403 . . . . . . . . 9 ((𝜑𝑤𝑊) → (𝐹𝑤) = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
345, 8syl6eleq 2177 . . . . . . . . . . . . . 14 (𝑤𝑊𝑤 ∈ (0..^(𝑀 · 𝑁)))
3534adantl 271 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑤 ∈ (0..^(𝑀 · 𝑁)))
3635, 7syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑤 ∈ ℤ)
37 zmodfzo 9685 . . . . . . . . . . . 12 ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑤 mod 𝑀) ∈ (0..^𝑀))
3836, 15, 37syl2anc 403 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑀) ∈ (0..^𝑀))
39 modgcd 10888 . . . . . . . . . . . . 13 ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀))
4036, 15, 39syl2anc 403 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀))
4115nnzd 8803 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → 𝑀 ∈ ℤ)
42 gcddvds 10861 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
4336, 41, 42syl2anc 403 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
4443simpld 110 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∥ 𝑤)
45 nnne0 8388 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℕ → 𝑀 ≠ 0)
46 simpr 108 . . . . . . . . . . . . . . . . . . . 20 ((𝑤 = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
4746necon3ai 2300 . . . . . . . . . . . . . . . . . . 19 (𝑀 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
4815, 45, 473syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤𝑊) → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
49 gcdn0cl 10860 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑀 = 0)) → (𝑤 gcd 𝑀) ∈ ℕ)
5036, 41, 48, 49syl21anc 1171 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∈ ℕ)
5150nnzd 8803 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∈ ℤ)
5221nnzd 8803 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → 𝑁 ∈ ℤ)
5343simprd 112 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∥ 𝑀)
5451, 41, 52, 53dvdsmultr1d 10741 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁))
5515, 21nnmulcld 8408 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → (𝑀 · 𝑁) ∈ ℕ)
5655nnzd 8803 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑀 · 𝑁) ∈ ℤ)
57 nnne0 8388 . . . . . . . . . . . . . . . . 17 ((𝑀 · 𝑁) ∈ ℕ → (𝑀 · 𝑁) ≠ 0)
58 simpr 108 . . . . . . . . . . . . . . . . . 18 ((𝑤 = 0 ∧ (𝑀 · 𝑁) = 0) → (𝑀 · 𝑁) = 0)
5958necon3ai 2300 . . . . . . . . . . . . . . . . 17 ((𝑀 · 𝑁) ≠ 0 → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0))
6055, 57, 593syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0))
61 dvdslegcd 10862 . . . . . . . . . . . . . . . 16 ((((𝑤 gcd 𝑀) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) → (((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁))))
6251, 36, 56, 60, 61syl31anc 1175 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁))))
6344, 54, 62mp2and 424 . . . . . . . . . . . . . 14 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁)))
644simprbi 269 . . . . . . . . . . . . . . 15 (𝑤𝑊 → (𝑤 gcd (𝑀 · 𝑁)) = 1)
6564adantl 271 . . . . . . . . . . . . . 14 ((𝜑𝑤𝑊) → (𝑤 gcd (𝑀 · 𝑁)) = 1)
6663, 65breqtrd 3846 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ≤ 1)
67 nnle1eq1 8384 . . . . . . . . . . . . . 14 ((𝑤 gcd 𝑀) ∈ ℕ → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1))
6850, 67syl 14 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1))
6966, 68mpbid 145 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) = 1)
7040, 69eqtrd 2117 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = 1)
71 oveq1 5622 . . . . . . . . . . . . 13 (𝑦 = (𝑤 mod 𝑀) → (𝑦 gcd 𝑀) = ((𝑤 mod 𝑀) gcd 𝑀))
7271eqeq1d 2093 . . . . . . . . . . . 12 (𝑦 = (𝑤 mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ ((𝑤 mod 𝑀) gcd 𝑀) = 1))
73 phimul.4 . . . . . . . . . . . 12 𝑈 = {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}
7472, 73elrab2 2765 . . . . . . . . . . 11 ((𝑤 mod 𝑀) ∈ 𝑈 ↔ ((𝑤 mod 𝑀) ∈ (0..^𝑀) ∧ ((𝑤 mod 𝑀) gcd 𝑀) = 1))
7538, 70, 74sylanbrc 408 . . . . . . . . . 10 ((𝜑𝑤𝑊) → (𝑤 mod 𝑀) ∈ 𝑈)
76 zmodfzo 9685 . . . . . . . . . . . 12 ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑤 mod 𝑁) ∈ (0..^𝑁))
7736, 21, 76syl2anc 403 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑁) ∈ (0..^𝑁))
78 modgcd 10888 . . . . . . . . . . . . 13 ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁))
7936, 21, 78syl2anc 403 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁))
80 gcddvds 10861 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
8136, 52, 80syl2anc 403 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
8281simpld 110 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∥ 𝑤)
8381simprd 112 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∥ 𝑁)
84 dvdsmul2 10725 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑀 · 𝑁))
8541, 52, 84syl2anc 403 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → 𝑁 ∥ (𝑀 · 𝑁))
86 nnne0 8388 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
87 simpr 108 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
8887necon3ai 2300 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
8921, 86, 883syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤𝑊) → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
90 gcdn0cl 10860 . . . . . . . . . . . . . . . . . . 19 (((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑁 = 0)) → (𝑤 gcd 𝑁) ∈ ℕ)
9136, 52, 89, 90syl21anc 1171 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∈ ℕ)
9291nnzd 8803 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∈ ℤ)
93 dvdstr 10739 . . . . . . . . . . . . . . . . 17 (((𝑤 gcd 𝑁) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑤 gcd 𝑁) ∥ 𝑁𝑁 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)))
9492, 52, 56, 93syl3anc 1172 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (((𝑤 gcd 𝑁) ∥ 𝑁𝑁 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)))
9583, 85, 94mp2and 424 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁))
96 dvdslegcd 10862 . . . . . . . . . . . . . . . 16 ((((𝑤 gcd 𝑁) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) → (((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁))))
9792, 36, 56, 60, 96syl31anc 1175 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁))))
9882, 95, 97mp2and 424 . . . . . . . . . . . . . 14 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁)))
9998, 65breqtrd 3846 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ≤ 1)
100 nnle1eq1 8384 . . . . . . . . . . . . . 14 ((𝑤 gcd 𝑁) ∈ ℕ → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1))
10191, 100syl 14 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1))
10299, 101mpbid 145 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) = 1)
10379, 102eqtrd 2117 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = 1)
104 oveq1 5622 . . . . . . . . . . . . 13 (𝑦 = (𝑤 mod 𝑁) → (𝑦 gcd 𝑁) = ((𝑤 mod 𝑁) gcd 𝑁))
105104eqeq1d 2093 . . . . . . . . . . . 12 (𝑦 = (𝑤 mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝑤 mod 𝑁) gcd 𝑁) = 1))
106 phimul.5 . . . . . . . . . . . 12 𝑉 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}
107105, 106elrab2 2765 . . . . . . . . . . 11 ((𝑤 mod 𝑁) ∈ 𝑉 ↔ ((𝑤 mod 𝑁) ∈ (0..^𝑁) ∧ ((𝑤 mod 𝑁) gcd 𝑁) = 1))
10877, 103, 107sylanbrc 408 . . . . . . . . . 10 ((𝜑𝑤𝑊) → (𝑤 mod 𝑁) ∈ 𝑉)
109 opelxpi 4444 . . . . . . . . . 10 (((𝑤 mod 𝑀) ∈ 𝑈 ∧ (𝑤 mod 𝑁) ∈ 𝑉) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
11075, 108, 109syl2anc 403 . . . . . . . . 9 ((𝜑𝑤𝑊) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
11133, 110eqeltrd 2161 . . . . . . . 8 ((𝜑𝑤𝑊) → (𝐹𝑤) ∈ (𝑈 × 𝑉))
112111ralrimiva 2442 . . . . . . 7 (𝜑 → ∀𝑤𝑊 (𝐹𝑤) ∈ (𝑈 × 𝑉))
113 crth.2 . . . . . . . . . 10 𝑇 = ((0..^𝑀) × (0..^𝑁))
1148, 113, 31, 13crth 11106 . . . . . . . . 9 (𝜑𝐹:𝑆1-1-onto𝑇)
115 f1ofn 5219 . . . . . . . . 9 (𝐹:𝑆1-1-onto𝑇𝐹 Fn 𝑆)
116 fnfun 5078 . . . . . . . . 9 (𝐹 Fn 𝑆 → Fun 𝐹)
117114, 115, 1163syl 17 . . . . . . . 8 (𝜑 → Fun 𝐹)
118 ssrab2 3095 . . . . . . . . . 10 {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} ⊆ 𝑆
1193, 118eqsstri 3045 . . . . . . . . 9 𝑊𝑆
120 fndm 5080 . . . . . . . . . 10 (𝐹 Fn 𝑆 → dom 𝐹 = 𝑆)
121114, 115, 1203syl 17 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝑆)
122119, 121syl5sseqr 3064 . . . . . . . 8 (𝜑𝑊 ⊆ dom 𝐹)
123 funimass4 5320 . . . . . . . 8 ((Fun 𝐹𝑊 ⊆ dom 𝐹) → ((𝐹𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤𝑊 (𝐹𝑤) ∈ (𝑈 × 𝑉)))
124117, 122, 123syl2anc 403 . . . . . . 7 (𝜑 → ((𝐹𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤𝑊 (𝐹𝑤) ∈ (𝑈 × 𝑉)))
125112, 124mpbird 165 . . . . . 6 (𝜑 → (𝐹𝑊) ⊆ (𝑈 × 𝑉))
126 ssrab2 3095 . . . . . . . . . . . . . 14 {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ⊆ (0..^𝑀)
12773, 126eqsstri 3045 . . . . . . . . . . . . 13 𝑈 ⊆ (0..^𝑀)
128 ssrab2 3095 . . . . . . . . . . . . . 14 {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁)
129106, 128eqsstri 3045 . . . . . . . . . . . . 13 𝑉 ⊆ (0..^𝑁)
130 xpss12 4515 . . . . . . . . . . . . 13 ((𝑈 ⊆ (0..^𝑀) ∧ 𝑉 ⊆ (0..^𝑁)) → (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁)))
131127, 129, 130mp2an 417 . . . . . . . . . . . 12 (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁))
132131, 113sseqtr4i 3048 . . . . . . . . . . 11 (𝑈 × 𝑉) ⊆ 𝑇
133132sseli 3010 . . . . . . . . . 10 (𝑧 ∈ (𝑈 × 𝑉) → 𝑧𝑇)
134 f1ocnvfv2 5520 . . . . . . . . . 10 ((𝐹:𝑆1-1-onto𝑇𝑧𝑇) → (𝐹‘(𝐹𝑧)) = 𝑧)
135114, 133, 134syl2an 283 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(𝐹𝑧)) = 𝑧)
136 f1ocnv 5231 . . . . . . . . . . . . 13 (𝐹:𝑆1-1-onto𝑇𝐹:𝑇1-1-onto𝑆)
137 f1of 5218 . . . . . . . . . . . . 13 (𝐹:𝑇1-1-onto𝑆𝐹:𝑇𝑆)
138114, 136, 1373syl 17 . . . . . . . . . . . 12 (𝜑𝐹:𝑇𝑆)
139 ffvelrn 5397 . . . . . . . . . . . 12 ((𝐹:𝑇𝑆𝑧𝑇) → (𝐹𝑧) ∈ 𝑆)
140138, 133, 139syl2an 283 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ 𝑆)
141140, 8syl6eleq 2177 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ (0..^(𝑀 · 𝑁)))
142 elfzoelz 9489 . . . . . . . . . . . . . . 15 ((𝐹𝑧) ∈ (0..^(𝑀 · 𝑁)) → (𝐹𝑧) ∈ ℤ)
143141, 142syl 14 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ ℤ)
14414adantr 270 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℕ)
145 modgcd 10888 . . . . . . . . . . . . . 14 (((𝐹𝑧) ∈ ℤ ∧ 𝑀 ∈ ℕ) → (((𝐹𝑧) mod 𝑀) gcd 𝑀) = ((𝐹𝑧) gcd 𝑀))
146143, 144, 145syl2anc 403 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) gcd 𝑀) = ((𝐹𝑧) gcd 𝑀))
147 zq 9046 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑧) ∈ ℤ → (𝐹𝑧) ∈ ℚ)
148143, 147syl 14 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ ℚ)
149144, 16syl 14 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℚ)
150144nngt0d 8403 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 0 < 𝑀)
151148, 149, 150modqcld 9666 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑀) ∈ ℚ)
15220adantr 270 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℕ)
153152, 22syl 14 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℚ)
154152nngt0d 8403 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 0 < 𝑁)
155148, 153, 154modqcld 9666 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑁) ∈ ℚ)
156 opexg 4031 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑧) mod 𝑀) ∈ ℚ ∧ ((𝐹𝑧) mod 𝑁) ∈ ℚ) → ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ V)
157151, 155, 156syl2anc 403 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ V)
158 oveq1 5622 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = (𝐹𝑧) → (𝑤 mod 𝑀) = ((𝐹𝑧) mod 𝑀))
159 oveq1 5622 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = (𝐹𝑧) → (𝑤 mod 𝑁) = ((𝐹𝑧) mod 𝑁))
160158, 159opeq12d 3615 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = (𝐹𝑧) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
16130cbvmptv 3911 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩) = (𝑤𝑆 ↦ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
16231, 161eqtri 2105 . . . . . . . . . . . . . . . . . . . . 21 𝐹 = (𝑤𝑆 ↦ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
163160, 162fvmptg 5345 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑧) ∈ 𝑆 ∧ ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ V) → (𝐹‘(𝐹𝑧)) = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
164140, 157, 163syl2anc 403 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(𝐹𝑧)) = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
165135, 164eqtr3d 2119 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
166 simpr 108 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝑈 × 𝑉))
167165, 166eqeltrrd 2162 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
168 opelxp 4442 . . . . . . . . . . . . . . . . 17 (⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ (𝑈 × 𝑉) ↔ (((𝐹𝑧) mod 𝑀) ∈ 𝑈 ∧ ((𝐹𝑧) mod 𝑁) ∈ 𝑉))
169167, 168sylib 120 . . . . . . . . . . . . . . . 16 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) ∈ 𝑈 ∧ ((𝐹𝑧) mod 𝑁) ∈ 𝑉))
170169simpld 110 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑀) ∈ 𝑈)
171 oveq1 5622 . . . . . . . . . . . . . . . . 17 (𝑦 = ((𝐹𝑧) mod 𝑀) → (𝑦 gcd 𝑀) = (((𝐹𝑧) mod 𝑀) gcd 𝑀))
172171eqeq1d 2093 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝐹𝑧) mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1))
173172, 73elrab2 2765 . . . . . . . . . . . . . . 15 (((𝐹𝑧) mod 𝑀) ∈ 𝑈 ↔ (((𝐹𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1))
174170, 173sylib 120 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1))
175174simprd 112 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1)
176146, 175eqtr3d 2119 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) gcd 𝑀) = 1)
177 modgcd 10888 . . . . . . . . . . . . . 14 (((𝐹𝑧) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐹𝑧) mod 𝑁) gcd 𝑁) = ((𝐹𝑧) gcd 𝑁))
178143, 152, 177syl2anc 403 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑁) gcd 𝑁) = ((𝐹𝑧) gcd 𝑁))
179169simprd 112 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑁) ∈ 𝑉)
180 oveq1 5622 . . . . . . . . . . . . . . . . 17 (𝑦 = ((𝐹𝑧) mod 𝑁) → (𝑦 gcd 𝑁) = (((𝐹𝑧) mod 𝑁) gcd 𝑁))
181180eqeq1d 2093 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝐹𝑧) mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1))
182181, 106elrab2 2765 . . . . . . . . . . . . . . 15 (((𝐹𝑧) mod 𝑁) ∈ 𝑉 ↔ (((𝐹𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1))
183179, 182sylib 120 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1))
184183simprd 112 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1)
185178, 184eqtr3d 2119 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) gcd 𝑁) = 1)
18614nnzd 8803 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℤ)
187186adantr 270 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℤ)
18820nnzd 8803 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
189188adantr 270 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℤ)
190 rpmul 10986 . . . . . . . . . . . . 13 (((𝐹𝑧) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((((𝐹𝑧) gcd 𝑀) = 1 ∧ ((𝐹𝑧) gcd 𝑁) = 1) → ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
191143, 187, 189, 190syl3anc 1172 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((((𝐹𝑧) gcd 𝑀) = 1 ∧ ((𝐹𝑧) gcd 𝑁) = 1) → ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
192176, 185, 191mp2and 424 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1)
193 oveq1 5622 . . . . . . . . . . . . 13 (𝑦 = (𝐹𝑧) → (𝑦 gcd (𝑀 · 𝑁)) = ((𝐹𝑧) gcd (𝑀 · 𝑁)))
194193eqeq1d 2093 . . . . . . . . . . . 12 (𝑦 = (𝐹𝑧) → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
195194, 3elrab2 2765 . . . . . . . . . . 11 ((𝐹𝑧) ∈ 𝑊 ↔ ((𝐹𝑧) ∈ 𝑆 ∧ ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
196140, 192, 195sylanbrc 408 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ 𝑊)
197 funfvima2 5490 . . . . . . . . . . . 12 ((Fun 𝐹𝑊 ⊆ dom 𝐹) → ((𝐹𝑧) ∈ 𝑊 → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊)))
198117, 122, 197syl2anc 403 . . . . . . . . . . 11 (𝜑 → ((𝐹𝑧) ∈ 𝑊 → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊)))
199198imp 122 . . . . . . . . . 10 ((𝜑 ∧ (𝐹𝑧) ∈ 𝑊) → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊))
200196, 199syldan 276 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊))
201135, 200eqeltrrd 2162 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝐹𝑊))
202201ex 113 . . . . . . 7 (𝜑 → (𝑧 ∈ (𝑈 × 𝑉) → 𝑧 ∈ (𝐹𝑊)))
203202ssrdv 3020 . . . . . 6 (𝜑 → (𝑈 × 𝑉) ⊆ (𝐹𝑊))
204125, 203eqssd 3031 . . . . 5 (𝜑 → (𝐹𝑊) = (𝑈 × 𝑉))
205 f1of1 5217 . . . . . . 7 (𝐹:𝑆1-1-onto𝑇𝐹:𝑆1-1𝑇)
206114, 205syl 14 . . . . . 6 (𝜑𝐹:𝑆1-1𝑇)
207119a1i 9 . . . . . 6 (𝜑𝑊𝑆)
208 0z 8697 . . . . . . . . . 10 0 ∈ ℤ
209186, 188zmulcld 8810 . . . . . . . . . 10 (𝜑 → (𝑀 · 𝑁) ∈ ℤ)
210 fzofig 9770 . . . . . . . . . 10 ((0 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (0..^(𝑀 · 𝑁)) ∈ Fin)
211208, 209, 210sylancr 405 . . . . . . . . 9 (𝜑 → (0..^(𝑀 · 𝑁)) ∈ Fin)
2128, 211syl5eqel 2171 . . . . . . . 8 (𝜑𝑆 ∈ Fin)
213 elfzoelz 9489 . . . . . . . . . . . . . 14 (𝑦 ∈ (0..^(𝑀 · 𝑁)) → 𝑦 ∈ ℤ)
214213, 8eleq2s 2179 . . . . . . . . . . . . 13 (𝑦𝑆𝑦 ∈ ℤ)
215214adantl 271 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → 𝑦 ∈ ℤ)
216209adantr 270 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → (𝑀 · 𝑁) ∈ ℤ)
217215, 216gcdcld 10866 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → (𝑦 gcd (𝑀 · 𝑁)) ∈ ℕ0)
218217nn0zd 8802 . . . . . . . . . 10 ((𝜑𝑦𝑆) → (𝑦 gcd (𝑀 · 𝑁)) ∈ ℤ)
219 1zzd 8713 . . . . . . . . . 10 ((𝜑𝑦𝑆) → 1 ∈ ℤ)
220 zdceq 8758 . . . . . . . . . 10 (((𝑦 gcd (𝑀 · 𝑁)) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝑦 gcd (𝑀 · 𝑁)) = 1)
221218, 219, 220syl2anc 403 . . . . . . . . 9 ((𝜑𝑦𝑆) → DECID (𝑦 gcd (𝑀 · 𝑁)) = 1)
222221ralrimiva 2442 . . . . . . . 8 (𝜑 → ∀𝑦𝑆 DECID (𝑦 gcd (𝑀 · 𝑁)) = 1)
223212, 222ssfirab 6596 . . . . . . 7 (𝜑 → {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} ∈ Fin)
2243, 223syl5eqel 2171 . . . . . 6 (𝜑𝑊 ∈ Fin)
225 f1imaeng 6463 . . . . . 6 ((𝐹:𝑆1-1𝑇𝑊𝑆𝑊 ∈ Fin) → (𝐹𝑊) ≈ 𝑊)
226206, 207, 224, 225syl3anc 1172 . . . . 5 (𝜑 → (𝐹𝑊) ≈ 𝑊)
227204, 226eqbrtrrd 3844 . . . 4 (𝜑 → (𝑈 × 𝑉) ≈ 𝑊)
228 fzofig 9770 . . . . . . . . 9 ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0..^𝑀) ∈ Fin)
229208, 186, 228sylancr 405 . . . . . . . 8 (𝜑 → (0..^𝑀) ∈ Fin)
230 elfzoelz 9489 . . . . . . . . . . . . 13 (𝑦 ∈ (0..^𝑀) → 𝑦 ∈ ℤ)
231230adantl 271 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑀)) → 𝑦 ∈ ℤ)
232186adantr 270 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑀)) → 𝑀 ∈ ℤ)
233231, 232gcdcld 10866 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (0..^𝑀)) → (𝑦 gcd 𝑀) ∈ ℕ0)
234233nn0zd 8802 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0..^𝑀)) → (𝑦 gcd 𝑀) ∈ ℤ)
235 1z 8712 . . . . . . . . . 10 1 ∈ ℤ
236 zdceq 8758 . . . . . . . . . 10 (((𝑦 gcd 𝑀) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝑦 gcd 𝑀) = 1)
237234, 235, 236sylancl 404 . . . . . . . . 9 ((𝜑𝑦 ∈ (0..^𝑀)) → DECID (𝑦 gcd 𝑀) = 1)
238237ralrimiva 2442 . . . . . . . 8 (𝜑 → ∀𝑦 ∈ (0..^𝑀)DECID (𝑦 gcd 𝑀) = 1)
239229, 238ssfirab 6596 . . . . . . 7 (𝜑 → {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ∈ Fin)
24073, 239syl5eqel 2171 . . . . . 6 (𝜑𝑈 ∈ Fin)
241 fzofig 9770 . . . . . . . . 9 ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0..^𝑁) ∈ Fin)
242208, 188, 241sylancr 405 . . . . . . . 8 (𝜑 → (0..^𝑁) ∈ Fin)
243 elfzoelz 9489 . . . . . . . . . . . . 13 (𝑦 ∈ (0..^𝑁) → 𝑦 ∈ ℤ)
244243adantl 271 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑁)) → 𝑦 ∈ ℤ)
245188adantr 270 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑁)) → 𝑁 ∈ ℤ)
246244, 245gcdcld 10866 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (0..^𝑁)) → (𝑦 gcd 𝑁) ∈ ℕ0)
247246nn0zd 8802 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0..^𝑁)) → (𝑦 gcd 𝑁) ∈ ℤ)
248 1zzd 8713 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0..^𝑁)) → 1 ∈ ℤ)
249 zdceq 8758 . . . . . . . . . 10 (((𝑦 gcd 𝑁) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝑦 gcd 𝑁) = 1)
250247, 248, 249syl2anc 403 . . . . . . . . 9 ((𝜑𝑦 ∈ (0..^𝑁)) → DECID (𝑦 gcd 𝑁) = 1)
251250ralrimiva 2442 . . . . . . . 8 (𝜑 → ∀𝑦 ∈ (0..^𝑁)DECID (𝑦 gcd 𝑁) = 1)
252242, 251ssfirab 6596 . . . . . . 7 (𝜑 → {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ∈ Fin)
253106, 252syl5eqel 2171 . . . . . 6 (𝜑𝑉 ∈ Fin)
254 xpfi 6593 . . . . . 6 ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) → (𝑈 × 𝑉) ∈ Fin)
255240, 253, 254syl2anc 403 . . . . 5 (𝜑 → (𝑈 × 𝑉) ∈ Fin)
256 hashen 10092 . . . . 5 (((𝑈 × 𝑉) ∈ Fin ∧ 𝑊 ∈ Fin) → ((♯‘(𝑈 × 𝑉)) = (♯‘𝑊) ↔ (𝑈 × 𝑉) ≈ 𝑊))
257255, 224, 256syl2anc 403 . . . 4 (𝜑 → ((♯‘(𝑈 × 𝑉)) = (♯‘𝑊) ↔ (𝑈 × 𝑉) ≈ 𝑊))
258227, 257mpbird 165 . . 3 (𝜑 → (♯‘(𝑈 × 𝑉)) = (♯‘𝑊))
259 hashxp 10134 . . . 4 ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) → (♯‘(𝑈 × 𝑉)) = ((♯‘𝑈) · (♯‘𝑉)))
260240, 253, 259syl2anc 403 . . 3 (𝜑 → (♯‘(𝑈 × 𝑉)) = ((♯‘𝑈) · (♯‘𝑉)))
261258, 260eqtr3d 2119 . 2 (𝜑 → (♯‘𝑊) = ((♯‘𝑈) · (♯‘𝑉)))
26214, 20nnmulcld 8408 . . 3 (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
263 dfphi2 11102 . . . 4 ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (♯‘{𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}))
2648rabeqi 2608 . . . . . 6 {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
2653, 264eqtri 2105 . . . . 5 𝑊 = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
266265fveq2i 5273 . . . 4 (♯‘𝑊) = (♯‘{𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1})
267263, 266syl6eqr 2135 . . 3 ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (♯‘𝑊))
268262, 267syl 14 . 2 (𝜑 → (ϕ‘(𝑀 · 𝑁)) = (♯‘𝑊))
269 dfphi2 11102 . . . . 5 (𝑀 ∈ ℕ → (ϕ‘𝑀) = (♯‘{𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}))
27073fveq2i 5273 . . . . 5 (♯‘𝑈) = (♯‘{𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1})
271269, 270syl6eqr 2135 . . . 4 (𝑀 ∈ ℕ → (ϕ‘𝑀) = (♯‘𝑈))
27214, 271syl 14 . . 3 (𝜑 → (ϕ‘𝑀) = (♯‘𝑈))
273 dfphi2 11102 . . . . 5 (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘{𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}))
274106fveq2i 5273 . . . . 5 (♯‘𝑉) = (♯‘{𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1})
275273, 274syl6eqr 2135 . . . 4 (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘𝑉))
27620, 275syl 14 . . 3 (𝜑 → (ϕ‘𝑁) = (♯‘𝑉))
277272, 276oveq12d 5633 . 2 (𝜑 → ((ϕ‘𝑀) · (ϕ‘𝑁)) = ((♯‘𝑈) · (♯‘𝑉)))
278261, 268, 2773eqtr4d 2127 1 (𝜑 → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  DECID wdc 778  w3a 922   = wceq 1287  wcel 1436  wne 2251  wral 2355  {crab 2359  Vcvv 2615  wss 2988  cop 3434   class class class wbr 3822  cmpt 3876   × cxp 4411  ccnv 4412  dom cdm 4413  cima 4416  Fun wfun 4977   Fn wfn 4978  wf 4979  1-1wf1 4980  1-1-ontowf1o 4982  cfv 4983  (class class class)co 5615  cen 6409  Fincfn 6411  0cc0 7297  1c1 7298   · cmul 7302  cle 7470  cn 8360  cz 8686  cq 9039  ..^cfzo 9484   mod cmo 9660  chash 10083  cdvds 10702   gcd cgcd 10844  ϕcphi 11092
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-coll 3931  ax-sep 3934  ax-nul 3942  ax-pow 3986  ax-pr 4012  ax-un 4236  ax-setind 4328  ax-iinf 4378  ax-cnex 7383  ax-resscn 7384  ax-1cn 7385  ax-1re 7386  ax-icn 7387  ax-addcl 7388  ax-addrcl 7389  ax-mulcl 7390  ax-mulrcl 7391  ax-addcom 7392  ax-mulcom 7393  ax-addass 7394  ax-mulass 7395  ax-distr 7396  ax-i2m1 7397  ax-0lt1 7398  ax-1rid 7399  ax-0id 7400  ax-rnegex 7401  ax-precex 7402  ax-cnre 7403  ax-pre-ltirr 7404  ax-pre-ltwlin 7405  ax-pre-lttrn 7406  ax-pre-apti 7407  ax-pre-ltadd 7408  ax-pre-mulgt0 7409  ax-pre-mulext 7410  ax-arch 7411  ax-caucvg 7412
This theorem depends on definitions:  df-bi 115  df-dc 779  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-nel 2347  df-ral 2360  df-rex 2361  df-reu 2362  df-rmo 2363  df-rab 2364  df-v 2617  df-sbc 2830  df-csb 2923  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-nul 3276  df-if 3380  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-int 3674  df-iun 3717  df-br 3823  df-opab 3877  df-mpt 3878  df-tr 3914  df-id 4096  df-po 4099  df-iso 4100  df-iord 4169  df-on 4171  df-ilim 4172  df-suc 4174  df-iom 4381  df-xp 4419  df-rel 4420  df-cnv 4421  df-co 4422  df-dm 4423  df-rn 4424  df-res 4425  df-ima 4426  df-iota 4948  df-fun 4985  df-fn 4986  df-f 4987  df-f1 4988  df-fo 4989  df-f1o 4990  df-fv 4991  df-riota 5571  df-ov 5618  df-oprab 5619  df-mpt2 5620  df-1st 5870  df-2nd 5871  df-recs 6026  df-irdg 6091  df-frec 6112  df-1o 6137  df-oadd 6141  df-er 6246  df-en 6412  df-dom 6413  df-fin 6414  df-sup 6626  df-pnf 7471  df-mnf 7472  df-xr 7473  df-ltxr 7474  df-le 7475  df-sub 7602  df-neg 7603  df-reap 7996  df-ap 8003  df-div 8082  df-inn 8361  df-2 8419  df-3 8420  df-4 8421  df-n0 8610  df-z 8687  df-uz 8955  df-q 9040  df-rp 9070  df-fz 9360  df-fzo 9485  df-fl 9608  df-mod 9661  df-iseq 9783  df-iexp 9857  df-ihash 10084  df-cj 10175  df-re 10176  df-im 10177  df-rsqrt 10330  df-abs 10331  df-dvds 10703  df-gcd 10845  df-phi 11093
This theorem is referenced by:  phimul  11108
  Copyright terms: Public domain W3C validator