Metamath Proof Explorer

Theorem esumfsup

Description: Formulating an extended sum over integers using the recursive sequence builder. (Contributed by Thierry Arnoux, 18-Oct-2017)

Ref Expression
Hypothesis esumfsup.1 ⊢ Ⅎ 𝑘 𝐹
Assertion esumfsup ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = sup ( ran seq 1 ( +𝑒 , 𝐹 ) , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 esumfsup.1 ⊢ Ⅎ 𝑘 𝐹
2 1z ⊢ 1 ∈ ℤ
3 seqfn ⊢ ( 1 ∈ ℤ → seq 1 ( +𝑒 , 𝐹 ) Fn ( ℤ≥ ‘ 1 ) )
4 2 3 ax-mp ⊢ seq 1 ( +𝑒 , 𝐹 ) Fn ( ℤ≥ ‘ 1 )
5 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
6 5 fneq2i ⊢ ( seq 1 ( +𝑒 , 𝐹 ) Fn ℕ ↔ seq 1 ( +𝑒 , 𝐹 ) Fn ( ℤ≥ ‘ 1 ) )
7 4 6 mpbir ⊢ seq 1 ( +𝑒 , 𝐹 ) Fn ℕ
8 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
9 1 esumfzf ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) )
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 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) ∈ ( 0 [,] +∞ ) )
29 8 28 sselid ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) ∈ ℝ* )
30 29 ralrimiva ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ∀ 𝑛 ∈ ℕ ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) ∈ ℝ* )
31 fnfvrnss ⊢ ( ( seq 1 ( +𝑒 , 𝐹 ) Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) ∈ ℝ* ) → ran seq 1 ( +𝑒 , 𝐹 ) ⊆ ℝ* )
32 7 30 31 sylancr ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ran seq 1 ( +𝑒 , 𝐹 ) ⊆ ℝ* )
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 ( +𝑒 , 𝐹 ) Fn ℕ → ( 𝑥 ∈ ran seq 1 ( +𝑒 , 𝐹 ) ↔ ∃ 𝑛 ∈ ℕ ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) = 𝑥 ) )
41 7 40 mp1i ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ( 𝑥 ∈ ran seq 1 ( +𝑒 , 𝐹 ) ↔ ∃ 𝑛 ∈ ℕ ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) = 𝑥 ) )
42 eqcom ⊢ ( Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = 𝑥 ↔ 𝑥 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) )
43 9 eqeq1d ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ( Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = 𝑥 ↔ ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) = 𝑥 ) )
44 42 43 bitr3id ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ↔ ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) = 𝑥 ) )
45 44 rexbidva ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ( ∃ 𝑛 ∈ ℕ 𝑥 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ↔ ∃ 𝑛 ∈ ℕ ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) = 𝑥 ) )
46 41 45 bitr4d ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ( 𝑥 ∈ ran seq 1 ( +𝑒 , 𝐹 ) ↔ ∃ 𝑛 ∈ ℕ 𝑥 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) )
47 46 biimpa ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ran seq 1 ( +𝑒 , 𝐹 ) ) → ∃ 𝑛 ∈ ℕ 𝑥 = Σ* 𝑘 ∈ ( 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 ( +𝑒 , 𝐹 ) ) → ∀ 𝑛 ∈ ℕ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ≤ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) )
54 47 53 jca ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ran seq 1 ( +𝑒 , 𝐹 ) ) → ( ∃ 𝑛 ∈ ℕ 𝑥 = Σ* 𝑘 ∈ ( 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 ( +𝑒 , 𝐹 ) ) → 𝑥 ≤ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) )
60 59 ralrimiva ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ∀ 𝑥 ∈ ran seq 1 ( +𝑒 , 𝐹 ) 𝑥 ≤ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) )
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 ( +𝑒 , 𝐹 ) Fn ℕ → ( 𝑦 ∈ ran seq 1 ( +𝑒 , 𝐹 ) ↔ ∃ 𝑛 ∈ ℕ ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) = 𝑦 ) )
131 7 130 mp1i ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ( 𝑦 ∈ ran seq 1 ( +𝑒 , 𝐹 ) ↔ ∃ 𝑛 ∈ ℕ ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) = 𝑦 ) )
132 eqcom ⊢ ( Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = 𝑦 ↔ 𝑦 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) )
133 9 eqeq1d ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ( Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) = 𝑦 ↔ ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) = 𝑦 ) )
134 132 133 bitr3id ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑦 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ↔ ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) = 𝑦 ) )
135 134 rexbidva ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ( ∃ 𝑛 ∈ ℕ 𝑦 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ↔ ∃ 𝑛 ∈ ℕ ( seq 1 ( +𝑒 , 𝐹 ) ‘ 𝑛 ) = 𝑦 ) )
136 131 135 bitr4d ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ( 𝑦 ∈ ran seq 1 ( +𝑒 , 𝐹 ) ↔ ∃ 𝑛 ∈ ℕ 𝑦 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) )
137 simpr ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑦 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) → 𝑦 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) )
138 137 breq2d ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑦 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) → ( 𝑥 < 𝑦 ↔ 𝑥 < Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) )
139 27 136 138 rexxfr2d ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ( ∃ 𝑦 ∈ ran seq 1 ( +𝑒 , 𝐹 ) 𝑥 < 𝑦 ↔ ∃ 𝑛 ∈ ℕ 𝑥 < Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) )
140 139 ad2antrr ⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) → ( ∃ 𝑦 ∈ ran seq 1 ( +𝑒 , 𝐹 ) 𝑥 < 𝑦 ↔ ∃ 𝑛 ∈ ℕ 𝑥 < Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) )
141 129 140 mpbird ⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) → ∃ 𝑦 ∈ ran seq 1 ( +𝑒 , 𝐹 ) 𝑥 < 𝑦 )
142 141 ex ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) → ∃ 𝑦 ∈ ran seq 1 ( +𝑒 , 𝐹 ) 𝑥 < 𝑦 ) )
143 142 ralrimiva ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → ∀ 𝑥 ∈ ℝ ( 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) → ∃ 𝑦 ∈ ran seq 1 ( +𝑒 , 𝐹 ) 𝑥 < 𝑦 ) )
144 supxr2 ⊢ ( ( ( ran seq 1 ( +𝑒 , 𝐹 ) ⊆ ℝ* ∧ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∈ ℝ* ) ∧ ( ∀ 𝑥 ∈ ran seq 1 ( +𝑒 , 𝐹 ) 𝑥 ≤ Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) → ∃ 𝑦 ∈ ran seq 1 ( +𝑒 , 𝐹 ) 𝑥 < 𝑦 ) ) ) → sup ( ran seq 1 ( +𝑒 , 𝐹 ) , ℝ* , < ) = Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) )
145 32 39 60 143 144 syl22anc ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → sup ( ran seq 1 ( +𝑒 , 𝐹 ) , ℝ* , < ) = Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) )
146 145 eqcomd ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) = sup ( ran seq 1 ( +𝑒 , 𝐹 ) , ℝ* , < ) )