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 ⊢ φ → C ∈ − 1 1
knoppndvlem12.n ⊢ φ → N ∈ ℕ
knoppndvlem12.1 ⊢ φ → 1 < N ⁢ C
Assertion knoppndvlem12 ⊢ φ → 2 ⋅ N ⁢ C ≠ 1 ∧ 1 < 2 ⋅ N ⁢ C − 1

Proof

Step Hyp Ref Expression
1 knoppndvlem12.c ⊢ φ → C ∈ − 1 1
2 knoppndvlem12.n ⊢ φ → N ∈ ℕ
3 knoppndvlem12.1 ⊢ φ → 1 < N ⁢ C
4 1red ⊢ φ → 1 ∈ ℝ
5 2re ⊢ 2 ∈ ℝ
6 5 a1i ⊢ φ → 2 ∈ ℝ
7 nnre ⊢ N ∈ ℕ → N ∈ ℝ
8 2 7 syl ⊢ φ → N ∈ ℝ
9 6 8 remulcld ⊢ φ → 2 ⋅ N ∈ ℝ
10 1 knoppndvlem3 ⊢ φ → C ∈ ℝ ∧ C < 1
11 10 simpld ⊢ φ → C ∈ ℝ
12 11 recnd ⊢ φ → C ∈ ℂ
13 12 abscld ⊢ φ → C ∈ ℝ
14 9 13 remulcld ⊢ φ → 2 ⋅ N ⁢ C ∈ ℝ
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 ⊢ φ → N ⁢ C ∈ ℝ
21 2rp ⊢ 2 ∈ ℝ +
22 21 a1i ⊢ φ → 2 ∈ ℝ +
23 4 20 22 3 ltmul2dd ⊢ φ → 2 ⋅ 1 < 2 ⁢ N ⁢ C
24 19 23 eqbrtrd ⊢ φ → 2 < 2 ⁢ N ⁢ C
25 6 recnd ⊢ φ → 2 ∈ ℂ
26 8 recnd ⊢ φ → N ∈ ℂ
27 13 recnd ⊢ φ → C ∈ ℂ
28 25 26 27 mulassd ⊢ φ → 2 ⋅ N ⁢ C = 2 ⁢ N ⁢ C
29 28 eqcomd ⊢ φ → 2 ⁢ N ⁢ C = 2 ⋅ N ⁢ C
30 24 29 breqtrd ⊢ φ → 2 < 2 ⋅ N ⁢ C
31 4 6 14 16 30 lttrd ⊢ φ → 1 < 2 ⋅ N ⁢ C
32 4 31 jca ⊢ φ → 1 ∈ ℝ ∧ 1 < 2 ⋅ N ⁢ C
33 ltne ⊢ 1 ∈ ℝ ∧ 1 < 2 ⋅ N ⁢ C → 2 ⋅ N ⁢ C ≠ 1
34 32 33 syl ⊢ φ → 2 ⋅ N ⁢ C ≠ 1
35 1p1e2 ⊢ 1 + 1 = 2
36 35 a1i ⊢ φ → 1 + 1 = 2
37 36 30 eqbrtrd ⊢ φ → 1 + 1 < 2 ⋅ N ⁢ C
38 4 4 14 ltaddsubd ⊢ φ → 1 + 1 < 2 ⋅ N ⁢ C ↔ 1 < 2 ⋅ N ⁢ C − 1
39 37 38 mpbid ⊢ φ → 1 < 2 ⋅ N ⁢ C − 1
40 34 39 jca ⊢ φ → 2 ⋅ N ⁢ C ≠ 1 ∧ 1 < 2 ⋅ N ⁢ C − 1