divalglemeuneg - Intuitionistic Logic Explorer

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

Theorem divalglemeuneg 12609

Description: Lemma for divalg 12610. Uniqueness for a negative denominator. (Contributed by Jim Kingdon, 4-Dec-2021.)

**Assertion**
Ref	Expression
divalglemeuneg	⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))

Distinct variable groups: 𝐷,𝑞,𝑟 𝑁,𝑞,𝑟

Proof of Theorem divalglemeuneg Dummy variables 𝑠 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp3 1026	. . . 4 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → 𝐷 < 0)
2	1	lt0ne0d 8787	. . 3 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → 𝐷 ≠ 0)
3		divalglemex 12608	. . 3 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
4	2, 3	syld3an3 1319	. 2 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
5		nfv 1577	. . . . . 6 ⊢ Ⅎ𝑞((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ))
6		nfre1 2585	. . . . . . 7 ⊢ Ⅎ𝑞∃𝑞 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠))
7		nfv 1577	. . . . . . 7 ⊢ Ⅎ𝑞 𝑟 = 𝑠
8	6, 7	nfim 1621	. . . . . 6 ⊢ Ⅎ𝑞(∃𝑞 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠)) → 𝑟 = 𝑠)
9		oveq1 6057	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑡 → (𝑞 · 𝐷) = (𝑡 · 𝐷))
10	9	oveq1d 6065	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑡 → ((𝑞 · 𝐷) + 𝑠) = ((𝑡 · 𝐷) + 𝑠))
11	10	eqeq2d 2244	. . . . . . . . . 10 ⊢ (𝑞 = 𝑡 → (𝑁 = ((𝑞 · 𝐷) + 𝑠) ↔ 𝑁 = ((𝑡 · 𝐷) + 𝑠)))
12	11	3anbi3d 1355	. . . . . . . . 9 ⊢ (𝑞 = 𝑡 → ((0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠)) ↔ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))))
13	12	cbvrexv 2779	. . . . . . . 8 ⊢ (∃𝑞 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠)) ↔ ∃𝑡 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠)))
14		simpr 110	. . . . . . . . . . . 12 ⊢ ((((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) ∧ 𝑞 < 𝑡) → 𝑞 < 𝑡)
15		simp2 1025	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → 𝐷 ∈ ℤ)
16	15	znegcld 9702	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → -𝐷 ∈ ℤ)
17	15	zred 9700	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → 𝐷 ∈ ℝ)
18	17	lt0neg1d 8789	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → (𝐷 < 0 ↔ 0 < -𝐷))
19	1, 18	mpbid 147	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → 0 < -𝐷)
20		elnnz 9587	. . . . . . . . . . . . . . . . 17 ⊢ (-𝐷 ∈ ℕ ↔ (-𝐷 ∈ ℤ ∧ 0 < -𝐷))
21	16, 19, 20	sylanbrc 417	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → -𝐷 ∈ ℕ)
22	21	ad5antr 496	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → -𝐷 ∈ ℕ)
23		simplrr 538	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) → 𝑠 ∈ ℤ)
24	23	ad3antrrr 492	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑠 ∈ ℤ)
25		simplrl 537	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) → 𝑟 ∈ ℤ)
26	25	ad3antrrr 492	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑟 ∈ ℤ)
27		simplr 529	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑡 ∈ ℤ)
28	27	znegcld 9702	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → -𝑡 ∈ ℤ)
29		simpr 110	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) → 𝑞 ∈ ℤ)
30	29	ad3antrrr 492	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑞 ∈ ℤ)
31	30	znegcld 9702	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → -𝑞 ∈ ℤ)
32		simpr1 1030	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) → 0 ≤ 𝑟)
33	32	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 0 ≤ 𝑟)
34		simpr2 1031	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑠 < (abs‘𝐷))
35		simpll2 1064	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) → 𝐷 ∈ ℤ)
36	35	ad3antrrr 492	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝐷 ∈ ℤ)
37	36	zred 9700	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝐷 ∈ ℝ)
38		0red 8275	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 0 ∈ ℝ)
39		simpll3 1065	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) → 𝐷 < 0)
40	39	ad3antrrr 492	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝐷 < 0)
41	37, 38, 40	ltled 8392	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝐷 ≤ 0)
42	37, 41	absnidd 11845	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → (abs‘𝐷) = -𝐷)
43	34, 42	breqtrd 4135	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑠 < -𝐷)
44		simpr3 1032	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑁 = ((𝑡 · 𝐷) + 𝑠))
45	27	zcnd 9701	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑡 ∈ ℂ)
46	36	zcnd 9701	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝐷 ∈ ℂ)
47	45, 46	mul2negd 8686	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → (-𝑡 · -𝐷) = (𝑡 · 𝐷))
48	47	oveq1d 6065	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → ((-𝑡 · -𝐷) + 𝑠) = ((𝑡 · 𝐷) + 𝑠))
49	44, 48	eqtr4d 2268	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑁 = ((-𝑡 · -𝐷) + 𝑠))
50		simpr3 1032	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) → 𝑁 = ((𝑞 · 𝐷) + 𝑟))
51	50	ad2antrr 488	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑁 = ((𝑞 · 𝐷) + 𝑟))
52	30	zcnd 9701	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑞 ∈ ℂ)
53	52, 46	mul2negd 8686	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → (-𝑞 · -𝐷) = (𝑞 · 𝐷))
54	53	oveq1d 6065	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → ((-𝑞 · -𝐷) + 𝑟) = ((𝑞 · 𝐷) + 𝑟))
55	51, 54	eqtr4d 2268	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑁 = ((-𝑞 · -𝐷) + 𝑟))
56	49, 55	eqtr3d 2267	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → ((-𝑡 · -𝐷) + 𝑠) = ((-𝑞 · -𝐷) + 𝑟))
57	22, 24, 26, 28, 31, 33, 43, 56	divalglemnqt 12606	. . . . . . . . . . . . . 14 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → ¬ -𝑡 < -𝑞)
58	30	zred 9700	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑞 ∈ ℝ)
59	27	zred 9700	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑡 ∈ ℝ)
60	58, 59	ltnegd 8797	. . . . . . . . . . . . . 14 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → (𝑞 < 𝑡 ↔ -𝑡 < -𝑞))
61	57, 60	mtbird 680	. . . . . . . . . . . . 13 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → ¬ 𝑞 < 𝑡)
62	61	adantr 276	. . . . . . . . . . . 12 ⊢ ((((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) ∧ 𝑞 < 𝑡) → ¬ 𝑞 < 𝑡)
63	14, 62	pm2.21dd 625	. . . . . . . . . . 11 ⊢ ((((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) ∧ 𝑞 < 𝑡) → 𝑟 = 𝑠)
64	36	adantr 276	. . . . . . . . . . . 12 ⊢ ((((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) ∧ 𝑞 = 𝑡) → 𝐷 ∈ ℤ)
65	26	adantr 276	. . . . . . . . . . . 12 ⊢ ((((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) ∧ 𝑞 = 𝑡) → 𝑟 ∈ ℤ)
66	24	adantr 276	. . . . . . . . . . . 12 ⊢ ((((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) ∧ 𝑞 = 𝑡) → 𝑠 ∈ ℤ)
67	30	adantr 276	. . . . . . . . . . . 12 ⊢ ((((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) ∧ 𝑞 = 𝑡) → 𝑞 ∈ ℤ)
68	27	adantr 276	. . . . . . . . . . . 12 ⊢ ((((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) ∧ 𝑞 = 𝑡) → 𝑡 ∈ ℤ)
69		simpr 110	. . . . . . . . . . . 12 ⊢ ((((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) ∧ 𝑞 = 𝑡) → 𝑞 = 𝑡)
70	51	adantr 276	. . . . . . . . . . . . 13 ⊢ ((((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) ∧ 𝑞 = 𝑡) → 𝑁 = ((𝑞 · 𝐷) + 𝑟))
71	44	adantr 276	. . . . . . . . . . . . 13 ⊢ ((((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) ∧ 𝑞 = 𝑡) → 𝑁 = ((𝑡 · 𝐷) + 𝑠))
72	70, 71	eqtr3d 2267	. . . . . . . . . . . 12 ⊢ ((((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) ∧ 𝑞 = 𝑡) → ((𝑞 · 𝐷) + 𝑟) = ((𝑡 · 𝐷) + 𝑠))
73	64, 65, 66, 67, 68, 69, 72	divalglemqt 12605	. . . . . . . . . . 11 ⊢ ((((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) ∧ 𝑞 = 𝑡) → 𝑟 = 𝑠)
74		simpr 110	. . . . . . . . . . . 12 ⊢ ((((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) ∧ 𝑡 < 𝑞) → 𝑡 < 𝑞)
75		simpr1 1030	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 0 ≤ 𝑠)
76		simpr2 1031	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) → 𝑟 < (abs‘𝐷))
77	76	ad2antrr 488	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑟 < (abs‘𝐷))
78	77, 42	breqtrd 4135	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑟 < -𝐷)
79	55, 49	eqtr3d 2267	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → ((-𝑞 · -𝐷) + 𝑟) = ((-𝑡 · -𝐷) + 𝑠))
80	22, 26, 24, 31, 28, 75, 78, 79	divalglemnqt 12606	. . . . . . . . . . . . . 14 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → ¬ -𝑞 < -𝑡)
81	59, 58	ltnegd 8797	. . . . . . . . . . . . . 14 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → (𝑡 < 𝑞 ↔ -𝑞 < -𝑡))
82	80, 81	mtbird 680	. . . . . . . . . . . . 13 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → ¬ 𝑡 < 𝑞)
83	82	adantr 276	. . . . . . . . . . . 12 ⊢ ((((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) ∧ 𝑡 < 𝑞) → ¬ 𝑡 < 𝑞)
84	74, 83	pm2.21dd 625	. . . . . . . . . . 11 ⊢ ((((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) ∧ 𝑡 < 𝑞) → 𝑟 = 𝑠)
85		simplr 529	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) → 𝑞 ∈ ℤ)
86	85	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑞 ∈ ℤ)
87		ztri3or 9620	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℤ ∧ 𝑡 ∈ ℤ) → (𝑞 < 𝑡 ∨ 𝑞 = 𝑡 ∨ 𝑡 < 𝑞))
88	86, 27, 87	syl2anc 411	. . . . . . . . . . 11 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → (𝑞 < 𝑡 ∨ 𝑞 = 𝑡 ∨ 𝑡 < 𝑞))
89	63, 73, 84, 88	mpjao3dan 1344	. . . . . . . . . 10 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑟 = 𝑠)
90	89	ex 115	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) → ((0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠)) → 𝑟 = 𝑠))
91	90	rexlimdva 2660	. . . . . . . 8 ⊢ (((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) → (∃𝑡 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠)) → 𝑟 = 𝑠))
92	13, 91	biimtrid 152	. . . . . . 7 ⊢ (((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) → (∃𝑞 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠)) → 𝑟 = 𝑠))
93	92	exp31 364	. . . . . 6 ⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝑞 ∈ ℤ → ((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) → (∃𝑞 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠)) → 𝑟 = 𝑠))))
94	5, 8, 93	rexlimd 2657	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) → (∃𝑞 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠)) → 𝑟 = 𝑠)))
95	94	impd 254	. . . 4 ⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ∧ ∃𝑞 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠))) → 𝑟 = 𝑠))
96	95	ralrimivva 2624	. . 3 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → ∀𝑟 ∈ ℤ ∀𝑠 ∈ ℤ ((∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ∧ ∃𝑞 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠))) → 𝑟 = 𝑠))
97		breq2 4113	. . . . . 6 ⊢ (𝑟 = 𝑠 → (0 ≤ 𝑟 ↔ 0 ≤ 𝑠))
98		breq1 4112	. . . . . 6 ⊢ (𝑟 = 𝑠 → (𝑟 < (abs‘𝐷) ↔ 𝑠 < (abs‘𝐷)))
99		oveq2 6058	. . . . . . 7 ⊢ (𝑟 = 𝑠 → ((𝑞 · 𝐷) + 𝑟) = ((𝑞 · 𝐷) + 𝑠))
100	99	eqeq2d 2244	. . . . . 6 ⊢ (𝑟 = 𝑠 → (𝑁 = ((𝑞 · 𝐷) + 𝑟) ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑠)))
101	97, 98, 100	3anbi123d 1349	. . . . 5 ⊢ (𝑟 = 𝑠 → ((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠))))
102	101	rexbidv 2543	. . . 4 ⊢ (𝑟 = 𝑠 → (∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃𝑞 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠))))
103	102	rmo4 3010	. . 3 ⊢ (∃*𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∀𝑟 ∈ ℤ ∀𝑠 ∈ ℤ ((∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ∧ ∃𝑞 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠))) → 𝑟 = 𝑠))
104	96, 103	sylibr 134	. 2 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → ∃*𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
105		reu5 2762	. 2 ⊢ (∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ (∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ∧ ∃*𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))))
106	4, 104, 105	sylanbrc 417	1 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ∨ w3o 1004 ∧ w3a 1005 = wceq 1398 ∈ wcel 2203 ≠ wne 2412 ∀wral 2520 ∃wrex 2521 ∃!wreu 2522 ∃*wrmo 2523 class class class wbr 4109 ‘cfv 5352 (class class class)co 6050 0cc0 8127 + caddc 8130 · cmul 8132 < clt 8308 ≤ cle 8309 -cneg 8445 ℕcn 9237 ℤcz 9577 abscabs 11682

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2205 ax-14 2206 ax-ext 2214 ax-coll 4225 ax-sep 4228 ax-nul 4236 ax-pow 4287 ax-pr 4322 ax-un 4554 ax-setind 4659 ax-iinf 4710 ax-cnex 8218 ax-resscn 8219 ax-1cn 8220 ax-1re 8221 ax-icn 8222 ax-addcl 8223 ax-addrcl 8224 ax-mulcl 8225 ax-mulrcl 8226 ax-addcom 8227 ax-mulcom 8228 ax-addass 8229 ax-mulass 8230 ax-distr 8231 ax-i2m1 8232 ax-0lt1 8233 ax-1rid 8234 ax-0id 8235 ax-rnegex 8236 ax-precex 8237 ax-cnre 8238 ax-pre-ltirr 8239 ax-pre-ltwlin 8240 ax-pre-lttrn 8241 ax-pre-apti 8242 ax-pre-ltadd 8243 ax-pre-mulgt0 8244 ax-pre-mulext 8245 ax-arch 8246

