prmpwdvds

Description: A relation involving divisibility by a prime power. (Contributed by Mario Carneiro, 2-Mar-2014)

		Ref	Expression
	Assertion	prmpwdvds	$⊢ ((K \in ℤ \land D \in ℤ) \land (P \in ℙ \land N \in ℕ) \land (D ∥ K P^{N} \land \neg D ∥ K P^{N - 1})) \to P^{N} ∥ D$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ k = K \to k P^{N} = K P^{N}$
2	1	breq2d	$⊢ k = K \to (D ∥ k P^{N} \leftrightarrow D ∥ K P^{N})$
3		oveq1	$⊢ k = K \to k P^{N - 1} = K P^{N - 1}$
4	3	breq2d	$⊢ k = K \to (D ∥ k P^{N - 1} \leftrightarrow D ∥ K P^{N - 1})$
5	4	notbid	$⊢ k = K \to (\neg D ∥ k P^{N - 1} \leftrightarrow \neg D ∥ K P^{N - 1})$
6	2 5	anbi12d	$⊢ k = K \to ((D ∥ k P^{N} \land \neg D ∥ k P^{N - 1}) \leftrightarrow (D ∥ K P^{N} \land \neg D ∥ K P^{N - 1}))$
7	6	imbi1d	$⊢ k = K \to (((D ∥ k P^{N} \land \neg D ∥ k P^{N - 1}) \to P^{N} ∥ D) \leftrightarrow ((D ∥ K P^{N} \land \neg D ∥ K P^{N - 1}) \to P^{N} ∥ D))$
8		oveq2	$⊢ x = 1 \to P^{x} = P^{1}$
9	8	oveq2d	$⊢ x = 1 \to k P^{x} = k P^{1}$
10	9	breq2d	$⊢ x = 1 \to (D ∥ k P^{x} \leftrightarrow D ∥ k P^{1})$
11		oveq1	$⊢ x = 1 \to x - 1 = 1 - 1$
12	11	oveq2d	$⊢ x = 1 \to P^{x - 1} = P^{1 - 1}$
13	12	oveq2d	$⊢ x = 1 \to k P^{x - 1} = k P^{1 - 1}$
14	13	breq2d	$⊢ x = 1 \to (D ∥ k P^{x - 1} \leftrightarrow D ∥ k P^{1 - 1})$
15	14	notbid	$⊢ x = 1 \to (\neg D ∥ k P^{x - 1} \leftrightarrow \neg D ∥ k P^{1 - 1})$
16	10 15	anbi12d	$⊢ x = 1 \to ((D ∥ k P^{x} \land \neg D ∥ k P^{x - 1}) \leftrightarrow (D ∥ k P^{1} \land \neg D ∥ k P^{1 - 1}))$
17	8	breq1d	$⊢ x = 1 \to (P^{x} ∥ D \leftrightarrow P^{1} ∥ D)$
18	16 17	imbi12d	$⊢ x = 1 \to (((D ∥ k P^{x} \land \neg D ∥ k P^{x - 1}) \to P^{x} ∥ D) \leftrightarrow ((D ∥ k P^{1} \land \neg D ∥ k P^{1 - 1}) \to P^{1} ∥ D))$
19	18	ralbidv	$⊢ x = 1 \to (\forall k \in ℤ ((D ∥ k P^{x} \land \neg D ∥ k P^{x - 1}) \to P^{x} ∥ D) \leftrightarrow \forall k \in ℤ ((D ∥ k P^{1} \land \neg D ∥ k P^{1 - 1}) \to P^{1} ∥ D))$
20	19	imbi2d	$⊢ x = 1 \to (((D \in ℤ \land P \in ℙ) \to \forall k \in ℤ ((D ∥ k P^{x} \land \neg D ∥ k P^{x - 1}) \to P^{x} ∥ D)) \leftrightarrow ((D \in ℤ \land P \in ℙ) \to \forall k \in ℤ ((D ∥ k P^{1} \land \neg D ∥ k P^{1 - 1}) \to P^{1} ∥ D)))$
21		oveq2	$⊢ x = n \to P^{x} = P^{n}$
22	21	oveq2d	$⊢ x = n \to k P^{x} = k P^{n}$
23	22	breq2d	$⊢ x = n \to (D ∥ k P^{x} \leftrightarrow D ∥ k P^{n})$
24		oveq1	$⊢ x = n \to x - 1 = n - 1$
25	24	oveq2d	$⊢ x = n \to P^{x - 1} = P^{n - 1}$
26	25	oveq2d	$⊢ x = n \to k P^{x - 1} = k P^{n - 1}$
27	26	breq2d	$⊢ x = n \to (D ∥ k P^{x - 1} \leftrightarrow D ∥ k P^{n - 1})$
28	27	notbid	$⊢ x = n \to (\neg D ∥ k P^{x - 1} \leftrightarrow \neg D ∥ k P^{n - 1})$
29	23 28	anbi12d	$⊢ x = n \to ((D ∥ k P^{x} \land \neg D ∥ k P^{x - 1}) \leftrightarrow (D ∥ k P^{n} \land \neg D ∥ k P^{n - 1}))$
30	21	breq1d	$⊢ x = n \to (P^{x} ∥ D \leftrightarrow P^{n} ∥ D)$
31	29 30	imbi12d	$⊢ x = n \to (((D ∥ k P^{x} \land \neg D ∥ k P^{x - 1}) \to P^{x} ∥ D) \leftrightarrow ((D ∥ k P^{n} \land \neg D ∥ k P^{n - 1}) \to P^{n} ∥ D))$
32	31	ralbidv	$⊢ x = n \to (\forall k \in ℤ ((D ∥ k P^{x} \land \neg D ∥ k P^{x - 1}) \to P^{x} ∥ D) \leftrightarrow \forall k \in ℤ ((D ∥ k P^{n} \land \neg D ∥ k P^{n - 1}) \to P^{n} ∥ D))$
33	32	imbi2d	$⊢ x = n \to (((D \in ℤ \land P \in ℙ) \to \forall k \in ℤ ((D ∥ k P^{x} \land \neg D ∥ k P^{x - 1}) \to P^{x} ∥ D)) \leftrightarrow ((D \in ℤ \land P \in ℙ) \to \forall k \in ℤ ((D ∥ k P^{n} \land \neg D ∥ k P^{n - 1}) \to P^{n} ∥ D)))$
34		oveq2	$⊢ x = n + 1 \to P^{x} = P^{n + 1}$
35	34	oveq2d	$⊢ x = n + 1 \to k P^{x} = k P^{n + 1}$
36	35	breq2d	$⊢ x = n + 1 \to (D ∥ k P^{x} \leftrightarrow D ∥ k P^{n + 1})$
37		oveq1	$⊢ x = n + 1 \to x - 1 = n + 1 - 1$
38	37	oveq2d	$⊢ x = n + 1 \to P^{x - 1} = P^{n + 1 - 1}$
39	38	oveq2d	$⊢ x = n + 1 \to k P^{x - 1} = k P^{n + 1 - 1}$
40	39	breq2d	$⊢ x = n + 1 \to (D ∥ k P^{x - 1} \leftrightarrow D ∥ k P^{n + 1 - 1})$
41	40	notbid	$⊢ x = n + 1 \to (\neg D ∥ k P^{x - 1} \leftrightarrow \neg D ∥ k P^{n + 1 - 1})$
42	36 41	anbi12d	$⊢ x = n + 1 \to ((D ∥ k P^{x} \land \neg D ∥ k P^{x - 1}) \leftrightarrow (D ∥ k P^{n + 1} \land \neg D ∥ k P^{n + 1 - 1}))$
43	34	breq1d	$⊢ x = n + 1 \to (P^{x} ∥ D \leftrightarrow P^{n + 1} ∥ D)$
44	42 43	imbi12d	$⊢ x = n + 1 \to (((D ∥ k P^{x} \land \neg D ∥ k P^{x - 1}) \to P^{x} ∥ D) \leftrightarrow ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n + 1 - 1}) \to P^{n + 1} ∥ D))$
45	44	ralbidv	$⊢ x = n + 1 \to (\forall k \in ℤ ((D ∥ k P^{x} \land \neg D ∥ k P^{x - 1}) \to P^{x} ∥ D) \leftrightarrow \forall k \in ℤ ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n + 1 - 1}) \to P^{n + 1} ∥ D))$
46	45	imbi2d	$⊢ x = n + 1 \to (((D \in ℤ \land P \in ℙ) \to \forall k \in ℤ ((D ∥ k P^{x} \land \neg D ∥ k P^{x - 1}) \to P^{x} ∥ D)) \leftrightarrow ((D \in ℤ \land P \in ℙ) \to \forall k \in ℤ ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n + 1 - 1}) \to P^{n + 1} ∥ D)))$
47		oveq2	$⊢ x = N \to P^{x} = P^{N}$
48	47	oveq2d	$⊢ x = N \to k P^{x} = k P^{N}$
49	48	breq2d	$⊢ x = N \to (D ∥ k P^{x} \leftrightarrow D ∥ k P^{N})$
50		oveq1	$⊢ x = N \to x - 1 = N - 1$
51	50	oveq2d	$⊢ x = N \to P^{x - 1} = P^{N - 1}$
52	51	oveq2d	$⊢ x = N \to k P^{x - 1} = k P^{N - 1}$
53	52	breq2d	$⊢ x = N \to (D ∥ k P^{x - 1} \leftrightarrow D ∥ k P^{N - 1})$
54	53	notbid	$⊢ x = N \to (\neg D ∥ k P^{x - 1} \leftrightarrow \neg D ∥ k P^{N - 1})$
55	49 54	anbi12d	$⊢ x = N \to ((D ∥ k P^{x} \land \neg D ∥ k P^{x - 1}) \leftrightarrow (D ∥ k P^{N} \land \neg D ∥ k P^{N - 1}))$
56	47	breq1d	$⊢ x = N \to (P^{x} ∥ D \leftrightarrow P^{N} ∥ D)$
57	55 56	imbi12d	$⊢ x = N \to (((D ∥ k P^{x} \land \neg D ∥ k P^{x - 1}) \to P^{x} ∥ D) \leftrightarrow ((D ∥ k P^{N} \land \neg D ∥ k P^{N - 1}) \to P^{N} ∥ D))$
58	57	ralbidv	$⊢ x = N \to (\forall k \in ℤ ((D ∥ k P^{x} \land \neg D ∥ k P^{x - 1}) \to P^{x} ∥ D) \leftrightarrow \forall k \in ℤ ((D ∥ k P^{N} \land \neg D ∥ k P^{N - 1}) \to P^{N} ∥ D))$
59	58	imbi2d	$⊢ x = N \to (((D \in ℤ \land P \in ℙ) \to \forall k \in ℤ ((D ∥ k P^{x} \land \neg D ∥ k P^{x - 1}) \to P^{x} ∥ D)) \leftrightarrow ((D \in ℤ \land P \in ℙ) \to \forall k \in ℤ ((D ∥ k P^{N} \land \neg D ∥ k P^{N - 1}) \to P^{N} ∥ D)))$
60		breq1	$⊢ x = D \to (x ∥ k P \leftrightarrow D ∥ k P)$
61		breq1	$⊢ x = D \to (x ∥ k \leftrightarrow D ∥ k)$
62	61	notbid	$⊢ x = D \to (\neg x ∥ k \leftrightarrow \neg D ∥ k)$
63	60 62	anbi12d	$⊢ x = D \to ((x ∥ k P \land \neg x ∥ k) \leftrightarrow (D ∥ k P \land \neg D ∥ k))$
64		breq2	$⊢ x = D \to (P ∥ x \leftrightarrow P ∥ D)$
65	63 64	imbi12d	$⊢ x = D \to (((x ∥ k P \land \neg x ∥ k) \to P ∥ x) \leftrightarrow ((D ∥ k P \land \neg D ∥ k) \to P ∥ D))$
66	65	imbi2d	$⊢ x = D \to (((P \in ℙ \land k \in ℤ) \to ((x ∥ k P \land \neg x ∥ k) \to P ∥ x)) \leftrightarrow ((P \in ℙ \land k \in ℤ) \to ((D ∥ k P \land \neg D ∥ k) \to P ∥ D)))$
67		simplrl	$⊢ ((x \in ℤ \land (P \in ℙ \land k \in ℤ)) \land x ∥ k P) \to P \in ℙ$
68		simpll	$⊢ ((x \in ℤ \land (P \in ℙ \land k \in ℤ)) \land x ∥ k P) \to x \in ℤ$
69		coprm	$⊢ (P \in ℙ \land x \in ℤ) \to (\neg P ∥ x \leftrightarrow P \gcd x = 1)$
70	67 68 69	syl2anc	$⊢ ((x \in ℤ \land (P \in ℙ \land k \in ℤ)) \land x ∥ k P) \to (\neg P ∥ x \leftrightarrow P \gcd x = 1)$
71		zcn	$⊢ k \in ℤ \to k \in ℂ$
72	71	ad2antll	$⊢ (x \in ℤ \land (P \in ℙ \land k \in ℤ)) \to k \in ℂ$
73		prmz	$⊢ P \in ℙ \to P \in ℤ$
74	73	ad2antrl	$⊢ (x \in ℤ \land (P \in ℙ \land k \in ℤ)) \to P \in ℤ$
75	74	zcnd	$⊢ (x \in ℤ \land (P \in ℙ \land k \in ℤ)) \to P \in ℂ$
76	72 75	mulcomd	$⊢ (x \in ℤ \land (P \in ℙ \land k \in ℤ)) \to k P = P k$
77	76	breq2d	$⊢ (x \in ℤ \land (P \in ℙ \land k \in ℤ)) \to (x ∥ k P \leftrightarrow x ∥ P k)$
78		simpl	$⊢ (x \in ℤ \land (P \in ℙ \land k \in ℤ)) \to x \in ℤ$
79	74 78	gcdcomd	$⊢ (x \in ℤ \land (P \in ℙ \land k \in ℤ)) \to P \gcd x = x \gcd P$
80	79	eqeq1d	$⊢ (x \in ℤ \land (P \in ℙ \land k \in ℤ)) \to (P \gcd x = 1 \leftrightarrow x \gcd P = 1)$
81	77 80	anbi12d	$⊢ (x \in ℤ \land (P \in ℙ \land k \in ℤ)) \to ((x ∥ k P \land P \gcd x = 1) \leftrightarrow (x ∥ P k \land x \gcd P = 1))$
82		simprr	$⊢ (x \in ℤ \land (P \in ℙ \land k \in ℤ)) \to k \in ℤ$
83		coprmdvds	$⊢ (x \in ℤ \land P \in ℤ \land k \in ℤ) \to ((x ∥ P k \land x \gcd P = 1) \to x ∥ k)$
84	78 74 82 83	syl3anc	$⊢ (x \in ℤ \land (P \in ℙ \land k \in ℤ)) \to ((x ∥ P k \land x \gcd P = 1) \to x ∥ k)$
85	81 84	sylbid	$⊢ (x \in ℤ \land (P \in ℙ \land k \in ℤ)) \to ((x ∥ k P \land P \gcd x = 1) \to x ∥ k)$
86	85	expdimp	$⊢ ((x \in ℤ \land (P \in ℙ \land k \in ℤ)) \land x ∥ k P) \to (P \gcd x = 1 \to x ∥ k)$
87	70 86	sylbid	$⊢ ((x \in ℤ \land (P \in ℙ \land k \in ℤ)) \land x ∥ k P) \to (\neg P ∥ x \to x ∥ k)$
88	87	con1d	$⊢ ((x \in ℤ \land (P \in ℙ \land k \in ℤ)) \land x ∥ k P) \to (\neg x ∥ k \to P ∥ x)$
89	88	expimpd	$⊢ (x \in ℤ \land (P \in ℙ \land k \in ℤ)) \to ((x ∥ k P \land \neg x ∥ k) \to P ∥ x)$
90	89	ex	$⊢ x \in ℤ \to ((P \in ℙ \land k \in ℤ) \to ((x ∥ k P \land \neg x ∥ k) \to P ∥ x))$
91	66 90	vtoclga	$⊢ D \in ℤ \to ((P \in ℙ \land k \in ℤ) \to ((D ∥ k P \land \neg D ∥ k) \to P ∥ D))$
92	91	impl	$⊢ ((D \in ℤ \land P \in ℙ) \land k \in ℤ) \to ((D ∥ k P \land \neg D ∥ k) \to P ∥ D)$
93	73	zcnd	$⊢ P \in ℙ \to P \in ℂ$
94	93	exp1d	$⊢ P \in ℙ \to P^{1} = P$
95	94	ad2antlr	$⊢ ((D \in ℤ \land P \in ℙ) \land k \in ℤ) \to P^{1} = P$
96	95	oveq2d	$⊢ ((D \in ℤ \land P \in ℙ) \land k \in ℤ) \to k P^{1} = k P$
97	96	breq2d	$⊢ ((D \in ℤ \land P \in ℙ) \land k \in ℤ) \to (D ∥ k P^{1} \leftrightarrow D ∥ k P)$
98		1m1e0	$⊢ 1 - 1 = 0$
99	98	oveq2i	$⊢ P^{1 - 1} = P^{0}$
100	73	ad2antlr	$⊢ ((D \in ℤ \land P \in ℙ) \land k \in ℤ) \to P \in ℤ$
101	100	zcnd	$⊢ ((D \in ℤ \land P \in ℙ) \land k \in ℤ) \to P \in ℂ$
102	101	exp0d	$⊢ ((D \in ℤ \land P \in ℙ) \land k \in ℤ) \to P^{0} = 1$
103	99 102	eqtrid	$⊢ ((D \in ℤ \land P \in ℙ) \land k \in ℤ) \to P^{1 - 1} = 1$
104	103	oveq2d	$⊢ ((D \in ℤ \land P \in ℙ) \land k \in ℤ) \to k P^{1 - 1} = k \cdot 1$
105	71	adantl	$⊢ ((D \in ℤ \land P \in ℙ) \land k \in ℤ) \to k \in ℂ$
106	105	mulid1d	$⊢ ((D \in ℤ \land P \in ℙ) \land k \in ℤ) \to k \cdot 1 = k$
107	104 106	eqtrd	$⊢ ((D \in ℤ \land P \in ℙ) \land k \in ℤ) \to k P^{1 - 1} = k$
108	107	breq2d	$⊢ ((D \in ℤ \land P \in ℙ) \land k \in ℤ) \to (D ∥ k P^{1 - 1} \leftrightarrow D ∥ k)$
109	108	notbid	$⊢ ((D \in ℤ \land P \in ℙ) \land k \in ℤ) \to (\neg D ∥ k P^{1 - 1} \leftrightarrow \neg D ∥ k)$
110	97 109	anbi12d	$⊢ ((D \in ℤ \land P \in ℙ) \land k \in ℤ) \to ((D ∥ k P^{1} \land \neg D ∥ k P^{1 - 1}) \leftrightarrow (D ∥ k P \land \neg D ∥ k))$
111	101	exp1d	$⊢ ((D \in ℤ \land P \in ℙ) \land k \in ℤ) \to P^{1} = P$
112	111	breq1d	$⊢ ((D \in ℤ \land P \in ℙ) \land k \in ℤ) \to (P^{1} ∥ D \leftrightarrow P ∥ D)$
113	92 110 112	3imtr4d	$⊢ ((D \in ℤ \land P \in ℙ) \land k \in ℤ) \to ((D ∥ k P^{1} \land \neg D ∥ k P^{1 - 1}) \to P^{1} ∥ D)$
114	113	ralrimiva	$⊢ (D \in ℤ \land P \in ℙ) \to \forall k \in ℤ ((D ∥ k P^{1} \land \neg D ∥ k P^{1 - 1}) \to P^{1} ∥ D)$
115		oveq1	$⊢ k = x \to k P^{n} = x P^{n}$
116	115	breq2d	$⊢ k = x \to (D ∥ k P^{n} \leftrightarrow D ∥ x P^{n})$
117		oveq1	$⊢ k = x \to k P^{n - 1} = x P^{n - 1}$
118	117	breq2d	$⊢ k = x \to (D ∥ k P^{n - 1} \leftrightarrow D ∥ x P^{n - 1})$
119	118	notbid	$⊢ k = x \to (\neg D ∥ k P^{n - 1} \leftrightarrow \neg D ∥ x P^{n - 1})$
120	116 119	anbi12d	$⊢ k = x \to ((D ∥ k P^{n} \land \neg D ∥ k P^{n - 1}) \leftrightarrow (D ∥ x P^{n} \land \neg D ∥ x P^{n - 1}))$
121	120	imbi1d	$⊢ k = x \to (((D ∥ k P^{n} \land \neg D ∥ k P^{n - 1}) \to P^{n} ∥ D) \leftrightarrow ((D ∥ x P^{n} \land \neg D ∥ x P^{n - 1}) \to P^{n} ∥ D))$
122	121	cbvralvw	$⊢ \forall k \in ℤ ((D ∥ k P^{n} \land \neg D ∥ k P^{n - 1}) \to P^{n} ∥ D) \leftrightarrow \forall x \in ℤ ((D ∥ x P^{n} \land \neg D ∥ x P^{n - 1}) \to P^{n} ∥ D)$
123		simprr	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to k \in ℤ$
124	73	ad2antrl	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P \in ℤ$
125	123 124	zmulcld	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to k P \in ℤ$
126		oveq1	$⊢ x = k P \to x P^{n} = k P P^{n}$
127	126	breq2d	$⊢ x = k P \to (D ∥ x P^{n} \leftrightarrow D ∥ k P P^{n})$
128		oveq1	$⊢ x = k P \to x P^{n - 1} = k P P^{n - 1}$
129	128	breq2d	$⊢ x = k P \to (D ∥ x P^{n - 1} \leftrightarrow D ∥ k P P^{n - 1})$
130	129	notbid	$⊢ x = k P \to (\neg D ∥ x P^{n - 1} \leftrightarrow \neg D ∥ k P P^{n - 1})$
131	127 130	anbi12d	$⊢ x = k P \to ((D ∥ x P^{n} \land \neg D ∥ x P^{n - 1}) \leftrightarrow (D ∥ k P P^{n} \land \neg D ∥ k P P^{n - 1}))$
132	131	imbi1d	$⊢ x = k P \to (((D ∥ x P^{n} \land \neg D ∥ x P^{n - 1}) \to P^{n} ∥ D) \leftrightarrow ((D ∥ k P P^{n} \land \neg D ∥ k P P^{n - 1}) \to P^{n} ∥ D))$
133	132	rspcv	$⊢ k P \in ℤ \to (\forall x \in ℤ ((D ∥ x P^{n} \land \neg D ∥ x P^{n - 1}) \to P^{n} ∥ D) \to ((D ∥ k P P^{n} \land \neg D ∥ k P P^{n - 1}) \to P^{n} ∥ D))$
134	125 133	syl	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (\forall x \in ℤ ((D ∥ x P^{n} \land \neg D ∥ x P^{n - 1}) \to P^{n} ∥ D) \to ((D ∥ k P P^{n} \land \neg D ∥ k P P^{n - 1}) \to P^{n} ∥ D))$
135		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
136	135	ad2antrr	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to n \in ℕ_{0}$
137		zexpcl	$⊢ (P \in ℤ \land n \in ℕ_{0}) \to P^{n} \in ℤ$
138	124 136 137	syl2anc	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P^{n} \in ℤ$
139		simplr	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to D \in ℤ$
140		divides	$⊢ (P^{n} \in ℤ \land D \in ℤ) \to (P^{n} ∥ D \leftrightarrow \exists x \in ℤ x P^{n} = D)$
141	138 139 140	syl2anc	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (P^{n} ∥ D \leftrightarrow \exists x \in ℤ x P^{n} = D)$
142	89	adantll	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to ((x ∥ k P \land \neg x ∥ k) \to P ∥ x)$
143		prmnn	$⊢ P \in ℙ \to P \in ℕ$
144	143	ad2antrl	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P \in ℕ$
145	144	nncnd	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P \in ℂ$
146	135	ad2antrr	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to n \in ℕ_{0}$
147	145 146	expp1d	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P^{n + 1} = P^{n} P$
148	144 146	nnexpcld	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P^{n} \in ℕ$
149	148	nncnd	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P^{n} \in ℂ$
150	149 145	mulcomd	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P^{n} P = P P^{n}$
151	147 150	eqtrd	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P^{n + 1} = P P^{n}$
152	151	oveq2d	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to k P^{n + 1} = k P P^{n}$
153	71	ad2antll	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to k \in ℂ$
154	153 145 149	mulassd	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to k P P^{n} = k P P^{n}$
155	152 154	eqtr4d	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to k P^{n + 1} = k P P^{n}$
156	155	breq2d	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (x P^{n} ∥ k P^{n + 1} \leftrightarrow x P^{n} ∥ k P P^{n})$
157		simplr	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to x \in ℤ$
158		simprr	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to k \in ℤ$
159	144	nnzd	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P \in ℤ$
160	158 159	zmulcld	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to k P \in ℤ$
161	148	nnzd	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P^{n} \in ℤ$
162	148	nnne0d	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P^{n} \neq 0$
163		dvdsmulcr	$⊢ (x \in ℤ \land k P \in ℤ \land (P^{n} \in ℤ \land P^{n} \neq 0)) \to (x P^{n} ∥ k P P^{n} \leftrightarrow x ∥ k P)$
164	157 160 161 162 163	syl112anc	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (x P^{n} ∥ k P P^{n} \leftrightarrow x ∥ k P)$
165	156 164	bitrd	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (x P^{n} ∥ k P^{n + 1} \leftrightarrow x ∥ k P)$
166		dvdsmulcr	$⊢ (x \in ℤ \land k \in ℤ \land (P^{n} \in ℤ \land P^{n} \neq 0)) \to (x P^{n} ∥ k P^{n} \leftrightarrow x ∥ k)$
167	157 158 161 162 166	syl112anc	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (x P^{n} ∥ k P^{n} \leftrightarrow x ∥ k)$
168	167	notbid	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (\neg x P^{n} ∥ k P^{n} \leftrightarrow \neg x ∥ k)$
169	165 168	anbi12d	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to ((x P^{n} ∥ k P^{n + 1} \land \neg x P^{n} ∥ k P^{n}) \leftrightarrow (x ∥ k P \land \neg x ∥ k))$
170	151	breq1d	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (P^{n + 1} ∥ x P^{n} \leftrightarrow P P^{n} ∥ x P^{n})$
171		dvdsmulcr	$⊢ (P \in ℤ \land x \in ℤ \land (P^{n} \in ℤ \land P^{n} \neq 0)) \to (P P^{n} ∥ x P^{n} \leftrightarrow P ∥ x)$
172	159 157 161 162 171	syl112anc	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (P P^{n} ∥ x P^{n} \leftrightarrow P ∥ x)$
173	170 172	bitrd	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (P^{n + 1} ∥ x P^{n} \leftrightarrow P ∥ x)$
174	142 169 173	3imtr4d	$⊢ ((n \in ℕ \land x \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to ((x P^{n} ∥ k P^{n + 1} \land \neg x P^{n} ∥ k P^{n}) \to P^{n + 1} ∥ x P^{n})$
175	174	an32s	$⊢ ((n \in ℕ \land (P \in ℙ \land k \in ℤ)) \land x \in ℤ) \to ((x P^{n} ∥ k P^{n + 1} \land \neg x P^{n} ∥ k P^{n}) \to P^{n + 1} ∥ x P^{n})$
176		breq1	$⊢ x P^{n} = D \to (x P^{n} ∥ k P^{n + 1} \leftrightarrow D ∥ k P^{n + 1})$
177		breq1	$⊢ x P^{n} = D \to (x P^{n} ∥ k P^{n} \leftrightarrow D ∥ k P^{n})$
178	177	notbid	$⊢ x P^{n} = D \to (\neg x P^{n} ∥ k P^{n} \leftrightarrow \neg D ∥ k P^{n})$
179	176 178	anbi12d	$⊢ x P^{n} = D \to ((x P^{n} ∥ k P^{n + 1} \land \neg x P^{n} ∥ k P^{n}) \leftrightarrow (D ∥ k P^{n + 1} \land \neg D ∥ k P^{n}))$
180		breq2	$⊢ x P^{n} = D \to (P^{n + 1} ∥ x P^{n} \leftrightarrow P^{n + 1} ∥ D)$
181	179 180	imbi12d	$⊢ x P^{n} = D \to (((x P^{n} ∥ k P^{n + 1} \land \neg x P^{n} ∥ k P^{n}) \to P^{n + 1} ∥ x P^{n}) \leftrightarrow ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n}) \to P^{n + 1} ∥ D))$
182	175 181	syl5ibcom	$⊢ ((n \in ℕ \land (P \in ℙ \land k \in ℤ)) \land x \in ℤ) \to (x P^{n} = D \to ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n}) \to P^{n + 1} ∥ D))$
183	182	rexlimdva	$⊢ (n \in ℕ \land (P \in ℙ \land k \in ℤ)) \to (\exists x \in ℤ x P^{n} = D \to ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n}) \to P^{n + 1} ∥ D))$
184	183	adantlr	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (\exists x \in ℤ x P^{n} = D \to ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n}) \to P^{n + 1} ∥ D))$
185	141 184	sylbid	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (P^{n} ∥ D \to ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n}) \to P^{n + 1} ∥ D))$
186	185	com23	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n}) \to (P^{n} ∥ D \to P^{n + 1} ∥ D))$
187	186	a2d	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n}) \to P^{n} ∥ D) \to ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n}) \to P^{n + 1} ∥ D))$
188	71	ad2antll	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to k \in ℂ$
189	124	zcnd	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P \in ℂ$
190	138	zcnd	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P^{n} \in ℂ$
191	188 189 190	mulassd	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to k P P^{n} = k P P^{n}$
192	189 190	mulcomd	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P P^{n} = P^{n} P$
193	189 136	expp1d	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P^{n + 1} = P^{n} P$
194	192 193	eqtr4d	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P P^{n} = P^{n + 1}$
195	194	oveq2d	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to k P P^{n} = k P^{n + 1}$
196	191 195	eqtrd	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to k P P^{n} = k P^{n + 1}$
197	196	breq2d	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (D ∥ k P P^{n} \leftrightarrow D ∥ k P^{n + 1})$
198		nnm1nn0	$⊢ n \in ℕ \to n - 1 \in ℕ_{0}$
199	198	ad2antrr	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to n - 1 \in ℕ_{0}$
200		zexpcl	$⊢ (P \in ℤ \land n - 1 \in ℕ_{0}) \to P^{n - 1} \in ℤ$
201	124 199 200	syl2anc	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P^{n - 1} \in ℤ$
202	201	zcnd	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P^{n - 1} \in ℂ$
203	188 189 202	mulassd	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to k P P^{n - 1} = k P P^{n - 1}$
204	189 202	mulcomd	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P P^{n - 1} = P^{n - 1} P$
205		simpll	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to n \in ℕ$
206		expm1t	$⊢ (P \in ℂ \land n \in ℕ) \to P^{n} = P^{n - 1} P$
207	189 205 206	syl2anc	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P^{n} = P^{n - 1} P$
208	204 207	eqtr4d	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P P^{n - 1} = P^{n}$
209	208	oveq2d	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to k P P^{n - 1} = k P^{n}$
210	203 209	eqtrd	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to k P P^{n - 1} = k P^{n}$
211	210	breq2d	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (D ∥ k P P^{n - 1} \leftrightarrow D ∥ k P^{n})$
212	211	notbid	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (\neg D ∥ k P P^{n - 1} \leftrightarrow \neg D ∥ k P^{n})$
213	197 212	anbi12d	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to ((D ∥ k P P^{n} \land \neg D ∥ k P P^{n - 1}) \leftrightarrow (D ∥ k P^{n + 1} \land \neg D ∥ k P^{n}))$
214	213	imbi1d	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (((D ∥ k P P^{n} \land \neg D ∥ k P P^{n - 1}) \to P^{n} ∥ D) \leftrightarrow ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n}) \to P^{n} ∥ D))$
215		nncn	$⊢ n \in ℕ \to n \in ℂ$
216	215	ad2antrr	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to n \in ℂ$
217		ax-1cn	$⊢ 1 \in ℂ$
218		pncan	$⊢ (n \in ℂ \land 1 \in ℂ) \to n + 1 - 1 = n$
219	216 217 218	sylancl	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to n + 1 - 1 = n$
220	219	oveq2d	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to P^{n + 1 - 1} = P^{n}$
221	220	oveq2d	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to k P^{n + 1 - 1} = k P^{n}$
222	221	breq2d	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (D ∥ k P^{n + 1 - 1} \leftrightarrow D ∥ k P^{n})$
223	222	notbid	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (\neg D ∥ k P^{n + 1 - 1} \leftrightarrow \neg D ∥ k P^{n})$
224	223	anbi2d	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n + 1 - 1}) \leftrightarrow (D ∥ k P^{n + 1} \land \neg D ∥ k P^{n}))$
225	224	imbi1d	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n + 1 - 1}) \to P^{n + 1} ∥ D) \leftrightarrow ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n}) \to P^{n + 1} ∥ D))$
226	187 214 225	3imtr4d	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (((D ∥ k P P^{n} \land \neg D ∥ k P P^{n - 1}) \to P^{n} ∥ D) \to ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n + 1 - 1}) \to P^{n + 1} ∥ D))$
227	134 226	syld	$⊢ ((n \in ℕ \land D \in ℤ) \land (P \in ℙ \land k \in ℤ)) \to (\forall x \in ℤ ((D ∥ x P^{n} \land \neg D ∥ x P^{n - 1}) \to P^{n} ∥ D) \to ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n + 1 - 1}) \to P^{n + 1} ∥ D))$
228	227	anassrs	$⊢ (((n \in ℕ \land D \in ℤ) \land P \in ℙ) \land k \in ℤ) \to (\forall x \in ℤ ((D ∥ x P^{n} \land \neg D ∥ x P^{n - 1}) \to P^{n} ∥ D) \to ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n + 1 - 1}) \to P^{n + 1} ∥ D))$
229	228	ralrimdva	$⊢ ((n \in ℕ \land D \in ℤ) \land P \in ℙ) \to (\forall x \in ℤ ((D ∥ x P^{n} \land \neg D ∥ x P^{n - 1}) \to P^{n} ∥ D) \to \forall k \in ℤ ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n + 1 - 1}) \to P^{n + 1} ∥ D))$
230	122 229	syl5bi	$⊢ ((n \in ℕ \land D \in ℤ) \land P \in ℙ) \to (\forall k \in ℤ ((D ∥ k P^{n} \land \neg D ∥ k P^{n - 1}) \to P^{n} ∥ D) \to \forall k \in ℤ ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n + 1 - 1}) \to P^{n + 1} ∥ D))$
231	230	expl	$⊢ n \in ℕ \to ((D \in ℤ \land P \in ℙ) \to (\forall k \in ℤ ((D ∥ k P^{n} \land \neg D ∥ k P^{n - 1}) \to P^{n} ∥ D) \to \forall k \in ℤ ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n + 1 - 1}) \to P^{n + 1} ∥ D)))$
232	231	a2d	$⊢ n \in ℕ \to (((D \in ℤ \land P \in ℙ) \to \forall k \in ℤ ((D ∥ k P^{n} \land \neg D ∥ k P^{n - 1}) \to P^{n} ∥ D)) \to ((D \in ℤ \land P \in ℙ) \to \forall k \in ℤ ((D ∥ k P^{n + 1} \land \neg D ∥ k P^{n + 1 - 1}) \to P^{n + 1} ∥ D)))$
233	20 33 46 59 114 232	nnind	$⊢ N \in ℕ \to ((D \in ℤ \land P \in ℙ) \to \forall k \in ℤ ((D ∥ k P^{N} \land \neg D ∥ k P^{N - 1}) \to P^{N} ∥ D))$
234	233	com12	$⊢ (D \in ℤ \land P \in ℙ) \to (N \in ℕ \to \forall k \in ℤ ((D ∥ k P^{N} \land \neg D ∥ k P^{N - 1}) \to P^{N} ∥ D))$
235	234	impr	$⊢ (D \in ℤ \land (P \in ℙ \land N \in ℕ)) \to \forall k \in ℤ ((D ∥ k P^{N} \land \neg D ∥ k P^{N - 1}) \to P^{N} ∥ D)$
236	235	adantll	$⊢ ((K \in ℤ \land D \in ℤ) \land (P \in ℙ \land N \in ℕ)) \to \forall k \in ℤ ((D ∥ k P^{N} \land \neg D ∥ k P^{N - 1}) \to P^{N} ∥ D)$
237		simpll	$⊢ ((K \in ℤ \land D \in ℤ) \land (P \in ℙ \land N \in ℕ)) \to K \in ℤ$
238	7 236 237	rspcdva	$⊢ ((K \in ℤ \land D \in ℤ) \land (P \in ℙ \land N \in ℕ)) \to ((D ∥ K P^{N} \land \neg D ∥ K P^{N - 1}) \to P^{N} ∥ D)$
239	238	3impia	$⊢ ((K \in ℤ \land D \in ℤ) \land (P \in ℙ \land N \in ℕ) \land (D ∥ K P^{N} \land \neg D ∥ K P^{N - 1})) \to P^{N} ∥ D$

Metamath Proof Explorer

Theorem prmpwdvds

Proof