pcdvdsb

Description: P ^ A divides N if and only if A is at most the count of P . (Contributed by Mario Carneiro, 3-Oct-2014)

		Ref	Expression
	Assertion	pcdvdsb	$⊢ (P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \to (A \leq P pCnt N \leftrightarrow P^{A} ∥ N)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ N = 0 \to P pCnt N = P pCnt 0$
2	1	breq2d	$⊢ N = 0 \to (A \leq P pCnt N \leftrightarrow A \leq P pCnt 0)$
3		breq2	$⊢ N = 0 \to (P^{A} ∥ N \leftrightarrow P^{A} ∥ 0)$
4	2 3	bibi12d	$⊢ N = 0 \to ((A \leq P pCnt N \leftrightarrow P^{A} ∥ N) \leftrightarrow (A \leq P pCnt 0 \leftrightarrow P^{A} ∥ 0))$
5		simpl3	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to A \in ℕ_{0}$
6	5	nn0zd	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to A \in ℤ$
7		simpl1	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to P \in ℙ$
8		simpl2	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to N \in ℤ$
9		simpr	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to N \neq 0$
10		pczcl	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to P pCnt N \in ℕ_{0}$
11	7 8 9 10	syl12anc	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to P pCnt N \in ℕ_{0}$
12	11	nn0zd	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to P pCnt N \in ℤ$
13		eluz	$⊢ (A \in ℤ \land P pCnt N \in ℤ) \to (P pCnt N \in ℤ_{\geq A} \leftrightarrow A \leq P pCnt N)$
14	6 12 13	syl2anc	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to (P pCnt N \in ℤ_{\geq A} \leftrightarrow A \leq P pCnt N)$
15		prmnn	$⊢ P \in ℙ \to P \in ℕ$
16	7 15	syl	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to P \in ℕ$
17	16	nnzd	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to P \in ℤ$
18		dvdsexp	$⊢ (P \in ℤ \land A \in ℕ_{0} \land P pCnt N \in ℤ_{\geq A}) \to P^{A} ∥ P^{P pCnt N}$
19	18	3expia	$⊢ (P \in ℤ \land A \in ℕ_{0}) \to (P pCnt N \in ℤ_{\geq A} \to P^{A} ∥ P^{P pCnt N})$
20	17 5 19	syl2anc	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to (P pCnt N \in ℤ_{\geq A} \to P^{A} ∥ P^{P pCnt N})$
21	14 20	sylbird	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to (A \leq P pCnt N \to P^{A} ∥ P^{P pCnt N})$
22		pczdvds	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to P^{P pCnt N} ∥ N$
23	7 8 9 22	syl12anc	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to P^{P pCnt N} ∥ N$
24		nnexpcl	$⊢ (P \in ℕ \land A \in ℕ_{0}) \to P^{A} \in ℕ$
25	15 24	sylan	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P^{A} \in ℕ$
26	25	3adant2	$⊢ (P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \to P^{A} \in ℕ$
27	26	nnzd	$⊢ (P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \to P^{A} \in ℤ$
28	27	adantr	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to P^{A} \in ℤ$
29	16 11	nnexpcld	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to P^{P pCnt N} \in ℕ$
30	29	nnzd	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to P^{P pCnt N} \in ℤ$
31		dvdstr	$⊢ (P^{A} \in ℤ \land P^{P pCnt N} \in ℤ \land N \in ℤ) \to ((P^{A} ∥ P^{P pCnt N} \land P^{P pCnt N} ∥ N) \to P^{A} ∥ N)$
32	28 30 8 31	syl3anc	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to ((P^{A} ∥ P^{P pCnt N} \land P^{P pCnt N} ∥ N) \to P^{A} ∥ N)$
33	23 32	mpan2d	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to (P^{A} ∥ P^{P pCnt N} \to P^{A} ∥ N)$
34	21 33	syld	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to (A \leq P pCnt N \to P^{A} ∥ N)$
35		nn0re	$⊢ P pCnt N \in ℕ_{0} \to P pCnt N \in ℝ$
36		nn0re	$⊢ A \in ℕ_{0} \to A \in ℝ$
37		ltnle	$⊢ (P pCnt N \in ℝ \land A \in ℝ) \to (P pCnt N < A \leftrightarrow \neg A \leq P pCnt N)$
38	35 36 37	syl2an	$⊢ (P pCnt N \in ℕ_{0} \land A \in ℕ_{0}) \to (P pCnt N < A \leftrightarrow \neg A \leq P pCnt N)$
39		nn0ltp1le	$⊢ (P pCnt N \in ℕ_{0} \land A \in ℕ_{0}) \to (P pCnt N < A \leftrightarrow (P pCnt N) + 1 \leq A)$
40	38 39	bitr3d	$⊢ (P pCnt N \in ℕ_{0} \land A \in ℕ_{0}) \to (\neg A \leq P pCnt N \leftrightarrow (P pCnt N) + 1 \leq A)$
41	11 5 40	syl2anc	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to (\neg A \leq P pCnt N \leftrightarrow (P pCnt N) + 1 \leq A)$
42		peano2nn0	$⊢ P pCnt N \in ℕ_{0} \to (P pCnt N) + 1 \in ℕ_{0}$
43	11 42	syl	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to (P pCnt N) + 1 \in ℕ_{0}$
44	43	nn0zd	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to (P pCnt N) + 1 \in ℤ$
45		eluz	$⊢ ((P pCnt N) + 1 \in ℤ \land A \in ℤ) \to (A \in ℤ_{\geq ((P pCnt N) + 1)} \leftrightarrow (P pCnt N) + 1 \leq A)$
46	44 6 45	syl2anc	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to (A \in ℤ_{\geq ((P pCnt N) + 1)} \leftrightarrow (P pCnt N) + 1 \leq A)$
47		dvdsexp	$⊢ (P \in ℤ \land (P pCnt N) + 1 \in ℕ_{0} \land A \in ℤ_{\geq ((P pCnt N) + 1)}) \to P^{(P pCnt N) + 1} ∥ P^{A}$
48	47	3expia	$⊢ (P \in ℤ \land (P pCnt N) + 1 \in ℕ_{0}) \to (A \in ℤ_{\geq ((P pCnt N) + 1)} \to P^{(P pCnt N) + 1} ∥ P^{A})$
49	17 43 48	syl2anc	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to (A \in ℤ_{\geq ((P pCnt N) + 1)} \to P^{(P pCnt N) + 1} ∥ P^{A})$
50	46 49	sylbird	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to ((P pCnt N) + 1 \leq A \to P^{(P pCnt N) + 1} ∥ P^{A})$
51		pczndvds	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to \neg P^{(P pCnt N) + 1} ∥ N$
52	7 8 9 51	syl12anc	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to \neg P^{(P pCnt N) + 1} ∥ N$
53	16 43	nnexpcld	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to P^{(P pCnt N) + 1} \in ℕ$
54	53	nnzd	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to P^{(P pCnt N) + 1} \in ℤ$
55		dvdstr	$⊢ (P^{(P pCnt N) + 1} \in ℤ \land P^{A} \in ℤ \land N \in ℤ) \to ((P^{(P pCnt N) + 1} ∥ P^{A} \land P^{A} ∥ N) \to P^{(P pCnt N) + 1} ∥ N)$
56	54 28 8 55	syl3anc	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to ((P^{(P pCnt N) + 1} ∥ P^{A} \land P^{A} ∥ N) \to P^{(P pCnt N) + 1} ∥ N)$
57	52 56	mtod	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to \neg (P^{(P pCnt N) + 1} ∥ P^{A} \land P^{A} ∥ N)$
58		imnan	$⊢ (P^{(P pCnt N) + 1} ∥ P^{A} \to \neg P^{A} ∥ N) \leftrightarrow \neg (P^{(P pCnt N) + 1} ∥ P^{A} \land P^{A} ∥ N)$
59	57 58	sylibr	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to (P^{(P pCnt N) + 1} ∥ P^{A} \to \neg P^{A} ∥ N)$
60	50 59	syld	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to ((P pCnt N) + 1 \leq A \to \neg P^{A} ∥ N)$
61	41 60	sylbid	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to (\neg A \leq P pCnt N \to \neg P^{A} ∥ N)$
62	34 61	impcon4bid	$⊢ ((P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \land N \neq 0) \to (A \leq P pCnt N \leftrightarrow P^{A} ∥ N)$
63	36	3ad2ant3	$⊢ (P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \to A \in ℝ$
64	63	rexrd	$⊢ (P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \to A \in ℝ^{*}$
65		pnfge	$⊢ A \in ℝ^{*} \to A \leq +∞$
66	64 65	syl	$⊢ (P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \to A \leq +∞$
67		pc0	$⊢ P \in ℙ \to P pCnt 0 = +∞$
68	67	3ad2ant1	$⊢ (P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \to P pCnt 0 = +∞$
69	66 68	breqtrrd	$⊢ (P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \to A \leq P pCnt 0$
70		dvds0	$⊢ P^{A} \in ℤ \to P^{A} ∥ 0$
71	27 70	syl	$⊢ (P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \to P^{A} ∥ 0$
72	69 71	2thd	$⊢ (P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \to (A \leq P pCnt 0 \leftrightarrow P^{A} ∥ 0)$
73	4 62 72	pm2.61ne	$⊢ (P \in ℙ \land N \in ℤ \land A \in ℕ_{0}) \to (A \leq P pCnt N \leftrightarrow P^{A} ∥ N)$

Metamath Proof Explorer

Theorem pcdvdsb

Proof