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 16816

Description: Lemma for phimul 16817. (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 7438	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (𝑦 gcd (𝑀 · 𝑁)) = (𝑤 gcd (𝑀 · 𝑁)))
2	1	eqeq1d 2739	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ (𝑤 gcd (𝑀 · 𝑁)) = 1))
3		phimul.6	. . . . . . . . . . . . 13 ⊢ 𝑊 = {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
4	2, 3	elrab2 3695	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ 𝑊 ↔ (𝑤 ∈ 𝑆 ∧ (𝑤 gcd (𝑀 · 𝑁)) = 1))
5	4	simplbi 497	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝑊 → 𝑤 ∈ 𝑆)
6		oveq1 7438	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → (𝑥 mod 𝑀) = (𝑤 mod 𝑀))
7		oveq1 7438	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → (𝑥 mod 𝑁) = (𝑤 mod 𝑁))
8	6, 7	opeq12d 4881	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩ = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
9		crth.3	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩)
10		opex 5469	. . . . . . . . . . . 12 ⊢ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ V
11	8, 9, 10	fvmpt 7016	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝑆 → (𝐹‘𝑤) = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
12	5, 11	syl 17	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑊 → (𝐹‘𝑤) = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
13	12	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝐹‘𝑤) = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
14		crth.1	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = (0..^(𝑀 · 𝑁))
15	5, 14	eleqtrdi 2851	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ 𝑊 → 𝑤 ∈ (0..^(𝑀 · 𝑁)))
16	15	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑤 ∈ (0..^(𝑀 · 𝑁)))
17		elfzoelz 13699	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ (0..^(𝑀 · 𝑁)) → 𝑤 ∈ ℤ)
18	16, 17	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑤 ∈ ℤ)
19		crth.4	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1))
20	19	simp1d 1143	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
21	20	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑀 ∈ ℕ)
22		zmodfzo 13934	. . . . . . . . . . . 12 ⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑤 mod 𝑀) ∈ (0..^𝑀))
23	18, 21, 22	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑀) ∈ (0..^𝑀))
24		modgcd 16569	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀))
25	18, 21, 24	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀))
26	21	nnzd 12640	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑀 ∈ ℤ)
27		gcddvds 16540	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
28	18, 26, 27	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
29	28	simpld 494	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∥ 𝑤)
30		nnne0 12300	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℕ → 𝑀 ≠ 0)
31		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
32	31	necon3ai 2965	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
33	21, 30, 32	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
34		gcdn0cl 16539	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑀 = 0)) → (𝑤 gcd 𝑀) ∈ ℕ)
35	18, 26, 33, 34	syl21anc 838	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∈ ℕ)
36	35	nnzd 12640	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∈ ℤ)
37	19	simp2d 1144	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℕ)
38	37	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑁 ∈ ℕ)
39	38	nnzd 12640	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑁 ∈ ℤ)
40	28	simprd 495	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∥ 𝑀)
41	36, 26, 39, 40	dvdsmultr1d 16334	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁))
42	21, 38	nnmulcld 12319	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑀 · 𝑁) ∈ ℕ)
43	42	nnzd 12640	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑀 · 𝑁) ∈ ℤ)
44		nnne0 12300	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 · 𝑁) ∈ ℕ → (𝑀 · 𝑁) ≠ 0)
45		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 = 0 ∧ (𝑀 · 𝑁) = 0) → (𝑀 · 𝑁) = 0)
46	45	necon3ai 2965	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 · 𝑁) ≠ 0 → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0))
47	42, 44, 46	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0))
48		dvdslegcd 16541	. . . . . . . . . . . . . . . 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 496	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ 𝑊 → (𝑤 gcd (𝑀 · 𝑁)) = 1)
52	51	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd (𝑀 · 𝑁)) = 1)
53	50, 52	breqtrd 5169	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ≤ 1)
54		nnle1eq1 12296	. . . . . . . . . . . . . 14 ⊢ ((𝑤 gcd 𝑀) ∈ ℕ → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1))
55	35, 54	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1))
56	53, 55	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) = 1)
57	25, 56	eqtrd 2777	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = 1)
58		oveq1 7438	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑤 mod 𝑀) → (𝑦 gcd 𝑀) = ((𝑤 mod 𝑀) gcd 𝑀))
59	58	eqeq1d 2739	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑤 mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ ((𝑤 mod 𝑀) gcd 𝑀) = 1))
60		phimul.4	. . . . . . . . . . . 12 ⊢ 𝑈 = {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}
61	59, 60	elrab2 3695	. . . . . . . . . . 11 ⊢ ((𝑤 mod 𝑀) ∈ 𝑈 ↔ ((𝑤 mod 𝑀) ∈ (0..^𝑀) ∧ ((𝑤 mod 𝑀) gcd 𝑀) = 1))
62	23, 57, 61	sylanbrc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑀) ∈ 𝑈)
63		zmodfzo 13934	. . . . . . . . . . . 12 ⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑤 mod 𝑁) ∈ (0..^𝑁))
64	18, 38, 63	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑁) ∈ (0..^𝑁))
65		modgcd 16569	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁))
66	18, 38, 65	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁))
67		gcddvds 16540	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
68	18, 39, 67	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
69	68	simpld 494	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∥ 𝑤)
70		nnne0 12300	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
71		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
72	71	necon3ai 2965	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
73	38, 70, 72	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
74		gcdn0cl 16539	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑁 = 0)) → (𝑤 gcd 𝑁) ∈ ℕ)
75	18, 39, 73, 74	syl21anc 838	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∈ ℕ)
76	75	nnzd 12640	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∈ ℤ)
77	68	simprd 495	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∥ 𝑁)
78		dvdsmul2 16316	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑀 · 𝑁))
79	26, 39, 78	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑁 ∥ (𝑀 · 𝑁))
80	76, 39, 43, 77, 79	dvdstrd 16332	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁))
81		dvdslegcd 16541	. . . . . . . . . . . . . . . 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 5169	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ≤ 1)
85		nnle1eq1 12296	. . . . . . . . . . . . . 14 ⊢ ((𝑤 gcd 𝑁) ∈ ℕ → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1))
86	75, 85	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1))
87	84, 86	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) = 1)
88	66, 87	eqtrd 2777	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = 1)
89		oveq1 7438	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑤 mod 𝑁) → (𝑦 gcd 𝑁) = ((𝑤 mod 𝑁) gcd 𝑁))
90	89	eqeq1d 2739	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑤 mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝑤 mod 𝑁) gcd 𝑁) = 1))
91		phimul.5	. . . . . . . . . . . 12 ⊢ 𝑉 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}
92	90, 91	elrab2 3695	. . . . . . . . . . 11 ⊢ ((𝑤 mod 𝑁) ∈ 𝑉 ↔ ((𝑤 mod 𝑁) ∈ (0..^𝑁) ∧ ((𝑤 mod 𝑁) gcd 𝑁) = 1))
93	64, 88, 92	sylanbrc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑁) ∈ 𝑉)
94	62, 93	opelxpd 5724	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
95	13, 94	eqeltrd 2841	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝐹‘𝑤) ∈ (𝑈 × 𝑉))
96	95	ralrimiva 3146	. . . . . . 7 ⊢ (𝜑 → ∀𝑤 ∈ 𝑊 (𝐹‘𝑤) ∈ (𝑈 × 𝑉))
97		crth.2	. . . . . . . . . 10 ⊢ 𝑇 = ((0..^𝑀) × (0..^𝑁))
98	14, 97, 9, 19	crth 16815	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝑆–1-1-onto→𝑇)
99		f1ofn 6849	. . . . . . . . 9 ⊢ (𝐹:𝑆–1-1-onto→𝑇 → 𝐹 Fn 𝑆)
100		fnfun 6668	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑆 → Fun 𝐹)
101	98, 99, 100	3syl 18	. . . . . . . 8 ⊢ (𝜑 → Fun 𝐹)
102	3	ssrab3 4082	. . . . . . . . 9 ⊢ 𝑊 ⊆ 𝑆
103		fndm 6671	. . . . . . . . . 10 ⊢ (𝐹 Fn 𝑆 → dom 𝐹 = 𝑆)
104	98, 99, 103	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐹 = 𝑆)
105	102, 104	sseqtrrid 4027	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ⊆ dom 𝐹)
106		funimass4 6973	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ 𝑊 ⊆ dom 𝐹) → ((𝐹 “ 𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤 ∈ 𝑊 (𝐹‘𝑤) ∈ (𝑈 × 𝑉)))
107	101, 105, 106	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((𝐹 “ 𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤 ∈ 𝑊 (𝐹‘𝑤) ∈ (𝑈 × 𝑉)))
108	96, 107	mpbird 257	. . . . . 6 ⊢ (𝜑 → (𝐹 “ 𝑊) ⊆ (𝑈 × 𝑉))
109	60	ssrab3 4082	. . . . . . . . . . 11 ⊢ 𝑈 ⊆ (0..^𝑀)
110	91	ssrab3 4082	. . . . . . . . . . 11 ⊢ 𝑉 ⊆ (0..^𝑁)
111		xpss12 5700	. . . . . . . . . . 11 ⊢ ((𝑈 ⊆ (0..^𝑀) ∧ 𝑉 ⊆ (0..^𝑁)) → (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁)))
112	109, 110, 111	mp2an 692	. . . . . . . . . 10 ⊢ (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁))
113	112, 97	sseqtrri 4033	. . . . . . . . 9 ⊢ (𝑈 × 𝑉) ⊆ 𝑇
114	113	sseli 3979	. . . . . . . 8 ⊢ (𝑧 ∈ (𝑈 × 𝑉) → 𝑧 ∈ 𝑇)
115		f1ocnvfv2 7297	. . . . . . . 8 ⊢ ((𝐹:𝑆–1-1-onto→𝑇 ∧ 𝑧 ∈ 𝑇) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
116	98, 114, 115	syl2an 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
117		f1ocnv 6860	. . . . . . . . . . 11 ⊢ (𝐹:𝑆–1-1-onto→𝑇 → ^◡𝐹:𝑇–1-1-onto→𝑆)
118		f1of 6848	. . . . . . . . . . 11 ⊢ (^◡𝐹:𝑇–1-1-onto→𝑆 → ^◡𝐹:𝑇⟶𝑆)
119	98, 117, 118	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ^◡𝐹:𝑇⟶𝑆)
120		ffvelcdm 7101	. . . . . . . . . 10 ⊢ ((^◡𝐹:𝑇⟶𝑆 ∧ 𝑧 ∈ 𝑇) → (^◡𝐹‘𝑧) ∈ 𝑆)
121	119, 114, 120	syl2an 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (^◡𝐹‘𝑧) ∈ 𝑆)
122	121, 14	eleqtrdi 2851	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (^◡𝐹‘𝑧) ∈ (0..^(𝑀 · 𝑁)))
123		elfzoelz 13699	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹‘𝑧) ∈ (0..^(𝑀 · 𝑁)) → (^◡𝐹‘𝑧) ∈ ℤ)
124	122, 123	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (^◡𝐹‘𝑧) ∈ ℤ)
125	20	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℕ)
126		modgcd 16569	. . . . . . . . . . . 12 ⊢ (((^◡𝐹‘𝑧) ∈ ℤ ∧ 𝑀 ∈ ℕ) → (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = ((^◡𝐹‘𝑧) gcd 𝑀))
127	124, 125, 126	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = ((^◡𝐹‘𝑧) gcd 𝑀))
128		oveq1 7438	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (^◡𝐹‘𝑧) → (𝑤 mod 𝑀) = ((^◡𝐹‘𝑧) mod 𝑀))
129		oveq1 7438	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (^◡𝐹‘𝑧) → (𝑤 mod 𝑁) = ((^◡𝐹‘𝑧) mod 𝑁))
130	128, 129	opeq12d 4881	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (^◡𝐹‘𝑧) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ = ⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩)
131	8	cbvmptv 5255	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩) = (𝑤 ∈ 𝑆 ↦ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
132	9, 131	eqtri 2765	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹 = (𝑤 ∈ 𝑆 ↦ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
133		opex 5469	. . . . . . . . . . . . . . . . . . 19 ⊢ ⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩ ∈ V
134	130, 132, 133	fvmpt 7016	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡𝐹‘𝑧) ∈ 𝑆 → (𝐹‘(^◡𝐹‘𝑧)) = ⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩)
135	121, 134	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(^◡𝐹‘𝑧)) = ⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩)
136	116, 135	eqtr3d 2779	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 = ⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩)
137		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝑈 × 𝑉))
138	136, 137	eqeltrrd 2842	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
139		opelxp 5721	. . . . . . . . . . . . . . 15 ⊢ (⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩ ∈ (𝑈 × 𝑉) ↔ (((^◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈 ∧ ((^◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉))
140	138, 139	sylib 218	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈 ∧ ((^◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉))
141	140	simpld 494	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((^◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈)
142		oveq1 7438	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ((^◡𝐹‘𝑧) mod 𝑀) → (𝑦 gcd 𝑀) = (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀))
143	142	eqeq1d 2739	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((^◡𝐹‘𝑧) mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1))
144	143, 60	elrab2 3695	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈 ↔ (((^◡𝐹‘𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1))
145	141, 144	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1))
146	145	simprd 495	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1)
147	127, 146	eqtr3d 2779	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((^◡𝐹‘𝑧) gcd 𝑀) = 1)
148	37	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℕ)
149		modgcd 16569	. . . . . . . . . . . 12 ⊢ (((^◡𝐹‘𝑧) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = ((^◡𝐹‘𝑧) gcd 𝑁))
150	124, 148, 149	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = ((^◡𝐹‘𝑧) gcd 𝑁))
151	140	simprd 495	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((^◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉)
152		oveq1 7438	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ((^◡𝐹‘𝑧) mod 𝑁) → (𝑦 gcd 𝑁) = (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁))
153	152	eqeq1d 2739	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((^◡𝐹‘𝑧) mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1))
154	153, 91	elrab2 3695	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉 ↔ (((^◡𝐹‘𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1))
155	151, 154	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1))
156	155	simprd 495	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1)
157	150, 156	eqtr3d 2779	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((^◡𝐹‘𝑧) gcd 𝑁) = 1)
158	20	nnzd 12640	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
159	158	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℤ)
160	37	nnzd 12640	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ)
161	160	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℤ)
162		rpmul 16696	. . . . . . . . . . 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 7438	. . . . . . . . . . 11 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (𝑦 gcd (𝑀 · 𝑁)) = ((^◡𝐹‘𝑧) gcd (𝑀 · 𝑁)))
166	165	eqeq1d 2739	. . . . . . . . . 10 ⊢ (𝑦 = (^◡𝐹‘𝑧) → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ ((^◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1))
167	166, 3	elrab2 3695	. . . . . . . . 9 ⊢ ((^◡𝐹‘𝑧) ∈ 𝑊 ↔ ((^◡𝐹‘𝑧) ∈ 𝑆 ∧ ((^◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1))
168	121, 164, 167	sylanbrc 583	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (^◡𝐹‘𝑧) ∈ 𝑊)
169		funfvima2 7251	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ 𝑊 ⊆ dom 𝐹) → ((^◡𝐹‘𝑧) ∈ 𝑊 → (𝐹‘(^◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊)))
170	101, 105, 169	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ((^◡𝐹‘𝑧) ∈ 𝑊 → (𝐹‘(^◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊)))
171	170	imp 406	. . . . . . . 8 ⊢ ((𝜑 ∧ (^◡𝐹‘𝑧) ∈ 𝑊) → (𝐹‘(^◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊))
172	168, 171	syldan 591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(^◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊))
173	116, 172	eqeltrrd 2842	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝐹 “ 𝑊))
174	108, 173	eqelssd 4005	. . . . 5 ⊢ (𝜑 → (𝐹 “ 𝑊) = (𝑈 × 𝑉))
175		f1of1 6847	. . . . . . 7 ⊢ (𝐹:𝑆–1-1-onto→𝑇 → 𝐹:𝑆–1-1→𝑇)
176	98, 175	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹:𝑆–1-1→𝑇)
177		fzofi 14015	. . . . . . . . . 10 ⊢ (0..^(𝑀 · 𝑁)) ∈ Fin
178	14, 177	eqeltri 2837	. . . . . . . . 9 ⊢ 𝑆 ∈ Fin
179		ssfi 9213	. . . . . . . . 9 ⊢ ((𝑆 ∈ Fin ∧ 𝑊 ⊆ 𝑆) → 𝑊 ∈ Fin)
180	178, 102, 179	mp2an 692	. . . . . . . 8 ⊢ 𝑊 ∈ Fin
181	180	elexi 3503	. . . . . . 7 ⊢ 𝑊 ∈ V
182	181	f1imaen 9057	. . . . . 6 ⊢ ((𝐹:𝑆–1-1→𝑇 ∧ 𝑊 ⊆ 𝑆) → (𝐹 “ 𝑊) ≈ 𝑊)
183	176, 102, 182	sylancl 586	. . . . 5 ⊢ (𝜑 → (𝐹 “ 𝑊) ≈ 𝑊)
184	174, 183	eqbrtrrd 5167	. . . 4 ⊢ (𝜑 → (𝑈 × 𝑉) ≈ 𝑊)
185		fzofi 14015	. . . . . . . 8 ⊢ (0..^𝑀) ∈ Fin
186		ssrab2 4080	. . . . . . . 8 ⊢ {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ⊆ (0..^𝑀)
187		ssfi 9213	. . . . . . . 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 2837	. . . . . 6 ⊢ 𝑈 ∈ Fin
190		fzofi 14015	. . . . . . . 8 ⊢ (0..^𝑁) ∈ Fin
191		ssrab2 4080	. . . . . . . 8 ⊢ {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁)
192		ssfi 9213	. . . . . . . 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 2837	. . . . . 6 ⊢ 𝑉 ∈ Fin
195		xpfi 9358	. . . . . 6 ⊢ ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) → (𝑈 × 𝑉) ∈ Fin)
196	189, 194, 195	mp2an 692	. . . . 5 ⊢ (𝑈 × 𝑉) ∈ Fin
197		hashen 14386	. . . . 5 ⊢ (((𝑈 × 𝑉) ∈ Fin ∧ 𝑊 ∈ Fin) → ((♯‘(𝑈 × 𝑉)) = (♯‘𝑊) ↔ (𝑈 × 𝑉) ≈ 𝑊))
198	196, 180, 197	mp2an 692	. . . 4 ⊢ ((♯‘(𝑈 × 𝑉)) = (♯‘𝑊) ↔ (𝑈 × 𝑉) ≈ 𝑊)
199	184, 198	sylibr 234	. . 3 ⊢ (𝜑 → (♯‘(𝑈 × 𝑉)) = (♯‘𝑊))
200		hashxp 14473	. . . 4 ⊢ ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) → (♯‘(𝑈 × 𝑉)) = ((♯‘𝑈) · (♯‘𝑉)))
201	189, 194, 200	mp2an 692	. . 3 ⊢ (♯‘(𝑈 × 𝑉)) = ((♯‘𝑈) · (♯‘𝑉))
202	199, 201	eqtr3di 2792	. 2 ⊢ (𝜑 → (♯‘𝑊) = ((♯‘𝑈) · (♯‘𝑉)))
203	20, 37	nnmulcld 12319	. . 3 ⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
204		dfphi2 16811	. . . 4 ⊢ ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (♯‘{𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}))
205	14	rabeqi 3450	. . . . . 6 ⊢ {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
206	3, 205	eqtri 2765	. . . . 5 ⊢ 𝑊 = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
207	206	fveq2i 6909	. . . 4 ⊢ (♯‘𝑊) = (♯‘{𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1})
208	204, 207	eqtr4di 2795	. . 3 ⊢ ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (♯‘𝑊))
209	203, 208	syl 17	. 2 ⊢ (𝜑 → (ϕ‘(𝑀 · 𝑁)) = (♯‘𝑊))
210		dfphi2 16811	. . . . 5 ⊢ (𝑀 ∈ ℕ → (ϕ‘𝑀) = (♯‘{𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}))
211	60	fveq2i 6909	. . . . 5 ⊢ (♯‘𝑈) = (♯‘{𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1})
212	210, 211	eqtr4di 2795	. . . 4 ⊢ (𝑀 ∈ ℕ → (ϕ‘𝑀) = (♯‘𝑈))
213	20, 212	syl 17	. . 3 ⊢ (𝜑 → (ϕ‘𝑀) = (♯‘𝑈))
214		dfphi2 16811	. . . . 5 ⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘{𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}))
215	91	fveq2i 6909	. . . . 5 ⊢ (♯‘𝑉) = (♯‘{𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1})
216	214, 215	eqtr4di 2795	. . . 4 ⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘𝑉))
217	37, 216	syl 17	. . 3 ⊢ (𝜑 → (ϕ‘𝑁) = (♯‘𝑉))
218	213, 217	oveq12d 7449	. 2 ⊢ (𝜑 → ((ϕ‘𝑀) · (ϕ‘𝑁)) = ((♯‘𝑈) · (♯‘𝑉)))
219	202, 209, 218	3eqtr4d 2787	1 ⊢ (𝜑 → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 {crab 3436 ⊆ wss 3951 ⟨cop 4632 class class class wbr 5143 ↦ cmpt 5225 × cxp 5683 ^◡ccnv 5684 dom cdm 5685 “ cima 5688 Fun wfun 6555 Fn wfn 6556 ⟶wf 6557 –1-1→wf1 6558 –1-1-onto→wf1o 6560 ‘cfv 6561 (class class class)co 7431 ≈ cen 8982 Fincfn 8985 0cc0 11155 1c1 11156 · cmul 11160 ≤ cle 11296 ℕcn 12266 ℤcz 12613 ..^cfzo 13694 mod cmo 13909 ♯chash 14369 ∥ cdvds 16290 gcd cgcd 16531 ϕcphi 16801

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-oadd 8510 df-er 8745 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-sup 9482 df-inf 9483 df-dju 9941 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-n0 12527 df-xnn0 12600 df-z 12614 df-uz 12879 df-rp 13035 df-fz 13548 df-fzo 13695 df-fl 13832 df-mod 13910 df-seq 14043 df-exp 14103 df-hash 14370 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-dvds 16291 df-gcd 16532 df-phi 16803

This theorem is referenced by: phimul 16817

W3C validator