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 16592

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 16552	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℕ₀)
2	1	nn0ge0d 12556	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 0 ≤ (𝑀 gcd 𝑁))
3		gcddvds 16549	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁))
4		3anass 1109	. . . . . . . 8 ⊢ ((𝑒 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ (𝑒 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
5	4	biancomi 467	. . . . . . 7 ⊢ ((𝑒 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑒 ∈ ℤ))
6		dvdsgcd 16590	. . . . . . 7 ⊢ ((𝑒 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))
7	5, 6	sylbir 238	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑒 ∈ ℤ) → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))
8	7	ralrimiva 3157	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))
9	2, 3, 8	3jca 1144	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
10	9	adantr 485	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐷 = (𝑀 gcd 𝑁)) → (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
11		breq2 5108	. . . . 5 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (0 ≤ 𝐷 ↔ 0 ≤ (𝑀 gcd 𝑁)))
12		breq1 5107	. . . . . 6 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (𝐷 ∥ 𝑀 ↔ (𝑀 gcd 𝑁) ∥ 𝑀))
13		breq1 5107	. . . . . 6 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (𝐷 ∥ 𝑁 ↔ (𝑀 gcd 𝑁) ∥ 𝑁))
14	12, 13	anbi12d 643	. . . . 5 ⊢ (𝐷 = (𝑀 gcd 𝑁) → ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ↔ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)))
15		breq2 5108	. . . . . . 7 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (𝑒 ∥ 𝐷 ↔ 𝑒 ∥ (𝑀 gcd 𝑁)))
16	15	imbi2d 343	. . . . . 6 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
17	16	ralbidv 3188	. . . . 5 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
18	11, 14, 17	3anbi123d 1460	. . . 4 ⊢ (𝐷 = (𝑀 gcd 𝑁) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) ↔ (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))))
19	18	adantl 486	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐷 = (𝑀 gcd 𝑁)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) ↔ (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))))
20	10, 19	mpbird 260	. 2 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐷 = (𝑀 gcd 𝑁)) → (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))
21		gcdval 16542	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )))
22	21	adantr 485	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → (𝑀 gcd 𝑁) = if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )))
23		iftrue 4489	. . . . . 6 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 0)
24	23	adantr 485	. . . . 5 ⊢ (((𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 0)
25		breq2 5108	. . . . . . . . . 10 ⊢ (𝑀 = 0 → (𝐷 ∥ 𝑀 ↔ 𝐷 ∥ 0))
26		breq2 5108	. . . . . . . . . 10 ⊢ (𝑁 = 0 → (𝐷 ∥ 𝑁 ↔ 𝐷 ∥ 0))
27	25, 26	bi2anan9 649	. . . . . . . . 9 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ↔ (𝐷 ∥ 0 ∧ 𝐷 ∥ 0)))
28		breq2 5108	. . . . . . . . . . . 12 ⊢ (𝑀 = 0 → (𝑒 ∥ 𝑀 ↔ 𝑒 ∥ 0))
29		breq2 5108	. . . . . . . . . . . 12 ⊢ (𝑁 = 0 → (𝑒 ∥ 𝑁 ↔ 𝑒 ∥ 0))
30	28, 29	bi2anan9 649	. . . . . . . . . . 11 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) ↔ (𝑒 ∥ 0 ∧ 𝑒 ∥ 0)))
31	30	imbi1d 344	. . . . . . . . . 10 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷)))
32	31	ralbidv 3188	. . . . . . . . 9 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷)))
33	27, 32	3anbi23d 1463	. . . . . . . 8 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) ↔ (0 ≤ 𝐷 ∧ (𝐷 ∥ 0 ∧ 𝐷 ∥ 0) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷))))
34		dvdszrcl 16303	. . . . . . . . . . 11 ⊢ (𝐷 ∥ 0 → (𝐷 ∈ ℤ ∧ 0 ∈ ℤ))
35		dvds0 16317	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 ∈ ℤ → 𝑒 ∥ 0)
36	35, 35	jca 520	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 ∈ ℤ → (𝑒 ∥ 0 ∧ 𝑒 ∥ 0))
37	36	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) ∧ 𝑒 ∈ ℤ) → (𝑒 ∥ 0 ∧ 𝑒 ∥ 0))
38		pm5.5 364	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → (((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) ↔ 𝑒 ∥ 𝐷))
39	37, 38	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) ∧ 𝑒 ∈ ℤ) → (((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) ↔ 𝑒 ∥ 𝐷))
40	39	ralbidva 3186	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) ↔ ∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷))
41		0z 12590	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℤ
42		breq1 5107	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 0 → (𝑒 ∥ 𝐷 ↔ 0 ∥ 𝐷))
43	42	rspcv 3580	. . . . . . . . . . . . . . . . 17 ⊢ (0 ∈ ℤ → (∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷 → 0 ∥ 𝐷))
44	41, 43	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷 → 0 ∥ 𝐷)
45		0dvds 16322	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐷 ∈ ℤ → (0 ∥ 𝐷 ↔ 𝐷 = 0))
46	45	biimpd 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∈ ℤ → (0 ∥ 𝐷 → 𝐷 = 0))
47		eqcom 2772	. . . . . . . . . . . . . . . . 17 ⊢ (0 = 𝐷 ↔ 𝐷 = 0)
48	46, 47	imbitrrdi 255	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∈ ℤ → (0 ∥ 𝐷 → 0 = 𝐷))
49	44, 48	syl5 35	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ ℤ → (∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷 → 0 = 𝐷))
50	49	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) → (∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷 → 0 = 𝐷))
51	40, 50	sylbid 243	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷))
52	51	ex 417	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ ℤ → (0 ≤ 𝐷 → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷)))
53	52	adantr 485	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℤ ∧ 0 ∈ ℤ) → (0 ≤ 𝐷 → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷)))
54	34, 53	syl 18	. . . . . . . . . 10 ⊢ (𝐷 ∥ 0 → (0 ≤ 𝐷 → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷)))
55	54	adantr 485	. . . . . . . . 9 ⊢ ((𝐷 ∥ 0 ∧ 𝐷 ∥ 0) → (0 ≤ 𝐷 → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷)))
56	55	3imp21 1129	. . . . . . . 8 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 0 ∧ 𝐷 ∥ 0) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷)) → 0 = 𝐷)
57	33, 56	biimtrdi 256	. . . . . . 7 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → 0 = 𝐷))
58	57	adantld 495	. . . . . 6 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → 0 = 𝐷))
59	58	imp 411	. . . . 5 ⊢ (((𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → 0 = 𝐷)
60	24, 59	eqtrd 2800	. . . 4 ⊢ (((𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 𝐷)
61		iffalse 4492	. . . . . 6 ⊢ (¬ (𝑀 = 0 ∧ 𝑁 = 0) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ))
62	61	adantr 485	. . . . 5 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ))
63		ltso 11278	. . . . . . 7 ⊢ < Or ℝ
64	63	a1i 11	. . . . . 6 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → < Or ℝ)
65		dvdszrcl 16303	. . . . . . . . . . 11 ⊢ (𝐷 ∥ 𝑀 → (𝐷 ∈ ℤ ∧ 𝑀 ∈ ℤ))
66	65	simpld 499	. . . . . . . . . 10 ⊢ (𝐷 ∥ 𝑀 → 𝐷 ∈ ℤ)
67	66	zred 12688	. . . . . . . . 9 ⊢ (𝐷 ∥ 𝑀 → 𝐷 ∈ ℝ)
68	67	adantr 485	. . . . . . . 8 ⊢ ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) → 𝐷 ∈ ℝ)
69	68	3ad2ant2 1150	. . . . . . 7 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → 𝐷 ∈ ℝ)
70	69	ad2antll 741	. . . . . 6 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → 𝐷 ∈ ℝ)
71		breq1 5107	. . . . . . . . . 10 ⊢ (𝑛 = 𝑦 → (𝑛 ∥ 𝑀 ↔ 𝑦 ∥ 𝑀))
72		breq1 5107	. . . . . . . . . 10 ⊢ (𝑛 = 𝑦 → (𝑛 ∥ 𝑁 ↔ 𝑦 ∥ 𝑁))
73	71, 72	anbi12d 643	. . . . . . . . 9 ⊢ (𝑛 = 𝑦 → ((𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁) ↔ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)))
74	73	elrab 3653	. . . . . . . 8 ⊢ (𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} ↔ (𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)))
75		breq1 5107	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑦 → (𝑒 ∥ 𝑀 ↔ 𝑦 ∥ 𝑀))
76		breq1 5107	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑦 → (𝑒 ∥ 𝑁 ↔ 𝑦 ∥ 𝑁))
77	75, 76	anbi12d 643	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑦 → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) ↔ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)))
78		breq1 5107	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑦 → (𝑒 ∥ 𝐷 ↔ 𝑦 ∥ 𝐷))
79	77, 78	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑦 → (((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ((𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁) → 𝑦 ∥ 𝐷)))
80	79	rspcv 3580	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℤ → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → ((𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁) → 𝑦 ∥ 𝐷)))
81	80	com23 87	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℤ → ((𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → 𝑦 ∥ 𝐷)))
82	81	imp 411	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → 𝑦 ∥ 𝐷))
83	82	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → 𝑦 ∥ 𝐷))
84		elnn0z 12592	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐷 ∈ ℕ₀ ↔ (𝐷 ∈ ℤ ∧ 0 ≤ 𝐷))
85	84	simplbi2 505	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ ℤ → (0 ≤ 𝐷 → 𝐷 ∈ ℕ₀))
86	85	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 ≤ 𝐷 → 𝐷 ∈ ℕ₀))
87	65, 86	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ∥ 𝑀 → (0 ≤ 𝐷 → 𝐷 ∈ ℕ₀))
88	87	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) → (0 ≤ 𝐷 → 𝐷 ∈ ℕ₀))
89	88	impcom 412	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ₀)
90		simp-4l 794	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ 𝐷 ∈ ℕ₀) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁))) → 𝑦 ∈ ℤ)
91		elnn0 12494	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐷 ∈ ℕ₀ ↔ (𝐷 ∈ ℕ ∨ 𝐷 = 0))
92		2a1 29	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐷 ∈ ℕ → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ)))
93		breq1 5107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝐷 = 0 → (𝐷 ∥ 𝑀 ↔ 0 ∥ 𝑀))
94		breq1 5107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝐷 = 0 → (𝐷 ∥ 𝑁 ↔ 0 ∥ 𝑁))
95	93, 94	anbi12d 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝐷 = 0 → ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ↔ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)))
96	95	anbi2d 641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐷 = 0 → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ↔ (0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁))))
97	96	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐷 = 0 ∧ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ↔ (0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁))))
98		ianor 997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (¬ (𝑀 = 0 ∧ 𝑁 = 0) ↔ (¬ 𝑀 = 0 ∨ ¬ 𝑁 = 0))
99		dvdszrcl 16303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (0 ∥ 𝑀 → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ))
100		0dvds 16322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑀 ∈ ℤ → (0 ∥ 𝑀 ↔ 𝑀 = 0))
101		pm2.24 125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑀 = 0 → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ))
102	100, 101	biimtrdi 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑀 ∈ ℤ → (0 ∥ 𝑀 → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ)))
103	102	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 ∥ 𝑀 → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ)))
104	99, 103	mpcom 39	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (0 ∥ 𝑀 → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ))
105	104	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ))
106	105	com12 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (¬ 𝑀 = 0 → ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ))
107		dvdszrcl 16303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (0 ∥ 𝑁 → (0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
108		0dvds 16322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑁 ∈ ℤ → (0 ∥ 𝑁 ↔ 𝑁 = 0))
109		pm2.24 125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑁 = 0 → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ))
110	108, 109	biimtrdi 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑁 ∈ ℤ → (0 ∥ 𝑁 → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ)))
111	110	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ∥ 𝑁 → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ)))
112	107, 111	mpcom 39	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (0 ∥ 𝑁 → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ))
113	112	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ))
114	113	com12 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (¬ 𝑁 = 0 → ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ))
115	106, 114	jaoi 870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((¬ 𝑀 = 0 ∨ ¬ 𝑁 = 0) → ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ))
116	98, 115	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (¬ (𝑀 = 0 ∧ 𝑁 = 0) → ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ))
117	116	adantld 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (¬ (𝑀 = 0 ∧ 𝑁 = 0) → ((0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)) → 𝐷 ∈ ℕ))
118	117	ad2antll 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐷 = 0 ∧ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → ((0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)) → 𝐷 ∈ ℕ))
119	97, 118	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐷 = 0 ∧ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ))
120	119	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐷 = 0 → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ)))
121	92, 120	jaoi 870	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐷 ∈ ℕ ∨ 𝐷 = 0) → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ)))
122	91, 121	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐷 ∈ ℕ₀ → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ)))
123	122	impcom 412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ 𝐷 ∈ ℕ₀) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ))
124	123	imp 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ 𝐷 ∈ ℕ₀) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁))) → 𝐷 ∈ ℕ)
125		dvdsle 16356	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷))
126	90, 124, 125	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ 𝐷 ∈ ℕ₀) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁))) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷))
127	126	exp31 424	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝐷 ∈ ℕ₀ → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷))))
128	127	com14 97	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∥ 𝐷 → (𝐷 ∈ ℕ₀ → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → 𝑦 ≤ 𝐷))))
129	128	imp 411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → 𝑦 ≤ 𝐷)))
130	129	impcom 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀)) → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → 𝑦 ≤ 𝐷))
131	130	imp 411	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀)) ∧ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → 𝑦 ≤ 𝐷)
132		zre 12583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℤ → 𝑦 ∈ ℝ)
133	132	ad2antrr 738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → 𝑦 ∈ ℝ)
134	68	ad2antlr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀)) → 𝐷 ∈ ℝ)
135		lenlt 11276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑦 ≤ 𝐷 ↔ ¬ 𝐷 < 𝑦))
136	133, 134, 135	syl2anr 608	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀)) ∧ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → (𝑦 ≤ 𝐷 ↔ ¬ 𝐷 < 𝑦))
137	131, 136	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ ((((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀)) ∧ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → ¬ 𝐷 < 𝑦)
138	137	exp31 424	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → ((𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀) → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ¬ 𝐷 < 𝑦)))
139	89, 138	mpan2d 706	. . . . . . . . . . . . . . . 16 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → (𝑦 ∥ 𝐷 → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ¬ 𝐷 < 𝑦)))
140	139	com13 89	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑦 ∥ 𝐷 → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → ¬ 𝐷 < 𝑦)))
141	140	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑦 ∥ 𝐷 → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → ¬ 𝐷 < 𝑦)))
142	83, 141	syld 48	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → ¬ 𝐷 < 𝑦)))
143	142	com13 89	. . . . . . . . . . . 12 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ¬ 𝐷 < 𝑦)))
144	143	3impia 1133	. . . . . . . . . . 11 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ¬ 𝐷 < 𝑦))
145	144	com12 33	. . . . . . . . . 10 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → ¬ 𝐷 < 𝑦))
146	145	expimpd 458	. . . . . . . . 9 ⊢ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → ¬ 𝐷 < 𝑦))
147	146	expimpd 458	. . . . . . . 8 ⊢ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) → ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → ¬ 𝐷 < 𝑦))
148	74, 147	sylbi 220	. . . . . . 7 ⊢ (𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} → ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → ¬ 𝐷 < 𝑦))
149	148	impcom 412	. . . . . 6 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ 𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}) → ¬ 𝐷 < 𝑦)
150	66	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) → 𝐷 ∈ ℤ)
151	150	ancri 558	. . . . . . . . . . 11 ⊢ ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) → (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
152	151	3ad2ant2 1150	. . . . . . . . . 10 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
153	152	ad2antll 741	. . . . . . . . 9 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
154	153	adantr 485	. . . . . . . 8 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
155		breq1 5107	. . . . . . . . . 10 ⊢ (𝑛 = 𝐷 → (𝑛 ∥ 𝑀 ↔ 𝐷 ∥ 𝑀))
156		breq1 5107	. . . . . . . . . 10 ⊢ (𝑛 = 𝐷 → (𝑛 ∥ 𝑁 ↔ 𝐷 ∥ 𝑁))
157	155, 156	anbi12d 643	. . . . . . . . 9 ⊢ (𝑛 = 𝐷 → ((𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁) ↔ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
158	157	elrab 3653	. . . . . . . 8 ⊢ (𝐷 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} ↔ (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
159	154, 158	sylibr 237	. . . . . . 7 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → 𝐷 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)})
160		breq2 5108	. . . . . . . 8 ⊢ (𝑧 = 𝐷 → (𝑦 < 𝑧 ↔ 𝑦 < 𝐷))
161	160	adantl 486	. . . . . . 7 ⊢ ((((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) ∧ 𝑧 = 𝐷) → (𝑦 < 𝑧 ↔ 𝑦 < 𝐷))
162		simprr 784	. . . . . . 7 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → 𝑦 < 𝐷)
163	159, 161, 162	rspcedvd 3586	. . . . . 6 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}𝑦 < 𝑧)
164	64, 70, 149, 163	eqsupd 9405	. . . . 5 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ) = 𝐷)
165	62, 164	eqtrd 2800	. . . 4 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 𝐷)
166	60, 165	pm2.61ian 823	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 𝐷)
167	22, 166	eqtr2d 2801	. 2 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → 𝐷 = (𝑀 gcd 𝑁))
168	20, 167	impbida 812	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐷 = (𝑀 gcd 𝑁) ↔ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 ∀wral 3079 {crab 3417 ifcif 4483 class class class wbr 5104 Or wor 5558 (class class class)co 7400 supcsup 9388 ℝcr 11087 0cc0 11088 < clt 11231 ≤ cle 11232 ℕcn 12221 ℕ₀cn0 12492 ℤcz 12579 ∥ cdvds 16298 gcd cgcd 16540

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5250 ax-nul 5260 ax-pow 5326 ax-pr 5394 ax-un 7722 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165 ax-pre-sup 11166

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-br 5105 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6291 df-ord 6352 df-on 6353 df-lim 6354 df-suc 6355 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-om 7851 df-2nd 7975 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-er 8682 df-en 8932 df-dom 8933 df-sdom 8934 df-sup 9390 df-inf 9391 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-div 11860 df-nn 12222 df-2 12291 df-3 12292 df-n0 12493 df-z 12580 df-uz 12851 df-rp 13005 df-fl 13813 df-mod 13891 df-seq 14026 df-exp 14086 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-dvds 16299 df-gcd 16541

This theorem is referenced by: dfgcd3 37823

W3C validator