mpodvdsmulf1o

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 . Version of dvdsmulf1o using maps-to notation, which does not require ax-mulf . (Contributed by GG, 18-Apr-2025)

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

Proof

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

Metamath Proof Explorer

Theorem mpodvdsmulf1o

Proof