esumfsup - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > esumfsup		Structured version Visualization version GIF version

Theorem esumfsup 34407

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

**Hypothesis**
Ref	Expression
esumfsup.1	⊢ Ⅎ𝑘𝐹

**Assertion**
Ref	Expression
esumfsup	⊢ (𝐹:ℕ⟶(0[,]+∞) → Σ^𝑘 ∈ ℕ(𝐹‘𝑘) = sup(ran seq1( +_𝑒 , 𝐹), ℝ^, < ))

Proof of Theorem esumfsup Dummy variables 𝑎 𝑛 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1z 12626	. . . . . 6 ⊢ 1 ∈ ℤ
2		seqfn 14051	. . . . . 6 ⊢ (1 ∈ ℤ → seq1( +_𝑒 , 𝐹) Fn (ℤ_≥‘1))
3	1, 2	ax-mp 5	. . . . 5 ⊢ seq1( +_𝑒 , 𝐹) Fn (ℤ_≥‘1)
4		nnuz 12903	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
5	4	fneq2i 6636	. . . . 5 ⊢ (seq1( +_𝑒 , 𝐹) Fn ℕ ↔ seq1( +_𝑒 , 𝐹) Fn (ℤ_≥‘1))
6	3, 5	mpbir 234	. . . 4 ⊢ seq1( +_𝑒 , 𝐹) Fn ℕ
7		iccssxr 13459	. . . . . 6 ⊢ (0[,]+∞) ⊆ ℝ^*
8		esumfsup.1	. . . . . . . 8 ⊢ Ⅎ𝑘𝐹
9	8	esumfzf 34406	. . . . . . 7 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) = (seq1( +_𝑒 , 𝐹)‘𝑛))
10		ovex 7446	. . . . . . . 8 ⊢ (1...𝑛) ∈ V
11		nfcv 2931	. . . . . . . . . . 11 ⊢ Ⅎ𝑘ℕ
12		nfcv 2931	. . . . . . . . . . 11 ⊢ Ⅎ𝑘(0[,]+∞)
13	8, 11, 12	nff 6704	. . . . . . . . . 10 ⊢ Ⅎ𝑘 𝐹:ℕ⟶(0[,]+∞)
14		nfv 1941	. . . . . . . . . 10 ⊢ Ⅎ𝑘 𝑛 ∈ ℕ
15	13, 14	nfan 1926	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ)
16		simpll 778	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐹:ℕ⟶(0[,]+∞))
17		1nn 12246	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ
18		fzssnn 13598	. . . . . . . . . . . . 13 ⊢ (1 ∈ ℕ → (1...𝑛) ⊆ ℕ)
19	17, 18	mp1i 14	. . . . . . . . . . . 12 ⊢ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1...𝑛) ⊆ ℕ)
20		simpr 489	. . . . . . . . . . . 12 ⊢ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...𝑛))
21	19, 20	sseldd 3946	. . . . . . . . . . 11 ⊢ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
22	16, 21	ffvelcdmd 7083	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐹‘𝑘) ∈ (0[,]+∞))
23	22	ex 417	. . . . . . . . 9 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ (1...𝑛) → (𝐹‘𝑘) ∈ (0[,]+∞)))
24	15, 23	ralrimi 3269	. . . . . . . 8 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ∈ (0[,]+∞))
25		nfcv 2931	. . . . . . . . 9 ⊢ Ⅎ𝑘(1...𝑛)
26	25	esumcl 34367	. . . . . . . 8 ⊢ (((1...𝑛) ∈ V ∧ ∀𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ∈ (0[,]+∞)) → Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ∈ (0[,]+∞))
27	10, 24, 26	sylancr 598	. . . . . . 7 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ∈ (0[,]+∞))
28	9, 27	eqeltrrd 2870	. . . . . 6 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (seq1( +_𝑒 , 𝐹)‘𝑛) ∈ (0[,]+∞))
29	7, 28	sselid 3943	. . . . 5 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (seq1( +_𝑒 , 𝐹)‘𝑛) ∈ ℝ^*)
30	29	ralrimiva 3163	. . . 4 ⊢ (𝐹:ℕ⟶(0[,]+∞) → ∀𝑛 ∈ ℕ (seq1( +_𝑒 , 𝐹)‘𝑛) ∈ ℝ^*)
31		fnfvrnss 7119	. . . 4 ⊢ ((seq1( +_𝑒 , 𝐹) Fn ℕ ∧ ∀𝑛 ∈ ℕ (seq1( +_𝑒 , 𝐹)‘𝑛) ∈ ℝ^) → ran seq1( +_𝑒 , 𝐹) ⊆ ℝ^)
32	6, 30, 31	sylancr 598	. . 3 ⊢ (𝐹:ℕ⟶(0[,]+∞) → ran seq1( +_𝑒 , 𝐹) ⊆ ℝ^*)
33		nnex 12241	. . . . 5 ⊢ ℕ ∈ V
34		ffvelcdm 7079	. . . . . . 7 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ (0[,]+∞))
35	34	ex 417	. . . . . 6 ⊢ (𝐹:ℕ⟶(0[,]+∞) → (𝑘 ∈ ℕ → (𝐹‘𝑘) ∈ (0[,]+∞)))
36	13, 35	ralrimi 3269	. . . . 5 ⊢ (𝐹:ℕ⟶(0[,]+∞) → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ (0[,]+∞))
37	11	esumcl 34367	. . . . 5 ⊢ ((ℕ ∈ V ∧ ∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ (0[,]+∞)) → Σ^*𝑘 ∈ ℕ(𝐹‘𝑘) ∈ (0[,]+∞))
38	33, 36, 37	sylancr 598	. . . 4 ⊢ (𝐹:ℕ⟶(0[,]+∞) → Σ^*𝑘 ∈ ℕ(𝐹‘𝑘) ∈ (0[,]+∞))
39	7, 38	sselid 3943	. . 3 ⊢ (𝐹:ℕ⟶(0[,]+∞) → Σ^𝑘 ∈ ℕ(𝐹‘𝑘) ∈ ℝ^)
40		fvelrnb 6944	. . . . . . . . 9 ⊢ (seq1( +_𝑒 , 𝐹) Fn ℕ → (𝑥 ∈ ran seq1( +_𝑒 , 𝐹) ↔ ∃𝑛 ∈ ℕ (seq1( +_𝑒 , 𝐹)‘𝑛) = 𝑥))
41	6, 40	mp1i 14	. . . . . . . 8 ⊢ (𝐹:ℕ⟶(0[,]+∞) → (𝑥 ∈ ran seq1( +_𝑒 , 𝐹) ↔ ∃𝑛 ∈ ℕ (seq1( +_𝑒 , 𝐹)‘𝑛) = 𝑥))
42		eqcom 2776	. . . . . . . . . 10 ⊢ (Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) = 𝑥 ↔ 𝑥 = Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘))
43	9	eqeq1d 2771	. . . . . . . . . 10 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) = 𝑥 ↔ (seq1( +_𝑒 , 𝐹)‘𝑛) = 𝑥))
44	42, 43	bitr3id 288	. . . . . . . . 9 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (𝑥 = Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ↔ (seq1( +_𝑒 , 𝐹)‘𝑛) = 𝑥))
45	44	rexbidva 3193	. . . . . . . 8 ⊢ (𝐹:ℕ⟶(0[,]+∞) → (∃𝑛 ∈ ℕ 𝑥 = Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ↔ ∃𝑛 ∈ ℕ (seq1( +_𝑒 , 𝐹)‘𝑛) = 𝑥))
46	41, 45	bitr4d 285	. . . . . . 7 ⊢ (𝐹:ℕ⟶(0[,]+∞) → (𝑥 ∈ ran seq1( +_𝑒 , 𝐹) ↔ ∃𝑛 ∈ ℕ 𝑥 = Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)))
47	46	biimpa 481	. . . . . 6 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ran seq1( +_𝑒 , 𝐹)) → ∃𝑛 ∈ ℕ 𝑥 = Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))
48	33	a1i 11	. . . . . . . . 9 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → ℕ ∈ V)
49	34	adantlr 727	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ (0[,]+∞))
50	17, 18	mp1i 14	. . . . . . . . 9 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ⊆ ℕ)
51	15, 48, 49, 50	esummono 34391	. . . . . . . 8 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ^𝑘 ∈ ℕ(𝐹‘𝑘))
52	51	ralrimiva 3163	. . . . . . 7 ⊢ (𝐹:ℕ⟶(0[,]+∞) → ∀𝑛 ∈ ℕ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ^𝑘 ∈ ℕ(𝐹‘𝑘))
53	52	adantr 485	. . . . . 6 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ran seq1( +_𝑒 , 𝐹)) → ∀𝑛 ∈ ℕ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ^𝑘 ∈ ℕ(𝐹‘𝑘))
54	47, 53	jca 520	. . . . 5 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ran seq1( +_𝑒 , 𝐹)) → (∃𝑛 ∈ ℕ 𝑥 = Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ∧ ∀𝑛 ∈ ℕ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)))
55		r19.29r 3135	. . . . 5 ⊢ ((∃𝑛 ∈ ℕ 𝑥 = Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ∧ ∀𝑛 ∈ ℕ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) → ∃𝑛 ∈ ℕ (𝑥 = Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ∧ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ^𝑘 ∈ ℕ(𝐹‘𝑘)))
56		breq1 5116	. . . . . . 7 ⊢ (𝑥 = Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) → (𝑥 ≤ Σ^𝑘 ∈ ℕ(𝐹‘𝑘) ↔ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ^𝑘 ∈ ℕ(𝐹‘𝑘)))
57	56	biimpar 482	. . . . . 6 ⊢ ((𝑥 = Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ∧ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) → 𝑥 ≤ Σ^𝑘 ∈ ℕ(𝐹‘𝑘))
58	57	rexlimivw 3168	. . . . 5 ⊢ (∃𝑛 ∈ ℕ (𝑥 = Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ∧ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ≤ Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) → 𝑥 ≤ Σ^𝑘 ∈ ℕ(𝐹‘𝑘))
59	54, 55, 58	3syl 19	. . . 4 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ran seq1( +_𝑒 , 𝐹)) → 𝑥 ≤ Σ^*𝑘 ∈ ℕ(𝐹‘𝑘))
60	59	ralrimiva 3163	. . 3 ⊢ (𝐹:ℕ⟶(0[,]+∞) → ∀𝑥 ∈ ran seq1( +_𝑒 , 𝐹)𝑥 ≤ Σ^*𝑘 ∈ ℕ(𝐹‘𝑘))
61		nfv 1941	. . . . . . . . . . 11 ⊢ Ⅎ𝑘 𝑥 ∈ ℝ
62	13, 61	nfan 1926	. . . . . . . . . 10 ⊢ Ⅎ𝑘(𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ)
63		nfcv 2931	. . . . . . . . . . 11 ⊢ Ⅎ𝑘𝑥
64		nfcv 2931	. . . . . . . . . . 11 ⊢ Ⅎ𝑘 <
65	11	nfesum1 34377	. . . . . . . . . . 11 ⊢ Ⅎ𝑘Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)
66	63, 64, 65	nfbr 5162	. . . . . . . . . 10 ⊢ Ⅎ𝑘 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)
67	62, 66	nfan 1926	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘))
68	33	a1i 11	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) → ℕ ∈ V)
69		simplll 786	. . . . . . . . . 10 ⊢ ((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶(0[,]+∞))
70	69, 34	sylancom 599	. . . . . . . . 9 ⊢ ((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ (0[,]+∞))
71		simplr 780	. . . . . . . . . 10 ⊢ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) → 𝑥 ∈ ℝ)
72	71	rexrd 11261	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) → 𝑥 ∈ ℝ^)
73		simpr 489	. . . . . . . . 9 ⊢ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) → 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘))
74	67, 68, 70, 72, 73	esumlub 34397	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) → ∃𝑎 ∈ (𝒫 ℕ ∩ Fin)𝑥 < Σ^𝑘 ∈ 𝑎(𝐹‘𝑘))
75		ssnnssfz 33075	. . . . . . . . . 10 ⊢ (𝑎 ∈ (𝒫 ℕ ∩ Fin) → ∃𝑛 ∈ ℕ 𝑎 ⊆ (1...𝑛))
76		r19.42v 3203	. . . . . . . . . . 11 ⊢ (∃𝑛 ∈ ℕ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) ↔ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ ∃𝑛 ∈ ℕ 𝑎 ⊆ (1...𝑛)))
77		nfv 1941	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘 𝑎 ⊆ (1...𝑛)
78	67, 77	nfan 1926	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘(((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛))
79	10	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) → (1...𝑛) ∈ V)
80		simp-4l 794	. . . . . . . . . . . . . 14 ⊢ (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) ∧ 𝑘 ∈ (1...𝑛)) → 𝐹:ℕ⟶(0[,]+∞))
81	17, 18	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (1...𝑛) ⊆ ℕ
82		simpr 489	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...𝑛))
83	81, 82	sselid 3943	. . . . . . . . . . . . . 14 ⊢ (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
84	80, 83	ffvelcdmd 7083	. . . . . . . . . . . . 13 ⊢ (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) ∧ 𝑘 ∈ (1...𝑛)) → (𝐹‘𝑘) ∈ (0[,]+∞))
85		simpr 489	. . . . . . . . . . . . 13 ⊢ ((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) → 𝑎 ⊆ (1...𝑛))
86	78, 79, 84, 85	esummono 34391	. . . . . . . . . . . 12 ⊢ ((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) → Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))
87	86	reximi 3109	. . . . . . . . . . 11 ⊢ (∃𝑛 ∈ ℕ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ⊆ (1...𝑛)) → ∃𝑛 ∈ ℕ Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))
88	76, 87	sylbir 238	. . . . . . . . . 10 ⊢ ((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ ∃𝑛 ∈ ℕ 𝑎 ⊆ (1...𝑛)) → ∃𝑛 ∈ ℕ Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))
89	75, 88	sylan2 604	. . . . . . . . 9 ⊢ ((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) → ∃𝑛 ∈ ℕ Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))
90	89	ralrimiva 3163	. . . . . . . 8 ⊢ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) → ∀𝑎 ∈ (𝒫 ℕ ∩ Fin)∃𝑛 ∈ ℕ Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘))
91		r19.29r 3135	. . . . . . . . 9 ⊢ ((∃𝑎 ∈ (𝒫 ℕ ∩ Fin)𝑥 < Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ ∀𝑎 ∈ (𝒫 ℕ ∩ Fin)∃𝑛 ∈ ℕ Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → ∃𝑎 ∈ (𝒫 ℕ ∩ Fin)(𝑥 < Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ ∃𝑛 ∈ ℕ Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘)))
92		r19.42v 3203	. . . . . . . . . 10 ⊢ (∃𝑛 ∈ ℕ (𝑥 < Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) ↔ (𝑥 < Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ ∃𝑛 ∈ ℕ Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘)))
93	92	rexbii 3118	. . . . . . . . 9 ⊢ (∃𝑎 ∈ (𝒫 ℕ ∩ Fin)∃𝑛 ∈ ℕ (𝑥 < Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) ↔ ∃𝑎 ∈ (𝒫 ℕ ∩ Fin)(𝑥 < Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ ∃𝑛 ∈ ℕ Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘)))
94	91, 93	sylibr 237	. . . . . . . 8 ⊢ ((∃𝑎 ∈ (𝒫 ℕ ∩ Fin)𝑥 < Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ ∀𝑎 ∈ (𝒫 ℕ ∩ Fin)∃𝑛 ∈ ℕ Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → ∃𝑎 ∈ (𝒫 ℕ ∩ Fin)∃𝑛 ∈ ℕ (𝑥 < Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘)))
95	74, 90, 94	syl2anc 595	. . . . . . 7 ⊢ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) → ∃𝑎 ∈ (𝒫 ℕ ∩ Fin)∃𝑛 ∈ ℕ (𝑥 < Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘)))
96		simp-4r 795	. . . . . . . . . . 11 ⊢ (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
97	96	rexrd 11261	. . . . . . . . . 10 ⊢ (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ^)
98		vex 3467	. . . . . . . . . . . 12 ⊢ 𝑎 ∈ V
99		nfcv 2931	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘𝑎
100	99	nfel1 2947	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘 𝑎 ∈ (𝒫 ℕ ∩ Fin)
101	67, 100	nfan 1926	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘(((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin))
102	101, 14	nfan 1926	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ)
103		simp-5l 796	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑎) → 𝐹:ℕ⟶(0[,]+∞))
104		simpllr 787	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑎) → 𝑎 ∈ (𝒫 ℕ ∩ Fin))
105		inss1 4197	. . . . . . . . . . . . . . . . . 18 ⊢ (𝒫 ℕ ∩ Fin) ⊆ 𝒫 ℕ
106	105	sseli 3941	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ (𝒫 ℕ ∩ Fin) → 𝑎 ∈ 𝒫 ℕ)
107		elpwi 4574	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ 𝒫 ℕ → 𝑎 ⊆ ℕ)
108	104, 106, 107	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑎) → 𝑎 ⊆ ℕ)
109		simpr 489	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑎) → 𝑘 ∈ 𝑎)
110	108, 109	sseldd 3946	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑎) → 𝑘 ∈ ℕ)
111	103, 110	ffvelcdmd 7083	. . . . . . . . . . . . . 14 ⊢ ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑎) → (𝐹‘𝑘) ∈ (0[,]+∞))
112	111	ex 417	. . . . . . . . . . . . 13 ⊢ (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ 𝑎 → (𝐹‘𝑘) ∈ (0[,]+∞)))
113	102, 112	ralrimi 3269	. . . . . . . . . . . 12 ⊢ (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ 𝑎 (𝐹‘𝑘) ∈ (0[,]+∞))
114	99	esumcl 34367	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ V ∧ ∀𝑘 ∈ 𝑎 (𝐹‘𝑘) ∈ (0[,]+∞)) → Σ^*𝑘 ∈ 𝑎(𝐹‘𝑘) ∈ (0[,]+∞))
115	98, 113, 114	sylancr 598	. . . . . . . . . . 11 ⊢ (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ∈ (0[,]+∞))
116	7, 115	sselid 3943	. . . . . . . . . 10 ⊢ (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ∈ ℝ^*)
117		simp-5l 796	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐹:ℕ⟶(0[,]+∞))
118		simpr 489	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...𝑛))
119	81, 118	sselid 3943	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
120	117, 119	ffvelcdmd 7083	. . . . . . . . . . . . . 14 ⊢ ((((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐹‘𝑘) ∈ (0[,]+∞))
121	120	ex 417	. . . . . . . . . . . . 13 ⊢ (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ (1...𝑛) → (𝐹‘𝑘) ∈ (0[,]+∞)))
122	102, 121	ralrimi 3269	. . . . . . . . . . . 12 ⊢ (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ∈ (0[,]+∞))
123	10, 122, 26	sylancr 598	. . . . . . . . . . 11 ⊢ (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ∈ (0[,]+∞))
124	7, 123	sselid 3943	. . . . . . . . . 10 ⊢ (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ∈ ℝ^*)
125		xrltletr 13184	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ^* ∧ Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ∈ ℝ^ ∧ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ∈ ℝ^) → ((𝑥 < Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → 𝑥 < Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘)))
126	97, 116, 124, 125	syl3anc 1396	. . . . . . . . 9 ⊢ (((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) ∧ 𝑛 ∈ ℕ) → ((𝑥 < Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → 𝑥 < Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)))
127	126	reximdva 3184	. . . . . . . 8 ⊢ ((((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) ∧ 𝑎 ∈ (𝒫 ℕ ∩ Fin)) → (∃𝑛 ∈ ℕ (𝑥 < Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → ∃𝑛 ∈ ℕ 𝑥 < Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)))
128	127	rexlimdva 3172	. . . . . . 7 ⊢ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) → (∃𝑎 ∈ (𝒫 ℕ ∩ Fin)∃𝑛 ∈ ℕ (𝑥 < Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ∧ Σ^𝑘 ∈ 𝑎(𝐹‘𝑘) ≤ Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → ∃𝑛 ∈ ℕ 𝑥 < Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)))
129	95, 128	mpd 16	. . . . . 6 ⊢ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) → ∃𝑛 ∈ ℕ 𝑥 < Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘))
130		fvelrnb 6944	. . . . . . . . . 10 ⊢ (seq1( +_𝑒 , 𝐹) Fn ℕ → (𝑦 ∈ ran seq1( +_𝑒 , 𝐹) ↔ ∃𝑛 ∈ ℕ (seq1( +_𝑒 , 𝐹)‘𝑛) = 𝑦))
131	6, 130	mp1i 14	. . . . . . . . 9 ⊢ (𝐹:ℕ⟶(0[,]+∞) → (𝑦 ∈ ran seq1( +_𝑒 , 𝐹) ↔ ∃𝑛 ∈ ℕ (seq1( +_𝑒 , 𝐹)‘𝑛) = 𝑦))
132		eqcom 2776	. . . . . . . . . . 11 ⊢ (Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘) = 𝑦 ↔ 𝑦 = Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘))
133	9	eqeq1d 2771	. . . . . . . . . . 11 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) = 𝑦 ↔ (seq1( +_𝑒 , 𝐹)‘𝑛) = 𝑦))
134	132, 133	bitr3id 288	. . . . . . . . . 10 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑛 ∈ ℕ) → (𝑦 = Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ↔ (seq1( +_𝑒 , 𝐹)‘𝑛) = 𝑦))
135	134	rexbidva 3193	. . . . . . . . 9 ⊢ (𝐹:ℕ⟶(0[,]+∞) → (∃𝑛 ∈ ℕ 𝑦 = Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘) ↔ ∃𝑛 ∈ ℕ (seq1( +_𝑒 , 𝐹)‘𝑛) = 𝑦))
136	131, 135	bitr4d 285	. . . . . . . 8 ⊢ (𝐹:ℕ⟶(0[,]+∞) → (𝑦 ∈ ran seq1( +_𝑒 , 𝐹) ↔ ∃𝑛 ∈ ℕ 𝑦 = Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)))
137		simpr 489	. . . . . . . . 9 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑦 = Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → 𝑦 = Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘))
138	137	breq2d 5125	. . . . . . . 8 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑦 = Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘)) → (𝑥 < 𝑦 ↔ 𝑥 < Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘)))
139	27, 136, 138	rexxfr2d 5385	. . . . . . 7 ⊢ (𝐹:ℕ⟶(0[,]+∞) → (∃𝑦 ∈ ran seq1( +_𝑒 , 𝐹)𝑥 < 𝑦 ↔ ∃𝑛 ∈ ℕ 𝑥 < Σ^*𝑘 ∈ (1...𝑛)(𝐹‘𝑘)))
140	139	ad2antrr 738	. . . . . 6 ⊢ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘)) → (∃𝑦 ∈ ran seq1( +_𝑒 , 𝐹)𝑥 < 𝑦 ↔ ∃𝑛 ∈ ℕ 𝑥 < Σ^𝑘 ∈ (1...𝑛)(𝐹‘𝑘)))
141	129, 140	mpbird 260	. . . . 5 ⊢ (((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘)) → ∃𝑦 ∈ ran seq1( +_𝑒 , 𝐹)𝑥 < 𝑦)
142	141	ex 417	. . . 4 ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑥 ∈ ℝ) → (𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘) → ∃𝑦 ∈ ran seq1( +_𝑒 , 𝐹)𝑥 < 𝑦))
143	142	ralrimiva 3163	. . 3 ⊢ (𝐹:ℕ⟶(0[,]+∞) → ∀𝑥 ∈ ℝ (𝑥 < Σ^*𝑘 ∈ ℕ(𝐹‘𝑘) → ∃𝑦 ∈ ran seq1( +_𝑒 , 𝐹)𝑥 < 𝑦))
144		supxr2 13342	. . 3 ⊢ (((ran seq1( +_𝑒 , 𝐹) ⊆ ℝ^* ∧ Σ^𝑘 ∈ ℕ(𝐹‘𝑘) ∈ ℝ^) ∧ (∀𝑥 ∈ ran seq1( +_𝑒 , 𝐹)𝑥 ≤ Σ^𝑘 ∈ ℕ(𝐹‘𝑘) ∧ ∀𝑥 ∈ ℝ (𝑥 < Σ^𝑘 ∈ ℕ(𝐹‘𝑘) → ∃𝑦 ∈ ran seq1( +_𝑒 , 𝐹)𝑥 < 𝑦))) → sup(ran seq1( +_𝑒 , 𝐹), ℝ^, < ) = Σ^𝑘 ∈ ℕ(𝐹‘𝑘))
145	32, 39, 60, 143, 144	syl22anc 851	. 2 ⊢ (𝐹:ℕ⟶(0[,]+∞) → sup(ran seq1( +_𝑒 , 𝐹), ℝ^, < ) = Σ^𝑘 ∈ ℕ(𝐹‘𝑘))
146	145	eqcomd 2775	1 ⊢ (𝐹:ℕ⟶(0[,]+∞) → Σ^𝑘 ∈ ℕ(𝐹‘𝑘) = sup(ran seq1( +_𝑒 , 𝐹), ℝ^, < ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1567 ∈ wcel 2149 Ⅎwnfc 2916 ∀wral 3085 ∃wrex 3095 Vcvv 3463 ∩ cin 3912 ⊆ wss 3913 𝒫 cpw 4567 class class class wbr 5113 ran crn 5665 Fn wfn 6534 ⟶wf 6535 ‘cfv 6539 (class class class)co 7413 Fincfn 8945 supcsup 9402 ℝcr 11101 0cc0 11102 1c1 11103 +∞cpnf 11242 ℝ^*cxr 11244 < clt 11245 ≤ cle 11246 ℕcn 12235 ℤcz 12593 ℤ_≥cuz 12864 +_𝑒 cxad 13137 [,]cicc 13377 ...cfz 13537 seqcseq 14039 Σ^*cesum 34364

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5273 ax-pow 5339 ax-pr 5407 ax-un 7735 ax-inf2 9612 ax-cnex 11158 ax-resscn 11159 ax-1cn 11160 ax-icn 11161 ax-addcl 11162 ax-addrcl 11163 ax-mulcl 11164 ax-mulrcl 11165 ax-mulcom 11166 ax-addass 11167 ax-mulass 11168 ax-distr 11169 ax-i2m1 11170 ax-1ne0 11171 ax-1rid 11172 ax-rnegex 11173 ax-rrecex 11174 ax-cnre 11175 ax-pre-lttri 11176 ax-pre-lttrn 11177 ax-pre-ltadd 11178 ax-pre-mulgt0 11179 ax-pre-sup 11180 ax-addf 11181 ax-mulf 11182

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-iin 4963 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5559 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-se 5618 df-we 5619 df-xp 5670 df-rel 5671 df-cnv 5672 df-co 5673 df-dm 5674 df-rn 5675 df-res 5676 df-ima 5677 df-pred 6305 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6495 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-isom 6548 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7677 df-om 7865 df-1st 7988 df-2nd 7989 df-supp 8159 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-2o 8456 df-er 8696 df-map 8828 df-pm 8829 df-ixp 8898 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-fsupp 9324 df-fi 9373 df-sup 9404 df-inf 9405 df-oi 9474 df-card 9927 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11445 df-neg 11446 df-div 11874 df-nn 12236 df-2 12305 df-3 12306 df-4 12307 df-5 12308 df-6 12309 df-7 12310 df-8 12311 df-9 12312 df-n0 12507 df-z 12594 df-dec 12714 df-uz 12865 df-q 12975 df-rp 13019 df-xneg 13139 df-xadd 13140 df-xmul 13141 df-ioo 13378 df-ioc 13379 df-ico 13380 df-icc 13381 df-fz 13538 df-fzo 13685 df-fl 13827 df-mod 13905 df-seq 14040 df-exp 14100 df-fac 14312 df-bc 14341 df-hash 14369 df-shft 15106 df-cj 15152 df-re 15153 df-im 15154 df-sqrt 15288 df-abs 15289 df-limsup 15524 df-clim 15541 df-rlim 15542 df-sum 15740 df-ef 16123 df-sin 16125 df-cos 16126 df-pi 16128 df-struct 17209 df-sets 17226 df-slot 17244 df-ndx 17256 df-base 17272 df-ress 17293 df-plusg 17325 df-mulr 17326 df-starv 17327 df-sca 17328 df-vsca 17329 df-ip 17330 df-tset 17331 df-ple 17332 df-ds 17334 df-unif 17335 df-hom 17336 df-cco 17337 df-rest 17477 df-topn 17478 df-0g 17496 df-gsum 17497 df-topgen 17498 df-pt 17499 df-prds 17502 df-ordt 17557 df-xrs 17558 df-qtop 17563 df-imas 17564 df-xps 17566 df-mre 17640 df-mrc 17641 df-acs 17643 df-ps 18624 df-tsr 18625 df-plusf 18699 df-mgm 18700 df-sgrp 18779 df-mnd 18795 df-mhm 18843 df-submnd 18844 df-grp 19005 df-minusg 19006 df-sbg 19007 df-mulg 19136 df-subg 19191 df-cntz 19389 df-cmn 19854 df-abl 19855 df-mgp 20219 df-rng 20233 df-ur 20266 df-ring 20319 df-cring 20320 df-subrng 20633 df-subrg 20657 df-abv 20892 df-lmod 20963 df-scaf 20964 df-sra 21274 df-rgmod 21275 df-psmet 21485 df-xmet 21486 df-met 21487 df-bl 21488 df-mopn 21489 df-fbas 21490 df-fg 21491 df-cnfld 21494 df-top 23022 df-topon 23039 df-topsp 23061 df-bases 23074 df-cld 23147 df-ntr 23148 df-cls 23149 df-nei 23226 df-lp 23264 df-perf 23265 df-cn 23355 df-cnp 23356 df-haus 23443 df-tx 23690 df-hmeo 23883 df-fil 23974 df-fm 24066 df-flim 24067 df-flf 24068 df-tmd 24200 df-tgp 24201 df-tsms 24255 df-trg 24288 df-xms 24448 df-ms 24449 df-tms 24450 df-nm 24710 df-ngp 24711 df-nrg 24713 df-nlm 24714 df-ii 25007 df-cncf 25008 df-limc 25996 df-dv 25997 df-log 26689 df-esum 34365

This theorem is referenced by: esumfsupre 34408 esumsup 34426

W3C validator