# 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 ${⊢}\left({M}\in ℕ\wedge {N}\in ℕ\right)\to \left(\left({M}\mathrm{lcm}{N}\right)\left({M}\mathrm{gcd}{N}\right)=\left|{M}\cdot {N}\right|\wedge \left(\left({K}\in ℕ\wedge \left({M}\parallel {K}\wedge {N}\parallel {K}\right)\right)\to \left({M}\mathrm{lcm}{N}\right)\parallel {K}\right)\right)$

### Proof

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