dfgcd2 - Metamath Proof Explorer

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

Theorem dfgcd2 16265

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.

Step	Hyp	Ref	Expression
1		gcdcl 16224	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℕ₀)
2	1	nn0ge0d 12307	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 0 ≤ (𝑀 gcd 𝑁))
3		gcddvds 16221	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁))
4		3anass 1094	. . . . . . . 8 ⊢ ((𝑒 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ (𝑒 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
5	4	biancomi 463	. . . . . . 7 ⊢ ((𝑒 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑒 ∈ ℤ))
6		dvdsgcd 16263	. . . . . . 7 ⊢ ((𝑒 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))
7	5, 6	sylbir 234	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑒 ∈ ℤ) → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))
8	7	ralrimiva 3110	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))
9	2, 3, 8	3jca 1127	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
10	9	adantr 481	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐷 = (𝑀 gcd 𝑁)) → (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
11		breq2 5083	. . . . 5 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (0 ≤ 𝐷 ↔ 0 ≤ (𝑀 gcd 𝑁)))
12		breq1 5082	. . . . . 6 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (𝐷 ∥ 𝑀 ↔ (𝑀 gcd 𝑁) ∥ 𝑀))
13		breq1 5082	. . . . . 6 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (𝐷 ∥ 𝑁 ↔ (𝑀 gcd 𝑁) ∥ 𝑁))
14	12, 13	anbi12d 631	. . . . 5 ⊢ (𝐷 = (𝑀 gcd 𝑁) → ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ↔ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)))
15		breq2 5083	. . . . . . 7 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (𝑒 ∥ 𝐷 ↔ 𝑒 ∥ (𝑀 gcd 𝑁)))
16	15	imbi2d 341	. . . . . 6 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
17	16	ralbidv 3123	. . . . 5 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
18	11, 14, 17	3anbi123d 1435	. . . 4 ⊢ (𝐷 = (𝑀 gcd 𝑁) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) ↔ (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))))
19	18	adantl 482	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐷 = (𝑀 gcd 𝑁)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) ↔ (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))))
20	10, 19	mpbird 256	. 2 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐷 = (𝑀 gcd 𝑁)) → (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))
21		gcdval 16214	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )))
22	21	adantr 481	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → (𝑀 gcd 𝑁) = if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )))
23		iftrue 4471	. . . . . 6 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 0)
24	23	adantr 481	. . . . 5 ⊢ (((𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 0)
25		breq2 5083	. . . . . . . . . 10 ⊢ (𝑀 = 0 → (𝐷 ∥ 𝑀 ↔ 𝐷 ∥ 0))
26		breq2 5083	. . . . . . . . . 10 ⊢ (𝑁 = 0 → (𝐷 ∥ 𝑁 ↔ 𝐷 ∥ 0))
27	25, 26	bi2anan9 636	. . . . . . . . 9 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ↔ (𝐷 ∥ 0 ∧ 𝐷 ∥ 0)))
28		breq2 5083	. . . . . . . . . . . 12 ⊢ (𝑀 = 0 → (𝑒 ∥ 𝑀 ↔ 𝑒 ∥ 0))
29		breq2 5083	. . . . . . . . . . . 12 ⊢ (𝑁 = 0 → (𝑒 ∥ 𝑁 ↔ 𝑒 ∥ 0))
30	28, 29	bi2anan9 636	. . . . . . . . . . 11 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) ↔ (𝑒 ∥ 0 ∧ 𝑒 ∥ 0)))
31	30	imbi1d 342	. . . . . . . . . 10 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷)))
32	31	ralbidv 3123	. . . . . . . . 9 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷)))
33	27, 32	3anbi23d 1438	. . . . . . . 8 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) ↔ (0 ≤ 𝐷 ∧ (𝐷 ∥ 0 ∧ 𝐷 ∥ 0) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷))))
34		dvdszrcl 15979	. . . . . . . . . . 11 ⊢ (𝐷 ∥ 0 → (𝐷 ∈ ℤ ∧ 0 ∈ ℤ))
35		dvds0 15992	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 ∈ ℤ → 𝑒 ∥ 0)
36	35, 35	jca 512	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 ∈ ℤ → (𝑒 ∥ 0 ∧ 𝑒 ∥ 0))
37	36	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) ∧ 𝑒 ∈ ℤ) → (𝑒 ∥ 0 ∧ 𝑒 ∥ 0))
38		pm5.5 362	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → (((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) ↔ 𝑒 ∥ 𝐷))
39	37, 38	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) ∧ 𝑒 ∈ ℤ) → (((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) ↔ 𝑒 ∥ 𝐷))
40	39	ralbidva 3122	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) ↔ ∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷))
41		0z 12341	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℤ
42		breq1 5082	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 0 → (𝑒 ∥ 𝐷 ↔ 0 ∥ 𝐷))
43	42	rspcv 3556	. . . . . . . . . . . . . . . . 17 ⊢ (0 ∈ ℤ → (∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷 → 0 ∥ 𝐷))
44	41, 43	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷 → 0 ∥ 𝐷)
45		0dvds 15997	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐷 ∈ ℤ → (0 ∥ 𝐷 ↔ 𝐷 = 0))
46	45	biimpd 228	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∈ ℤ → (0 ∥ 𝐷 → 𝐷 = 0))
47		eqcom 2747	. . . . . . . . . . . . . . . . 17 ⊢ (0 = 𝐷 ↔ 𝐷 = 0)
48	46, 47	syl6ibr 251	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∈ ℤ → (0 ∥ 𝐷 → 0 = 𝐷))
49	44, 48	syl5 34	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ ℤ → (∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷 → 0 = 𝐷))
50	49	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) → (∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷 → 0 = 𝐷))
51	40, 50	sylbid 239	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷))
52	51	ex 413	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ ℤ → (0 ≤ 𝐷 → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷)))
53	52	adantr 481	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℤ ∧ 0 ∈ ℤ) → (0 ≤ 𝐷 → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷)))
54	34, 53	syl 17	. . . . . . . . . 10 ⊢ (𝐷 ∥ 0 → (0 ≤ 𝐷 → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷)))
55	54	adantr 481	. . . . . . . . 9 ⊢ ((𝐷 ∥ 0 ∧ 𝐷 ∥ 0) → (0 ≤ 𝐷 → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷)))
56	55	3imp21 1113	. . . . . . . 8 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 0 ∧ 𝐷 ∥ 0) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷)) → 0 = 𝐷)
57	33, 56	syl6bi 252	. . . . . . 7 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → 0 = 𝐷))
58	57	adantld 491	. . . . . 6 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → 0 = 𝐷))
59	58	imp 407	. . . . 5 ⊢ (((𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → 0 = 𝐷)
60	24, 59	eqtrd 2780	. . . 4 ⊢ (((𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 𝐷)
61		iffalse 4474	. . . . . 6 ⊢ (¬ (𝑀 = 0 ∧ 𝑁 = 0) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ))
62	61	adantr 481	. . . . 5 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ))
63		ltso 11066	. . . . . . 7 ⊢ < Or ℝ
64	63	a1i 11	. . . . . 6 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → < Or ℝ)
65		dvdszrcl 15979	. . . . . . . . . . 11 ⊢ (𝐷 ∥ 𝑀 → (𝐷 ∈ ℤ ∧ 𝑀 ∈ ℤ))
66	65	simpld 495	. . . . . . . . . 10 ⊢ (𝐷 ∥ 𝑀 → 𝐷 ∈ ℤ)
67	66	zred 12437	. . . . . . . . 9 ⊢ (𝐷 ∥ 𝑀 → 𝐷 ∈ ℝ)
68	67	adantr 481	. . . . . . . 8 ⊢ ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) → 𝐷 ∈ ℝ)
69	68	3ad2ant2 1133	. . . . . . 7 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → 𝐷 ∈ ℝ)
70	69	ad2antll 726	. . . . . 6 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → 𝐷 ∈ ℝ)
71		breq1 5082	. . . . . . . . . 10 ⊢ (𝑛 = 𝑦 → (𝑛 ∥ 𝑀 ↔ 𝑦 ∥ 𝑀))
72		breq1 5082	. . . . . . . . . 10 ⊢ (𝑛 = 𝑦 → (𝑛 ∥ 𝑁 ↔ 𝑦 ∥ 𝑁))
73	71, 72	anbi12d 631	. . . . . . . . 9 ⊢ (𝑛 = 𝑦 → ((𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁) ↔ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)))
74	73	elrab 3626	. . . . . . . 8 ⊢ (𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} ↔ (𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)))
75		breq1 5082	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑦 → (𝑒 ∥ 𝑀 ↔ 𝑦 ∥ 𝑀))
76		breq1 5082	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑦 → (𝑒 ∥ 𝑁 ↔ 𝑦 ∥ 𝑁))
77	75, 76	anbi12d 631	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑦 → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) ↔ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)))
78		breq1 5082	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑦 → (𝑒 ∥ 𝐷 ↔ 𝑦 ∥ 𝐷))
79	77, 78	imbi12d 345	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑦 → (((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ((𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁) → 𝑦 ∥ 𝐷)))
80	79	rspcv 3556	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℤ → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → ((𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁) → 𝑦 ∥ 𝐷)))
81	80	com23 86	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℤ → ((𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → 𝑦 ∥ 𝐷)))
82	81	imp 407	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → 𝑦 ∥ 𝐷))
83	82	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → 𝑦 ∥ 𝐷))
84		elnn0z 12343	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐷 ∈ ℕ₀ ↔ (𝐷 ∈ ℤ ∧ 0 ≤ 𝐷))
85	84	simplbi2 501	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ ℤ → (0 ≤ 𝐷 → 𝐷 ∈ ℕ₀))
86	85	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 ≤ 𝐷 → 𝐷 ∈ ℕ₀))
87	65, 86	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ∥ 𝑀 → (0 ≤ 𝐷 → 𝐷 ∈ ℕ₀))
88	87	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) → (0 ≤ 𝐷 → 𝐷 ∈ ℕ₀))
89	88	impcom 408	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ₀)
90		simp-4l 780	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ 𝐷 ∈ ℕ₀) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁))) → 𝑦 ∈ ℤ)
91		elnn0 12246	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐷 ∈ ℕ₀ ↔ (𝐷 ∈ ℕ ∨ 𝐷 = 0))
92		2a1 28	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐷 ∈ ℕ → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ)))
93		breq1 5082	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝐷 = 0 → (𝐷 ∥ 𝑀 ↔ 0 ∥ 𝑀))
94		breq1 5082	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝐷 = 0 → (𝐷 ∥ 𝑁 ↔ 0 ∥ 𝑁))
95	93, 94	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝐷 = 0 → ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ↔ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)))
96	95	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐷 = 0 → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ↔ (0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁))))
97	96	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐷 = 0 ∧ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ↔ (0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁))))
98		ianor 979	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (¬ (𝑀 = 0 ∧ 𝑁 = 0) ↔ (¬ 𝑀 = 0 ∨ ¬ 𝑁 = 0))
99		dvdszrcl 15979	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (0 ∥ 𝑀 → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ))
100		0dvds 15997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑀 ∈ ℤ → (0 ∥ 𝑀 ↔ 𝑀 = 0))
101		pm2.24 124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑀 = 0 → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ))
102	100, 101	syl6bi 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑀 ∈ ℤ → (0 ∥ 𝑀 → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ)))
103	102	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 ∥ 𝑀 → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ)))
104	99, 103	mpcom 38	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (0 ∥ 𝑀 → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ))
105	104	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ))
106	105	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (¬ 𝑀 = 0 → ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ))
107		dvdszrcl 15979	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (0 ∥ 𝑁 → (0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
108		0dvds 15997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑁 ∈ ℤ → (0 ∥ 𝑁 ↔ 𝑁 = 0))
109		pm2.24 124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑁 = 0 → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ))
110	108, 109	syl6bi 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑁 ∈ ℤ → (0 ∥ 𝑁 → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ)))
111	110	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ∥ 𝑁 → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ)))
112	107, 111	mpcom 38	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (0 ∥ 𝑁 → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ))
113	112	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ))
114	113	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (¬ 𝑁 = 0 → ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ))
115	106, 114	jaoi 854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((¬ 𝑀 = 0 ∨ ¬ 𝑁 = 0) → ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ))
116	98, 115	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (¬ (𝑀 = 0 ∧ 𝑁 = 0) → ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ))
117	116	adantld 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (¬ (𝑀 = 0 ∧ 𝑁 = 0) → ((0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)) → 𝐷 ∈ ℕ))
118	117	ad2antll 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐷 = 0 ∧ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → ((0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)) → 𝐷 ∈ ℕ))
119	97, 118	sylbid 239	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐷 = 0 ∧ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ))
120	119	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐷 = 0 → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ)))
121	92, 120	jaoi 854	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐷 ∈ ℕ ∨ 𝐷 = 0) → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ)))
122	91, 121	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐷 ∈ ℕ₀ → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ)))
123	122	impcom 408	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ 𝐷 ∈ ℕ₀) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ))
124	123	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ 𝐷 ∈ ℕ₀) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁))) → 𝐷 ∈ ℕ)
125		dvdsle 16030	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷))
126	90, 124, 125	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ 𝐷 ∈ ℕ₀) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁))) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷))
127	126	exp31 420	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝐷 ∈ ℕ₀ → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷))))
128	127	com14 96	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∥ 𝐷 → (𝐷 ∈ ℕ₀ → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → 𝑦 ≤ 𝐷))))
129	128	imp 407	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → 𝑦 ≤ 𝐷)))
130	129	impcom 408	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀)) → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → 𝑦 ≤ 𝐷))
131	130	imp 407	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀)) ∧ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → 𝑦 ≤ 𝐷)
132		zre 12334	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℤ → 𝑦 ∈ ℝ)
133	132	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → 𝑦 ∈ ℝ)
134	68	ad2antlr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀)) → 𝐷 ∈ ℝ)
135		lenlt 11064	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑦 ≤ 𝐷 ↔ ¬ 𝐷 < 𝑦))
136	133, 134, 135	syl2anr 597	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀)) ∧ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → (𝑦 ≤ 𝐷 ↔ ¬ 𝐷 < 𝑦))
137	131, 136	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀)) ∧ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → ¬ 𝐷 < 𝑦)
138	137	exp31 420	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → ((𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀) → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ¬ 𝐷 < 𝑦)))
139	89, 138	mpan2d 691	. . . . . . . . . . . . . . . 16 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → (𝑦 ∥ 𝐷 → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ¬ 𝐷 < 𝑦)))
140	139	com13 88	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑦 ∥ 𝐷 → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → ¬ 𝐷 < 𝑦)))
141	140	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑦 ∥ 𝐷 → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → ¬ 𝐷 < 𝑦)))
142	83, 141	syld 47	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → ¬ 𝐷 < 𝑦)))
143	142	com13 88	. . . . . . . . . . . 12 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ¬ 𝐷 < 𝑦)))
144	143	3impia 1116	. . . . . . . . . . 11 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ¬ 𝐷 < 𝑦))
145	144	com12 32	. . . . . . . . . 10 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → ¬ 𝐷 < 𝑦))
146	145	expimpd 454	. . . . . . . . 9 ⊢ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → ¬ 𝐷 < 𝑦))
147	146	expimpd 454	. . . . . . . 8 ⊢ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) → ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → ¬ 𝐷 < 𝑦))
148	74, 147	sylbi 216	. . . . . . 7 ⊢ (𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} → ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → ¬ 𝐷 < 𝑦))
149	148	impcom 408	. . . . . 6 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ 𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}) → ¬ 𝐷 < 𝑦)
150	66	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) → 𝐷 ∈ ℤ)
151	150	ancri 550	. . . . . . . . . . 11 ⊢ ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) → (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
152	151	3ad2ant2 1133	. . . . . . . . . 10 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
153	152	ad2antll 726	. . . . . . . . 9 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
154	153	adantr 481	. . . . . . . 8 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
155		breq1 5082	. . . . . . . . . 10 ⊢ (𝑛 = 𝐷 → (𝑛 ∥ 𝑀 ↔ 𝐷 ∥ 𝑀))
156		breq1 5082	. . . . . . . . . 10 ⊢ (𝑛 = 𝐷 → (𝑛 ∥ 𝑁 ↔ 𝐷 ∥ 𝑁))
157	155, 156	anbi12d 631	. . . . . . . . 9 ⊢ (𝑛 = 𝐷 → ((𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁) ↔ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
158	157	elrab 3626	. . . . . . . 8 ⊢ (𝐷 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} ↔ (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
159	154, 158	sylibr 233	. . . . . . 7 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → 𝐷 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)})
160		breq2 5083	. . . . . . . 8 ⊢ (𝑧 = 𝐷 → (𝑦 < 𝑧 ↔ 𝑦 < 𝐷))
161	160	adantl 482	. . . . . . 7 ⊢ ((((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) ∧ 𝑧 = 𝐷) → (𝑦 < 𝑧 ↔ 𝑦 < 𝐷))
162		simprr 770	. . . . . . 7 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → 𝑦 < 𝐷)
163	159, 161, 162	rspcedvd 3564	. . . . . 6 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}𝑦 < 𝑧)
164	64, 70, 149, 163	eqsupd 9204	. . . . 5 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ) = 𝐷)
165	62, 164	eqtrd 2780	. . . 4 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 𝐷)
166	60, 165	pm2.61ian 809	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 𝐷)
167	22, 166	eqtr2d 2781	. 2 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → 𝐷 = (𝑀 gcd 𝑁))
168	20, 167	impbida 798	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐷 = (𝑀 gcd 𝑁) ↔ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 ∧ w3a 1086 = wceq 1542 ∈ wcel 2110 ∀wral 3066 {crab 3070 ifcif 4465 class class class wbr 5079 Or wor 5503 (class class class)co 7272 supcsup 9187 ℝcr 10881 0cc0 10882 < clt 11020 ≤ cle 11021 ℕcn 11984 ℕ₀cn0 12244 ℤcz 12330 ∥ cdvds 15974 gcd cgcd 16212

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2711 ax-sep 5227 ax-nul 5234 ax-pow 5292 ax-pr 5356 ax-un 7583 ax-cnex 10938 ax-resscn 10939 ax-1cn 10940 ax-icn 10941 ax-addcl 10942 ax-addrcl 10943 ax-mulcl 10944 ax-mulrcl 10945 ax-mulcom 10946 ax-addass 10947 ax-mulass 10948 ax-distr 10949 ax-i2m1 10950 ax-1ne0 10951 ax-1rid 10952 ax-rnegex 10953 ax-rrecex 10954 ax-cnre 10955 ax-pre-lttri 10956 ax-pre-lttrn 10957 ax-pre-ltadd 10958 ax-pre-mulgt0 10959 ax-pre-sup 10960

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2072 df-mo 2542 df-eu 2571 df-clab 2718 df-cleq 2732 df-clel 2818 df-nfc 2891 df-ne 2946 df-nel 3052 df-ral 3071 df-rex 3072 df-reu 3073 df-rmo 3074 df-rab 3075 df-v 3433 df-sbc 3721 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-pss 3911 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4846 df-iun 4932 df-br 5080 df-opab 5142 df-mpt 5163 df-tr 5197 df-id 5490 df-eprel 5496 df-po 5504 df-so 5505 df-fr 5545 df-we 5547 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-pred 6201 df-ord 6268 df-on 6269 df-lim 6270 df-suc 6271 df-iota 6390 df-fun 6434 df-fn 6435 df-f 6436 df-f1 6437 df-fo 6438 df-f1o 6439 df-fv 6440 df-riota 7229 df-ov 7275 df-oprab 7276 df-mpo 7277 df-om 7708 df-2nd 7826 df-frecs 8089 df-wrecs 8120 df-recs 8194 df-rdg 8233 df-er 8490 df-en 8726 df-dom 8727 df-sdom 8728 df-sup 9189 df-inf 9190 df-pnf 11022 df-mnf 11023 df-xr 11024 df-ltxr 11025 df-le 11026 df-sub 11218 df-neg 11219 df-div 11644 df-nn 11985 df-2 12047 df-3 12048 df-n0 12245 df-z 12331 df-uz 12594 df-rp 12742 df-fl 13523 df-mod 13601 df-seq 13733 df-exp 13794 df-cj 14821 df-re 14822 df-im 14823 df-sqrt 14957 df-abs 14958 df-dvds 15975 df-gcd 16213

This theorem is referenced by: dfgcd3 35504

W3C validator