divalglemeuneg - Intuitionistic Logic Explorer

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

Theorem divalglemeuneg 12634

Description: Lemma for divalg 12635. 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 8804	. . 3 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → 𝐷 ≠ 0)
3		divalglemex 12633	. . 3 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
4	2, 3	syld3an3 1319	. 2 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
5		nfv 1577	. . . . . 6 ⊢ Ⅎ𝑞((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ))
6		nfre1 2587	. . . . . . 7 ⊢ Ⅎ𝑞∃𝑞 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠))
7		nfv 1577	. . . . . . 7 ⊢ Ⅎ𝑞 𝑟 = 𝑠
8	6, 7	nfim 1621	. . . . . 6 ⊢ Ⅎ𝑞(∃𝑞 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠)) → 𝑟 = 𝑠)
9		oveq1 6065	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑡 → (𝑞 · 𝐷) = (𝑡 · 𝐷))
10	9	oveq1d 6073	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑡 → ((𝑞 · 𝐷) + 𝑠) = ((𝑡 · 𝐷) + 𝑠))
11	10	eqeq2d 2246	. . . . . . . . . 10 ⊢ (𝑞 = 𝑡 → (𝑁 = ((𝑞 · 𝐷) + 𝑠) ↔ 𝑁 = ((𝑡 · 𝐷) + 𝑠)))
12	11	3anbi3d 1355	. . . . . . . . 9 ⊢ (𝑞 = 𝑡 → ((0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠)) ↔ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))))
13	12	cbvrexv 2781	. . . . . . . 8 ⊢ (∃𝑞 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠)) ↔ ∃𝑡 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠)))
14		simpr 110	. . . . . . . . . . . 12 ⊢ ((((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) ∧ 𝑞 < 𝑡) → 𝑞 < 𝑡)
15		simp2 1025	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → 𝐷 ∈ ℤ)
16	15	znegcld 9720	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → -𝐷 ∈ ℤ)
17	15	zred 9718	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → 𝐷 ∈ ℝ)
18	17	lt0neg1d 8806	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → (𝐷 < 0 ↔ 0 < -𝐷))
19	1, 18	mpbid 147	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → 0 < -𝐷)
20		elnnz 9604	. . . . . . . . . . . . . . . . 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 9720	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → -𝑡 ∈ ℤ)
29		simpr 110	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) → 𝑞 ∈ ℤ)
30	29	ad3antrrr 492	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑞 ∈ ℤ)
31	30	znegcld 9720	. . . . . . . . . . . . . . 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 9718	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝐷 ∈ ℝ)
38		0red 8291	. . . . . . . . . . . . . . . . . 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 8408	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝐷 ≤ 0)
42	37, 41	absnidd 11870	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → (abs‘𝐷) = -𝐷)
43	34, 42	breqtrd 4140	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑠 < -𝐷)
44		simpr3 1032	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑁 = ((𝑡 · 𝐷) + 𝑠))
45	27	zcnd 9719	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑡 ∈ ℂ)
46	36	zcnd 9719	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝐷 ∈ ℂ)
47	45, 46	mul2negd 8703	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → (-𝑡 · -𝐷) = (𝑡 · 𝐷))
48	47	oveq1d 6073	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → ((-𝑡 · -𝐷) + 𝑠) = ((𝑡 · 𝐷) + 𝑠))
49	44, 48	eqtr4d 2270	. . . . . . . . . . . . . . . 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 9719	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑞 ∈ ℂ)
53	52, 46	mul2negd 8703	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → (-𝑞 · -𝐷) = (𝑞 · 𝐷))
54	53	oveq1d 6073	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → ((-𝑞 · -𝐷) + 𝑟) = ((𝑞 · 𝐷) + 𝑟))
55	51, 54	eqtr4d 2270	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑁 = ((-𝑞 · -𝐷) + 𝑟))
56	49, 55	eqtr3d 2269	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → ((-𝑡 · -𝐷) + 𝑠) = ((-𝑞 · -𝐷) + 𝑟))
57	22, 24, 26, 28, 31, 33, 43, 56	divalglemnqt 12631	. . . . . . . . . . . . . 14 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → ¬ -𝑡 < -𝑞)
58	30	zred 9718	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑞 ∈ ℝ)
59	27	zred 9718	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑡 ∈ ℝ)
60	58, 59	ltnegd 8814	. . . . . . . . . . . . . 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 2269	. . . . . . . . . . . 12 ⊢ ((((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) ∧ 𝑞 = 𝑡) → ((𝑞 · 𝐷) + 𝑟) = ((𝑡 · 𝐷) + 𝑠))
73	64, 65, 66, 67, 68, 69, 72	divalglemqt 12630	. . . . . . . . . . 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 4140	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → 𝑟 < -𝐷)
79	55, 49	eqtr3d 2269	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → ((-𝑞 · -𝐷) + 𝑟) = ((-𝑡 · -𝐷) + 𝑠))
80	22, 26, 24, 31, 28, 75, 78, 79	divalglemnqt 12631	. . . . . . . . . . . . . 14 ⊢ (((((((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ 𝑞 ∈ ℤ) ∧ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) ∧ 𝑡 ∈ ℤ) ∧ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑡 · 𝐷) + 𝑠))) → ¬ -𝑞 < -𝑡)
81	59, 58	ltnegd 8814	. . . . . . . . . . . . . 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 9637	. . . . . . . . . . . 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 2662	. . . . . . . 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 2659	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) → (∃𝑞 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠)) → 𝑟 = 𝑠)))
95	94	impd 254	. . . 4 ⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ∧ ∃𝑞 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠))) → 𝑟 = 𝑠))
96	95	ralrimivva 2626	. . 3 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → ∀𝑟 ∈ ℤ ∀𝑠 ∈ ℤ ((∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ∧ ∃𝑞 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠))) → 𝑟 = 𝑠))
97		breq2 4118	. . . . . 6 ⊢ (𝑟 = 𝑠 → (0 ≤ 𝑟 ↔ 0 ≤ 𝑠))
98		breq1 4117	. . . . . 6 ⊢ (𝑟 = 𝑠 → (𝑟 < (abs‘𝐷) ↔ 𝑠 < (abs‘𝐷)))
99		oveq2 6066	. . . . . . 7 ⊢ (𝑟 = 𝑠 → ((𝑞 · 𝐷) + 𝑟) = ((𝑞 · 𝐷) + 𝑠))
100	99	eqeq2d 2246	. . . . . 6 ⊢ (𝑟 = 𝑠 → (𝑁 = ((𝑞 · 𝐷) + 𝑟) ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑠)))
101	97, 98, 100	3anbi123d 1349	. . . . 5 ⊢ (𝑟 = 𝑠 → ((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠))))
102	101	rexbidv 2545	. . . 4 ⊢ (𝑟 = 𝑠 → (∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃𝑞 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠))))
103	102	rmo4 3013	. . 3 ⊢ (∃*𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∀𝑟 ∈ ℤ ∀𝑠 ∈ ℤ ((∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ∧ ∃𝑞 ∈ ℤ (0 ≤ 𝑠 ∧ 𝑠 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑠))) → 𝑟 = 𝑠))
104	96, 103	sylibr 134	. 2 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → ∃*𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
105		reu5 2764	. 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 2205 ≠ wne 2414 ∀wral 2522 ∃wrex 2523 ∃!wreu 2524 ∃*wrmo 2525 class class class wbr 4114 ‘cfv 5357 (class class class)co 6058 0cc0 8143 + caddc 8146 · cmul 8148 < clt 8324 ≤ cle 8325 -cneg 8461 ℕcn 9254 ℤcz 9594 abscabs 11707

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 2207 ax-14 2208 ax-ext 2216 ax-coll 4230 ax-sep 4233 ax-nul 4241 ax-pow 4292 ax-pr 4327 ax-un 4559 ax-setind 4664 ax-iinf 4715 ax-cnex 8234 ax-resscn 8235 ax-1cn 8236 ax-1re 8237 ax-icn 8238 ax-addcl 8239 ax-addrcl 8240 ax-mulcl 8241 ax-mulrcl 8242 ax-addcom 8243 ax-mulcom 8244 ax-addass 8245 ax-mulass 8246 ax-distr 8247 ax-i2m1 8248 ax-0lt1 8249 ax-1rid 8250 ax-0id 8251 ax-rnegex 8252 ax-precex 8253 ax-cnre 8254 ax-pre-ltirr 8255 ax-pre-ltwlin 8256 ax-pre-lttrn 8257 ax-pre-apti 8258 ax-pre-ltadd 8259 ax-pre-mulgt0 8260 ax-pre-mulext 8261 ax-arch 8262

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 2085 df-mo 2086 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ne 2415 df-nel 2510 df-ral 2527 df-rex 2528 df-reu 2529 df-rmo 2530 df-rab 2531 df-v 2817 df-sbc 3046 df-csb 3142 df-dif 3216 df-un 3218 df-in 3220 df-ss 3227 df-nul 3513 df-if 3625 df-pw 3676 df-sn 3700 df-pr 3701 df-op 3703 df-uni 3920 df-int 3955 df-iun 3998 df-br 4115 df-opab 4177 df-mpt 4178 df-tr 4214 df-id 4419 df-po 4422 df-iso 4423 df-iord 4492 df-on 4494 df-ilim 4495 df-suc 4497 df-iom 4718 df-xp 4760 df-rel 4761 df-cnv 4762 df-co 4763 df-dm 4764 df-rn 4765 df-res 4766 df-ima 4767 df-iota 5317 df-fun 5359 df-fn 5360 df-f 5361 df-f1 5362 df-fo 5363 df-f1o 5364 df-fv 5365 df-riota 6011 df-ov 6061 df-oprab 6062 df-mpo 6063 df-1st 6347 df-2nd 6348 df-recs 6549 df-frec 6635 df-pnf 8326 df-mnf 8327 df-xr 8328 df-ltxr 8329 df-le 8330 df-sub 8462 df-neg 8463 df-reap 8866 df-ap 8873 df-div 8964 df-inn 9255 df-2 9313 df-n0 9514 df-z 9595 df-uz 9872 df-q 9970 df-rp 10005 df-fl 10654 df-mod 10709 df-seqfrec 10834 df-exp 10925 df-cj 11552 df-re 11553 df-im 11554 df-rsqrt 11708 df-abs 11709

This theorem is referenced by: divalg 12635

W3C validator