# Metamath Proof Explorer

## Theorem dfgcd2

Description: Alternate definition of the gcd operator, see definition in ApostolNT p. 15. (Contributed by AV, 8-Aug-2021)

Ref Expression
Assertion dfgcd2 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({D}={M}\mathrm{gcd}{N}↔\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 gcdcl ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}\mathrm{gcd}{N}\in {ℕ}_{0}$
2 1 nn0ge0d ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to 0\le {M}\mathrm{gcd}{N}$
3 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)$
4 3anass ${⊢}\left({e}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)↔\left({e}\in ℤ\wedge \left({M}\in ℤ\wedge {N}\in ℤ\right)\right)$
5 4 biancomi ${⊢}\left({e}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)↔\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge {e}\in ℤ\right)$
6 dvdsgcd ${⊢}\left({e}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel \left({M}\mathrm{gcd}{N}\right)\right)$
7 5 6 sylbir ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge {e}\in ℤ\right)\to \left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel \left({M}\mathrm{gcd}{N}\right)\right)$
8 7 ralrimiva ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel \left({M}\mathrm{gcd}{N}\right)\right)$
9 2 3 8 3jca ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left(0\le {M}\mathrm{gcd}{N}\wedge \left(\left({M}\mathrm{gcd}{N}\right)\parallel {M}\wedge \left({M}\mathrm{gcd}{N}\right)\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel \left({M}\mathrm{gcd}{N}\right)\right)\right)$
10 9 adantr ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge {D}={M}\mathrm{gcd}{N}\right)\to \left(0\le {M}\mathrm{gcd}{N}\wedge \left(\left({M}\mathrm{gcd}{N}\right)\parallel {M}\wedge \left({M}\mathrm{gcd}{N}\right)\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel \left({M}\mathrm{gcd}{N}\right)\right)\right)$
11 breq2 ${⊢}{D}={M}\mathrm{gcd}{N}\to \left(0\le {D}↔0\le {M}\mathrm{gcd}{N}\right)$
12 breq1 ${⊢}{D}={M}\mathrm{gcd}{N}\to \left({D}\parallel {M}↔\left({M}\mathrm{gcd}{N}\right)\parallel {M}\right)$
13 breq1 ${⊢}{D}={M}\mathrm{gcd}{N}\to \left({D}\parallel {N}↔\left({M}\mathrm{gcd}{N}\right)\parallel {N}\right)$
14 12 13 anbi12d ${⊢}{D}={M}\mathrm{gcd}{N}\to \left(\left({D}\parallel {M}\wedge {D}\parallel {N}\right)↔\left(\left({M}\mathrm{gcd}{N}\right)\parallel {M}\wedge \left({M}\mathrm{gcd}{N}\right)\parallel {N}\right)\right)$
15 breq2 ${⊢}{D}={M}\mathrm{gcd}{N}\to \left({e}\parallel {D}↔{e}\parallel \left({M}\mathrm{gcd}{N}\right)\right)$
16 15 imbi2d ${⊢}{D}={M}\mathrm{gcd}{N}\to \left(\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)↔\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel \left({M}\mathrm{gcd}{N}\right)\right)\right)$
17 16 ralbidv ${⊢}{D}={M}\mathrm{gcd}{N}\to \left(\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)↔\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel \left({M}\mathrm{gcd}{N}\right)\right)\right)$
18 11 14 17 3anbi123d ${⊢}{D}={M}\mathrm{gcd}{N}\to \left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)↔\left(0\le {M}\mathrm{gcd}{N}\wedge \left(\left({M}\mathrm{gcd}{N}\right)\parallel {M}\wedge \left({M}\mathrm{gcd}{N}\right)\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel \left({M}\mathrm{gcd}{N}\right)\right)\right)\right)$
19 18 adantl ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge {D}={M}\mathrm{gcd}{N}\right)\to \left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)↔\left(0\le {M}\mathrm{gcd}{N}\wedge \left(\left({M}\mathrm{gcd}{N}\right)\parallel {M}\wedge \left({M}\mathrm{gcd}{N}\right)\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel \left({M}\mathrm{gcd}{N}\right)\right)\right)\right)$
20 10 19 mpbird ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge {D}={M}\mathrm{gcd}{N}\right)\to \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)$
21 gcdval ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}\mathrm{gcd}{N}=if\left(\left({M}=0\wedge {N}=0\right),0,sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)\right)$
22 21 adantr ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\to {M}\mathrm{gcd}{N}=if\left(\left({M}=0\wedge {N}=0\right),0,sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)\right)$
23 iftrue ${⊢}\left({M}=0\wedge {N}=0\right)\to if\left(\left({M}=0\wedge {N}=0\right),0,sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)\right)=0$
24 23 adantr ${⊢}\left(\left({M}=0\wedge {N}=0\right)\wedge \left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\right)\to if\left(\left({M}=0\wedge {N}=0\right),0,sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)\right)=0$
25 breq2 ${⊢}{M}=0\to \left({D}\parallel {M}↔{D}\parallel 0\right)$
26 breq2 ${⊢}{N}=0\to \left({D}\parallel {N}↔{D}\parallel 0\right)$
27 25 26 bi2anan9 ${⊢}\left({M}=0\wedge {N}=0\right)\to \left(\left({D}\parallel {M}\wedge {D}\parallel {N}\right)↔\left({D}\parallel 0\wedge {D}\parallel 0\right)\right)$
28 breq2 ${⊢}{M}=0\to \left({e}\parallel {M}↔{e}\parallel 0\right)$
29 breq2 ${⊢}{N}=0\to \left({e}\parallel {N}↔{e}\parallel 0\right)$
30 28 29 bi2anan9 ${⊢}\left({M}=0\wedge {N}=0\right)\to \left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)↔\left({e}\parallel 0\wedge {e}\parallel 0\right)\right)$
31 30 imbi1d ${⊢}\left({M}=0\wedge {N}=0\right)\to \left(\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)↔\left(\left({e}\parallel 0\wedge {e}\parallel 0\right)\to {e}\parallel {D}\right)\right)$
32 31 ralbidv ${⊢}\left({M}=0\wedge {N}=0\right)\to \left(\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)↔\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel 0\wedge {e}\parallel 0\right)\to {e}\parallel {D}\right)\right)$
33 27 32 3anbi23d ${⊢}\left({M}=0\wedge {N}=0\right)\to \left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)↔\left(0\le {D}\wedge \left({D}\parallel 0\wedge {D}\parallel 0\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel 0\wedge {e}\parallel 0\right)\to {e}\parallel {D}\right)\right)\right)$
34 dvdszrcl ${⊢}{D}\parallel 0\to \left({D}\in ℤ\wedge 0\in ℤ\right)$
35 dvds0 ${⊢}{e}\in ℤ\to {e}\parallel 0$
36 35 35 jca ${⊢}{e}\in ℤ\to \left({e}\parallel 0\wedge {e}\parallel 0\right)$
37 36 adantl ${⊢}\left(\left({D}\in ℤ\wedge 0\le {D}\right)\wedge {e}\in ℤ\right)\to \left({e}\parallel 0\wedge {e}\parallel 0\right)$
38 pm5.5 ${⊢}\left({e}\parallel 0\wedge {e}\parallel 0\right)\to \left(\left(\left({e}\parallel 0\wedge {e}\parallel 0\right)\to {e}\parallel {D}\right)↔{e}\parallel {D}\right)$
39 37 38 syl ${⊢}\left(\left({D}\in ℤ\wedge 0\le {D}\right)\wedge {e}\in ℤ\right)\to \left(\left(\left({e}\parallel 0\wedge {e}\parallel 0\right)\to {e}\parallel {D}\right)↔{e}\parallel {D}\right)$
40 39 ralbidva ${⊢}\left({D}\in ℤ\wedge 0\le {D}\right)\to \left(\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel 0\wedge {e}\parallel 0\right)\to {e}\parallel {D}\right)↔\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}{e}\parallel {D}\right)$
41 0z ${⊢}0\in ℤ$
42 breq1 ${⊢}{e}=0\to \left({e}\parallel {D}↔0\parallel {D}\right)$
43 42 rspcv ${⊢}0\in ℤ\to \left(\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}{e}\parallel {D}\to 0\parallel {D}\right)$
44 41 43 ax-mp ${⊢}\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}{e}\parallel {D}\to 0\parallel {D}$
45 0dvds ${⊢}{D}\in ℤ\to \left(0\parallel {D}↔{D}=0\right)$
46 45 biimpd ${⊢}{D}\in ℤ\to \left(0\parallel {D}\to {D}=0\right)$
47 eqcom ${⊢}0={D}↔{D}=0$
48 46 47 syl6ibr ${⊢}{D}\in ℤ\to \left(0\parallel {D}\to 0={D}\right)$
49 44 48 syl5 ${⊢}{D}\in ℤ\to \left(\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}{e}\parallel {D}\to 0={D}\right)$
50 49 adantr ${⊢}\left({D}\in ℤ\wedge 0\le {D}\right)\to \left(\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}{e}\parallel {D}\to 0={D}\right)$
51 40 50 sylbid ${⊢}\left({D}\in ℤ\wedge 0\le {D}\right)\to \left(\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel 0\wedge {e}\parallel 0\right)\to {e}\parallel {D}\right)\to 0={D}\right)$
52 51 ex ${⊢}{D}\in ℤ\to \left(0\le {D}\to \left(\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel 0\wedge {e}\parallel 0\right)\to {e}\parallel {D}\right)\to 0={D}\right)\right)$
53 52 adantr ${⊢}\left({D}\in ℤ\wedge 0\in ℤ\right)\to \left(0\le {D}\to \left(\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel 0\wedge {e}\parallel 0\right)\to {e}\parallel {D}\right)\to 0={D}\right)\right)$
54 34 53 syl ${⊢}{D}\parallel 0\to \left(0\le {D}\to \left(\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel 0\wedge {e}\parallel 0\right)\to {e}\parallel {D}\right)\to 0={D}\right)\right)$
55 54 adantr ${⊢}\left({D}\parallel 0\wedge {D}\parallel 0\right)\to \left(0\le {D}\to \left(\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel 0\wedge {e}\parallel 0\right)\to {e}\parallel {D}\right)\to 0={D}\right)\right)$
56 55 3imp21 ${⊢}\left(0\le {D}\wedge \left({D}\parallel 0\wedge {D}\parallel 0\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel 0\wedge {e}\parallel 0\right)\to {e}\parallel {D}\right)\right)\to 0={D}$
57 33 56 syl6bi ${⊢}\left({M}=0\wedge {N}=0\right)\to \left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\to 0={D}\right)$
58 57 adantld ${⊢}\left({M}=0\wedge {N}=0\right)\to \left(\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\to 0={D}\right)$
59 58 imp ${⊢}\left(\left({M}=0\wedge {N}=0\right)\wedge \left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\right)\to 0={D}$
60 24 59 eqtrd ${⊢}\left(\left({M}=0\wedge {N}=0\right)\wedge \left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\right)\to if\left(\left({M}=0\wedge {N}=0\right),0,sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)\right)={D}$
61 iffalse ${⊢}¬\left({M}=0\wedge {N}=0\right)\to if\left(\left({M}=0\wedge {N}=0\right),0,sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)\right)=sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)$
62 61 adantr ${⊢}\left(¬\left({M}=0\wedge {N}=0\right)\wedge \left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\right)\to if\left(\left({M}=0\wedge {N}=0\right),0,sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)\right)=sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)$
63 ltso ${⊢}<\mathrm{Or}ℝ$
64 63 a1i ${⊢}\left(¬\left({M}=0\wedge {N}=0\right)\wedge \left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\right)\to <\mathrm{Or}ℝ$
65 dvdszrcl ${⊢}{D}\parallel {M}\to \left({D}\in ℤ\wedge {M}\in ℤ\right)$
66 65 simpld ${⊢}{D}\parallel {M}\to {D}\in ℤ$
67 66 zred ${⊢}{D}\parallel {M}\to {D}\in ℝ$
68 67 adantr ${⊢}\left({D}\parallel {M}\wedge {D}\parallel {N}\right)\to {D}\in ℝ$
69 68 3ad2ant2 ${⊢}\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\to {D}\in ℝ$
70 69 ad2antll ${⊢}\left(¬\left({M}=0\wedge {N}=0\right)\wedge \left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\right)\to {D}\in ℝ$
71 breq1 ${⊢}{n}={y}\to \left({n}\parallel {M}↔{y}\parallel {M}\right)$
72 breq1 ${⊢}{n}={y}\to \left({n}\parallel {N}↔{y}\parallel {N}\right)$
73 71 72 anbi12d ${⊢}{n}={y}\to \left(\left({n}\parallel {M}\wedge {n}\parallel {N}\right)↔\left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)$
74 73 elrab ${⊢}{y}\in \left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\}↔\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)$
75 breq1 ${⊢}{e}={y}\to \left({e}\parallel {M}↔{y}\parallel {M}\right)$
76 breq1 ${⊢}{e}={y}\to \left({e}\parallel {N}↔{y}\parallel {N}\right)$
77 75 76 anbi12d ${⊢}{e}={y}\to \left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)↔\left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)$
78 breq1 ${⊢}{e}={y}\to \left({e}\parallel {D}↔{y}\parallel {D}\right)$
79 77 78 imbi12d ${⊢}{e}={y}\to \left(\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)↔\left(\left({y}\parallel {M}\wedge {y}\parallel {N}\right)\to {y}\parallel {D}\right)\right)$
80 79 rspcv ${⊢}{y}\in ℤ\to \left(\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\to \left(\left({y}\parallel {M}\wedge {y}\parallel {N}\right)\to {y}\parallel {D}\right)\right)$
81 80 com23 ${⊢}{y}\in ℤ\to \left(\left({y}\parallel {M}\wedge {y}\parallel {N}\right)\to \left(\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\to {y}\parallel {D}\right)\right)$
82 81 imp ${⊢}\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\to \left(\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\to {y}\parallel {D}\right)$
83 82 ad2antrr ${⊢}\left(\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\wedge \left({M}\in ℤ\wedge {N}\in ℤ\right)\right)\to \left(\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\to {y}\parallel {D}\right)$
84 elnn0z ${⊢}{D}\in {ℕ}_{0}↔\left({D}\in ℤ\wedge 0\le {D}\right)$
85 84 simplbi2 ${⊢}{D}\in ℤ\to \left(0\le {D}\to {D}\in {ℕ}_{0}\right)$
86 85 adantr ${⊢}\left({D}\in ℤ\wedge {M}\in ℤ\right)\to \left(0\le {D}\to {D}\in {ℕ}_{0}\right)$
87 65 86 syl ${⊢}{D}\parallel {M}\to \left(0\le {D}\to {D}\in {ℕ}_{0}\right)$
88 87 adantr ${⊢}\left({D}\parallel {M}\wedge {D}\parallel {N}\right)\to \left(0\le {D}\to {D}\in {ℕ}_{0}\right)$
89 88 impcom ${⊢}\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\to {D}\in {ℕ}_{0}$
90 simp-4l ${⊢}\left(\left(\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\wedge {D}\in {ℕ}_{0}\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\right)\to {y}\in ℤ$
91 elnn0 ${⊢}{D}\in {ℕ}_{0}↔\left({D}\in ℕ\vee {D}=0\right)$
92 2a1 ${⊢}{D}\in ℕ\to \left(\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to \left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\to {D}\in ℕ\right)\right)$
93 breq1 ${⊢}{D}=0\to \left({D}\parallel {M}↔0\parallel {M}\right)$
94 breq1 ${⊢}{D}=0\to \left({D}\parallel {N}↔0\parallel {N}\right)$
95 93 94 anbi12d ${⊢}{D}=0\to \left(\left({D}\parallel {M}\wedge {D}\parallel {N}\right)↔\left(0\parallel {M}\wedge 0\parallel {N}\right)\right)$
96 95 anbi2d ${⊢}{D}=0\to \left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)↔\left(0\le {D}\wedge \left(0\parallel {M}\wedge 0\parallel {N}\right)\right)\right)$
97 96 adantr ${⊢}\left({D}=0\wedge \left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\right)\to \left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)↔\left(0\le {D}\wedge \left(0\parallel {M}\wedge 0\parallel {N}\right)\right)\right)$
98 ianor ${⊢}¬\left({M}=0\wedge {N}=0\right)↔\left(¬{M}=0\vee ¬{N}=0\right)$
99 dvdszrcl ${⊢}0\parallel {M}\to \left(0\in ℤ\wedge {M}\in ℤ\right)$
100 0dvds ${⊢}{M}\in ℤ\to \left(0\parallel {M}↔{M}=0\right)$
101 pm2.24 ${⊢}{M}=0\to \left(¬{M}=0\to {D}\in ℕ\right)$
102 100 101 syl6bi ${⊢}{M}\in ℤ\to \left(0\parallel {M}\to \left(¬{M}=0\to {D}\in ℕ\right)\right)$
103 102 adantl ${⊢}\left(0\in ℤ\wedge {M}\in ℤ\right)\to \left(0\parallel {M}\to \left(¬{M}=0\to {D}\in ℕ\right)\right)$
104 99 103 mpcom ${⊢}0\parallel {M}\to \left(¬{M}=0\to {D}\in ℕ\right)$
105 104 adantr ${⊢}\left(0\parallel {M}\wedge 0\parallel {N}\right)\to \left(¬{M}=0\to {D}\in ℕ\right)$
106 105 com12 ${⊢}¬{M}=0\to \left(\left(0\parallel {M}\wedge 0\parallel {N}\right)\to {D}\in ℕ\right)$
107 dvdszrcl ${⊢}0\parallel {N}\to \left(0\in ℤ\wedge {N}\in ℤ\right)$
108 0dvds ${⊢}{N}\in ℤ\to \left(0\parallel {N}↔{N}=0\right)$
109 pm2.24 ${⊢}{N}=0\to \left(¬{N}=0\to {D}\in ℕ\right)$
110 108 109 syl6bi ${⊢}{N}\in ℤ\to \left(0\parallel {N}\to \left(¬{N}=0\to {D}\in ℕ\right)\right)$
111 110 adantl ${⊢}\left(0\in ℤ\wedge {N}\in ℤ\right)\to \left(0\parallel {N}\to \left(¬{N}=0\to {D}\in ℕ\right)\right)$
112 107 111 mpcom ${⊢}0\parallel {N}\to \left(¬{N}=0\to {D}\in ℕ\right)$
113 112 adantl ${⊢}\left(0\parallel {M}\wedge 0\parallel {N}\right)\to \left(¬{N}=0\to {D}\in ℕ\right)$
114 113 com12 ${⊢}¬{N}=0\to \left(\left(0\parallel {M}\wedge 0\parallel {N}\right)\to {D}\in ℕ\right)$
115 106 114 jaoi ${⊢}\left(¬{M}=0\vee ¬{N}=0\right)\to \left(\left(0\parallel {M}\wedge 0\parallel {N}\right)\to {D}\in ℕ\right)$
116 98 115 sylbi ${⊢}¬\left({M}=0\wedge {N}=0\right)\to \left(\left(0\parallel {M}\wedge 0\parallel {N}\right)\to {D}\in ℕ\right)$
117 116 adantld ${⊢}¬\left({M}=0\wedge {N}=0\right)\to \left(\left(0\le {D}\wedge \left(0\parallel {M}\wedge 0\parallel {N}\right)\right)\to {D}\in ℕ\right)$
118 117 ad2antll ${⊢}\left({D}=0\wedge \left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\right)\to \left(\left(0\le {D}\wedge \left(0\parallel {M}\wedge 0\parallel {N}\right)\right)\to {D}\in ℕ\right)$
119 97 118 sylbid ${⊢}\left({D}=0\wedge \left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\right)\to \left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\to {D}\in ℕ\right)$
120 119 ex ${⊢}{D}=0\to \left(\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to \left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\to {D}\in ℕ\right)\right)$
121 92 120 jaoi ${⊢}\left({D}\in ℕ\vee {D}=0\right)\to \left(\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to \left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\to {D}\in ℕ\right)\right)$
122 91 121 sylbi ${⊢}{D}\in {ℕ}_{0}\to \left(\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to \left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\to {D}\in ℕ\right)\right)$
123 122 impcom ${⊢}\left(\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\wedge {D}\in {ℕ}_{0}\right)\to \left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\to {D}\in ℕ\right)$
124 123 imp ${⊢}\left(\left(\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\wedge {D}\in {ℕ}_{0}\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\right)\to {D}\in ℕ$
125 dvdsle ${⊢}\left({y}\in ℤ\wedge {D}\in ℕ\right)\to \left({y}\parallel {D}\to {y}\le {D}\right)$
126 90 124 125 syl2anc ${⊢}\left(\left(\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\wedge {D}\in {ℕ}_{0}\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\right)\to \left({y}\parallel {D}\to {y}\le {D}\right)$
127 126 exp31 ${⊢}\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to \left({D}\in {ℕ}_{0}\to \left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\to \left({y}\parallel {D}\to {y}\le {D}\right)\right)\right)$
128 127 com14 ${⊢}{y}\parallel {D}\to \left({D}\in {ℕ}_{0}\to \left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\to \left(\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to {y}\le {D}\right)\right)\right)$
129 128 imp ${⊢}\left({y}\parallel {D}\wedge {D}\in {ℕ}_{0}\right)\to \left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\to \left(\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to {y}\le {D}\right)\right)$
130 129 impcom ${⊢}\left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\wedge \left({y}\parallel {D}\wedge {D}\in {ℕ}_{0}\right)\right)\to \left(\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to {y}\le {D}\right)$
131 130 imp ${⊢}\left(\left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\wedge \left({y}\parallel {D}\wedge {D}\in {ℕ}_{0}\right)\right)\wedge \left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\right)\to {y}\le {D}$
132 zre ${⊢}{y}\in ℤ\to {y}\in ℝ$
133 132 ad2antrr ${⊢}\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to {y}\in ℝ$
134 68 ad2antlr ${⊢}\left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\wedge \left({y}\parallel {D}\wedge {D}\in {ℕ}_{0}\right)\right)\to {D}\in ℝ$
135 lenlt ${⊢}\left({y}\in ℝ\wedge {D}\in ℝ\right)\to \left({y}\le {D}↔¬{D}<{y}\right)$
136 133 134 135 syl2anr ${⊢}\left(\left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\wedge \left({y}\parallel {D}\wedge {D}\in {ℕ}_{0}\right)\right)\wedge \left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\right)\to \left({y}\le {D}↔¬{D}<{y}\right)$
137 131 136 mpbid ${⊢}\left(\left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\wedge \left({y}\parallel {D}\wedge {D}\in {ℕ}_{0}\right)\right)\wedge \left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\right)\to ¬{D}<{y}$
138 137 exp31 ${⊢}\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\to \left(\left({y}\parallel {D}\wedge {D}\in {ℕ}_{0}\right)\to \left(\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to ¬{D}<{y}\right)\right)$
139 89 138 mpan2d ${⊢}\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\to \left({y}\parallel {D}\to \left(\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to ¬{D}<{y}\right)\right)$
140 139 com13 ${⊢}\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to \left({y}\parallel {D}\to \left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\to ¬{D}<{y}\right)\right)$
141 140 adantr ${⊢}\left(\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\wedge \left({M}\in ℤ\wedge {N}\in ℤ\right)\right)\to \left({y}\parallel {D}\to \left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\to ¬{D}<{y}\right)\right)$
142 83 141 syld ${⊢}\left(\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\wedge \left({M}\in ℤ\wedge {N}\in ℤ\right)\right)\to \left(\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\to \left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\to ¬{D}<{y}\right)\right)$
143 142 com13 ${⊢}\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)\to \left(\forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\to \left(\left(\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\wedge \left({M}\in ℤ\wedge {N}\in ℤ\right)\right)\to ¬{D}<{y}\right)\right)$
144 143 3impia ${⊢}\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\to \left(\left(\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\wedge \left({M}\in ℤ\wedge {N}\in ℤ\right)\right)\to ¬{D}<{y}\right)$
145 144 com12 ${⊢}\left(\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\wedge \left({M}\in ℤ\wedge {N}\in ℤ\right)\right)\to \left(\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\to ¬{D}<{y}\right)$
146 145 expimpd ${⊢}\left(\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to \left(\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\to ¬{D}<{y}\right)$
147 146 expimpd ${⊢}\left({y}\in ℤ\wedge \left({y}\parallel {M}\wedge {y}\parallel {N}\right)\right)\to \left(\left(¬\left({M}=0\wedge {N}=0\right)\wedge \left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\right)\to ¬{D}<{y}\right)$
148 74 147 sylbi ${⊢}{y}\in \left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\}\to \left(\left(¬\left({M}=0\wedge {N}=0\right)\wedge \left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\right)\to ¬{D}<{y}\right)$
149 148 impcom ${⊢}\left(\left(¬\left({M}=0\wedge {N}=0\right)\wedge \left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\right)\wedge {y}\in \left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\}\right)\to ¬{D}<{y}$
150 66 adantr ${⊢}\left({D}\parallel {M}\wedge {D}\parallel {N}\right)\to {D}\in ℤ$
151 150 ancri ${⊢}\left({D}\parallel {M}\wedge {D}\parallel {N}\right)\to \left({D}\in ℤ\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)$
152 151 3ad2ant2 ${⊢}\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\to \left({D}\in ℤ\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)$
153 152 ad2antll ${⊢}\left(¬\left({M}=0\wedge {N}=0\right)\wedge \left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\right)\to \left({D}\in ℤ\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)$
154 153 adantr ${⊢}\left(\left(¬\left({M}=0\wedge {N}=0\right)\wedge \left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\right)\wedge \left({y}\in ℝ\wedge {y}<{D}\right)\right)\to \left({D}\in ℤ\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)$
155 breq1 ${⊢}{n}={D}\to \left({n}\parallel {M}↔{D}\parallel {M}\right)$
156 breq1 ${⊢}{n}={D}\to \left({n}\parallel {N}↔{D}\parallel {N}\right)$
157 155 156 anbi12d ${⊢}{n}={D}\to \left(\left({n}\parallel {M}\wedge {n}\parallel {N}\right)↔\left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)$
158 157 elrab ${⊢}{D}\in \left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\}↔\left({D}\in ℤ\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\right)$
159 154 158 sylibr ${⊢}\left(\left(¬\left({M}=0\wedge {N}=0\right)\wedge \left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\right)\wedge \left({y}\in ℝ\wedge {y}<{D}\right)\right)\to {D}\in \left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\}$
160 breq2 ${⊢}{z}={D}\to \left({y}<{z}↔{y}<{D}\right)$
161 160 adantl ${⊢}\left(\left(\left(¬\left({M}=0\wedge {N}=0\right)\wedge \left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\right)\wedge \left({y}\in ℝ\wedge {y}<{D}\right)\right)\wedge {z}={D}\right)\to \left({y}<{z}↔{y}<{D}\right)$
162 simprr ${⊢}\left(\left(¬\left({M}=0\wedge {N}=0\right)\wedge \left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\right)\wedge \left({y}\in ℝ\wedge {y}<{D}\right)\right)\to {y}<{D}$
163 159 161 162 rspcedvd ${⊢}\left(\left(¬\left({M}=0\wedge {N}=0\right)\wedge \left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\right)\wedge \left({y}\in ℝ\wedge {y}<{D}\right)\right)\to \exists {z}\in \left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\}\phantom{\rule{.4em}{0ex}}{y}<{z}$
164 64 70 149 163 eqsupd ${⊢}\left(¬\left({M}=0\wedge {N}=0\right)\wedge \left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\right)\to sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)={D}$
165 62 164 eqtrd ${⊢}\left(¬\left({M}=0\wedge {N}=0\right)\wedge \left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\right)\to if\left(\left({M}=0\wedge {N}=0\right),0,sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)\right)={D}$
166 60 165 pm2.61ian ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\to if\left(\left({M}=0\wedge {N}=0\right),0,sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)\right)={D}$
167 22 166 eqtr2d ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)\to {D}={M}\mathrm{gcd}{N}$
168 20 167 impbida ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({D}={M}\mathrm{gcd}{N}↔\left(0\le {D}\wedge \left({D}\parallel {M}\wedge {D}\parallel {N}\right)\wedge \forall {e}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({e}\parallel {M}\wedge {e}\parallel {N}\right)\to {e}\parallel {D}\right)\right)\right)$