Metamath Proof Explorer


Theorem cnndvlem1

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

Ref Expression
Hypotheses cnndvlem1.t T = x x + 1 2 x
cnndvlem1.f F = y n 0 1 2 n T 2 3 n y
cnndvlem1.w W = w i 0 F w i
Assertion cnndvlem1 W : cn dom W =

Proof

Step Hyp Ref Expression
1 cnndvlem1.t T = x x + 1 2 x
2 cnndvlem1.f F = y n 0 1 2 n T 2 3 n y
3 cnndvlem1.w W = w i 0 F w i
4 3nn 3
5 4 a1i 3
6 neg1rr 1
7 6 rexri 1 *
8 1re 1
9 8 rexri 1 *
10 halfre 1 2
11 10 rexri 1 2 *
12 7 9 11 3pm3.2i 1 * 1 * 1 2 *
13 neg1lt0 1 < 0
14 halfgt0 0 < 1 2
15 13 14 pm3.2i 1 < 0 0 < 1 2
16 0re 0
17 6 16 10 lttri 1 < 0 0 < 1 2 1 < 1 2
18 15 17 ax-mp 1 < 1 2
19 halflt1 1 2 < 1
20 18 19 pm3.2i 1 < 1 2 1 2 < 1
21 12 20 pm3.2i 1 * 1 * 1 2 * 1 < 1 2 1 2 < 1
22 elioo3g 1 2 1 1 1 * 1 * 1 2 * 1 < 1 2 1 2 < 1
23 21 22 mpbir 1 2 1 1
24 23 a1i 1 2 1 1
25 1 2 3 5 24 knoppcn2 W : cn
26 25 mptru W : cn
27 2cn 2
28 27 mulid2i 1 2 = 2
29 2lt3 2 < 3
30 28 29 eqbrtri 1 2 < 3
31 2pos 0 < 2
32 4 nnrei 3
33 2re 2
34 8 32 33 ltmuldivi 0 < 2 1 2 < 3 1 < 3 2
35 31 34 ax-mp 1 2 < 3 1 < 3 2
36 30 35 mpbi 1 < 3 2
37 16 10 14 ltleii 0 1 2
38 10 absidi 0 1 2 1 2 = 1 2
39 37 38 ax-mp 1 2 = 1 2
40 39 oveq2i 3 1 2 = 3 1 2
41 4 nncni 3
42 2ne0 2 0
43 41 27 42 divreci 3 2 = 3 1 2
44 43 eqcomi 3 1 2 = 3 2
45 40 44 eqtri 3 1 2 = 3 2
46 36 45 breqtrri 1 < 3 1 2
47 46 a1i 1 < 3 1 2
48 1 2 3 24 5 47 knoppndv dom W =
49 48 mptru dom W =
50 26 49 pm3.2i W : cn dom W =