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 ffvelrnd ( ( ( 𝐹 : ℕ ⟶ ( 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 ffvelrn ( ( 𝐹 : ℕ ⟶ ( 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 ffvelrnd ( ( ( ( ( 𝐹 : ℕ ⟶ ( 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 ffvelrnd ( ( ( ( ( ( 𝐹 : ℕ ⟶ ( 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 ffvelrnd ( ( ( ( ( ( 𝐹 : ℕ ⟶ ( 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 ( +𝑒 , 𝐹 ) , ℝ* , < ) )