lcmgcdlem

Description: Lemma for lcmgcd and lcmdvds . Prove them for positive M , N , and K . (Contributed by Steve Rodriguez, 20-Jan-2020) (Proof shortened by AV, 16-Sep-2020)

		Ref	Expression
	Assertion	lcmgcdlem	$⊢ (M \in ℕ \land N \in ℕ) \to ((M lcm N) (M \gcd N) = \|M \cdot N\| \land ((K \in ℕ \land (M ∥ K \land N ∥ K)) \to (M lcm N) ∥ K))$

Proof

Step	Hyp	Ref	Expression
1		nnmulcl	$⊢ (M \in ℕ \land N \in ℕ) \to M \cdot N \in ℕ$
2	1	nnred	$⊢ (M \in ℕ \land N \in ℕ) \to M \cdot N \in ℝ$
3		nnz	$⊢ M \in ℕ \to M \in ℤ$
4	3	adantr	$⊢ (M \in ℕ \land N \in ℕ) \to M \in ℤ$
5	4	zred	$⊢ (M \in ℕ \land N \in ℕ) \to M \in ℝ$
6		nnz	$⊢ N \in ℕ \to N \in ℤ$
7	6	adantl	$⊢ (M \in ℕ \land N \in ℕ) \to N \in ℤ$
8	7	zred	$⊢ (M \in ℕ \land N \in ℕ) \to N \in ℝ$
9		0red	$⊢ M \in ℕ \to 0 \in ℝ$
10		nnre	$⊢ M \in ℕ \to M \in ℝ$
11		nngt0	$⊢ M \in ℕ \to 0 < M$
12	9 10 11	ltled	$⊢ M \in ℕ \to 0 \leq M$
13	12	adantr	$⊢ (M \in ℕ \land N \in ℕ) \to 0 \leq M$
14		0red	$⊢ N \in ℕ \to 0 \in ℝ$
15		nnre	$⊢ N \in ℕ \to N \in ℝ$
16		nngt0	$⊢ N \in ℕ \to 0 < N$
17	14 15 16	ltled	$⊢ N \in ℕ \to 0 \leq N$
18	17	adantl	$⊢ (M \in ℕ \land N \in ℕ) \to 0 \leq N$
19	5 8 13 18	mulge0d	$⊢ (M \in ℕ \land N \in ℕ) \to 0 \leq M \cdot N$
20	2 19	absidd	$⊢ (M \in ℕ \land N \in ℕ) \to \|M \cdot N\| = M \cdot N$
21	3 6	anim12i	$⊢ (M \in ℕ \land N \in ℕ) \to (M \in ℤ \land N \in ℤ)$
22		nnne0	$⊢ M \in ℕ \to M \neq 0$
23	22	neneqd	$⊢ M \in ℕ \to \neg M = 0$
24		nnne0	$⊢ N \in ℕ \to N \neq 0$
25	24	neneqd	$⊢ N \in ℕ \to \neg N = 0$
26	23 25	anim12i	$⊢ (M \in ℕ \land N \in ℕ) \to (\neg M = 0 \land \neg N = 0)$
27		ioran	$⊢ \neg (M = 0 \lor N = 0) \leftrightarrow (\neg M = 0 \land \neg N = 0)$
28	26 27	sylibr	$⊢ (M \in ℕ \land N \in ℕ) \to \neg (M = 0 \lor N = 0)$
29		lcmn0val	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \lor N = 0)) \to M lcm N = inf (\{x \in ℕ \| (M ∥ x \land N ∥ x)\} ℝ <)$
30	21 28 29	syl2anc	$⊢ (M \in ℕ \land N \in ℕ) \to M lcm N = inf (\{x \in ℕ \| (M ∥ x \land N ∥ x)\} ℝ <)$
31		ltso	$⊢ < Or ℝ$
32	31	a1i	$⊢ (M \in ℕ \land N \in ℕ) \to < Or ℝ$
33		gcddvds	$⊢ (M \in ℤ \land N \in ℤ) \to ((M \gcd N) ∥ M \land (M \gcd N) ∥ N)$
34	33	simpld	$⊢ (M \in ℤ \land N \in ℤ) \to (M \gcd N) ∥ M$
35		gcdcl	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N \in ℕ_{0}$
36	35	nn0zd	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N \in ℤ$
37		dvdsmultr1	$⊢ (M \gcd N \in ℤ \land M \in ℤ \land N \in ℤ) \to ((M \gcd N) ∥ M \to (M \gcd N) ∥ M \cdot N)$
38	37	3expb	$⊢ (M \gcd N \in ℤ \land (M \in ℤ \land N \in ℤ)) \to ((M \gcd N) ∥ M \to (M \gcd N) ∥ M \cdot N)$
39	36 38	mpancom	$⊢ (M \in ℤ \land N \in ℤ) \to ((M \gcd N) ∥ M \to (M \gcd N) ∥ M \cdot N)$
40	34 39	mpd	$⊢ (M \in ℤ \land N \in ℤ) \to (M \gcd N) ∥ M \cdot N$
41	21 40	syl	$⊢ (M \in ℕ \land N \in ℕ) \to (M \gcd N) ∥ M \cdot N$
42		gcdnncl	$⊢ (M \in ℕ \land N \in ℕ) \to M \gcd N \in ℕ$
43		nndivdvds	$⊢ (M \cdot N \in ℕ \land M \gcd N \in ℕ) \to ((M \gcd N) ∥ M \cdot N \leftrightarrow \frac{M \cdot N}{M \gcd N} \in ℕ)$
44	1 42 43	syl2anc	$⊢ (M \in ℕ \land N \in ℕ) \to ((M \gcd N) ∥ M \cdot N \leftrightarrow \frac{M \cdot N}{M \gcd N} \in ℕ)$
45	41 44	mpbid	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{M \cdot N}{M \gcd N} \in ℕ$
46	45	nnred	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{M \cdot N}{M \gcd N} \in ℝ$
47		breq2	$⊢ x = \frac{M \cdot N}{M \gcd N} \to (M ∥ x \leftrightarrow M ∥ (\frac{M \cdot N}{M \gcd N}))$
48		breq2	$⊢ x = \frac{M \cdot N}{M \gcd N} \to (N ∥ x \leftrightarrow N ∥ (\frac{M \cdot N}{M \gcd N}))$
49	47 48	anbi12d	$⊢ x = \frac{M \cdot N}{M \gcd N} \to ((M ∥ x \land N ∥ x) \leftrightarrow (M ∥ (\frac{M \cdot N}{M \gcd N}) \land N ∥ (\frac{M \cdot N}{M \gcd N})))$
50	33	simprd	$⊢ (M \in ℤ \land N \in ℤ) \to (M \gcd N) ∥ N$
51	21 50	syl	$⊢ (M \in ℕ \land N \in ℕ) \to (M \gcd N) ∥ N$
52	21 36	syl	$⊢ (M \in ℕ \land N \in ℕ) \to M \gcd N \in ℤ$
53	42	nnne0d	$⊢ (M \in ℕ \land N \in ℕ) \to M \gcd N \neq 0$
54		dvdsval2	$⊢ (M \gcd N \in ℤ \land M \gcd N \neq 0 \land N \in ℤ) \to ((M \gcd N) ∥ N \leftrightarrow \frac{N}{M \gcd N} \in ℤ)$
55	52 53 7 54	syl3anc	$⊢ (M \in ℕ \land N \in ℕ) \to ((M \gcd N) ∥ N \leftrightarrow \frac{N}{M \gcd N} \in ℤ)$
56	51 55	mpbid	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{N}{M \gcd N} \in ℤ$
57		dvdsmul1	$⊢ (M \in ℤ \land \frac{N}{M \gcd N} \in ℤ) \to M ∥ M (\frac{N}{M \gcd N})$
58	4 56 57	syl2anc	$⊢ (M \in ℕ \land N \in ℕ) \to M ∥ M (\frac{N}{M \gcd N})$
59		nncn	$⊢ M \in ℕ \to M \in ℂ$
60	59	adantr	$⊢ (M \in ℕ \land N \in ℕ) \to M \in ℂ$
61		nncn	$⊢ N \in ℕ \to N \in ℂ$
62	61	adantl	$⊢ (M \in ℕ \land N \in ℕ) \to N \in ℂ$
63	42	nncnd	$⊢ (M \in ℕ \land N \in ℕ) \to M \gcd N \in ℂ$
64	60 62 63 53	divassd	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{M \cdot N}{M \gcd N} = M (\frac{N}{M \gcd N})$
65	58 64	breqtrrd	$⊢ (M \in ℕ \land N \in ℕ) \to M ∥ (\frac{M \cdot N}{M \gcd N})$
66	21 34	syl	$⊢ (M \in ℕ \land N \in ℕ) \to (M \gcd N) ∥ M$
67		dvdsval2	$⊢ (M \gcd N \in ℤ \land M \gcd N \neq 0 \land M \in ℤ) \to ((M \gcd N) ∥ M \leftrightarrow \frac{M}{M \gcd N} \in ℤ)$
68	52 53 4 67	syl3anc	$⊢ (M \in ℕ \land N \in ℕ) \to ((M \gcd N) ∥ M \leftrightarrow \frac{M}{M \gcd N} \in ℤ)$
69	66 68	mpbid	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{M}{M \gcd N} \in ℤ$
70		dvdsmul1	$⊢ (N \in ℤ \land \frac{M}{M \gcd N} \in ℤ) \to N ∥ N (\frac{M}{M \gcd N})$
71	7 69 70	syl2anc	$⊢ (M \in ℕ \land N \in ℕ) \to N ∥ N (\frac{M}{M \gcd N})$
72	60 62	mulcomd	$⊢ (M \in ℕ \land N \in ℕ) \to M \cdot N = N \cdot M$
73	72	oveq1d	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{M \cdot N}{M \gcd N} = \frac{N \cdot M}{M \gcd N}$
74	62 60 63 53	divassd	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{N \cdot M}{M \gcd N} = N (\frac{M}{M \gcd N})$
75	73 74	eqtrd	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{M \cdot N}{M \gcd N} = N (\frac{M}{M \gcd N})$
76	71 75	breqtrrd	$⊢ (M \in ℕ \land N \in ℕ) \to N ∥ (\frac{M \cdot N}{M \gcd N})$
77	65 76	jca	$⊢ (M \in ℕ \land N \in ℕ) \to (M ∥ (\frac{M \cdot N}{M \gcd N}) \land N ∥ (\frac{M \cdot N}{M \gcd N}))$
78	49 45 77	elrabd	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{M \cdot N}{M \gcd N} \in \{x \in ℕ \| (M ∥ x \land N ∥ x)\}$
79	46	adantr	$⊢ ((M \in ℕ \land N \in ℕ) \land n \in \{x \in ℕ \| (M ∥ x \land N ∥ x)\}) \to \frac{M \cdot N}{M \gcd N} \in ℝ$
80		elrabi	$⊢ n \in \{x \in ℕ \| (M ∥ x \land N ∥ x)\} \to n \in ℕ$
81	80	nnred	$⊢ n \in \{x \in ℕ \| (M ∥ x \land N ∥ x)\} \to n \in ℝ$
82	81	adantl	$⊢ ((M \in ℕ \land N \in ℕ) \land n \in \{x \in ℕ \| (M ∥ x \land N ∥ x)\}) \to n \in ℝ$
83		breq2	$⊢ x = n \to (M ∥ x \leftrightarrow M ∥ n)$
84		breq2	$⊢ x = n \to (N ∥ x \leftrightarrow N ∥ n)$
85	83 84	anbi12d	$⊢ x = n \to ((M ∥ x \land N ∥ x) \leftrightarrow (M ∥ n \land N ∥ n))$
86	85	elrab	$⊢ n \in \{x \in ℕ \| (M ∥ x \land N ∥ x)\} \leftrightarrow (n \in ℕ \land (M ∥ n \land N ∥ n))$
87		bezout	$⊢ (M \in ℤ \land N \in ℤ) \to \exists x \in ℤ \exists y \in ℤ M \gcd N = M x + N y$
88	21 87	syl	$⊢ (M \in ℕ \land N \in ℕ) \to \exists x \in ℤ \exists y \in ℤ M \gcd N = M x + N y$
89	88	adantr	$⊢ ((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \to \exists x \in ℤ \exists y \in ℤ M \gcd N = M x + N y$
90		nncn	$⊢ n \in ℕ \to n \in ℂ$
91	90	ad2antlr	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to n \in ℂ$
92	1	nncnd	$⊢ (M \in ℕ \land N \in ℕ) \to M \cdot N \in ℂ$
93	92	ad2antrr	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to M \cdot N \in ℂ$
94	63	ad2antrr	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to M \gcd N \in ℂ$
95	60	ad2antrr	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to M \in ℂ$
96	61	ad3antlr	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to N \in ℂ$
97	22	ad3antrrr	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to M \neq 0$
98	24	ad3antlr	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to N \neq 0$
99	95 96 97 98	mulne0d	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to M \cdot N \neq 0$
100	53	ad2antrr	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to M \gcd N \neq 0$
101	91 93 94 99 100	divdiv2d	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to \frac{n}{\frac{M \cdot N}{M \gcd N}} = \frac{n (M \gcd N)}{M \cdot N}$
102	101	adantr	$⊢ ((((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \land M \gcd N = M x + N y) \to \frac{n}{\frac{M \cdot N}{M \gcd N}} = \frac{n (M \gcd N)}{M \cdot N}$
103		oveq2	$⊢ M \gcd N = M x + N y \to n (M \gcd N) = n (M x + N y)$
104	103	oveq1d	$⊢ M \gcd N = M x + N y \to \frac{n (M \gcd N)}{M \cdot N} = \frac{n (M x + N y)}{M \cdot N}$
105		zcn	$⊢ x \in ℤ \to x \in ℂ$
106	105	ad2antrl	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to x \in ℂ$
107	95 106	mulcld	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to M x \in ℂ$
108		zcn	$⊢ y \in ℤ \to y \in ℂ$
109	108	ad2antll	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to y \in ℂ$
110	96 109	mulcld	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to N y \in ℂ$
111	91 107 110	adddid	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to n (M x + N y) = n M x + n N y$
112	111	oveq1d	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to \frac{n (M x + N y)}{M \cdot N} = \frac{n M x + n N y}{M \cdot N}$
113	91 107	mulcld	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to n M x \in ℂ$
114	91 110	mulcld	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to n N y \in ℂ$
115	113 114 93 99	divdird	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to \frac{n M x + n N y}{M \cdot N} = (\frac{n M x}{M \cdot N}) + (\frac{n N y}{M \cdot N})$
116	112 115	eqtrd	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to \frac{n (M x + N y)}{M \cdot N} = (\frac{n M x}{M \cdot N}) + (\frac{n N y}{M \cdot N})$
117	104 116	sylan9eqr	$⊢ ((((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \land M \gcd N = M x + N y) \to \frac{n (M \gcd N)}{M \cdot N} = (\frac{n M x}{M \cdot N}) + (\frac{n N y}{M \cdot N})$
118	91 95 106	mul12d	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to n M x = M n x$
119	118	oveq1d	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to \frac{n M x}{M \cdot N} = \frac{M n x}{M \cdot N}$
120	91 106	mulcld	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to n x \in ℂ$
121	120 96 95 98 97	divcan5d	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to \frac{M n x}{M \cdot N} = \frac{n x}{N}$
122	119 121	eqtrd	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to \frac{n M x}{M \cdot N} = \frac{n x}{N}$
123	91 96 109	mul12d	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to n N y = N n y$
124	123	oveq1d	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to \frac{n N y}{M \cdot N} = \frac{N n y}{M \cdot N}$
125	72	ad2antrr	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to M \cdot N = N \cdot M$
126	125	oveq2d	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to \frac{N n y}{M \cdot N} = \frac{N n y}{N \cdot M}$
127	91 109	mulcld	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to n y \in ℂ$
128	127 95 96 97 98	divcan5d	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to \frac{N n y}{N \cdot M} = \frac{n y}{M}$
129	124 126 128	3eqtrd	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to \frac{n N y}{M \cdot N} = \frac{n y}{M}$
130	122 129	oveq12d	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to (\frac{n M x}{M \cdot N}) + (\frac{n N y}{M \cdot N}) = (\frac{n x}{N}) + (\frac{n y}{M})$
131	130	adantr	$⊢ ((((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \land M \gcd N = M x + N y) \to (\frac{n M x}{M \cdot N}) + (\frac{n N y}{M \cdot N}) = (\frac{n x}{N}) + (\frac{n y}{M})$
132	102 117 131	3eqtrd	$⊢ ((((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \land M \gcd N = M x + N y) \to \frac{n}{\frac{M \cdot N}{M \gcd N}} = (\frac{n x}{N}) + (\frac{n y}{M})$
133	132	ex	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to (M \gcd N = M x + N y \to \frac{n}{\frac{M \cdot N}{M \gcd N}} = (\frac{n x}{N}) + (\frac{n y}{M}))$
134	133	adantlrr	$⊢ (((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \land (x \in ℤ \land y \in ℤ)) \to (M \gcd N = M x + N y \to \frac{n}{\frac{M \cdot N}{M \gcd N}} = (\frac{n x}{N}) + (\frac{n y}{M}))$
135	134	imp	$⊢ ((((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \land (x \in ℤ \land y \in ℤ)) \land M \gcd N = M x + N y) \to \frac{n}{\frac{M \cdot N}{M \gcd N}} = (\frac{n x}{N}) + (\frac{n y}{M})$
136	6	ad3antlr	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to N \in ℤ$
137		nnz	$⊢ n \in ℕ \to n \in ℤ$
138	137	ad2antlr	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to n \in ℤ$
139		simprl	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to x \in ℤ$
140		dvdsmultr1	$⊢ (N \in ℤ \land n \in ℤ \land x \in ℤ) \to (N ∥ n \to N ∥ n x)$
141	136 138 139 140	syl3anc	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to (N ∥ n \to N ∥ n x)$
142	138 139	zmulcld	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to n x \in ℤ$
143		dvdsval2	$⊢ (N \in ℤ \land N \neq 0 \land n x \in ℤ) \to (N ∥ n x \leftrightarrow \frac{n x}{N} \in ℤ)$
144	136 98 142 143	syl3anc	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to (N ∥ n x \leftrightarrow \frac{n x}{N} \in ℤ)$
145	141 144	sylibd	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to (N ∥ n \to \frac{n x}{N} \in ℤ)$
146	145	adantld	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to ((M ∥ n \land N ∥ n) \to \frac{n x}{N} \in ℤ)$
147	146	3impia	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ) \land (M ∥ n \land N ∥ n)) \to \frac{n x}{N} \in ℤ$
148	3	ad3antrrr	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to M \in ℤ$
149		simprr	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to y \in ℤ$
150		dvdsmultr1	$⊢ (M \in ℤ \land n \in ℤ \land y \in ℤ) \to (M ∥ n \to M ∥ n y)$
151	148 138 149 150	syl3anc	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to (M ∥ n \to M ∥ n y)$
152	138 149	zmulcld	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to n y \in ℤ$
153		dvdsval2	$⊢ (M \in ℤ \land M \neq 0 \land n y \in ℤ) \to (M ∥ n y \leftrightarrow \frac{n y}{M} \in ℤ)$
154	148 97 152 153	syl3anc	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to (M ∥ n y \leftrightarrow \frac{n y}{M} \in ℤ)$
155	151 154	sylibd	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to (M ∥ n \to \frac{n y}{M} \in ℤ)$
156	155	adantrd	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to ((M ∥ n \land N ∥ n) \to \frac{n y}{M} \in ℤ)$
157	156	3impia	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ) \land (M ∥ n \land N ∥ n)) \to \frac{n y}{M} \in ℤ$
158	147 157	zaddcld	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ) \land (M ∥ n \land N ∥ n)) \to (\frac{n x}{N}) + (\frac{n y}{M}) \in ℤ$
159	158	3expia	$⊢ (((M \in ℕ \land N \in ℕ) \land n \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to ((M ∥ n \land N ∥ n) \to (\frac{n x}{N}) + (\frac{n y}{M}) \in ℤ)$
160	159	an32s	$⊢ (((M \in ℕ \land N \in ℕ) \land (x \in ℤ \land y \in ℤ)) \land n \in ℕ) \to ((M ∥ n \land N ∥ n) \to (\frac{n x}{N}) + (\frac{n y}{M}) \in ℤ)$
161	160	impr	$⊢ (((M \in ℕ \land N \in ℕ) \land (x \in ℤ \land y \in ℤ)) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \to (\frac{n x}{N}) + (\frac{n y}{M}) \in ℤ$
162	161	an32s	$⊢ (((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \land (x \in ℤ \land y \in ℤ)) \to (\frac{n x}{N}) + (\frac{n y}{M}) \in ℤ$
163	162	adantr	$⊢ ((((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \land (x \in ℤ \land y \in ℤ)) \land M \gcd N = M x + N y) \to (\frac{n x}{N}) + (\frac{n y}{M}) \in ℤ$
164	135 163	eqeltrd	$⊢ ((((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \land (x \in ℤ \land y \in ℤ)) \land M \gcd N = M x + N y) \to \frac{n}{\frac{M \cdot N}{M \gcd N}} \in ℤ$
165	45	nnzd	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{M \cdot N}{M \gcd N} \in ℤ$
166	165	ad2antrr	$⊢ (((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \land (x \in ℤ \land y \in ℤ)) \to \frac{M \cdot N}{M \gcd N} \in ℤ$
167	1	nnne0d	$⊢ (M \in ℕ \land N \in ℕ) \to M \cdot N \neq 0$
168	92 63 167 53	divne0d	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{M \cdot N}{M \gcd N} \neq 0$
169	168	ad2antrr	$⊢ (((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \land (x \in ℤ \land y \in ℤ)) \to \frac{M \cdot N}{M \gcd N} \neq 0$
170	138	adantlrr	$⊢ (((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \land (x \in ℤ \land y \in ℤ)) \to n \in ℤ$
171		dvdsval2	$⊢ (\frac{M \cdot N}{M \gcd N} \in ℤ \land \frac{M \cdot N}{M \gcd N} \neq 0 \land n \in ℤ) \to ((\frac{M \cdot N}{M \gcd N}) ∥ n \leftrightarrow \frac{n}{\frac{M \cdot N}{M \gcd N}} \in ℤ)$
172	166 169 170 171	syl3anc	$⊢ (((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \land (x \in ℤ \land y \in ℤ)) \to ((\frac{M \cdot N}{M \gcd N}) ∥ n \leftrightarrow \frac{n}{\frac{M \cdot N}{M \gcd N}} \in ℤ)$
173	172	adantr	$⊢ ((((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \land (x \in ℤ \land y \in ℤ)) \land M \gcd N = M x + N y) \to ((\frac{M \cdot N}{M \gcd N}) ∥ n \leftrightarrow \frac{n}{\frac{M \cdot N}{M \gcd N}} \in ℤ)$
174	164 173	mpbird	$⊢ ((((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \land (x \in ℤ \land y \in ℤ)) \land M \gcd N = M x + N y) \to (\frac{M \cdot N}{M \gcd N}) ∥ n$
175	174	ex	$⊢ (((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \land (x \in ℤ \land y \in ℤ)) \to (M \gcd N = M x + N y \to (\frac{M \cdot N}{M \gcd N}) ∥ n)$
176	175	reximdvva	$⊢ ((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \to (\exists x \in ℤ \exists y \in ℤ M \gcd N = M x + N y \to \exists x \in ℤ \exists y \in ℤ (\frac{M \cdot N}{M \gcd N}) ∥ n)$
177	89 176	mpd	$⊢ ((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \to \exists x \in ℤ \exists y \in ℤ (\frac{M \cdot N}{M \gcd N}) ∥ n$
178		1z	$⊢ 1 \in ℤ$
179		ne0i	$⊢ 1 \in ℤ \to ℤ \neq \emptyset$
180		r19.9rzv	$⊢ ℤ \neq \emptyset \to ((\frac{M \cdot N}{M \gcd N}) ∥ n \leftrightarrow \exists y \in ℤ (\frac{M \cdot N}{M \gcd N}) ∥ n)$
181	178 179 180	mp2b	$⊢ (\frac{M \cdot N}{M \gcd N}) ∥ n \leftrightarrow \exists y \in ℤ (\frac{M \cdot N}{M \gcd N}) ∥ n$
182		r19.9rzv	$⊢ ℤ \neq \emptyset \to (\exists y \in ℤ (\frac{M \cdot N}{M \gcd N}) ∥ n \leftrightarrow \exists x \in ℤ \exists y \in ℤ (\frac{M \cdot N}{M \gcd N}) ∥ n)$
183	178 179 182	mp2b	$⊢ \exists y \in ℤ (\frac{M \cdot N}{M \gcd N}) ∥ n \leftrightarrow \exists x \in ℤ \exists y \in ℤ (\frac{M \cdot N}{M \gcd N}) ∥ n$
184	181 183	bitri	$⊢ (\frac{M \cdot N}{M \gcd N}) ∥ n \leftrightarrow \exists x \in ℤ \exists y \in ℤ (\frac{M \cdot N}{M \gcd N}) ∥ n$
185	177 184	sylibr	$⊢ ((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \to (\frac{M \cdot N}{M \gcd N}) ∥ n$
186	165	adantr	$⊢ ((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \to \frac{M \cdot N}{M \gcd N} \in ℤ$
187		simprl	$⊢ ((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \to n \in ℕ$
188		dvdsle	$⊢ (\frac{M \cdot N}{M \gcd N} \in ℤ \land n \in ℕ) \to ((\frac{M \cdot N}{M \gcd N}) ∥ n \to \frac{M \cdot N}{M \gcd N} \leq n)$
189	186 187 188	syl2anc	$⊢ ((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \to ((\frac{M \cdot N}{M \gcd N}) ∥ n \to \frac{M \cdot N}{M \gcd N} \leq n)$
190	185 189	mpd	$⊢ ((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \to \frac{M \cdot N}{M \gcd N} \leq n$
191	86 190	sylan2b	$⊢ ((M \in ℕ \land N \in ℕ) \land n \in \{x \in ℕ \| (M ∥ x \land N ∥ x)\}) \to \frac{M \cdot N}{M \gcd N} \leq n$
192	79 82 191	lensymd	$⊢ ((M \in ℕ \land N \in ℕ) \land n \in \{x \in ℕ \| (M ∥ x \land N ∥ x)\}) \to \neg n < \frac{M \cdot N}{M \gcd N}$
193	32 46 78 192	infmin	$⊢ (M \in ℕ \land N \in ℕ) \to inf (\{x \in ℕ \| (M ∥ x \land N ∥ x)\} ℝ <) = \frac{M \cdot N}{M \gcd N}$
194	30 193	eqtr2d	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{M \cdot N}{M \gcd N} = M lcm N$
195	194 45	eqeltrrd	$⊢ (M \in ℕ \land N \in ℕ) \to M lcm N \in ℕ$
196	195	nncnd	$⊢ (M \in ℕ \land N \in ℕ) \to M lcm N \in ℂ$
197	92 196 63 53	divmul3d	$⊢ (M \in ℕ \land N \in ℕ) \to (\frac{M \cdot N}{M \gcd N} = M lcm N \leftrightarrow M \cdot N = (M lcm N) (M \gcd N))$
198	194 197	mpbid	$⊢ (M \in ℕ \land N \in ℕ) \to M \cdot N = (M lcm N) (M \gcd N)$
199	20 198	eqtr2d	$⊢ (M \in ℕ \land N \in ℕ) \to (M lcm N) (M \gcd N) = \|M \cdot N\|$
200		simprl	$⊢ ((M \in ℕ \land N \in ℕ) \land (K \in ℕ \land (M ∥ K \land N ∥ K))) \to K \in ℕ$
201		eleq1	$⊢ n = K \to (n \in ℕ \leftrightarrow K \in ℕ)$
202		breq2	$⊢ n = K \to (M ∥ n \leftrightarrow M ∥ K)$
203		breq2	$⊢ n = K \to (N ∥ n \leftrightarrow N ∥ K)$
204	202 203	anbi12d	$⊢ n = K \to ((M ∥ n \land N ∥ n) \leftrightarrow (M ∥ K \land N ∥ K))$
205	201 204	anbi12d	$⊢ n = K \to ((n \in ℕ \land (M ∥ n \land N ∥ n)) \leftrightarrow (K \in ℕ \land (M ∥ K \land N ∥ K)))$
206	205	anbi2d	$⊢ n = K \to (((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \leftrightarrow ((M \in ℕ \land N \in ℕ) \land (K \in ℕ \land (M ∥ K \land N ∥ K))))$
207		breq2	$⊢ n = K \to ((M lcm N) ∥ n \leftrightarrow (M lcm N) ∥ K)$
208	206 207	imbi12d	$⊢ n = K \to ((((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \to (M lcm N) ∥ n) \leftrightarrow (((M \in ℕ \land N \in ℕ) \land (K \in ℕ \land (M ∥ K \land N ∥ K))) \to (M lcm N) ∥ K))$
209	194	breq1d	$⊢ (M \in ℕ \land N \in ℕ) \to ((\frac{M \cdot N}{M \gcd N}) ∥ n \leftrightarrow (M lcm N) ∥ n)$
210	209	adantr	$⊢ ((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \to ((\frac{M \cdot N}{M \gcd N}) ∥ n \leftrightarrow (M lcm N) ∥ n)$
211	185 210	mpbid	$⊢ ((M \in ℕ \land N \in ℕ) \land (n \in ℕ \land (M ∥ n \land N ∥ n))) \to (M lcm N) ∥ n$
212	208 211	vtoclg	$⊢ K \in ℕ \to (((M \in ℕ \land N \in ℕ) \land (K \in ℕ \land (M ∥ K \land N ∥ K))) \to (M lcm N) ∥ K)$
213	200 212	mpcom	$⊢ ((M \in ℕ \land N \in ℕ) \land (K \in ℕ \land (M ∥ K \land N ∥ K))) \to (M lcm N) ∥ K$
214	213	ex	$⊢ (M \in ℕ \land N \in ℕ) \to ((K \in ℕ \land (M ∥ K \land N ∥ K)) \to (M lcm N) ∥ K)$
215	199 214	jca	$⊢ (M \in ℕ \land N \in ℕ) \to ((M lcm N) (M \gcd N) = \|M \cdot N\| \land ((K \in ℕ \land (M ∥ K \land N ∥ K)) \to (M lcm N) ∥ K))$

Metamath Proof Explorer

Theorem lcmgcdlem

Proof