Description: Condition for a prime dividing a square. (Contributed by Scott Fenton, 8-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by SN, 21-Aug-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | prmdvdssq | |- ( ( P e. Prime /\ M e. ZZ ) -> ( P || M <-> P || ( M ^ 2 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2nn | |- 2 e. NN |
|
| 2 | prmdvdsexp | |- ( ( P e. Prime /\ M e. ZZ /\ 2 e. NN ) -> ( P || ( M ^ 2 ) <-> P || M ) ) |
|
| 3 | 1 2 | mp3an3 | |- ( ( P e. Prime /\ M e. ZZ ) -> ( P || ( M ^ 2 ) <-> P || M ) ) |
| 4 | 3 | bicomd | |- ( ( P e. Prime /\ M e. ZZ ) -> ( P || M <-> P || ( M ^ 2 ) ) ) |