Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pntibndlem3 Structured version   Visualization version   GIF version

Theorem pntibndlem3 25480
 Description: Lemma for pntibnd 25481. Package up pntibndlem2 25479 in quantifiers. (Contributed by Mario Carneiro, 10-Apr-2016.)
Hypotheses
Ref Expression
pntibnd.r 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
pntibndlem1.1 (𝜑𝐴 ∈ ℝ+)
pntibndlem1.l 𝐿 = ((1 / 4) / (𝐴 + 3))
pntibndlem3.2 (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)
pntibndlem3.3 (𝜑𝐵 ∈ ℝ+)
pntibndlem3.k 𝐾 = (exp‘(𝐵 / (𝐸 / 2)))
pntibndlem3.c 𝐶 = ((2 · 𝐵) + (log‘2))
pntibndlem3.4 (𝜑𝐸 ∈ (0(,)1))
pntibndlem3.6 (𝜑𝑍 ∈ ℝ+)
pntibndlem3.5 (𝜑 → ∀𝑚 ∈ (𝐾[,)+∞)∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖𝑖 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅𝑖) / 𝑖)) ≤ (𝐸 / 2)))
Assertion
Ref Expression
pntibndlem3 (𝜑 → ∃𝑥 ∈ ℝ+𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
Distinct variable groups:   𝑖,𝑎,𝑘,𝑚,𝑢,𝑣,𝑥,𝑦,𝑧,𝐸   𝑢,𝐿,𝑣,𝑥,𝑧   𝑢,𝐴,𝑣,𝑥   𝑢,𝐶,𝑣,𝑥,𝑦   𝑅,𝑖,𝑘,𝑚,𝑢,𝑣,𝑥,𝑦,𝑧   𝑚,𝐾   𝑘,𝑍,𝑚,𝑢,𝑣,𝑥,𝑦   𝜑,𝑘,𝑢,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑧,𝑣,𝑖,𝑚,𝑎)   𝐴(𝑦,𝑧,𝑖,𝑘,𝑚,𝑎)   𝐵(𝑥,𝑦,𝑧,𝑣,𝑢,𝑖,𝑘,𝑚,𝑎)   𝐶(𝑧,𝑖,𝑘,𝑚,𝑎)   𝑅(𝑎)   𝐾(𝑥,𝑦,𝑧,𝑣,𝑢,𝑖,𝑘,𝑎)   𝐿(𝑦,𝑖,𝑘,𝑚,𝑎)   𝑍(𝑧,𝑖,𝑎)

