Metamath Proof Explorer

Theorem sqfpc

Description: The prime count of a squarefree number is at most 1. (Contributed by Mario Carneiro, 1-Jul-2015)

Ref Expression
Assertion sqfpc 
|- ( ( A e. NN /\ ( mmu ` A ) =/= 0 /\ P e. Prime ) -> ( P pCnt A ) <_ 1 )

Proof

Step Hyp Ref Expression
1 issqf 
 |-  ( A e. NN -> ( ( mmu ` A ) =/= 0 <-> A. p e. Prime ( p pCnt A ) <_ 1 ) )
2 1 biimpa 
 |-  ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) -> A. p e. Prime ( p pCnt A ) <_ 1 )
3 oveq1 
 |-  ( p = P -> ( p pCnt A ) = ( P pCnt A ) )
4 3 breq1d 
 |-  ( p = P -> ( ( p pCnt A ) <_ 1 <-> ( P pCnt A ) <_ 1 ) )
5 4 rspccv 
 |-  ( A. p e. Prime ( p pCnt A ) <_ 1 -> ( P e. Prime -> ( P pCnt A ) <_ 1 ) )
6 2 5 syl 
 |-  ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) -> ( P e. Prime -> ( P pCnt A ) <_ 1 ) )
7 6 3impia 
 |-  ( ( A e. NN /\ ( mmu ` A ) =/= 0 /\ P e. Prime ) -> ( P pCnt A ) <_ 1 )