Metamath Proof Explorer


Theorem pntlemp

Description: Lemma for pnt . Wrapping up more quantifiers. (Contributed by Mario Carneiro, 14-Apr-2016)

Ref Expression
Hypotheses pntlem3.r R = a + ψ a a
pntlem3.a φ A +
pntlem3.A φ x + R x x A
pntlemp.b φ B +
pntlemp.l φ L 0 1
pntlemp.d D = A + 1
pntlemp.f F = 1 1 D L 32 B D 2
pntlemp.K φ e 0 1 x + k e B e +∞ y x +∞ z + y < z 1 + L e z < k y u z 1 + L e z R u u e
pntlemp.u φ U +
pntlemp.u2 φ U A
pntlemp.e E = U D
pntlemp.k K = e B E
pntlemp.y φ Y + 1 Y
pntlemp.U φ z Y +∞ R z z U
Assertion pntlemp φ w + v w +∞ R v v U F U 3

Proof

Step Hyp Ref Expression
1 pntlem3.r R = a + ψ a a
2 pntlem3.a φ A +
3 pntlem3.A φ x + R x x A
4 pntlemp.b φ B +
5 pntlemp.l φ L 0 1
6 pntlemp.d D = A + 1
7 pntlemp.f F = 1 1 D L 32 B D 2
8 pntlemp.K φ e 0 1 x + k e B e +∞ y x +∞ z + y < z 1 + L e z < k y u z 1 + L e z R u u e
9 pntlemp.u φ U +
10 pntlemp.u2 φ U A
11 pntlemp.e E = U D
12 pntlemp.k K = e B E
13 pntlemp.y φ Y + 1 Y
14 pntlemp.U φ z Y +∞ R z z U
15 oveq2 e = E B e = B E
16 15 fveq2d e = E e B e = e B E
17 16 12 eqtr4di e = E e B e = K
18 17 oveq1d e = E e B e +∞ = K +∞
19 oveq2 e = E L e = L E
20 19 oveq2d e = E 1 + L e = 1 + L E
21 20 oveq1d e = E 1 + L e z = 1 + L E z
22 21 breq1d e = E 1 + L e z < k y 1 + L E z < k y
23 22 anbi2d e = E y < z 1 + L e z < k y y < z 1 + L E z < k y
24 21 oveq2d e = E z 1 + L e z = z 1 + L E z
25 breq2 e = E R u u e R u u E
26 24 25 raleqbidv e = E u z 1 + L e z R u u e u z 1 + L E z R u u E
27 23 26 anbi12d e = E 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
28 27 rexbidv e = E 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
29 28 ralbidv e = E 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
30 18 29 raleqbidv e = E k e B e +∞ y x +∞ z + y < z 1 + L e z < k y u z 1 + L e z R u u e k K +∞ y x +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E
31 30 rexbidv e = E x + k e B e +∞ y x +∞ z + y < z 1 + L e z < k y u z 1 + L e z R u u e x + k K +∞ y x +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E
32 oveq1 x = t x +∞ = t +∞
33 32 raleqdv x = t y x +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E
34 33 ralbidv x = t k K +∞ y x +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E
35 34 cbvrexvw x + k K +∞ y x +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E t + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E
36 31 35 bitrdi e = E x + k e B e +∞ y x +∞ z + y < z 1 + L e z < k y u z 1 + L e z R u u e t + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E
37 1 2 4 5 6 7 9 10 11 12 pntlemc φ E + K + E 0 1 1 < K U E +
38 37 simp3d φ E 0 1 1 < K U E +
39 38 simp1d φ E 0 1
40 36 8 39 rspcdva φ t + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E
41 13 simpld φ Y +
42 41 rpred φ Y
43 13 simprd φ 1 Y
44 1 pntrlog2bnd Y 1 Y c + z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c
45 42 43 44 syl2anc φ c + z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c
46 reeanv t + c + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c t + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E c + z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c
47 2 adantr φ t + c + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c A +
48 4 adantr φ t + c + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c B +
49 5 adantr φ t + c + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c L 0 1
50 9 adantr φ t + c + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c U +
51 10 adantr φ t + c + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c U A
52 13 adantr φ t + c + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c Y + 1 Y
53 simpl t + c + t +
54 rpaddcl Y + t + Y + t +
55 41 53 54 syl2an φ t + c + Y + t +
56 ltaddrp Y t + Y < Y + t
57 42 53 56 syl2an φ t + c + Y < Y + t
58 55 57 jca φ t + c + Y + t + Y < Y + t
59 58 adantrr φ t + c + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c Y + t + Y < Y + t
60 simprlr φ t + c + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c c +
61 eqid Y + 4 L E 2 + Y + t K 2 4 + e 32 B U E L E 2 U 3 + c = Y + 4 L E 2 + Y + t K 2 4 + e 32 B U E L E 2 U 3 + c
62 14 adantr φ t + c + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c z Y +∞ R z z U
63 rpxr t + t *
64 63 ad2antrl φ t + c + t *
65 rpre t + t
66 65 ad2antrl φ t + c + t
67 55 rpred φ t + c + Y + t
68 41 adantr φ t + c + Y +
69 66 68 ltaddrp2d φ t + c + t < Y + t
70 66 67 69 ltled φ t + c + t Y + t
71 iooss1 t * t Y + t Y + t +∞ t +∞
72 64 70 71 syl2anc φ t + c + Y + t +∞ t +∞
73 72 adantrr φ t + c + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c Y + t +∞ t +∞
74 simprrl φ t + c + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E
75 ssralv Y + t +∞ t +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E y Y + t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E
76 75 ralimdv Y + t +∞ t +∞ k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E k K +∞ y Y + t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E
77 73 74 76 sylc φ t + c + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c k K +∞ y Y + t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E
78 simprrr φ t + c + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c
79 1 47 48 49 6 7 50 51 11 12 52 59 60 61 62 77 78 pntleme φ t + c + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c w + v w +∞ R v v U F U 3
80 79 expr φ t + c + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c w + v w +∞ R v v U F U 3
81 80 rexlimdvva φ t + c + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c w + v w +∞ R v v U F U 3
82 46 81 syl5bir φ t + k K +∞ y t +∞ z + y < z 1 + L E z < k y u z 1 + L E z R u u E c + z 1 +∞ R z log z 2 log z n = 1 z Y R z n log n z c w + v w +∞ R v v U F U 3
83 40 45 82 mp2and φ w + v w +∞ R v v U F U 3