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