pcexp

Description: Prime power of an exponential. (Contributed by Mario Carneiro, 10-Aug-2015)

		Ref	Expression
	Assertion	pcexp	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land N \in ℤ) \to P pCnt A^{N} = N (P pCnt A)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = 0 \to A^{x} = A^{0}$
2	1	oveq2d	$⊢ x = 0 \to P pCnt A^{x} = P pCnt A^{0}$
3		oveq1	$⊢ x = 0 \to x (P pCnt A) = 0 \cdot (P pCnt A)$
4	2 3	eqeq12d	$⊢ x = 0 \to (P pCnt A^{x} = x (P pCnt A) \leftrightarrow P pCnt A^{0} = 0 \cdot (P pCnt A))$
5		oveq2	$⊢ x = y \to A^{x} = A^{y}$
6	5	oveq2d	$⊢ x = y \to P pCnt A^{x} = P pCnt A^{y}$
7		oveq1	$⊢ x = y \to x (P pCnt A) = y (P pCnt A)$
8	6 7	eqeq12d	$⊢ x = y \to (P pCnt A^{x} = x (P pCnt A) \leftrightarrow P pCnt A^{y} = y (P pCnt A))$
9		oveq2	$⊢ x = y + 1 \to A^{x} = A^{y + 1}$
10	9	oveq2d	$⊢ x = y + 1 \to P pCnt A^{x} = P pCnt A^{y + 1}$
11		oveq1	$⊢ x = y + 1 \to x (P pCnt A) = (y + 1) (P pCnt A)$
12	10 11	eqeq12d	$⊢ x = y + 1 \to (P pCnt A^{x} = x (P pCnt A) \leftrightarrow P pCnt A^{y + 1} = (y + 1) (P pCnt A))$
13		oveq2	$⊢ x = - y \to A^{x} = A^{- y}$
14	13	oveq2d	$⊢ x = - y \to P pCnt A^{x} = P pCnt A^{- y}$
15		oveq1	$⊢ x = - y \to x (P pCnt A) = (- y) (P pCnt A)$
16	14 15	eqeq12d	$⊢ x = - y \to (P pCnt A^{x} = x (P pCnt A) \leftrightarrow P pCnt A^{- y} = (- y) (P pCnt A))$
17		oveq2	$⊢ x = N \to A^{x} = A^{N}$
18	17	oveq2d	$⊢ x = N \to P pCnt A^{x} = P pCnt A^{N}$
19		oveq1	$⊢ x = N \to x (P pCnt A) = N (P pCnt A)$
20	18 19	eqeq12d	$⊢ x = N \to (P pCnt A^{x} = x (P pCnt A) \leftrightarrow P pCnt A^{N} = N (P pCnt A))$
21		pc1	$⊢ P \in ℙ \to P pCnt 1 = 0$
22	21	adantr	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0)) \to P pCnt 1 = 0$
23		qcn	$⊢ A \in ℚ \to A \in ℂ$
24	23	ad2antrl	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0)) \to A \in ℂ$
25	24	exp0d	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0)) \to A^{0} = 1$
26	25	oveq2d	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0)) \to P pCnt A^{0} = P pCnt 1$
27		pcqcl	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0)) \to P pCnt A \in ℤ$
28	27	zcnd	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0)) \to P pCnt A \in ℂ$
29	28	mul02d	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0)) \to 0 \cdot (P pCnt A) = 0$
30	22 26 29	3eqtr4d	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0)) \to P pCnt A^{0} = 0 \cdot (P pCnt A)$
31		oveq1	$⊢ P pCnt A^{y} = y (P pCnt A) \to (P pCnt A^{y}) + (P pCnt A) = y (P pCnt A) + (P pCnt A)$
32		expp1	$⊢ (A \in ℂ \land y \in ℕ_{0}) \to A^{y + 1} = A^{y} A$
33	24 32	sylan	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ_{0}) \to A^{y + 1} = A^{y} A$
34	33	oveq2d	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ_{0}) \to P pCnt A^{y + 1} = P pCnt A^{y} A$
35		simpll	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ_{0}) \to P \in ℙ$
36		simplrl	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ_{0}) \to A \in ℚ$
37		simplrr	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ_{0}) \to A \neq 0$
38		nn0z	$⊢ y \in ℕ_{0} \to y \in ℤ$
39	38	adantl	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ_{0}) \to y \in ℤ$
40		qexpclz	$⊢ (A \in ℚ \land A \neq 0 \land y \in ℤ) \to A^{y} \in ℚ$
41	36 37 39 40	syl3anc	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ_{0}) \to A^{y} \in ℚ$
42	24	adantr	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ_{0}) \to A \in ℂ$
43	42 37 39	expne0d	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ_{0}) \to A^{y} \neq 0$
44		pcqmul	$⊢ (P \in ℙ \land (A^{y} \in ℚ \land A^{y} \neq 0) \land (A \in ℚ \land A \neq 0)) \to P pCnt A^{y} A = (P pCnt A^{y}) + (P pCnt A)$
45	35 41 43 36 37 44	syl122anc	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ_{0}) \to P pCnt A^{y} A = (P pCnt A^{y}) + (P pCnt A)$
46	34 45	eqtrd	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ_{0}) \to P pCnt A^{y + 1} = (P pCnt A^{y}) + (P pCnt A)$
47		nn0cn	$⊢ y \in ℕ_{0} \to y \in ℂ$
48	47	adantl	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ_{0}) \to y \in ℂ$
49	28	adantr	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ_{0}) \to P pCnt A \in ℂ$
50	48 49	adddirp1d	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ_{0}) \to (y + 1) (P pCnt A) = y (P pCnt A) + (P pCnt A)$
51	46 50	eqeq12d	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ_{0}) \to (P pCnt A^{y + 1} = (y + 1) (P pCnt A) \leftrightarrow (P pCnt A^{y}) + (P pCnt A) = y (P pCnt A) + (P pCnt A))$
52	31 51	syl5ibr	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ_{0}) \to (P pCnt A^{y} = y (P pCnt A) \to P pCnt A^{y + 1} = (y + 1) (P pCnt A))$
53	52	ex	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0)) \to (y \in ℕ_{0} \to (P pCnt A^{y} = y (P pCnt A) \to P pCnt A^{y + 1} = (y + 1) (P pCnt A)))$
54		negeq	$⊢ P pCnt A^{y} = y (P pCnt A) \to - (P pCnt A^{y}) = - y (P pCnt A)$
55		nnnn0	$⊢ y \in ℕ \to y \in ℕ_{0}$
56		expneg	$⊢ (A \in ℂ \land y \in ℕ_{0}) \to A^{- y} = \frac{1}{A^{y}}$
57	24 55 56	syl2an	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ) \to A^{- y} = \frac{1}{A^{y}}$
58	57	oveq2d	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ) \to P pCnt A^{- y} = P pCnt (\frac{1}{A^{y}})$
59		simpll	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ) \to P \in ℙ$
60	55 41	sylan2	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ) \to A^{y} \in ℚ$
61	55 43	sylan2	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ) \to A^{y} \neq 0$
62		pcrec	$⊢ (P \in ℙ \land (A^{y} \in ℚ \land A^{y} \neq 0)) \to P pCnt (\frac{1}{A^{y}}) = - (P pCnt A^{y})$
63	59 60 61 62	syl12anc	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ) \to P pCnt (\frac{1}{A^{y}}) = - (P pCnt A^{y})$
64	58 63	eqtrd	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ) \to P pCnt A^{- y} = - (P pCnt A^{y})$
65		nncn	$⊢ y \in ℕ \to y \in ℂ$
66		mulneg1	$⊢ (y \in ℂ \land P pCnt A \in ℂ) \to (- y) (P pCnt A) = - y (P pCnt A)$
67	65 28 66	syl2anr	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ) \to (- y) (P pCnt A) = - y (P pCnt A)$
68	64 67	eqeq12d	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ) \to (P pCnt A^{- y} = (- y) (P pCnt A) \leftrightarrow - (P pCnt A^{y}) = - y (P pCnt A))$
69	54 68	syl5ibr	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0)) \land y \in ℕ) \to (P pCnt A^{y} = y (P pCnt A) \to P pCnt A^{- y} = (- y) (P pCnt A))$
70	69	ex	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0)) \to (y \in ℕ \to (P pCnt A^{y} = y (P pCnt A) \to P pCnt A^{- y} = (- y) (P pCnt A)))$
71	4 8 12 16 20 30 53 70	zindd	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0)) \to (N \in ℤ \to P pCnt A^{N} = N (P pCnt A))$
72	71	3impia	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land N \in ℤ) \to P pCnt A^{N} = N (P pCnt A)$

Metamath Proof Explorer

Theorem pcexp

Proof