This theorem depends on definitions: df-bi 117 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2083 df-mo 2084 df-clab 2219 df-cleq 2225 df-clel 2228 df-nfc 2373 df-ne 2413 df-nel 2508 df-ral 2525 df-rex 2526 df-reu 2527 df-rmo 2528 df-rab 2529 df-v 2815 df-sbc 3043 df-csb 3139 df-dif 3213 df-un 3215 df-in 3217 df-ss 3224 df-nul 3509 df-if 3621 df-pw 3671 df-sn 3695 df-pr 3696 df-op 3698 df-uni 3915 df-int 3950 df-iun 3993 df-br 4110 df-opab 4172 df-mpt 4173 df-tr 4209 df-id 4414 df-po 4417 df-iso 4418 df-iord 4487 df-on 4489 df-ilim 4490 df-suc 4492 df-iom 4713 df-xp 4755 df-rel 4756 df-cnv 4757 df-co 4758 df-dm 4759 df-rn 4760 df-res 4761 df-ima 4762 df-iota 5312 df-fun 5354 df-fn 5355 df-f 5356 df-f1 5357 df-fo 5358 df-f1o 5359 df-fv 5360 df-riota 6003 df-ov 6053 df-oprab 6054 df-mpo 6055 df-1st 6334 df-2nd 6335 df-recs 6536 df-frec 6622 df-pnf 8310 df-mnf 8311 df-xr 8312 df-ltxr 8313 df-le 8314 df-sub 8446 df-neg 8447 df-reap 8849 df-ap 8856 df-div 8947 df-inn 9238 df-2 9296 df-n0 9497 df-z 9578 df-uz 9854 df-q 9952 df-rp 9987 df-fl 10630 df-mod 10685 df-seqfrec 10810 df-exp 10901 df-cj 11527 df-re 11528 df-im 11529 df-rsqrt 11683 df-abs 11684

This theorem is referenced by: divalg 12610

W3C validator