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 16319

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 16318	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ ∃𝑘 ∈ ℤ (𝑘 · 𝑀) = 𝑁))
2	1	3adant2 1148	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ ∃𝑘 ∈ ℤ (𝑘 · 𝑀) = 𝑁))
3		zcn 12602	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
4	3	3ad2ant3 1152	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℂ)
5	4	adantr 485	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → 𝑁 ∈ ℂ)
6		zcn 12602	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
7	6	adantl 486	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℂ)
8		zcn 12602	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
9	8	3ad2ant1 1150	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℂ)
10	9	adantr 485	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → 𝑀 ∈ ℂ)
11		simpl2 1210	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → 𝑀 ≠ 0)
12	5, 7, 10, 11	divmul3d 12031	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → ((𝑁 / 𝑀) = 𝑘 ↔ 𝑁 = (𝑘 · 𝑀)))
13		eqcom 2769	. . . . . . . 8 ⊢ (𝑁 = (𝑘 · 𝑀) ↔ (𝑘 · 𝑀) = 𝑁)
14	12, 13	bitrdi 290	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → ((𝑁 / 𝑀) = 𝑘 ↔ (𝑘 · 𝑀) = 𝑁))
15	14	biimprd 251	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → ((𝑘 · 𝑀) = 𝑁 → (𝑁 / 𝑀) = 𝑘))
16	15	impr 459	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑘 · 𝑀) = 𝑁)) → (𝑁 / 𝑀) = 𝑘)
17		simprl 782	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑘 · 𝑀) = 𝑁)) → 𝑘 ∈ ℤ)
18	16, 17	eqeltrd 2862	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑘 · 𝑀) = 𝑁)) → (𝑁 / 𝑀) ∈ ℤ)
19	18	rexlimdvaa 3166	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → (∃𝑘 ∈ ℤ (𝑘 · 𝑀) = 𝑁 → (𝑁 / 𝑀) ∈ ℤ))
20		simpr 489	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ (𝑁 / 𝑀) ∈ ℤ) → (𝑁 / 𝑀) ∈ ℤ)
21		simp2 1154	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → 𝑀 ≠ 0)
22	4, 9, 21	divcan1d 11998	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → ((𝑁 / 𝑀) · 𝑀) = 𝑁)
23	22	adantr 485	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ (𝑁 / 𝑀) ∈ ℤ) → ((𝑁 / 𝑀) · 𝑀) = 𝑁)
24		oveq1 7419	. . . . . . 7 ⊢ (𝑘 = (𝑁 / 𝑀) → (𝑘 · 𝑀) = ((𝑁 / 𝑀) · 𝑀))
25	24	eqeq1d 2764	. . . . . 6 ⊢ (𝑘 = (𝑁 / 𝑀) → ((𝑘 · 𝑀) = 𝑁 ↔ ((𝑁 / 𝑀) · 𝑀) = 𝑁))
26	25	rspcev 3580	. . . . 5 ⊢ (((𝑁 / 𝑀) ∈ ℤ ∧ ((𝑁 / 𝑀) · 𝑀) = 𝑁) → ∃𝑘 ∈ ℤ (𝑘 · 𝑀) = 𝑁)
27	20, 23, 26	syl2anc 595	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) ∧ (𝑁 / 𝑀) ∈ ℤ) → ∃𝑘 ∈ ℤ (𝑘 · 𝑀) = 𝑁)
28	27	ex 417	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → ((𝑁 / 𝑀) ∈ ℤ → ∃𝑘 ∈ ℤ (𝑘 · 𝑀) = 𝑁))
29	19, 28	impbid 215	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → (∃𝑘 ∈ ℤ (𝑘 · 𝑀) = 𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ))
30	2, 29	bitrd 282	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1102 = wceq 1569 ∈ wcel 2142 ≠ wne 2957 ∃wrex 3088 class class class wbr 5108 (class class class)co 7412 ℂcc 11104 0cc0 11106 · cmul 11111 / cdiv 11877 ℤcz 12597 ∥ cdvds 16316

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-br 5109 df-opab 5173 df-mpt 5192 df-id 5555 df-po 5568 df-so 5569 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-er 8692 df-en 8942 df-dom 8943 df-sdom 8944 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-div 11878 df-z 12598 df-dvds 16317

This theorem is used by: dvdsval3 16320 nndivdvds 16325 fsumdvds 16372 divconjdvds 16379 3dvds 16395 evend2 16421 oddp1d2 16422 fldivndvdslt 16480 bitsmod 16500 sadaddlem 16530 bitsuz 16538 divgcdz 16575 dvdsgcdidd 16601 mulgcd 16612 sqgcd 16626 lcmgcdlem 16670 mulgcddvds 16719 qredeu 16722 prmind2 16749 isprm5 16772 divgcdodd 16775 divnumden 16813 hashdvds 16840 hashgcdlem 16853 pythagtriplem19 16899 pcprendvds2 16907 pcpremul 16909 pc2dvds 16945 pcz 16947 dvdsprmpweqle 16952 pcadd 16955 pcmptdvds 16960 fldivp1 16963 pockthlem 16971 prmreclem1 16982 prmreclem3 16984 4sqlem8 17011 4sqlem9 17012 4sqlem12 17022 4sqlem14 17024 sylow1lem1 19674 sylow3lem4 19706 odadd1 19924 odadd2 19925 pgpfac1lem3 20155 prmirredlem 21633 znidomb 21722 root1eq1 26931 atantayl2 27114 efchtdvds 27334 muinv 27368 bposlem6 27464 lgseisenlem1 27550 lgsquad2lem1 27559 lgsquad3 27562 m1lgs 27563 2sqlem3 27595 2sqlem8 27601 qqhval2lem 34380 nn0prpwlem 36861 knoppndvlem8 37136 aks4d1p8d3 42881 aks4d1p8 42882 aks6d1c1 42911 aks6d1c3 42918 aks6d1c4 42919 aks6d1c2lem4 42922 aks6d1c6lem3 42967 aks6d1c6lem4 42968 unitscyglem4 42993 congrep 43728 jm2.22 43750 jm2.23 43751 proot1ex 43951 nzss 45055 etransclem9 46985 etransclem38 47014 etransclem44 47020 etransclem45 47021 facnn0dvdsfac 48150 divgcdoddALTV 48475 0dig2nn0o 49421

W3C validator