pcfaclem

		Ref	Expression
	Assertion	pcfaclem	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to ⌊\frac{N}{P^{M}}⌋ = 0$

Proof

Step	Hyp	Ref	Expression
1		nn0ge0	$⊢ N \in ℕ_{0} \to 0 \leq N$
2	1	3ad2ant1	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to 0 \leq N$
3		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
4	3	3ad2ant1	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to N \in ℝ$
5		prmnn	$⊢ P \in ℙ \to P \in ℕ$
6	5	3ad2ant3	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to P \in ℕ$
7		eluznn0	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N}) \to M \in ℕ_{0}$
8	7	3adant3	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to M \in ℕ_{0}$
9	6 8	nnexpcld	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to P^{M} \in ℕ$
10	9	nnred	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to P^{M} \in ℝ$
11	9	nngt0d	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to 0 < P^{M}$
12		ge0div	$⊢ (N \in ℝ \land P^{M} \in ℝ \land 0 < P^{M}) \to (0 \leq N \leftrightarrow 0 \leq \frac{N}{P^{M}})$
13	4 10 11 12	syl3anc	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to (0 \leq N \leftrightarrow 0 \leq \frac{N}{P^{M}})$
14	2 13	mpbid	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to 0 \leq \frac{N}{P^{M}}$
15	8	nn0red	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to M \in ℝ$
16		eluzle	$⊢ M \in ℤ_{\geq N} \to N \leq M$
17	16	3ad2ant2	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to N \leq M$
18		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
19	18	3ad2ant3	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to P \in ℤ_{\geq 2}$
20		bernneq3	$⊢ (P \in ℤ_{\geq 2} \land M \in ℕ_{0}) \to M < P^{M}$
21	19 8 20	syl2anc	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to M < P^{M}$
22	4 15 10 17 21	lelttrd	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to N < P^{M}$
23	9	nncnd	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to P^{M} \in ℂ$
24	23	mulid1d	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to P^{M} \cdot 1 = P^{M}$
25	22 24	breqtrrd	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to N < P^{M} \cdot 1$
26		1red	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to 1 \in ℝ$
27		ltdivmul	$⊢ (N \in ℝ \land 1 \in ℝ \land (P^{M} \in ℝ \land 0 < P^{M})) \to (\frac{N}{P^{M}} < 1 \leftrightarrow N < P^{M} \cdot 1)$
28	4 26 10 11 27	syl112anc	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to (\frac{N}{P^{M}} < 1 \leftrightarrow N < P^{M} \cdot 1)$
29	25 28	mpbird	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to \frac{N}{P^{M}} < 1$
30		0p1e1	$⊢ 0 + 1 = 1$
31	29 30	breqtrrdi	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to \frac{N}{P^{M}} < 0 + 1$
32	4 9	nndivred	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to \frac{N}{P^{M}} \in ℝ$
33		0z	$⊢ 0 \in ℤ$
34		flbi	$⊢ (\frac{N}{P^{M}} \in ℝ \land 0 \in ℤ) \to (⌊\frac{N}{P^{M}}⌋ = 0 \leftrightarrow (0 \leq \frac{N}{P^{M}} \land \frac{N}{P^{M}} < 0 + 1))$
35	32 33 34	sylancl	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to (⌊\frac{N}{P^{M}}⌋ = 0 \leftrightarrow (0 \leq \frac{N}{P^{M}} \land \frac{N}{P^{M}} < 0 + 1))$
36	14 31 35	mpbir2and	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to ⌊\frac{N}{P^{M}}⌋ = 0$

Metamath Proof Explorer

Theorem pcfaclem

Proof