dfgcd2 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > dfgcd2		GIF version

Theorem dfgcd2 12410

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 12362	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℕ₀)
2	1	nn0ge0d 9371	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 0 ≤ (𝑀 gcd 𝑁))
3		gcddvds 12359	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁))
4		3anass 985	. . . . . . . 8 ⊢ ((𝑒 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ (𝑒 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
5		ancom 266	. . . . . . . 8 ⊢ ((𝑒 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑒 ∈ ℤ))
6	4, 5	bitri 184	. . . . . . 7 ⊢ ((𝑒 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑒 ∈ ℤ))
7		dvdsgcd 12408	. . . . . . 7 ⊢ ((𝑒 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))
8	6, 7	sylbir 135	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑒 ∈ ℤ) → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))
9	8	ralrimiva 2580	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))
10	2, 3, 9	3jca 1180	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
11	10	adantr 276	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐷 = (𝑀 gcd 𝑁)) → (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
12		breq2 4055	. . . . 5 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (0 ≤ 𝐷 ↔ 0 ≤ (𝑀 gcd 𝑁)))
13		breq1 4054	. . . . . 6 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (𝐷 ∥ 𝑀 ↔ (𝑀 gcd 𝑁) ∥ 𝑀))
14		breq1 4054	. . . . . 6 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (𝐷 ∥ 𝑁 ↔ (𝑀 gcd 𝑁) ∥ 𝑁))
15	13, 14	anbi12d 473	. . . . 5 ⊢ (𝐷 = (𝑀 gcd 𝑁) → ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ↔ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)))
16		breq2 4055	. . . . . . 7 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (𝑒 ∥ 𝐷 ↔ 𝑒 ∥ (𝑀 gcd 𝑁)))
17	16	imbi2d 230	. . . . . 6 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
18	17	ralbidv 2507	. . . . 5 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
19	12, 15, 18	3anbi123d 1325	. . . 4 ⊢ (𝐷 = (𝑀 gcd 𝑁) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) ↔ (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))))
20	19	adantl 277	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐷 = (𝑀 gcd 𝑁)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) ↔ (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))))
21	11, 20	mpbird 167	. 2 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐷 = (𝑀 gcd 𝑁)) → (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))
22		gcdval 12355	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )))
23	22	adantr 276	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → (𝑀 gcd 𝑁) = if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )))
24		iftrue 3580	. . . . . . 7 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 0)
25	24	adantr 276	. . . . . 6 ⊢ (((𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 0)
26		breq2 4055	. . . . . . . . . . 11 ⊢ (𝑀 = 0 → (𝐷 ∥ 𝑀 ↔ 𝐷 ∥ 0))
27		breq2 4055	. . . . . . . . . . 11 ⊢ (𝑁 = 0 → (𝐷 ∥ 𝑁 ↔ 𝐷 ∥ 0))
28	26, 27	bi2anan9 606	. . . . . . . . . 10 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ↔ (𝐷 ∥ 0 ∧ 𝐷 ∥ 0)))
29		breq2 4055	. . . . . . . . . . . . 13 ⊢ (𝑀 = 0 → (𝑒 ∥ 𝑀 ↔ 𝑒 ∥ 0))
30		breq2 4055	. . . . . . . . . . . . 13 ⊢ (𝑁 = 0 → (𝑒 ∥ 𝑁 ↔ 𝑒 ∥ 0))
31	29, 30	bi2anan9 606	. . . . . . . . . . . 12 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) ↔ (𝑒 ∥ 0 ∧ 𝑒 ∥ 0)))
32	31	imbi1d 231	. . . . . . . . . . 11 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷)))
33	32	ralbidv 2507	. . . . . . . . . 10 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷)))
34	28, 33	3anbi23d 1328	. . . . . . . . 9 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) ↔ (0 ≤ 𝐷 ∧ (𝐷 ∥ 0 ∧ 𝐷 ∥ 0) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷))))
35		dvdszrcl 12178	. . . . . . . . . . . . 13 ⊢ (𝐷 ∥ 0 → (𝐷 ∈ ℤ ∧ 0 ∈ ℤ))
36		dvds0 12192	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 ∈ ℤ → 𝑒 ∥ 0)
37	36, 36	jca 306	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 ∈ ℤ → (𝑒 ∥ 0 ∧ 𝑒 ∥ 0))
38	37	adantl 277	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) ∧ 𝑒 ∈ ℤ) → (𝑒 ∥ 0 ∧ 𝑒 ∥ 0))
39		pm5.5 242	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → (((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) ↔ 𝑒 ∥ 𝐷))
40	38, 39	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) ∧ 𝑒 ∈ ℤ) → (((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) ↔ 𝑒 ∥ 𝐷))
41	40	ralbidva 2503	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) ↔ ∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷))
42		0z 9403	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℤ
43		breq1 4054	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 0 → (𝑒 ∥ 𝐷 ↔ 0 ∥ 𝐷))
44	43	rspcv 2877	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 ∈ ℤ → (∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷 → 0 ∥ 𝐷))
45	42, 44	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷 → 0 ∥ 𝐷)
46		0dvds 12197	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐷 ∈ ℤ → (0 ∥ 𝐷 ↔ 𝐷 = 0))
47	46	biimpd 144	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ∈ ℤ → (0 ∥ 𝐷 → 𝐷 = 0))
48		eqcom 2208	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 = 𝐷 ↔ 𝐷 = 0)
49	47, 48	imbitrrdi 162	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐷 ∈ ℤ → (0 ∥ 𝐷 → 0 = 𝐷))
50	45, 49	syl5 32	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∈ ℤ → (∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷 → 0 = 𝐷))
51	50	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) → (∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷 → 0 = 𝐷))
52	41, 51	sylbid 150	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷))
53	52	ex 115	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ ℤ → (0 ≤ 𝐷 → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷)))
54	53	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ ℤ ∧ 0 ∈ ℤ) → (0 ≤ 𝐷 → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷)))
55	35, 54	syl 14	. . . . . . . . . . . 12 ⊢ (𝐷 ∥ 0 → (0 ≤ 𝐷 → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷)))
56	55	adantr 276	. . . . . . . . . . 11 ⊢ ((𝐷 ∥ 0 ∧ 𝐷 ∥ 0) → (0 ≤ 𝐷 → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷)))
57	56	com12 30	. . . . . . . . . 10 ⊢ (0 ≤ 𝐷 → ((𝐷 ∥ 0 ∧ 𝐷 ∥ 0) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷)))
58	57	3imp 1196	. . . . . . . . 9 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 0 ∧ 𝐷 ∥ 0) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷)) → 0 = 𝐷)
59	34, 58	biimtrdi 163	. . . . . . . 8 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → 0 = 𝐷))
60	59	adantld 278	. . . . . . 7 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → 0 = 𝐷))
61	60	imp 124	. . . . . 6 ⊢ (((𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → 0 = 𝐷)
62	25, 61	eqtrd 2239	. . . . 5 ⊢ (((𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 𝐷)
63	62	ancoms 268	. . . 4 ⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) ∧ (𝑀 = 0 ∧ 𝑁 = 0)) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 𝐷)
64		iffalse 3583	. . . . . . 7 ⊢ (¬ (𝑀 = 0 ∧ 𝑁 = 0) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ))
65	64	adantr 276	. . . . . 6 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ))
66		lttri3 8172	. . . . . . . 8 ⊢ ((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) → (𝑓 = 𝑔 ↔ (¬ 𝑓 < 𝑔 ∧ ¬ 𝑔 < 𝑓)))
67	66	adantl 277	. . . . . . 7 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) → (𝑓 = 𝑔 ↔ (¬ 𝑓 < 𝑔 ∧ ¬ 𝑔 < 𝑓)))
68		dvdszrcl 12178	. . . . . . . . . . . 12 ⊢ (𝐷 ∥ 𝑀 → (𝐷 ∈ ℤ ∧ 𝑀 ∈ ℤ))
69	68	simpld 112	. . . . . . . . . . 11 ⊢ (𝐷 ∥ 𝑀 → 𝐷 ∈ ℤ)
70	69	zred 9515	. . . . . . . . . 10 ⊢ (𝐷 ∥ 𝑀 → 𝐷 ∈ ℝ)
71	70	adantr 276	. . . . . . . . 9 ⊢ ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) → 𝐷 ∈ ℝ)
72	71	3ad2ant2 1022	. . . . . . . 8 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → 𝐷 ∈ ℝ)
73	72	ad2antll 491	. . . . . . 7 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → 𝐷 ∈ ℝ)
74		breq1 4054	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑦 → (𝑛 ∥ 𝑀 ↔ 𝑦 ∥ 𝑀))
75		breq1 4054	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑦 → (𝑛 ∥ 𝑁 ↔ 𝑦 ∥ 𝑁))
76	74, 75	anbi12d 473	. . . . . . . . . 10 ⊢ (𝑛 = 𝑦 → ((𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁) ↔ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)))
77	76	elrab 2933	. . . . . . . . 9 ⊢ (𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} ↔ (𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)))
78		breq1 4054	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑦 → (𝑒 ∥ 𝑀 ↔ 𝑦 ∥ 𝑀))
79		breq1 4054	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑦 → (𝑒 ∥ 𝑁 ↔ 𝑦 ∥ 𝑁))
80	78, 79	anbi12d 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑦 → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) ↔ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)))
81		breq1 4054	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑦 → (𝑒 ∥ 𝐷 ↔ 𝑦 ∥ 𝐷))
82	80, 81	imbi12d 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑦 → (((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ((𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁) → 𝑦 ∥ 𝐷)))
83	82	rspcv 2877	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℤ → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → ((𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁) → 𝑦 ∥ 𝐷)))
84	83	com23 78	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℤ → ((𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → 𝑦 ∥ 𝐷)))
85	84	imp 124	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → 𝑦 ∥ 𝐷))
86	85	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → 𝑦 ∥ 𝐷))
87		elnn0z 9405	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐷 ∈ ℕ₀ ↔ (𝐷 ∈ ℤ ∧ 0 ≤ 𝐷))
88	87	simplbi2 385	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ ℤ → (0 ≤ 𝐷 → 𝐷 ∈ ℕ₀))
89	88	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 ≤ 𝐷 → 𝐷 ∈ ℕ₀))
90	68, 89	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ∥ 𝑀 → (0 ≤ 𝐷 → 𝐷 ∈ ℕ₀))
91	90	adantr 276	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) → (0 ≤ 𝐷 → 𝐷 ∈ ℕ₀))
92	91	impcom 125	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ₀)
93		zre 9396	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℤ → 𝑦 ∈ ℝ)
94	93	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → 𝑦 ∈ ℝ)
95	94	ad2antrl 490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀)) ∧ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑦 ∈ ℝ)
96	71	ad3antlr 493	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀)) ∧ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝐷 ∈ ℝ)
97		simp-5l 543	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐷 ∈ ℕ₀) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁))) → 𝑦 ∈ ℤ)
98		elnn0 9317	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐷 ∈ ℕ₀ ↔ (𝐷 ∈ ℕ ∨ 𝐷 = 0))
99		2a1 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐷 ∈ ℕ → ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ)))
100		breq1 4054	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝐷 = 0 → (𝐷 ∥ 𝑀 ↔ 0 ∥ 𝑀))
101		breq1 4054	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝐷 = 0 → (𝐷 ∥ 𝑁 ↔ 0 ∥ 𝑁))
102	100, 101	anbi12d 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝐷 = 0 → ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ↔ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)))
103	102	anbi2d 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐷 = 0 → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ↔ (0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁))))
104	103	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐷 = 0 ∧ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ↔ (0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁))))
105		simplr 528	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ¬ (𝑀 = 0 ∧ 𝑁 = 0))
106		zdceq 9468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑀 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑀 = 0)
107	42, 106	mpan2 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑀 ∈ ℤ → DECID 𝑀 = 0)
108		ianordc 901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (DECID 𝑀 = 0 → (¬ (𝑀 = 0 ∧ 𝑁 = 0) ↔ (¬ 𝑀 = 0 ∨ ¬ 𝑁 = 0)))
109	107, 108	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑀 ∈ ℤ → (¬ (𝑀 = 0 ∧ 𝑁 = 0) ↔ (¬ 𝑀 = 0 ∨ ¬ 𝑁 = 0)))
110	109	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (¬ (𝑀 = 0 ∧ 𝑁 = 0) ↔ (¬ 𝑀 = 0 ∨ ¬ 𝑁 = 0)))
111	105, 110	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (¬ 𝑀 = 0 ∨ ¬ 𝑁 = 0))
112		dvdszrcl 12178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (0 ∥ 𝑀 → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ))
113		0dvds 12197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑀 ∈ ℤ → (0 ∥ 𝑀 ↔ 𝑀 = 0))
114		pm2.24 622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑀 = 0 → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ))
115	113, 114	biimtrdi 163	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑀 ∈ ℤ → (0 ∥ 𝑀 → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ)))
116	115	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 ∥ 𝑀 → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ)))
117	112, 116	mpcom 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (0 ∥ 𝑀 → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ))
118	117	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ))
119	118	com12 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (¬ 𝑀 = 0 → ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ))
120		dvdszrcl 12178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (0 ∥ 𝑁 → (0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
121		0dvds 12197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑁 ∈ ℤ → (0 ∥ 𝑁 ↔ 𝑁 = 0))
122		pm2.24 622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑁 = 0 → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ))
123	121, 122	biimtrdi 163	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑁 ∈ ℤ → (0 ∥ 𝑁 → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ)))
124	123	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ∥ 𝑁 → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ)))
125	120, 124	mpcom 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (0 ∥ 𝑁 → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ))
126	125	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ))
127	126	com12 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (¬ 𝑁 = 0 → ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ))
128	119, 127	jaoi 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((¬ 𝑀 = 0 ∨ ¬ 𝑁 = 0) → ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ))
129	111, 128	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ))
130	129	adantld 278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)) → 𝐷 ∈ ℕ))
131	130	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐷 = 0 ∧ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)) → 𝐷 ∈ ℕ))
132	104, 131	sylbid 150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐷 = 0 ∧ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ))
133	132	ex 115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐷 = 0 → ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ)))
134	99, 133	jaoi 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐷 ∈ ℕ ∨ 𝐷 = 0) → ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ)))
135	98, 134	sylbi 121	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐷 ∈ ℕ₀ → ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ)))
136	135	impcom 125	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐷 ∈ ℕ₀) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ))
137	136	imp 124	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐷 ∈ ℕ₀) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁))) → 𝐷 ∈ ℕ)
138		dvdsle 12230	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷))
139	97, 137, 138	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐷 ∈ ℕ₀) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁))) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷))
140	139	exp31 364	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐷 ∈ ℕ₀ → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷))))
141	140	com14 88	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∥ 𝐷 → (𝐷 ∈ ℕ₀ → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑦 ≤ 𝐷))))
142	141	imp 124	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑦 ≤ 𝐷)))
143	142	impcom 125	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀)) → ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑦 ≤ 𝐷))
144	143	imp 124	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀)) ∧ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑦 ≤ 𝐷)
145	95, 96, 144	lensymd 8214	. . . . . . . . . . . . . . . . . 18 ⊢ ((((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀)) ∧ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ¬ 𝐷 < 𝑦)
146	145	exp31 364	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → ((𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ₀) → ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ¬ 𝐷 < 𝑦)))
147	92, 146	mpan2d 428	. . . . . . . . . . . . . . . 16 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → (𝑦 ∥ 𝐷 → ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ¬ 𝐷 < 𝑦)))
148	147	com13 80	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑦 ∥ 𝐷 → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → ¬ 𝐷 < 𝑦)))
149	86, 148	syld 45	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → ¬ 𝐷 < 𝑦)))
150	149	com13 80	. . . . . . . . . . . . 13 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ¬ 𝐷 < 𝑦)))
151	150	3impia 1203	. . . . . . . . . . . 12 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ¬ 𝐷 < 𝑦))
152	151	com12 30	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → ¬ 𝐷 < 𝑦))
153	152	expimpd 363	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → ¬ 𝐷 < 𝑦))
154	153	expimpd 363	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) → ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → ¬ 𝐷 < 𝑦))
155	77, 154	sylbi 121	. . . . . . . 8 ⊢ (𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} → ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → ¬ 𝐷 < 𝑦))
156	155	impcom 125	. . . . . . 7 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ 𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}) → ¬ 𝐷 < 𝑦)
157	69	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) → 𝐷 ∈ ℤ)
158	157	ancri 324	. . . . . . . . . . . 12 ⊢ ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) → (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
159	158	3ad2ant2 1022	. . . . . . . . . . 11 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
160	159	ad2antll 491	. . . . . . . . . 10 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
161	160	adantr 276	. . . . . . . . 9 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
162		breq1 4054	. . . . . . . . . . 11 ⊢ (𝑛 = 𝐷 → (𝑛 ∥ 𝑀 ↔ 𝐷 ∥ 𝑀))
163		breq1 4054	. . . . . . . . . . 11 ⊢ (𝑛 = 𝐷 → (𝑛 ∥ 𝑁 ↔ 𝐷 ∥ 𝑁))
164	162, 163	anbi12d 473	. . . . . . . . . 10 ⊢ (𝑛 = 𝐷 → ((𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁) ↔ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
165	164	elrab 2933	. . . . . . . . 9 ⊢ (𝐷 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} ↔ (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
166	161, 165	sylibr 134	. . . . . . . 8 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → 𝐷 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)})
167		breq2 4055	. . . . . . . . 9 ⊢ (𝑧 = 𝐷 → (𝑦 < 𝑧 ↔ 𝑦 < 𝐷))
168	167	adantl 277	. . . . . . . 8 ⊢ ((((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) ∧ 𝑧 = 𝐷) → (𝑦 < 𝑧 ↔ 𝑦 < 𝐷))
169		simprr 531	. . . . . . . 8 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → 𝑦 < 𝐷)
170	166, 168, 169	rspcedvd 2887	. . . . . . 7 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}𝑦 < 𝑧)
171	67, 73, 156, 170	eqsuptid 7114	. . . . . 6 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ) = 𝐷)
172	65, 171	eqtrd 2239	. . . . 5 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 𝐷)
173	172	ancoms 268	. . . 4 ⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 𝐷)
174		gcdmndc 12351	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (𝑀 = 0 ∧ 𝑁 = 0))
175	174	adantr 276	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → DECID (𝑀 = 0 ∧ 𝑁 = 0))
176		exmiddc 838	. . . . 5 ⊢ (DECID (𝑀 = 0 ∧ 𝑁 = 0) → ((𝑀 = 0 ∧ 𝑁 = 0) ∨ ¬ (𝑀 = 0 ∧ 𝑁 = 0)))
177	175, 176	syl 14	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → ((𝑀 = 0 ∧ 𝑁 = 0) ∨ ¬ (𝑀 = 0 ∧ 𝑁 = 0)))
178	63, 173, 177	mpjaodan 800	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 𝐷)
179	23, 178	eqtr2d 2240	. 2 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → 𝐷 = (𝑀 gcd 𝑁))
180	21, 179	impbida 596	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐷 = (𝑀 gcd 𝑁) ↔ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 710 DECID wdc 836 ∧ w3a 981 = wceq 1373 ∈ wcel 2177 ∀wral 2485 {crab 2489 ifcif 3575 class class class wbr 4051 (class class class)co 5957 supcsup 7099 ℝcr 7944 0cc0 7945 < clt 8127 ≤ cle 8128 ℕcn 9056 ℕ₀cn0 9315 ℤcz 9392 ∥ cdvds 12173 gcd cgcd 12349

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-coll 4167 ax-sep 4170 ax-nul 4178 ax-pow 4226 ax-pr 4261 ax-un 4488 ax-setind 4593 ax-iinf 4644 ax-cnex 8036 ax-resscn 8037 ax-1cn 8038 ax-1re 8039 ax-icn 8040 ax-addcl 8041 ax-addrcl 8042 ax-mulcl 8043 ax-mulrcl 8044 ax-addcom 8045 ax-mulcom 8046 ax-addass 8047 ax-mulass 8048 ax-distr 8049 ax-i2m1 8050 ax-0lt1 8051 ax-1rid 8052 ax-0id 8053 ax-rnegex 8054 ax-precex 8055 ax-cnre 8056 ax-pre-ltirr 8057 ax-pre-ltwlin 8058 ax-pre-lttrn 8059 ax-pre-apti 8060 ax-pre-ltadd 8061 ax-pre-mulgt0 8062 ax-pre-mulext 8063 ax-arch 8064 ax-caucvg 8065

This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rmo 2493 df-rab 2494 df-v 2775 df-sbc 3003 df-csb 3098 df-dif 3172 df-un 3174 df-in 3176 df-ss 3183 df-nul 3465 df-if 3576 df-pw 3623 df-sn 3644 df-pr 3645 df-op 3647 df-uni 3857 df-int 3892 df-iun 3935 df-br 4052 df-opab 4114 df-mpt 4115 df-tr 4151 df-id 4348 df-po 4351 df-iso 4352 df-iord 4421 df-on 4423 df-ilim 4424 df-suc 4426 df-iom 4647 df-xp 4689 df-rel 4690 df-cnv 4691 df-co 4692 df-dm 4693 df-rn 4694 df-res 4695 df-ima 4696 df-iota 5241 df-fun 5282 df-fn 5283 df-f 5284 df-f1 5285 df-fo 5286 df-f1o 5287 df-fv 5288 df-riota 5912 df-ov 5960 df-oprab 5961 df-mpo 5962 df-1st 6239 df-2nd 6240 df-recs 6404 df-frec 6490 df-sup 7101 df-pnf 8129 df-mnf 8130 df-xr 8131 df-ltxr 8132 df-le 8133 df-sub 8265 df-neg 8266 df-reap 8668 df-ap 8675 df-div 8766 df-inn 9057 df-2 9115 df-3 9116 df-4 9117 df-n0 9316 df-z 9393 df-uz 9669 df-q 9761 df-rp 9796 df-fz 10151 df-fzo 10285 df-fl 10435 df-mod 10490 df-seqfrec 10615 df-exp 10706 df-cj 11228 df-re 11229 df-im 11230 df-rsqrt 11384 df-abs 11385 df-dvds 12174 df-gcd 12350

This theorem is referenced by: (None)

W3C validator