climsup - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > climsup		Structured version Visualization version GIF version

Theorem climsup 15309

Description: A bounded monotonic sequence converges to the supremum of its range. Theorem 12-5.1 of [Gleason] p. 180. (Contributed by NM, 13-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.)

**Hypotheses**
Ref	Expression
climsup.1	⊢ 𝑍 = (ℤ_≥‘𝑀)
climsup.2	⊢ (𝜑 → 𝑀 ∈ ℤ)
climsup.3	⊢ (𝜑 → 𝐹:𝑍⟶ℝ)
climsup.4	⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)))
climsup.5	⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ≤ 𝑥)

**Assertion**
Ref	Expression
climsup	⊢ (𝜑 → 𝐹 ⇝ sup(ran 𝐹, ℝ, < ))

Distinct variable groups: 𝑥,𝑘,𝐹 𝜑,𝑘 𝑘,𝑍,𝑥 Allowed substitution hints: 𝜑(𝑥) 𝑀(𝑥,𝑘)

Proof of Theorem climsup Dummy variables 𝑗 𝑛 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		climsup.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)
2	1	frnd 6592	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 ⊆ ℝ)
3	1	ffnd 6585	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 Fn 𝑍)
4		climsup.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℤ)
5		uzid 12526	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ_≥‘𝑀))
6	4, 5	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘𝑀))
7		climsup.1	. . . . . . . . . . . 12 ⊢ 𝑍 = (ℤ_≥‘𝑀)
8	6, 7	eleqtrrdi 2850	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ 𝑍)
9		fnfvelrn 6940	. . . . . . . . . . 11 ⊢ ((𝐹 Fn 𝑍 ∧ 𝑀 ∈ 𝑍) → (𝐹‘𝑀) ∈ ran 𝐹)
10	3, 8, 9	syl2anc 583	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘𝑀) ∈ ran 𝐹)
11	10	ne0d 4266	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 ≠ ∅)
12		climsup.5	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ≤ 𝑥)
13		breq1 5073	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹‘𝑘) → (𝑦 ≤ 𝑥 ↔ (𝐹‘𝑘) ≤ 𝑥))
14	13	ralrn 6946	. . . . . . . . . . . 12 ⊢ (𝐹 Fn 𝑍 → (∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ↔ ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ≤ 𝑥))
15	14	rexbidv 3225	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝑍 → (∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ≤ 𝑥))
16	3, 15	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ≤ 𝑥))
17	12, 16	mpbird 256	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥)
18	2, 11, 17	3jca 1126	. . . . . . . 8 ⊢ (𝜑 → (ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥))
19		suprcl 11865	. . . . . . . 8 ⊢ ((ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → sup(ran 𝐹, ℝ, < ) ∈ ℝ)
20	18, 19	syl 17	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝐹, ℝ, < ) ∈ ℝ)
21		ltsubrp 12695	. . . . . . 7 ⊢ ((sup(ran 𝐹, ℝ, < ) ∈ ℝ ∧ 𝑦 ∈ ℝ⁺) → (sup(ran 𝐹, ℝ, < ) − 𝑦) < sup(ran 𝐹, ℝ, < ))
22	20, 21	sylan 579	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (sup(ran 𝐹, ℝ, < ) − 𝑦) < sup(ran 𝐹, ℝ, < ))
23	18	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥))
24		rpre 12667	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ⁺ → 𝑦 ∈ ℝ)
25		resubcl 11215	. . . . . . . 8 ⊢ ((sup(ran 𝐹, ℝ, < ) ∈ ℝ ∧ 𝑦 ∈ ℝ) → (sup(ran 𝐹, ℝ, < ) − 𝑦) ∈ ℝ)
26	20, 24, 25	syl2an 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (sup(ran 𝐹, ℝ, < ) − 𝑦) ∈ ℝ)
27		suprlub 11869	. . . . . . 7 ⊢ (((ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) − 𝑦) ∈ ℝ) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < sup(ran 𝐹, ℝ, < ) ↔ ∃𝑘 ∈ ran 𝐹(sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘))
28	23, 26, 27	syl2anc 583	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < sup(ran 𝐹, ℝ, < ) ↔ ∃𝑘 ∈ ran 𝐹(sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘))
29	22, 28	mpbid 231	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ∃𝑘 ∈ ran 𝐹(sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘)
30		breq2 5074	. . . . . . . 8 ⊢ (𝑘 = (𝐹‘𝑗) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘 ↔ (sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗)))
31	30	rexrn 6945	. . . . . . 7 ⊢ (𝐹 Fn 𝑍 → (∃𝑘 ∈ ran 𝐹(sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘 ↔ ∃𝑗 ∈ 𝑍 (sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗)))
32	3, 31	syl 17	. . . . . 6 ⊢ (𝜑 → (∃𝑘 ∈ ran 𝐹(sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘 ↔ ∃𝑗 ∈ 𝑍 (sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗)))
33	32	biimpa 476	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑘 ∈ ran 𝐹(sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘) → ∃𝑗 ∈ 𝑍 (sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗))
34	29, 33	syldan 590	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ∃𝑗 ∈ 𝑍 (sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗))
35		ffvelrn 6941	. . . . . . . . . . . 12 ⊢ ((𝐹:𝑍⟶ℝ ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) ∈ ℝ)
36	1, 35	sylan 579	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) ∈ ℝ)
37	36	ad2ant2r 743	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → (𝐹‘𝑗) ∈ ℝ)
38	1	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝐹:𝑍⟶ℝ)
39	7	uztrn2 12530	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) → 𝑘 ∈ 𝑍)
40		ffvelrn 6941	. . . . . . . . . . 11 ⊢ ((𝐹:𝑍⟶ℝ ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)
41	38, 39, 40	syl2an 595	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → (𝐹‘𝑘) ∈ ℝ)
42	20	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → sup(ran 𝐹, ℝ, < ) ∈ ℝ)
43		simprr 769	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → 𝑘 ∈ (ℤ_≥‘𝑗))
44		fzssuz 13226	. . . . . . . . . . . . . 14 ⊢ (𝑗...𝑘) ⊆ (ℤ_≥‘𝑗)
45		uzss 12534	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → (ℤ_≥‘𝑗) ⊆ (ℤ_≥‘𝑀))
46	45, 7	sseqtrrdi 3968	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → (ℤ_≥‘𝑗) ⊆ 𝑍)
47	46, 7	eleq2s 2857	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ 𝑍 → (ℤ_≥‘𝑗) ⊆ 𝑍)
48	47	ad2antrl 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → (ℤ_≥‘𝑗) ⊆ 𝑍)
49	44, 48	sstrid 3928	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → (𝑗...𝑘) ⊆ 𝑍)
50		ffvelrn 6941	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑍⟶ℝ ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ ℝ)
51	50	ralrimiva 3107	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝑍⟶ℝ → ∀𝑛 ∈ 𝑍 (𝐹‘𝑛) ∈ ℝ)
52	1, 51	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑛 ∈ 𝑍 (𝐹‘𝑛) ∈ ℝ)
53	52	ad2antrr 722	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → ∀𝑛 ∈ 𝑍 (𝐹‘𝑛) ∈ ℝ)
54		ssralv 3983	. . . . . . . . . . . . 13 ⊢ ((𝑗...𝑘) ⊆ 𝑍 → (∀𝑛 ∈ 𝑍 (𝐹‘𝑛) ∈ ℝ → ∀𝑛 ∈ (𝑗...𝑘)(𝐹‘𝑛) ∈ ℝ))
55	49, 53, 54	sylc 65	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → ∀𝑛 ∈ (𝑗...𝑘)(𝐹‘𝑛) ∈ ℝ)
56	55	r19.21bi 3132	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) ∧ 𝑛 ∈ (𝑗...𝑘)) → (𝐹‘𝑛) ∈ ℝ)
57		fzssuz 13226	. . . . . . . . . . . . . 14 ⊢ (𝑗...(𝑘 − 1)) ⊆ (ℤ_≥‘𝑗)
58	57, 48	sstrid 3928	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → (𝑗...(𝑘 − 1)) ⊆ 𝑍)
59	58	sselda 3917	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) ∧ 𝑛 ∈ (𝑗...(𝑘 − 1))) → 𝑛 ∈ 𝑍)
60		climsup.4	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)))
61	60	ralrimiva 3107	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)))
62	61	ad2antrr 722	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)))
63		fveq2 6756	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛))
64		fvoveq1 7278	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑛 + 1)))
65	63, 64	breq12d 5083	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)) ↔ (𝐹‘𝑛) ≤ (𝐹‘(𝑛 + 1))))
66	65	rspccva 3551	. . . . . . . . . . . . 13 ⊢ ((∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ≤ (𝐹‘(𝑛 + 1)))
67	62, 66	sylan 579	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ≤ (𝐹‘(𝑛 + 1)))
68	59, 67	syldan 590	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) ∧ 𝑛 ∈ (𝑗...(𝑘 − 1))) → (𝐹‘𝑛) ≤ (𝐹‘(𝑛 + 1)))
69	43, 56, 68	monoord 13681	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → (𝐹‘𝑗) ≤ (𝐹‘𝑘))
70	37, 41, 42, 69	lesub2dd 11522	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑘)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗)))
71	42, 41	resubcld 11333	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑘)) ∈ ℝ)
72	42, 37	resubcld 11333	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗)) ∈ ℝ)
73	24	ad2antlr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → 𝑦 ∈ ℝ)
74		lelttr 10996	. . . . . . . . . 10 ⊢ (((sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑘)) ∈ ℝ ∧ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗)) ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑘)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗)) ∧ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗)) < 𝑦) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑘)) < 𝑦))
75	71, 72, 73, 74	syl3anc 1369	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → (((sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑘)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗)) ∧ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗)) < 𝑦) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑘)) < 𝑦))
76	70, 75	mpand 691	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → ((sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗)) < 𝑦 → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑘)) < 𝑦))
77		ltsub23 11385	. . . . . . . . 9 ⊢ ((sup(ran 𝐹, ℝ, < ) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ (𝐹‘𝑗) ∈ ℝ) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗) ↔ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗)) < 𝑦))
78	42, 73, 37, 77	syl3anc 1369	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗) ↔ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗)) < 𝑦))
79	18	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → (ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥))
80	3	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝐹 Fn 𝑍)
81		fnfvelrn 6940	. . . . . . . . . . . 12 ⊢ ((𝐹 Fn 𝑍 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ran 𝐹)
82	80, 39, 81	syl2an 595	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → (𝐹‘𝑘) ∈ ran 𝐹)
83		suprub 11866	. . . . . . . . . . 11 ⊢ (((ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝐹‘𝑘) ∈ ran 𝐹) → (𝐹‘𝑘) ≤ sup(ran 𝐹, ℝ, < ))
84	79, 82, 83	syl2anc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → (𝐹‘𝑘) ≤ sup(ran 𝐹, ℝ, < ))
85	41, 42, 84	abssuble0d 15072	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → (abs‘((𝐹‘𝑘) − sup(ran 𝐹, ℝ, < ))) = (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑘)))
86	85	breq1d 5080	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → ((abs‘((𝐹‘𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦 ↔ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑘)) < 𝑦))
87	76, 78, 86	3imtr4d 293	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑗))) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗) → (abs‘((𝐹‘𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦))
88	87	anassrs 467	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗) → (abs‘((𝐹‘𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦))
89	88	ralrimdva 3112	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑗 ∈ 𝑍) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗) → ∀𝑘 ∈ (ℤ_≥‘𝑗)(abs‘((𝐹‘𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦))
90	89	reximdva 3202	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (∃𝑗 ∈ 𝑍 (sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ_≥‘𝑗)(abs‘((𝐹‘𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦))
91	34, 90	mpd 15	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ_≥‘𝑗)(abs‘((𝐹‘𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦)
92	91	ralrimiva 3107	. 2 ⊢ (𝜑 → ∀𝑦 ∈ ℝ⁺ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ_≥‘𝑗)(abs‘((𝐹‘𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦)
93	7	fvexi 6770	. . . 4 ⊢ 𝑍 ∈ V
94		fex 7084	. . . 4 ⊢ ((𝐹:𝑍⟶ℝ ∧ 𝑍 ∈ V) → 𝐹 ∈ V)
95	1, 93, 94	sylancl 585	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
96		eqidd 2739	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘))
97	20	recnd 10934	. . 3 ⊢ (𝜑 → sup(ran 𝐹, ℝ, < ) ∈ ℂ)
98	1, 40	sylan 579	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)
99	98	recnd 10934	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)
100	7, 4, 95, 96, 97, 99	clim2c 15142	. 2 ⊢ (𝜑 → (𝐹 ⇝ sup(ran 𝐹, ℝ, < ) ↔ ∀𝑦 ∈ ℝ⁺ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ_≥‘𝑗)(abs‘((𝐹‘𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦))
101	92, 100	mpbird 256	1 ⊢ (𝜑 → 𝐹 ⇝ sup(ran 𝐹, ℝ, < ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 ∃wrex 3064 Vcvv 3422 ⊆ wss 3883 ∅c0 4253 class class class wbr 5070 ran crn 5581 Fn wfn 6413 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 supcsup 9129 ℝcr 10801 1c1 10803 + caddc 10805 < clt 10940 ≤ cle 10941 − cmin 11135 ℤcz 12249 ℤ_≥cuz 12511 ℝ⁺crp 12659 ...cfz 13168 abscabs 14873 ⇝ cli 15121

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-sup 9131 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-z 12250 df-uz 12512 df-rp 12660 df-fz 13169 df-seq 13650 df-exp 13711 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-clim 15125

This theorem is referenced by: isumsup2 15486 climcnds 15491 itg1climres 24784 itg2monolem1 24820 itg2i1fseq 24825 itg2i1fseq2 24826 emcllem6 26055 lmdvg 31805 esumpcvgval 31946 meaiuninclem 43908

W3C validator