divalgb - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > divalgb		Structured version Visualization version GIF version

Theorem divalgb 16351

Description: Express the division algorithm as stated in divalg 16350 in terms of ∥. (Contributed by Paul Chapman, 31-Mar-2011.)

**Assertion**
Ref	Expression
divalgb	⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃!𝑟 ∈ ℕ₀ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))))

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

**Proof of Theorem divalgb**
Step	Hyp	Ref	Expression
1		df-3an 1086	. . . . . . . . 9 ⊢ ((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷)) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
2	1	rexbii 3088	. . . . . . . 8 ⊢ (∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃𝑞 ∈ ℤ ((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷)) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
3		r19.42v 3184	. . . . . . . 8 ⊢ (∃𝑞 ∈ ℤ ((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷)) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷)) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
4	2, 3	bitri 275	. . . . . . 7 ⊢ (∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷)) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
5		zsubcl 12605	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (𝑁 − 𝑟) ∈ ℤ)
6		divides 16203	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ ℤ ∧ (𝑁 − 𝑟) ∈ ℤ) → (𝐷 ∥ (𝑁 − 𝑟) ↔ ∃𝑞 ∈ ℤ (𝑞 · 𝐷) = (𝑁 − 𝑟)))
7	5, 6	sylan2 592	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ)) → (𝐷 ∥ (𝑁 − 𝑟) ↔ ∃𝑞 ∈ ℤ (𝑞 · 𝐷) = (𝑁 − 𝑟)))
8	7	3impb 1112	. . . . . . . . . 10 ⊢ ((𝐷 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (𝐷 ∥ (𝑁 − 𝑟) ↔ ∃𝑞 ∈ ℤ (𝑞 · 𝐷) = (𝑁 − 𝑟)))
9	8	3com12 1120	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (𝐷 ∥ (𝑁 − 𝑟) ↔ ∃𝑞 ∈ ℤ (𝑞 · 𝐷) = (𝑁 − 𝑟)))
10		zcn 12564	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
11		zcn 12564	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 ∈ ℤ → 𝑟 ∈ ℂ)
12		zmulcl 12612	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝑞 · 𝐷) ∈ ℤ)
13	12	zcnd 12668	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝑞 · 𝐷) ∈ ℂ)
14		subadd 11464	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℂ ∧ 𝑟 ∈ ℂ ∧ (𝑞 · 𝐷) ∈ ℂ) → ((𝑁 − 𝑟) = (𝑞 · 𝐷) ↔ (𝑟 + (𝑞 · 𝐷)) = 𝑁))
15	10, 11, 13, 14	syl3an 1157	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ (𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → ((𝑁 − 𝑟) = (𝑞 · 𝐷) ↔ (𝑟 + (𝑞 · 𝐷)) = 𝑁))
16		addcom 11401	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑟 ∈ ℂ ∧ (𝑞 · 𝐷) ∈ ℂ) → (𝑟 + (𝑞 · 𝐷)) = ((𝑞 · 𝐷) + 𝑟))
17	11, 13, 16	syl2an 595	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑟 ∈ ℤ ∧ (𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → (𝑟 + (𝑞 · 𝐷)) = ((𝑞 · 𝐷) + 𝑟))
18	17	3adant1 1127	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ (𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → (𝑟 + (𝑞 · 𝐷)) = ((𝑞 · 𝐷) + 𝑟))
19	18	eqeq1d 2728	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ (𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → ((𝑟 + (𝑞 · 𝐷)) = 𝑁 ↔ ((𝑞 · 𝐷) + 𝑟) = 𝑁))
20	15, 19	bitrd 279	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ (𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → ((𝑁 − 𝑟) = (𝑞 · 𝐷) ↔ ((𝑞 · 𝐷) + 𝑟) = 𝑁))
21		eqcom 2733	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 − 𝑟) = (𝑞 · 𝐷) ↔ (𝑞 · 𝐷) = (𝑁 − 𝑟))
22		eqcom 2733	. . . . . . . . . . . . . . . 16 ⊢ (((𝑞 · 𝐷) + 𝑟) = 𝑁 ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑟))
23	20, 21, 22	3bitr3g 313	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ (𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → ((𝑞 · 𝐷) = (𝑁 − 𝑟) ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
24	23	3expia 1118	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ) → ((𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝑞 · 𝐷) = (𝑁 − 𝑟) ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑟))))
25	24	expcomd 416	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (𝐷 ∈ ℤ → (𝑞 ∈ ℤ → ((𝑞 · 𝐷) = (𝑁 − 𝑟) ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))))
26	25	3impia 1114	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝑞 ∈ ℤ → ((𝑞 · 𝐷) = (𝑁 − 𝑟) ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑟))))
27	26	imp 406	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ 𝑞 ∈ ℤ) → ((𝑞 · 𝐷) = (𝑁 − 𝑟) ↔ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
28	27	rexbidva 3170	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (∃𝑞 ∈ ℤ (𝑞 · 𝐷) = (𝑁 − 𝑟) ↔ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
29	28	3com23 1123	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (∃𝑞 ∈ ℤ (𝑞 · 𝐷) = (𝑁 − 𝑟) ↔ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
30	9, 29	bitrd 279	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (𝐷 ∥ (𝑁 − 𝑟) ↔ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
31	30	anbi2d 628	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷)) ∧ 𝐷 ∥ (𝑁 − 𝑟)) ↔ ((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷)) ∧ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟))))
32	4, 31	bitr4id 290	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷)) ∧ 𝐷 ∥ (𝑁 − 𝑟))))
33		anass 468	. . . . . 6 ⊢ (((0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷)) ∧ 𝐷 ∥ (𝑁 − 𝑟)) ↔ (0 ≤ 𝑟 ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))))
34	32, 33	bitrdi 287	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ (0 ≤ 𝑟 ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))))
35	34	3expa 1115	. . . 4 ⊢ (((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ 𝑟 ∈ ℤ) → (∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ (0 ≤ 𝑟 ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))))
36	35	reubidva 3386	. . 3 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃!𝑟 ∈ ℤ (0 ≤ 𝑟 ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))))
37		elnn0z 12572	. . . . . . 7 ⊢ (𝑟 ∈ ℕ₀ ↔ (𝑟 ∈ ℤ ∧ 0 ≤ 𝑟))
38	37	anbi1i 623	. . . . . 6 ⊢ ((𝑟 ∈ ℕ₀ ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))) ↔ ((𝑟 ∈ ℤ ∧ 0 ≤ 𝑟) ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))))
39		anass 468	. . . . . 6 ⊢ (((𝑟 ∈ ℤ ∧ 0 ≤ 𝑟) ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))) ↔ (𝑟 ∈ ℤ ∧ (0 ≤ 𝑟 ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))))
40	38, 39	bitri 275	. . . . 5 ⊢ ((𝑟 ∈ ℕ₀ ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))) ↔ (𝑟 ∈ ℤ ∧ (0 ≤ 𝑟 ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))))
41	40	eubii 2573	. . . 4 ⊢ (∃!𝑟(𝑟 ∈ ℕ₀ ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))) ↔ ∃!𝑟(𝑟 ∈ ℤ ∧ (0 ≤ 𝑟 ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))))
42		df-reu 3371	. . . 4 ⊢ (∃!𝑟 ∈ ℕ₀ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)) ↔ ∃!𝑟(𝑟 ∈ ℕ₀ ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))))
43		df-reu 3371	. . . 4 ⊢ (∃!𝑟 ∈ ℤ (0 ≤ 𝑟 ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))) ↔ ∃!𝑟(𝑟 ∈ ℤ ∧ (0 ≤ 𝑟 ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))))
44	41, 42, 43	3bitr4ri 304	. . 3 ⊢ (∃!𝑟 ∈ ℤ (0 ≤ 𝑟 ∧ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))) ↔ ∃!𝑟 ∈ ℕ₀ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))
45	36, 44	bitrdi 287	. 2 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃!𝑟 ∈ ℕ₀ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))))
46	45	3adant3 1129	1 ⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃!𝑟 ∈ ℕ₀ (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ∃!weu 2556 ≠ wne 2934 ∃wrex 3064 ∃!wreu 3368 class class class wbr 5141 ‘cfv 6536 (class class class)co 7404 ℂcc 11107 0cc0 11109 + caddc 11112 · cmul 11114 < clt 11249 ≤ cle 11250 − cmin 11445 ℕ₀cn0 12473 ℤcz 12559 abscabs 15184 ∥ cdvds 16201

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2697 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7721 ax-resscn 11166 ax-1cn 11167 ax-icn 11168 ax-addcl 11169 ax-addrcl 11170 ax-mulcl 11171 ax-mulrcl 11172 ax-mulcom 11173 ax-addass 11174 ax-mulass 11175 ax-distr 11176 ax-i2m1 11177 ax-1ne0 11178 ax-1rid 11179 ax-rnegex 11180 ax-rrecex 11181 ax-cnre 11182 ax-pre-lttri 11183 ax-pre-lttrn 11184 ax-pre-ltadd 11185 ax-pre-mulgt0 11186

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-nfc 2879 df-ne 2935 df-nel 3041 df-ral 3056 df-rex 3065 df-reu 3371 df-rab 3427 df-v 3470 df-sbc 3773 df-csb 3889 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-pss 3962 df-nul 4318 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-iun 4992 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5567 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-we 5626 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-pred 6293 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6488 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7360 df-ov 7407 df-oprab 7408 df-mpo 7409 df-om 7852 df-2nd 7972 df-frecs 8264 df-wrecs 8295 df-recs 8369 df-rdg 8408 df-er 8702 df-en 8939 df-dom 8940 df-sdom 8941 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11447 df-neg 11448 df-nn 12214 df-n0 12474 df-z 12560 df-dvds 16202

This theorem is referenced by: divalg2 16352

W3C validator