| Step | Hyp | Ref
| Expression |
| 1 | | 1z 12647 |
. . . . . 6
⊢ 1 ∈
ℤ |
| 2 | | seqfn 14054 |
. . . . . 6
⊢ (1 ∈
ℤ → seq1( +𝑒 , 𝐹) Fn
(ℤ≥‘1)) |
| 3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢ seq1(
+𝑒 , 𝐹)
Fn (ℤ≥‘1) |
| 4 | | nnuz 12921 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
| 5 | 4 | fneq2i 6666 |
. . . . 5
⊢ (seq1(
+𝑒 , 𝐹)
Fn ℕ ↔ seq1( +𝑒 , 𝐹) Fn
(ℤ≥‘1)) |
| 6 | 3, 5 | mpbir 231 |
. . . 4
⊢ seq1(
+𝑒 , 𝐹)
Fn ℕ |
| 7 | | iccssxr 13470 |
. . . . . 6
⊢
(0[,]+∞) ⊆ ℝ* |
| 8 | | esumfsup.1 |
. . . . . . . 8
⊢
Ⅎ𝑘𝐹 |
| 9 | 8 | esumfzf 34070 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ Σ*𝑘
∈ (1...𝑛)(𝐹‘𝑘) = (seq1( +𝑒 , 𝐹)‘𝑛)) |
| 10 | | ovex 7464 |
. . . . . . . 8
⊢
(1...𝑛) ∈
V |
| 11 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘ℕ |
| 12 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(0[,]+∞) |
| 13 | 8, 11, 12 | nff 6732 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 𝐹:ℕ⟶(0[,]+∞) |
| 14 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 𝑛 ∈ ℕ |
| 15 | 13, 14 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈
ℕ) |
| 16 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ 𝑘 ∈ (1...𝑛)) → 𝐹:ℕ⟶(0[,]+∞)) |
| 17 | | 1nn 12277 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℕ |
| 18 | | fzssnn 13608 |
. . . . . . . . . . . . 13
⊢ (1 ∈
ℕ → (1...𝑛)
⊆ ℕ) |
| 19 | 17, 18 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ 𝑘 ∈ (1...𝑛)) → (1...𝑛) ⊆
ℕ) |
| 20 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...𝑛)) |
| 21 | 19, 20 | sseldd 3984 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
| 22 | 16, 21 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
∧ 𝑘 ∈ (1...𝑛)) → (𝐹‘𝑘) ∈ (0[,]+∞)) |
| 23 | 22 | ex 412 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ (𝑘 ∈ (1...𝑛) → (𝐹‘𝑘) ∈ (0[,]+∞))) |
| 24 | 15, 23 | ralrimi 3257 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ ∀𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ∈ (0[,]+∞)) |
| 25 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑘(1...𝑛) |
| 26 | 25 | esumcl 34031 |
. . . . . . . 8
⊢
(((1...𝑛) ∈ V
∧ ∀𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ∈ (0[,]+∞)) →
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ∈ (0[,]+∞)) |
| 27 | 10, 24, 26 | sylancr 587 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ Σ*𝑘
∈ (1...𝑛)(𝐹‘𝑘) ∈ (0[,]+∞)) |
| 28 | 9, 27 | eqeltrrd 2842 |
. . . . . 6
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ (seq1( +𝑒 , 𝐹)‘𝑛) ∈ (0[,]+∞)) |
| 29 | 7, 28 | sselid 3981 |
. . . . 5
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ (seq1( +𝑒 , 𝐹)‘𝑛) ∈
ℝ*) |
| 30 | 29 | ralrimiva 3146 |
. . . 4
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ ∀𝑛 ∈
ℕ (seq1( +𝑒 , 𝐹)‘𝑛) ∈
ℝ*) |
| 31 | | fnfvrnss 7141 |
. . . 4
⊢ ((seq1(
+𝑒 , 𝐹)
Fn ℕ ∧ ∀𝑛
∈ ℕ (seq1( +𝑒 , 𝐹)‘𝑛) ∈ ℝ*) → ran
seq1( +𝑒 , 𝐹) ⊆
ℝ*) |
| 32 | 6, 30, 31 | sylancr 587 |
. . 3
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ ran seq1( +𝑒 , 𝐹) ⊆
ℝ*) |
| 33 | | nnex 12272 |
. . . . 5
⊢ ℕ
∈ V |
| 34 | | ffvelcdm 7101 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑘 ∈ ℕ)
→ (𝐹‘𝑘) ∈
(0[,]+∞)) |
| 35 | 34 | ex 412 |
. . . . . 6
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ (𝑘 ∈ ℕ
→ (𝐹‘𝑘) ∈
(0[,]+∞))) |
| 36 | 13, 35 | ralrimi 3257 |
. . . . 5
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ ∀𝑘 ∈
ℕ (𝐹‘𝑘) ∈
(0[,]+∞)) |
| 37 | 11 | esumcl 34031 |
. . . . 5
⊢ ((ℕ
∈ V ∧ ∀𝑘
∈ ℕ (𝐹‘𝑘) ∈ (0[,]+∞)) →
Σ*𝑘 ∈
ℕ(𝐹‘𝑘) ∈
(0[,]+∞)) |
| 38 | 33, 36, 37 | sylancr 587 |
. . . 4
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ Σ*𝑘
∈ ℕ(𝐹‘𝑘) ∈ (0[,]+∞)) |
| 39 | 7, 38 | sselid 3981 |
. . 3
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ Σ*𝑘
∈ ℕ(𝐹‘𝑘) ∈
ℝ*) |
| 40 | | fvelrnb 6969 |
. . . . . . . . 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 285 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ (𝑥 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ↔ (seq1( +𝑒 , 𝐹)‘𝑛) = 𝑥)) |
| 45 | 44 | rexbidva 3177 |
. . . . . . . 8
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ (∃𝑛 ∈
ℕ 𝑥 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ↔ ∃𝑛 ∈ ℕ (seq1( +𝑒
, 𝐹)‘𝑛) = 𝑥)) |
| 46 | 41, 45 | bitr4d 282 |
. . . . . . 7
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ (𝑥 ∈ ran seq1(
+𝑒 , 𝐹)
↔ ∃𝑛 ∈
ℕ 𝑥 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘))) |
| 47 | 46 | biimpa 476 |
. . . . . 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 34055 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ Σ*𝑘
∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) |
| 52 | 51 | ralrimiva 3146 |
. . . . . . 7
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ ∀𝑛 ∈
ℕ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) |
| 53 | 52 | adantr 480 |
. . . . . 6
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ran seq1(
+𝑒 , 𝐹))
→ ∀𝑛 ∈
ℕ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) |
| 54 | 47, 53 | jca 511 |
. . . . 5
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ran seq1(
+𝑒 , 𝐹))
→ (∃𝑛 ∈
ℕ 𝑥 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ∧ ∀𝑛 ∈ ℕ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘))) |
| 55 | | r19.29r 3116 |
. . . . 5
⊢
((∃𝑛 ∈
ℕ 𝑥 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ∧ ∀𝑛 ∈ ℕ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) → ∃𝑛 ∈ ℕ (𝑥 = Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ∧ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘))) |
| 56 | | breq1 5146 |
. . . . . . 7
⊢ (𝑥 = Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) → (𝑥 ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘) ↔ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘))) |
| 57 | 56 | biimpar 477 |
. . . . . 6
⊢ ((𝑥 = Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ∧ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) → 𝑥 ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) |
| 58 | 57 | rexlimivw 3151 |
. . . . 5
⊢
(∃𝑛 ∈
ℕ (𝑥 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ∧ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) → 𝑥 ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) |
| 59 | 54, 55, 58 | 3syl 18 |
. . . 4
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ran seq1(
+𝑒 , 𝐹))
→ 𝑥 ≤
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) |
| 60 | 59 | ralrimiva 3146 |
. . 3
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ ∀𝑥 ∈ ran
seq1( +𝑒 , 𝐹)𝑥 ≤ Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) |
| 61 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘 𝑥 ∈ ℝ |
| 62 | 13, 61 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈
ℝ) |
| 63 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘𝑥 |
| 64 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘
< |
| 65 | 11 | nfesum1 34041 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘Σ*𝑘 ∈ ℕ(𝐹‘𝑘) |
| 66 | 63, 64, 65 | nfbr 5190 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘) |
| 67 | 62, 66 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑘((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) |
| 68 | 33 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → ℕ ∈
V) |
| 69 | | simplll 775 |
. . . . . . . . . 10
⊢ ((((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶(0[,]+∞)) |
| 70 | 69, 34 | sylancom 588 |
. . . . . . . . 9
⊢ ((((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ (0[,]+∞)) |
| 71 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → 𝑥 ∈ ℝ) |
| 72 | 71 | rexrd 11311 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → 𝑥 ∈ ℝ*) |
| 73 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) |
| 74 | 67, 68, 70, 72, 73 | esumlub 34061 |
. . . . . . . 8
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → ∃𝑎 ∈ (𝒫 ℕ ∩
Fin)𝑥 <
Σ*𝑘 ∈
𝑎(𝐹‘𝑘)) |
| 75 | | ssnnssfz 32789 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (𝒫 ℕ ∩
Fin) → ∃𝑛 ∈
ℕ 𝑎 ⊆
(1...𝑛)) |
| 76 | | r19.42v 3191 |
. . . . . . . . . . 11
⊢
(∃𝑛 ∈
ℕ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) ↔ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ ∃𝑛 ∈ ℕ 𝑎 ⊆ (1...𝑛))) |
| 77 | | nfv 1914 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘 𝑎 ⊆ (1...𝑛) |
| 78 | 67, 77 | nfan 1899 |
. . . . . . . . . . . . 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 484 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...𝑛)) |
| 83 | 81, 82 | sselid 3981 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
| 84 | 80, 83 | ffvelcdmd 7105 |
. . . . . . . . . . . . 13
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) ∧ 𝑘 ∈ (1...𝑛)) → (𝐹‘𝑘) ∈ (0[,]+∞)) |
| 85 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) → 𝑎 ⊆ (1...𝑛)) |
| 86 | 78, 79, 84, 85 | esummono 34055 |
. . . . . . . . . . . 12
⊢ ((((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) → Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) |
| 87 | 86 | reximi 3084 |
. . . . . . . . . . 11
⊢
(∃𝑛 ∈
ℕ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) → ∃𝑛 ∈ ℕ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) |
| 88 | 76, 87 | sylbir 235 |
. . . . . . . . . 10
⊢ ((((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ ∃𝑛 ∈ ℕ 𝑎 ⊆ (1...𝑛)) → ∃𝑛 ∈ ℕ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) |
| 89 | 75, 88 | sylan2 593 |
. . . . . . . . 9
⊢ ((((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) →
∃𝑛 ∈ ℕ
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) |
| 90 | 89 | ralrimiva 3146 |
. . . . . . . 8
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → ∀𝑎 ∈ (𝒫 ℕ ∩
Fin)∃𝑛 ∈ ℕ
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) |
| 91 | | r19.29r 3116 |
. . . . . . . . 9
⊢
((∃𝑎 ∈
(𝒫 ℕ ∩ Fin)𝑥 < Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ ∀𝑎 ∈ (𝒫 ℕ ∩
Fin)∃𝑛 ∈ ℕ
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → ∃𝑎 ∈ (𝒫 ℕ ∩ Fin)(𝑥 < Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ ∃𝑛 ∈ ℕ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
| 92 | | r19.42v 3191 |
. . . . . . . . . 10
⊢
(∃𝑛 ∈
ℕ (𝑥 <
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ∧ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) ↔ (𝑥 < Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ ∃𝑛 ∈ ℕ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
| 93 | 92 | rexbii 3094 |
. . . . . . . . 9
⊢
(∃𝑎 ∈
(𝒫 ℕ ∩ Fin)∃𝑛 ∈ ℕ (𝑥 < Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) ↔ ∃𝑎 ∈ (𝒫 ℕ ∩ Fin)(𝑥 < Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ ∃𝑛 ∈ ℕ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
| 94 | 91, 93 | sylibr 234 |
. . . . . . . 8
⊢
((∃𝑎 ∈
(𝒫 ℕ ∩ Fin)𝑥 < Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ ∀𝑎 ∈ (𝒫 ℕ ∩
Fin)∃𝑛 ∈ ℕ
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → ∃𝑎 ∈ (𝒫 ℕ ∩
Fin)∃𝑛 ∈ ℕ
(𝑥 <
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ∧ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
| 95 | 74, 90, 94 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → ∃𝑎 ∈ (𝒫 ℕ ∩
Fin)∃𝑛 ∈ ℕ
(𝑥 <
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ∧ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
| 96 | | simp-4r 784 |
. . . . . . . . . . 11
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
𝑥 ∈
ℝ) |
| 97 | 96 | rexrd 11311 |
. . . . . . . . . 10
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
𝑥 ∈
ℝ*) |
| 98 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑎 ∈ V |
| 99 | | nfcv 2905 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘𝑎 |
| 100 | 99 | nfel1 2922 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘 𝑎 ∈ (𝒫 ℕ ∩
Fin) |
| 101 | 67, 100 | nfan 1899 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘(((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩
Fin)) |
| 102 | 101, 14 | nfan 1899 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘((((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈
ℕ) |
| 103 | | simp-5l 785 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ 𝑎) → 𝐹:ℕ⟶(0[,]+∞)) |
| 104 | | simpllr 776 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ 𝑎) → 𝑎 ∈ (𝒫 ℕ ∩
Fin)) |
| 105 | | inss1 4237 |
. . . . . . . . . . . . . . . . . 18
⊢
(𝒫 ℕ ∩ Fin) ⊆ 𝒫 ℕ |
| 106 | 105 | sseli 3979 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ (𝒫 ℕ ∩
Fin) → 𝑎 ∈
𝒫 ℕ) |
| 107 | | elpwi 4607 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ 𝒫 ℕ →
𝑎 ⊆
ℕ) |
| 108 | 104, 106,
107 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ 𝑎) → 𝑎 ⊆ ℕ) |
| 109 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ 𝑎) → 𝑘 ∈ 𝑎) |
| 110 | 108, 109 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ 𝑎) → 𝑘 ∈ ℕ) |
| 111 | 103, 110 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ 𝑎) → (𝐹‘𝑘) ∈ (0[,]+∞)) |
| 112 | 111 | ex 412 |
. . . . . . . . . . . . 13
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
(𝑘 ∈ 𝑎 → (𝐹‘𝑘) ∈ (0[,]+∞))) |
| 113 | 102, 112 | ralrimi 3257 |
. . . . . . . . . . . 12
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
∀𝑘 ∈ 𝑎 (𝐹‘𝑘) ∈ (0[,]+∞)) |
| 114 | 99 | esumcl 34031 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ V ∧ ∀𝑘 ∈ 𝑎 (𝐹‘𝑘) ∈ (0[,]+∞)) →
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ∈ (0[,]+∞)) |
| 115 | 98, 113, 114 | sylancr 587 |
. . . . . . . . . . 11
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ∈ (0[,]+∞)) |
| 116 | 7, 115 | sselid 3981 |
. . . . . . . . . 10
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ∈
ℝ*) |
| 117 | | simp-5l 785 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ (1...𝑛)) → 𝐹:ℕ⟶(0[,]+∞)) |
| 118 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...𝑛)) |
| 119 | 81, 118 | sselid 3981 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
| 120 | 117, 119 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢
((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈ (1...𝑛)) → (𝐹‘𝑘) ∈ (0[,]+∞)) |
| 121 | 120 | ex 412 |
. . . . . . . . . . . . 13
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
(𝑘 ∈ (1...𝑛) → (𝐹‘𝑘) ∈ (0[,]+∞))) |
| 122 | 102, 121 | ralrimi 3257 |
. . . . . . . . . . . 12
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
∀𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ∈ (0[,]+∞)) |
| 123 | 10, 122, 26 | sylancr 587 |
. . . . . . . . . . 11
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ∈ (0[,]+∞)) |
| 124 | 7, 123 | sselid 3981 |
. . . . . . . . . 10
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ∈
ℝ*) |
| 125 | | xrltletr 13199 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ*
∧ Σ*𝑘
∈ 𝑎(𝐹‘𝑘) ∈ ℝ* ∧
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ∈ ℝ*) → ((𝑥 < Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
| 126 | 97, 116, 124, 125 | syl3anc 1373 |
. . . . . . . . 9
⊢
(((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑛 ∈ ℕ) →
((𝑥 <
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ∧ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
| 127 | 126 | reximdva 3168 |
. . . . . . . 8
⊢ ((((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) →
(∃𝑛 ∈ ℕ
(𝑥 <
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ∧ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → ∃𝑛 ∈ ℕ 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
| 128 | 127 | rexlimdva 3155 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → (∃𝑎 ∈ (𝒫 ℕ ∩
Fin)∃𝑛 ∈ ℕ
(𝑥 <
Σ*𝑘 ∈
𝑎(𝐹‘𝑘) ∧ Σ*𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → ∃𝑛 ∈ ℕ 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
| 129 | 95, 128 | mpd 15 |
. . . . . 6
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → ∃𝑛 ∈ ℕ 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) |
| 130 | | fvelrnb 6969 |
. . . . . . . . . 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 285 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑛 ∈ ℕ)
→ (𝑦 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ↔ (seq1( +𝑒 , 𝐹)‘𝑛) = 𝑦)) |
| 135 | 134 | rexbidva 3177 |
. . . . . . . . 9
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ (∃𝑛 ∈
ℕ 𝑦 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘) ↔ ∃𝑛 ∈ ℕ (seq1( +𝑒
, 𝐹)‘𝑛) = 𝑦)) |
| 136 | 131, 135 | bitr4d 282 |
. . . . . . . 8
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ (𝑦 ∈ ran seq1(
+𝑒 , 𝐹)
↔ ∃𝑛 ∈
ℕ 𝑦 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘))) |
| 137 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑦 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘)) → 𝑦 = Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) |
| 138 | 137 | breq2d 5155 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑦 =
Σ*𝑘 ∈
(1...𝑛)(𝐹‘𝑘)) → (𝑥 < 𝑦 ↔ 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
| 139 | 27, 136, 138 | rexxfr2d 5411 |
. . . . . . 7
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ (∃𝑦 ∈ ran
seq1( +𝑒 , 𝐹)𝑥 < 𝑦 ↔ ∃𝑛 ∈ ℕ 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
| 140 | 139 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → (∃𝑦 ∈ ran seq1(
+𝑒 , 𝐹)𝑥 < 𝑦 ↔ ∃𝑛 ∈ ℕ 𝑥 < Σ*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))) |
| 141 | 129, 140 | mpbird 257 |
. . . . 5
⊢ (((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
∧ 𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘)) → ∃𝑦 ∈ ran seq1(
+𝑒 , 𝐹)𝑥 < 𝑦) |
| 142 | 141 | ex 412 |
. . . 4
⊢ ((𝐹:ℕ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
→ (𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘) → ∃𝑦 ∈ ran seq1(
+𝑒 , 𝐹)𝑥 < 𝑦)) |
| 143 | 142 | ralrimiva 3146 |
. . 3
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ ∀𝑥 ∈
ℝ (𝑥 <
Σ*𝑘 ∈
ℕ(𝐹‘𝑘) → ∃𝑦 ∈ ran seq1(
+𝑒 , 𝐹)𝑥 < 𝑦)) |
| 144 | | supxr2 13356 |
. . 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( +𝑒 ,
𝐹), ℝ*,
< )) |