pcprmpw2

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

		Ref	Expression
	Assertion	pcprmpw2	$⊢ (P \in ℙ \land A \in ℕ) \to (\exists n \in ℕ_{0} A ∥ P^{n} \leftrightarrow A = P^{P pCnt A})$

Proof

Step	Hyp	Ref	Expression
1		simplr	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to A \in ℕ$
2	1	nnnn0d	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to A \in ℕ_{0}$
3		prmnn	$⊢ P \in ℙ \to P \in ℕ$
4	3	ad2antrr	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to P \in ℕ$
5		pccl	$⊢ (P \in ℙ \land A \in ℕ) \to P pCnt A \in ℕ_{0}$
6	5	adantr	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to P pCnt A \in ℕ_{0}$
7	4 6	nnexpcld	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to P^{P pCnt A} \in ℕ$
8	7	nnnn0d	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to P^{P pCnt A} \in ℕ_{0}$
9	6	nn0red	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to P pCnt A \in ℝ$
10	9	leidd	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to P pCnt A \leq P pCnt A$
11		simpll	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to P \in ℙ$
12	6	nn0zd	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to P pCnt A \in ℤ$
13		pcid	$⊢ (P \in ℙ \land P pCnt A \in ℤ) \to P pCnt P^{P pCnt A} = P pCnt A$
14	11 12 13	syl2anc	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to P pCnt P^{P pCnt A} = P pCnt A$
15	10 14	breqtrrd	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to P pCnt A \leq P pCnt P^{P pCnt A}$
16	15	ad2antrr	$⊢ ((((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \land p = P) \to P pCnt A \leq P pCnt P^{P pCnt A}$
17		simpr	$⊢ ((((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \land p = P) \to p = P$
18	17	oveq1d	$⊢ ((((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \land p = P) \to p pCnt A = P pCnt A$
19	17	oveq1d	$⊢ ((((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \land p = P) \to p pCnt P^{P pCnt A} = P pCnt P^{P pCnt A}$
20	16 18 19	3brtr4d	$⊢ ((((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \land p = P) \to p pCnt A \leq p pCnt P^{P pCnt A}$
21		simplrr	$⊢ (((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \to A ∥ P^{n}$
22		prmz	$⊢ p \in ℙ \to p \in ℤ$
23	22	adantl	$⊢ (((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \to p \in ℤ$
24	1	adantr	$⊢ (((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \to A \in ℕ$
25	24	nnzd	$⊢ (((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \to A \in ℤ$
26		simprl	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to n \in ℕ_{0}$
27	4 26	nnexpcld	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to P^{n} \in ℕ$
28	27	adantr	$⊢ (((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \to P^{n} \in ℕ$
29	28	nnzd	$⊢ (((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \to P^{n} \in ℤ$
30		dvdstr	$⊢ (p \in ℤ \land A \in ℤ \land P^{n} \in ℤ) \to ((p ∥ A \land A ∥ P^{n}) \to p ∥ P^{n})$
31	23 25 29 30	syl3anc	$⊢ (((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \to ((p ∥ A \land A ∥ P^{n}) \to p ∥ P^{n})$
32	21 31	mpan2d	$⊢ (((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \to (p ∥ A \to p ∥ P^{n})$
33		simpr	$⊢ (((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \to p \in ℙ$
34	11	adantr	$⊢ (((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \to P \in ℙ$
35		simplrl	$⊢ (((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \to n \in ℕ_{0}$
36		prmdvdsexpr	$⊢ (p \in ℙ \land P \in ℙ \land n \in ℕ_{0}) \to (p ∥ P^{n} \to p = P)$
37	33 34 35 36	syl3anc	$⊢ (((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \to (p ∥ P^{n} \to p = P)$
38	32 37	syld	$⊢ (((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \to (p ∥ A \to p = P)$
39	38	necon3ad	$⊢ (((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \to (p \neq P \to \neg p ∥ A)$
40	39	imp	$⊢ ((((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \land p \neq P) \to \neg p ∥ A$
41		simplr	$⊢ ((((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \land p \neq P) \to p \in ℙ$
42	1	ad2antrr	$⊢ ((((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \land p \neq P) \to A \in ℕ$
43		pceq0	$⊢ (p \in ℙ \land A \in ℕ) \to (p pCnt A = 0 \leftrightarrow \neg p ∥ A)$
44	41 42 43	syl2anc	$⊢ ((((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \land p \neq P) \to (p pCnt A = 0 \leftrightarrow \neg p ∥ A)$
45	40 44	mpbird	$⊢ ((((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \land p \neq P) \to p pCnt A = 0$
46	7	ad2antrr	$⊢ ((((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \land p \neq P) \to P^{P pCnt A} \in ℕ$
47	41 46	pccld	$⊢ ((((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \land p \neq P) \to p pCnt P^{P pCnt A} \in ℕ_{0}$
48	47	nn0ge0d	$⊢ ((((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \land p \neq P) \to 0 \leq p pCnt P^{P pCnt A}$
49	45 48	eqbrtrd	$⊢ ((((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \land p \neq P) \to p pCnt A \leq p pCnt P^{P pCnt A}$
50	20 49	pm2.61dane	$⊢ (((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \land p \in ℙ) \to p pCnt A \leq p pCnt P^{P pCnt A}$
51	50	ralrimiva	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to \forall p \in ℙ p pCnt A \leq p pCnt P^{P pCnt A}$
52	1	nnzd	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to A \in ℤ$
53	7	nnzd	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to P^{P pCnt A} \in ℤ$
54		pc2dvds	$⊢ (A \in ℤ \land P^{P pCnt A} \in ℤ) \to (A ∥ P^{P pCnt A} \leftrightarrow \forall p \in ℙ p pCnt A \leq p pCnt P^{P pCnt A})$
55	52 53 54	syl2anc	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to (A ∥ P^{P pCnt A} \leftrightarrow \forall p \in ℙ p pCnt A \leq p pCnt P^{P pCnt A})$
56	51 55	mpbird	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to A ∥ P^{P pCnt A}$
57		pcdvds	$⊢ (P \in ℙ \land A \in ℕ) \to P^{P pCnt A} ∥ A$
58	57	adantr	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to P^{P pCnt A} ∥ A$
59		dvdseq	$⊢ ((A \in ℕ_{0} \land P^{P pCnt A} \in ℕ_{0}) \land (A ∥ P^{P pCnt A} \land P^{P pCnt A} ∥ A)) \to A = P^{P pCnt A}$
60	2 8 56 58 59	syl22anc	$⊢ ((P \in ℙ \land A \in ℕ) \land (n \in ℕ_{0} \land A ∥ P^{n})) \to A = P^{P pCnt A}$
61	60	rexlimdvaa	$⊢ (P \in ℙ \land A \in ℕ) \to (\exists n \in ℕ_{0} A ∥ P^{n} \to A = P^{P pCnt A})$
62	3	adantr	$⊢ (P \in ℙ \land A \in ℕ) \to P \in ℕ$
63	62 5	nnexpcld	$⊢ (P \in ℙ \land A \in ℕ) \to P^{P pCnt A} \in ℕ$
64	63	nnzd	$⊢ (P \in ℙ \land A \in ℕ) \to P^{P pCnt A} \in ℤ$
65		iddvds	$⊢ P^{P pCnt A} \in ℤ \to P^{P pCnt A} ∥ P^{P pCnt A}$
66	64 65	syl	$⊢ (P \in ℙ \land A \in ℕ) \to P^{P pCnt A} ∥ P^{P pCnt A}$
67		oveq2	$⊢ n = P pCnt A \to P^{n} = P^{P pCnt A}$
68	67	breq2d	$⊢ n = P pCnt A \to (P^{P pCnt A} ∥ P^{n} \leftrightarrow P^{P pCnt A} ∥ P^{P pCnt A})$
69	68	rspcev	$⊢ (P pCnt A \in ℕ_{0} \land P^{P pCnt A} ∥ P^{P pCnt A}) \to \exists n \in ℕ_{0} P^{P pCnt A} ∥ P^{n}$
70	5 66 69	syl2anc	$⊢ (P \in ℙ \land A \in ℕ) \to \exists n \in ℕ_{0} P^{P pCnt A} ∥ P^{n}$
71		breq1	$⊢ A = P^{P pCnt A} \to (A ∥ P^{n} \leftrightarrow P^{P pCnt A} ∥ P^{n})$
72	71	rexbidv	$⊢ A = P^{P pCnt A} \to (\exists n \in ℕ_{0} A ∥ P^{n} \leftrightarrow \exists n \in ℕ_{0} P^{P pCnt A} ∥ P^{n})$
73	70 72	syl5ibrcom	$⊢ (P \in ℙ \land A \in ℕ) \to (A = P^{P pCnt A} \to \exists n \in ℕ_{0} A ∥ P^{n})$
74	61 73	impbid	$⊢ (P \in ℙ \land A \in ℕ) \to (\exists n \in ℕ_{0} A ∥ P^{n} \leftrightarrow A = P^{P pCnt A})$

Metamath Proof Explorer

Theorem pcprmpw2

Proof