This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mulridd ⊢ ( ( 𝑁 ∈ ℕ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 )