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

Theorem dvdscmulr 11578
 Description: Cancellation law for the divides relation. Theorem 1.1(e) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
Assertion
Ref Expression
dvdscmulr

Proof of Theorem dvdscmulr
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simp3l 1010 . . . . 5
2 simp1 982 . . . . 5
31, 2zmulcld 9223 . . . 4
4 simp2 983 . . . . 5
51, 4zmulcld 9223 . . . 4
63, 5jca 304 . . 3
72, 4jca 304 . . 3
8 simpr 109 . . 3
91adantr 274 . . . . . . . 8
109zcnd 9218 . . . . . . 7
118zcnd 9218 . . . . . . 7
122adantr 274 . . . . . . . 8
1312zcnd 9218 . . . . . . 7
1410, 11, 13mul12d 7958 . . . . . 6
1514eqeq1d 2149 . . . . 5
1611, 13mulcld 7830 . . . . . 6
174adantr 274 . . . . . . 7
1817zcnd 9218 . . . . . 6
19 simpl3r 1038 . . . . . . 7
20 0z 9109 . . . . . . . 8
21 zapne 9169 . . . . . . . 8 #
229, 20, 21sylancl 410 . . . . . . 7 #
2319, 22mpbird 166 . . . . . 6 #
2416, 18, 10, 23mulcanapd 8466 . . . . 5
2515, 24bitr3d 189 . . . 4
2625biimpd 143 . . 3
276, 7, 8, 26dvds1lem 11560 . 2
28 dvdscmul 11576 . . 3