phimullem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > phimullem		Structured version Visualization version GIF version

Theorem phimullem 16313

Description: Lemma for phimul 16314. (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.

Step	Hyp	Ref	Expression
1		oveq1 7209	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (𝑦 gcd (𝑀 · 𝑁)) = (𝑤 gcd (𝑀 · 𝑁)))
2	1	eqeq1d 2736	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ (𝑤 gcd (𝑀 · 𝑁)) = 1))
3		phimul.6	. . . . . . . . . . . . 13 ⊢ 𝑊 = {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
4	2, 3	elrab2 3598	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ 𝑊 ↔ (𝑤 ∈ 𝑆 ∧ (𝑤 gcd (𝑀 · 𝑁)) = 1))
5	4	simplbi 501	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝑊 → 𝑤 ∈ 𝑆)
6		oveq1 7209	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → (𝑥 mod 𝑀) = (𝑤 mod 𝑀))
7		oveq1 7209	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → (𝑥 mod 𝑁) = (𝑤 mod 𝑁))
8	6, 7	opeq12d 4782	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩ = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
9		crth.3	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩)
10		opex 5337	. . . . . . . . . . . 12 ⊢ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ V
11	8, 9, 10	fvmpt 6807	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝑆 → (𝐹‘𝑤) = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
12	5, 11	syl 17	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑊 → (𝐹‘𝑤) = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
13	12	adantl 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝐹‘𝑤) = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
14		crth.1	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = (0..^(𝑀 · 𝑁))
15	5, 14	eleqtrdi 2844	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ 𝑊 → 𝑤 ∈ (0..^(𝑀 · 𝑁)))
16	15	adantl 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑤 ∈ (0..^(𝑀 · 𝑁)))
17		elfzoelz 13226	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ (0..^(𝑀 · 𝑁)) → 𝑤 ∈ ℤ)
18	16, 17	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑤 ∈ ℤ)
19		crth.4	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1))
20	19	simp1d 1144	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
21	20	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑀 ∈ ℕ)
22		zmodfzo 13450	. . . . . . . . . . . 12 ⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑤 mod 𝑀) ∈ (0..^𝑀))
23	18, 21, 22	syl2anc 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑀) ∈ (0..^𝑀))
24		modgcd 16073	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀))
25	18, 21, 24	syl2anc 587	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀))
26	21	nnzd 12264	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑀 ∈ ℤ)
27		gcddvds 16043	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
28	18, 26, 27	syl2anc 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
29	28	simpld 498	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∥ 𝑤)
30		nnne0 11847	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℕ → 𝑀 ≠ 0)
31		simpr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
32	31	necon3ai 2960	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
33	21, 30, 32	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
34		gcdn0cl 16042	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑀 = 0)) → (𝑤 gcd 𝑀) ∈ ℕ)
35	18, 26, 33, 34	syl21anc 838	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∈ ℕ)
36	35	nnzd 12264	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∈ ℤ)
37	19	simp2d 1145	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℕ)
38	37	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑁 ∈ ℕ)
39	38	nnzd 12264	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑁 ∈ ℤ)
40	28	simprd 499	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∥ 𝑀)
41	36, 26, 39, 40	dvdsmultr1d 15839	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁))
42	21, 38	nnmulcld 11866	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑀 · 𝑁) ∈ ℕ)
43	42	nnzd 12264	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑀 · 𝑁) ∈ ℤ)
44		nnne0 11847	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 · 𝑁) ∈ ℕ → (𝑀 · 𝑁) ≠ 0)
45		simpr 488	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 = 0 ∧ (𝑀 · 𝑁) = 0) → (𝑀 · 𝑁) = 0)
46	45	necon3ai 2960	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 · 𝑁) ≠ 0 → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0))
47	42, 44, 46	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0))
48		dvdslegcd 16044	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑤 gcd 𝑀) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) → (((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁))))
49	36, 18, 43, 47, 48	syl31anc 1375	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁))))
50	29, 41, 49	mp2and 699	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁)))
51	4	simprbi 500	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ 𝑊 → (𝑤 gcd (𝑀 · 𝑁)) = 1)
52	51	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd (𝑀 · 𝑁)) = 1)
53	50, 52	breqtrd 5069	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ≤ 1)
54		nnle1eq1 11843	. . . . . . . . . . . . . 14 ⊢ ((𝑤 gcd 𝑀) ∈ ℕ → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1))
55	35, 54	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1))
56	53, 55	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) = 1)
57	25, 56	eqtrd 2774	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = 1)
58		oveq1 7209	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑤 mod 𝑀) → (𝑦 gcd 𝑀) = ((𝑤 mod 𝑀) gcd 𝑀))
59	58	eqeq1d 2736	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑤 mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ ((𝑤 mod 𝑀) gcd 𝑀) = 1))
60		phimul.4	. . . . . . . . . . . 12 ⊢ 𝑈 = {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}
61	59, 60	elrab2 3598	. . . . . . . . . . 11 ⊢ ((𝑤 mod 𝑀) ∈ 𝑈 ↔ ((𝑤 mod 𝑀) ∈ (0..^𝑀) ∧ ((𝑤 mod 𝑀) gcd 𝑀) = 1))
62	23, 57, 61	sylanbrc 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑀) ∈ 𝑈)
63		zmodfzo 13450	. . . . . . . . . . . 12 ⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑤 mod 𝑁) ∈ (0..^𝑁))
64	18, 38, 63	syl2anc 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑁) ∈ (0..^𝑁))
65		modgcd 16073	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁))
66	18, 38, 65	syl2anc 587	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁))
67		gcddvds 16043	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
68	18, 39, 67	syl2anc 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
69	68	simpld 498	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∥ 𝑤)
70		nnne0 11847	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
71		simpr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
72	71	necon3ai 2960	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
73	38, 70, 72	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
74		gcdn0cl 16042	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑁 = 0)) → (𝑤 gcd 𝑁) ∈ ℕ)
75	18, 39, 73, 74	syl21anc 838	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∈ ℕ)
76	75	nnzd 12264	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∈ ℤ)
77	68	simprd 499	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∥ 𝑁)
78		dvdsmul2 15821	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑀 · 𝑁))
79	26, 39, 78	syl2anc 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑁 ∥ (𝑀 · 𝑁))
80	76, 39, 43, 77, 79	dvdstrd 15837	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁))
81		dvdslegcd 16044	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑤 gcd 𝑁) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) → (((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁))))
82	76, 18, 43, 47, 81	syl31anc 1375	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁))))
83	69, 80, 82	mp2and 699	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁)))
84	83, 52	breqtrd 5069	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ≤ 1)
85		nnle1eq1 11843	. . . . . . . . . . . . . 14 ⊢ ((𝑤 gcd 𝑁) ∈ ℕ → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1))
86	75, 85	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1))
87	84, 86	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) = 1)
88	66, 87	eqtrd 2774	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = 1)
89		oveq1 7209	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑤 mod 𝑁) → (𝑦 gcd 𝑁) = ((𝑤 mod 𝑁) gcd 𝑁))
90	89	eqeq1d 2736	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑤 mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝑤 mod 𝑁) gcd 𝑁) = 1))
91		phimul.5	. . . . . . . . . . . 12 ⊢ 𝑉 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}
92	90, 91	elrab2 3598	. . . . . . . . . . 11 ⊢ ((𝑤 mod 𝑁) ∈ 𝑉 ↔ ((𝑤 mod 𝑁) ∈ (0..^𝑁) ∧ ((𝑤 mod 𝑁) gcd 𝑁) = 1))
93	64, 88, 92	sylanbrc 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑁) ∈ 𝑉)
94	62, 93	opelxpd 5578	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
95	13, 94	eqeltrd 2834	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝐹‘𝑤) ∈ (𝑈 × 𝑉))
96	95	ralrimiva 3098	. . . . . . 7 ⊢ (𝜑 → ∀𝑤 ∈ 𝑊 (𝐹‘𝑤) ∈ (𝑈 × 𝑉))
97		crth.2	. . . . . . . . . 10 ⊢ 𝑇 = ((0..^𝑀) × (0..^𝑁))
98	14, 97, 9, 19	crth 16312	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝑆–1-1-onto→𝑇)
99		f1ofn 6651	. . . . . . . . 9 ⊢ (𝐹:𝑆–1-1-onto→𝑇 → 𝐹 Fn 𝑆)
100		fnfun 6468	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑆 → Fun 𝐹)
101	98, 99, 100	3syl 18	. . . . . . . 8 ⊢ (𝜑 → Fun 𝐹)
102	3	ssrab3 3985	. . . . . . . . 9 ⊢ 𝑊 ⊆ 𝑆
103		fndm 6470	. . . . . . . . . 10 ⊢ (𝐹 Fn 𝑆 → dom 𝐹 = 𝑆)
104	98, 99, 103	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐹 = 𝑆)
105	102, 104	sseqtrrid 3944	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ⊆ dom 𝐹)
106		funimass4 6766	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ 𝑊 ⊆ dom 𝐹) → ((𝐹 “ 𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤 ∈ 𝑊 (𝐹‘𝑤) ∈ (𝑈 × 𝑉)))
107	101, 105, 106	syl2anc 587	. . . . . . 7 ⊢ (𝜑 → ((𝐹 “ 𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤 ∈ 𝑊 (𝐹‘𝑤) ∈ (𝑈 × 𝑉)))
108	96, 107	mpbird 260	. . . . . 6 ⊢ (𝜑 → (𝐹 “ 𝑊) ⊆ (𝑈 × 𝑉))
109	60	ssrab3 3985	. . . . . . . . . . 11 ⊢ 𝑈 ⊆ (0..^𝑀)
110	91	ssrab3 3985	. . . . . . . . . . 11 ⊢ 𝑉 ⊆ (0..^𝑁)
111		xpss12 5555	. . . . . . . . . . 11 ⊢ ((𝑈 ⊆ (0..^𝑀) ∧ 𝑉 ⊆ (0..^𝑁)) → (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁)))
112	109, 110, 111	mp2an 692	. . . . . . . . . 10 ⊢ (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁))
113	112, 97	sseqtrri 3928	. . . . . . . . 9 ⊢ (𝑈 × 𝑉) ⊆ 𝑇
114	113	sseli 3887	. . . . . . . 8 ⊢ (𝑧 ∈ (𝑈 × 𝑉) → 𝑧 ∈ 𝑇)
115		f1ocnvfv2 7077	. . . . . . . 8 ⊢ ((𝐹:𝑆–1-1-onto→𝑇 ∧ 𝑧 ∈ 𝑇) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
116	98, 114, 115	syl2an 599	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
117		f1ocnv 6662	. . . . . . . . . . 11 ⊢ (𝐹:𝑆–1-1-onto→𝑇 → ^◡𝐹:𝑇–1-1-onto→𝑆)
118		f1of 6650	. . . . . . . . . . 11 ⊢ (^◡𝐹:𝑇–1-1-onto→𝑆 → ^◡𝐹:𝑇⟶𝑆)
119	98, 117, 118	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ^◡𝐹:𝑇⟶𝑆)
120		ffvelrn 6891	. . . . . . . . . 10 ⊢ ((^◡𝐹:𝑇⟶𝑆 ∧ 𝑧 ∈ 𝑇) → (^◡𝐹‘𝑧) ∈ 𝑆)
121	119, 114, 120	syl2an 599	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (^◡𝐹‘𝑧) ∈ 𝑆)
122	121, 14	eleqtrdi 2844	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (^◡𝐹‘𝑧) ∈ (0..^(𝑀 · 𝑁)))
123		elfzoelz 13226	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹‘𝑧) ∈ (0..^(𝑀 · 𝑁)) → (^◡𝐹‘𝑧) ∈ ℤ)
124	122, 123	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (^◡𝐹‘𝑧) ∈ ℤ)
125	20	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℕ)
126		modgcd 16073	. . . . . . . . . . . 12 ⊢ (((^◡𝐹‘𝑧) ∈ ℤ ∧ 𝑀 ∈ ℕ) → (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = ((^◡𝐹‘𝑧) gcd 𝑀))
127	124, 125, 126	syl2anc 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = ((^◡𝐹‘𝑧) gcd 𝑀))
128		oveq1 7209	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (^◡𝐹‘𝑧) → (𝑤 mod 𝑀) = ((^◡𝐹‘𝑧) mod 𝑀))
129		oveq1 7209	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (^◡𝐹‘𝑧) → (𝑤 mod 𝑁) = ((^◡𝐹‘𝑧) mod 𝑁))
130	128, 129	opeq12d 4782	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (^◡𝐹‘𝑧) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ = ⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩)
131	8	cbvmptv 5147	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩) = (𝑤 ∈ 𝑆 ↦ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
132	9, 131	eqtri 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹 = (𝑤 ∈ 𝑆 ↦ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
133		opex 5337	. . . . . . . . . . . . . . . . . . 19 ⊢ ⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩ ∈ V
134	130, 132, 133	fvmpt 6807	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡𝐹‘𝑧) ∈ 𝑆 → (𝐹‘(^◡𝐹‘𝑧)) = ⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩)
135	121, 134	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(^◡𝐹‘𝑧)) = ⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩)
136	116, 135	eqtr3d 2776	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 = ⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩)
137		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝑈 × 𝑉))
138	136, 137	eqeltrrd 2835	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
139		opelxp 5576	. . . . . . . . . . . . . . 15 ⊢ (⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩ ∈ (𝑈 × 𝑉) ↔ (((^◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈 ∧ ((^◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉))
140	138, 139	sylib 221	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈 ∧ ((^◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉))
141	140	simpld 498	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((^◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈)
142		oveq1 7209	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ((^◡𝐹‘𝑧) mod 𝑀) → (𝑦 gcd 𝑀) = (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀))
143	142	eqeq1d 2736	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((^◡𝐹‘𝑧) mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1))
144	143, 60	elrab2 3598	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈 ↔ (((^◡𝐹‘𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1))
145	141, 144	sylib 221	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1))
146	145	simprd 499	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1)
147	127, 146	eqtr3d 2776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((^◡𝐹‘𝑧) gcd 𝑀) = 1)
148	37	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℕ)
149		modgcd 16073	. . . . . . . . . . . 12 ⊢ (((^◡𝐹‘𝑧) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = ((^◡𝐹‘𝑧) gcd 𝑁))
150	124, 148, 149	syl2anc 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = ((^◡𝐹‘𝑧) gcd 𝑁))
151	140	simprd 499	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((^◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉)
152		oveq1 7209	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ((^◡𝐹‘𝑧) mod 𝑁) → (𝑦 gcd 𝑁) = (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁))
153	152	eqeq1d 2736	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((^◡𝐹‘𝑧) mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1))
154	153, 91	elrab2 3598	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉 ↔ (((^◡𝐹‘𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1))
155	151, 154	sylib 221	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1))
156	155	simprd 499	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1)
157	150, 156	eqtr3d 2776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((^◡𝐹‘𝑧) gcd 𝑁) = 1)
158	20	nnzd 12264	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
159	158	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℤ)
160	37	nnzd 12264	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ)
161	160	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℤ)
162		rpmul 16197	. . . . . . . . . . 11 ⊢ (((^◡𝐹‘𝑧) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((((^◡𝐹‘𝑧) gcd 𝑀) = 1 ∧ ((^◡𝐹‘𝑧) gcd 𝑁) = 1) → ((^◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1))
163	124, 159, 161, 162	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((((^◡𝐹‘𝑧) gcd 𝑀) = 1 ∧ ((^◡𝐹‘𝑧) gcd 𝑁) = 1) → ((^◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1))
164	147, 157, 163	mp2and 699	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((^◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1)
165		oveq1 7209	. . . . . . . . . . 11 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (𝑦 gcd (𝑀 · 𝑁)) = ((^◡𝐹‘𝑧) gcd (𝑀 · 𝑁)))
166	165	eqeq1d 2736	. . . . . . . . . 10 ⊢ (𝑦 = (^◡𝐹‘𝑧) → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ ((^◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1))
167	166, 3	elrab2 3598	. . . . . . . . 9 ⊢ ((^◡𝐹‘𝑧) ∈ 𝑊 ↔ ((^◡𝐹‘𝑧) ∈ 𝑆 ∧ ((^◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1))
168	121, 164, 167	sylanbrc 586	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (^◡𝐹‘𝑧) ∈ 𝑊)
169		funfvima2 7036	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ 𝑊 ⊆ dom 𝐹) → ((^◡𝐹‘𝑧) ∈ 𝑊 → (𝐹‘(^◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊)))
170	101, 105, 169	syl2anc 587	. . . . . . . . 9 ⊢ (𝜑 → ((^◡𝐹‘𝑧) ∈ 𝑊 → (𝐹‘(^◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊)))
171	170	imp 410	. . . . . . . 8 ⊢ ((𝜑 ∧ (^◡𝐹‘𝑧) ∈ 𝑊) → (𝐹‘(^◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊))
172	168, 171	syldan 594	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(^◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊))
173	116, 172	eqeltrrd 2835	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝐹 “ 𝑊))
174	108, 173	eqelssd 3912	. . . . 5 ⊢ (𝜑 → (𝐹 “ 𝑊) = (𝑈 × 𝑉))
175		f1of1 6649	. . . . . . 7 ⊢ (𝐹:𝑆–1-1-onto→𝑇 → 𝐹:𝑆–1-1→𝑇)
176	98, 175	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹:𝑆–1-1→𝑇)
177		fzofi 13530	. . . . . . . . . 10 ⊢ (0..^(𝑀 · 𝑁)) ∈ Fin
178	14, 177	eqeltri 2830	. . . . . . . . 9 ⊢ 𝑆 ∈ Fin
179		ssfi 8840	. . . . . . . . 9 ⊢ ((𝑆 ∈ Fin ∧ 𝑊 ⊆ 𝑆) → 𝑊 ∈ Fin)
180	178, 102, 179	mp2an 692	. . . . . . . 8 ⊢ 𝑊 ∈ Fin
181	180	elexi 3420	. . . . . . 7 ⊢ 𝑊 ∈ V
182	181	f1imaen 8679	. . . . . 6 ⊢ ((𝐹:𝑆–1-1→𝑇 ∧ 𝑊 ⊆ 𝑆) → (𝐹 “ 𝑊) ≈ 𝑊)
183	176, 102, 182	sylancl 589	. . . . 5 ⊢ (𝜑 → (𝐹 “ 𝑊) ≈ 𝑊)
184	174, 183	eqbrtrrd 5067	. . . 4 ⊢ (𝜑 → (𝑈 × 𝑉) ≈ 𝑊)
185		fzofi 13530	. . . . . . . 8 ⊢ (0..^𝑀) ∈ Fin
186		ssrab2 3983	. . . . . . . 8 ⊢ {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ⊆ (0..^𝑀)
187		ssfi 8840	. . . . . . . 8 ⊢ (((0..^𝑀) ∈ Fin ∧ {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ⊆ (0..^𝑀)) → {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ∈ Fin)
188	185, 186, 187	mp2an 692	. . . . . . 7 ⊢ {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ∈ Fin
189	60, 188	eqeltri 2830	. . . . . 6 ⊢ 𝑈 ∈ Fin
190		fzofi 13530	. . . . . . . 8 ⊢ (0..^𝑁) ∈ Fin
191		ssrab2 3983	. . . . . . . 8 ⊢ {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁)
192		ssfi 8840	. . . . . . . 8 ⊢ (((0..^𝑁) ∈ Fin ∧ {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁)) → {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ∈ Fin)
193	190, 191, 192	mp2an 692	. . . . . . 7 ⊢ {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ∈ Fin
194	91, 193	eqeltri 2830	. . . . . 6 ⊢ 𝑉 ∈ Fin
195		xpfi 8931	. . . . . 6 ⊢ ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) → (𝑈 × 𝑉) ∈ Fin)
196	189, 194, 195	mp2an 692	. . . . 5 ⊢ (𝑈 × 𝑉) ∈ Fin
197		hashen 13896	. . . . 5 ⊢ (((𝑈 × 𝑉) ∈ Fin ∧ 𝑊 ∈ Fin) → ((♯‘(𝑈 × 𝑉)) = (♯‘𝑊) ↔ (𝑈 × 𝑉) ≈ 𝑊))
198	196, 180, 197	mp2an 692	. . . 4 ⊢ ((♯‘(𝑈 × 𝑉)) = (♯‘𝑊) ↔ (𝑈 × 𝑉) ≈ 𝑊)
199	184, 198	sylibr 237	. . 3 ⊢ (𝜑 → (♯‘(𝑈 × 𝑉)) = (♯‘𝑊))
200		hashxp 13984	. . . 4 ⊢ ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) → (♯‘(𝑈 × 𝑉)) = ((♯‘𝑈) · (♯‘𝑉)))
201	189, 194, 200	mp2an 692	. . 3 ⊢ (♯‘(𝑈 × 𝑉)) = ((♯‘𝑈) · (♯‘𝑉))
202	199, 201	eqtr3di 2789	. 2 ⊢ (𝜑 → (♯‘𝑊) = ((♯‘𝑈) · (♯‘𝑉)))
203	20, 37	nnmulcld 11866	. . 3 ⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
204		dfphi2 16308	. . . 4 ⊢ ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (♯‘{𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}))
205	14	rabeqi 3385	. . . . . 6 ⊢ {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
206	3, 205	eqtri 2762	. . . . 5 ⊢ 𝑊 = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
207	206	fveq2i 6709	. . . 4 ⊢ (♯‘𝑊) = (♯‘{𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1})
208	204, 207	eqtr4di 2792	. . 3 ⊢ ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (♯‘𝑊))
209	203, 208	syl 17	. 2 ⊢ (𝜑 → (ϕ‘(𝑀 · 𝑁)) = (♯‘𝑊))
210		dfphi2 16308	. . . . 5 ⊢ (𝑀 ∈ ℕ → (ϕ‘𝑀) = (♯‘{𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}))
211	60	fveq2i 6709	. . . . 5 ⊢ (♯‘𝑈) = (♯‘{𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1})
212	210, 211	eqtr4di 2792	. . . 4 ⊢ (𝑀 ∈ ℕ → (ϕ‘𝑀) = (♯‘𝑈))
213	20, 212	syl 17	. . 3 ⊢ (𝜑 → (ϕ‘𝑀) = (♯‘𝑈))
214		dfphi2 16308	. . . . 5 ⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘{𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}))
215	91	fveq2i 6709	. . . . 5 ⊢ (♯‘𝑉) = (♯‘{𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1})
216	214, 215	eqtr4di 2792	. . . 4 ⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘𝑉))
217	37, 216	syl 17	. . 3 ⊢ (𝜑 → (ϕ‘𝑁) = (♯‘𝑉))
218	213, 217	oveq12d 7220	. 2 ⊢ (𝜑 → ((ϕ‘𝑀) · (ϕ‘𝑁)) = ((♯‘𝑈) · (♯‘𝑉)))
219	202, 209, 218	3eqtr4d 2784	1 ⊢ (𝜑 → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1089 = wceq 1543 ∈ wcel 2110 ≠ wne 2935 ∀wral 3054 {crab 3058 ⊆ wss 3857 ⟨cop 4537 class class class wbr 5043 ↦ cmpt 5124 × cxp 5538 ^◡ccnv 5539 dom cdm 5540 “ cima 5543 Fun wfun 6363 Fn wfn 6364 ⟶wf 6365 –1-1→wf1 6366 –1-1-onto→wf1o 6368 ‘cfv 6369 (class class class)co 7202 ≈ cen 8612 Fincfn 8615 0cc0 10712 1c1 10713 · cmul 10717 ≤ cle 10851 ℕcn 11813 ℤcz 12159 ..^cfzo 13221 mod cmo 13425 ♯chash 13879 ∥ cdvds 15796 gcd cgcd 16034 ϕcphi 16298

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2706 ax-rep 5168 ax-sep 5181 ax-nul 5188 ax-pow 5247 ax-pr 5311 ax-un 7512 ax-cnex 10768 ax-resscn 10769 ax-1cn 10770 ax-icn 10771 ax-addcl 10772 ax-addrcl 10773 ax-mulcl 10774 ax-mulrcl 10775 ax-mulcom 10776 ax-addass 10777 ax-mulass 10778 ax-distr 10779 ax-i2m1 10780 ax-1ne0 10781 ax-1rid 10782 ax-rnegex 10783 ax-rrecex 10784 ax-cnre 10785 ax-pre-lttri 10786 ax-pre-lttrn 10787 ax-pre-ltadd 10788 ax-pre-mulgt0 10789 ax-pre-sup 10790

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2726 df-clel 2812 df-nfc 2882 df-ne 2936 df-nel 3040 df-ral 3059 df-rex 3060 df-reu 3061 df-rmo 3062 df-rab 3063 df-v 3403 df-sbc 3688 df-csb 3803 df-dif 3860 df-un 3862 df-in 3864 df-ss 3874 df-pss 3876 df-nul 4228 df-if 4430 df-pw 4505 df-sn 4532 df-pr 4534 df-tp 4536 df-op 4538 df-uni 4810 df-int 4850 df-iun 4896 df-br 5044 df-opab 5106 df-mpt 5125 df-tr 5151 df-id 5444 df-eprel 5449 df-po 5457 df-so 5458 df-fr 5498 df-we 5500 df-xp 5546 df-rel 5547 df-cnv 5548 df-co 5549 df-dm 5550 df-rn 5551 df-res 5552 df-ima 5553 df-pred 6149 df-ord 6205 df-on 6206 df-lim 6207 df-suc 6208 df-iota 6327 df-fun 6371 df-fn 6372 df-f 6373 df-f1 6374 df-fo 6375 df-f1o 6376 df-fv 6377 df-riota 7159 df-ov 7205 df-oprab 7206 df-mpo 7207 df-om 7634 df-1st 7750 df-2nd 7751 df-wrecs 8036 df-recs 8097 df-rdg 8135 df-1o 8191 df-oadd 8195 df-er 8380 df-map 8499 df-en 8616 df-dom 8617 df-sdom 8618 df-fin 8619 df-sup 9047 df-inf 9048 df-dju 9500 df-card 9538 df-pnf 10852 df-mnf 10853 df-xr 10854 df-ltxr 10855 df-le 10856 df-sub 11047 df-neg 11048 df-div 11473 df-nn 11814 df-2 11876 df-3 11877 df-n0 12074 df-xnn0 12146 df-z 12160 df-uz 12422 df-rp 12570 df-fz 13079 df-fzo 13222 df-fl 13350 df-mod 13426 df-seq 13558 df-exp 13619 df-hash 13880 df-cj 14645 df-re 14646 df-im 14647 df-sqrt 14781 df-abs 14782 df-dvds 15797 df-gcd 16035 df-phi 16300

This theorem is referenced by: phimul 16314

W3C validator