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 +