dvdsmulf1o

Description: If M and N are two coprime integers, multiplication forms a bijection from the set of pairs <. j , k >. where j || M and k || N , to the set of divisors of M x. N . (Contributed by Mario Carneiro, 2-Jul-2015)

	Ref	Expression
Hypotheses	dvdsmulf1o.1	$⊢ φ \to M \in ℕ$
	dvdsmulf1o.2	$⊢ φ \to N \in ℕ$
	dvdsmulf1o.3	$⊢ φ \to M \gcd N = 1$
	dvdsmulf1o.x	$⊢ X = \{x \in ℕ \| x ∥ M\}$
	dvdsmulf1o.y	$⊢ Y = \{x \in ℕ \| x ∥ N\}$
	dvdsmulf1o.z	$⊢ Z = \{x \in ℕ \| x ∥ M \cdot N\}$
Assertion	dvdsmulf1o	$⊢ φ \to ({\times ↾}_{(X \times Y)}) : X \times Y \underset{1-1 onto}{⟶} Z$

Proof

Step	Hyp	Ref	Expression
1		dvdsmulf1o.1	$⊢ φ \to M \in ℕ$
2		dvdsmulf1o.2	$⊢ φ \to N \in ℕ$
3		dvdsmulf1o.3	$⊢ φ \to M \gcd N = 1$
4		dvdsmulf1o.x	$⊢ X = \{x \in ℕ \| x ∥ M\}$
5		dvdsmulf1o.y	$⊢ Y = \{x \in ℕ \| x ∥ N\}$
6		dvdsmulf1o.z	$⊢ Z = \{x \in ℕ \| x ∥ M \cdot N\}$
7		ax-mulf	$⊢ \times : ℂ \times ℂ ⟶ ℂ$
8		ffn	$⊢ \times : ℂ \times ℂ ⟶ ℂ \to \times Fn (ℂ \times ℂ)$
9	7 8	ax-mp	$⊢ \times Fn (ℂ \times ℂ)$
10	4	ssrab3	$⊢ X \subseteq ℕ$
11		nnsscn	$⊢ ℕ \subseteq ℂ$
12	10 11	sstri	$⊢ X \subseteq ℂ$
13	5	ssrab3	$⊢ Y \subseteq ℕ$
14	13 11	sstri	$⊢ Y \subseteq ℂ$
15		xpss12	$⊢ (X \subseteq ℂ \land Y \subseteq ℂ) \to X \times Y \subseteq ℂ \times ℂ$
16	12 14 15	mp2an	$⊢ X \times Y \subseteq ℂ \times ℂ$
17		fnssres	$⊢ (\times Fn (ℂ \times ℂ) \land X \times Y \subseteq ℂ \times ℂ) \to ({\times ↾}_{(X \times Y)}) Fn (X \times Y)$
18	9 16 17	mp2an	$⊢ ({\times ↾}_{(X \times Y)}) Fn (X \times Y)$
19	18	a1i	$⊢ φ \to ({\times ↾}_{(X \times Y)}) Fn (X \times Y)$
20		ovres	$⊢ (i \in X \land j \in Y) \to i ({\times ↾}_{(X \times Y)}) j = i j$
21	20	adantl	$⊢ (φ \land (i \in X \land j \in Y)) \to i ({\times ↾}_{(X \times Y)}) j = i j$
22		breq1	$⊢ x = i \to (x ∥ M \leftrightarrow i ∥ M)$
23	22 4	elrab2	$⊢ i \in X \leftrightarrow (i \in ℕ \land i ∥ M)$
24	23	simplbi	$⊢ i \in X \to i \in ℕ$
25	24	ad2antrl	$⊢ (φ \land (i \in X \land j \in Y)) \to i \in ℕ$
26		breq1	$⊢ x = j \to (x ∥ N \leftrightarrow j ∥ N)$
27	26 5	elrab2	$⊢ j \in Y \leftrightarrow (j \in ℕ \land j ∥ N)$
28	27	simplbi	$⊢ j \in Y \to j \in ℕ$
29	28	ad2antll	$⊢ (φ \land (i \in X \land j \in Y)) \to j \in ℕ$
30	25 29	nnmulcld	$⊢ (φ \land (i \in X \land j \in Y)) \to i j \in ℕ$
31	27	simprbi	$⊢ j \in Y \to j ∥ N$
32	31	ad2antll	$⊢ (φ \land (i \in X \land j \in Y)) \to j ∥ N$
33	23	simprbi	$⊢ i \in X \to i ∥ M$
34	33	ad2antrl	$⊢ (φ \land (i \in X \land j \in Y)) \to i ∥ M$
35	29	nnzd	$⊢ (φ \land (i \in X \land j \in Y)) \to j \in ℤ$
36	2	adantr	$⊢ (φ \land (i \in X \land j \in Y)) \to N \in ℕ$
37	36	nnzd	$⊢ (φ \land (i \in X \land j \in Y)) \to N \in ℤ$
38	25	nnzd	$⊢ (φ \land (i \in X \land j \in Y)) \to i \in ℤ$
39		dvdscmul	$⊢ (j \in ℤ \land N \in ℤ \land i \in ℤ) \to (j ∥ N \to i j ∥ i \cdot N)$
40	35 37 38 39	syl3anc	$⊢ (φ \land (i \in X \land j \in Y)) \to (j ∥ N \to i j ∥ i \cdot N)$
41	1	adantr	$⊢ (φ \land (i \in X \land j \in Y)) \to M \in ℕ$
42	41	nnzd	$⊢ (φ \land (i \in X \land j \in Y)) \to M \in ℤ$
43		dvdsmulc	$⊢ (i \in ℤ \land M \in ℤ \land N \in ℤ) \to (i ∥ M \to i \cdot N ∥ M \cdot N)$
44	38 42 37 43	syl3anc	$⊢ (φ \land (i \in X \land j \in Y)) \to (i ∥ M \to i \cdot N ∥ M \cdot N)$
45	30	nnzd	$⊢ (φ \land (i \in X \land j \in Y)) \to i j \in ℤ$
46	38 37	zmulcld	$⊢ (φ \land (i \in X \land j \in Y)) \to i \cdot N \in ℤ$
47	42 37	zmulcld	$⊢ (φ \land (i \in X \land j \in Y)) \to M \cdot N \in ℤ$
48		dvdstr	$⊢ (i j \in ℤ \land i \cdot N \in ℤ \land M \cdot N \in ℤ) \to ((i j ∥ i \cdot N \land i \cdot N ∥ M \cdot N) \to i j ∥ M \cdot N)$
49	45 46 47 48	syl3anc	$⊢ (φ \land (i \in X \land j \in Y)) \to ((i j ∥ i \cdot N \land i \cdot N ∥ M \cdot N) \to i j ∥ M \cdot N)$
50	40 44 49	syl2and	$⊢ (φ \land (i \in X \land j \in Y)) \to ((j ∥ N \land i ∥ M) \to i j ∥ M \cdot N)$
51	32 34 50	mp2and	$⊢ (φ \land (i \in X \land j \in Y)) \to i j ∥ M \cdot N$
52		breq1	$⊢ x = i j \to (x ∥ M \cdot N \leftrightarrow i j ∥ M \cdot N)$
53	52 6	elrab2	$⊢ i j \in Z \leftrightarrow (i j \in ℕ \land i j ∥ M \cdot N)$
54	30 51 53	sylanbrc	$⊢ (φ \land (i \in X \land j \in Y)) \to i j \in Z$
55	21 54	eqeltrd	$⊢ (φ \land (i \in X \land j \in Y)) \to i ({\times ↾}_{(X \times Y)}) j \in Z$
56	55	ralrimivva	$⊢ φ \to \forall i \in X \forall j \in Y i ({\times ↾}_{(X \times Y)}) j \in Z$
57		ffnov	$⊢ ({\times ↾}_{(X \times Y)}) : X \times Y ⟶ Z \leftrightarrow (({\times ↾}_{(X \times Y)}) Fn (X \times Y) \land \forall i \in X \forall j \in Y i ({\times ↾}_{(X \times Y)}) j \in Z)$
58	19 56 57	sylanbrc	$⊢ φ \to ({\times ↾}_{(X \times Y)}) : X \times Y ⟶ Z$
59	25	adantr	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to i \in ℕ$
60	59	nnnn0d	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to i \in ℕ_{0}$
61		simprll	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to m \in X$
62		breq1	$⊢ x = m \to (x ∥ M \leftrightarrow m ∥ M)$
63	62 4	elrab2	$⊢ m \in X \leftrightarrow (m \in ℕ \land m ∥ M)$
64	63	simplbi	$⊢ m \in X \to m \in ℕ$
65	61 64	syl	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to m \in ℕ$
66	65	nnnn0d	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to m \in ℕ_{0}$
67	59	nnzd	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to i \in ℤ$
68	29	adantr	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to j \in ℕ$
69	68	nnzd	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to j \in ℤ$
70		dvdsmul1	$⊢ (i \in ℤ \land j \in ℤ) \to i ∥ i j$
71	67 69 70	syl2anc	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to i ∥ i j$
72		simprr	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to i j = m n$
73	12 61	sseldi	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to m \in ℂ$
74		simprlr	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to n \in Y$
75		breq1	$⊢ x = n \to (x ∥ N \leftrightarrow n ∥ N)$
76	75 5	elrab2	$⊢ n \in Y \leftrightarrow (n \in ℕ \land n ∥ N)$
77	76	simplbi	$⊢ n \in Y \to n \in ℕ$
78	74 77	syl	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to n \in ℕ$
79	78	nncnd	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to n \in ℂ$
80	73 79	mulcomd	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to m n = n m$
81	72 80	eqtrd	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to i j = n m$
82	71 81	breqtrd	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to i ∥ n m$
83	78	nnzd	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to n \in ℤ$
84	37	adantr	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to N \in ℤ$
85	67 84	gcdcomd	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to i \gcd N = N \gcd i$
86	42	adantr	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to M \in ℤ$
87	2	nnzd	$⊢ φ \to N \in ℤ$
88	1	nnzd	$⊢ φ \to M \in ℤ$
89	87 88	gcdcomd	$⊢ φ \to N \gcd M = M \gcd N$
90	89 3	eqtrd	$⊢ φ \to N \gcd M = 1$
91	90	ad2antrr	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to N \gcd M = 1$
92	34	adantr	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to i ∥ M$
93		rpdvds	$⊢ ((N \in ℤ \land i \in ℤ \land M \in ℤ) \land (N \gcd M = 1 \land i ∥ M)) \to N \gcd i = 1$
94	84 67 86 91 92 93	syl32anc	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to N \gcd i = 1$
95	85 94	eqtrd	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to i \gcd N = 1$
96	76	simprbi	$⊢ n \in Y \to n ∥ N$
97	74 96	syl	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to n ∥ N$
98		rpdvds	$⊢ ((i \in ℤ \land n \in ℤ \land N \in ℤ) \land (i \gcd N = 1 \land n ∥ N)) \to i \gcd n = 1$
99	67 83 84 95 97 98	syl32anc	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to i \gcd n = 1$
100	65	nnzd	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to m \in ℤ$
101		coprmdvds	$⊢ (i \in ℤ \land n \in ℤ \land m \in ℤ) \to ((i ∥ n m \land i \gcd n = 1) \to i ∥ m)$
102	67 83 100 101	syl3anc	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to ((i ∥ n m \land i \gcd n = 1) \to i ∥ m)$
103	82 99 102	mp2and	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to i ∥ m$
104		dvdsmul1	$⊢ (m \in ℤ \land n \in ℤ) \to m ∥ m n$
105	100 83 104	syl2anc	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to m ∥ m n$
106	59	nncnd	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to i \in ℂ$
107	68	nncnd	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to j \in ℂ$
108	106 107	mulcomd	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to i j = j i$
109	72 108	eqtr3d	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to m n = j i$
110	105 109	breqtrd	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to m ∥ j i$
111	100 84	gcdcomd	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to m \gcd N = N \gcd m$
112	63	simprbi	$⊢ m \in X \to m ∥ M$
113	61 112	syl	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to m ∥ M$
114		rpdvds	$⊢ ((N \in ℤ \land m \in ℤ \land M \in ℤ) \land (N \gcd M = 1 \land m ∥ M)) \to N \gcd m = 1$
115	84 100 86 91 113 114	syl32anc	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to N \gcd m = 1$
116	111 115	eqtrd	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to m \gcd N = 1$
117	32	adantr	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to j ∥ N$
118		rpdvds	$⊢ ((m \in ℤ \land j \in ℤ \land N \in ℤ) \land (m \gcd N = 1 \land j ∥ N)) \to m \gcd j = 1$
119	100 69 84 116 117 118	syl32anc	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to m \gcd j = 1$
120		coprmdvds	$⊢ (m \in ℤ \land j \in ℤ \land i \in ℤ) \to ((m ∥ j i \land m \gcd j = 1) \to m ∥ i)$
121	100 69 67 120	syl3anc	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to ((m ∥ j i \land m \gcd j = 1) \to m ∥ i)$
122	110 119 121	mp2and	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to m ∥ i$
123		dvdseq	$⊢ ((i \in ℕ_{0} \land m \in ℕ_{0}) \land (i ∥ m \land m ∥ i)) \to i = m$
124	60 66 103 122 123	syl22anc	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to i = m$
125	59	nnne0d	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to i \neq 0$
126	124	oveq1d	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to i n = m n$
127	72 126	eqtr4d	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to i j = i n$
128	107 79 106 125 127	mulcanad	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to j = n$
129	124 128	opeq12d	$⊢ ((φ \land (i \in X \land j \in Y)) \land ((m \in X \land n \in Y) \land i j = m n)) \to ⟨i, j⟩ = ⟨m, n⟩$
130	129	expr	$⊢ ((φ \land (i \in X \land j \in Y)) \land (m \in X \land n \in Y)) \to (i j = m n \to ⟨i, j⟩ = ⟨m, n⟩)$
131	130	ralrimivva	$⊢ (φ \land (i \in X \land j \in Y)) \to \forall m \in X \forall n \in Y (i j = m n \to ⟨i, j⟩ = ⟨m, n⟩)$
132	131	ralrimivva	$⊢ φ \to \forall i \in X \forall j \in Y \forall m \in X \forall n \in Y (i j = m n \to ⟨i, j⟩ = ⟨m, n⟩)$
133		fvres	$⊢ u \in (X \times Y) \to ({\times ↾}_{(X \times Y)}) (u) = \times (u)$
134		fvres	$⊢ v \in (X \times Y) \to ({\times ↾}_{(X \times Y)}) (v) = \times (v)$
135	133 134	eqeqan12d	$⊢ (u \in (X \times Y) \land v \in (X \times Y)) \to (({\times ↾}_{(X \times Y)}) (u) = ({\times ↾}_{(X \times Y)}) (v) \leftrightarrow \times (u) = \times (v))$
136	135	imbi1d	$⊢ (u \in (X \times Y) \land v \in (X \times Y)) \to ((({\times ↾}_{(X \times Y)}) (u) = ({\times ↾}_{(X \times Y)}) (v) \to u = v) \leftrightarrow (\times (u) = \times (v) \to u = v))$
137	136	ralbidva	$⊢ u \in (X \times Y) \to (\forall v \in (X \times Y) (({\times ↾}_{(X \times Y)}) (u) = ({\times ↾}_{(X \times Y)}) (v) \to u = v) \leftrightarrow \forall v \in (X \times Y) (\times (u) = \times (v) \to u = v))$
138	137	ralbiia	$⊢ \forall u \in (X \times Y) \forall v \in (X \times Y) (({\times ↾}_{(X \times Y)}) (u) = ({\times ↾}_{(X \times Y)}) (v) \to u = v) \leftrightarrow \forall u \in (X \times Y) \forall v \in (X \times Y) (\times (u) = \times (v) \to u = v)$
139		fveq2	$⊢ v = ⟨m, n⟩ \to \times (v) = \times (⟨m, n⟩)$
140		df-ov	$⊢ m n = \times (⟨m, n⟩)$
141	139 140	eqtr4di	$⊢ v = ⟨m, n⟩ \to \times (v) = m n$
142	141	eqeq2d	$⊢ v = ⟨m, n⟩ \to (\times (u) = \times (v) \leftrightarrow \times (u) = m n)$
143		eqeq2	$⊢ v = ⟨m, n⟩ \to (u = v \leftrightarrow u = ⟨m, n⟩)$
144	142 143	imbi12d	$⊢ v = ⟨m, n⟩ \to ((\times (u) = \times (v) \to u = v) \leftrightarrow (\times (u) = m n \to u = ⟨m, n⟩))$
145	144	ralxp	$⊢ \forall v \in (X \times Y) (\times (u) = \times (v) \to u = v) \leftrightarrow \forall m \in X \forall n \in Y (\times (u) = m n \to u = ⟨m, n⟩)$
146		fveq2	$⊢ u = ⟨i, j⟩ \to \times (u) = \times (⟨i, j⟩)$
147		df-ov	$⊢ i j = \times (⟨i, j⟩)$
148	146 147	eqtr4di	$⊢ u = ⟨i, j⟩ \to \times (u) = i j$
149	148	eqeq1d	$⊢ u = ⟨i, j⟩ \to (\times (u) = m n \leftrightarrow i j = m n)$
150		eqeq1	$⊢ u = ⟨i, j⟩ \to (u = ⟨m, n⟩ \leftrightarrow ⟨i, j⟩ = ⟨m, n⟩)$
151	149 150	imbi12d	$⊢ u = ⟨i, j⟩ \to ((\times (u) = m n \to u = ⟨m, n⟩) \leftrightarrow (i j = m n \to ⟨i, j⟩ = ⟨m, n⟩))$
152	151	2ralbidv	$⊢ u = ⟨i, j⟩ \to (\forall m \in X \forall n \in Y (\times (u) = m n \to u = ⟨m, n⟩) \leftrightarrow \forall m \in X \forall n \in Y (i j = m n \to ⟨i, j⟩ = ⟨m, n⟩))$
153	145 152	syl5bb	$⊢ u = ⟨i, j⟩ \to (\forall v \in (X \times Y) (\times (u) = \times (v) \to u = v) \leftrightarrow \forall m \in X \forall n \in Y (i j = m n \to ⟨i, j⟩ = ⟨m, n⟩))$
154	153	ralxp	$⊢ \forall u \in (X \times Y) \forall v \in (X \times Y) (\times (u) = \times (v) \to u = v) \leftrightarrow \forall i \in X \forall j \in Y \forall m \in X \forall n \in Y (i j = m n \to ⟨i, j⟩ = ⟨m, n⟩)$
155	138 154	bitri	$⊢ \forall u \in (X \times Y) \forall v \in (X \times Y) (({\times ↾}_{(X \times Y)}) (u) = ({\times ↾}_{(X \times Y)}) (v) \to u = v) \leftrightarrow \forall i \in X \forall j \in Y \forall m \in X \forall n \in Y (i j = m n \to ⟨i, j⟩ = ⟨m, n⟩)$
156	132 155	sylibr	$⊢ φ \to \forall u \in (X \times Y) \forall v \in (X \times Y) (({\times ↾}_{(X \times Y)}) (u) = ({\times ↾}_{(X \times Y)}) (v) \to u = v)$
157		dff13	$⊢ ({\times ↾}_{(X \times Y)}) : X \times Y \underset{1-1}{⟶} Z \leftrightarrow (({\times ↾}_{(X \times Y)}) : X \times Y ⟶ Z \land \forall u \in (X \times Y) \forall v \in (X \times Y) (({\times ↾}_{(X \times Y)}) (u) = ({\times ↾}_{(X \times Y)}) (v) \to u = v))$
158	58 156 157	sylanbrc	$⊢ φ \to ({\times ↾}_{(X \times Y)}) : X \times Y \underset{1-1}{⟶} Z$
159		breq1	$⊢ x = w \to (x ∥ M \cdot N \leftrightarrow w ∥ M \cdot N)$
160	159 6	elrab2	$⊢ w \in Z \leftrightarrow (w \in ℕ \land w ∥ M \cdot N)$
161	160	simplbi	$⊢ w \in Z \to w \in ℕ$
162	161	adantl	$⊢ (φ \land w \in Z) \to w \in ℕ$
163	162	nnzd	$⊢ (φ \land w \in Z) \to w \in ℤ$
164	1	adantr	$⊢ (φ \land w \in Z) \to M \in ℕ$
165	164	nnzd	$⊢ (φ \land w \in Z) \to M \in ℤ$
166	164	nnne0d	$⊢ (φ \land w \in Z) \to M \neq 0$
167		simpr	$⊢ (w = 0 \land M = 0) \to M = 0$
168	167	necon3ai	$⊢ M \neq 0 \to \neg (w = 0 \land M = 0)$
169	166 168	syl	$⊢ (φ \land w \in Z) \to \neg (w = 0 \land M = 0)$
170		gcdn0cl	$⊢ ((w \in ℤ \land M \in ℤ) \land \neg (w = 0 \land M = 0)) \to w \gcd M \in ℕ$
171	163 165 169 170	syl21anc	$⊢ (φ \land w \in Z) \to w \gcd M \in ℕ$
172		gcddvds	$⊢ (w \in ℤ \land M \in ℤ) \to ((w \gcd M) ∥ w \land (w \gcd M) ∥ M)$
173	163 165 172	syl2anc	$⊢ (φ \land w \in Z) \to ((w \gcd M) ∥ w \land (w \gcd M) ∥ M)$
174	173	simprd	$⊢ (φ \land w \in Z) \to (w \gcd M) ∥ M$
175		breq1	$⊢ x = w \gcd M \to (x ∥ M \leftrightarrow (w \gcd M) ∥ M)$
176	175 4	elrab2	$⊢ w \gcd M \in X \leftrightarrow (w \gcd M \in ℕ \land (w \gcd M) ∥ M)$
177	171 174 176	sylanbrc	$⊢ (φ \land w \in Z) \to w \gcd M \in X$
178	2	adantr	$⊢ (φ \land w \in Z) \to N \in ℕ$
179	178	nnzd	$⊢ (φ \land w \in Z) \to N \in ℤ$
180	178	nnne0d	$⊢ (φ \land w \in Z) \to N \neq 0$
181		simpr	$⊢ (w = 0 \land N = 0) \to N = 0$
182	181	necon3ai	$⊢ N \neq 0 \to \neg (w = 0 \land N = 0)$
183	180 182	syl	$⊢ (φ \land w \in Z) \to \neg (w = 0 \land N = 0)$
184		gcdn0cl	$⊢ ((w \in ℤ \land N \in ℤ) \land \neg (w = 0 \land N = 0)) \to w \gcd N \in ℕ$
185	163 179 183 184	syl21anc	$⊢ (φ \land w \in Z) \to w \gcd N \in ℕ$
186		gcddvds	$⊢ (w \in ℤ \land N \in ℤ) \to ((w \gcd N) ∥ w \land (w \gcd N) ∥ N)$
187	163 179 186	syl2anc	$⊢ (φ \land w \in Z) \to ((w \gcd N) ∥ w \land (w \gcd N) ∥ N)$
188	187	simprd	$⊢ (φ \land w \in Z) \to (w \gcd N) ∥ N$
189		breq1	$⊢ x = w \gcd N \to (x ∥ N \leftrightarrow (w \gcd N) ∥ N)$
190	189 5	elrab2	$⊢ w \gcd N \in Y \leftrightarrow (w \gcd N \in ℕ \land (w \gcd N) ∥ N)$
191	185 188 190	sylanbrc	$⊢ (φ \land w \in Z) \to w \gcd N \in Y$
192	177 191	opelxpd	$⊢ (φ \land w \in Z) \to ⟨w \gcd M, w \gcd N⟩ \in (X \times Y)$
193	192	fvresd	$⊢ (φ \land w \in Z) \to ({\times ↾}_{(X \times Y)}) (⟨w \gcd M, w \gcd N⟩) = \times (⟨w \gcd M, w \gcd N⟩)$
194	3	adantr	$⊢ (φ \land w \in Z) \to M \gcd N = 1$
195		rpmulgcd2	$⊢ ((w \in ℤ \land M \in ℤ \land N \in ℤ) \land M \gcd N = 1) \to w \gcd M \cdot N = (w \gcd M) (w \gcd N)$
196	163 165 179 194 195	syl31anc	$⊢ (φ \land w \in Z) \to w \gcd M \cdot N = (w \gcd M) (w \gcd N)$
197		df-ov	$⊢ (w \gcd M) (w \gcd N) = \times (⟨w \gcd M, w \gcd N⟩)$
198	196 197	eqtrdi	$⊢ (φ \land w \in Z) \to w \gcd M \cdot N = \times (⟨w \gcd M, w \gcd N⟩)$
199	160	simprbi	$⊢ w \in Z \to w ∥ M \cdot N$
200	199	adantl	$⊢ (φ \land w \in Z) \to w ∥ M \cdot N$
201	1 2	nnmulcld	$⊢ φ \to M \cdot N \in ℕ$
202		gcdeq	$⊢ (w \in ℕ \land M \cdot N \in ℕ) \to (w \gcd M \cdot N = w \leftrightarrow w ∥ M \cdot N)$
203	161 201 202	syl2anr	$⊢ (φ \land w \in Z) \to (w \gcd M \cdot N = w \leftrightarrow w ∥ M \cdot N)$
204	200 203	mpbird	$⊢ (φ \land w \in Z) \to w \gcd M \cdot N = w$
205	193 198 204	3eqtr2rd	$⊢ (φ \land w \in Z) \to w = ({\times ↾}_{(X \times Y)}) (⟨w \gcd M, w \gcd N⟩)$
206		fveq2	$⊢ u = ⟨w \gcd M, w \gcd N⟩ \to ({\times ↾}_{(X \times Y)}) (u) = ({\times ↾}_{(X \times Y)}) (⟨w \gcd M, w \gcd N⟩)$
207	206	rspceeqv	$⊢ (⟨w \gcd M, w \gcd N⟩ \in (X \times Y) \land w = ({\times ↾}_{(X \times Y)}) (⟨w \gcd M, w \gcd N⟩)) \to \exists u \in (X \times Y) w = ({\times ↾}_{(X \times Y)}) (u)$
208	192 205 207	syl2anc	$⊢ (φ \land w \in Z) \to \exists u \in (X \times Y) w = ({\times ↾}_{(X \times Y)}) (u)$
209	208	ralrimiva	$⊢ φ \to \forall w \in Z \exists u \in (X \times Y) w = ({\times ↾}_{(X \times Y)}) (u)$
210		dffo3	$⊢ ({\times ↾}_{(X \times Y)}) : X \times Y \underset{onto}{⟶} Z \leftrightarrow (({\times ↾}_{(X \times Y)}) : X \times Y ⟶ Z \land \forall w \in Z \exists u \in (X \times Y) w = ({\times ↾}_{(X \times Y)}) (u))$
211	58 209 210	sylanbrc	$⊢ φ \to ({\times ↾}_{(X \times Y)}) : X \times Y \underset{onto}{⟶} Z$
212		df-f1o	$⊢ ({\times ↾}_{(X \times Y)}) : X \times Y \underset{1-1 onto}{⟶} Z \leftrightarrow (({\times ↾}_{(X \times Y)}) : X \times Y \underset{1-1}{⟶} Z \land ({\times ↾}_{(X \times Y)}) : X \times Y \underset{onto}{⟶} Z)$
213	158 211 212	sylanbrc	$⊢ φ \to ({\times ↾}_{(X \times Y)}) : X \times Y \underset{1-1 onto}{⟶} Z$

Metamath Proof Explorer

Theorem dvdsmulf1o

Proof