| Step |
Hyp |
Ref |
Expression |
| 1 |
|
esumfsup.1 |
⊢ Ⅎ 𝑘 𝐹 |
| 2 |
|
1z |
⊢ 1 ∈ ℤ |
| 3 |
|
seqfn |
⊢ ( 1 ∈ ℤ → seq 1 ( +e , 𝐹 ) Fn ( ℤ≥ ‘ 1 ) ) |
| 4 |
2 3
|
ax-mp |
⊢ seq 1 ( +e , 𝐹 ) Fn ( ℤ≥ ‘ 1 ) |
| 5 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
| 6 |
5
|
fneq2i |
⊢ ( seq 1 ( +e , 𝐹 ) Fn ℕ ↔ seq 1 ( +e , 𝐹 ) Fn ( ℤ≥ ‘ 1 ) ) |
| 7 |
4 6
|
mpbir |
⊢ seq 1 ( +e , 𝐹 ) Fn ℕ |
| 8 |
|
iccssxr |
⊢ ( 0 [,] +∞ ) ⊆ ℝ* |
| 9 |
1
|
esumfzf |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +e , 𝐹 ) ‘ 𝑛 ) ) |
| 10 |
|
ovex |
⊢ ( 1 ... 𝑛 ) ∈ V |
| 11 |
|
nfcv |
⊢ Ⅎ 𝑘 ℕ |
| 12 |
|
nfcv |
⊢ Ⅎ 𝑘 ( 0 [,] +∞ ) |
| 13 |
1 11 12
|
nff |
⊢ Ⅎ 𝑘 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) |
| 14 |
|
nfv |
⊢ Ⅎ 𝑘 𝑛 ∈ ℕ |
| 15 |
13 14
|
nfan |
⊢ Ⅎ 𝑘 ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) |
| 16 |
|
simpll |
⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) |
| 17 |
|
1nn |
⊢ 1 ∈ ℕ |
| 18 |
|
fzssnn |
⊢ ( 1 ∈ ℕ → ( 1 ... 𝑛 ) ⊆ ℕ ) |
| 19 |
17 18
|
mp1i |
⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 1 ... 𝑛 ) ⊆ ℕ ) |
| 20 |
|
simpr |
⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ( 1 ... 𝑛 ) ) |
| 21 |
19 20
|
sseldd |
⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ℕ ) |
| 22 |
16 21
|
ffvelcdmd |
⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) |
| 23 |
22
|
ex |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑘 ∈ ( 1 ... 𝑛 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) ) |
| 24 |
15 23
|
ralrimi |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) |
| 25 |
|
nfcv |
⊢ Ⅎ 𝑘 ( 1 ... 𝑛 ) |
| 26 |
25
|
esumcl |
⊢ ( ( ( 1 ... 𝑛 ) ∈ V ∧ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) |
| 27 |
10 24 26
|
sylancr |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) |
| 28 |
9 27
|
eqeltrrd |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( +e , 𝐹 ) ‘ 𝑛 ) ∈ ( 0 [,] +∞ ) ) |
| 29 |
8 28
|
sselid |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( +e , 𝐹 ) ‘ 𝑛 ) ∈ ℝ* ) |
| 30 |
29
|
ralrimiva |
⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ∀ 𝑛 ∈ ℕ ( seq 1 ( +e , 𝐹 ) ‘ 𝑛 ) ∈ ℝ* ) |
| 31 |
|
fnfvrnss |
⊢ ( ( seq 1 ( +e , 𝐹 ) Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( seq 1 ( +e , 𝐹 ) ‘ 𝑛 ) ∈ ℝ* ) → ran seq 1 ( +e , 𝐹 ) ⊆ ℝ* ) |
| 32 |
7 30 31
|
sylancr |
⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ran seq 1 ( +e , 𝐹 ) ⊆ ℝ* ) |
| 33 |
|
nnex |
⊢ ℕ ∈ V |
| 34 |
|
ffvelcdm |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) |
| 35 |
34
|
ex |
⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ( 𝑘 ∈ ℕ → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) ) |
| 36 |
13 35
|
ralrimi |
⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ∀ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) |
| 37 |
11
|
esumcl |
⊢ ( ( ℕ ∈ V ∧ ∀ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) |
| 38 |
33 36 37
|
sylancr |
⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) |
| 39 |
8 38
|
sselid |
⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∈ ℝ* ) |
| 40 |
|
fvelrnb |
⊢ ( seq 1 ( +e , 𝐹 ) Fn ℕ → ( 𝑥 ∈ ran seq 1 ( +e , 𝐹 ) ↔ ∃ 𝑛 ∈ ℕ ( seq 1 ( +e , 𝐹 ) ‘ 𝑛 ) = 𝑥 ) ) |
| 41 |
7 40
|
mp1i |
⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ( 𝑥 ∈ ran seq 1 ( +e , 𝐹 ) ↔ ∃ 𝑛 ∈ ℕ ( seq 1 ( +e , 𝐹 ) ‘ 𝑛 ) = 𝑥 ) ) |
| 42 |
|
eqcom |
⊢ ( Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = 𝑥 ↔ 𝑥 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) |
| 43 |
9
|
eqeq1d |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ( Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = 𝑥 ↔ ( seq 1 ( +e , 𝐹 ) ‘ 𝑛 ) = 𝑥 ) ) |
| 44 |
42 43
|
bitr3id |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ↔ ( seq 1 ( +e , 𝐹 ) ‘ 𝑛 ) = 𝑥 ) ) |
| 45 |
44
|
rexbidva |
⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ( ∃ 𝑛 ∈ ℕ 𝑥 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ↔ ∃ 𝑛 ∈ ℕ ( seq 1 ( +e , 𝐹 ) ‘ 𝑛 ) = 𝑥 ) ) |
| 46 |
41 45
|
bitr4d |
⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ( 𝑥 ∈ ran seq 1 ( +e , 𝐹 ) ↔ ∃ 𝑛 ∈ ℕ 𝑥 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) |
| 47 |
46
|
biimpa |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ran seq 1 ( +e , 𝐹 ) ) → ∃ 𝑛 ∈ ℕ 𝑥 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) |
| 48 |
33
|
a1i |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ℕ ∈ V ) |
| 49 |
34
|
adantlr |
⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) |
| 50 |
17 18
|
mp1i |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ⊆ ℕ ) |
| 51 |
15 48 49 50
|
esummono |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) |
| 52 |
51
|
ralrimiva |
⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ∀ 𝑛 ∈ ℕ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) |
| 53 |
52
|
adantr |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ran seq 1 ( +e , 𝐹 ) ) → ∀ 𝑛 ∈ ℕ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) |
| 54 |
47 53
|
jca |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ran seq 1 ( +e , 𝐹 ) ) → ( ∃ 𝑛 ∈ ℕ 𝑥 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∧ ∀ 𝑛 ∈ ℕ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ) |
| 55 |
|
r19.29r |
⊢ ( ( ∃ 𝑛 ∈ ℕ 𝑥 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∧ ∀ 𝑛 ∈ ℕ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) → ∃ 𝑛 ∈ ℕ ( 𝑥 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∧ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ) |
| 56 |
|
breq1 |
⊢ ( 𝑥 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) → ( 𝑥 ≤ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ↔ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ) |
| 57 |
56
|
biimpar |
⊢ ( ( 𝑥 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∧ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) → 𝑥 ≤ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) |
| 58 |
57
|
rexlimivw |
⊢ ( ∃ 𝑛 ∈ ℕ ( 𝑥 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∧ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) → 𝑥 ≤ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) |
| 59 |
54 55 58
|
3syl |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ran seq 1 ( +e , 𝐹 ) ) → 𝑥 ≤ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) |
| 60 |
59
|
ralrimiva |
⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ∀ 𝑥 ∈ ran seq 1 ( +e , 𝐹 ) 𝑥 ≤ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) |
| 61 |
|
nfv |
⊢ Ⅎ 𝑘 𝑥 ∈ ℝ |
| 62 |
13 61
|
nfan |
⊢ Ⅎ 𝑘 ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) |
| 63 |
|
nfcv |
⊢ Ⅎ 𝑘 𝑥 |
| 64 |
|
nfcv |
⊢ Ⅎ 𝑘 < |
| 65 |
11
|
nfesum1 |
⊢ Ⅎ 𝑘 Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) |
| 66 |
63 64 65
|
nfbr |
⊢ Ⅎ 𝑘 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) |
| 67 |
62 66
|
nfan |
⊢ Ⅎ 𝑘 ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) |
| 68 |
33
|
a1i |
⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) → ℕ ∈ V ) |
| 69 |
|
simplll |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑘 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) |
| 70 |
69 34
|
sylancom |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) |
| 71 |
|
simplr |
⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) → 𝑥 ∈ ℝ ) |
| 72 |
71
|
rexrd |
⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) → 𝑥 ∈ ℝ* ) |
| 73 |
|
simpr |
⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) → 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) |
| 74 |
67 68 70 72 73
|
esumlub |
⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) → ∃ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑥 < Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ) |
| 75 |
|
ssnnssfz |
⊢ ( 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) → ∃ 𝑛 ∈ ℕ 𝑎 ⊆ ( 1 ... 𝑛 ) ) |
| 76 |
|
r19.42v |
⊢ ( ∃ 𝑛 ∈ ℕ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ⊆ ( 1 ... 𝑛 ) ) ↔ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ ∃ 𝑛 ∈ ℕ 𝑎 ⊆ ( 1 ... 𝑛 ) ) ) |
| 77 |
|
nfv |
⊢ Ⅎ 𝑘 𝑎 ⊆ ( 1 ... 𝑛 ) |
| 78 |
67 77
|
nfan |
⊢ Ⅎ 𝑘 ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ⊆ ( 1 ... 𝑛 ) ) |
| 79 |
10
|
a1i |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ⊆ ( 1 ... 𝑛 ) ) → ( 1 ... 𝑛 ) ∈ V ) |
| 80 |
|
simp-4l |
⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ⊆ ( 1 ... 𝑛 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) |
| 81 |
17 18
|
ax-mp |
⊢ ( 1 ... 𝑛 ) ⊆ ℕ |
| 82 |
|
simpr |
⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ⊆ ( 1 ... 𝑛 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ( 1 ... 𝑛 ) ) |
| 83 |
81 82
|
sselid |
⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ⊆ ( 1 ... 𝑛 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ℕ ) |
| 84 |
80 83
|
ffvelcdmd |
⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ⊆ ( 1 ... 𝑛 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) |
| 85 |
|
simpr |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ⊆ ( 1 ... 𝑛 ) ) → 𝑎 ⊆ ( 1 ... 𝑛 ) ) |
| 86 |
78 79 84 85
|
esummono |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ⊆ ( 1 ... 𝑛 ) ) → Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) |
| 87 |
86
|
reximi |
⊢ ( ∃ 𝑛 ∈ ℕ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ⊆ ( 1 ... 𝑛 ) ) → ∃ 𝑛 ∈ ℕ Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) |
| 88 |
76 87
|
sylbir |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ ∃ 𝑛 ∈ ℕ 𝑎 ⊆ ( 1 ... 𝑛 ) ) → ∃ 𝑛 ∈ ℕ Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) |
| 89 |
75 88
|
sylan2 |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ∃ 𝑛 ∈ ℕ Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) |
| 90 |
89
|
ralrimiva |
⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) → ∀ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ∃ 𝑛 ∈ ℕ Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) |
| 91 |
|
r19.29r |
⊢ ( ( ∃ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑥 < Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ∧ ∀ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ∃ 𝑛 ∈ ℕ Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) → ∃ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ( 𝑥 < Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ∧ ∃ 𝑛 ∈ ℕ Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) |
| 92 |
|
r19.42v |
⊢ ( ∃ 𝑛 ∈ ℕ ( 𝑥 < Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ∧ Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ↔ ( 𝑥 < Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ∧ ∃ 𝑛 ∈ ℕ Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) |
| 93 |
92
|
rexbii |
⊢ ( ∃ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ∃ 𝑛 ∈ ℕ ( 𝑥 < Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ∧ Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ↔ ∃ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ( 𝑥 < Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ∧ ∃ 𝑛 ∈ ℕ Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) |
| 94 |
91 93
|
sylibr |
⊢ ( ( ∃ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑥 < Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ∧ ∀ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ∃ 𝑛 ∈ ℕ Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) → ∃ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ∃ 𝑛 ∈ ℕ ( 𝑥 < Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ∧ Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) |
| 95 |
74 90 94
|
syl2anc |
⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) → ∃ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ∃ 𝑛 ∈ ℕ ( 𝑥 < Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ∧ Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) |
| 96 |
|
simp-4r |
⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ ℝ ) |
| 97 |
96
|
rexrd |
⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ ℝ* ) |
| 98 |
|
vex |
⊢ 𝑎 ∈ V |
| 99 |
|
nfcv |
⊢ Ⅎ 𝑘 𝑎 |
| 100 |
99
|
nfel1 |
⊢ Ⅎ 𝑘 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) |
| 101 |
67 100
|
nfan |
⊢ Ⅎ 𝑘 ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) |
| 102 |
101 14
|
nfan |
⊢ Ⅎ 𝑘 ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) |
| 103 |
|
simp-5l |
⊢ ( ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑎 ) → 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) |
| 104 |
|
simpllr |
⊢ ( ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑎 ) → 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) |
| 105 |
|
inss1 |
⊢ ( 𝒫 ℕ ∩ Fin ) ⊆ 𝒫 ℕ |
| 106 |
105
|
sseli |
⊢ ( 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) → 𝑎 ∈ 𝒫 ℕ ) |
| 107 |
|
elpwi |
⊢ ( 𝑎 ∈ 𝒫 ℕ → 𝑎 ⊆ ℕ ) |
| 108 |
104 106 107
|
3syl |
⊢ ( ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑎 ) → 𝑎 ⊆ ℕ ) |
| 109 |
|
simpr |
⊢ ( ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑎 ) → 𝑘 ∈ 𝑎 ) |
| 110 |
108 109
|
sseldd |
⊢ ( ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑎 ) → 𝑘 ∈ ℕ ) |
| 111 |
103 110
|
ffvelcdmd |
⊢ ( ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑎 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) |
| 112 |
111
|
ex |
⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑘 ∈ 𝑎 → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) ) |
| 113 |
102 112
|
ralrimi |
⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) → ∀ 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) |
| 114 |
99
|
esumcl |
⊢ ( ( 𝑎 ∈ V ∧ ∀ 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) |
| 115 |
98 113 114
|
sylancr |
⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) |
| 116 |
8 115
|
sselid |
⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ∈ ℝ* ) |
| 117 |
|
simp-5l |
⊢ ( ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ) |
| 118 |
|
simpr |
⊢ ( ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ( 1 ... 𝑛 ) ) |
| 119 |
81 118
|
sselid |
⊢ ( ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ℕ ) |
| 120 |
117 119
|
ffvelcdmd |
⊢ ( ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) |
| 121 |
120
|
ex |
⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑘 ∈ ( 1 ... 𝑛 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) ) |
| 122 |
102 121
|
ralrimi |
⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) → ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) |
| 123 |
10 122 26
|
sylancr |
⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) ) |
| 124 |
8 123
|
sselid |
⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ* ) |
| 125 |
|
xrltletr |
⊢ ( ( 𝑥 ∈ ℝ* ∧ Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ∈ ℝ* ∧ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ* ) → ( ( 𝑥 < Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ∧ Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) → 𝑥 < Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) |
| 126 |
97 116 124 125
|
syl3anc |
⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑥 < Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ∧ Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) → 𝑥 < Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) |
| 127 |
126
|
reximdva |
⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( ∃ 𝑛 ∈ ℕ ( 𝑥 < Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ∧ Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) → ∃ 𝑛 ∈ ℕ 𝑥 < Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) |
| 128 |
127
|
rexlimdva |
⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) → ( ∃ 𝑎 ∈ ( 𝒫 ℕ ∩ Fin ) ∃ 𝑛 ∈ ℕ ( 𝑥 < Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ∧ Σ* 𝑘 ∈ 𝑎 ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) → ∃ 𝑛 ∈ ℕ 𝑥 < Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) |
| 129 |
95 128
|
mpd |
⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) → ∃ 𝑛 ∈ ℕ 𝑥 < Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) |
| 130 |
|
fvelrnb |
⊢ ( seq 1 ( +e , 𝐹 ) Fn ℕ → ( 𝑦 ∈ ran seq 1 ( +e , 𝐹 ) ↔ ∃ 𝑛 ∈ ℕ ( seq 1 ( +e , 𝐹 ) ‘ 𝑛 ) = 𝑦 ) ) |
| 131 |
7 130
|
mp1i |
⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ( 𝑦 ∈ ran seq 1 ( +e , 𝐹 ) ↔ ∃ 𝑛 ∈ ℕ ( seq 1 ( +e , 𝐹 ) ‘ 𝑛 ) = 𝑦 ) ) |
| 132 |
|
eqcom |
⊢ ( Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = 𝑦 ↔ 𝑦 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) |
| 133 |
9
|
eqeq1d |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ( Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = 𝑦 ↔ ( seq 1 ( +e , 𝐹 ) ‘ 𝑛 ) = 𝑦 ) ) |
| 134 |
132 133
|
bitr3id |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑦 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ↔ ( seq 1 ( +e , 𝐹 ) ‘ 𝑛 ) = 𝑦 ) ) |
| 135 |
134
|
rexbidva |
⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ( ∃ 𝑛 ∈ ℕ 𝑦 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ↔ ∃ 𝑛 ∈ ℕ ( seq 1 ( +e , 𝐹 ) ‘ 𝑛 ) = 𝑦 ) ) |
| 136 |
131 135
|
bitr4d |
⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ( 𝑦 ∈ ran seq 1 ( +e , 𝐹 ) ↔ ∃ 𝑛 ∈ ℕ 𝑦 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) |
| 137 |
|
simpr |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑦 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) → 𝑦 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) |
| 138 |
137
|
breq2d |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑦 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) → ( 𝑥 < 𝑦 ↔ 𝑥 < Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) |
| 139 |
27 136 138
|
rexxfr2d |
⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ( ∃ 𝑦 ∈ ran seq 1 ( +e , 𝐹 ) 𝑥 < 𝑦 ↔ ∃ 𝑛 ∈ ℕ 𝑥 < Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) |
| 140 |
139
|
ad2antrr |
⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) → ( ∃ 𝑦 ∈ ran seq 1 ( +e , 𝐹 ) 𝑥 < 𝑦 ↔ ∃ 𝑛 ∈ ℕ 𝑥 < Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) |
| 141 |
129 140
|
mpbird |
⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) → ∃ 𝑦 ∈ ran seq 1 ( +e , 𝐹 ) 𝑥 < 𝑦 ) |
| 142 |
141
|
ex |
⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) → ∃ 𝑦 ∈ ran seq 1 ( +e , 𝐹 ) 𝑥 < 𝑦 ) ) |
| 143 |
142
|
ralrimiva |
⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ∀ 𝑥 ∈ ℝ ( 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) → ∃ 𝑦 ∈ ran seq 1 ( +e , 𝐹 ) 𝑥 < 𝑦 ) ) |
| 144 |
|
supxr2 |
⊢ ( ( ( ran seq 1 ( +e , 𝐹 ) ⊆ ℝ* ∧ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∈ ℝ* ) ∧ ( ∀ 𝑥 ∈ ran seq 1 ( +e , 𝐹 ) 𝑥 ≤ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) → ∃ 𝑦 ∈ ran seq 1 ( +e , 𝐹 ) 𝑥 < 𝑦 ) ) ) → sup ( ran seq 1 ( +e , 𝐹 ) , ℝ* , < ) = Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) |
| 145 |
32 39 60 143 144
|
syl22anc |
⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → sup ( ran seq 1 ( +e , 𝐹 ) , ℝ* , < ) = Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) |
| 146 |
145
|
eqcomd |
⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = sup ( ran seq 1 ( +e , 𝐹 ) , ℝ* , < ) ) |