Proof of Theorem pntibndlem3
Dummy variables 𝑛 𝑡 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2re 11282 . . 3 2 ∈ ℝ
2 1le2 11433 . . 3 1 ≤ 2
3 chpdifbnd 25443 . . 3 ((2 ∈ ℝ ∧ 1 ≤ 2) → ∃𝑡 ∈ ℝ+𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))
41, 2, 3mp2an 710 . 2 𝑡 ∈ ℝ+𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣))))
5 simpr 479 . . . . . . . . 9 ((𝜑𝑡 ∈ ℝ+) → 𝑡 ∈ ℝ+)
6 ioossre 12428 . . . . . . . . . . . . 13 (0(,)1) ⊆ ℝ
7 pntibndlem3.4 . . . . . . . . . . . . 13 (𝜑𝐸 ∈ (0(,)1))
86, 7sseldi 3742 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℝ)
9 eliooord 12426 . . . . . . . . . . . . . 14 (𝐸 ∈ (0(,)1) → (0 < 𝐸𝐸 < 1))
107, 9syl 17 . . . . . . . . . . . . 13 (𝜑 → (0 < 𝐸𝐸 < 1))
1110simpld 477 . . . . . . . . . . . 12 (𝜑 → 0 < 𝐸)
128, 11elrpd 12062 . . . . . . . . . . 11 (𝜑𝐸 ∈ ℝ+)
1312adantr 472 . . . . . . . . . 10 ((𝜑𝑡 ∈ ℝ+) → 𝐸 ∈ ℝ+)
14 4nn 11379 . . . . . . . . . . 11 4 ∈ ℕ
15 nnrp 12035 . . . . . . . . . . 11 (4 ∈ ℕ → 4 ∈ ℝ+)
1614, 15ax-mp 5 . . . . . . . . . 10 4 ∈ ℝ+
17 rpdivcl 12049 . . . . . . . . . 10 ((𝐸 ∈ ℝ+ ∧ 4 ∈ ℝ+) → (𝐸 / 4) ∈ ℝ+)
1813, 16, 17sylancl 697 . . . . . . . . 9 ((𝜑𝑡 ∈ ℝ+) → (𝐸 / 4) ∈ ℝ+)
195, 18rpdivcld 12082 . . . . . . . 8 ((𝜑𝑡 ∈ ℝ+) → (𝑡 / (𝐸 / 4)) ∈ ℝ+)
2019rpred 12065 . . . . . . 7 ((𝜑𝑡 ∈ ℝ+) → (𝑡 / (𝐸 / 4)) ∈ ℝ)
2120rpefcld 15034 . . . . . 6 ((𝜑𝑡 ∈ ℝ+) → (exp‘(𝑡 / (𝐸 / 4))) ∈ ℝ+)
22 pntibndlem3.6 . . . . . . 7 (𝜑𝑍 ∈ ℝ+)
2322adantr 472 . . . . . 6 ((𝜑𝑡 ∈ ℝ+) → 𝑍 ∈ ℝ+)
2421, 23rpaddcld 12080 . . . . 5 ((𝜑𝑡 ∈ ℝ+) → ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) ∈ ℝ+)
2524adantrr 755 . . . 4 ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) → ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) ∈ ℝ+)
26 breq2 4808 . . . . . . . . . . 11 (𝑖 = 𝑛 → (𝑣 < 𝑖𝑣 < 𝑛))
27 breq1 4807 . . . . . . . . . . 11 (𝑖 = 𝑛 → (𝑖 ≤ ((𝑘 / 2) · 𝑣) ↔ 𝑛 ≤ ((𝑘 / 2) · 𝑣)))
2826, 27anbi12d 749 . . . . . . . . . 10 (𝑖 = 𝑛 → ((𝑣 < 𝑖𝑖 ≤ ((𝑘 / 2) · 𝑣)) ↔ (𝑣 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑣))))
29 fveq2 6352 . . . . . . . . . . . . 13 (𝑖 = 𝑛 → (𝑅𝑖) = (𝑅𝑛))
30 id 22 . . . . . . . . . . . . 13 (𝑖 = 𝑛𝑖 = 𝑛)
3129, 30oveq12d 6831 . . . . . . . . . . . 12 (𝑖 = 𝑛 → ((𝑅𝑖) / 𝑖) = ((𝑅𝑛) / 𝑛))
3231fveq2d 6356 . . . . . . . . . . 11 (𝑖 = 𝑛 → (abs‘((𝑅𝑖) / 𝑖)) = (abs‘((𝑅𝑛) / 𝑛)))
3332breq1d 4814 . . . . . . . . . 10 (𝑖 = 𝑛 → ((abs‘((𝑅𝑖) / 𝑖)) ≤ (𝐸 / 2) ↔ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2)))
3428, 33anbi12d 749 . . . . . . . . 9 (𝑖 = 𝑛 → (((𝑣 < 𝑖𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅𝑖) / 𝑖)) ≤ (𝐸 / 2)) ↔ ((𝑣 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2))))
3534cbvrexv 3311 . . . . . . . 8 (∃𝑖 ∈ ℕ ((𝑣 < 𝑖𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅𝑖) / 𝑖)) ≤ (𝐸 / 2)) ↔ ∃𝑛 ∈ ℕ ((𝑣 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2)))
36 breq1 4807 . . . . . . . . . . 11 (𝑣 = 𝑦 → (𝑣 < 𝑛𝑦 < 𝑛))
37 oveq2 6821 . . . . . . . . . . . 12 (𝑣 = 𝑦 → ((𝑘 / 2) · 𝑣) = ((𝑘 / 2) · 𝑦))
3837breq2d 4816 . . . . . . . . . . 11 (𝑣 = 𝑦 → (𝑛 ≤ ((𝑘 / 2) · 𝑣) ↔ 𝑛 ≤ ((𝑘 / 2) · 𝑦)))
3936, 38anbi12d 749 . . . . . . . . . 10 (𝑣 = 𝑦 → ((𝑣 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑣)) ↔ (𝑦 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑦))))
4039anbi1d 743 . . . . . . . . 9 (𝑣 = 𝑦 → (((𝑣 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2)) ↔ ((𝑦 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2))))
4140rexbidv 3190 . . . . . . . 8 (𝑣 = 𝑦 → (∃𝑛 ∈ ℕ ((𝑣 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2)) ↔ ∃𝑛 ∈ ℕ ((𝑦 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2))))
4235, 41syl5bb 272 . . . . . . 7 (𝑣 = 𝑦 → (∃𝑖 ∈ ℕ ((𝑣 < 𝑖𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅𝑖) / 𝑖)) ≤ (𝐸 / 2)) ↔ ∃𝑛 ∈ ℕ ((𝑦 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2))))
43 oveq1 6820 . . . . . . . . . . . . 13 (𝑚 = (𝑘 / 2) → (𝑚 · 𝑣) = ((𝑘 / 2) · 𝑣))
4443breq2d 4816 . . . . . . . . . . . 12 (𝑚 = (𝑘 / 2) → (𝑖 ≤ (𝑚 · 𝑣) ↔ 𝑖 ≤ ((𝑘 / 2) · 𝑣)))
4544anbi2d 742 . . . . . . . . . . 11 (𝑚 = (𝑘 / 2) → ((𝑣 < 𝑖𝑖 ≤ (𝑚 · 𝑣)) ↔ (𝑣 < 𝑖𝑖 ≤ ((𝑘 / 2) · 𝑣))))
4645anbi1d 743 . . . . . . . . . 10 (𝑚 = (𝑘 / 2) → (((𝑣 < 𝑖𝑖 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅𝑖) / 𝑖)) ≤ (𝐸 / 2)) ↔ ((𝑣 < 𝑖𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅𝑖) / 𝑖)) ≤ (𝐸 / 2))))
4746rexbidv 3190 . . . . . . . . 9 (𝑚 = (𝑘 / 2) → (∃𝑖 ∈ ℕ ((𝑣 < 𝑖𝑖 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅𝑖) / 𝑖)) ≤ (𝐸 / 2)) ↔ ∃𝑖 ∈ ℕ ((𝑣 < 𝑖𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅𝑖) / 𝑖)) ≤ (𝐸 / 2))))
4847ralbidv 3124 . . . . . . . 8 (𝑚 = (𝑘 / 2) → (∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖𝑖 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅𝑖) / 𝑖)) ≤ (𝐸 / 2)) ↔ ∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅𝑖) / 𝑖)) ≤ (𝐸 / 2))))
49 pntibndlem3.5 . . . . . . . . 9 (𝜑 → ∀𝑚 ∈ (𝐾[,)+∞)∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖𝑖 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅𝑖) / 𝑖)) ≤ (𝐸 / 2)))
5049ad2antrr 764 . . . . . . . 8 (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → ∀𝑚 ∈ (𝐾[,)+∞)∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖𝑖 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅𝑖) / 𝑖)) ≤ (𝐸 / 2)))
51 pntibndlem3.c . . . . . . . . . . . . . . . . 17 𝐶 = ((2 · 𝐵) + (log‘2))
52 pntibndlem3.3 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 ∈ ℝ+)
5352adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ ℝ+) → 𝐵 ∈ ℝ+)
5453rpred 12065 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ ℝ+) → 𝐵 ∈ ℝ)
55 remulcl 10213 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (2 · 𝐵) ∈ ℝ)
561, 54, 55sylancr 698 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ ℝ+) → (2 · 𝐵) ∈ ℝ)
57 2rp 12030 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℝ+
58 relogcl 24521 . . . . . . . . . . . . . . . . . . 19 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
5957, 58ax-mp 5 . . . . . . . . . . . . . . . . . 18 (log‘2) ∈ ℝ
60 readdcl 10211 . . . . . . . . . . . . . . . . . 18 (((2 · 𝐵) ∈ ℝ ∧ (log‘2) ∈ ℝ) → ((2 · 𝐵) + (log‘2)) ∈ ℝ)
6156, 59, 60sylancl 697 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ ℝ+) → ((2 · 𝐵) + (log‘2)) ∈ ℝ)
6251, 61syl5eqel 2843 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ ℝ+) → 𝐶 ∈ ℝ)
6362, 13rerpdivcld 12096 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ ℝ+) → (𝐶 / 𝐸) ∈ ℝ)
6463reefcld 15017 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ ℝ+) → (exp‘(𝐶 / 𝐸)) ∈ ℝ)
65 elicopnf 12462 . . . . . . . . . . . . . 14 ((exp‘(𝐶 / 𝐸)) ∈ ℝ → (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ↔ (𝑘 ∈ ℝ ∧ (exp‘(𝐶 / 𝐸)) ≤ 𝑘)))
6664, 65syl 17 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ ℝ+) → (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ↔ (𝑘 ∈ ℝ ∧ (exp‘(𝐶 / 𝐸)) ≤ 𝑘)))
6766simprbda 654 . . . . . . . . . . . 12 (((𝜑𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → 𝑘 ∈ ℝ)
6867rehalfcld 11471 . . . . . . . . . . 11 (((𝜑𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (𝑘 / 2) ∈ ℝ)
69 pntibndlem3.k . . . . . . . . . . . 12 𝐾 = (exp‘(𝐵 / (𝐸 / 2)))
7013rphalfcld 12077 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ ℝ+) → (𝐸 / 2) ∈ ℝ+)
7154, 70rerpdivcld 12096 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ ℝ+) → (𝐵 / (𝐸 / 2)) ∈ ℝ)
7271reefcld 15017 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ ℝ+) → (exp‘(𝐵 / (𝐸 / 2))) ∈ ℝ)
73 remulcl 10213 . . . . . . . . . . . . . . . 16 (((exp‘(𝐵 / (𝐸 / 2))) ∈ ℝ ∧ 2 ∈ ℝ) → ((exp‘(𝐵 / (𝐸 / 2))) · 2) ∈ ℝ)
7472, 1, 73sylancl 697 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ ℝ+) → ((exp‘(𝐵 / (𝐸 / 2))) · 2) ∈ ℝ)
7574adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → ((exp‘(𝐵 / (𝐸 / 2))) · 2) ∈ ℝ)
7664adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (exp‘(𝐶 / 𝐸)) ∈ ℝ)
7771recnd 10260 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ ℝ+) → (𝐵 / (𝐸 / 2)) ∈ ℂ)
7859recni 10244 . . . . . . . . . . . . . . . . . 18 (log‘2) ∈ ℂ
79 efadd 15023 . . . . . . . . . . . . . . . . . 18 (((𝐵 / (𝐸 / 2)) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (exp‘((𝐵 / (𝐸 / 2)) + (log‘2))) = ((exp‘(𝐵 / (𝐸 / 2))) · (exp‘(log‘2))))
8077, 78, 79sylancl 697 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ ℝ+) → (exp‘((𝐵 / (𝐸 / 2)) + (log‘2))) = ((exp‘(𝐵 / (𝐸 / 2))) · (exp‘(log‘2))))
81 reeflog 24526 . . . . . . . . . . . . . . . . . . 19 (2 ∈ ℝ+ → (exp‘(log‘2)) = 2)
8257, 81ax-mp 5 . . . . . . . . . . . . . . . . . 18 (exp‘(log‘2)) = 2
8382oveq2i 6824 . . . . . . . . . . . . . . . . 17 ((exp‘(𝐵 / (𝐸 / 2))) · (exp‘(log‘2))) = ((exp‘(𝐵 / (𝐸 / 2))) · 2)
8480, 83syl6eq 2810 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ ℝ+) → (exp‘((𝐵 / (𝐸 / 2)) + (log‘2))) = ((exp‘(𝐵 / (𝐸 / 2))) · 2))
8559a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ ℝ+) → (log‘2) ∈ ℝ)
86 rerpdivcl 12054 . . . . . . . . . . . . . . . . . . . 20 (((log‘2) ∈ ℝ ∧ 𝐸 ∈ ℝ+) → ((log‘2) / 𝐸) ∈ ℝ)
8759, 13, 86sylancr 698 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ ℝ+) → ((log‘2) / 𝐸) ∈ ℝ)
8878div1i 10945 . . . . . . . . . . . . . . . . . . . 20 ((log‘2) / 1) = (log‘2)
8910simprd 482 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐸 < 1)
9089adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ ℝ+) → 𝐸 < 1)
918adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ ℝ+) → 𝐸 ∈ ℝ)
92 1re 10231 . . . . . . . . . . . . . . . . . . . . . . 23 1 ∈ ℝ
93 ltle 10318 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐸 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐸 < 1 → 𝐸 ≤ 1))
9491, 92, 93sylancl 697 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ ℝ+) → (𝐸 < 1 → 𝐸 ≤ 1))
9590, 94mpd 15 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ ℝ+) → 𝐸 ≤ 1)
9613rpregt0d 12071 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ ℝ+) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
97 1rp 12029 . . . . . . . . . . . . . . . . . . . . . . 23 1 ∈ ℝ+
98 rpregt0 12039 . . . . . . . . . . . . . . . . . . . . . . 23 (1 ∈ ℝ+ → (1 ∈ ℝ ∧ 0 < 1))
9997, 98mp1i 13 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ ℝ+) → (1 ∈ ℝ ∧ 0 < 1))
100 1lt2 11386 . . . . . . . . . . . . . . . . . . . . . . . 24 1 < 2
101 rplogcl 24549 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2 ∈ ℝ ∧ 1 < 2) → (log‘2) ∈ ℝ+)
1021, 100, 101mp2an 710 . . . . . . . . . . . . . . . . . . . . . . 23 (log‘2) ∈ ℝ+
103 rpregt0 12039 . . . . . . . . . . . . . . . . . . . . . . 23 ((log‘2) ∈ ℝ+ → ((log‘2) ∈ ℝ ∧ 0 < (log‘2)))
104102, 103mp1i 13 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ ℝ+) → ((log‘2) ∈ ℝ ∧ 0 < (log‘2)))
105 lediv2 11105 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐸 ∈ ℝ ∧ 0 < 𝐸) ∧ (1 ∈ ℝ ∧ 0 < 1) ∧ ((log‘2) ∈ ℝ ∧ 0 < (log‘2))) → (𝐸 ≤ 1 ↔ ((log‘2) / 1) ≤ ((log‘2) / 𝐸)))
10696, 99, 104, 105syl3anc 1477 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ ℝ+) → (𝐸 ≤ 1 ↔ ((log‘2) / 1) ≤ ((log‘2) / 𝐸)))
10795, 106mpbid 222 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ ℝ+) → ((log‘2) / 1) ≤ ((log‘2) / 𝐸))
10888, 107syl5eqbrr 4840 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ ℝ+) → (log‘2) ≤ ((log‘2) / 𝐸))
10985, 87, 71, 108leadd2dd 10834 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ ℝ+) → ((𝐵 / (𝐸 / 2)) + (log‘2)) ≤ ((𝐵 / (𝐸 / 2)) + ((log‘2) / 𝐸)))
11051oveq1i 6823 . . . . . . . . . . . . . . . . . . . 20 (𝐶 / 𝐸) = (((2 · 𝐵) + (log‘2)) / 𝐸)
11156recnd 10260 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ ℝ+) → (2 · 𝐵) ∈ ℂ)
11278a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ ℝ+) → (log‘2) ∈ ℂ)
113 rpcnne0 12043 . . . . . . . . . . . . . . . . . . . . . 22 (𝐸 ∈ ℝ+ → (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0))
11413, 113syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ ℝ+) → (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0))
115 divdir 10902 . . . . . . . . . . . . . . . . . . . . 21 (((2 · 𝐵) ∈ ℂ ∧ (log‘2) ∈ ℂ ∧ (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0)) → (((2 · 𝐵) + (log‘2)) / 𝐸) = (((2 · 𝐵) / 𝐸) + ((log‘2) / 𝐸)))
116111, 112, 114, 115syl3anc 1477 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ ℝ+) → (((2 · 𝐵) + (log‘2)) / 𝐸) = (((2 · 𝐵) / 𝐸) + ((log‘2) / 𝐸)))
117110, 116syl5eq 2806 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ ℝ+) → (𝐶 / 𝐸) = (((2 · 𝐵) / 𝐸) + ((log‘2) / 𝐸)))
1181recni 10244 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℂ
11954recnd 10260 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑡 ∈ ℝ+) → 𝐵 ∈ ℂ)
120 mulcom 10214 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2 · 𝐵) = (𝐵 · 2))
121118, 119, 120sylancr 698 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ ℝ+) → (2 · 𝐵) = (𝐵 · 2))
122121oveq1d 6828 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ ℝ+) → ((2 · 𝐵) / 𝐸) = ((𝐵 · 2) / 𝐸))
123 rpcnne0 12043 . . . . . . . . . . . . . . . . . . . . . . 23 (2 ∈ ℝ+ → (2 ∈ ℂ ∧ 2 ≠ 0))
12457, 123mp1i 13 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ ℝ+) → (2 ∈ ℂ ∧ 2 ≠ 0))
125 divdiv2 10929 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐵 ∈ ℂ ∧ (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (𝐵 / (𝐸 / 2)) = ((𝐵 · 2) / 𝐸))
126119, 114, 124, 125syl3anc 1477 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ ℝ+) → (𝐵 / (𝐸 / 2)) = ((𝐵 · 2) / 𝐸))
127122, 126eqtr4d 2797 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ ℝ+) → ((2 · 𝐵) / 𝐸) = (𝐵 / (𝐸 / 2)))
128127oveq1d 6828 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ ℝ+) → (((2 · 𝐵) / 𝐸) + ((log‘2) / 𝐸)) = ((𝐵 / (𝐸 / 2)) + ((log‘2) / 𝐸)))
129117, 128eqtrd 2794 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ ℝ+) → (𝐶 / 𝐸) = ((𝐵 / (𝐸 / 2)) + ((log‘2) / 𝐸)))
130109, 129breqtrrd 4832 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ ℝ+) → ((𝐵 / (𝐸 / 2)) + (log‘2)) ≤ (𝐶 / 𝐸))
131 readdcl 10211 . . . . . . . . . . . . . . . . . . 19 (((𝐵 / (𝐸 / 2)) ∈ ℝ ∧ (log‘2) ∈ ℝ) → ((𝐵 / (𝐸 / 2)) + (log‘2)) ∈ ℝ)
13271, 59, 131sylancl 697 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ ℝ+) → ((𝐵 / (𝐸 / 2)) + (log‘2)) ∈ ℝ)
133 efle 15047 . . . . . . . . . . . . . . . . . 18 ((((𝐵 / (𝐸 / 2)) + (log‘2)) ∈ ℝ ∧ (𝐶 / 𝐸) ∈ ℝ) → (((𝐵 / (𝐸 / 2)) + (log‘2)) ≤ (𝐶 / 𝐸) ↔ (exp‘((𝐵 / (𝐸 / 2)) + (log‘2))) ≤ (exp‘(𝐶 / 𝐸))))
134132, 63, 133syl2anc 696 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡 ∈ ℝ+) → (((𝐵 / (𝐸 / 2)) + (log‘2)) ≤ (𝐶 / 𝐸) ↔ (exp‘((𝐵 / (𝐸 / 2)) + (log‘2))) ≤ (exp‘(𝐶 / 𝐸))))
135130, 134mpbid 222 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ ℝ+) → (exp‘((𝐵 / (𝐸 / 2)) + (log‘2))) ≤ (exp‘(𝐶 / 𝐸)))
13684, 135eqbrtrrd 4828 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ ℝ+) → ((exp‘(𝐵 / (𝐸 / 2))) · 2) ≤ (exp‘(𝐶 / 𝐸)))
137136adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → ((exp‘(𝐵 / (𝐸 / 2))) · 2) ≤ (exp‘(𝐶 / 𝐸)))
13866simplbda 655 . . . . . . . . . . . . . 14 (((𝜑𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (exp‘(𝐶 / 𝐸)) ≤ 𝑘)
13975, 76, 67, 137, 138letrd 10386 . . . . . . . . . . . . 13 (((𝜑𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → ((exp‘(𝐵 / (𝐸 / 2))) · 2) ≤ 𝑘)
14072adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (exp‘(𝐵 / (𝐸 / 2))) ∈ ℝ)
141 rpregt0 12039 . . . . . . . . . . . . . . 15 (2 ∈ ℝ+ → (2 ∈ ℝ ∧ 0 < 2))
14257, 141mp1i 13 . . . . . . . . . . . . . 14 (((𝜑𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (2 ∈ ℝ ∧ 0 < 2))
143 lemuldiv 11095 . . . . . . . . . . . . . 14 (((exp‘(𝐵 / (𝐸 / 2))) ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((exp‘(𝐵 / (𝐸 / 2))) · 2) ≤ 𝑘 ↔ (exp‘(𝐵 / (𝐸 / 2))) ≤ (𝑘 / 2)))
144140, 67, 142, 143syl3anc 1477 . . . . . . . . . . . . 13 (((𝜑𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (((exp‘(𝐵 / (𝐸 / 2))) · 2) ≤ 𝑘 ↔ (exp‘(𝐵 / (𝐸 / 2))) ≤ (𝑘 / 2)))
145139, 144mpbid 222 . . . . . . . . . . . 12 (((𝜑𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (exp‘(𝐵 / (𝐸 / 2))) ≤ (𝑘 / 2))
14669, 145syl5eqbr 4839 . . . . . . . . . . 11 (((𝜑𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → 𝐾 ≤ (𝑘 / 2))
14769, 140syl5eqel 2843 . . . . . . . . . . . 12 (((𝜑𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → 𝐾 ∈ ℝ)
148 elicopnf 12462 . . . . . . . . . . . 12 (𝐾 ∈ ℝ → ((𝑘 / 2) ∈ (𝐾[,)+∞) ↔ ((𝑘 / 2) ∈ ℝ ∧ 𝐾 ≤ (𝑘 / 2))))
149147, 148syl 17 . . . . . . . . . . 11 (((𝜑𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → ((𝑘 / 2) ∈ (𝐾[,)+∞) ↔ ((𝑘 / 2) ∈ ℝ ∧ 𝐾 ≤ (𝑘 / 2))))
15068, 146, 149mpbir2and 995 . . . . . . . . . 10 (((𝜑𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (𝑘 / 2) ∈ (𝐾[,)+∞))
151150adantrr 755 . . . . . . . . 9 (((𝜑𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → (𝑘 / 2) ∈ (𝐾[,)+∞))
152151adantlrr 759 . . . . . . . 8 (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → (𝑘 / 2) ∈ (𝐾[,)+∞))
15348, 50, 152rspcdva 3455 . . . . . . 7 (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → ∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅𝑖) / 𝑖)) ≤ (𝐸 / 2)))
154 elioore 12398 . . . . . . . . . 10 (𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞) → 𝑦 ∈ ℝ)
155154ad2antll 767 . . . . . . . . 9 (((𝜑𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑦 ∈ ℝ)
15623rpred 12065 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ℝ+) → 𝑍 ∈ ℝ)
157156adantr 472 . . . . . . . . . 10 (((𝜑𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑍 ∈ ℝ)
15820reefcld 15017 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ ℝ+) → (exp‘(𝑡 / (𝐸 / 4))) ∈ ℝ)
159158, 156readdcld 10261 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ℝ+) → ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) ∈ ℝ)
160159adantr 472 . . . . . . . . . 10 (((𝜑𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) ∈ ℝ)
161156, 21ltaddrp2d 12099 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ℝ+) → 𝑍 < ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍))
162161adantr 472 . . . . . . . . . 10 (((𝜑𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑍 < ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍))
163 eliooord 12426 . . . . . . . . . . . 12 (𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞) → (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) < 𝑦𝑦 < +∞))
164163simpld 477 . . . . . . . . . . 11 (𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞) → ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) < 𝑦)
165164ad2antll 767 . . . . . . . . . 10 (((𝜑𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) < 𝑦)
166157, 160, 155, 162, 165lttrd 10390 . . . . . . . . 9 (((𝜑𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑍 < 𝑦)
167157rexrd 10281 . . . . . . . . . 10 (((𝜑𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑍 ∈ ℝ*)
168 elioopnf 12460 . . . . . . . . . 10 (𝑍 ∈ ℝ* → (𝑦 ∈ (𝑍(,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑍 < 𝑦)))
169167, 168syl 17 . . . . . . . . 9 (((𝜑𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → (𝑦 ∈ (𝑍(,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑍 < 𝑦)))
170155, 166, 169mpbir2and 995 . . . . . . . 8 (((𝜑𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑦 ∈ (𝑍(,)+∞))
171170adantlrr 759 . . . . . . 7 (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑦 ∈ (𝑍(,)+∞))
17242, 153, 171rspcdva 3455 . . . . . 6 (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → ∃𝑛 ∈ ℕ ((𝑦 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2)))
173 pntibnd.r . . . . . . . 8 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
174 pntibndlem1.1 . . . . . . . . 9 (𝜑𝐴 ∈ ℝ+)
175174ad2antrr 764 . . . . . . . 8 (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝐴 ∈ ℝ+)
176 pntibndlem1.l . . . . . . . 8 𝐿 = ((1 / 4) / (𝐴 + 3))
177 pntibndlem3.2 . . . . . . . . . 10 (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)
178 fveq2 6352 . . . . . . . . . . . . . 14 (𝑥 = 𝑣 → (𝑅𝑥) = (𝑅𝑣))
179 id 22 . . . . . . . . . . . . . 14 (𝑥 = 𝑣𝑥 = 𝑣)
180178, 179oveq12d 6831 . . . . . . . . . . . . 13 (𝑥 = 𝑣 → ((𝑅𝑥) / 𝑥) = ((𝑅𝑣) / 𝑣))
181180fveq2d 6356 . . . . . . . . . . . 12 (𝑥 = 𝑣 → (abs‘((𝑅𝑥) / 𝑥)) = (abs‘((𝑅𝑣) / 𝑣)))
182181breq1d 4814 . . . . . . . . . . 11 (𝑥 = 𝑣 → ((abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴 ↔ (abs‘((𝑅𝑣) / 𝑣)) ≤ 𝐴))
183182cbvralv 3310 . . . . . . . . . 10 (∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴 ↔ ∀𝑣 ∈ ℝ+ (abs‘((𝑅𝑣) / 𝑣)) ≤ 𝐴)
184177, 183sylib 208 . . . . . . . . 9 (𝜑 → ∀𝑣 ∈ ℝ+ (abs‘((𝑅𝑣) / 𝑣)) ≤ 𝐴)
185184ad2antrr 764 . . . . . . . 8 (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → ∀𝑣 ∈ ℝ+ (abs‘((𝑅𝑣) / 𝑣)) ≤ 𝐴)
18652ad2antrr 764 . . . . . . . 8 (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝐵 ∈ ℝ+)
1877ad2antrr 764 . . . . . . . 8 (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝐸 ∈ (0(,)1))
18822ad2antrr 764 . . . . . . . 8 (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝑍 ∈ ℝ+)
189 simprrl 823 . . . . . . . 8 (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝑛 ∈ ℕ)
190 simplrl 819 . . . . . . . 8 (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝑡 ∈ ℝ+)
191 simplrr 820 . . . . . . . 8 (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))
192 eqid 2760 . . . . . . . 8 ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) = ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)
193 simprll 821 . . . . . . . 8 (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞))
194 simprlr 822 . . . . . . . 8 (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))
195 simprrr 824 . . . . . . . 8 (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → ((𝑦 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2)))
196173, 175, 176, 185, 186, 69, 51, 187, 188, 189, 190, 191, 192, 193, 194, 195pntibndlem2 25479 . . . . . . 7 (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → ∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
197196anassrs 683 . . . . . 6 ((((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ (𝐸 / 2)))) → ∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
198172, 197rexlimddv 3173 . . . . 5 (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → ∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
199198ralrimivva 3109 . . . 4 ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) → ∀𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
200 oveq1 6820 . . . . . . 7 (𝑥 = ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) → (𝑥(,)+∞) = (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))
201200raleqdv 3283 . . . . . 6 (𝑥 = ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) → (∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸) ↔ ∀𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)))
202201ralbidv 3124 . . . . 5 (𝑥 = ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) → (∀𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸) ↔ ∀𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)))
203202rspcev 3449 . . . 4 ((((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) ∈ ℝ+ ∧ ∀𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)) → ∃𝑥 ∈ ℝ+𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
20425, 199, 203syl2anc 696 . . 3 ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) → ∃𝑥 ∈ ℝ+𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
205204rexlimdvaa 3170 . 2 (𝜑 → (∃𝑡 ∈ ℝ+𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))) → ∃𝑥 ∈ ℝ+𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)))
2064, 205mpi 20 1 (𝜑 → ∃𝑥 ∈ ℝ+𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632   ∈ wcel 2139   ≠ wne 2932  ∀wral 3050  ∃wrex 3051   class class class wbr 4804   ↦ cmpt 4881  ‘cfv 6049  (class class class)co 6813  ℂcc 10126  ℝcr 10127  0cc0 10128  1c1 10129   + caddc 10131   · cmul 10133  +∞cpnf 10263  ℝ*cxr 10265   < clt 10266   ≤ cle 10267   − cmin 10458   / cdiv 10876  ℕcn 11212  2c2 11262  3c3 11263  4c4 11264  ℝ+crp 12025  (,)cioo 12368  [,)cico 12370  [,]cicc 12371  abscabs 14173  expce 14991  logclog 24500  ψcchp 25018 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206  ax-addf 10207  ax-mulf 10208 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-disj 4773  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-of 7062  df-om 7231  df-1st 7333  df-2nd 7334  df-supp 7464  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-er 7911  df-map 8025  df-pm 8026  df-ixp 8075  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-fsupp 8441  df-fi 8482  df-sup 8513  df-inf 8514  df-oi 8580  df-card 8955  df-cda 9182  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-xnn0 11556  df-z 11570  df-dec 11686  df-uz 11880  df-q 11982  df-rp 12026  df-xneg 12139  df-xadd 12140  df-xmul 12141  df-ioo 12372  df-ioc 12373  df-ico 12374  df-icc 12375  df-fz 12520  df-fzo 12660  df-fl 12787  df-mod 12863  df-seq 12996  df-exp 13055  df-fac 13255  df-bc 13284  df-hash 13312  df-shft 14006  df-cj 14038  df-re 14039  df-im 14040  df-sqrt 14174  df-abs 14175  df-limsup 14401  df-clim 14418  df-rlim 14419  df-o1 14420  df-lo1 14421  df-sum 14616  df-ef 14997  df-e 14998  df-sin 14999  df-cos 15000  df-pi 15002  df-dvds 15183  df-gcd 15419  df-prm 15588  df-pc 15744  df-struct 16061  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-ress 16067  df-plusg 16156  df-mulr 16157  df-starv 16158  df-sca 16159  df-vsca 16160  df-ip 16161  df-tset 16162  df-ple 16163  df-ds 16166  df-unif 16167  df-hom 16168  df-cco 16169  df-rest 16285  df-topn 16286  df-0g 16304  df-gsum 16305  df-topgen 16306  df-pt 16307  df-prds 16310  df-xrs 16364  df-qtop 16369  df-imas 16370  df-xps 16372  df-mre 16448  df-mrc 16449  df-acs 16451  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-submnd 17537  df-mulg 17742  df-cntz 17950  df-cmn 18395  df-psmet 19940  df-xmet 19941  df-met 19942  df-bl 19943  df-mopn 19944  df-fbas 19945  df-fg 19946  df-cnfld 19949  df-top 20901  df-topon 20918  df-topsp 20939  df-bases 20952  df-cld 21025  df-ntr 21026  df-cls 21027  df-nei 21104  df-lp 21142  df-perf 21143  df-cn 21233  df-cnp 21234  df-haus 21321  df-cmp 21392  df-tx 21567  df-hmeo 21760  df-fil 21851  df-fm 21943  df-flim 21944  df-flf 21945  df-xms 22326  df-ms 22327  df-tms 22328  df-cncf 22882  df-limc 23829  df-dv 23830  df-log 24502  df-cxp 24503  df-em 24918  df-cht 25022  df-vma 25023  df-chp 25024  df-ppi 25025  df-mu 25026 This theorem is referenced by:  pntibnd  25481
 Copyright terms: Public domain W3C validator