Description: Lemma for dnibnd . (Contributed by Asger C. Ipsen, 4-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dnibndlem13.1 | |
|
dnibndlem13.2 | |
||
dnibndlem13.3 | |
||
dnibndlem13.4 | |
||
Assertion | dnibndlem13 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dnibndlem13.1 | |
|
2 | dnibndlem13.2 | |
|
3 | dnibndlem13.3 | |
|
4 | dnibndlem13.4 | |
|
5 | 2 | ad2antrr | |
6 | 3 | ad2antrr | |
7 | simpr | |
|
8 | 1 5 6 7 | dnibndlem12 | |
9 | 2 | ad2antrr | |
10 | 3 | ad2antrr | |
11 | simpr | |
|
12 | 11 | eqcomd | |
13 | 1 9 10 12 | dnibndlem9 | |
14 | simpr | |
|
15 | halfre | |
|
16 | 15 | a1i | |
17 | 2 16 | readdcld | |
18 | 17 | flcld | |
19 | 3 16 | readdcld | |
20 | 19 | flcld | |
21 | 18 20 | jca | |
22 | 21 | adantr | |
23 | zltp1le | |
|
24 | 22 23 | syl | |
25 | 14 24 | mpbid | |
26 | reflcl | |
|
27 | 17 26 | syl | |
28 | peano2re | |
|
29 | 27 28 | syl | |
30 | 29 | adantr | |
31 | 20 | zred | |
32 | 31 | adantr | |
33 | 30 32 | leloed | |
34 | 25 33 | mpbid | |
35 | 18 | peano2zd | |
36 | 35 20 | jca | |
37 | zltp1le | |
|
38 | 36 37 | syl | |
39 | 27 | recnd | |
40 | 1cnd | |
|
41 | 39 40 40 | addassd | |
42 | 1p1e2 | |
|
43 | 42 | a1i | |
44 | 43 | oveq2d | |
45 | 41 44 | eqtrd | |
46 | 45 | breq1d | |
47 | 38 46 | bitrd | |
48 | 47 | biimpd | |
49 | 48 | adantr | |
50 | 49 | orim1d | |
51 | 34 50 | mpd | |
52 | 8 13 51 | mpjaodan | |
53 | 2 | adantr | |
54 | 3 | adantr | |
55 | simpr | |
|
56 | 55 | eqcomd | |
57 | 1 53 54 56 | dnibndlem2 | |
58 | 27 31 | leloed | |
59 | 4 58 | mpbid | |
60 | 52 57 59 | mpjaodan | |