Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > cvg1nlemf | GIF version |
Description: Lemma for cvg1n 10928. The modified sequence 𝐺 is a sequence. (Contributed by Jim Kingdon, 1-Aug-2021.) |
Ref | Expression |
---|---|
cvg1n.f | ⊢ (𝜑 → 𝐹:ℕ⟶ℝ) |
cvg1n.c | ⊢ (𝜑 → 𝐶 ∈ ℝ+) |
cvg1n.cau | ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛)))) |
cvg1nlem.g | ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ (𝐹‘(𝑗 · 𝑍))) |
cvg1nlem.z | ⊢ (𝜑 → 𝑍 ∈ ℕ) |
cvg1nlem.start | ⊢ (𝜑 → 𝐶 < 𝑍) |
Ref | Expression |
---|---|
cvg1nlemf | ⊢ (𝜑 → 𝐺:ℕ⟶ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cvg1n.f | . . . 4 ⊢ (𝜑 → 𝐹:ℕ⟶ℝ) | |
2 | 1 | adantr 274 | . . 3 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐹:ℕ⟶ℝ) |
3 | simpr 109 | . . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) | |
4 | cvg1nlem.z | . . . . 5 ⊢ (𝜑 → 𝑍 ∈ ℕ) | |
5 | 4 | adantr 274 | . . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ ℕ) |
6 | 3, 5 | nnmulcld 8906 | . . 3 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 · 𝑍) ∈ ℕ) |
7 | 2, 6 | ffvelrnd 5621 | . 2 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 · 𝑍)) ∈ ℝ) |
8 | cvg1nlem.g | . 2 ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ (𝐹‘(𝑗 · 𝑍))) | |
9 | 7, 8 | fmptd 5639 | 1 ⊢ (𝜑 → 𝐺:ℕ⟶ℝ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1343 ∈ wcel 2136 ∀wral 2444 class class class wbr 3982 ↦ cmpt 4043 ⟶wf 5184 ‘cfv 5188 (class class class)co 5842 ℝcr 7752 + caddc 7756 · cmul 7758 < clt 7933 / cdiv 8568 ℕcn 8857 ℤ≥cuz 9466 ℝ+crp 9589 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-14 2139 ax-ext 2147 ax-sep 4100 ax-pow 4153 ax-pr 4187 ax-cnex 7844 ax-resscn 7845 ax-1cn 7846 ax-1re 7847 ax-icn 7848 ax-addcl 7849 ax-addrcl 7850 ax-mulcl 7851 ax-mulcom 7854 ax-addass 7855 ax-mulass 7856 ax-distr 7857 ax-1rid 7860 ax-cnre 7864 |
This theorem depends on definitions: df-bi 116 df-3an 970 df-tru 1346 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ral 2449 df-rex 2450 df-rab 2453 df-v 2728 df-sbc 2952 df-un 3120 df-in 3122 df-ss 3129 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-br 3983 df-opab 4044 df-mpt 4045 df-id 4271 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-fv 5196 df-ov 5845 df-inn 8858 |
This theorem is referenced by: cvg1nlemres 10927 |
Copyright terms: Public domain | W3C validator |