dfgcd2 - Intuitionistic Logic Explorer

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

Theorem dfgcd2 12530

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 12482	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℕ₀)
2	1	nn0ge0d 9421	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 0 ≤ (𝑀 gcd 𝑁))
3		gcddvds 12479	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁))
4		3anass 1006	. . . . . . . 8 ⊢ ((𝑒 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ (𝑒 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
5		ancom 266	. . . . . . . 8 ⊢ ((𝑒 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑒 ∈ ℤ))
6	4, 5	bitri 184	. . . . . . 7 ⊢ ((𝑒 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑒 ∈ ℤ))
7		dvdsgcd 12528	. . . . . . 7 ⊢ ((𝑒 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))
8	6, 7	sylbir 135	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑒 ∈ ℤ) → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))
9	8	ralrimiva 2603	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))
10	2, 3, 9	3jca 1201	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
11	10	adantr 276	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐷 = (𝑀 gcd 𝑁)) → (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
12		breq2 4086	. . . . 5 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (0 ≤ 𝐷 ↔ 0 ≤ (𝑀 gcd 𝑁)))
13		breq1 4085	. . . . . 6 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (𝐷 ∥ 𝑀 ↔ (𝑀 gcd 𝑁) ∥ 𝑀))
14		breq1 4085	. . . . . 6 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (𝐷 ∥ 𝑁 ↔ (𝑀 gcd 𝑁) ∥ 𝑁))
15	13, 14	anbi12d 473	. . . . 5 ⊢ (𝐷 = (𝑀 gcd 𝑁) → ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ↔ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)))
16		breq2 4086	. . . . . . 7 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (𝑒 ∥ 𝐷 ↔ 𝑒 ∥ (𝑀 gcd 𝑁)))
17	16	imbi2d 230	. . . . . 6 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
18	17	ralbidv 2530	. . . . 5 ⊢ (𝐷 = (𝑀 gcd 𝑁) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))
19	12, 15, 18	3anbi123d 1346	. . . 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 12475	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )))
23	22	adantr 276	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → (𝑀 gcd 𝑁) = if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )))
24		iftrue 3607	. . . . . . 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 4086	. . . . . . . . . . 11 ⊢ (𝑀 = 0 → (𝐷 ∥ 𝑀 ↔ 𝐷 ∥ 0))
27		breq2 4086	. . . . . . . . . . 11 ⊢ (𝑁 = 0 → (𝐷 ∥ 𝑁 ↔ 𝐷 ∥ 0))
28	26, 27	bi2anan9 608	. . . . . . . . . 10 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ↔ (𝐷 ∥ 0 ∧ 𝐷 ∥ 0)))
29		breq2 4086	. . . . . . . . . . . . 13 ⊢ (𝑀 = 0 → (𝑒 ∥ 𝑀 ↔ 𝑒 ∥ 0))
30		breq2 4086	. . . . . . . . . . . . 13 ⊢ (𝑁 = 0 → (𝑒 ∥ 𝑁 ↔ 𝑒 ∥ 0))
31	29, 30	bi2anan9 608	. . . . . . . . . . . 12 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) ↔ (𝑒 ∥ 0 ∧ 𝑒 ∥ 0)))
32	31	imbi1d 231	. . . . . . . . . . 11 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷)))
33	32	ralbidv 2530	. . . . . . . . . 10 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷)))
34	28, 33	3anbi23d 1349	. . . . . . . . 9 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) ↔ (0 ≤ 𝐷 ∧ (𝐷 ∥ 0 ∧ 𝐷 ∥ 0) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷))))
35		dvdszrcl 12298	. . . . . . . . . . . . 13 ⊢ (𝐷 ∥ 0 → (𝐷 ∈ ℤ ∧ 0 ∈ ℤ))
36		dvds0 12312	. . . . . . . . . . . . . . . . . . . 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 2526	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ ℤ ∧ 0 ≤ 𝐷) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) ↔ ∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷))
42		0z 9453	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℤ
43		breq1 4085	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 0 → (𝑒 ∥ 𝐷 ↔ 0 ∥ 𝐷))
44	43	rspcv 2903	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 ∈ ℤ → (∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷 → 0 ∥ 𝐷))
45	42, 44	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷 → 0 ∥ 𝐷)
46		0dvds 12317	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐷 ∈ ℤ → (0 ∥ 𝐷 ↔ 𝐷 = 0))
47	46	biimpd 144	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ∈ ℤ → (0 ∥ 𝐷 → 𝐷 = 0))
48		eqcom 2231	. . . . . . . . . . . . . . . . . . 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 1217	. . . . . . . . 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 2262	. . . . 5 ⊢ (((𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 𝐷)
63	62	ancoms 268	. . . 4 ⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) ∧ (𝑀 = 0 ∧ 𝑁 = 0)) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 𝐷)
64		iffalse 3610	. . . . . . 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 8222	. . . . . . . 8 ⊢ ((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) → (𝑓 = 𝑔 ↔ (¬ 𝑓 < 𝑔 ∧ ¬ 𝑔 < 𝑓)))
67	66	adantl 277	. . . . . . 7 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) → (𝑓 = 𝑔 ↔ (¬ 𝑓 < 𝑔 ∧ ¬ 𝑔 < 𝑓)))
68		dvdszrcl 12298	. . . . . . . . . . . 12 ⊢ (𝐷 ∥ 𝑀 → (𝐷 ∈ ℤ ∧ 𝑀 ∈ ℤ))
69	68	simpld 112	. . . . . . . . . . 11 ⊢ (𝐷 ∥ 𝑀 → 𝐷 ∈ ℤ)
70	69	zred 9565	. . . . . . . . . 10 ⊢ (𝐷 ∥ 𝑀 → 𝐷 ∈ ℝ)
71	70	adantr 276	. . . . . . . . 9 ⊢ ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) → 𝐷 ∈ ℝ)
72	71	3ad2ant2 1043	. . . . . . . 8 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → 𝐷 ∈ ℝ)
73	72	ad2antll 491	. . . . . . 7 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → 𝐷 ∈ ℝ)
74		breq1 4085	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑦 → (𝑛 ∥ 𝑀 ↔ 𝑦 ∥ 𝑀))
75		breq1 4085	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑦 → (𝑛 ∥ 𝑁 ↔ 𝑦 ∥ 𝑁))
76	74, 75	anbi12d 473	. . . . . . . . . 10 ⊢ (𝑛 = 𝑦 → ((𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁) ↔ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)))
77	76	elrab 2959	. . . . . . . . 9 ⊢ (𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} ↔ (𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)))
78		breq1 4085	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑦 → (𝑒 ∥ 𝑀 ↔ 𝑦 ∥ 𝑀))
79		breq1 4085	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑦 → (𝑒 ∥ 𝑁 ↔ 𝑦 ∥ 𝑁))
80	78, 79	anbi12d 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑦 → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) ↔ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)))
81		breq1 4085	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑦 → (𝑒 ∥ 𝐷 ↔ 𝑦 ∥ 𝐷))
82	80, 81	imbi12d 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑦 → (((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ((𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁) → 𝑦 ∥ 𝐷)))
83	82	rspcv 2903	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℤ → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → ((𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁) → 𝑦 ∥ 𝐷)))
84	83	com23 78	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℤ → ((𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → 𝑦 ∥ 𝐷)))
85	84	imp 124	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → 𝑦 ∥ 𝐷))
86	85	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → 𝑦 ∥ 𝐷))
87		elnn0z 9455	. . . . . . . . . . . . . . . . . . . . . 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 9446	. . . . . . . . . . . . . . . . . . . . 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 9367	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐷 ∈ ℕ₀ ↔ (𝐷 ∈ ℕ ∨ 𝐷 = 0))
99		2a1 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐷 ∈ ℕ → ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ)))
100		breq1 4085	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝐷 = 0 → (𝐷 ∥ 𝑀 ↔ 0 ∥ 𝑀))
101		breq1 4085	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑀 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑀 = 0)
107	42, 106	mpan2 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑀 ∈ ℤ → DECID 𝑀 = 0)
108		ianordc 904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (0 ∥ 𝑀 → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ))
113		0dvds 12317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑀 ∈ ℤ → (0 ∥ 𝑀 ↔ 𝑀 = 0))
114		pm2.24 624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (0 ∥ 𝑁 → (0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
121		0dvds 12317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑁 ∈ ℤ → (0 ∥ 𝑁 ↔ 𝑁 = 0))
122		pm2.24 624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 721	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12350	. . . . . . . . . . . . . . . . . . . . . . . . 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 8264	. . . . . . . . . . . . . . . . . 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 1224	. . . . . . . . . . . 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 1043	. . . . . . . . . . 11 ⊢ ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
160	159	ad2antll 491	. . . . . . . . . 10 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
161	160	adantr 276	. . . . . . . . 9 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
162		breq1 4085	. . . . . . . . . . 11 ⊢ (𝑛 = 𝐷 → (𝑛 ∥ 𝑀 ↔ 𝐷 ∥ 𝑀))
163		breq1 4085	. . . . . . . . . . 11 ⊢ (𝑛 = 𝐷 → (𝑛 ∥ 𝑁 ↔ 𝐷 ∥ 𝑁))
164	162, 163	anbi12d 473	. . . . . . . . . 10 ⊢ (𝑛 = 𝐷 → ((𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁) ↔ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
165	164	elrab 2959	. . . . . . . . 9 ⊢ (𝐷 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} ↔ (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)))
166	161, 165	sylibr 134	. . . . . . . 8 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → 𝐷 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)})
167		breq2 4086	. . . . . . . . 9 ⊢ (𝑧 = 𝐷 → (𝑦 < 𝑧 ↔ 𝑦 < 𝐷))
168	167	adantl 277	. . . . . . . 8 ⊢ ((((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) ∧ 𝑧 = 𝐷) → (𝑦 < 𝑧 ↔ 𝑦 < 𝐷))
169		simprr 531	. . . . . . . 8 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → 𝑦 < 𝐷)
170	166, 168, 169	rspcedvd 2913	. . . . . . 7 ⊢ (((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}𝑦 < 𝑧)
171	67, 73, 156, 170	eqsuptid 7160	. . . . . 6 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ) = 𝐷)
172	65, 171	eqtrd 2262	. . . . 5 ⊢ ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 𝐷)
173	172	ancoms 268	. . . 4 ⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 𝐷)
174		gcdmndc 12471	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (𝑀 = 0 ∧ 𝑁 = 0))
175	174	adantr 276	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → DECID (𝑀 = 0 ∧ 𝑁 = 0))
176		exmiddc 841	. . . . 5 ⊢ (DECID (𝑀 = 0 ∧ 𝑁 = 0) → ((𝑀 = 0 ∧ 𝑁 = 0) ∨ ¬ (𝑀 = 0 ∧ 𝑁 = 0)))
177	175, 176	syl 14	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → ((𝑀 = 0 ∧ 𝑁 = 0) ∨ ¬ (𝑀 = 0 ∧ 𝑁 = 0)))
178	63, 173, 177	mpjaodan 803	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 𝐷)
179	23, 178	eqtr2d 2263	. 2 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → 𝐷 = (𝑀 gcd 𝑁))
180	21, 179	impbida 598	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐷 = (𝑀 gcd 𝑁) ↔ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 713 DECID wdc 839 ∧ w3a 1002 = wceq 1395 ∈ wcel 2200 ∀wral 2508 {crab 2512 ifcif 3602 class class class wbr 4082 (class class class)co 6000 supcsup 7145 ℝcr 7994 0cc0 7995 < clt 8177 ≤ cle 8178 ℕcn 9106 ℕ₀cn0 9365 ℤcz 9442 ∥ cdvds 12293 gcd cgcd 12469

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4198 ax-sep 4201 ax-nul 4209 ax-pow 4257 ax-pr 4292 ax-un 4523 ax-setind 4628 ax-iinf 4679 ax-cnex 8086 ax-resscn 8087 ax-1cn 8088 ax-1re 8089 ax-icn 8090 ax-addcl 8091 ax-addrcl 8092 ax-mulcl 8093 ax-mulrcl 8094 ax-addcom 8095 ax-mulcom 8096 ax-addass 8097 ax-mulass 8098 ax-distr 8099 ax-i2m1 8100 ax-0lt1 8101 ax-1rid 8102 ax-0id 8103 ax-rnegex 8104 ax-precex 8105 ax-cnre 8106 ax-pre-ltirr 8107 ax-pre-ltwlin 8108 ax-pre-lttrn 8109 ax-pre-apti 8110 ax-pre-ltadd 8111 ax-pre-mulgt0 8112 ax-pre-mulext 8113 ax-arch 8114 ax-caucvg 8115

This theorem depends on definitions: df-bi 117 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-if 3603 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3888 df-int 3923 df-iun 3966 df-br 4083 df-opab 4145 df-mpt 4146 df-tr 4182 df-id 4383 df-po 4386 df-iso 4387 df-iord 4456 df-on 4458 df-ilim 4459 df-suc 4461 df-iom 4682 df-xp 4724 df-rel 4725 df-cnv 4726 df-co 4727 df-dm 4728 df-rn 4729 df-res 4730 df-ima 4731 df-iota 5277 df-fun 5319 df-fn 5320 df-f 5321 df-f1 5322 df-fo 5323 df-f1o 5324 df-fv 5325 df-riota 5953 df-ov 6003 df-oprab 6004 df-mpo 6005 df-1st 6284 df-2nd 6285 df-recs 6449 df-frec 6535 df-sup 7147 df-pnf 8179 df-mnf 8180 df-xr 8181 df-ltxr 8182 df-le 8183 df-sub 8315 df-neg 8316 df-reap 8718 df-ap 8725 df-div 8816 df-inn 9107 df-2 9165 df-3 9166 df-4 9167 df-n0 9366 df-z 9443 df-uz 9719 df-q 9811 df-rp 9846 df-fz 10201 df-fzo 10335 df-fl 10485 df-mod 10540 df-seqfrec 10665 df-exp 10756 df-cj 11348 df-re 11349 df-im 11350 df-rsqrt 11504 df-abs 11505 df-dvds 12294 df-gcd 12470

This theorem is referenced by: (None)

W3C validator