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

Theorem dvdsmulcr 10137
 Description: Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.)
Assertion
Ref Expression
dvdsmulcr

Proof of Theorem dvdsmulcr
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simp1 915 . . . . 5
2 simp3l 943 . . . . 5
31, 2zmulcld 8425 . . . 4
4 simp2 916 . . . . 5
54, 2zmulcld 8425 . . . 4
63, 5jca 294 . . 3
7 3simpa 912 . . 3
8 simpr 107 . . 3
98zcnd 8420 . . . . . . 7
101zcnd 8420 . . . . . . . 8
1110adantr 265 . . . . . . 7
122adantr 265 . . . . . . . 8
1312zcnd 8420 . . . . . . 7
149, 11, 13mulassd 7108 . . . . . 6
1514eqeq1d 2064 . . . . 5
169, 11mulcld 7105 . . . . . 6
174adantr 265 . . . . . . 7
1817zcnd 8420 . . . . . 6
19 simpl3r 971 . . . . . . 7
20 0z 8313 . . . . . . . . . . 11
21 zapne 8373 . . . . . . . . . . 11 #
2220, 21mpan2 409 . . . . . . . . . 10 #
2322adantr 265 . . . . . . . . 9 #
24233ad2ant3 938 . . . . . . . 8 #
2524adantr 265 . . . . . . 7 #
2619, 25mpbird 160 . . . . . 6 #
2716, 18, 13, 26mulcanap2d 7717 . . . . 5
2815, 27bitr3d 183 . . . 4
2928biimpd 136 . . 3
306, 7, 8, 29dvds1lem 10119 . 2
31 dvdsmulc 10135 . . 3