phimullem

	Ref	Expression
Hypotheses	crth.1	$⊢ S = (0 ..^M \cdot N)$
	crth.2	$⊢ T = (0 ..^M) \times (0 ..^N)$
	crth.3	$⊢ F = (x \in S ⟼ ⟨x \mod M, x \mod N⟩)$
	crth.4	$⊢ φ \to (M \in ℕ \land N \in ℕ \land M \gcd N = 1)$
	phimul.4	$⊢ U = \{y \in (0 ..^M) \| y \gcd M = 1\}$
	phimul.5	$⊢ V = \{y \in (0 ..^N) \| y \gcd N = 1\}$
	phimul.6	$⊢ W = \{y \in S \| y \gcd M \cdot N = 1\}$
Assertion	phimullem	$⊢ φ \to ϕ (M \cdot N) = ϕ (M) ϕ (N)$

Proof

Step	Hyp	Ref	Expression
1		crth.1	$⊢ S = (0 ..^M \cdot N)$
2		crth.2	$⊢ T = (0 ..^M) \times (0 ..^N)$
3		crth.3	$⊢ F = (x \in S ⟼ ⟨x \mod M, x \mod N⟩)$
4		crth.4	$⊢ φ \to (M \in ℕ \land N \in ℕ \land M \gcd N = 1)$
5		phimul.4	$⊢ U = \{y \in (0 ..^M) \| y \gcd M = 1\}$
6		phimul.5	$⊢ V = \{y \in (0 ..^N) \| y \gcd N = 1\}$
7		phimul.6	$⊢ W = \{y \in S \| y \gcd M \cdot N = 1\}$
8		oveq1	$⊢ y = w \to y \gcd M \cdot N = w \gcd M \cdot N$
9	8	eqeq1d	$⊢ y = w \to (y \gcd M \cdot N = 1 \leftrightarrow w \gcd M \cdot N = 1)$
10	9 7	elrab2	$⊢ w \in W \leftrightarrow (w \in S \land w \gcd M \cdot N = 1)$
11	10	simplbi	$⊢ w \in W \to w \in S$
12		oveq1	$⊢ x = w \to x \mod M = w \mod M$
13		oveq1	$⊢ x = w \to x \mod N = w \mod N$
14	12 13	opeq12d	$⊢ x = w \to ⟨x \mod M, x \mod N⟩ = ⟨w \mod M, w \mod N⟩$
15		opex	$⊢ ⟨w \mod M, w \mod N⟩ \in V$
16	14 3 15	fvmpt	$⊢ w \in S \to F (w) = ⟨w \mod M, w \mod N⟩$
17	11 16	syl	$⊢ w \in W \to F (w) = ⟨w \mod M, w \mod N⟩$
18	17	adantl	$⊢ (φ \land w \in W) \to F (w) = ⟨w \mod M, w \mod N⟩$
19	11 1	eleqtrdi	$⊢ w \in W \to w \in (0 ..^M \cdot N)$
20	19	adantl	$⊢ (φ \land w \in W) \to w \in (0 ..^M \cdot N)$
21		elfzoelz	$⊢ w \in (0 ..^M \cdot N) \to w \in ℤ$
22	20 21	syl	$⊢ (φ \land w \in W) \to w \in ℤ$
23	4	simp1d	$⊢ φ \to M \in ℕ$
24	23	adantr	$⊢ (φ \land w \in W) \to M \in ℕ$
25		zmodfzo	$⊢ (w \in ℤ \land M \in ℕ) \to w \mod M \in (0 ..^M)$
26	22 24 25	syl2anc	$⊢ (φ \land w \in W) \to w \mod M \in (0 ..^M)$
27		modgcd	$⊢ (w \in ℤ \land M \in ℕ) \to (w \mod M) \gcd M = w \gcd M$
28	22 24 27	syl2anc	$⊢ (φ \land w \in W) \to (w \mod M) \gcd M = w \gcd M$
29	24	nnzd	$⊢ (φ \land w \in W) \to M \in ℤ$
30		gcddvds	$⊢ (w \in ℤ \land M \in ℤ) \to ((w \gcd M) ∥ w \land (w \gcd M) ∥ M)$
31	22 29 30	syl2anc	$⊢ (φ \land w \in W) \to ((w \gcd M) ∥ w \land (w \gcd M) ∥ M)$
32	31	simpld	$⊢ (φ \land w \in W) \to (w \gcd M) ∥ w$
33		nnne0	$⊢ M \in ℕ \to M \neq 0$
34		simpr	$⊢ (w = 0 \land M = 0) \to M = 0$
35	34	necon3ai	$⊢ M \neq 0 \to \neg (w = 0 \land M = 0)$
36	24 33 35	3syl	$⊢ (φ \land w \in W) \to \neg (w = 0 \land M = 0)$
37		gcdn0cl	$⊢ ((w \in ℤ \land M \in ℤ) \land \neg (w = 0 \land M = 0)) \to w \gcd M \in ℕ$
38	22 29 36 37	syl21anc	$⊢ (φ \land w \in W) \to w \gcd M \in ℕ$
39	38	nnzd	$⊢ (φ \land w \in W) \to w \gcd M \in ℤ$
40	4	simp2d	$⊢ φ \to N \in ℕ$
41	40	adantr	$⊢ (φ \land w \in W) \to N \in ℕ$
42	41	nnzd	$⊢ (φ \land w \in W) \to N \in ℤ$
43	31	simprd	$⊢ (φ \land w \in W) \to (w \gcd M) ∥ M$
44	39 29 42 43	dvdsmultr1d	$⊢ (φ \land w \in W) \to (w \gcd M) ∥ M \cdot N$
45	24 41	nnmulcld	$⊢ (φ \land w \in W) \to M \cdot N \in ℕ$
46	45	nnzd	$⊢ (φ \land w \in W) \to M \cdot N \in ℤ$
47		nnne0	$⊢ M \cdot N \in ℕ \to M \cdot N \neq 0$
48		simpr	$⊢ (w = 0 \land M \cdot N = 0) \to M \cdot N = 0$
49	48	necon3ai	$⊢ M \cdot N \neq 0 \to \neg (w = 0 \land M \cdot N = 0)$
50	45 47 49	3syl	$⊢ (φ \land w \in W) \to \neg (w = 0 \land M \cdot N = 0)$
51		dvdslegcd	$⊢ ((w \gcd M \in ℤ \land w \in ℤ \land M \cdot N \in ℤ) \land \neg (w = 0 \land M \cdot N = 0)) \to (((w \gcd M) ∥ w \land (w \gcd M) ∥ M \cdot N) \to w \gcd M \leq w \gcd M \cdot N)$
52	39 22 46 50 51	syl31anc	$⊢ (φ \land w \in W) \to (((w \gcd M) ∥ w \land (w \gcd M) ∥ M \cdot N) \to w \gcd M \leq w \gcd M \cdot N)$
53	32 44 52	mp2and	$⊢ (φ \land w \in W) \to w \gcd M \leq w \gcd M \cdot N$
54	10	simprbi	$⊢ w \in W \to w \gcd M \cdot N = 1$
55	54	adantl	$⊢ (φ \land w \in W) \to w \gcd M \cdot N = 1$
56	53 55	breqtrd	$⊢ (φ \land w \in W) \to w \gcd M \leq 1$
57		nnle1eq1	$⊢ w \gcd M \in ℕ \to (w \gcd M \leq 1 \leftrightarrow w \gcd M = 1)$
58	38 57	syl	$⊢ (φ \land w \in W) \to (w \gcd M \leq 1 \leftrightarrow w \gcd M = 1)$
59	56 58	mpbid	$⊢ (φ \land w \in W) \to w \gcd M = 1$
60	28 59	eqtrd	$⊢ (φ \land w \in W) \to (w \mod M) \gcd M = 1$
61		oveq1	$⊢ y = w \mod M \to y \gcd M = (w \mod M) \gcd M$
62	61	eqeq1d	$⊢ y = w \mod M \to (y \gcd M = 1 \leftrightarrow (w \mod M) \gcd M = 1)$
63	62 5	elrab2	$⊢ w \mod M \in U \leftrightarrow (w \mod M \in (0 ..^M) \land (w \mod M) \gcd M = 1)$
64	26 60 63	sylanbrc	$⊢ (φ \land w \in W) \to w \mod M \in U$
65		zmodfzo	$⊢ (w \in ℤ \land N \in ℕ) \to w \mod N \in (0 ..^N)$
66	22 41 65	syl2anc	$⊢ (φ \land w \in W) \to w \mod N \in (0 ..^N)$
67		modgcd	$⊢ (w \in ℤ \land N \in ℕ) \to (w \mod N) \gcd N = w \gcd N$
68	22 41 67	syl2anc	$⊢ (φ \land w \in W) \to (w \mod N) \gcd N = w \gcd N$
69		gcddvds	$⊢ (w \in ℤ \land N \in ℤ) \to ((w \gcd N) ∥ w \land (w \gcd N) ∥ N)$
70	22 42 69	syl2anc	$⊢ (φ \land w \in W) \to ((w \gcd N) ∥ w \land (w \gcd N) ∥ N)$
71	70	simpld	$⊢ (φ \land w \in W) \to (w \gcd N) ∥ w$
72		nnne0	$⊢ N \in ℕ \to N \neq 0$
73		simpr	$⊢ (w = 0 \land N = 0) \to N = 0$
74	73	necon3ai	$⊢ N \neq 0 \to \neg (w = 0 \land N = 0)$
75	41 72 74	3syl	$⊢ (φ \land w \in W) \to \neg (w = 0 \land N = 0)$
76		gcdn0cl	$⊢ ((w \in ℤ \land N \in ℤ) \land \neg (w = 0 \land N = 0)) \to w \gcd N \in ℕ$
77	22 42 75 76	syl21anc	$⊢ (φ \land w \in W) \to w \gcd N \in ℕ$
78	77	nnzd	$⊢ (φ \land w \in W) \to w \gcd N \in ℤ$
79	70	simprd	$⊢ (φ \land w \in W) \to (w \gcd N) ∥ N$
80		dvdsmul2	$⊢ (M \in ℤ \land N \in ℤ) \to N ∥ M \cdot N$
81	29 42 80	syl2anc	$⊢ (φ \land w \in W) \to N ∥ M \cdot N$
82	78 42 46 79 81	dvdstrd	$⊢ (φ \land w \in W) \to (w \gcd N) ∥ M \cdot N$
83		dvdslegcd	$⊢ ((w \gcd N \in ℤ \land w \in ℤ \land M \cdot N \in ℤ) \land \neg (w = 0 \land M \cdot N = 0)) \to (((w \gcd N) ∥ w \land (w \gcd N) ∥ M \cdot N) \to w \gcd N \leq w \gcd M \cdot N)$
84	78 22 46 50 83	syl31anc	$⊢ (φ \land w \in W) \to (((w \gcd N) ∥ w \land (w \gcd N) ∥ M \cdot N) \to w \gcd N \leq w \gcd M \cdot N)$
85	71 82 84	mp2and	$⊢ (φ \land w \in W) \to w \gcd N \leq w \gcd M \cdot N$
86	85 55	breqtrd	$⊢ (φ \land w \in W) \to w \gcd N \leq 1$
87		nnle1eq1	$⊢ w \gcd N \in ℕ \to (w \gcd N \leq 1 \leftrightarrow w \gcd N = 1)$
88	77 87	syl	$⊢ (φ \land w \in W) \to (w \gcd N \leq 1 \leftrightarrow w \gcd N = 1)$
89	86 88	mpbid	$⊢ (φ \land w \in W) \to w \gcd N = 1$
90	68 89	eqtrd	$⊢ (φ \land w \in W) \to (w \mod N) \gcd N = 1$
91		oveq1	$⊢ y = w \mod N \to y \gcd N = (w \mod N) \gcd N$
92	91	eqeq1d	$⊢ y = w \mod N \to (y \gcd N = 1 \leftrightarrow (w \mod N) \gcd N = 1)$
93	92 6	elrab2	$⊢ w \mod N \in V \leftrightarrow (w \mod N \in (0 ..^N) \land (w \mod N) \gcd N = 1)$
94	66 90 93	sylanbrc	$⊢ (φ \land w \in W) \to w \mod N \in V$
95	64 94	opelxpd	$⊢ (φ \land w \in W) \to ⟨w \mod M, w \mod N⟩ \in (U \times V)$
96	18 95	eqeltrd	$⊢ (φ \land w \in W) \to F (w) \in (U \times V)$
97	96	ralrimiva	$⊢ φ \to \forall w \in W F (w) \in (U \times V)$
98	1 2 3 4	crth	$⊢ φ \to F : S \underset{1-1 onto}{⟶} T$
99		f1ofn	$⊢ F : S \underset{1-1 onto}{⟶} T \to F Fn S$
100		fnfun	$⊢ F Fn S \to Fun F$
101	98 99 100	3syl	$⊢ φ \to Fun F$
102	7	ssrab3	$⊢ W \subseteq S$
103		fndm	$⊢ F Fn S \to dom F = S$
104	98 99 103	3syl	$⊢ φ \to dom F = S$
105	102 104	sseqtrrid	$⊢ φ \to W \subseteq dom F$
106		funimass4	$⊢ (Fun F \land W \subseteq dom F) \to (F [W] \subseteq U \times V \leftrightarrow \forall w \in W F (w) \in (U \times V))$
107	101 105 106	syl2anc	$⊢ φ \to (F [W] \subseteq U \times V \leftrightarrow \forall w \in W F (w) \in (U \times V))$
108	97 107	mpbird	$⊢ φ \to F [W] \subseteq U \times V$
109	5	ssrab3	$⊢ U \subseteq (0 ..^M)$
110	6	ssrab3	$⊢ V \subseteq (0 ..^N)$
111		xpss12	$⊢ (U \subseteq (0 ..^M) \land V \subseteq (0 ..^N)) \to U \times V \subseteq (0 ..^M) \times (0 ..^N)$
112	109 110 111	mp2an	$⊢ U \times V \subseteq (0 ..^M) \times (0 ..^N)$
113	112 2	sseqtrri	$⊢ U \times V \subseteq T$
114	113	sseli	$⊢ z \in (U \times V) \to z \in T$
115		f1ocnvfv2	$⊢ (F : S \underset{1-1 onto}{⟶} T \land z \in T) \to F (F^{-1} (z)) = z$
116	98 114 115	syl2an	$⊢ (φ \land z \in (U \times V)) \to F (F^{-1} (z)) = z$
117		f1ocnv	$⊢ F : S \underset{1-1 onto}{⟶} T \to F^{-1} : T \underset{1-1 onto}{⟶} S$
118		f1of	$⊢ F^{-1} : T \underset{1-1 onto}{⟶} S \to F^{-1} : T ⟶ S$
119	98 117 118	3syl	$⊢ φ \to F^{-1} : T ⟶ S$
120		ffvelrn	$⊢ (F^{-1} : T ⟶ S \land z \in T) \to F^{-1} (z) \in S$
121	119 114 120	syl2an	$⊢ (φ \land z \in (U \times V)) \to F^{-1} (z) \in S$
122	121 1	eleqtrdi	$⊢ (φ \land z \in (U \times V)) \to F^{-1} (z) \in (0 ..^M \cdot N)$
123		elfzoelz	$⊢ F^{-1} (z) \in (0 ..^M \cdot N) \to F^{-1} (z) \in ℤ$
124	122 123	syl	$⊢ (φ \land z \in (U \times V)) \to F^{-1} (z) \in ℤ$
125	23	adantr	$⊢ (φ \land z \in (U \times V)) \to M \in ℕ$
126		modgcd	$⊢ (F^{-1} (z) \in ℤ \land M \in ℕ) \to (F^{-1} (z) \mod M) \gcd M = F^{-1} (z) \gcd M$
127	124 125 126	syl2anc	$⊢ (φ \land z \in (U \times V)) \to (F^{-1} (z) \mod M) \gcd M = F^{-1} (z) \gcd M$
128		oveq1	$⊢ w = F^{-1} (z) \to w \mod M = F^{-1} (z) \mod M$
129		oveq1	$⊢ w = F^{-1} (z) \to w \mod N = F^{-1} (z) \mod N$
130	128 129	opeq12d	$⊢ w = F^{-1} (z) \to ⟨w \mod M, w \mod N⟩ = ⟨F^{-1} (z) \mod M, F^{-1} (z) \mod N⟩$
131	14	cbvmptv	$⊢ (x \in S ⟼ ⟨x \mod M, x \mod N⟩) = (w \in S ⟼ ⟨w \mod M, w \mod N⟩)$
132	3 131	eqtri	$⊢ F = (w \in S ⟼ ⟨w \mod M, w \mod N⟩)$
133		opex	$⊢ ⟨F^{-1} (z) \mod M, F^{-1} (z) \mod N⟩ \in V$
134	130 132 133	fvmpt	$⊢ F^{-1} (z) \in S \to F (F^{-1} (z)) = ⟨F^{-1} (z) \mod M, F^{-1} (z) \mod N⟩$
135	121 134	syl	$⊢ (φ \land z \in (U \times V)) \to F (F^{-1} (z)) = ⟨F^{-1} (z) \mod M, F^{-1} (z) \mod N⟩$
136	116 135	eqtr3d	$⊢ (φ \land z \in (U \times V)) \to z = ⟨F^{-1} (z) \mod M, F^{-1} (z) \mod N⟩$
137		simpr	$⊢ (φ \land z \in (U \times V)) \to z \in (U \times V)$
138	136 137	eqeltrrd	$⊢ (φ \land z \in (U \times V)) \to ⟨F^{-1} (z) \mod M, F^{-1} (z) \mod N⟩ \in (U \times V)$
139		opelxp	$⊢ ⟨F^{-1} (z) \mod M, F^{-1} (z) \mod N⟩ \in (U \times V) \leftrightarrow (F^{-1} (z) \mod M \in U \land F^{-1} (z) \mod N \in V)$
140	138 139	sylib	$⊢ (φ \land z \in (U \times V)) \to (F^{-1} (z) \mod M \in U \land F^{-1} (z) \mod N \in V)$
141	140	simpld	$⊢ (φ \land z \in (U \times V)) \to F^{-1} (z) \mod M \in U$
142		oveq1	$⊢ y = F^{-1} (z) \mod M \to y \gcd M = (F^{-1} (z) \mod M) \gcd M$
143	142	eqeq1d	$⊢ y = F^{-1} (z) \mod M \to (y \gcd M = 1 \leftrightarrow (F^{-1} (z) \mod M) \gcd M = 1)$
144	143 5	elrab2	$⊢ F^{-1} (z) \mod M \in U \leftrightarrow (F^{-1} (z) \mod M \in (0 ..^M) \land (F^{-1} (z) \mod M) \gcd M = 1)$
145	141 144	sylib	$⊢ (φ \land z \in (U \times V)) \to (F^{-1} (z) \mod M \in (0 ..^M) \land (F^{-1} (z) \mod M) \gcd M = 1)$
146	145	simprd	$⊢ (φ \land z \in (U \times V)) \to (F^{-1} (z) \mod M) \gcd M = 1$
147	127 146	eqtr3d	$⊢ (φ \land z \in (U \times V)) \to F^{-1} (z) \gcd M = 1$
148	40	adantr	$⊢ (φ \land z \in (U \times V)) \to N \in ℕ$
149		modgcd	$⊢ (F^{-1} (z) \in ℤ \land N \in ℕ) \to (F^{-1} (z) \mod N) \gcd N = F^{-1} (z) \gcd N$
150	124 148 149	syl2anc	$⊢ (φ \land z \in (U \times V)) \to (F^{-1} (z) \mod N) \gcd N = F^{-1} (z) \gcd N$
151	140	simprd	$⊢ (φ \land z \in (U \times V)) \to F^{-1} (z) \mod N \in V$
152		oveq1	$⊢ y = F^{-1} (z) \mod N \to y \gcd N = (F^{-1} (z) \mod N) \gcd N$
153	152	eqeq1d	$⊢ y = F^{-1} (z) \mod N \to (y \gcd N = 1 \leftrightarrow (F^{-1} (z) \mod N) \gcd N = 1)$
154	153 6	elrab2	$⊢ F^{-1} (z) \mod N \in V \leftrightarrow (F^{-1} (z) \mod N \in (0 ..^N) \land (F^{-1} (z) \mod N) \gcd N = 1)$
155	151 154	sylib	$⊢ (φ \land z \in (U \times V)) \to (F^{-1} (z) \mod N \in (0 ..^N) \land (F^{-1} (z) \mod N) \gcd N = 1)$
156	155	simprd	$⊢ (φ \land z \in (U \times V)) \to (F^{-1} (z) \mod N) \gcd N = 1$
157	150 156	eqtr3d	$⊢ (φ \land z \in (U \times V)) \to F^{-1} (z) \gcd N = 1$
158	23	nnzd	$⊢ φ \to M \in ℤ$
159	158	adantr	$⊢ (φ \land z \in (U \times V)) \to M \in ℤ$
160	40	nnzd	$⊢ φ \to N \in ℤ$
161	160	adantr	$⊢ (φ \land z \in (U \times V)) \to N \in ℤ$
162		rpmul	$⊢ (F^{-1} (z) \in ℤ \land M \in ℤ \land N \in ℤ) \to ((F^{-1} (z) \gcd M = 1 \land F^{-1} (z) \gcd N = 1) \to F^{-1} (z) \gcd M \cdot N = 1)$
163	124 159 161 162	syl3anc	$⊢ (φ \land z \in (U \times V)) \to ((F^{-1} (z) \gcd M = 1 \land F^{-1} (z) \gcd N = 1) \to F^{-1} (z) \gcd M \cdot N = 1)$
164	147 157 163	mp2and	$⊢ (φ \land z \in (U \times V)) \to F^{-1} (z) \gcd M \cdot N = 1$
165		oveq1	$⊢ y = F^{-1} (z) \to y \gcd M \cdot N = F^{-1} (z) \gcd M \cdot N$
166	165	eqeq1d	$⊢ y = F^{-1} (z) \to (y \gcd M \cdot N = 1 \leftrightarrow F^{-1} (z) \gcd M \cdot N = 1)$
167	166 7	elrab2	$⊢ F^{-1} (z) \in W \leftrightarrow (F^{-1} (z) \in S \land F^{-1} (z) \gcd M \cdot N = 1)$
168	121 164 167	sylanbrc	$⊢ (φ \land z \in (U \times V)) \to F^{-1} (z) \in W$
169		funfvima2	$⊢ (Fun F \land W \subseteq dom F) \to (F^{-1} (z) \in W \to F (F^{-1} (z)) \in F [W])$
170	101 105 169	syl2anc	$⊢ φ \to (F^{-1} (z) \in W \to F (F^{-1} (z)) \in F [W])$
171	170	imp	$⊢ (φ \land F^{-1} (z) \in W) \to F (F^{-1} (z)) \in F [W]$
172	168 171	syldan	$⊢ (φ \land z \in (U \times V)) \to F (F^{-1} (z)) \in F [W]$
173	116 172	eqeltrrd	$⊢ (φ \land z \in (U \times V)) \to z \in F [W]$
174	108 173	eqelssd	$⊢ φ \to F [W] = U \times V$
175		f1of1	$⊢ F : S \underset{1-1 onto}{⟶} T \to F : S \underset{1-1}{⟶} T$
176	98 175	syl	$⊢ φ \to F : S \underset{1-1}{⟶} T$
177		fzofi	$⊢ (0 ..^M \cdot N) \in Fin$
178	1 177	eqeltri	$⊢ S \in Fin$
179		ssfi	$⊢ (S \in Fin \land W \subseteq S) \to W \in Fin$
180	178 102 179	mp2an	$⊢ W \in Fin$
181	180	elexi	$⊢ W \in V$
182	181	f1imaen	$⊢ (F : S \underset{1-1}{⟶} T \land W \subseteq S) \to F [W] \approx W$
183	176 102 182	sylancl	$⊢ φ \to F [W] \approx W$
184	174 183	eqbrtrrd	$⊢ φ \to (U \times V) \approx W$
185		fzofi	$⊢ (0 ..^M) \in Fin$
186		ssrab2	$⊢ \{y \in (0 ..^M) \| y \gcd M = 1\} \subseteq (0 ..^M)$
187		ssfi	$⊢ ((0 ..^M) \in Fin \land \{y \in (0 ..^M) \| y \gcd M = 1\} \subseteq (0 ..^M)) \to \{y \in (0 ..^M) \| y \gcd M = 1\} \in Fin$
188	185 186 187	mp2an	$⊢ \{y \in (0 ..^M) \| y \gcd M = 1\} \in Fin$
189	5 188	eqeltri	$⊢ U \in Fin$
190		fzofi	$⊢ (0 ..^N) \in Fin$
191		ssrab2	$⊢ \{y \in (0 ..^N) \| y \gcd N = 1\} \subseteq (0 ..^N)$
192		ssfi	$⊢ ((0 ..^N) \in Fin \land \{y \in (0 ..^N) \| y \gcd N = 1\} \subseteq (0 ..^N)) \to \{y \in (0 ..^N) \| y \gcd N = 1\} \in Fin$
193	190 191 192	mp2an	$⊢ \{y \in (0 ..^N) \| y \gcd N = 1\} \in Fin$
194	6 193	eqeltri	$⊢ V \in Fin$
195		xpfi	$⊢ (U \in Fin \land V \in Fin) \to U \times V \in Fin$
196	189 194 195	mp2an	$⊢ U \times V \in Fin$
197		hashen	$⊢ (U \times V \in Fin \land W \in Fin) \to (\|U \times V\| = \|W\| \leftrightarrow (U \times V) \approx W)$
198	196 180 197	mp2an	$⊢ \|U \times V\| = \|W\| \leftrightarrow (U \times V) \approx W$
199	184 198	sylibr	$⊢ φ \to \|U \times V\| = \|W\|$
200		hashxp	$⊢ (U \in Fin \land V \in Fin) \to \|U \times V\| = \|U\| \|V\|$
201	189 194 200	mp2an	$⊢ \|U \times V\| = \|U\| \|V\|$
202	199 201	eqtr3di	$⊢ φ \to \|W\| = \|U\| \|V\|$
203	23 40	nnmulcld	$⊢ φ \to M \cdot N \in ℕ$
204		dfphi2	$⊢ M \cdot N \in ℕ \to ϕ (M \cdot N) = \|\{y \in (0 ..^M \cdot N) \| y \gcd M \cdot N = 1\}\|$
205	1	rabeqi	$⊢ \{y \in S \| y \gcd M \cdot N = 1\} = \{y \in (0 ..^M \cdot N) \| y \gcd M \cdot N = 1\}$
206	7 205	eqtri	$⊢ W = \{y \in (0 ..^M \cdot N) \| y \gcd M \cdot N = 1\}$
207	206	fveq2i	$⊢ \|W\| = \|\{y \in (0 ..^M \cdot N) \| y \gcd M \cdot N = 1\}\|$
208	204 207	eqtr4di	$⊢ M \cdot N \in ℕ \to ϕ (M \cdot N) = \|W\|$
209	203 208	syl	$⊢ φ \to ϕ (M \cdot N) = \|W\|$
210		dfphi2	$⊢ M \in ℕ \to ϕ (M) = \|\{y \in (0 ..^M) \| y \gcd M = 1\}\|$
211	5	fveq2i	$⊢ \|U\| = \|\{y \in (0 ..^M) \| y \gcd M = 1\}\|$
212	210 211	eqtr4di	$⊢ M \in ℕ \to ϕ (M) = \|U\|$
213	23 212	syl	$⊢ φ \to ϕ (M) = \|U\|$
214		dfphi2	$⊢ N \in ℕ \to ϕ (N) = \|\{y \in (0 ..^N) \| y \gcd N = 1\}\|$
215	6	fveq2i	$⊢ \|V\| = \|\{y \in (0 ..^N) \| y \gcd N = 1\}\|$
216	214 215	eqtr4di	$⊢ N \in ℕ \to ϕ (N) = \|V\|$
217	40 216	syl	$⊢ φ \to ϕ (N) = \|V\|$
218	213 217	oveq12d	$⊢ φ \to ϕ (M) ϕ (N) = \|U\| \|V\|$
219	202 209 218	3eqtr4d	$⊢ φ \to ϕ (M \cdot N) = ϕ (M) ϕ (N)$

Metamath Proof Explorer

Theorem phimullem

Proof