pclem

Description: - Lemma for the prime power pre-function's properties. (Contributed by Mario Carneiro, 23-Feb-2014)

		Ref	Expression
	Hypothesis	pclem.1	$⊢ A = \{n \in ℕ_{0} \| P^{n} ∥ N\}$
	Assertion	pclem	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to (A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℤ \forall y \in A y \leq x)$

Proof

Step	Hyp	Ref	Expression
1		pclem.1	$⊢ A = \{n \in ℕ_{0} \| P^{n} ∥ N\}$
2	1	ssrab3	$⊢ A \subseteq ℕ_{0}$
3		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
4	2 3	sstri	$⊢ A \subseteq ℤ$
5	4	a1i	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to A \subseteq ℤ$
6		0nn0	$⊢ 0 \in ℕ_{0}$
7	6	a1i	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to 0 \in ℕ_{0}$
8		eluzelcn	$⊢ P \in ℤ_{\geq 2} \to P \in ℂ$
9	8	adantr	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to P \in ℂ$
10	9	exp0d	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to P^{0} = 1$
11		1dvds	$⊢ N \in ℤ \to 1 ∥ N$
12	11	ad2antrl	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to 1 ∥ N$
13	10 12	eqbrtrd	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to P^{0} ∥ N$
14		oveq2	$⊢ n = 0 \to P^{n} = P^{0}$
15	14	breq1d	$⊢ n = 0 \to (P^{n} ∥ N \leftrightarrow P^{0} ∥ N)$
16	15 1	elrab2	$⊢ 0 \in A \leftrightarrow (0 \in ℕ_{0} \land P^{0} ∥ N)$
17	7 13 16	sylanbrc	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to 0 \in A$
18	17	ne0d	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to A \neq \emptyset$
19		nnssz	$⊢ ℕ \subseteq ℤ$
20		zcn	$⊢ N \in ℤ \to N \in ℂ$
21	20	abscld	$⊢ N \in ℤ \to \|N\| \in ℝ$
22	21	ad2antrl	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to \|N\| \in ℝ$
23		eluzelre	$⊢ P \in ℤ_{\geq 2} \to P \in ℝ$
24	23	adantr	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to P \in ℝ$
25		eluz2gt1	$⊢ P \in ℤ_{\geq 2} \to 1 < P$
26	25	adantr	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to 1 < P$
27		expnbnd	$⊢ (\|N\| \in ℝ \land P \in ℝ \land 1 < P) \to \exists x \in ℕ \|N\| < P^{x}$
28	22 24 26 27	syl3anc	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to \exists x \in ℕ \|N\| < P^{x}$
29		simprr	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to y \in A$
30		oveq2	$⊢ n = y \to P^{n} = P^{y}$
31	30	breq1d	$⊢ n = y \to (P^{n} ∥ N \leftrightarrow P^{y} ∥ N)$
32	31 1	elrab2	$⊢ y \in A \leftrightarrow (y \in ℕ_{0} \land P^{y} ∥ N)$
33	29 32	sylib	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to (y \in ℕ_{0} \land P^{y} ∥ N)$
34	33	simprd	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to P^{y} ∥ N$
35		eluz2nn	$⊢ P \in ℤ_{\geq 2} \to P \in ℕ$
36	35	ad2antrr	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to P \in ℕ$
37	33	simpld	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to y \in ℕ_{0}$
38	36 37	nnexpcld	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to P^{y} \in ℕ$
39	38	nnzd	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to P^{y} \in ℤ$
40		simplrl	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to N \in ℤ$
41		simplrr	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to N \neq 0$
42		dvdsleabs	$⊢ (P^{y} \in ℤ \land N \in ℤ \land N \neq 0) \to (P^{y} ∥ N \to P^{y} \leq \|N\|)$
43	39 40 41 42	syl3anc	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to (P^{y} ∥ N \to P^{y} \leq \|N\|)$
44	34 43	mpd	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to P^{y} \leq \|N\|$
45	38	nnred	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to P^{y} \in ℝ$
46	22	adantr	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to \|N\| \in ℝ$
47	23	ad2antrr	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to P \in ℝ$
48		nnnn0	$⊢ x \in ℕ \to x \in ℕ_{0}$
49	48	ad2antrl	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to x \in ℕ_{0}$
50	47 49	reexpcld	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to P^{x} \in ℝ$
51		lelttr	$⊢ (P^{y} \in ℝ \land \|N\| \in ℝ \land P^{x} \in ℝ) \to ((P^{y} \leq \|N\| \land \|N\| < P^{x}) \to P^{y} < P^{x})$
52	45 46 50 51	syl3anc	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to ((P^{y} \leq \|N\| \land \|N\| < P^{x}) \to P^{y} < P^{x})$
53	44 52	mpand	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to (\|N\| < P^{x} \to P^{y} < P^{x})$
54	37	nn0zd	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to y \in ℤ$
55		nnz	$⊢ x \in ℕ \to x \in ℤ$
56	55	ad2antrl	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to x \in ℤ$
57	25	ad2antrr	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to 1 < P$
58	47 54 56 57	ltexp2d	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to (y < x \leftrightarrow P^{y} < P^{x})$
59	53 58	sylibrd	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to (\|N\| < P^{x} \to y < x)$
60	37	nn0red	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to y \in ℝ$
61		nnre	$⊢ x \in ℕ \to x \in ℝ$
62	61	ad2antrl	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to x \in ℝ$
63		ltle	$⊢ (y \in ℝ \land x \in ℝ) \to (y < x \to y \leq x)$
64	60 62 63	syl2anc	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to (y < x \to y \leq x)$
65	59 64	syld	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land (x \in ℕ \land y \in A)) \to (\|N\| < P^{x} \to y \leq x)$
66	65	anassrs	$⊢ (((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land x \in ℕ) \land y \in A) \to (\|N\| < P^{x} \to y \leq x)$
67	66	ralrimdva	$⊢ ((P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \land x \in ℕ) \to (\|N\| < P^{x} \to \forall y \in A y \leq x)$
68	67	reximdva	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to (\exists x \in ℕ \|N\| < P^{x} \to \exists x \in ℕ \forall y \in A y \leq x)$
69	28 68	mpd	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to \exists x \in ℕ \forall y \in A y \leq x$
70		ssrexv	$⊢ ℕ \subseteq ℤ \to (\exists x \in ℕ \forall y \in A y \leq x \to \exists x \in ℤ \forall y \in A y \leq x)$
71	19 69 70	mpsyl	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to \exists x \in ℤ \forall y \in A y \leq x$
72	5 18 71	3jca	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to (A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℤ \forall y \in A y \leq x)$

Metamath Proof Explorer

Theorem pclem

Proof