Step | Hyp | Ref
| Expression |
1 | | 1z 12207 |
. . . . . 6
⊢ 1 ∈
ℤ |
2 | | seqfn 13586 |
. . . . . 6
⊢ (1 ∈
ℤ → seq1( +𝑒 , 𝐹) Fn
(ℤ≥‘1)) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢ seq1(
+𝑒 , 𝐹)
Fn (ℤ≥‘1) |
4 | | nnuz 12477 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
5 | 4 | fneq2i 6477 |
. . . . 5
⊢ (seq1(
+𝑒 , 𝐹)
Fn ℕ ↔ seq1( +𝑒 , 𝐹) Fn
(ℤ≥‘1)) |
6 | 3, 5 | mpbir 234 |
. . . 4
⊢ seq1(
+𝑒 , 𝐹)
Fn ℕ |
7 | | iccssxr 13018 |
. . . . . 6
⊢
(0[,]+∞) ⊆ ℝ* |
8 | | esumfsup.1 |
. . . . . . . 8
⊢
Ⅎ𝑘𝐹 |
9 | 8 | esumfzf 31749 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ Σ*𝑘
∈ (1...𝑛)(𝐹‘𝑘) = (seq1( +𝑒 , 𝐹)‘𝑛)) |
10 | | ovex 7246 |
. . . . . . . 8
⊢
(1...𝑛) ∈
V |
11 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘ℕ |
12 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(0[,]+∞) |
13 | 8, 11, 12 | nff 6541 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 𝐹:ℕ⟶(0[,]+∞) |
14 | | nfv 1922 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 𝑛 ∈ ℕ |
15 | 13, 14 | nfan 1907 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈
ℕ) |
16 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ 𝑘 ∈ (1...𝑛)) → 𝐹:ℕ⟶(0[,]+∞)) |
17 | | 1nn 11841 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℕ |
18 | | fzssnn 13156 |
. . . . . . . . . . . . 13
⊢ (1 ∈
ℕ → (1...𝑛)
⊆ ℕ) |
19 | 17, 18 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ 𝑘 ∈ (1...𝑛)) → (1...𝑛) ⊆
ℕ) |
20 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...𝑛)) |
21 | 19, 20 | sseldd 3902 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
22 | 16, 21 | ffvelrnd 6905 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ 𝑘 ∈ (1...𝑛)) → (𝐹‘𝑘) ∈ (0[,]+∞)) |
23 | 22 | ex 416 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ (𝑘 ∈ (1...𝑛) → (𝐹‘𝑘) ∈ (0[,]+∞))) |
24 | 15, 23 | ralrimi 3137 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ ∀𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ∈ (0[,]+∞)) |
25 | | nfcv 2904 |
. . . . . . . . 9
⊢
Ⅎ𝑘(1...𝑛) |
26 | 25 | esumcl 31710 |
. . . . . . . 8
⊢
(((1...𝑛) ∈ V
∧ ∀𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ∈ (0[,]+∞)) →
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ∈ (0[,]+∞)) |
27 | 10, 24, 26 | sylancr 590 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ Σ*𝑘
∈ (1...𝑛)(𝐹‘𝑘) ∈ (0[,]+∞)) |
28 | 9, 27 | eqeltrrd 2839 |
. . . . . 6
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ (seq1( +𝑒 , 𝐹)‘𝑛) ∈ (0[,]+∞)) |
29 | 7, 28 | sseldi 3899 |
. . . . 5
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ (seq1( +𝑒 , 𝐹)‘𝑛) ∈
ℝ*) |
30 | 29 | ralrimiva 3105 |
. . . 4
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ ∀𝑛 ∈
ℕ (seq1( +𝑒 , 𝐹)‘𝑛) ∈
ℝ*) |
31 | | fnfvrnss 6937 |
. . . 4
⊢ ((seq1(
+𝑒 , 𝐹)
Fn ℕ ∧ ∀𝑛
∈ ℕ (seq1( +𝑒 , 𝐹)‘𝑛) ∈ ℝ*) → ran
seq1( +𝑒 , 𝐹) ⊆
ℝ*) |
32 | 6, 30, 31 | sylancr 590 |
. . 3
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ ran seq1( +𝑒 , 𝐹) ⊆
ℝ*) |
33 | | nnex 11836 |
. . . . 5
⊢ ℕ
∈ V |
34 | | ffvelrn 6902 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑘 ∈ ℕ)
→ (𝐹‘𝑘) ∈
(0[,]+∞)) |
35 | 34 | ex 416 |
. . . . . 6
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ (𝑘 ∈ ℕ
→ (𝐹‘𝑘) ∈
(0[,]+∞))) |
36 | 13, 35 | ralrimi 3137 |
. . . . 5
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ ∀𝑘 ∈
ℕ (𝐹‘𝑘) ∈
(0[,]+∞)) |
37 | 11 | esumcl 31710 |
. . . . 5
⊢ ((ℕ
∈ V ∧ ∀𝑘
∈ ℕ (𝐹‘𝑘) ∈ (0[,]+∞)) →
Σ*𝑘 ∈
ℕ(𝐹‘𝑘) ∈
(0[,]+∞)) |
38 | 33, 36, 37 | sylancr 590 |
. . . 4
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ Σ*𝑘
∈ ℕ(𝐹‘𝑘) ∈ (0[,]+∞)) |
39 | 7, 38 | sseldi 3899 |
. . 3
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ Σ*𝑘
∈ ℕ(𝐹‘𝑘) ∈
ℝ*) |
40 | | fvelrnb 6773 |
. . . . . . . . 9
⊢ (seq1(
+𝑒 , 𝐹)
Fn ℕ → (𝑥 ∈
ran seq1( +𝑒 , 𝐹) ↔ ∃𝑛 ∈ ℕ (seq1( +𝑒
, 𝐹)‘𝑛) = 𝑥)) |
41 | 6, 40 | mp1i 13 |
. . . . . . . 8
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ (𝑥 ∈ ran seq1(
+𝑒 , 𝐹)
↔ ∃𝑛 ∈
ℕ (seq1( +𝑒 , 𝐹)‘𝑛) = 𝑥)) |
42 | | eqcom 2744 |
. . . . . . . . . 10
⊢
(Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) = 𝑥 ↔ 𝑥 = Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) |
43 | 9 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ (Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) = 𝑥 ↔ (seq1( +𝑒 , 𝐹)‘𝑛) = 𝑥)) |
44 | 42, 43 | bitr3id 288 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ (𝑥 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ↔ (seq1( +𝑒 , 𝐹)‘𝑛) = 𝑥)) |
45 | 44 | rexbidva 3215 |
. . . . . . . 8
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ (∃𝑛 ∈
ℕ 𝑥 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ↔ ∃𝑛 ∈ ℕ (seq1( +𝑒
, 𝐹)‘𝑛) = 𝑥)) |
46 | 41, 45 | bitr4d 285 |
. . . . . . 7
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ (𝑥 ∈ ran seq1(
+𝑒 , 𝐹)
↔ ∃𝑛 ∈
ℕ 𝑥 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘))) |
47 | 46 | biimpa 480 |
. . . . . 6
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ran seq1(
+𝑒 , 𝐹))
→ ∃𝑛 ∈
ℕ 𝑥 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘)) |
48 | 33 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ ℕ ∈ V) |
49 | 34 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ 𝑘 ∈ ℕ)
→ (𝐹‘𝑘) ∈
(0[,]+∞)) |
50 | 17, 18 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ (1...𝑛) ⊆
ℕ) |
51 | 15, 48, 49, 50 | esummono 31734 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ Σ*𝑘
∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) |
52 | 51 | ralrimiva 3105 |
. . . . . . 7
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ ∀𝑛 ∈
ℕ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) |
53 | 52 | adantr 484 |
. . . . . 6
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ran seq1(
+𝑒 , 𝐹))
→ ∀𝑛 ∈
ℕ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) |
54 | 47, 53 | jca 515 |
. . . . 5
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ran seq1(
+𝑒 , 𝐹))
→ (∃𝑛 ∈
ℕ 𝑥 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ∧ ∀𝑛 ∈ ℕ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘))) |
55 | | r19.29r 3177 |
. . . . 5
⊢
((∃𝑛 ∈
ℕ 𝑥 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ∧ ∀𝑛 ∈ ℕ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) → ∃𝑛 ∈ ℕ (𝑥 = Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ∧ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘))) |
56 | | breq1 5056 |
. . . . . . 7
⊢ (𝑥 = Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) → (𝑥 ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘) ↔ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘))) |
57 | 56 | biimpar 481 |
. . . . . 6
⊢ ((𝑥 = Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ∧ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) → 𝑥 ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) |
58 | 57 | rexlimivw 3201 |
. . . . 5
⊢
(∃𝑛 ∈
ℕ (𝑥 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ∧ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) → 𝑥 ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) |
59 | 54, 55, 58 | 3syl 18 |
. . . 4
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ran seq1(
+𝑒 , 𝐹))
→ 𝑥 ≤
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) |
60 | 59 | ralrimiva 3105 |
. . 3
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ ∀𝑥 ∈ ran
seq1( +𝑒 , 𝐹)𝑥 ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) |
61 | | nfv 1922 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘 𝑥 ∈ ℝ |
62 | 13, 61 | nfan 1907 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈
ℝ) |
63 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘𝑥 |
64 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘
< |
65 | 11 | nfesum1 31720 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘Σ*𝑘 ∈ ℕ(𝐹‘𝑘) |
66 | 63, 64, 65 | nfbr 5100 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘) |
67 | 62, 66 | nfan 1907 |
. . . . . . . . 9
⊢
Ⅎ𝑘((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) |
68 | 33 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → ℕ ∈
V) |
69 | | simplll 775 |
. . . . . . . . . 10
⊢ ((((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶(0[,]+∞)) |
70 | 69, 34 | sylancom 591 |
. . . . . . . . 9
⊢ ((((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ (0[,]+∞)) |
71 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → 𝑥 ∈ ℝ) |
72 | 71 | rexrd 10883 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → 𝑥 ∈ ℝ*) |
73 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) |
74 | 67, 68, 70, 72, 73 | esumlub 31740 |
. . . . . . . 8
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → ∃𝑎 ∈ (𝒫 ℕ ∩
Fin)𝑥 <
Σ*𝑘 ∈
𝑎(𝐹‘𝑘)) |
75 | | ssnnssfz 30828 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (𝒫 ℕ ∩
Fin) → ∃𝑛 ∈
ℕ 𝑎 ⊆
(1...𝑛)) |
76 | | r19.42v 3263 |
. . . . . . . . . . 11
⊢
(∃𝑛 ∈
ℕ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) ↔ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ ∃𝑛 ∈ ℕ 𝑎 ⊆ (1...𝑛))) |
77 | | nfv 1922 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘 𝑎 ⊆ (1...𝑛) |
78 | 67, 77 | nfan 1907 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘(((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) |
79 | 10 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) → (1...𝑛) ∈ V) |
80 | | simp-4l 783 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) ∧ 𝑘 ∈ (1...𝑛)) → 𝐹:ℕ⟶(0[,]+∞)) |
81 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑛) ⊆
ℕ |
82 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...𝑛)) |
83 | 81, 82 | sseldi 3899 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
84 | 80, 83 | ffvelrnd 6905 |
. . . . . . . . . . . . 13
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) ∧ 𝑘 ∈ (1...𝑛)) → (𝐹‘𝑘) ∈ (0[,]+∞)) |
85 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) → 𝑎 ⊆ (1...𝑛)) |
86 | 78, 79, 84, 85 | esummono 31734 |
. . . . . . . . . . . 12
⊢ ((((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) → Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) |
87 | 86 | reximi 3166 |
. . . . . . . . . . 11
⊢
(∃𝑛 ∈
ℕ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) → ∃𝑛 ∈ ℕ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) |
88 | 76, 87 | sylbir 238 |
. . . . . . . . . 10
⊢ ((((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ ∃𝑛 ∈ ℕ 𝑎 ⊆ (1...𝑛)) → ∃𝑛 ∈ ℕ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) |
89 | 75, 88 | sylan2 596 |
. . . . . . . . 9
⊢ ((((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) →
∃𝑛 ∈ ℕ
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) |
90 | 89 | ralrimiva 3105 |
. . . . . . . 8
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → ∀𝑎 ∈ (𝒫 ℕ ∩
Fin)∃𝑛 ∈ ℕ
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) |
91 | | r19.29r 3177 |
. . . . . . . . 9
⊢
((∃𝑎 ∈
(𝒫 ℕ ∩ Fin)𝑥 < Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ ∀𝑎 ∈ (𝒫 ℕ ∩
Fin)∃𝑛 ∈ ℕ
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → ∃𝑎 ∈ (𝒫 ℕ ∩ Fin)(𝑥 < Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ ∃𝑛 ∈ ℕ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
92 | | r19.42v 3263 |
. . . . . . . . . 10
⊢
(∃𝑛 ∈
ℕ (𝑥 <
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ∧ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) ↔ (𝑥 < Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ ∃𝑛 ∈ ℕ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
93 | 92 | rexbii 3170 |
. . . . . . . . 9
⊢
(∃𝑎 ∈
(𝒫 ℕ ∩ Fin)∃𝑛 ∈ ℕ (𝑥 < Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) ↔ ∃𝑎 ∈ (𝒫 ℕ ∩ Fin)(𝑥 < Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ ∃𝑛 ∈ ℕ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
94 | 91, 93 | sylibr 237 |
. . . . . . . 8
⊢
((∃𝑎 ∈
(𝒫 ℕ ∩ Fin)𝑥 < Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ ∀𝑎 ∈ (𝒫 ℕ ∩
Fin)∃𝑛 ∈ ℕ
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → ∃𝑎 ∈ (𝒫 ℕ ∩
Fin)∃𝑛 ∈ ℕ
(𝑥 <
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ∧ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
95 | 74, 90, 94 | syl2anc 587 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → ∃𝑎 ∈ (𝒫 ℕ ∩
Fin)∃𝑛 ∈ ℕ
(𝑥 <
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ∧ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
96 | | simp-4r 784 |
. . . . . . . . . . 11
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
𝑥 ∈
ℝ) |
97 | 96 | rexrd 10883 |
. . . . . . . . . 10
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
𝑥 ∈
ℝ*) |
98 | | vex 3412 |
. . . . . . . . . . . 12
⊢ 𝑎 ∈ V |
99 | | nfcv 2904 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘𝑎 |
100 | 99 | nfel1 2920 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘 𝑎 ∈ (𝒫 ℕ ∩
Fin) |
101 | 67, 100 | nfan 1907 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘(((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩
Fin)) |
102 | 101, 14 | nfan 1907 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘((((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈
ℕ) |
103 | | simp-5l 785 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ 𝑎) → 𝐹:ℕ⟶(0[,]+∞)) |
104 | | simpllr 776 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ 𝑎) → 𝑎 ∈ (𝒫 ℕ ∩
Fin)) |
105 | | inss1 4143 |
. . . . . . . . . . . . . . . . . 18
⊢
(𝒫 ℕ ∩ Fin) ⊆ 𝒫 ℕ |
106 | 105 | sseli 3896 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ (𝒫 ℕ ∩
Fin) → 𝑎 ∈
𝒫 ℕ) |
107 | | elpwi 4522 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ 𝒫 ℕ →
𝑎 ⊆
ℕ) |
108 | 104, 106,
107 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ 𝑎) → 𝑎 ⊆ ℕ) |
109 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ 𝑎) → 𝑘 ∈ 𝑎) |
110 | 108, 109 | sseldd 3902 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ 𝑎) → 𝑘 ∈ ℕ) |
111 | 103, 110 | ffvelrnd 6905 |
. . . . . . . . . . . . . 14
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ 𝑎) → (𝐹‘𝑘) ∈ (0[,]+∞)) |
112 | 111 | ex 416 |
. . . . . . . . . . . . 13
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
(𝑘 ∈ 𝑎 → (𝐹‘𝑘) ∈ (0[,]+∞))) |
113 | 102, 112 | ralrimi 3137 |
. . . . . . . . . . . 12
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
∀𝑘 ∈ 𝑎 (𝐹‘𝑘) ∈ (0[,]+∞)) |
114 | 99 | esumcl 31710 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ V ∧ ∀𝑘 ∈ 𝑎 (𝐹‘𝑘) ∈ (0[,]+∞)) →
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ∈ (0[,]+∞)) |
115 | 98, 113, 114 | sylancr 590 |
. . . . . . . . . . 11
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ∈ (0[,]+∞)) |
116 | 7, 115 | sseldi 3899 |
. . . . . . . . . 10
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ∈
ℝ*) |
117 | | simp-5l 785 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ (1...𝑛)) → 𝐹:ℕ⟶(0[,]+∞)) |
118 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...𝑛)) |
119 | 81, 118 | sseldi 3899 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
120 | 117, 119 | ffvelrnd 6905 |
. . . . . . . . . . . . . 14
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ (1...𝑛)) → (𝐹‘𝑘) ∈ (0[,]+∞)) |
121 | 120 | ex 416 |
. . . . . . . . . . . . 13
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
(𝑘 ∈ (1...𝑛) → (𝐹‘𝑘) ∈ (0[,]+∞))) |
122 | 102, 121 | ralrimi 3137 |
. . . . . . . . . . . 12
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
∀𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ∈ (0[,]+∞)) |
123 | 10, 122, 26 | sylancr 590 |
. . . . . . . . . . 11
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ∈ (0[,]+∞)) |
124 | 7, 123 | sseldi 3899 |
. . . . . . . . . 10
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ∈
ℝ*) |
125 | | xrltletr 12747 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ*
∧ Σ*𝑘
∈ 𝑎(𝐹‘𝑘) ∈ ℝ* ∧
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ∈ ℝ*) → ((𝑥 < Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
126 | 97, 116, 124, 125 | syl3anc 1373 |
. . . . . . . . 9
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
((𝑥 <
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ∧ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
127 | 126 | reximdva 3193 |
. . . . . . . 8
⊢ ((((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) →
(∃𝑛 ∈ ℕ
(𝑥 <
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ∧ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → ∃𝑛 ∈ ℕ 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
128 | 127 | rexlimdva 3203 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → (∃𝑎 ∈ (𝒫 ℕ ∩
Fin)∃𝑛 ∈ ℕ
(𝑥 <
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ∧ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → ∃𝑛 ∈ ℕ 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
129 | 95, 128 | mpd 15 |
. . . . . 6
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → ∃𝑛 ∈ ℕ 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) |
130 | | fvelrnb 6773 |
. . . . . . . . . 10
⊢ (seq1(
+𝑒 , 𝐹)
Fn ℕ → (𝑦 ∈
ran seq1( +𝑒 , 𝐹) ↔ ∃𝑛 ∈ ℕ (seq1( +𝑒
, 𝐹)‘𝑛) = 𝑦)) |
131 | 6, 130 | mp1i 13 |
. . . . . . . . 9
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ (𝑦 ∈ ran seq1(
+𝑒 , 𝐹)
↔ ∃𝑛 ∈
ℕ (seq1( +𝑒 , 𝐹)‘𝑛) = 𝑦)) |
132 | | eqcom 2744 |
. . . . . . . . . . 11
⊢
(Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) = 𝑦 ↔ 𝑦 = Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) |
133 | 9 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ (Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) = 𝑦 ↔ (seq1( +𝑒 , 𝐹)‘𝑛) = 𝑦)) |
134 | 132, 133 | bitr3id 288 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ (𝑦 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ↔ (seq1( +𝑒 , 𝐹)‘𝑛) = 𝑦)) |
135 | 134 | rexbidva 3215 |
. . . . . . . . 9
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ (∃𝑛 ∈
ℕ 𝑦 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ↔ ∃𝑛 ∈ ℕ (seq1( +𝑒
, 𝐹)‘𝑛) = 𝑦)) |
136 | 131, 135 | bitr4d 285 |
. . . . . . . 8
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ (𝑦 ∈ ran seq1(
+𝑒 , 𝐹)
↔ ∃𝑛 ∈
ℕ 𝑦 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘))) |
137 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑦 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘)) → 𝑦 = Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) |
138 | 137 | breq2d 5065 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑦 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘)) → (𝑥 < 𝑦 ↔ 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
139 | 27, 136, 138 | rexxfr2d 5304 |
. . . . . . 7
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ (∃𝑦 ∈ ran
seq1( +𝑒 , 𝐹)𝑥 < 𝑦 ↔ ∃𝑛 ∈ ℕ 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
140 | 139 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → (∃𝑦 ∈ ran seq1(
+𝑒 , 𝐹)𝑥 < 𝑦 ↔ ∃𝑛 ∈ ℕ 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
141 | 129, 140 | mpbird 260 |
. . . . 5
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → ∃𝑦 ∈ ran seq1(
+𝑒 , 𝐹)𝑥 < 𝑦) |
142 | 141 | ex 416 |
. . . 4
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
→ (𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘) → ∃𝑦 ∈ ran seq1(
+𝑒 , 𝐹)𝑥 < 𝑦)) |
143 | 142 | ralrimiva 3105 |
. . 3
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ ∀𝑥 ∈
ℝ (𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘) → ∃𝑦 ∈ ran seq1(
+𝑒 , 𝐹)𝑥 < 𝑦)) |
144 | | supxr2 12904 |
. . 3
⊢ (((ran
seq1( +𝑒 , 𝐹) ⊆ ℝ* ∧
Σ*𝑘 ∈
ℕ(𝐹‘𝑘) ∈ ℝ*)
∧ (∀𝑥 ∈ ran
seq1( +𝑒 , 𝐹)𝑥 ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘) ∧ ∀𝑥 ∈ ℝ (𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘) → ∃𝑦 ∈ ran seq1( +𝑒 ,
𝐹)𝑥 < 𝑦))) → sup(ran seq1(
+𝑒 , 𝐹),
ℝ*, < ) = Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) |
145 | 32, 39, 60, 143, 144 | syl22anc 839 |
. 2
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ sup(ran seq1( +𝑒 , 𝐹), ℝ*, < ) =
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) |
146 | 145 | eqcomd 2743 |
1
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ Σ*𝑘
∈ ℕ(𝐹‘𝑘) = sup(ran seq1( +𝑒 ,
𝐹), ℝ*,
< )) |