Metamath Proof Explorer


Theorem pntlemd

Description: Lemma for pnt . Closure for the constants used in the proof. For comparison with Equation 10.6.27 of Shapiro, p. 434, A is C^*, B is c_1, L is λ, D is c_2, and F is c_3. (Contributed by Mario Carneiro, 13-Apr-2016)

Ref Expression
Hypotheses pntlem1.r R = a + ψ a a
pntlem1.a φ A +
pntlem1.b φ B +
pntlem1.l φ L 0 1
pntlem1.d D = A + 1
pntlem1.f F = 1 1 D L 32 B D 2
Assertion pntlemd φ L + D + F +

Proof

Step Hyp Ref Expression
1 pntlem1.r R = a + ψ a a
2 pntlem1.a φ A +
3 pntlem1.b φ B +
4 pntlem1.l φ L 0 1
5 pntlem1.d D = A + 1
6 pntlem1.f F = 1 1 D L 32 B D 2
7 ioossre 0 1
8 7 4 sseldi φ L
9 eliooord L 0 1 0 < L L < 1
10 4 9 syl φ 0 < L L < 1
11 10 simpld φ 0 < L
12 8 11 elrpd φ L +
13 1rp 1 +
14 rpaddcl A + 1 + A + 1 +
15 2 13 14 sylancl φ A + 1 +
16 5 15 eqeltrid φ D +
17 1re 1
18 ltaddrp 1 A + 1 < 1 + A
19 17 2 18 sylancr φ 1 < 1 + A
20 2 rpcnd φ A
21 ax-1cn 1
22 addcom A 1 A + 1 = 1 + A
23 20 21 22 sylancl φ A + 1 = 1 + A
24 5 23 syl5eq φ D = 1 + A
25 19 24 breqtrrd φ 1 < D
26 16 recgt1d φ 1 < D 1 D < 1
27 25 26 mpbid φ 1 D < 1
28 16 rprecred φ 1 D
29 difrp 1 D 1 1 D < 1 1 1 D +
30 28 17 29 sylancl φ 1 D < 1 1 1 D +
31 27 30 mpbid φ 1 1 D +
32 3nn0 3 0
33 2nn 2
34 32 33 decnncl 32
35 nnrp 32 32 +
36 34 35 ax-mp 32 +
37 rpmulcl 32 + B + 32 B +
38 36 3 37 sylancr φ 32 B +
39 12 38 rpdivcld φ L 32 B +
40 2z 2
41 rpexpcl D + 2 D 2 +
42 16 40 41 sylancl φ D 2 +
43 39 42 rpdivcld φ L 32 B D 2 +
44 31 43 rpmulcld φ 1 1 D L 32 B D 2 +
45 6 44 eqeltrid φ F +
46 12 16 45 3jca φ L + D + F +