theorem prlem1 (n: nat): $ 2 || n * suc n $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvdmul11 | 2 || n -> 2 || n * suc n |
|
2 | d2dvdS | 2 || suc n <-> ~2 || n |
|
3 | dvdmul12 | 2 || suc n -> 2 || n * suc n |
|
4 | 2, 3 | sylbir | ~2 || n -> 2 || n * suc n |
5 | 1, 4 | cases | 2 || n * suc n |