Theorem pcprmpw

Description: Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015)

	Ref	Expression
Assertion	pcprmpw	|- ( ( P e. Prime /\ A e. NN ) -> ( E. n e. NN0 A = ( P ^ n ) <-> A = ( P ^ ( P pCnt A ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		prmz	|- ( P e. Prime -> P e. ZZ )
2	1	adantr	|- ( ( P e. Prime /\ A e. NN ) -> P e. ZZ )
3		zexpcl	|- ( ( P e. ZZ /\ n e. NN0 ) -> ( P ^ n ) e. ZZ )
4	2 3	sylan	|- ( ( ( P e. Prime /\ A e. NN ) /\ n e. NN0 ) -> ( P ^ n ) e. ZZ )
5		iddvds	|- ( ( P ^ n ) e. ZZ -> ( P ^ n ) || ( P ^ n ) )
6	4 5	syl	|- ( ( ( P e. Prime /\ A e. NN ) /\ n e. NN0 ) -> ( P ^ n ) || ( P ^ n ) )
7		breq1	|- ( A = ( P ^ n ) -> ( A || ( P ^ n ) <-> ( P ^ n ) || ( P ^ n ) ) )
8	6 7	syl5ibrcom	|- ( ( ( P e. Prime /\ A e. NN ) /\ n e. NN0 ) -> ( A = ( P ^ n ) -> A || ( P ^ n ) ) )
9	8	reximdva	|- ( ( P e. Prime /\ A e. NN ) -> ( E. n e. NN0 A = ( P ^ n ) -> E. n e. NN0 A || ( P ^ n ) ) )
10		pcprmpw2	|- ( ( P e. Prime /\ A e. NN ) -> ( E. n e. NN0 A || ( P ^ n ) <-> A = ( P ^ ( P pCnt A ) ) ) )
11	9 10	sylibd	|- ( ( P e. Prime /\ A e. NN ) -> ( E. n e. NN0 A = ( P ^ n ) -> A = ( P ^ ( P pCnt A ) ) ) )
12		pccl	|- ( ( P e. Prime /\ A e. NN ) -> ( P pCnt A ) e. NN0 )
13		oveq2	|- ( n = ( P pCnt A ) -> ( P ^ n ) = ( P ^ ( P pCnt A ) ) )
14	13	rspceeqv	|- ( ( ( P pCnt A ) e. NN0 /\ A = ( P ^ ( P pCnt A ) ) ) -> E. n e. NN0 A = ( P ^ n ) )
15	14	ex	|- ( ( P pCnt A ) e. NN0 -> ( A = ( P ^ ( P pCnt A ) ) -> E. n e. NN0 A = ( P ^ n ) ) )
16	12 15	syl	|- ( ( P e. Prime /\ A e. NN ) -> ( A = ( P ^ ( P pCnt A ) ) -> E. n e. NN0 A = ( P ^ n ) ) )
17	11 16	impbid	|- ( ( P e. Prime /\ A e. NN ) -> ( E. n e. NN0 A = ( P ^ n ) <-> A = ( P ^ ( P pCnt A ) ) ) )