knoppndvlem20

	Ref	Expression
Hypotheses	knoppndvlem20.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
	knoppndvlem20.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	knoppndvlem20.1	⊢ ( 𝜑 → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
Assertion	knoppndvlem20	⊢ ( 𝜑 → ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ⁺ )

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem20.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
2		knoppndvlem20.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3		knoppndvlem20.1	⊢ ( 𝜑 → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
4	1 2 3	knoppndvlem12	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ≠ 1 ∧ 1 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) )
5	4	simprd	⊢ ( 𝜑 → 1 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) )
6		2re	⊢ 2 ∈ ℝ
7	6	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
8	2	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
9	7 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		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
16	14 15	resubcld	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ∈ ℝ )
17		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
18		0lt1	⊢ 0 < 1
19	18	a1i	⊢ ( 𝜑 → 0 < 1 )
20	17 15 16 19 5	lttrd	⊢ ( 𝜑 → 0 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) )
21	16 20	elrpd	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ∈ ℝ⁺ )
22	21	recgt1d	⊢ ( 𝜑 → ( 1 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ↔ ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) < 1 ) )
23	5 22	mpbid	⊢ ( 𝜑 → ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) < 1 )
24	21	rprecred	⊢ ( 𝜑 → ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ∈ ℝ )
25	24 15	jca	⊢ ( 𝜑 → ( ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) )
26		difrp	⊢ ( ( ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) < 1 ↔ ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ⁺ ) )
27	25 26	syl	⊢ ( 𝜑 → ( ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) < 1 ↔ ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ⁺ ) )
28	23 27	mpbid	⊢ ( 𝜑 → ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ⁺ )

Metamath Proof Explorer

Theorem knoppndvlem20

Proof