Theorem pcfaclem

Description: Lemma for pcfac . (Contributed by Mario Carneiro, 20-May-2014)

	Ref	Expression
Assertion	pcfaclem	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑀 ) ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		nn0ge0	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
2	1	3ad2ant1	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 0 ≤ 𝑁 )
3		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
4	3	3ad2ant1	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 𝑁 ∈ ℝ )
5		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
6	5	3ad2ant3	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 𝑃 ∈ ℕ )
7		eluznn0	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ℕ0 )
8	7	3adant3	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 𝑀 ∈ ℕ0 )
9	6 8	nnexpcld	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑃 ↑ 𝑀 ) ∈ ℕ )
10	9	nnred	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑃 ↑ 𝑀 ) ∈ ℝ )
11	9	nngt0d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 0 < ( 𝑃 ↑ 𝑀 ) )
12		ge0div	⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝑃 ↑ 𝑀 ) ∈ ℝ ∧ 0 < ( 𝑃 ↑ 𝑀 ) ) → ( 0 ≤ 𝑁 ↔ 0 ≤ ( 𝑁 / ( 𝑃 ↑ 𝑀 ) ) ) )
13	4 10 11 12	syl3anc	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 0 ≤ 𝑁 ↔ 0 ≤ ( 𝑁 / ( 𝑃 ↑ 𝑀 ) ) ) )
14	2 13	mpbid	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 0 ≤ ( 𝑁 / ( 𝑃 ↑ 𝑀 ) ) )
15	8	nn0red	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 𝑀 ∈ ℝ )
16		eluzle	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ≤ 𝑀 )
17	16	3ad2ant2	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 𝑁 ≤ 𝑀 )
18		prmuz2	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
19	18	3ad2ant3	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
20		bernneq3	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ0 ) → 𝑀 < ( 𝑃 ↑ 𝑀 ) )
21	19 8 20	syl2anc	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 𝑀 < ( 𝑃 ↑ 𝑀 ) )
22	4 15 10 17 21	lelttrd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 𝑁 < ( 𝑃 ↑ 𝑀 ) )
23	9	nncnd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑃 ↑ 𝑀 ) ∈ ℂ )
24	23	mulid1d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( ( 𝑃 ↑ 𝑀 ) · 1 ) = ( 𝑃 ↑ 𝑀 ) )
25	22 24	breqtrrd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 𝑁 < ( ( 𝑃 ↑ 𝑀 ) · 1 ) )
26		1red	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 1 ∈ ℝ )
27		ltdivmul	⊢ ( ( 𝑁 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( 𝑃 ↑ 𝑀 ) ∈ ℝ ∧ 0 < ( 𝑃 ↑ 𝑀 ) ) ) → ( ( 𝑁 / ( 𝑃 ↑ 𝑀 ) ) < 1 ↔ 𝑁 < ( ( 𝑃 ↑ 𝑀 ) · 1 ) ) )
28	4 26 10 11 27	syl112anc	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( ( 𝑁 / ( 𝑃 ↑ 𝑀 ) ) < 1 ↔ 𝑁 < ( ( 𝑃 ↑ 𝑀 ) · 1 ) ) )
29	25 28	mpbird	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑁 / ( 𝑃 ↑ 𝑀 ) ) < 1 )
30		0p1e1	⊢ ( 0 + 1 ) = 1
31	29 30	breqtrrdi	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑁 / ( 𝑃 ↑ 𝑀 ) ) < ( 0 + 1 ) )
32	4 9	nndivred	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑁 / ( 𝑃 ↑ 𝑀 ) ) ∈ ℝ )
33		0z	⊢ 0 ∈ ℤ
34		flbi	⊢ ( ( ( 𝑁 / ( 𝑃 ↑ 𝑀 ) ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑀 ) ) ) = 0 ↔ ( 0 ≤ ( 𝑁 / ( 𝑃 ↑ 𝑀 ) ) ∧ ( 𝑁 / ( 𝑃 ↑ 𝑀 ) ) < ( 0 + 1 ) ) ) )
35	32 33 34	sylancl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑀 ) ) ) = 0 ↔ ( 0 ≤ ( 𝑁 / ( 𝑃 ↑ 𝑀 ) ) ∧ ( 𝑁 / ( 𝑃 ↑ 𝑀 ) ) < ( 0 + 1 ) ) ) )
36	14 31 35	mpbir2and	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑀 ) ) ) = 0 )