Description: Lemma 2 for pthd . (Contributed by Alexander van der Vekens, 11-Nov-2017) (Revised by AV, 10-Feb-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pthd.p | |
|
pthd.r | |
||
pthd.s | |
||
Assertion | pthdlem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pthd.p | |
|
2 | pthd.r | |
|
3 | pthd.s | |
|
4 | lencl | |
|
5 | df-ne | |
|
6 | elnnne0 | |
|
7 | 6 | simplbi2 | |
8 | 5 7 | syl5bir | |
9 | 1 4 8 | 3syl | |
10 | eqid | |
|
11 | 10 | orci | |
12 | 1 2 3 | pthdlem2lem | |
13 | 11 12 | mp3an3 | |
14 | eqid | |
|
15 | 14 | olci | |
16 | 1 2 3 | pthdlem2lem | |
17 | 15 16 | mp3an3 | |
18 | wrdffz | |
|
19 | 1 18 | syl | |
20 | 19 | adantr | |
21 | 2 | oveq2i | |
22 | 21 | feq2i | |
23 | 20 22 | sylibr | |
24 | nnm1nn0 | |
|
25 | 2 24 | eqeltrid | |
26 | 25 | adantl | |
27 | fvinim0ffz | |
|
28 | 23 26 27 | syl2anc | |
29 | 13 17 28 | mpbir2and | |
30 | 29 | ex | |
31 | 9 30 | syld | |
32 | oveq1 | |
|
33 | 2 32 | eqtrid | |
34 | 33 | oveq2d | |
35 | 0le2 | |
|
36 | 1p1e2 | |
|
37 | 35 36 | breqtrri | |
38 | 0re | |
|
39 | 1re | |
|
40 | 38 39 39 | lesubadd2i | |
41 | 37 40 | mpbir | |
42 | 1z | |
|
43 | 0z | |
|
44 | peano2zm | |
|
45 | 43 44 | ax-mp | |
46 | fzon | |
|
47 | 42 45 46 | mp2an | |
48 | 41 47 | mpbi | |
49 | 34 48 | eqtrdi | |
50 | 49 | imaeq2d | |
51 | ima0 | |
|
52 | 50 51 | eqtrdi | |
53 | 52 | ineq2d | |
54 | in0 | |
|
55 | 53 54 | eqtrdi | |
56 | 31 55 | pm2.61d2 | |