This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑁 ) ∥ 𝐾 ) ) )