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 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐷 = ( 𝑀 gcd 𝑁 ) ↔ ( 0 ≤ 𝐷 ∧ ( 𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁 ) ∧ ∀ 𝑒 ∈ ℤ ( ( 𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁 ) → 𝑒 ∥ 𝐷 ) ) ) )

Proof

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