Metamath Proof Explorer

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 ) ) )