This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chtppilim

Description: The theta function is asymptotic to ppi ( x ) log ( x ) , so it is sufficient to prove theta ( x ) / x ~>r 1 to establish the PNT. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion chtppilim ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ⇝𝑟 1

Proof

Step Hyp Ref Expression
1 halfre ⊢ ( 1 / 2 ) ∈ ℝ
2 1re ⊢ 1 ∈ ℝ
3 rpre ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ )
4 resubcl ⊢ ( ( 1 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 1 − 𝑦 ) ∈ ℝ )
5 2 3 4 sylancr ⊢ ( 𝑦 ∈ ℝ+ → ( 1 − 𝑦 ) ∈ ℝ )
6 ifcl ⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ ( 1 − 𝑦 ) ∈ ℝ ) → if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ∈ ℝ )
7 1 5 6 sylancr ⊢ ( 𝑦 ∈ ℝ+ → if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ∈ ℝ )
8 0red ⊢ ( 𝑦 ∈ ℝ+ → 0 ∈ ℝ )
9 1 a1i ⊢ ( 𝑦 ∈ ℝ+ → ( 1 / 2 ) ∈ ℝ )
10 halfgt0 ⊢ 0 < ( 1 / 2 )
11 10 a1i ⊢ ( 𝑦 ∈ ℝ+ → 0 < ( 1 / 2 ) )
12 max2 ⊢ ( ( ( 1 − 𝑦 ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 1 / 2 ) ≤ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) )
13 5 1 12 sylancl ⊢ ( 𝑦 ∈ ℝ+ → ( 1 / 2 ) ≤ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) )
14 8 9 7 11 13 ltletrd ⊢ ( 𝑦 ∈ ℝ+ → 0 < if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) )
15 7 14 elrpd ⊢ ( 𝑦 ∈ ℝ+ → if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ∈ ℝ+ )
16 15 rpsqrtcld ⊢ ( 𝑦 ∈ ℝ+ → ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ∈ ℝ+ )
17 halflt1 ⊢ ( 1 / 2 ) < 1
18 ltsubrp ⊢ ( ( 1 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 1 − 𝑦 ) < 1 )
19 2 18 mpan ⊢ ( 𝑦 ∈ ℝ+ → ( 1 − 𝑦 ) < 1 )
20 breq1 ⊢ ( ( 1 / 2 ) = if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) → ( ( 1 / 2 ) < 1 ↔ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < 1 ) )
21 breq1 ⊢ ( ( 1 − 𝑦 ) = if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) → ( ( 1 − 𝑦 ) < 1 ↔ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < 1 ) )
22 20 21 ifboth ⊢ ( ( ( 1 / 2 ) < 1 ∧ ( 1 − 𝑦 ) < 1 ) → if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < 1 )
23 17 19 22 sylancr ⊢ ( 𝑦 ∈ ℝ+ → if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < 1 )
24 15 rpge0d ⊢ ( 𝑦 ∈ ℝ+ → 0 ≤ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) )
25 2 a1i ⊢ ( 𝑦 ∈ ℝ+ → 1 ∈ ℝ )
26 0le1 ⊢ 0 ≤ 1
27 26 a1i ⊢ ( 𝑦 ∈ ℝ+ → 0 ≤ 1 )
28 7 24 25 27 sqrtltd ⊢ ( 𝑦 ∈ ℝ+ → ( if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < 1 ↔ ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) < ( √ ‘ 1 ) ) )
29 23 28 mpbid ⊢ ( 𝑦 ∈ ℝ+ → ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) < ( √ ‘ 1 ) )
30 sqrt1 ⊢ ( √ ‘ 1 ) = 1
31 29 30 breqtrdi ⊢ ( 𝑦 ∈ ℝ+ → ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) < 1 )
32 16 31 chtppilimlem2 ⊢ ( 𝑦 ∈ ℝ+ → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ) )
33 5 adantr ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 1 − 𝑦 ) ∈ ℝ )
34 max1 ⊢ ( ( ( 1 − 𝑦 ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 1 − 𝑦 ) ≤ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) )
35 33 1 34 sylancl ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 1 − 𝑦 ) ≤ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) )
36 7 adantr ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ∈ ℝ )
37 2re ⊢ 2 ∈ ℝ
38 elicopnf ⊢ ( 2 ∈ ℝ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) ) )
39 37 38 ax-mp ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) )
40 39 simplbi ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℝ )
41 chtcl ⊢ ( 𝑥 ∈ ℝ → ( θ ‘ 𝑥 ) ∈ ℝ )
42 40 41 syl ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( θ ‘ 𝑥 ) ∈ ℝ )
43 ppinncl ⊢ ( ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) → ( π ‘ 𝑥 ) ∈ ℕ )
44 39 43 sylbi ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( π ‘ 𝑥 ) ∈ ℕ )
45 44 nnrpd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( π ‘ 𝑥 ) ∈ ℝ+ )
46 2 a1i ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 1 ∈ ℝ )
47 37 a1i ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 2 ∈ ℝ )
48 1lt2 ⊢ 1 < 2
49 48 a1i ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 1 < 2 )
50 39 simprbi ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 2 ≤ 𝑥 )
51 46 47 40 49 50 ltletrd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 1 < 𝑥 )
52 40 51 rplogcld ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
53 45 52 rpmulcld ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ+ )
54 42 53 rerpdivcld ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
55 54 adantl ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
56 lelttr ⊢ ( ( ( 1 − 𝑦 ) ∈ ℝ ∧ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ∈ ℝ ∧ ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ ) → ( ( ( 1 − 𝑦 ) ≤ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ∧ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) → ( 1 − 𝑦 ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) )
57 33 36 55 56 syl3anc ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( 1 − 𝑦 ) ≤ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ∧ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) → ( 1 − 𝑦 ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) )
58 35 57 mpand ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) → ( 1 − 𝑦 ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) )
59 7 recnd ⊢ ( 𝑦 ∈ ℝ+ → if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ∈ ℂ )
60 59 sqsqrtd ⊢ ( 𝑦 ∈ ℝ+ → ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) = if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) )
61 60 adantr ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) = if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) )
62 61 oveq1d ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) = ( if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
63 62 breq1d ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ↔ ( if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ) )
64 42 adantl ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( θ ‘ 𝑥 ) ∈ ℝ )
65 53 rpregt0d ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ ∧ 0 < ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
66 65 adantl ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ ∧ 0 < ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
67 ltmuldiv ⊢ ( ( if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ∈ ℝ ∧ ( θ ‘ 𝑥 ) ∈ ℝ ∧ ( ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ ∧ 0 < ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) → ( ( if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ↔ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) )
68 36 64 66 67 syl3anc ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ↔ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) )
69 63 68 bitrd ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ↔ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) )
70 0red ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 ∈ ℝ )
71 2pos ⊢ 0 < 2
72 71 a1i ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 < 2 )
73 70 47 40 72 50 ltletrd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 < 𝑥 )
74 40 73 elrpd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℝ+ )
75 chtleppi ⊢ ( 𝑥 ∈ ℝ+ → ( θ ‘ 𝑥 ) ≤ ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) )
76 74 75 syl ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( θ ‘ 𝑥 ) ≤ ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) )
77 53 rpcnd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
78 77 mulridd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) · 1 ) = ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) )
79 76 78 breqtrrd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( θ ‘ 𝑥 ) ≤ ( ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) · 1 ) )
80 42 46 53 ledivmuld ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ≤ 1 ↔ ( θ ‘ 𝑥 ) ≤ ( ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) · 1 ) ) )
81 79 80 mpbird ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ≤ 1 )
82 54 46 81 abssuble0d ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) = ( 1 − ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) )
83 82 breq1d ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 ↔ ( 1 − ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) < 𝑦 ) )
84 83 adantl ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 ↔ ( 1 − ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) < 𝑦 ) )
85 2 a1i ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 1 ∈ ℝ )
86 3 adantr ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 𝑦 ∈ ℝ )
87 ltsub23 ⊢ ( ( 1 ∈ ℝ ∧ ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 1 − ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) < 𝑦 ↔ ( 1 − 𝑦 ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) )
88 85 55 86 87 syl3anc ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( 1 − ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) < 𝑦 ↔ ( 1 − 𝑦 ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) )
89 84 88 bitrd ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 ↔ ( 1 − 𝑦 ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) )
90 58 69 89 3imtr4d ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) → ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 ) )
91 90 imim2d ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( 𝑧 ≤ 𝑥 → ( ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ) → ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 ) ) )
92 91 ralimdva ⊢ ( 𝑦 ∈ ℝ+ → ( ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ) → ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 ) ) )
93 92 reximdv ⊢ ( 𝑦 ∈ ℝ+ → ( ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 ) ) )
94 32 93 mpd ⊢ ( 𝑦 ∈ ℝ+ → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 ) )
95 94 rgen ⊢ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 )
96 54 recnd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
97 96 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
98 97 ralrimiva ⊢ ( ⊤ → ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
99 40 ssriv ⊢ ( 2 [,) +∞ ) ⊆ ℝ
100 99 a1i ⊢ ( ⊤ → ( 2 [,) +∞ ) ⊆ ℝ )
101 1cnd ⊢ ( ⊤ → 1 ∈ ℂ )
102 98 100 101 rlim2 ⊢ ( ⊤ → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ⇝𝑟 1 ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 ) ) )
103 95 102 mpbiri ⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ⇝𝑟 1 )
104 103 mptru ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ⇝𝑟 1