ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cvg1nlemcau GIF version

Theorem cvg1nlemcau 9810
Description: Lemma for cvg1n 9812. By selecting spaced out terms for the modified sequence 𝐺, the terms are within 1 / 𝑛 (without the constant 𝐶). (Contributed by Jim Kingdon, 1-Aug-2021.)
Hypotheses
Ref Expression
cvg1n.f (𝜑𝐹:ℕ⟶ℝ)
cvg1n.c (𝜑𝐶 ∈ ℝ+)
cvg1n.cau (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((𝐹𝑛) < ((𝐹𝑘) + (𝐶 / 𝑛)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝐶 / 𝑛))))
cvg1nlem.g 𝐺 = (𝑗 ∈ ℕ ↦ (𝐹‘(𝑗 · 𝑍)))
cvg1nlem.z (𝜑𝑍 ∈ ℕ)
cvg1nlem.start (𝜑𝐶 < 𝑍)
Assertion
Ref Expression
cvg1nlemcau (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((𝐺𝑛) < ((𝐺𝑘) + (1 / 𝑛)) ∧ (𝐺𝑘) < ((𝐺𝑛) + (1 / 𝑛))))
Distinct variable groups:   𝐶,𝑛,𝑘   𝑛,𝐹,𝑗,𝑘   𝑗,𝑍   𝜑,𝑘,𝑛
Allowed substitution hints:   𝜑(𝑗)   𝐶(𝑗)   𝐺(𝑗,𝑘,𝑛)   𝑍(𝑘,𝑛)

