dvdsval2 - Metamath Proof Explorer

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

Theorem dvdsval2 16219

Description: One nonzero integer divides another integer if and only if their quotient is an integer. (Contributed by Jeff Hankins, 29-Sep-2013.)

**Assertion**
Ref	Expression
dvdsval2	⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ))

Proof of Theorem dvdsval2 Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		divides 16218	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ ∃𝑘 ∈ ℤ (𝑘 · 𝑀) = 𝑁))
2	1	3adant2 1138	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ ∃𝑘 ∈ ℤ (𝑘 · 𝑀) = 𝑁))
3		zcn 12524	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
4	3	3ad2ant3 1142	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℂ)
5	4	adantr 482	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → 𝑁 ∈ ℂ)
6		zcn 12524	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
7	6	adantl 483	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℂ)
8		zcn 12524	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
9	8	3ad2ant1 1140	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℂ)
10	9	adantr 482	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → 𝑀 ∈ ℂ)
11		simpl2 1200	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → 𝑀 ≠ 0)
12	5, 7, 10, 11	divmul3d 11960	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → ((𝑁 / 𝑀) = 𝑘 ↔ 𝑁 = (𝑘 · 𝑀)))
13		eqcom 2748	. . . . . . . 8 ⊢ (𝑁 = (𝑘 · 𝑀) ↔ (𝑘 · 𝑀) = 𝑁)
14	12, 13	bitrdi 289	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → ((𝑁 / 𝑀) = 𝑘 ↔ (𝑘 · 𝑀) = 𝑁))
15	14	biimprd 250	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → ((𝑘 · 𝑀) = 𝑁 → (𝑁 / 𝑀) = 𝑘))
16	15	impr 456	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑘 · 𝑀) = 𝑁)) → (𝑁 / 𝑀) = 𝑘)
17		simprl 777	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑘 · 𝑀) = 𝑁)) → 𝑘 ∈ ℤ)
18	16, 17	eqeltrd 2841	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑘 · 𝑀) = 𝑁)) → (𝑁 / 𝑀) ∈ ℤ)
19	18	rexlimdvaa 3143	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → (∃𝑘 ∈ ℤ (𝑘 · 𝑀) = 𝑁 → (𝑁 / 𝑀) ∈ ℤ))
20		simpr 486	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ (𝑁 / 𝑀) ∈ ℤ) → (𝑁 / 𝑀) ∈ ℤ)
21		simp2 1144	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → 𝑀 ≠ 0)
22	4, 9, 21	divcan1d 11927	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → ((𝑁 / 𝑀) · 𝑀) = 𝑁)
23	22	adantr 482	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ (𝑁 / 𝑀) ∈ ℤ) → ((𝑁 / 𝑀) · 𝑀) = 𝑁)
24		oveq1 7367	. . . . . . 7 ⊢ (𝑘 = (𝑁 / 𝑀) → (𝑘 · 𝑀) = ((𝑁 / 𝑀) · 𝑀))
25	24	eqeq1d 2743	. . . . . 6 ⊢ (𝑘 = (𝑁 / 𝑀) → ((𝑘 · 𝑀) = 𝑁 ↔ ((𝑁 / 𝑀) · 𝑀) = 𝑁))
26	25	rspcev 3562	. . . . 5 ⊢ (((𝑁 / 𝑀) ∈ ℤ ∧ ((𝑁 / 𝑀) · 𝑀) = 𝑁) → ∃𝑘 ∈ ℤ (𝑘 · 𝑀) = 𝑁)
27	20, 23, 26	syl2anc 591	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ (𝑁 / 𝑀) ∈ ℤ) → ∃𝑘 ∈ ℤ (𝑘 · 𝑀) = 𝑁)
28	27	ex 414	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → ((𝑁 / 𝑀) ∈ ℤ → ∃𝑘 ∈ ℤ (𝑘 · 𝑀) = 𝑁))
29	19, 28	impbid 214	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → (∃𝑘 ∈ ℤ (𝑘 · 𝑀) = 𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ))
30	2, 29	bitrd 281	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 397 ∧ w3a 1093 = wceq 1548 ∈ wcel 2121 ≠ wne 2936 ∃wrex 3065 class class class wbr 5075 (class class class)co 7360 ℂcc 11031 0cc0 11033 · cmul 11038 / cdiv 11802 ℤcz 12519 ∥ cdvds 16216

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-sep 5221 ax-nul 5231 ax-pow 5297 ax-pr 5365 ax-un 7682 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3or 1094 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-nfc 2890 df-ne 2937 df-nel 3041 df-ral 3056 df-rex 3066 df-rmo 3346 df-reu 3347 df-rab 3394 df-v 3435 df-sbc 3726 df-csb 3834 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-nul 4265 df-if 4458 df-pw 4534 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4842 df-br 5076 df-opab 5138 df-mpt 5157 df-id 5516 df-po 5529 df-so 5530 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-er 8637 df-en 8888 df-dom 8889 df-sdom 8890 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-div 11803 df-z 12520 df-dvds 16217

This theorem is referenced by: dvdsval3 16220 nndivdvds 16225 fsumdvds 16272 divconjdvds 16279 3dvds 16295 evend2 16321 oddp1d2 16322 fldivndvdslt 16380 bitsmod 16400 sadaddlem 16430 bitsuz 16438 divgcdz 16475 dvdsgcdidd 16501 mulgcd 16512 sqgcd 16526 lcmgcdlem 16570 mulgcddvds 16619 qredeu 16622 prmind2 16649 isprm5 16672 divgcdodd 16675 divnumden 16713 hashdvds 16740 hashgcdlem 16753 pythagtriplem19 16799 pcprendvds2 16807 pcpremul 16809 pc2dvds 16845 pcz 16847 dvdsprmpweqle 16852 pcadd 16855 pcmptdvds 16860 fldivp1 16863 pockthlem 16871 prmreclem1 16882 prmreclem3 16884 4sqlem8 16911 4sqlem9 16912 4sqlem12 16922 4sqlem14 16924 sylow1lem1 19568 sylow3lem4 19600 odadd1 19818 odadd2 19819 pgpfac1lem3 20049 prmirredlem 21451 znidomb 21540 root1eq1 26741 atantayl2 26924 efchtdvds 27144 muinv 27178 bposlem6 27274 lgseisenlem1 27360 lgsquad2lem1 27369 lgsquad3 27372 m1lgs 27373 2sqlem3 27405 2sqlem8 27411 qqhval2lem 34177 nn0prpwlem 36565 knoppndvlem8 36840 aks4d1p8d3 42586 aks4d1p8 42587 aks6d1c1 42616 aks6d1c3 42623 aks6d1c4 42624 aks6d1c2lem4 42627 aks6d1c6lem3 42672 aks6d1c6lem4 42673 unitscyglem4 42698 congrep 43433 jm2.22 43455 jm2.23 43456 proot1ex 43656 nzss 44776 etransclem9 46700 etransclem38 46729 etransclem44 46735 etransclem45 46736 facnn0dvdsfac 47862 divgcdoddALTV 48187 0dig2nn0o 49118

W3C validator