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	$$⊢\phi \to C\in \left(-1,1\right)$$
	knoppndvlem13.n	$$⊢\phi \to N\in \mathbb{N}$$
	knoppndvlem13.1	$$⊢\phi \to 1<N\left|C\right|$$
Assertion	knoppndvlem13	$$⊢\phi \to C\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem13.c	$$⊢\phi \to C\in \left(-1,1\right)$$
2		knoppndvlem13.n	$$⊢\phi \to N\in \mathbb{N}$$
3		knoppndvlem13.1	$$⊢\phi \to 1<N\left|C\right|$$
4	3	adantr	$$⊢\left(\phi \wedge C=0\right)\to 1<N\left|C\right|$$
5		0lt1	$$⊢0<1$$
6		0re	$$⊢0\in ℝ$$
7		1re	$$⊢1\in ℝ$$
8	6 7	ltnsymi	$$⊢0<1\to \neg 1<0$$
9	5 8	ax-mp	$$⊢\neg 1<0$$
10	9	a1i	$$⊢\left(\phi \wedge C=0\right)\to \neg 1<0$$
11		id	$$⊢C=0\to C=0$$
12	11	abs00bd	$$⊢C=0\to \left|C\right|=0$$
13	12	oveq2d	$$⊢C=0\to N\left|C\right|=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 0$$
14	13	adantl	$$⊢\left(\phi \wedge C=0\right)\to N\left|C\right|=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 0$$
15		nncn	$$⊢N\in \mathbb{N}\to N\in ℂ$$
16	2 15	syl	$$⊢\phi \to N\in ℂ$$
17	16	adantr	$$⊢\left(\phi \wedge C=0\right)\to N\in ℂ$$
18	17	mul01d	$$⊢\left(\phi \wedge C=0\right)\to \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 0=0$$
19	14 18	eqtrd	$$⊢\left(\phi \wedge C=0\right)\to N\left|C\right|=0$$
20	19	eqcomd	$$⊢\left(\phi \wedge C=0\right)\to 0=N\left|C\right|$$
21	20	breq2d	$$⊢\left(\phi \wedge C=0\right)\to \left(1<0\leftrightarrow 1<N\left|C\right|\right)$$
22	10 21	mtbid	$$⊢\left(\phi \wedge C=0\right)\to \neg 1<N\left|C\right|$$
23	4 22	pm2.65da	$$⊢\phi \to \neg C=0$$
24	23	neqned	$$⊢\phi \to C\ne 0$$