Theorem knoppndvlem12

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

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

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem12.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
2		knoppndvlem12.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3		knoppndvlem12.1	⊢ ( 𝜑 → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
4		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
5		2re	⊢ 2 ∈ ℝ
6	5	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
7		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
8	2 7	syl	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
9	6 8	remulcld	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
10	1	knoppndvlem3	⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ( abs ‘ 𝐶 ) < 1 ) )
11	10	simpld	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
12	11	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
13	12	abscld	⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℝ )
14	9 13	remulcld	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ∈ ℝ )
15		1lt2	⊢ 1 < 2
16	15	a1i	⊢ ( 𝜑 → 1 < 2 )
17		2t1e2	⊢ ( 2 · 1 ) = 2
18	17	eqcomi	⊢ 2 = ( 2 · 1 )
19	18	a1i	⊢ ( 𝜑 → 2 = ( 2 · 1 ) )
20	8 13	remulcld	⊢ ( 𝜑 → ( 𝑁 · ( abs ‘ 𝐶 ) ) ∈ ℝ )
21		2rp	⊢ 2 ∈ ℝ+
22	21	a1i	⊢ ( 𝜑 → 2 ∈ ℝ+ )
23	4 20 22 3	ltmul2dd	⊢ ( 𝜑 → ( 2 · 1 ) < ( 2 · ( 𝑁 · ( abs ‘ 𝐶 ) ) ) )
24	19 23	eqbrtrd	⊢ ( 𝜑 → 2 < ( 2 · ( 𝑁 · ( abs ‘ 𝐶 ) ) ) )
25	6	recnd	⊢ ( 𝜑 → 2 ∈ ℂ )
26	8	recnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
27	13	recnd	⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℂ )
28	25 26 27	mulassd	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) = ( 2 · ( 𝑁 · ( abs ‘ 𝐶 ) ) ) )
29	28	eqcomd	⊢ ( 𝜑 → ( 2 · ( 𝑁 · ( abs ‘ 𝐶 ) ) ) = ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) )
30	24 29	breqtrd	⊢ ( 𝜑 → 2 < ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) )
31	4 6 14 16 30	lttrd	⊢ ( 𝜑 → 1 < ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) )
32	4 31	jca	⊢ ( 𝜑 → ( 1 ∈ ℝ ∧ 1 < ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ) )
33		ltne	⊢ ( ( 1 ∈ ℝ ∧ 1 < ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ) → ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ≠ 1 )
34	32 33	syl	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ≠ 1 )
35		1p1e2	⊢ ( 1 + 1 ) = 2
36	35	a1i	⊢ ( 𝜑 → ( 1 + 1 ) = 2 )
37	36 30	eqbrtrd	⊢ ( 𝜑 → ( 1 + 1 ) < ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) )
38	4 4 14	ltaddsubd	⊢ ( 𝜑 → ( ( 1 + 1 ) < ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↔ 1 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) )
39	37 38	mpbid	⊢ ( 𝜑 → 1 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) )
40	34 39	jca	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ≠ 1 ∧ 1 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) )