liminflelimsuplem - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > liminflelimsuplem		Structured version Visualization version GIF version

Theorem liminflelimsuplem 44478

Description: The superior limit is greater than or equal to the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.)

**Hypotheses**
Ref	Expression
liminflelimsuplem.1	⊢ (𝜑 → 𝐹 ∈ 𝑉)
liminflelimsuplem.2	⊢ (𝜑 → ∀𝑘 ∈ ℝ ∃𝑗 ∈ (𝑘[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^*) ≠ ∅)

**Assertion**
Ref	Expression
liminflelimsuplem	⊢ (𝜑 → (lim inf‘𝐹) ≤ (lim sup‘𝐹))

Distinct variable groups: 𝑗,𝐹,𝑘 𝜑,𝑗 Allowed substitution hints: 𝜑(𝑘) 𝑉(𝑗,𝑘)

Proof of Theorem liminflelimsuplem Dummy variables 𝑖 𝑙 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 486	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) → 𝑙 ∈ ℝ)
2		simpl 484	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) → 𝑖 ∈ ℝ)
3	1, 2	ifcld 4574	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) → if(𝑖 ≤ 𝑙, 𝑙, 𝑖) ∈ ℝ)
4	3	adantll 713	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑙 ∈ ℝ) → if(𝑖 ≤ 𝑙, 𝑙, 𝑖) ∈ ℝ)
5		liminflelimsuplem.2	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑘 ∈ ℝ ∃𝑗 ∈ (𝑘[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^*) ≠ ∅)
6	5	ad2antrr 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑙 ∈ ℝ) → ∀𝑘 ∈ ℝ ∃𝑗 ∈ (𝑘[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^*) ≠ ∅)
7		oveq1 7413	. . . . . . . . . . . 12 ⊢ (𝑘 = if(𝑖 ≤ 𝑙, 𝑙, 𝑖) → (𝑘[,)+∞) = (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞))
8	7	rexeqdv 3327	. . . . . . . . . . 11 ⊢ (𝑘 = if(𝑖 ≤ 𝑙, 𝑙, 𝑖) → (∃𝑗 ∈ (𝑘[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ≠ ∅ ↔ ∃𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ≠ ∅))
9	8	rspcva 3611	. . . . . . . . . 10 ⊢ ((if(𝑖 ≤ 𝑙, 𝑙, 𝑖) ∈ ℝ ∧ ∀𝑘 ∈ ℝ ∃𝑗 ∈ (𝑘[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ≠ ∅) → ∃𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ≠ ∅)
10	4, 6, 9	syl2anc 585	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑙 ∈ ℝ) → ∃𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^*) ≠ ∅)
11		inss2 4229	. . . . . . . . . . . . . 14 ⊢ ((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^) ⊆ ℝ^
12		infxrcl 13309	. . . . . . . . . . . . . 14 ⊢ (((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^) ⊆ ℝ^ → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^*)
13	11, 12	ax-mp 5	. . . . . . . . . . . . 13 ⊢ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^*
14	13	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ≠ ∅) → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^)
15		inss2 4229	. . . . . . . . . . . . . 14 ⊢ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ⊆ ℝ^
16		infxrcl 13309	. . . . . . . . . . . . . 14 ⊢ (((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ⊆ ℝ^ → inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^*)
17	15, 16	ax-mp 5	. . . . . . . . . . . . 13 ⊢ inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^*
18	17	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ≠ ∅) → inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^)
19		inss2 4229	. . . . . . . . . . . . . 14 ⊢ ((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^) ⊆ ℝ^
20		supxrcl 13291	. . . . . . . . . . . . . 14 ⊢ (((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^) ⊆ ℝ^ → sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^*)
21	19, 20	ax-mp 5	. . . . . . . . . . . . 13 ⊢ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^*
22	21	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ≠ ∅) → sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^)
23		rexr 11257	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ ℝ → 𝑖 ∈ ℝ^*)
24	23	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → 𝑖 ∈ ℝ^*)
25		pnfxr 11265	. . . . . . . . . . . . . . . . . 18 ⊢ +∞ ∈ ℝ^*
26	25	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → +∞ ∈ ℝ^*)
27	3	rexrd 11261	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) → if(𝑖 ≤ 𝑙, 𝑙, 𝑖) ∈ ℝ^*)
28	27	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → if(𝑖 ≤ 𝑙, 𝑙, 𝑖) ∈ ℝ^*)
29		icossxr 13406	. . . . . . . . . . . . . . . . . . . 20 ⊢ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞) ⊆ ℝ^*
30		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞) → 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞))
31	29, 30	sselid 3980	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞) → 𝑗 ∈ ℝ^*)
32	31	adantl 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → 𝑗 ∈ ℝ^*)
33		max1 13161	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) → 𝑖 ≤ if(𝑖 ≤ 𝑙, 𝑙, 𝑖))
34	33	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → 𝑖 ≤ if(𝑖 ≤ 𝑙, 𝑙, 𝑖))
35		simpr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞))
36	28, 26, 35	icogelbd 44258	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → if(𝑖 ≤ 𝑙, 𝑙, 𝑖) ≤ 𝑗)
37	24, 28, 32, 34, 36	xrletrd 13138	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → 𝑖 ≤ 𝑗)
38	24, 26, 37	icossico2 44264	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → (𝑗[,)+∞) ⊆ (𝑖[,)+∞))
39	38	imass2d 43953	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → (𝐹 “ (𝑗[,)+∞)) ⊆ (𝐹 “ (𝑖[,)+∞)))
40	39	ssrind 4235	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ⊆ ((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^))
41	11	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → ((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^) ⊆ ℝ^)
42		infxrss 13315	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ⊆ ((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^) ∧ ((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^) ⊆ ℝ^) → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^), ℝ^, < ))
43	40, 41, 42	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^), ℝ^, < ))
44	43	adantr 482	. . . . . . . . . . . 12 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ≠ ∅) → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^), ℝ^*, < ))
45		supxrcl 13291	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ⊆ ℝ^ → sup(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^*)
46	15, 45	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ sup(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^*
47	46	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ≠ ∅) → sup(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^)
48	15	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ≠ ∅) → ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ⊆ ℝ^*)
49		simpr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ≠ ∅) → ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ≠ ∅)
50	48, 49	infxrlesupxr 44133	. . . . . . . . . . . . 13 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ≠ ∅) → inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ sup(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^), ℝ^*, < ))
51		rexr 11257	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑙 ∈ ℝ → 𝑙 ∈ ℝ^*)
52	51	ad2antlr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → 𝑙 ∈ ℝ^*)
53		max2 13163	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) → 𝑙 ≤ if(𝑖 ≤ 𝑙, 𝑙, 𝑖))
54	53	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → 𝑙 ≤ if(𝑖 ≤ 𝑙, 𝑙, 𝑖))
55	52, 28, 32, 54, 36	xrletrd 13138	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → 𝑙 ≤ 𝑗)
56	52, 26, 55	icossico2 44264	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → (𝑗[,)+∞) ⊆ (𝑙[,)+∞))
57	56	imass2d 43953	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → (𝐹 “ (𝑗[,)+∞)) ⊆ (𝐹 “ (𝑙[,)+∞)))
58	57	ssrind 4235	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ⊆ ((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^))
59	19	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → ((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^) ⊆ ℝ^)
60		supxrss 13308	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ⊆ ((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^) ∧ ((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^) ⊆ ℝ^) → sup(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < ))
61	58, 59, 60	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → sup(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < ))
62	61	adantr 482	. . . . . . . . . . . . 13 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ≠ ∅) → sup(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^*, < ))
63	18, 47, 22, 50, 62	xrletrd 13138	. . . . . . . . . . . 12 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ≠ ∅) → inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^*, < ))
64	14, 18, 22, 44, 63	xrletrd 13138	. . . . . . . . . . 11 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ≠ ∅) → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^*, < ))
65	64	ad5ant2345 1371	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ≠ ∅) → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^*, < ))
66	65	rexlimdva2 3158	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑙 ∈ ℝ) → (∃𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ^) ≠ ∅ → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^*, < )))
67	10, 66	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑙 ∈ ℝ) → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < ))
68	67	ralrimiva 3147	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → ∀𝑙 ∈ ℝ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < ))
69		nfv 1918	. . . . . . . . 9 ⊢ Ⅎ𝑙𝜑
70		xrltso 13117	. . . . . . . . . . 11 ⊢ < Or ℝ^*
71	70	supex 9455	. . . . . . . . . 10 ⊢ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ V
72	71	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℝ) → sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ V)
73		breq2 5152	. . . . . . . . 9 ⊢ (𝑦 = sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < ) → (inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ 𝑦 ↔ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < )))
74	69, 72, 73	ralrnmpt3 43950	. . . . . . . 8 ⊢ (𝜑 → (∀𝑦 ∈ ran (𝑙 ∈ ℝ ↦ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < ))inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ 𝑦 ↔ ∀𝑙 ∈ ℝ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < )))
75	74	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → (∀𝑦 ∈ ran (𝑙 ∈ ℝ ↦ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < ))inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ 𝑦 ↔ ∀𝑙 ∈ ℝ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < )))
76	68, 75	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → ∀𝑦 ∈ ran (𝑙 ∈ ℝ ↦ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < ))inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ 𝑦)
77		oveq1 7413	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑖 → (𝑙[,)+∞) = (𝑖[,)+∞))
78	77	imaeq2d 6058	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝑖 → (𝐹 “ (𝑙[,)+∞)) = (𝐹 “ (𝑖[,)+∞)))
79	78	ineq1d 4211	. . . . . . . . . . 11 ⊢ (𝑙 = 𝑖 → ((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^) = ((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^))
80	79	supeq1d 9438	. . . . . . . . . 10 ⊢ (𝑙 = 𝑖 → sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < ) = sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ))
81	80	cbvmptv 5261	. . . . . . . . 9 ⊢ (𝑙 ∈ ℝ ↦ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < )) = (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ))
82	81	rneqi 5935	. . . . . . . 8 ⊢ ran (𝑙 ∈ ℝ ↦ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < )) = ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ))
83	82	raleqi 3324	. . . . . . 7 ⊢ (∀𝑦 ∈ ran (𝑙 ∈ ℝ ↦ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < ))inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ 𝑦 ↔ ∀𝑦 ∈ ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ))inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ 𝑦)
84	83	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → (∀𝑦 ∈ ran (𝑙 ∈ ℝ ↦ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ^), ℝ^, < ))inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ 𝑦 ↔ ∀𝑦 ∈ ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ))inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ 𝑦))
85	76, 84	mpbid 231	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → ∀𝑦 ∈ ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ))inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ 𝑦)
86		supxrcl 13291	. . . . . . . . . 10 ⊢ (((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^) ⊆ ℝ^ → sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^*)
87	11, 86	ax-mp 5	. . . . . . . . 9 ⊢ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^*
88	87	rgenw 3066	. . . . . . . 8 ⊢ ∀𝑖 ∈ ℝ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^*
89		eqid 2733	. . . . . . . . 9 ⊢ (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )) = (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ))
90	89	rnmptss 7119	. . . . . . . 8 ⊢ (∀𝑖 ∈ ℝ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^* → ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )) ⊆ ℝ^*)
91	88, 90	ax-mp 5	. . . . . . 7 ⊢ ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )) ⊆ ℝ^*
92	91	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )) ⊆ ℝ^*)
93	13	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^*)
94		infxrgelb 13311	. . . . . 6 ⊢ ((ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )) ⊆ ℝ^* ∧ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^) → (inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ) ↔ ∀𝑦 ∈ ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ))inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ 𝑦))
95	92, 93, 94	syl2anc 585	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → (inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ) ↔ ∀𝑦 ∈ ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ))inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^*, < ) ≤ 𝑦))
96	85, 95	mpbird 257	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^*, < ))
97	96	ralrimiva 3147	. . 3 ⊢ (𝜑 → ∀𝑖 ∈ ℝ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^*, < ))
98		nfv 1918	. . . 4 ⊢ Ⅎ𝑖𝜑
99		nfcv 2904	. . . 4 ⊢ Ⅎ𝑖ℝ
100		nfmpt1 5256	. . . . . 6 ⊢ Ⅎ𝑖(𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ))
101	100	nfrn 5950	. . . . 5 ⊢ Ⅎ𝑖ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ))
102		nfcv 2904	. . . . 5 ⊢ Ⅎ𝑖ℝ^*
103		nfcv 2904	. . . . 5 ⊢ Ⅎ𝑖 <
104	101, 102, 103	nfinf 9474	. . . 4 ⊢ Ⅎ𝑖inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^*, < )
105		infxrcl 13309	. . . . . 6 ⊢ (ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )) ⊆ ℝ^* → inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ) ∈ ℝ^)
106	91, 105	ax-mp 5	. . . . 5 ⊢ inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ) ∈ ℝ^
107	106	a1i 11	. . . 4 ⊢ (𝜑 → inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ) ∈ ℝ^)
108	98, 99, 104, 93, 107	supxrleubrnmptf 44148	. . 3 ⊢ (𝜑 → (sup(ran (𝑖 ∈ ℝ ↦ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ) ≤ inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ) ↔ ∀𝑖 ∈ ℝ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ) ≤ inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^*, < )))
109	97, 108	mpbird 257	. 2 ⊢ (𝜑 → sup(ran (𝑖 ∈ ℝ ↦ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ) ≤ inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ))
110		liminflelimsuplem.1	. . . 4 ⊢ (𝜑 → 𝐹 ∈ 𝑉)
111		eqid 2733	. . . 4 ⊢ (𝑖 ∈ ℝ ↦ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )) = (𝑖 ∈ ℝ ↦ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < ))
112	110, 111	liminfvald 44467	. . 3 ⊢ (𝜑 → (lim inf‘𝐹) = sup(ran (𝑖 ∈ ℝ ↦ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^*, < ))
113	110, 89	limsupvald 44458	. . 3 ⊢ (𝜑 → (lim sup‘𝐹) = inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^*, < ))
114	112, 113	breq12d 5161	. 2 ⊢ (𝜑 → ((lim inf‘𝐹) ≤ (lim sup‘𝐹) ↔ sup(ran (𝑖 ∈ ℝ ↦ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ) ≤ inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < )))
115	109, 114	mpbird 257	1 ⊢ (𝜑 → (lim inf‘𝐹) ≤ (lim sup‘𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ≠ wne 2941 ∀wral 3062 ∃wrex 3071 Vcvv 3475 ∩ cin 3947 ⊆ wss 3948 ∅c0 4322 ifcif 4528 class class class wbr 5148 ↦ cmpt 5231 ran crn 5677 “ cima 5679 ‘cfv 6541 (class class class)co 7406 supcsup 9432 infcinf 9433 ℝcr 11106 +∞cpnf 11242 ℝ^*cxr 11244 < clt 11245 ≤ cle 11246 [,)cico 13323 lim supclsp 15411 lim infclsi 44454

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184 ax-pre-sup 11185

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-po 5588 df-so 5589 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-1st 7972 df-2nd 7973 df-er 8700 df-en 8937 df-dom 8938 df-sdom 8939 df-sup 9434 df-inf 9435 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-ico 13327 df-limsup 15412 df-liminf 44455

This theorem is referenced by: liminflelimsup 44479

W3C validator