Description: Example for df-dvds : 3 divides into 6. (Contributed by David A. Wheeler, 19-May-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ex-dvds | |- 3 || 6 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2z | |- 2 e. ZZ |
|
| 2 | 3z | |- 3 e. ZZ |
|
| 3 | 6nn | |- 6 e. NN |
|
| 4 | 3 | nnzi | |- 6 e. ZZ |
| 5 | 1 2 4 | 3pm3.2i | |- ( 2 e. ZZ /\ 3 e. ZZ /\ 6 e. ZZ ) |
| 6 | 3cn | |- 3 e. CC |
|
| 7 | 6 | 2timesi | |- ( 2 x. 3 ) = ( 3 + 3 ) |
| 8 | 3p3e6 | |- ( 3 + 3 ) = 6 |
|
| 9 | 7 8 | eqtri | |- ( 2 x. 3 ) = 6 |
| 10 | dvds0lem | |- ( ( ( 2 e. ZZ /\ 3 e. ZZ /\ 6 e. ZZ ) /\ ( 2 x. 3 ) = 6 ) -> 3 || 6 ) |
|
| 11 | 5 9 10 | mp2an | |- 3 || 6 |