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 15322

Description: Lemma for phimul 15323. (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		phimul.4	. . . . 5 ⊢ 𝑈 = {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}
2		fzofi 12635	. . . . . 6 ⊢ (0..^𝑀) ∈ Fin
3		ssrab2 3650	. . . . . 6 ⊢ {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ⊆ (0..^𝑀)
4		ssfi 8065	. . . . . 6 ⊢ (((0..^𝑀) ∈ Fin ∧ {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ⊆ (0..^𝑀)) → {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ∈ Fin)
5	2, 3, 4	mp2an 704	. . . . 5 ⊢ {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ∈ Fin
6	1, 5	eqeltri 2684	. . . 4 ⊢ 𝑈 ∈ Fin
7		phimul.5	. . . . 5 ⊢ 𝑉 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}
8		fzofi 12635	. . . . . 6 ⊢ (0..^𝑁) ∈ Fin
9		ssrab2 3650	. . . . . 6 ⊢ {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁)
10		ssfi 8065	. . . . . 6 ⊢ (((0..^𝑁) ∈ Fin ∧ {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁)) → {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ∈ Fin)
11	8, 9, 10	mp2an 704	. . . . 5 ⊢ {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ∈ Fin
12	7, 11	eqeltri 2684	. . . 4 ⊢ 𝑉 ∈ Fin
13		hashxp 13081	. . . 4 ⊢ ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) → (#‘(𝑈 × 𝑉)) = ((#‘𝑈) · (#‘𝑉)))
14	6, 12, 13	mp2an 704	. . 3 ⊢ (#‘(𝑈 × 𝑉)) = ((#‘𝑈) · (#‘𝑉))
15		oveq1 6556	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (𝑦 gcd (𝑀 · 𝑁)) = (𝑤 gcd (𝑀 · 𝑁)))
16	15	eqeq1d 2612	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ (𝑤 gcd (𝑀 · 𝑁)) = 1))
17		phimul.6	. . . . . . . . . . . . 13 ⊢ 𝑊 = {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
18	16, 17	elrab2 3333	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ 𝑊 ↔ (𝑤 ∈ 𝑆 ∧ (𝑤 gcd (𝑀 · 𝑁)) = 1))
19	18	simplbi 475	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝑊 → 𝑤 ∈ 𝑆)
20		oveq1 6556	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → (𝑥 mod 𝑀) = (𝑤 mod 𝑀))
21		oveq1 6556	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → (𝑥 mod 𝑁) = (𝑤 mod 𝑁))
22	20, 21	opeq12d 4348	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩ = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
23		crth.3	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩)
24		opex 4859	. . . . . . . . . . . 12 ⊢ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ V
25	22, 23, 24	fvmpt 6191	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝑆 → (𝐹‘𝑤) = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
26	19, 25	syl 17	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑊 → (𝐹‘𝑤) = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
27	26	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝐹‘𝑤) = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
28		crth.1	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = (0..^(𝑀 · 𝑁))
29	19, 28	syl6eleq 2698	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ 𝑊 → 𝑤 ∈ (0..^(𝑀 · 𝑁)))
30	29	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑤 ∈ (0..^(𝑀 · 𝑁)))
31		elfzoelz 12339	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ (0..^(𝑀 · 𝑁)) → 𝑤 ∈ ℤ)
32	30, 31	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑤 ∈ ℤ)
33		crth.4	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1))
34	33	simp1d 1066	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
35	34	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑀 ∈ ℕ)
36		zmodfzo 12555	. . . . . . . . . . . 12 ⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑤 mod 𝑀) ∈ (0..^𝑀))
37	32, 35, 36	syl2anc 691	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑀) ∈ (0..^𝑀))
38		modgcd 15091	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀))
39	32, 35, 38	syl2anc 691	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀))
40	35	nnzd 11357	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑀 ∈ ℤ)
41		gcddvds 15063	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
42	32, 40, 41	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
43	42	simpld 474	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∥ 𝑤)
44	42	simprd 478	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∥ 𝑀)
45	33	simp2d 1067	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℕ)
46	45	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑁 ∈ ℕ)
47	46	nnzd 11357	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑁 ∈ ℤ)
48		dvdsmul1 14841	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∥ (𝑀 · 𝑁))
49	40, 47, 48	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑀 ∥ (𝑀 · 𝑁))
50		nnne0 10930	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ ℕ → 𝑀 ≠ 0)
51		simpr 476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤 = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
52	51	necon3ai 2807	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
53	35, 50, 52	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
54		gcdn0cl 15062	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑀 = 0)) → (𝑤 gcd 𝑀) ∈ ℕ)
55	32, 40, 53, 54	syl21anc 1317	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∈ ℕ)
56	55	nnzd 11357	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∈ ℤ)
57	35, 46	nnmulcld 10945	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑀 · 𝑁) ∈ ℕ)
58	57	nnzd 11357	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑀 · 𝑁) ∈ ℤ)
59		dvdstr 14856	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑤 gcd 𝑀) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑤 gcd 𝑀) ∥ 𝑀 ∧ 𝑀 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)))
60	56, 40, 58, 59	syl3anc 1318	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (((𝑤 gcd 𝑀) ∥ 𝑀 ∧ 𝑀 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)))
61	44, 49, 60	mp2and 711	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁))
62		nnne0 10930	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 · 𝑁) ∈ ℕ → (𝑀 · 𝑁) ≠ 0)
63		simpr 476	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 = 0 ∧ (𝑀 · 𝑁) = 0) → (𝑀 · 𝑁) = 0)
64	63	necon3ai 2807	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 · 𝑁) ≠ 0 → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0))
65	57, 62, 64	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0))
66		dvdslegcd 15064	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑤 gcd 𝑀) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) → (((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁))))
67	56, 32, 58, 65, 66	syl31anc 1321	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁))))
68	43, 61, 67	mp2and 711	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁)))
69	18	simprbi 479	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ 𝑊 → (𝑤 gcd (𝑀 · 𝑁)) = 1)
70	69	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd (𝑀 · 𝑁)) = 1)
71	68, 70	breqtrd 4609	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) ≤ 1)
72		nnle1eq1 10925	. . . . . . . . . . . . . 14 ⊢ ((𝑤 gcd 𝑀) ∈ ℕ → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1))
73	55, 72	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1))
74	71, 73	mpbid 221	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑀) = 1)
75	39, 74	eqtrd 2644	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = 1)
76		oveq1 6556	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑤 mod 𝑀) → (𝑦 gcd 𝑀) = ((𝑤 mod 𝑀) gcd 𝑀))
77	76	eqeq1d 2612	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑤 mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ ((𝑤 mod 𝑀) gcd 𝑀) = 1))
78	77, 1	elrab2 3333	. . . . . . . . . . 11 ⊢ ((𝑤 mod 𝑀) ∈ 𝑈 ↔ ((𝑤 mod 𝑀) ∈ (0..^𝑀) ∧ ((𝑤 mod 𝑀) gcd 𝑀) = 1))
79	37, 75, 78	sylanbrc 695	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑀) ∈ 𝑈)
80		zmodfzo 12555	. . . . . . . . . . . 12 ⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑤 mod 𝑁) ∈ (0..^𝑁))
81	32, 46, 80	syl2anc 691	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑁) ∈ (0..^𝑁))
82		modgcd 15091	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁))
83	32, 46, 82	syl2anc 691	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁))
84		gcddvds 15063	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
85	32, 47, 84	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
86	85	simpld 474	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∥ 𝑤)
87	85	simprd 478	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∥ 𝑁)
88		dvdsmul2 14842	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑀 · 𝑁))
89	40, 47, 88	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → 𝑁 ∥ (𝑀 · 𝑁))
90		nnne0 10930	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
91		simpr 476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
92	91	necon3ai 2807	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
93	46, 90, 92	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
94		gcdn0cl 15062	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑁 = 0)) → (𝑤 gcd 𝑁) ∈ ℕ)
95	32, 47, 93, 94	syl21anc 1317	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∈ ℕ)
96	95	nnzd 11357	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∈ ℤ)
97		dvdstr 14856	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑤 gcd 𝑁) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑤 gcd 𝑁) ∥ 𝑁 ∧ 𝑁 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)))
98	96, 47, 58, 97	syl3anc 1318	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (((𝑤 gcd 𝑁) ∥ 𝑁 ∧ 𝑁 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)))
99	87, 89, 98	mp2and 711	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁))
100		dvdslegcd 15064	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑤 gcd 𝑁) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) → (((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁))))
101	96, 32, 58, 65, 100	syl31anc 1321	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁))))
102	86, 99, 101	mp2and 711	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁)))
103	102, 70	breqtrd 4609	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) ≤ 1)
104		nnle1eq1 10925	. . . . . . . . . . . . . 14 ⊢ ((𝑤 gcd 𝑁) ∈ ℕ → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1))
105	95, 104	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1))
106	103, 105	mpbid 221	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 gcd 𝑁) = 1)
107	83, 106	eqtrd 2644	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = 1)
108		oveq1 6556	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑤 mod 𝑁) → (𝑦 gcd 𝑁) = ((𝑤 mod 𝑁) gcd 𝑁))
109	108	eqeq1d 2612	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑤 mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝑤 mod 𝑁) gcd 𝑁) = 1))
110	109, 7	elrab2 3333	. . . . . . . . . . 11 ⊢ ((𝑤 mod 𝑁) ∈ 𝑉 ↔ ((𝑤 mod 𝑁) ∈ (0..^𝑁) ∧ ((𝑤 mod 𝑁) gcd 𝑁) = 1))
111	81, 107, 110	sylanbrc 695	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝑤 mod 𝑁) ∈ 𝑉)
112		opelxpi 5072	. . . . . . . . . 10 ⊢ (((𝑤 mod 𝑀) ∈ 𝑈 ∧ (𝑤 mod 𝑁) ∈ 𝑉) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
113	79, 111, 112	syl2anc 691	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
114	27, 113	eqeltrd 2688	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑊) → (𝐹‘𝑤) ∈ (𝑈 × 𝑉))
115	114	ralrimiva 2949	. . . . . . 7 ⊢ (𝜑 → ∀𝑤 ∈ 𝑊 (𝐹‘𝑤) ∈ (𝑈 × 𝑉))
116		crth.2	. . . . . . . . . 10 ⊢ 𝑇 = ((0..^𝑀) × (0..^𝑁))
117	28, 116, 23, 33	crth 15321	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝑆–1-1-onto→𝑇)
118		f1ofn 6051	. . . . . . . . 9 ⊢ (𝐹:𝑆–1-1-onto→𝑇 → 𝐹 Fn 𝑆)
119		fnfun 5902	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑆 → Fun 𝐹)
120	117, 118, 119	3syl 18	. . . . . . . 8 ⊢ (𝜑 → Fun 𝐹)
121		ssrab2 3650	. . . . . . . . . 10 ⊢ {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} ⊆ 𝑆
122	17, 121	eqsstri 3598	. . . . . . . . 9 ⊢ 𝑊 ⊆ 𝑆
123		fndm 5904	. . . . . . . . . 10 ⊢ (𝐹 Fn 𝑆 → dom 𝐹 = 𝑆)
124	117, 118, 123	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐹 = 𝑆)
125	122, 124	syl5sseqr 3617	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ⊆ dom 𝐹)
126		funimass4 6157	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ 𝑊 ⊆ dom 𝐹) → ((𝐹 “ 𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤 ∈ 𝑊 (𝐹‘𝑤) ∈ (𝑈 × 𝑉)))
127	120, 125, 126	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → ((𝐹 “ 𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤 ∈ 𝑊 (𝐹‘𝑤) ∈ (𝑈 × 𝑉)))
128	115, 127	mpbird 246	. . . . . 6 ⊢ (𝜑 → (𝐹 “ 𝑊) ⊆ (𝑈 × 𝑉))
129	1, 3	eqsstri 3598	. . . . . . . . . . . . 13 ⊢ 𝑈 ⊆ (0..^𝑀)
130	7, 9	eqsstri 3598	. . . . . . . . . . . . 13 ⊢ 𝑉 ⊆ (0..^𝑁)
131		xpss12 5148	. . . . . . . . . . . . 13 ⊢ ((𝑈 ⊆ (0..^𝑀) ∧ 𝑉 ⊆ (0..^𝑁)) → (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁)))
132	129, 130, 131	mp2an 704	. . . . . . . . . . . 12 ⊢ (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁))
133	132, 116	sseqtr4i 3601	. . . . . . . . . . 11 ⊢ (𝑈 × 𝑉) ⊆ 𝑇
134	133	sseli 3564	. . . . . . . . . 10 ⊢ (𝑧 ∈ (𝑈 × 𝑉) → 𝑧 ∈ 𝑇)
135		f1ocnvfv2 6433	. . . . . . . . . 10 ⊢ ((𝐹:𝑆–1-1-onto→𝑇 ∧ 𝑧 ∈ 𝑇) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
136	117, 134, 135	syl2an 493	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
137		f1ocnv 6062	. . . . . . . . . . . . 13 ⊢ (𝐹:𝑆–1-1-onto→𝑇 → ^◡𝐹:𝑇–1-1-onto→𝑆)
138		f1of 6050	. . . . . . . . . . . . 13 ⊢ (^◡𝐹:𝑇–1-1-onto→𝑆 → ^◡𝐹:𝑇⟶𝑆)
139	117, 137, 138	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ^◡𝐹:𝑇⟶𝑆)
140		ffvelrn 6265	. . . . . . . . . . . 12 ⊢ ((^◡𝐹:𝑇⟶𝑆 ∧ 𝑧 ∈ 𝑇) → (^◡𝐹‘𝑧) ∈ 𝑆)
141	139, 134, 140	syl2an 493	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (^◡𝐹‘𝑧) ∈ 𝑆)
142	141, 28	syl6eleq 2698	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (^◡𝐹‘𝑧) ∈ (0..^(𝑀 · 𝑁)))
143		elfzoelz 12339	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹‘𝑧) ∈ (0..^(𝑀 · 𝑁)) → (^◡𝐹‘𝑧) ∈ ℤ)
144	142, 143	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (^◡𝐹‘𝑧) ∈ ℤ)
145	34	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℕ)
146		modgcd 15091	. . . . . . . . . . . . . 14 ⊢ (((^◡𝐹‘𝑧) ∈ ℤ ∧ 𝑀 ∈ ℕ) → (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = ((^◡𝐹‘𝑧) gcd 𝑀))
147	144, 145, 146	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = ((^◡𝐹‘𝑧) gcd 𝑀))
148		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = (^◡𝐹‘𝑧) → (𝑤 mod 𝑀) = ((^◡𝐹‘𝑧) mod 𝑀))
149		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = (^◡𝐹‘𝑧) → (𝑤 mod 𝑁) = ((^◡𝐹‘𝑧) mod 𝑁))
150	148, 149	opeq12d 4348	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = (^◡𝐹‘𝑧) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ = ⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩)
151	22	cbvmptv 4678	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ 𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩) = (𝑤 ∈ 𝑆 ↦ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
152	23, 151	eqtri 2632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐹 = (𝑤 ∈ 𝑆 ↦ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
153		opex 4859	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩ ∈ V
154	150, 152, 153	fvmpt 6191	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((^◡𝐹‘𝑧) ∈ 𝑆 → (𝐹‘(^◡𝐹‘𝑧)) = ⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩)
155	141, 154	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(^◡𝐹‘𝑧)) = ⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩)
156	136, 155	eqtr3d 2646	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 = ⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩)
157		simpr 476	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝑈 × 𝑉))
158	156, 157	eqeltrrd 2689	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
159		opelxp 5070	. . . . . . . . . . . . . . . . 17 ⊢ (⟨((^◡𝐹‘𝑧) mod 𝑀), ((^◡𝐹‘𝑧) mod 𝑁)⟩ ∈ (𝑈 × 𝑉) ↔ (((^◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈 ∧ ((^◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉))
160	158, 159	sylib 207	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈 ∧ ((^◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉))
161	160	simpld 474	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((^◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈)
162		oveq1 6556	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ((^◡𝐹‘𝑧) mod 𝑀) → (𝑦 gcd 𝑀) = (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀))
163	162	eqeq1d 2612	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ((^◡𝐹‘𝑧) mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1))
164	163, 1	elrab2 3333	. . . . . . . . . . . . . . 15 ⊢ (((^◡𝐹‘𝑧) mod 𝑀) ∈ 𝑈 ↔ (((^◡𝐹‘𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1))
165	161, 164	sylib 207	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1))
166	165	simprd 478	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑀) gcd 𝑀) = 1)
167	147, 166	eqtr3d 2646	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((^◡𝐹‘𝑧) gcd 𝑀) = 1)
168	45	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℕ)
169		modgcd 15091	. . . . . . . . . . . . . 14 ⊢ (((^◡𝐹‘𝑧) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = ((^◡𝐹‘𝑧) gcd 𝑁))
170	144, 168, 169	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = ((^◡𝐹‘𝑧) gcd 𝑁))
171	160	simprd 478	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((^◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉)
172		oveq1 6556	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ((^◡𝐹‘𝑧) mod 𝑁) → (𝑦 gcd 𝑁) = (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁))
173	172	eqeq1d 2612	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ((^◡𝐹‘𝑧) mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1))
174	173, 7	elrab2 3333	. . . . . . . . . . . . . . 15 ⊢ (((^◡𝐹‘𝑧) mod 𝑁) ∈ 𝑉 ↔ (((^◡𝐹‘𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1))
175	171, 174	sylib 207	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1))
176	175	simprd 478	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (((^◡𝐹‘𝑧) mod 𝑁) gcd 𝑁) = 1)
177	170, 176	eqtr3d 2646	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((^◡𝐹‘𝑧) gcd 𝑁) = 1)
178	34	nnzd 11357	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℤ)
179	178	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℤ)
180	45	nnzd 11357	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℤ)
181	180	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℤ)
182		rpmul 15211	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘𝑧) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((((^◡𝐹‘𝑧) gcd 𝑀) = 1 ∧ ((^◡𝐹‘𝑧) gcd 𝑁) = 1) → ((^◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1))
183	144, 179, 181, 182	syl3anc 1318	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((((^◡𝐹‘𝑧) gcd 𝑀) = 1 ∧ ((^◡𝐹‘𝑧) gcd 𝑁) = 1) → ((^◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1))
184	167, 177, 183	mp2and 711	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → ((^◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1)
185		oveq1 6556	. . . . . . . . . . . . 13 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (𝑦 gcd (𝑀 · 𝑁)) = ((^◡𝐹‘𝑧) gcd (𝑀 · 𝑁)))
186	185	eqeq1d 2612	. . . . . . . . . . . 12 ⊢ (𝑦 = (^◡𝐹‘𝑧) → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ ((^◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1))
187	186, 17	elrab2 3333	. . . . . . . . . . 11 ⊢ ((^◡𝐹‘𝑧) ∈ 𝑊 ↔ ((^◡𝐹‘𝑧) ∈ 𝑆 ∧ ((^◡𝐹‘𝑧) gcd (𝑀 · 𝑁)) = 1))
188	141, 184, 187	sylanbrc 695	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (^◡𝐹‘𝑧) ∈ 𝑊)
189		funfvima2 6397	. . . . . . . . . . . 12 ⊢ ((Fun 𝐹 ∧ 𝑊 ⊆ dom 𝐹) → ((^◡𝐹‘𝑧) ∈ 𝑊 → (𝐹‘(^◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊)))
190	120, 125, 189	syl2anc 691	. . . . . . . . . . 11 ⊢ (𝜑 → ((^◡𝐹‘𝑧) ∈ 𝑊 → (𝐹‘(^◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊)))
191	190	imp 444	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (^◡𝐹‘𝑧) ∈ 𝑊) → (𝐹‘(^◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊))
192	188, 191	syldan 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(^◡𝐹‘𝑧)) ∈ (𝐹 “ 𝑊))
193	136, 192	eqeltrrd 2689	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝐹 “ 𝑊))
194	193	ex 449	. . . . . . 7 ⊢ (𝜑 → (𝑧 ∈ (𝑈 × 𝑉) → 𝑧 ∈ (𝐹 “ 𝑊)))
195	194	ssrdv 3574	. . . . . 6 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ (𝐹 “ 𝑊))
196	128, 195	eqssd 3585	. . . . 5 ⊢ (𝜑 → (𝐹 “ 𝑊) = (𝑈 × 𝑉))
197		f1of1 6049	. . . . . . 7 ⊢ (𝐹:𝑆–1-1-onto→𝑇 → 𝐹:𝑆–1-1→𝑇)
198	117, 197	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹:𝑆–1-1→𝑇)
199		fzofi 12635	. . . . . . . . . 10 ⊢ (0..^(𝑀 · 𝑁)) ∈ Fin
200	28, 199	eqeltri 2684	. . . . . . . . 9 ⊢ 𝑆 ∈ Fin
201		ssfi 8065	. . . . . . . . 9 ⊢ ((𝑆 ∈ Fin ∧ 𝑊 ⊆ 𝑆) → 𝑊 ∈ Fin)
202	200, 122, 201	mp2an 704	. . . . . . . 8 ⊢ 𝑊 ∈ Fin
203	202	elexi 3186	. . . . . . 7 ⊢ 𝑊 ∈ V
204	203	f1imaen 7904	. . . . . 6 ⊢ ((𝐹:𝑆–1-1→𝑇 ∧ 𝑊 ⊆ 𝑆) → (𝐹 “ 𝑊) ≈ 𝑊)
205	198, 122, 204	sylancl 693	. . . . 5 ⊢ (𝜑 → (𝐹 “ 𝑊) ≈ 𝑊)
206	196, 205	eqbrtrrd 4607	. . . 4 ⊢ (𝜑 → (𝑈 × 𝑉) ≈ 𝑊)
207		xpfi 8116	. . . . . 6 ⊢ ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) → (𝑈 × 𝑉) ∈ Fin)
208	6, 12, 207	mp2an 704	. . . . 5 ⊢ (𝑈 × 𝑉) ∈ Fin
209		hashen 12997	. . . . 5 ⊢ (((𝑈 × 𝑉) ∈ Fin ∧ 𝑊 ∈ Fin) → ((#‘(𝑈 × 𝑉)) = (#‘𝑊) ↔ (𝑈 × 𝑉) ≈ 𝑊))
210	208, 202, 209	mp2an 704	. . . 4 ⊢ ((#‘(𝑈 × 𝑉)) = (#‘𝑊) ↔ (𝑈 × 𝑉) ≈ 𝑊)
211	206, 210	sylibr 223	. . 3 ⊢ (𝜑 → (#‘(𝑈 × 𝑉)) = (#‘𝑊))
212	14, 211	syl5reqr 2659	. 2 ⊢ (𝜑 → (#‘𝑊) = ((#‘𝑈) · (#‘𝑉)))
213	34, 45	nnmulcld 10945	. . 3 ⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
214		dfphi2 15317	. . . 4 ⊢ ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (#‘{𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}))
215		rabeq 3166	. . . . . . 7 ⊢ (𝑆 = (0..^(𝑀 · 𝑁)) → {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1})
216	28, 215	ax-mp 5	. . . . . 6 ⊢ {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
217	17, 216	eqtri 2632	. . . . 5 ⊢ 𝑊 = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
218	217	fveq2i 6106	. . . 4 ⊢ (#‘𝑊) = (#‘{𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1})
219	214, 218	syl6eqr 2662	. . 3 ⊢ ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (#‘𝑊))
220	213, 219	syl 17	. 2 ⊢ (𝜑 → (ϕ‘(𝑀 · 𝑁)) = (#‘𝑊))
221		dfphi2 15317	. . . . 5 ⊢ (𝑀 ∈ ℕ → (ϕ‘𝑀) = (#‘{𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}))
222	1	fveq2i 6106	. . . . 5 ⊢ (#‘𝑈) = (#‘{𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1})
223	221, 222	syl6eqr 2662	. . . 4 ⊢ (𝑀 ∈ ℕ → (ϕ‘𝑀) = (#‘𝑈))
224	34, 223	syl 17	. . 3 ⊢ (𝜑 → (ϕ‘𝑀) = (#‘𝑈))
225		dfphi2 15317	. . . . 5 ⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) = (#‘{𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}))
226	7	fveq2i 6106	. . . . 5 ⊢ (#‘𝑉) = (#‘{𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1})
227	225, 226	syl6eqr 2662	. . . 4 ⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) = (#‘𝑉))
228	45, 227	syl 17	. . 3 ⊢ (𝜑 → (ϕ‘𝑁) = (#‘𝑉))
229	224, 228	oveq12d 6567	. 2 ⊢ (𝜑 → ((ϕ‘𝑀) · (ϕ‘𝑁)) = ((#‘𝑈) · (#‘𝑉)))
230	212, 220, 229	3eqtr4d 2654	1 ⊢ (𝜑 → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∀wral 2896 {crab 2900 ⊆ wss 3540 ⟨cop 4131 class class class wbr 4583 ↦ cmpt 4643 × cxp 5036 ^◡ccnv 5037 dom cdm 5038 “ cima 5041 Fun wfun 5798 Fn wfn 5799 ⟶wf 5800 –1-1→wf1 5801 –1-1-onto→wf1o 5803 ‘cfv 5804 (class class class)co 6549 ≈ cen 7838 Fincfn 7841 0cc0 9815 1c1 9816 · cmul 9820 ≤ cle 9954 ℕcn 10897 ℤcz 11254 ..^cfzo 12334 mod cmo 12530 #chash 12979 ∥ cdvds 14821 gcd cgcd 15054 ϕcphi 15307

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-map 7746 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-sup 8231 df-inf 8232 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-n0 11170 df-xnn0 11241 df-z 11255 df-uz 11564 df-rp 11709 df-fz 12198 df-fzo 12335 df-fl 12455 df-mod 12531 df-seq 12664 df-exp 12723 df-hash 12980 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-dvds 14822 df-gcd 15055 df-phi 15309

This theorem is referenced by: phimul 15323

W3C validator