Proof of Theorem cvg1nlemcau
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplr 490 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑛 ∈ ℕ)
2 cvg1n.f . . . . . . . . 9 (𝜑𝐹:ℕ⟶ℝ)
32ad2antrr 465 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝐹:ℕ⟶ℝ)
4 cvg1nlem.z . . . . . . . . . 10 (𝜑𝑍 ∈ ℕ)
54ad2antrr 465 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑍 ∈ ℕ)
61, 5nnmulcld 8037 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝑛 · 𝑍) ∈ ℕ)
73, 6ffvelrnd 5330 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹‘(𝑛 · 𝑍)) ∈ ℝ)
8 oveq1 5546 . . . . . . . . 9 (𝑗 = 𝑛 → (𝑗 · 𝑍) = (𝑛 · 𝑍))
98fveq2d 5209 . . . . . . . 8 (𝑗 = 𝑛 → (𝐹‘(𝑗 · 𝑍)) = (𝐹‘(𝑛 · 𝑍)))
10 cvg1nlem.g . . . . . . . 8 𝐺 = (𝑗 ∈ ℕ ↦ (𝐹‘(𝑗 · 𝑍)))
119, 10fvmptg 5275 . . . . . . 7 ((𝑛 ∈ ℕ ∧ (𝐹‘(𝑛 · 𝑍)) ∈ ℝ) → (𝐺𝑛) = (𝐹‘(𝑛 · 𝑍)))
121, 7, 11syl2anc 397 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐺𝑛) = (𝐹‘(𝑛 · 𝑍)))
1312, 7eqeltrd 2130 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐺𝑛) ∈ ℝ)
14 eluznn 8633 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑘 ∈ ℕ)
1514adantll 453 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑘 ∈ ℕ)
1615, 5nnmulcld 8037 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝑘 · 𝑍) ∈ ℕ)
173, 16ffvelrnd 5330 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐹‘(𝑘 · 𝑍)) ∈ ℝ)
18 oveq1 5546 . . . . . . . . . 10 (𝑗 = 𝑘 → (𝑗 · 𝑍) = (𝑘 · 𝑍))
1918fveq2d 5209 . . . . . . . . 9 (𝑗 = 𝑘 → (𝐹‘(𝑗 · 𝑍)) = (𝐹‘(𝑘 · 𝑍)))
2019, 10fvmptg 5275 . . . . . . . 8 ((𝑘 ∈ ℕ ∧ (𝐹‘(𝑘 · 𝑍)) ∈ ℝ) → (𝐺𝑘) = (𝐹‘(𝑘 · 𝑍)))
2115, 17, 20syl2anc 397 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐺𝑘) = (𝐹‘(𝑘 · 𝑍)))
2221, 17eqeltrd 2130 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐺𝑘) ∈ ℝ)
23 cvg1n.c . . . . . . . . 9 (𝜑𝐶 ∈ ℝ+)
2423rpred 8719 . . . . . . . 8 (𝜑𝐶 ∈ ℝ)
2524ad2antrr 465 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝐶 ∈ ℝ)
2625, 6nndivred 8038 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐶 / (𝑛 · 𝑍)) ∈ ℝ)
2722, 26readdcld 7113 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐺𝑘) + (𝐶 / (𝑛 · 𝑍))) ∈ ℝ)
281nnrecred 8035 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (1 / 𝑛) ∈ ℝ)
2922, 28readdcld 7113 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐺𝑘) + (1 / 𝑛)) ∈ ℝ)
30 eluzle 8580 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ𝑛) → 𝑛𝑘)
3130adantl 266 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑛𝑘)
321nnred 8002 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑛 ∈ ℝ)
3315nnred 8002 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑘 ∈ ℝ)
345nnrpd 8718 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑍 ∈ ℝ+)
3532, 33, 34lemul1d 8763 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝑛𝑘 ↔ (𝑛 · 𝑍) ≤ (𝑘 · 𝑍)))
3631, 35mpbid 139 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝑛 · 𝑍) ≤ (𝑘 · 𝑍))
376nnzd 8417 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝑛 · 𝑍) ∈ ℤ)
3816nnzd 8417 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝑘 · 𝑍) ∈ ℤ)
39 eluz 8581 . . . . . . . . . . 11 (((𝑛 · 𝑍) ∈ ℤ ∧ (𝑘 · 𝑍) ∈ ℤ) → ((𝑘 · 𝑍) ∈ (ℤ‘(𝑛 · 𝑍)) ↔ (𝑛 · 𝑍) ≤ (𝑘 · 𝑍)))
4037, 38, 39syl2anc 397 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝑘 · 𝑍) ∈ (ℤ‘(𝑛 · 𝑍)) ↔ (𝑛 · 𝑍) ≤ (𝑘 · 𝑍)))
4136, 40mpbird 160 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝑘 · 𝑍) ∈ (ℤ‘(𝑛 · 𝑍)))
42 cvg1n.cau . . . . . . . . . . . 12 (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((𝐹𝑛) < ((𝐹𝑘) + (𝐶 / 𝑛)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝐶 / 𝑛))))
43 fveq2 5205 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑏 → (𝐹𝑘) = (𝐹𝑏))
4443oveq1d 5554 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑏 → ((𝐹𝑘) + (𝐶 / 𝑛)) = ((𝐹𝑏) + (𝐶 / 𝑛)))
4544breq2d 3803 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑏 → ((𝐹𝑛) < ((𝐹𝑘) + (𝐶 / 𝑛)) ↔ (𝐹𝑛) < ((𝐹𝑏) + (𝐶 / 𝑛))))
4643breq1d 3801 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑏 → ((𝐹𝑘) < ((𝐹𝑛) + (𝐶 / 𝑛)) ↔ (𝐹𝑏) < ((𝐹𝑛) + (𝐶 / 𝑛))))
4745, 46anbi12d 450 . . . . . . . . . . . . . . 15 (𝑘 = 𝑏 → (((𝐹𝑛) < ((𝐹𝑘) + (𝐶 / 𝑛)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝐶 / 𝑛))) ↔ ((𝐹𝑛) < ((𝐹𝑏) + (𝐶 / 𝑛)) ∧ (𝐹𝑏) < ((𝐹𝑛) + (𝐶 / 𝑛)))))
4847cbvralv 2550 . . . . . . . . . . . . . 14 (∀𝑘 ∈ (ℤ𝑛)((𝐹𝑛) < ((𝐹𝑘) + (𝐶 / 𝑛)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝐶 / 𝑛))) ↔ ∀𝑏 ∈ (ℤ𝑛)((𝐹𝑛) < ((𝐹𝑏) + (𝐶 / 𝑛)) ∧ (𝐹𝑏) < ((𝐹𝑛) + (𝐶 / 𝑛))))
4948ralbii 2347 . . . . . . . . . . . . 13 (∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((𝐹𝑛) < ((𝐹𝑘) + (𝐶 / 𝑛)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝐶 / 𝑛))) ↔ ∀𝑛 ∈ ℕ ∀𝑏 ∈ (ℤ𝑛)((𝐹𝑛) < ((𝐹𝑏) + (𝐶 / 𝑛)) ∧ (𝐹𝑏) < ((𝐹𝑛) + (𝐶 / 𝑛))))
50 fveq2 5205 . . . . . . . . . . . . . . 15 (𝑛 = 𝑎 → (ℤ𝑛) = (ℤ𝑎))
51 fveq2 5205 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑎 → (𝐹𝑛) = (𝐹𝑎))
52 oveq2 5547 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑎 → (𝐶 / 𝑛) = (𝐶 / 𝑎))
5352oveq2d 5555 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑎 → ((𝐹𝑏) + (𝐶 / 𝑛)) = ((𝐹𝑏) + (𝐶 / 𝑎)))
5451, 53breq12d 3804 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑎 → ((𝐹𝑛) < ((𝐹𝑏) + (𝐶 / 𝑛)) ↔ (𝐹𝑎) < ((𝐹𝑏) + (𝐶 / 𝑎))))
5551, 52oveq12d 5557 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑎 → ((𝐹𝑛) + (𝐶 / 𝑛)) = ((𝐹𝑎) + (𝐶 / 𝑎)))
5655breq2d 3803 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑎 → ((𝐹𝑏) < ((𝐹𝑛) + (𝐶 / 𝑛)) ↔ (𝐹𝑏) < ((𝐹𝑎) + (𝐶 / 𝑎))))
5754, 56anbi12d 450 . . . . . . . . . . . . . . 15 (𝑛 = 𝑎 → (((𝐹𝑛) < ((𝐹𝑏) + (𝐶 / 𝑛)) ∧ (𝐹𝑏) < ((𝐹𝑛) + (𝐶 / 𝑛))) ↔ ((𝐹𝑎) < ((𝐹𝑏) + (𝐶 / 𝑎)) ∧ (𝐹𝑏) < ((𝐹𝑎) + (𝐶 / 𝑎)))))
5850, 57raleqbidv 2534 . . . . . . . . . . . . . 14 (𝑛 = 𝑎 → (∀𝑏 ∈ (ℤ𝑛)((𝐹𝑛) < ((𝐹𝑏) + (𝐶 / 𝑛)) ∧ (𝐹𝑏) < ((𝐹𝑛) + (𝐶 / 𝑛))) ↔ ∀𝑏 ∈ (ℤ𝑎)((𝐹𝑎) < ((𝐹𝑏) + (𝐶 / 𝑎)) ∧ (𝐹𝑏) < ((𝐹𝑎) + (𝐶 / 𝑎)))))
5958cbvralv 2550 . . . . . . . . . . . . 13 (∀𝑛 ∈ ℕ ∀𝑏 ∈ (ℤ𝑛)((𝐹𝑛) < ((𝐹𝑏) + (𝐶 / 𝑛)) ∧ (𝐹𝑏) < ((𝐹𝑛) + (𝐶 / 𝑛))) ↔ ∀𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ𝑎)((𝐹𝑎) < ((𝐹𝑏) + (𝐶 / 𝑎)) ∧ (𝐹𝑏) < ((𝐹𝑎) + (𝐶 / 𝑎))))
6049, 59bitri 177 . . . . . . . . . . . 12 (∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((𝐹𝑛) < ((𝐹𝑘) + (𝐶 / 𝑛)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝐶 / 𝑛))) ↔ ∀𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ𝑎)((𝐹𝑎) < ((𝐹𝑏) + (𝐶 / 𝑎)) ∧ (𝐹𝑏) < ((𝐹𝑎) + (𝐶 / 𝑎))))
6142, 60sylib 131 . . . . . . . . . . 11 (𝜑 → ∀𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ𝑎)((𝐹𝑎) < ((𝐹𝑏) + (𝐶 / 𝑎)) ∧ (𝐹𝑏) < ((𝐹𝑎) + (𝐶 / 𝑎))))
6261ad2antrr 465 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ∀𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ𝑎)((𝐹𝑎) < ((𝐹𝑏) + (𝐶 / 𝑎)) ∧ (𝐹𝑏) < ((𝐹𝑎) + (𝐶 / 𝑎))))
63 fveq2 5205 . . . . . . . . . . . 12 (𝑎 = (𝑛 · 𝑍) → (ℤ𝑎) = (ℤ‘(𝑛 · 𝑍)))
64 fveq2 5205 . . . . . . . . . . . . . 14 (𝑎 = (𝑛 · 𝑍) → (𝐹𝑎) = (𝐹‘(𝑛 · 𝑍)))
65 oveq2 5547 . . . . . . . . . . . . . . 15 (𝑎 = (𝑛 · 𝑍) → (𝐶 / 𝑎) = (𝐶 / (𝑛 · 𝑍)))
6665oveq2d 5555 . . . . . . . . . . . . . 14 (𝑎 = (𝑛 · 𝑍) → ((𝐹𝑏) + (𝐶 / 𝑎)) = ((𝐹𝑏) + (𝐶 / (𝑛 · 𝑍))))
6764, 66breq12d 3804 . . . . . . . . . . . . 13 (𝑎 = (𝑛 · 𝑍) → ((𝐹𝑎) < ((𝐹𝑏) + (𝐶 / 𝑎)) ↔ (𝐹‘(𝑛 · 𝑍)) < ((𝐹𝑏) + (𝐶 / (𝑛 · 𝑍)))))
6864, 65oveq12d 5557 . . . . . . . . . . . . . 14 (𝑎 = (𝑛 · 𝑍) → ((𝐹𝑎) + (𝐶 / 𝑎)) = ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍))))
6968breq2d 3803 . . . . . . . . . . . . 13 (𝑎 = (𝑛 · 𝑍) → ((𝐹𝑏) < ((𝐹𝑎) + (𝐶 / 𝑎)) ↔ (𝐹𝑏) < ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍)))))
7067, 69anbi12d 450 . . . . . . . . . . . 12 (𝑎 = (𝑛 · 𝑍) → (((𝐹𝑎) < ((𝐹𝑏) + (𝐶 / 𝑎)) ∧ (𝐹𝑏) < ((𝐹𝑎) + (𝐶 / 𝑎))) ↔ ((𝐹‘(𝑛 · 𝑍)) < ((𝐹𝑏) + (𝐶 / (𝑛 · 𝑍))) ∧ (𝐹𝑏) < ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍))))))
7163, 70raleqbidv 2534 . . . . . . . . . . 11 (𝑎 = (𝑛 · 𝑍) → (∀𝑏 ∈ (ℤ𝑎)((𝐹𝑎) < ((𝐹𝑏) + (𝐶 / 𝑎)) ∧ (𝐹𝑏) < ((𝐹𝑎) + (𝐶 / 𝑎))) ↔ ∀𝑏 ∈ (ℤ‘(𝑛 · 𝑍))((𝐹‘(𝑛 · 𝑍)) < ((𝐹𝑏) + (𝐶 / (𝑛 · 𝑍))) ∧ (𝐹𝑏) < ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍))))))
7271rspcv 2669 . . . . . . . . . 10 ((𝑛 · 𝑍) ∈ ℕ → (∀𝑎 ∈ ℕ ∀𝑏 ∈ (ℤ𝑎)((𝐹𝑎) < ((𝐹𝑏) + (𝐶 / 𝑎)) ∧ (𝐹𝑏) < ((𝐹𝑎) + (𝐶 / 𝑎))) → ∀𝑏 ∈ (ℤ‘(𝑛 · 𝑍))((𝐹‘(𝑛 · 𝑍)) < ((𝐹𝑏) + (𝐶 / (𝑛 · 𝑍))) ∧ (𝐹𝑏) < ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍))))))
736, 62, 72sylc 60 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ∀𝑏 ∈ (ℤ‘(𝑛 · 𝑍))((𝐹‘(𝑛 · 𝑍)) < ((𝐹𝑏) + (𝐶 / (𝑛 · 𝑍))) ∧ (𝐹𝑏) < ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍)))))
74 fveq2 5205 . . . . . . . . . . . . 13 (𝑏 = (𝑘 · 𝑍) → (𝐹𝑏) = (𝐹‘(𝑘 · 𝑍)))
7574oveq1d 5554 . . . . . . . . . . . 12 (𝑏 = (𝑘 · 𝑍) → ((𝐹𝑏) + (𝐶 / (𝑛 · 𝑍))) = ((𝐹‘(𝑘 · 𝑍)) + (𝐶 / (𝑛 · 𝑍))))
7675breq2d 3803 . . . . . . . . . . 11 (𝑏 = (𝑘 · 𝑍) → ((𝐹‘(𝑛 · 𝑍)) < ((𝐹𝑏) + (𝐶 / (𝑛 · 𝑍))) ↔ (𝐹‘(𝑛 · 𝑍)) < ((𝐹‘(𝑘 · 𝑍)) + (𝐶 / (𝑛 · 𝑍)))))
7774breq1d 3801 . . . . . . . . . . 11 (𝑏 = (𝑘 · 𝑍) → ((𝐹𝑏) < ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍))) ↔ (𝐹‘(𝑘 · 𝑍)) < ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍)))))
7876, 77anbi12d 450 . . . . . . . . . 10 (𝑏 = (𝑘 · 𝑍) → (((𝐹‘(𝑛 · 𝑍)) < ((𝐹𝑏) + (𝐶 / (𝑛 · 𝑍))) ∧ (𝐹𝑏) < ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍)))) ↔ ((𝐹‘(𝑛 · 𝑍)) < ((𝐹‘(𝑘 · 𝑍)) + (𝐶 / (𝑛 · 𝑍))) ∧ (𝐹‘(𝑘 · 𝑍)) < ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍))))))
7978rspcv 2669 . . . . . . . . 9 ((𝑘 · 𝑍) ∈ (ℤ‘(𝑛 · 𝑍)) → (∀𝑏 ∈ (ℤ‘(𝑛 · 𝑍))((𝐹‘(𝑛 · 𝑍)) < ((𝐹𝑏) + (𝐶 / (𝑛 · 𝑍))) ∧ (𝐹𝑏) < ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍)))) → ((𝐹‘(𝑛 · 𝑍)) < ((𝐹‘(𝑘 · 𝑍)) + (𝐶 / (𝑛 · 𝑍))) ∧ (𝐹‘(𝑘 · 𝑍)) < ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍))))))
8041, 73, 79sylc 60 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐹‘(𝑛 · 𝑍)) < ((𝐹‘(𝑘 · 𝑍)) + (𝐶 / (𝑛 · 𝑍))) ∧ (𝐹‘(𝑘 · 𝑍)) < ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍)))))
8121oveq1d 5554 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐺𝑘) + (𝐶 / (𝑛 · 𝑍))) = ((𝐹‘(𝑘 · 𝑍)) + (𝐶 / (𝑛 · 𝑍))))
8281breq2d 3803 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐹‘(𝑛 · 𝑍)) < ((𝐺𝑘) + (𝐶 / (𝑛 · 𝑍))) ↔ (𝐹‘(𝑛 · 𝑍)) < ((𝐹‘(𝑘 · 𝑍)) + (𝐶 / (𝑛 · 𝑍)))))
8321breq1d 3801 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐺𝑘) < ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍))) ↔ (𝐹‘(𝑘 · 𝑍)) < ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍)))))
8482, 83anbi12d 450 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (((𝐹‘(𝑛 · 𝑍)) < ((𝐺𝑘) + (𝐶 / (𝑛 · 𝑍))) ∧ (𝐺𝑘) < ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍)))) ↔ ((𝐹‘(𝑛 · 𝑍)) < ((𝐹‘(𝑘 · 𝑍)) + (𝐶 / (𝑛 · 𝑍))) ∧ (𝐹‘(𝑘 · 𝑍)) < ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍))))))
8580, 84mpbird 160 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐹‘(𝑛 · 𝑍)) < ((𝐺𝑘) + (𝐶 / (𝑛 · 𝑍))) ∧ (𝐺𝑘) < ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍)))))
8612breq1d 3801 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐺𝑛) < ((𝐺𝑘) + (𝐶 / (𝑛 · 𝑍))) ↔ (𝐹‘(𝑛 · 𝑍)) < ((𝐺𝑘) + (𝐶 / (𝑛 · 𝑍)))))
8712oveq1d 5554 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐺𝑛) + (𝐶 / (𝑛 · 𝑍))) = ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍))))
8887breq2d 3803 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐺𝑘) < ((𝐺𝑛) + (𝐶 / (𝑛 · 𝑍))) ↔ (𝐺𝑘) < ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍)))))
8986, 88anbi12d 450 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (((𝐺𝑛) < ((𝐺𝑘) + (𝐶 / (𝑛 · 𝑍))) ∧ (𝐺𝑘) < ((𝐺𝑛) + (𝐶 / (𝑛 · 𝑍)))) ↔ ((𝐹‘(𝑛 · 𝑍)) < ((𝐺𝑘) + (𝐶 / (𝑛 · 𝑍))) ∧ (𝐺𝑘) < ((𝐹‘(𝑛 · 𝑍)) + (𝐶 / (𝑛 · 𝑍))))))
9085, 89mpbird 160 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐺𝑛) < ((𝐺𝑘) + (𝐶 / (𝑛 · 𝑍))) ∧ (𝐺𝑘) < ((𝐺𝑛) + (𝐶 / (𝑛 · 𝑍)))))
9190simpld 109 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐺𝑛) < ((𝐺𝑘) + (𝐶 / (𝑛 · 𝑍))))
925nnred 8002 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑍 ∈ ℝ)
931nnrpd 8718 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑛 ∈ ℝ+)
94 cvg1nlem.start . . . . . . . . 9 (𝜑𝐶 < 𝑍)
9594ad2antrr 465 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝐶 < 𝑍)
9625, 92, 93, 95ltmul1dd 8775 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐶 · 𝑛) < (𝑍 · 𝑛))
976nncnd 8003 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝑛 · 𝑍) ∈ ℂ)
9897mulid2d 7102 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (1 · (𝑛 · 𝑍)) = (𝑛 · 𝑍))
9998breq2d 3803 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐶 · 𝑛) < (1 · (𝑛 · 𝑍)) ↔ (𝐶 · 𝑛) < (𝑛 · 𝑍)))
100 1red 7099 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → 1 ∈ ℝ)
1016nnrpd 8718 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝑛 · 𝑍) ∈ ℝ+)
10225, 93, 100, 101lt2mul2divd 8782 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐶 · 𝑛) < (1 · (𝑛 · 𝑍)) ↔ (𝐶 / (𝑛 · 𝑍)) < (1 / 𝑛)))
1031nncnd 8003 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑛 ∈ ℂ)
1045nncnd 8003 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑍 ∈ ℂ)
105103, 104mulcomd 7105 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝑛 · 𝑍) = (𝑍 · 𝑛))
106105breq2d 3803 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐶 · 𝑛) < (𝑛 · 𝑍) ↔ (𝐶 · 𝑛) < (𝑍 · 𝑛)))
10799, 102, 1063bitr3d 211 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐶 / (𝑛 · 𝑍)) < (1 / 𝑛) ↔ (𝐶 · 𝑛) < (𝑍 · 𝑛)))
10896, 107mpbird 160 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐶 / (𝑛 · 𝑍)) < (1 / 𝑛))
10926, 28, 22, 108ltadd2dd 7490 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐺𝑘) + (𝐶 / (𝑛 · 𝑍))) < ((𝐺𝑘) + (1 / 𝑛)))
11013, 27, 29, 91, 109lttrd 7200 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐺𝑛) < ((𝐺𝑘) + (1 / 𝑛)))
11113, 26readdcld 7113 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐺𝑛) + (𝐶 / (𝑛 · 𝑍))) ∈ ℝ)
11213, 28readdcld 7113 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐺𝑛) + (1 / 𝑛)) ∈ ℝ)
11390simprd 111 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐺𝑘) < ((𝐺𝑛) + (𝐶 / (𝑛 · 𝑍))))
11426, 28, 13, 108ltadd2dd 7490 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐺𝑛) + (𝐶 / (𝑛 · 𝑍))) < ((𝐺𝑛) + (1 / 𝑛)))
11522, 111, 112, 113, 114lttrd 7200 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → (𝐺𝑘) < ((𝐺𝑛) + (1 / 𝑛)))
116110, 115jca 294 . . 3 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐺𝑛) < ((𝐺𝑘) + (1 / 𝑛)) ∧ (𝐺𝑘) < ((𝐺𝑛) + (1 / 𝑛))))
117116ralrimiva 2409 . 2 ((𝜑𝑛 ∈ ℕ) → ∀𝑘 ∈ (ℤ𝑛)((𝐺𝑛) < ((𝐺𝑘) + (1 / 𝑛)) ∧ (𝐺𝑘) < ((𝐺𝑛) + (1 / 𝑛))))
118117ralrimiva 2409 1 (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((𝐺𝑛) < ((𝐺𝑘) + (1 / 𝑛)) ∧ (𝐺𝑘) < ((𝐺𝑛) + (1 / 𝑛))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wb 102   = wceq 1259  wcel 1409  wral 2323   class class class wbr 3791  cmpt 3845  wf 4925  cfv 4929  (class class class)co 5539  cr 6945  1c1 6947   + caddc 6949   · cmul 6951   < clt 7118  cle 7119   / cdiv 7724  cn 7989  cz 8301  cuz 8568  +crp 8680
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-13 1420  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-coll 3899  ax-sep 3902  ax-nul 3910  ax-pow 3954  ax-pr 3971  ax-un 4197  ax-setind 4289  ax-iinf 4338  ax-cnex 7032  ax-resscn 7033  ax-1cn 7034  ax-1re 7035  ax-icn 7036  ax-addcl 7037  ax-addrcl 7038  ax-mulcl 7039  ax-mulrcl 7040  ax-addcom 7041  ax-mulcom 7042  ax-addass 7043  ax-mulass 7044  ax-distr 7045  ax-i2m1 7046  ax-1rid 7048  ax-0id 7049  ax-rnegex 7050  ax-precex 7051  ax-cnre 7052  ax-pre-ltirr 7053  ax-pre-ltwlin 7054  ax-pre-lttrn 7055  ax-pre-apti 7056  ax-pre-ltadd 7057  ax-pre-mulgt0 7058  ax-pre-mulext 7059
This theorem depends on definitions:  df-bi 114  df-dc 754  df-3or 897  df-3an 898  df-tru 1262  df-fal 1265  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ne 2221  df-nel 2315  df-ral 2328  df-rex 2329  df-reu 2330  df-rmo 2331  df-rab 2332  df-v 2576  df-sbc 2787  df-csb 2880  df-dif 2947  df-un 2949  df-in 2951  df-ss 2958  df-nul 3252  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-int 3643  df-iun 3686  df-br 3792  df-opab 3846  df-mpt 3847  df-tr 3882  df-eprel 4053  df-id 4057  df-po 4060  df-iso 4061  df-iord 4130  df-on 4132  df-suc 4135  df-iom 4341  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-rn 4383  df-res 4384  df-ima 4385  df-iota 4894  df-fun 4931  df-fn 4932  df-f 4933  df-f1 4934  df-fo 4935  df-f1o 4936  df-fv 4937  df-riota 5495  df-ov 5542  df-oprab 5543  df-mpt2 5544  df-1st 5794  df-2nd 5795  df-recs 5950  df-irdg 5987  df-1o 6031  df-2o 6032  df-oadd 6035  df-omul 6036  df-er 6136  df-ec 6138  df-qs 6142  df-ni 6459  df-pli 6460  df-mi 6461  df-lti 6462  df-plpq 6499  df-mpq 6500  df-enq 6502  df-nqqs 6503  df-plqqs 6504  df-mqqs 6505  df-1nqqs 6506  df-rq 6507  df-ltnqqs 6508  df-enq0 6579  df-nq0 6580  df-0nq0 6581  df-plq0 6582  df-mq0 6583  df-inp 6621  df-i1p 6622  df-iplp 6623  df-iltp 6625  df-enr 6868  df-nr 6869  df-ltr 6872  df-0r 6873  df-1r 6874  df-0 6953  df-1 6954  df-r 6956  df-lt 6959  df-pnf 7120  df-mnf 7121  df-xr 7122  df-ltxr 7123  df-le 7124  df-sub 7246  df-neg 7247  df-reap 7639  df-ap 7646  df-div 7725  df-inn 7990  df-n0 8239  df-z 8302  df-uz 8569  df-rp 8681
This theorem is referenced by:  cvg1nlemres  9811
  Copyright terms: Public domain W3C validator