MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfgcd2 Structured version   Visualization version   GIF version

Theorem dfgcd2 16427
Description: Alternate definition of the gcd operator, see definition in [ApostolNT] p. 15. (Contributed by AV, 8-Aug-2021.)
Assertion
Ref Expression
dfgcd2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐷 = (𝑀 gcd 𝑁) ↔ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷))))
Distinct variable groups:   𝐷,𝑒   𝑒,𝑀   𝑒,𝑁

Proof of Theorem dfgcd2
Dummy variables 𝑛 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gcdcl 16386 . . . . . 6 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℕ0)
21nn0ge0d 12476 . . . . 5 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 0 ≤ (𝑀 gcd 𝑁))
3 gcddvds 16383 . . . . 5 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁))
4 3anass 1095 . . . . . . . 8 ((𝑒 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ (𝑒 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
54biancomi 463 . . . . . . 7 ((𝑒 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑒 ∈ ℤ))
6 dvdsgcd 16425 . . . . . . 7 ((𝑒 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑒𝑀𝑒𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))
75, 6sylbir 234 . . . . . 6 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑒 ∈ ℤ) → ((𝑒𝑀𝑒𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))
87ralrimiva 3143 . . . . 5 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))
92, 3, 83jca 1128 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
109adantr 481 . . 3 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐷 = (𝑀 gcd 𝑁)) → (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
11 breq2 5109 . . . . 5 (𝐷 = (𝑀 gcd 𝑁) → (0 ≤ 𝐷 ↔ 0 ≤ (𝑀 gcd 𝑁)))
12 breq1 5108 . . . . . 6 (𝐷 = (𝑀 gcd 𝑁) → (𝐷𝑀 ↔ (𝑀 gcd 𝑁) ∥ 𝑀))
13 breq1 5108 . . . . . 6 (𝐷 = (𝑀 gcd 𝑁) → (𝐷𝑁 ↔ (𝑀 gcd 𝑁) ∥ 𝑁))
1412, 13anbi12d 631 . . . . 5 (𝐷 = (𝑀 gcd 𝑁) → ((𝐷𝑀𝐷𝑁) ↔ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)))
15 breq2 5109 . . . . . . 7 (𝐷 = (𝑀 gcd 𝑁) → (𝑒𝐷𝑒 ∥ (𝑀 gcd 𝑁)))
1615imbi2d 340 . . . . . 6 (𝐷 = (𝑀 gcd 𝑁) → (((𝑒𝑀𝑒𝑁) → 𝑒𝐷) ↔ ((𝑒𝑀𝑒𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
1716ralbidv 3174 . . . . 5 (𝐷 = (𝑀 gcd 𝑁) → (∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷) ↔ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
1811, 14, 173anbi123d 1436 . . . 4 (𝐷 = (𝑀 gcd 𝑁) → ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)) ↔ (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))))
1918adantl 482 . . 3 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐷 = (𝑀 gcd 𝑁)) → ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)) ↔ (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))))
2010, 19mpbird 256 . 2 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐷 = (𝑀 gcd 𝑁)) → (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)))
21 gcdval 16376 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)}, ℝ, < )))
2221adantr 481 . . 3 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷))) → (𝑀 gcd 𝑁) = if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)}, ℝ, < )))
23 iftrue 4492 . . . . . 6 ((𝑀 = 0 ∧ 𝑁 = 0) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)}, ℝ, < )) = 0)
2423adantr 481 . . . . 5 (((𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)}, ℝ, < )) = 0)
25 breq2 5109 . . . . . . . . . 10 (𝑀 = 0 → (𝐷𝑀𝐷 ∥ 0))
26 breq2 5109 . . . . . . . . . 10 (𝑁 = 0 → (𝐷𝑁𝐷 ∥ 0))
2725, 26bi2anan9 637 . . . . . . . . 9 ((𝑀 = 0 ∧ 𝑁 = 0) → ((𝐷𝑀𝐷𝑁) ↔ (𝐷 ∥ 0 ∧ 𝐷 ∥ 0)))
28 breq2 5109 . . . . . . . . . . . 12 (𝑀 = 0 → (𝑒𝑀𝑒 ∥ 0))
29 breq2 5109 . . . . . . . . . . . 12 (𝑁 = 0 → (𝑒𝑁𝑒 ∥ 0))
3028, 29bi2anan9 637 . . . . . . . . . . 11 ((𝑀 = 0 ∧ 𝑁 = 0) → ((𝑒𝑀𝑒𝑁) ↔ (𝑒 ∥ 0 ∧ 𝑒 ∥ 0)))
3130imbi1d 341 . . . . . . . . . 10 ((𝑀 = 0 ∧ 𝑁 = 0) → (((𝑒𝑀𝑒𝑁) → 𝑒𝐷) ↔ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒𝐷)))
3231ralbidv 3174 . . . . . . . . 9 ((𝑀 = 0 ∧ 𝑁 = 0) → (∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷) ↔ ∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒𝐷)))
3327, 323anbi23d 1439 . . . . . . . 8 ((𝑀 = 0 ∧ 𝑁 = 0) → ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)) ↔ (0 ≤ 𝐷 ∧ (𝐷 ∥ 0 ∧ 𝐷 ∥ 0) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒𝐷))))
34 dvdszrcl 16141 . . . . . . . . . . 11 (𝐷 ∥ 0 → (𝐷 ∈ ℤ ∧ 0 ∈ ℤ))
35 dvds0 16154 . . . . . . . . . . . . . . . . . 18 (𝑒 ∈ ℤ → 𝑒 ∥ 0)
3635, 35jca 512 . . . . . . . . . . . . . . . . 17 (𝑒 ∈ ℤ → (𝑒 ∥ 0 ∧ 𝑒 ∥ 0))
3736adantl 482 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) ∧ 𝑒 ∈ ℤ) → (𝑒 ∥ 0 ∧ 𝑒 ∥ 0))
38 pm5.5 361 . . . . . . . . . . . . . . . 16 ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → (((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒𝐷) ↔ 𝑒𝐷))
3937, 38syl 17 . . . . . . . . . . . . . . 15 (((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) ∧ 𝑒 ∈ ℤ) → (((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒𝐷) ↔ 𝑒𝐷))
4039ralbidva 3172 . . . . . . . . . . . . . 14 ((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒𝐷) ↔ ∀𝑒 ∈ ℤ 𝑒𝐷))
41 0z 12510 . . . . . . . . . . . . . . . . 17 0 ∈ ℤ
42 breq1 5108 . . . . . . . . . . . . . . . . . 18 (𝑒 = 0 → (𝑒𝐷 ↔ 0 ∥ 𝐷))
4342rspcv 3577 . . . . . . . . . . . . . . . . 17 (0 ∈ ℤ → (∀𝑒 ∈ ℤ 𝑒𝐷 → 0 ∥ 𝐷))
4441, 43ax-mp 5 . . . . . . . . . . . . . . . 16 (∀𝑒 ∈ ℤ 𝑒𝐷 → 0 ∥ 𝐷)
45 0dvds 16159 . . . . . . . . . . . . . . . . . 18 (𝐷 ∈ ℤ → (0 ∥ 𝐷𝐷 = 0))
4645biimpd 228 . . . . . . . . . . . . . . . . 17 (𝐷 ∈ ℤ → (0 ∥ 𝐷𝐷 = 0))
47 eqcom 2743 . . . . . . . . . . . . . . . . 17 (0 = 𝐷𝐷 = 0)
4846, 47syl6ibr 251 . . . . . . . . . . . . . . . 16 (𝐷 ∈ ℤ → (0 ∥ 𝐷 → 0 = 𝐷))
4944, 48syl5 34 . . . . . . . . . . . . . . 15 (𝐷 ∈ ℤ → (∀𝑒 ∈ ℤ 𝑒𝐷 → 0 = 𝐷))
5049adantr 481 . . . . . . . . . . . . . 14 ((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) → (∀𝑒 ∈ ℤ 𝑒𝐷 → 0 = 𝐷))
5140, 50sylbid 239 . . . . . . . . . . . . 13 ((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒𝐷) → 0 = 𝐷))
5251ex 413 . . . . . . . . . . . 12 (𝐷 ∈ ℤ → (0 ≤ 𝐷 → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒𝐷) → 0 = 𝐷)))
5352adantr 481 . . . . . . . . . . 11 ((𝐷 ∈ ℤ ∧ 0 ∈ ℤ) → (0 ≤ 𝐷 → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒𝐷) → 0 = 𝐷)))
5434, 53syl 17 . . . . . . . . . 10 (𝐷 ∥ 0 → (0 ≤ 𝐷 → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒𝐷) → 0 = 𝐷)))
5554adantr 481 . . . . . . . . 9 ((𝐷 ∥ 0 ∧ 𝐷 ∥ 0) → (0 ≤ 𝐷 → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒𝐷) → 0 = 𝐷)))
56553imp21 1114 . . . . . . . 8 ((0 ≤ 𝐷 ∧ (𝐷 ∥ 0 ∧ 𝐷 ∥ 0) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒𝐷)) → 0 = 𝐷)
5733, 56syl6bi 252 . . . . . . 7 ((𝑀 = 0 ∧ 𝑁 = 0) → ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)) → 0 = 𝐷))
5857adantld 491 . . . . . 6 ((𝑀 = 0 ∧ 𝑁 = 0) → (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷))) → 0 = 𝐷))
5958imp 407 . . . . 5 (((𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)))) → 0 = 𝐷)
6024, 59eqtrd 2776 . . . 4 (((𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)}, ℝ, < )) = 𝐷)
61 iffalse 4495 . . . . . 6 (¬ (𝑀 = 0 ∧ 𝑁 = 0) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)}, ℝ, < )) = sup({𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)}, ℝ, < ))
6261adantr 481 . . . . 5 ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)}, ℝ, < )) = sup({𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)}, ℝ, < ))
63 ltso 11235 . . . . . . 7 < Or ℝ
6463a1i 11 . . . . . 6 ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)))) → < Or ℝ)
65 dvdszrcl 16141 . . . . . . . . . . 11 (𝐷𝑀 → (𝐷 ∈ ℤ ∧ 𝑀 ∈ ℤ))
6665simpld 495 . . . . . . . . . 10 (𝐷𝑀𝐷 ∈ ℤ)
6766zred 12607 . . . . . . . . 9 (𝐷𝑀𝐷 ∈ ℝ)
6867adantr 481 . . . . . . . 8 ((𝐷𝑀𝐷𝑁) → 𝐷 ∈ ℝ)
69683ad2ant2 1134 . . . . . . 7 ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)) → 𝐷 ∈ ℝ)
7069ad2antll 727 . . . . . 6 ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)))) → 𝐷 ∈ ℝ)
71 breq1 5108 . . . . . . . . . 10 (𝑛 = 𝑦 → (𝑛𝑀𝑦𝑀))
72 breq1 5108 . . . . . . . . . 10 (𝑛 = 𝑦 → (𝑛𝑁𝑦𝑁))
7371, 72anbi12d 631 . . . . . . . . 9 (𝑛 = 𝑦 → ((𝑛𝑀𝑛𝑁) ↔ (𝑦𝑀𝑦𝑁)))
7473elrab 3645 . . . . . . . 8 (𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)} ↔ (𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)))
75 breq1 5108 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = 𝑦 → (𝑒𝑀𝑦𝑀))
76 breq1 5108 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = 𝑦 → (𝑒𝑁𝑦𝑁))
7775, 76anbi12d 631 . . . . . . . . . . . . . . . . . . 19 (𝑒 = 𝑦 → ((𝑒𝑀𝑒𝑁) ↔ (𝑦𝑀𝑦𝑁)))
78 breq1 5108 . . . . . . . . . . . . . . . . . . 19 (𝑒 = 𝑦 → (𝑒𝐷𝑦𝐷))
7977, 78imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑦 → (((𝑒𝑀𝑒𝑁) → 𝑒𝐷) ↔ ((𝑦𝑀𝑦𝑁) → 𝑦𝐷)))
8079rspcv 3577 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℤ → (∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷) → ((𝑦𝑀𝑦𝑁) → 𝑦𝐷)))
8180com23 86 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℤ → ((𝑦𝑀𝑦𝑁) → (∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷) → 𝑦𝐷)))
8281imp 407 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) → (∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷) → 𝑦𝐷))
8382ad2antrr 724 . . . . . . . . . . . . . 14 ((((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷) → 𝑦𝐷))
84 elnn0z 12512 . . . . . . . . . . . . . . . . . . . . . 22 (𝐷 ∈ ℕ0 ↔ (𝐷 ∈ ℤ ∧ 0 ≤ 𝐷))
8584simplbi2 501 . . . . . . . . . . . . . . . . . . . . 21 (𝐷 ∈ ℤ → (0 ≤ 𝐷𝐷 ∈ ℕ0))
8685adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 ≤ 𝐷𝐷 ∈ ℕ0))
8765, 86syl 17 . . . . . . . . . . . . . . . . . . 19 (𝐷𝑀 → (0 ≤ 𝐷𝐷 ∈ ℕ0))
8887adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝐷𝑀𝐷𝑁) → (0 ≤ 𝐷𝐷 ∈ ℕ0))
8988impcom 408 . . . . . . . . . . . . . . . . 17 ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) → 𝐷 ∈ ℕ0)
90 simp-4l 781 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ 𝐷 ∈ ℕ0) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁))) → 𝑦 ∈ ℤ)
91 elnn0 12415 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐷 ∈ ℕ0 ↔ (𝐷 ∈ ℕ ∨ 𝐷 = 0))
92 2a1 28 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐷 ∈ ℕ → (((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) → 𝐷 ∈ ℕ)))
93 breq1 5108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝐷 = 0 → (𝐷𝑀 ↔ 0 ∥ 𝑀))
94 breq1 5108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝐷 = 0 → (𝐷𝑁 ↔ 0 ∥ 𝑁))
9593, 94anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝐷 = 0 → ((𝐷𝑀𝐷𝑁) ↔ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)))
9695anbi2d 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐷 = 0 → ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) ↔ (0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁))))
9796adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐷 = 0 ∧ ((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) ↔ (0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁))))
98 ianor 980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (¬ (𝑀 = 0 ∧ 𝑁 = 0) ↔ (¬ 𝑀 = 0 ∨ ¬ 𝑁 = 0))
99 dvdszrcl 16141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (0 ∥ 𝑀 → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ))
100 0dvds 16159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑀 ∈ ℤ → (0 ∥ 𝑀𝑀 = 0))
101 pm2.24 124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑀 = 0 → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ))
102100, 101syl6bi 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑀 ∈ ℤ → (0 ∥ 𝑀 → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ)))
103102adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 ∥ 𝑀 → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ)))
10499, 103mpcom 38 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (0 ∥ 𝑀 → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ))
105104adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ))
106105com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑀 = 0 → ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ))
107 dvdszrcl 16141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (0 ∥ 𝑁 → (0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
108 0dvds 16159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑁 ∈ ℤ → (0 ∥ 𝑁𝑁 = 0))
109 pm2.24 124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑁 = 0 → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ))
110108, 109syl6bi 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑁 ∈ ℤ → (0 ∥ 𝑁 → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ)))
111110adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ∥ 𝑁 → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ)))
112107, 111mpcom 38 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (0 ∥ 𝑁 → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ))
113112adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ))
114113com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑁 = 0 → ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ))
115106, 114jaoi 855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((¬ 𝑀 = 0 ∨ ¬ 𝑁 = 0) → ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ))
11698, 115sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (¬ (𝑀 = 0 ∧ 𝑁 = 0) → ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ))
117116adantld 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (¬ (𝑀 = 0 ∧ 𝑁 = 0) → ((0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)) → 𝐷 ∈ ℕ))
118117ad2antll 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐷 = 0 ∧ ((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → ((0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)) → 𝐷 ∈ ℕ))
11997, 118sylbid 239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐷 = 0 ∧ ((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) → 𝐷 ∈ ℕ))
120119ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐷 = 0 → (((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) → 𝐷 ∈ ℕ)))
12192, 120jaoi 855 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐷 ∈ ℕ ∨ 𝐷 = 0) → (((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) → 𝐷 ∈ ℕ)))
12291, 121sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐷 ∈ ℕ0 → (((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) → 𝐷 ∈ ℕ)))
123122impcom 408 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ 𝐷 ∈ ℕ0) → ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) → 𝐷 ∈ ℕ))
124123imp 407 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ 𝐷 ∈ ℕ0) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁))) → 𝐷 ∈ ℕ)
125 dvdsle 16192 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑦𝐷𝑦𝐷))
12690, 124, 125syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ 𝐷 ∈ ℕ0) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁))) → (𝑦𝐷𝑦𝐷))
127126exp31 420 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝐷 ∈ ℕ0 → ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) → (𝑦𝐷𝑦𝐷))))
128127com14 96 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝐷 → (𝐷 ∈ ℕ0 → ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) → (((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → 𝑦𝐷))))
129128imp 407 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝐷𝐷 ∈ ℕ0) → ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) → (((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → 𝑦𝐷)))
130129impcom 408 . . . . . . . . . . . . . . . . . . . 20 (((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) ∧ (𝑦𝐷𝐷 ∈ ℕ0)) → (((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → 𝑦𝐷))
131130imp 407 . . . . . . . . . . . . . . . . . . 19 ((((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) ∧ (𝑦𝐷𝐷 ∈ ℕ0)) ∧ ((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → 𝑦𝐷)
132 zre 12503 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℤ → 𝑦 ∈ ℝ)
133132ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → 𝑦 ∈ ℝ)
13468ad2antlr 725 . . . . . . . . . . . . . . . . . . . 20 (((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) ∧ (𝑦𝐷𝐷 ∈ ℕ0)) → 𝐷 ∈ ℝ)
135 lenlt 11233 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑦𝐷 ↔ ¬ 𝐷 < 𝑦))
136133, 134, 135syl2anr 597 . . . . . . . . . . . . . . . . . . 19 ((((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) ∧ (𝑦𝐷𝐷 ∈ ℕ0)) ∧ ((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → (𝑦𝐷 ↔ ¬ 𝐷 < 𝑦))
137131, 136mpbid 231 . . . . . . . . . . . . . . . . . 18 ((((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) ∧ (𝑦𝐷𝐷 ∈ ℕ0)) ∧ ((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → ¬ 𝐷 < 𝑦)
138137exp31 420 . . . . . . . . . . . . . . . . 17 ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) → ((𝑦𝐷𝐷 ∈ ℕ0) → (((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ¬ 𝐷 < 𝑦)))
13989, 138mpan2d 692 . . . . . . . . . . . . . . . 16 ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) → (𝑦𝐷 → (((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ¬ 𝐷 < 𝑦)))
140139com13 88 . . . . . . . . . . . . . . 15 (((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑦𝐷 → ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) → ¬ 𝐷 < 𝑦)))
141140adantr 481 . . . . . . . . . . . . . 14 ((((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑦𝐷 → ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) → ¬ 𝐷 < 𝑦)))
14283, 141syld 47 . . . . . . . . . . . . 13 ((((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷) → ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) → ¬ 𝐷 < 𝑦)))
143142com13 88 . . . . . . . . . . . 12 ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁)) → (∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷) → ((((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ¬ 𝐷 < 𝑦)))
1441433impia 1117 . . . . . . . . . . 11 ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)) → ((((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ¬ 𝐷 < 𝑦))
145144com12 32 . . . . . . . . . 10 ((((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)) → ¬ 𝐷 < 𝑦))
146145expimpd 454 . . . . . . . . 9 (((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷))) → ¬ 𝐷 < 𝑦))
147146expimpd 454 . . . . . . . 8 ((𝑦 ∈ ℤ ∧ (𝑦𝑀𝑦𝑁)) → ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)))) → ¬ 𝐷 < 𝑦))
14874, 147sylbi 216 . . . . . . 7 (𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)} → ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)))) → ¬ 𝐷 < 𝑦))
149148impcom 408 . . . . . 6 (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)))) ∧ 𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)}) → ¬ 𝐷 < 𝑦)
15066adantr 481 . . . . . . . . . . . 12 ((𝐷𝑀𝐷𝑁) → 𝐷 ∈ ℤ)
151150ancri 550 . . . . . . . . . . 11 ((𝐷𝑀𝐷𝑁) → (𝐷 ∈ ℤ ∧ (𝐷𝑀𝐷𝑁)))
1521513ad2ant2 1134 . . . . . . . . . 10 ((0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)) → (𝐷 ∈ ℤ ∧ (𝐷𝑀𝐷𝑁)))
153152ad2antll 727 . . . . . . . . 9 ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)))) → (𝐷 ∈ ℤ ∧ (𝐷𝑀𝐷𝑁)))
154153adantr 481 . . . . . . . 8 (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → (𝐷 ∈ ℤ ∧ (𝐷𝑀𝐷𝑁)))
155 breq1 5108 . . . . . . . . . 10 (𝑛 = 𝐷 → (𝑛𝑀𝐷𝑀))
156 breq1 5108 . . . . . . . . . 10 (𝑛 = 𝐷 → (𝑛𝑁𝐷𝑁))
157155, 156anbi12d 631 . . . . . . . . 9 (𝑛 = 𝐷 → ((𝑛𝑀𝑛𝑁) ↔ (𝐷𝑀𝐷𝑁)))
158157elrab 3645 . . . . . . . 8 (𝐷 ∈ {𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)} ↔ (𝐷 ∈ ℤ ∧ (𝐷𝑀𝐷𝑁)))
159154, 158sylibr 233 . . . . . . 7 (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → 𝐷 ∈ {𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)})
160 breq2 5109 . . . . . . . 8 (𝑧 = 𝐷 → (𝑦 < 𝑧𝑦 < 𝐷))
161160adantl 482 . . . . . . 7 ((((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) ∧ 𝑧 = 𝐷) → (𝑦 < 𝑧𝑦 < 𝐷))
162 simprr 771 . . . . . . 7 (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → 𝑦 < 𝐷)
163159, 161, 162rspcedvd 3583 . . . . . 6 (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)}𝑦 < 𝑧)
16464, 70, 149, 163eqsupd 9393 . . . . 5 ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)))) → sup({𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)}, ℝ, < ) = 𝐷)
16562, 164eqtrd 2776 . . . 4 ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)}, ℝ, < )) = 𝐷)
16660, 165pm2.61ian 810 . . 3 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛𝑀𝑛𝑁)}, ℝ, < )) = 𝐷)
16722, 166eqtr2d 2777 . 2 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷))) → 𝐷 = (𝑀 gcd 𝑁))
16820, 167impbida 799 1 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐷 = (𝑀 gcd 𝑁) ↔ (0 ≤ 𝐷 ∧ (𝐷𝑀𝐷𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒𝑀𝑒𝑁) → 𝑒𝐷))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wral 3064  {crab 3407  ifcif 4486   class class class wbr 5105   Or wor 5544  (class class class)co 7357  supcsup 9376  cr 11050  0cc0 11051   < clt 11189  cle 11190  cn 12153  0cn0 12413  cz 12499  cdvds 16136   gcd cgcd 16374
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-sup 9378  df-inf 9379  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-z 12500  df-uz 12764  df-rp 12916  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-dvds 16137  df-gcd 16375
This theorem is referenced by:  dfgcd3  35795
  Copyright terms: Public domain W3C validator