Theorem pczndvds2

Description: The remainder after dividing out all factors of P is not divisible by P . (Contributed by Mario Carneiro, 9-Sep-2014)

	Ref	Expression
Assertion	pczndvds2	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		prmuz2	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
2		eqid	⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 }
3		eqid	⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } , ℝ , < )
4	2 3	pcprendvds2	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } , ℝ , < ) ) ) )
5	1 4	sylan	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } , ℝ , < ) ) ) )
6	3	pczpre	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 pCnt 𝑁 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } , ℝ , < ) )
7	6	oveq2d	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) = ( 𝑃 ↑ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } , ℝ , < ) ) )
8	7	oveq2d	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) = ( 𝑁 / ( 𝑃 ↑ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } , ℝ , < ) ) ) )
9	8	breq2d	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ↔ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } , ℝ , < ) ) ) ) )
10	5 9	mtbird	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )