Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 17-Aug-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | knoppndvlem19.a | |
|
knoppndvlem19.b | |
||
knoppndvlem19.j | |
||
knoppndvlem19.h | |
||
knoppndvlem19.n | |
||
Assertion | knoppndvlem19 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | knoppndvlem19.a | |
|
2 | knoppndvlem19.b | |
|
3 | knoppndvlem19.j | |
|
4 | knoppndvlem19.h | |
|
5 | knoppndvlem19.n | |
|
6 | 2re | |
|
7 | 6 | a1i | |
8 | 5 | nnred | |
9 | 7 8 | remulcld | |
10 | 2pos | |
|
11 | 10 | a1i | |
12 | 5 | nngt0d | |
13 | 7 8 11 12 | mulgt0d | |
14 | 13 | gt0ne0d | |
15 | 3 | nn0zd | |
16 | 15 | znegcld | |
17 | 9 14 16 | reexpclzd | |
18 | 7 | recnd | |
19 | 8 | recnd | |
20 | 18 19 14 | mulne0bad | |
21 | 17 7 20 | redivcld | |
22 | 9 16 13 | 3jca | |
23 | expgt0 | |
|
24 | 22 23 | syl | |
25 | 17 7 24 11 | divgt0d | |
26 | 25 | gt0ne0d | |
27 | 4 21 26 | redivcld | |
28 | 27 | flcld | |
29 | 1 | a1i | |
30 | id | |
|
31 | 30 | oveq2d | |
32 | 29 31 | eqtrd | |
33 | 32 | breq1d | |
34 | 2 | a1i | |
35 | 30 | oveq1d | |
36 | 35 | oveq2d | |
37 | 34 36 | eqtrd | |
38 | 37 | breq2d | |
39 | 33 38 | anbi12d | |
40 | 39 | adantl | |
41 | 28 | zred | |
42 | 0red | |
|
43 | 42 21 25 | ltled | |
44 | flle | |
|
45 | 27 44 | syl | |
46 | 41 27 21 43 45 | lemul2ad | |
47 | 4 | recnd | |
48 | 21 | recnd | |
49 | 47 48 26 | divcan2d | |
50 | 46 49 | breqtrd | |
51 | 49 | eqcomd | |
52 | peano2re | |
|
53 | 41 52 | syl | |
54 | fllep1 | |
|
55 | 27 54 | syl | |
56 | 27 53 21 43 55 | lemul2ad | |
57 | 51 56 | eqbrtrd | |
58 | 50 57 | jca | |
59 | 28 40 58 | rspcedvd | |