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∈−11
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∈−11
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