Metamath Proof Explorer


Theorem pntleme

Description: Lemma for pnt . Package up pntlemo in quantifiers. (Contributed by Mario Carneiro, 14-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
pntlem1.u φ U +
pntlem1.u2 φ U A
pntlem1.e E = U D
pntlem1.k K = e B E
pntlem1.y φ Y + 1 Y
pntlem1.x φ X + Y < X
pntlem1.c φ C +
pntlem1.w W = Y + 4 L E 2 + X K 2 4 + e 32 B U E L E 2 U 3 + C
pntleme.U φ z Y +∞ R z z U
pntleme.K φ k K +∞ y X +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E
pntleme.C φ z 1 +∞ R z log z 2 log z i = 1 z Y R z i log i z C
Assertion pntleme φ w + v w +∞ R v v U F U 3

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 pntlem1.u φ U +
8 pntlem1.u2 φ U A
9 pntlem1.e E = U D
10 pntlem1.k K = e B E
11 pntlem1.y φ Y + 1 Y
12 pntlem1.x φ X + Y < X
13 pntlem1.c φ C +
14 pntlem1.w W = Y + 4 L E 2 + X K 2 4 + e 32 B U E L E 2 U 3 + C
15 pntleme.U φ z Y +∞ R z z U
16 pntleme.K φ k K +∞ y X +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E
17 pntleme.C φ z 1 +∞ R z log z 2 log z i = 1 z Y R z i log i z C
18 1 2 3 4 5 6 7 8 9 10 11 12 13 14 pntlema φ W +
19 2 adantr φ v W +∞ A +
20 3 adantr φ v W +∞ B +
21 4 adantr φ v W +∞ L 0 1
22 7 adantr φ v W +∞ U +
23 8 adantr φ v W +∞ U A
24 11 adantr φ v W +∞ Y + 1 Y
25 12 adantr φ v W +∞ X + Y < X
26 13 adantr φ v W +∞ C +
27 simpr φ v W +∞ v W +∞
28 eqid log X log K + 1 = log X log K + 1
29 eqid log v log K 2 = log v log K 2
30 15 adantr φ v W +∞ z Y +∞ R z z U
31 oveq1 k = K k y = K y
32 31 breq2d k = K 1 + L E z < k y 1 + L E z < K y
33 32 anbi2d k = K y < z 1 + L E z < k y y < z 1 + L E z < K y
34 33 anbi1d k = K y < z 1 + L E z < k y u z 1 + L E z R u u E y < z 1 + L E z < K y u z 1 + L E z R u u E
35 34 rexbidv k = K z + y < z 1 + L E z < k y u z 1 + L E z R u u E z + y < z 1 + L E z < K y u z 1 + L E z R u u E
36 35 ralbidv k = K y X +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E y X +∞ z + y < z 1 + L E z < K y u z 1 + L E z R u u E
37 1 2 3 4 5 6 7 8 9 10 pntlemc φ E + K + E 0 1 1 < K U E +
38 37 simp2d φ K +
39 38 rpxrd φ K *
40 pnfxr +∞ *
41 40 a1i φ +∞ *
42 38 rpred φ K
43 42 ltpnfd φ K < +∞
44 lbico1 K * +∞ * K < +∞ K K +∞
45 39 41 43 44 syl3anc φ K K +∞
46 36 16 45 rspcdva φ y X +∞ z + y < z 1 + L E z < K y u z 1 + L E z R u u E
47 46 adantr φ v W +∞ y X +∞ z + y < z 1 + L E z < K y u z 1 + L E z R u u E
48 17 adantr φ v W +∞ z 1 +∞ R z log z 2 log z i = 1 z Y R z i log i z C
49 1 19 20 21 5 6 22 23 9 10 24 25 26 14 27 28 29 30 47 48 pntlemo φ v W +∞ R v v U F U 3
50 49 ralrimiva φ v W +∞ R v v U F U 3
51 oveq1 w = W w +∞ = W +∞
52 51 raleqdv w = W v w +∞ R v v U F U 3 v W +∞ R v v U F U 3
53 52 rspcev W + v W +∞ R v v U F U 3 w + v w +∞ R v v U F U 3
54 18 50 53 syl2anc φ w + v w +∞ R v v U F U 3