Metamath Proof Explorer

Theorem knoppndvlem20

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

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

Proof

Step Hyp Ref Expression
1 knoppndvlem20.c ⊢ φ → C ∈ − 1 1
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 ↔ 1 2 ⋅ N ⁢ C − 1 < 1
23 5 22 mpbid ⊢ φ → 1 2 ⋅ N ⁢ C − 1 < 1
24 21 rprecred ⊢ φ → 1 2 ⋅ N ⁢ C − 1 ∈ ℝ
25 24 15 jca ⊢ φ → 1 2 ⋅ N ⁢ C − 1 ∈ ℝ ∧ 1 ∈ ℝ
26 difrp ⊢ 1 2 ⋅ N ⁢ C − 1 ∈ ℝ ∧ 1 ∈ ℝ → 1 2 ⋅ N ⁢ C − 1 < 1 ↔ 1 − 1 2 ⋅ N ⁢ C − 1 ∈ ℝ +
27 25 26 syl ⊢ φ → 1 2 ⋅ N ⁢ C − 1 < 1 ↔ 1 − 1 2 ⋅ N ⁢ C − 1 ∈ ℝ +
28 23 27 mpbid ⊢ φ → 1 − 1 2 ⋅ N ⁢ C − 1 ∈ ℝ +