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

Theorem dvdsval2 12860
 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

Proof of Theorem dvdsval2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 divides 12859 . . 3
213adant2 977 . 2
3 zcn 10292 . . . . . . . . . . 11
433ad2ant3 981 . . . . . . . . . 10
54adantr 453 . . . . . . . . 9
6 zcn 10292 . . . . . . . . . 10
76adantl 454 . . . . . . . . 9
8 zcn 10292 . . . . . . . . . . 11
983ad2ant1 979 . . . . . . . . . 10
109adantr 453 . . . . . . . . 9
11 simpl2 962 . . . . . . . . 9
125, 7, 10, 11divmul3d 9829 . . . . . . . 8
13 eqcom 2440 . . . . . . . 8
1412, 13syl6bb 254 . . . . . . 7
1514biimprd 216 . . . . . 6
1615impr 604 . . . . 5
17 simprl 734 . . . . 5
1816, 17eqeltrd 2512 . . . 4
1918rexlimdvaa 2833 . . 3
20 simpr 449 . . . . 5
21 simp2 959 . . . . . . 7
224, 9, 21divcan1d 9796 . . . . . 6
2322adantr 453 . . . . 5
24 oveq1 6091 . . . . . . 7
2524eqeq1d 2446 . . . . . 6
2625rspcev 3054 . . . . 5
2720, 23, 26syl2anc 644 . . . 4
2827ex 425 . . 3
2919, 28impbid 185 . 2
302, 29bitrd 246 1