Theorem 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	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑀 lcm 𝑁 ) · ( 𝑀 gcd 𝑁 ) ) = ( abs ‘ ( 𝑀 · 𝑁 ) ) ∧ ( ( 𝐾 ∈ ℕ ∧ ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) ) → ( 𝑀 lcm 𝑁 ) ∥ 𝐾 ) ) )

Proof

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