Metamath Proof Explorer


Theorem knoppndvlem21

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 18-Aug-2021)

Ref Expression
Hypotheses knoppndvlem21.t T = x x + 1 2 x
knoppndvlem21.f F = y n 0 C n T 2 N n y
knoppndvlem21.w W = w i 0 F w i
knoppndvlem21.g G = 1 1 2 N C 1
knoppndvlem21.c φ C 1 1
knoppndvlem21.d φ D +
knoppndvlem21.e φ E +
knoppndvlem21.h φ H
knoppndvlem21.j φ J 0
knoppndvlem21.n φ N
knoppndvlem21.1 φ 1 < N C
knoppndvlem21.2 φ 2 N J 2 < D
knoppndvlem21.3 φ E 2 N C J G
Assertion knoppndvlem21 φ a b a H H b b a < D a b E W b W a b a

Proof

Step Hyp Ref Expression
1 knoppndvlem21.t T = x x + 1 2 x
2 knoppndvlem21.f F = y n 0 C n T 2 N n y
3 knoppndvlem21.w W = w i 0 F w i
4 knoppndvlem21.g G = 1 1 2 N C 1
5 knoppndvlem21.c φ C 1 1
6 knoppndvlem21.d φ D +
7 knoppndvlem21.e φ E +
8 knoppndvlem21.h φ H
9 knoppndvlem21.j φ J 0
10 knoppndvlem21.n φ N
11 knoppndvlem21.1 φ 1 < N C
12 knoppndvlem21.2 φ 2 N J 2 < D
13 knoppndvlem21.3 φ E 2 N C J G
14 eqid 2 N J 2 m = 2 N J 2 m
15 eqid 2 N J 2 m + 1 = 2 N J 2 m + 1
16 14 15 9 8 10 knoppndvlem19 φ m 2 N J 2 m H H 2 N J 2 m + 1
17 2re 2
18 17 a1i φ 2
19 10 nnred φ N
20 18 19 remulcld φ 2 N
21 2pos 0 < 2
22 21 a1i φ 0 < 2
23 10 nngt0d φ 0 < N
24 18 19 22 23 mulgt0d φ 0 < 2 N
25 24 gt0ne0d φ 2 N 0
26 9 nn0zd φ J
27 26 znegcld φ J
28 20 25 27 reexpclzd φ 2 N J
29 28 rehalfcld φ 2 N J 2
30 29 adantr φ m 2 N J 2
31 simpr φ m m
32 31 zred φ m m
33 30 32 remulcld φ m 2 N J 2 m
34 33 adantrr φ m 2 N J 2 m H H 2 N J 2 m + 1 2 N J 2 m
35 peano2re m m + 1
36 32 35 syl φ m m + 1
37 30 36 jca φ m 2 N J 2 m + 1
38 remulcl 2 N J 2 m + 1 2 N J 2 m + 1
39 37 38 syl φ m 2 N J 2 m + 1
40 39 adantrr φ m 2 N J 2 m H H 2 N J 2 m + 1 2 N J 2 m + 1
41 simprr φ m 2 N J 2 m H H 2 N J 2 m + 1 2 N J 2 m H H 2 N J 2 m + 1
42 9 adantr φ m J 0
43 10 adantr φ m N
44 14 15 42 31 43 knoppndvlem16 φ m 2 N J 2 m + 1 2 N J 2 m = 2 N J 2
45 12 adantr φ m 2 N J 2 < D
46 44 45 eqbrtrd φ m 2 N J 2 m + 1 2 N J 2 m < D
47 20 27 24 3jca φ 2 N J 0 < 2 N
48 expgt0 2 N J 0 < 2 N 0 < 2 N J
49 47 48 syl φ 0 < 2 N J
50 28 18 49 22 divgt0d φ 0 < 2 N J 2
51 50 adantr φ m 0 < 2 N J 2
52 44 eqcomd φ m 2 N J 2 = 2 N J 2 m + 1 2 N J 2 m
53 51 52 breqtrd φ m 0 < 2 N J 2 m + 1 2 N J 2 m
54 33 39 posdifd φ m 2 N J 2 m < 2 N J 2 m + 1 0 < 2 N J 2 m + 1 2 N J 2 m
55 53 54 mpbird φ m 2 N J 2 m < 2 N J 2 m + 1
56 33 55 ltned φ m 2 N J 2 m 2 N J 2 m + 1
57 46 56 jca φ m 2 N J 2 m + 1 2 N J 2 m < D 2 N J 2 m 2 N J 2 m + 1
58 57 adantrr φ m 2 N J 2 m H H 2 N J 2 m + 1 2 N J 2 m + 1 2 N J 2 m < D 2 N J 2 m 2 N J 2 m + 1
59 7 rpred φ E
60 59 adantr φ m E
61 5 knoppndvlem3 φ C C < 1
62 61 simpld φ C
63 62 recnd φ C
64 63 abscld φ C
65 20 64 remulcld φ 2 N C
66 65 9 reexpcld φ 2 N C J
67 4 a1i φ G = 1 1 2 N C 1
68 5 10 11 knoppndvlem20 φ 1 1 2 N C 1 +
69 68 rpred φ 1 1 2 N C 1
70 67 69 eqeltrd φ G
71 66 70 remulcld φ 2 N C J G
72 71 adantr φ m 2 N C J G
73 62 adantr φ m C
74 61 simprd φ C < 1
75 74 adantr φ m C < 1
76 1 2 3 39 43 73 75 knoppcld φ m W 2 N J 2 m + 1
77 1 2 3 33 43 73 75 knoppcld φ m W 2 N J 2 m
78 76 77 subcld φ m W 2 N J 2 m + 1 W 2 N J 2 m
79 78 abscld φ m W 2 N J 2 m + 1 W 2 N J 2 m
80 44 30 eqeltrd φ m 2 N J 2 m + 1 2 N J 2 m
81 53 gt0ne0d φ m 2 N J 2 m + 1 2 N J 2 m 0
82 79 80 81 redivcld φ m W 2 N J 2 m + 1 W 2 N J 2 m 2 N J 2 m + 1 2 N J 2 m
83 13 adantr φ m E 2 N C J G
84 4 oveq2i 2 N C J G = 2 N C J 1 1 2 N C 1
85 84 a1i φ m 2 N C J G = 2 N C J 1 1 2 N C 1
86 5 adantr φ m C 1 1
87 11 adantr φ m 1 < N C
88 1 2 3 14 15 86 42 31 43 87 knoppndvlem17 φ m 2 N C J 1 1 2 N C 1 W 2 N J 2 m + 1 W 2 N J 2 m 2 N J 2 m + 1 2 N J 2 m
89 85 88 eqbrtrd φ m 2 N C J G W 2 N J 2 m + 1 W 2 N J 2 m 2 N J 2 m + 1 2 N J 2 m
90 60 72 82 83 89 letrd φ m E W 2 N J 2 m + 1 W 2 N J 2 m 2 N J 2 m + 1 2 N J 2 m
91 90 adantrr φ m 2 N J 2 m H H 2 N J 2 m + 1 E W 2 N J 2 m + 1 W 2 N J 2 m 2 N J 2 m + 1 2 N J 2 m
92 41 58 91 3jca φ m 2 N J 2 m H H 2 N J 2 m + 1 2 N J 2 m H H 2 N J 2 m + 1 2 N J 2 m + 1 2 N J 2 m < D 2 N J 2 m 2 N J 2 m + 1 E W 2 N J 2 m + 1 W 2 N J 2 m 2 N J 2 m + 1 2 N J 2 m
93 34 40 92 3jca φ m 2 N J 2 m H H 2 N J 2 m + 1 2 N J 2 m 2 N J 2 m + 1 2 N J 2 m H H 2 N J 2 m + 1 2 N J 2 m + 1 2 N J 2 m < D 2 N J 2 m 2 N J 2 m + 1 E W 2 N J 2 m + 1 W 2 N J 2 m 2 N J 2 m + 1 2 N J 2 m
94 breq1 a = 2 N J 2 m a H 2 N J 2 m H
95 94 anbi1d a = 2 N J 2 m a H H b 2 N J 2 m H H b
96 oveq2 a = 2 N J 2 m b a = b 2 N J 2 m
97 96 breq1d a = 2 N J 2 m b a < D b 2 N J 2 m < D
98 neeq1 a = 2 N J 2 m a b 2 N J 2 m b
99 97 98 anbi12d a = 2 N J 2 m b a < D a b b 2 N J 2 m < D 2 N J 2 m b
100 fveq2 a = 2 N J 2 m W a = W 2 N J 2 m
101 100 oveq2d a = 2 N J 2 m W b W a = W b W 2 N J 2 m
102 101 fveq2d a = 2 N J 2 m W b W a = W b W 2 N J 2 m
103 102 96 oveq12d a = 2 N J 2 m W b W a b a = W b W 2 N J 2 m b 2 N J 2 m
104 103 breq2d a = 2 N J 2 m E W b W a b a E W b W 2 N J 2 m b 2 N J 2 m
105 95 99 104 3anbi123d a = 2 N J 2 m a H H b b a < D a b E W b W a b a 2 N J 2 m H H b b 2 N J 2 m < D 2 N J 2 m b E W b W 2 N J 2 m b 2 N J 2 m
106 breq2 b = 2 N J 2 m + 1 H b H 2 N J 2 m + 1
107 106 anbi2d b = 2 N J 2 m + 1 2 N J 2 m H H b 2 N J 2 m H H 2 N J 2 m + 1
108 oveq1 b = 2 N J 2 m + 1 b 2 N J 2 m = 2 N J 2 m + 1 2 N J 2 m
109 108 breq1d b = 2 N J 2 m + 1 b 2 N J 2 m < D 2 N J 2 m + 1 2 N J 2 m < D
110 neeq2 b = 2 N J 2 m + 1 2 N J 2 m b 2 N J 2 m 2 N J 2 m + 1
111 109 110 anbi12d b = 2 N J 2 m + 1 b 2 N J 2 m < D 2 N J 2 m b 2 N J 2 m + 1 2 N J 2 m < D 2 N J 2 m 2 N J 2 m + 1
112 fveq2 b = 2 N J 2 m + 1 W b = W 2 N J 2 m + 1
113 112 fvoveq1d b = 2 N J 2 m + 1 W b W 2 N J 2 m = W 2 N J 2 m + 1 W 2 N J 2 m
114 113 108 oveq12d b = 2 N J 2 m + 1 W b W 2 N J 2 m b 2 N J 2 m = W 2 N J 2 m + 1 W 2 N J 2 m 2 N J 2 m + 1 2 N J 2 m
115 114 breq2d b = 2 N J 2 m + 1 E W b W 2 N J 2 m b 2 N J 2 m E W 2 N J 2 m + 1 W 2 N J 2 m 2 N J 2 m + 1 2 N J 2 m
116 107 111 115 3anbi123d b = 2 N J 2 m + 1 2 N J 2 m H H b b 2 N J 2 m < D 2 N J 2 m b E W b W 2 N J 2 m b 2 N J 2 m 2 N J 2 m H H 2 N J 2 m + 1 2 N J 2 m + 1 2 N J 2 m < D 2 N J 2 m 2 N J 2 m + 1 E W 2 N J 2 m + 1 W 2 N J 2 m 2 N J 2 m + 1 2 N J 2 m
117 105 116 rspc2ev 2 N J 2 m 2 N J 2 m + 1 2 N J 2 m H H 2 N J 2 m + 1 2 N J 2 m + 1 2 N J 2 m < D 2 N J 2 m 2 N J 2 m + 1 E W 2 N J 2 m + 1 W 2 N J 2 m 2 N J 2 m + 1 2 N J 2 m a b a H H b b a < D a b E W b W a b a
118 93 117 syl φ m 2 N J 2 m H H 2 N J 2 m + 1 a b a H H b b a < D a b E W b W a b a
119 16 118 rexlimddv φ a b a H H b b a < D a b E W b W a b a