pcpre1

Description: Value of the prime power pre-function at 1. (Contributed by Mario Carneiro, 23-Feb-2014) (Revised by Mario Carneiro, 26-Apr-2016)

	Ref	Expression
Hypotheses	pclem.1	$⊢ A = \{n \in ℕ_{0} \| P^{n} ∥ N\}$
	pclem.2	$⊢ S = sup (A ℝ <)$
Assertion	pcpre1	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to S = 0$

Proof

Step	Hyp	Ref	Expression
1		pclem.1	$⊢ A = \{n \in ℕ_{0} \| P^{n} ∥ N\}$
2		pclem.2	$⊢ S = sup (A ℝ <)$
3		1z	$⊢ 1 \in ℤ$
4		eleq1	$⊢ N = 1 \to (N \in ℤ \leftrightarrow 1 \in ℤ)$
5	3 4	mpbiri	$⊢ N = 1 \to N \in ℤ$
6		ax-1ne0	$⊢ 1 \neq 0$
7		neeq1	$⊢ N = 1 \to (N \neq 0 \leftrightarrow 1 \neq 0)$
8	6 7	mpbiri	$⊢ N = 1 \to N \neq 0$
9	5 8	jca	$⊢ N = 1 \to (N \in ℤ \land N \neq 0)$
10	1 2	pcprecl	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to (S \in ℕ_{0} \land P^{S} ∥ N)$
11	9 10	sylan2	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to (S \in ℕ_{0} \land P^{S} ∥ N)$
12	11	simprd	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to P^{S} ∥ N$
13		simpr	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to N = 1$
14	12 13	breqtrd	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to P^{S} ∥ 1$
15		eluz2nn	$⊢ P \in ℤ_{\geq 2} \to P \in ℕ$
16	15	adantr	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to P \in ℕ$
17	11	simpld	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to S \in ℕ_{0}$
18	16 17	nnexpcld	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to P^{S} \in ℕ$
19	18	nnzd	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to P^{S} \in ℤ$
20		1nn	$⊢ 1 \in ℕ$
21		dvdsle	$⊢ (P^{S} \in ℤ \land 1 \in ℕ) \to (P^{S} ∥ 1 \to P^{S} \leq 1)$
22	19 20 21	sylancl	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to (P^{S} ∥ 1 \to P^{S} \leq 1)$
23	14 22	mpd	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to P^{S} \leq 1$
24	16	nncnd	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to P \in ℂ$
25	24	exp0d	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to P^{0} = 1$
26	23 25	breqtrrd	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to P^{S} \leq P^{0}$
27	16	nnred	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to P \in ℝ$
28	17	nn0zd	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to S \in ℤ$
29		0zd	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to 0 \in ℤ$
30		eluz2gt1	$⊢ P \in ℤ_{\geq 2} \to 1 < P$
31	30	adantr	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to 1 < P$
32	27 28 29 31	leexp2d	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to (S \leq 0 \leftrightarrow P^{S} \leq P^{0})$
33	26 32	mpbird	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to S \leq 0$
34	10	simpld	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to S \in ℕ_{0}$
35	9 34	sylan2	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to S \in ℕ_{0}$
36		nn0le0eq0	$⊢ S \in ℕ_{0} \to (S \leq 0 \leftrightarrow S = 0)$
37	35 36	syl	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to (S \leq 0 \leftrightarrow S = 0)$
38	33 37	mpbid	$⊢ (P \in ℤ_{\geq 2} \land N = 1) \to S = 0$

Metamath Proof Explorer

Theorem pcpre1

Proof