Theorem knoppndvlem13

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 1-Jul-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

	Ref	Expression
Hypotheses	knoppndvlem13.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
	knoppndvlem13.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	knoppndvlem13.1	⊢ ( 𝜑 → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
Assertion	knoppndvlem13	⊢ ( 𝜑 → 𝐶 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem13.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
2		knoppndvlem13.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3		knoppndvlem13.1	⊢ ( 𝜑 → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
4	3	adantr	⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
5		0lt1	⊢ 0 < 1
6		0re	⊢ 0 ∈ ℝ
7		1re	⊢ 1 ∈ ℝ
8	6 7	ltnsymi	⊢ ( 0 < 1 → ¬ 1 < 0 )
9	5 8	ax-mp	⊢ ¬ 1 < 0
10	9	a1i	⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → ¬ 1 < 0 )
11		id	⊢ ( 𝐶 = 0 → 𝐶 = 0 )
12	11	abs00bd	⊢ ( 𝐶 = 0 → ( abs ‘ 𝐶 ) = 0 )
13	12	oveq2d	⊢ ( 𝐶 = 0 → ( 𝑁 · ( abs ‘ 𝐶 ) ) = ( 𝑁 · 0 ) )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → ( 𝑁 · ( abs ‘ 𝐶 ) ) = ( 𝑁 · 0 ) )
15		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
16	2 15	syl	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → 𝑁 ∈ ℂ )
18	17	mul01d	⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → ( 𝑁 · 0 ) = 0 )
19	14 18	eqtrd	⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → ( 𝑁 · ( abs ‘ 𝐶 ) ) = 0 )
20	19	eqcomd	⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → 0 = ( 𝑁 · ( abs ‘ 𝐶 ) ) )
21	20	breq2d	⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → ( 1 < 0 ↔ 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) ) )
22	10 21	mtbid	⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → ¬ 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
23	4 22	pm2.65da	⊢ ( 𝜑 → ¬ 𝐶 = 0 )
24	23	neqned	⊢ ( 𝜑 → 𝐶 ≠ 0 )