Metamath Proof Explorer

Theorem knoppndvlem20

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 18-Aug-2021)

Ref Expression
Hypotheses knoppndvlem20.c ⊢φ→C∈−11
knoppndvlem20.n ⊢φ→N∈ℕ
knoppndvlem20.1 ⊢φ→1<N⁢C
Assertion knoppndvlem20 ⊢φ→1−12⋅ N⁢C−1∈ℝ+

Proof

Step Hyp Ref Expression
1 knoppndvlem20.c ⊢φ→C∈−11
2 knoppndvlem20.n ⊢φ→N∈ℕ
3 knoppndvlem20.1 ⊢φ→1<N⁢C
4 1 2 3 knoppndvlem12 ⊢φ→2⋅ N⁢C≠1∧1<2⋅ N⁢C−1
5 4 simprd ⊢φ→1<2⋅ N⁢C−1
6 2re ⊢2∈ℝ
7 6 a1i ⊢φ→2∈ℝ
8 2 nnred ⊢φ→N∈ℝ
9 7 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 1red ⊢φ→1∈ℝ
16 14 15 resubcld ⊢φ→2⋅ N⁢C−1∈ℝ
17 0red ⊢φ→0∈ℝ
18 0lt1 ⊢0<1
19 18 a1i ⊢φ→0<1
20 17 15 16 19 5 lttrd ⊢φ→0<2⋅ N⁢C−1
21 16 20 elrpd ⊢φ→2⋅ N⁢C−1∈ℝ+
22 21 recgt1d ⊢φ→1<2⋅ N⁢C−1↔12⋅ N⁢C−1<1
23 5 22 mpbid ⊢φ→12⋅ N⁢C−1<1
24 21 rprecred ⊢φ→12⋅ N⁢C−1∈ℝ
25 24 15 jca ⊢φ→12⋅ N⁢C−1∈ℝ∧1∈ℝ
26 difrp ⊢12⋅ N⁢C−1∈ℝ∧1∈ℝ→12⋅ N⁢C−1<1↔1−12⋅ N⁢C−1∈ℝ+
27 25 26 syl ⊢φ→12⋅ N⁢C−1<1↔1−12⋅ N⁢C−1∈ℝ+
28 23 27 mpbid ⊢φ→1−12⋅ N⁢C−1∈ℝ+