liminfreuzlem

Description: Given a function on the reals, its inferior limit is real if and only if two condition holds: 1. there is a real number that is greater than or equal to the function, infinitely often; 2. there is a real number that is smaller than or equal to the function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminfreuzlem.1	$⊢ \underline{Ⅎ} j F$
	liminfreuzlem.2	$⊢ φ \to M \in ℤ$
	liminfreuzlem.3	$⊢ Z = ℤ_{\geq M}$
	liminfreuzlem.4	$⊢ φ \to F : Z ⟶ ℝ$
Assertion	liminfreuzlem	$⊢ φ \to (lim inf (F) \in ℝ \leftrightarrow (\exists x \in ℝ \forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq x \land \exists x \in ℝ \forall j \in Z x \leq F (j)))$

Proof

Step	Hyp	Ref	Expression
1		liminfreuzlem.1	$⊢ \underline{Ⅎ} j F$
2		liminfreuzlem.2	$⊢ φ \to M \in ℤ$
3		liminfreuzlem.3	$⊢ Z = ℤ_{\geq M}$
4		liminfreuzlem.4	$⊢ φ \to F : Z ⟶ ℝ$
5		nfv	$⊢ Ⅎ j φ$
6	5 1 2 3 4	liminfvaluz4	$⊢ φ \to lim inf (F) = - lim sup ((j \in Z ⟼ - F (j)))$
7	6	eleq1d	$⊢ φ \to (lim inf (F) \in ℝ \leftrightarrow - lim sup ((j \in Z ⟼ - F (j))) \in ℝ)$
8	3	fvexi	$⊢ Z \in V$
9	8	mptex	$⊢ (j \in Z ⟼ - F (j)) \in V$
10		limsupcl	$⊢ (j \in Z ⟼ - F (j)) \in V \to lim sup ((j \in Z ⟼ - F (j))) \in ℝ^{*}$
11	9 10	ax-mp	$⊢ lim sup ((j \in Z ⟼ - F (j))) \in ℝ^{*}$
12	11	a1i	$⊢ φ \to lim sup ((j \in Z ⟼ - F (j))) \in ℝ^{*}$
13	12	xnegred	$⊢ φ \to (lim sup ((j \in Z ⟼ - F (j))) \in ℝ \leftrightarrow - lim sup ((j \in Z ⟼ - F (j))) \in ℝ)$
14	7 13	bitr4d	$⊢ φ \to (lim inf (F) \in ℝ \leftrightarrow lim sup ((j \in Z ⟼ - F (j))) \in ℝ)$
15	4	ffvelcdmda	$⊢ (φ \land j \in Z) \to F (j) \in ℝ$
16	15	renegcld	$⊢ (φ \land j \in Z) \to - F (j) \in ℝ$
17	5 2 3 16	limsupreuzmpt	$⊢ φ \to (lim sup ((j \in Z ⟼ - F (j))) \in ℝ \leftrightarrow (\exists y \in ℝ \forall k \in Z \exists j \in ℤ_{\geq k} y \leq - F (j) \land \exists y \in ℝ \forall j \in Z - F (j) \leq y))$
18		renegcl	$⊢ y \in ℝ \to - y \in ℝ$
19	18	ad2antlr	$⊢ ((φ \land y \in ℝ) \land \forall k \in Z \exists j \in ℤ_{\geq k} y \leq - F (j)) \to - y \in ℝ$
20		simpllr	$⊢ (((φ \land y \in ℝ) \land k \in Z) \land j \in ℤ_{\geq k}) \to y \in ℝ$
21	4	ad2antrr	$⊢ ((φ \land k \in Z) \land j \in ℤ_{\geq k}) \to F : Z ⟶ ℝ$
22	3	uztrn2	$⊢ (k \in Z \land j \in ℤ_{\geq k}) \to j \in Z$
23	22	adantll	$⊢ ((φ \land k \in Z) \land j \in ℤ_{\geq k}) \to j \in Z$
24	21 23	ffvelcdmd	$⊢ ((φ \land k \in Z) \land j \in ℤ_{\geq k}) \to F (j) \in ℝ$
25	24	adantllr	$⊢ (((φ \land y \in ℝ) \land k \in Z) \land j \in ℤ_{\geq k}) \to F (j) \in ℝ$
26	20 25	leneg2d	$⊢ (((φ \land y \in ℝ) \land k \in Z) \land j \in ℤ_{\geq k}) \to (y \leq - F (j) \leftrightarrow F (j) \leq - y)$
27	26	rexbidva	$⊢ ((φ \land y \in ℝ) \land k \in Z) \to (\exists j \in ℤ_{\geq k} y \leq - F (j) \leftrightarrow \exists j \in ℤ_{\geq k} F (j) \leq - y)$
28	27	ralbidva	$⊢ (φ \land y \in ℝ) \to (\forall k \in Z \exists j \in ℤ_{\geq k} y \leq - F (j) \leftrightarrow \forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq - y)$
29	28	biimpd	$⊢ (φ \land y \in ℝ) \to (\forall k \in Z \exists j \in ℤ_{\geq k} y \leq - F (j) \to \forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq - y)$
30	29	imp	$⊢ ((φ \land y \in ℝ) \land \forall k \in Z \exists j \in ℤ_{\geq k} y \leq - F (j)) \to \forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq - y$
31		breq2	$⊢ x = - y \to (F (j) \leq x \leftrightarrow F (j) \leq - y)$
32	31	rexbidv	$⊢ x = - y \to (\exists j \in ℤ_{\geq k} F (j) \leq x \leftrightarrow \exists j \in ℤ_{\geq k} F (j) \leq - y)$
33	32	ralbidv	$⊢ x = - y \to (\forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq x \leftrightarrow \forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq - y)$
34	33	rspcev	$⊢ (- y \in ℝ \land \forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq - y) \to \exists x \in ℝ \forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq x$
35	19 30 34	syl2anc	$⊢ ((φ \land y \in ℝ) \land \forall k \in Z \exists j \in ℤ_{\geq k} y \leq - F (j)) \to \exists x \in ℝ \forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq x$
36	35	rexlimdva2	$⊢ φ \to (\exists y \in ℝ \forall k \in Z \exists j \in ℤ_{\geq k} y \leq - F (j) \to \exists x \in ℝ \forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq x)$
37		renegcl	$⊢ x \in ℝ \to - x \in ℝ$
38	37	ad2antlr	$⊢ ((φ \land x \in ℝ) \land \forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq x) \to - x \in ℝ$
39	24	adantllr	$⊢ (((φ \land x \in ℝ) \land k \in Z) \land j \in ℤ_{\geq k}) \to F (j) \in ℝ$
40		simpllr	$⊢ (((φ \land x \in ℝ) \land k \in Z) \land j \in ℤ_{\geq k}) \to x \in ℝ$
41	39 40	lenegd	$⊢ (((φ \land x \in ℝ) \land k \in Z) \land j \in ℤ_{\geq k}) \to (F (j) \leq x \leftrightarrow - x \leq - F (j))$
42	41	rexbidva	$⊢ ((φ \land x \in ℝ) \land k \in Z) \to (\exists j \in ℤ_{\geq k} F (j) \leq x \leftrightarrow \exists j \in ℤ_{\geq k} - x \leq - F (j))$
43	42	ralbidva	$⊢ (φ \land x \in ℝ) \to (\forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq x \leftrightarrow \forall k \in Z \exists j \in ℤ_{\geq k} - x \leq - F (j))$
44	43	biimpd	$⊢ (φ \land x \in ℝ) \to (\forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq x \to \forall k \in Z \exists j \in ℤ_{\geq k} - x \leq - F (j))$
45	44	imp	$⊢ ((φ \land x \in ℝ) \land \forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq x) \to \forall k \in Z \exists j \in ℤ_{\geq k} - x \leq - F (j)$
46		breq1	$⊢ y = - x \to (y \leq - F (j) \leftrightarrow - x \leq - F (j))$
47	46	rexbidv	$⊢ y = - x \to (\exists j \in ℤ_{\geq k} y \leq - F (j) \leftrightarrow \exists j \in ℤ_{\geq k} - x \leq - F (j))$
48	47	ralbidv	$⊢ y = - x \to (\forall k \in Z \exists j \in ℤ_{\geq k} y \leq - F (j) \leftrightarrow \forall k \in Z \exists j \in ℤ_{\geq k} - x \leq - F (j))$
49	48	rspcev	$⊢ (- x \in ℝ \land \forall k \in Z \exists j \in ℤ_{\geq k} - x \leq - F (j)) \to \exists y \in ℝ \forall k \in Z \exists j \in ℤ_{\geq k} y \leq - F (j)$
50	38 45 49	syl2anc	$⊢ ((φ \land x \in ℝ) \land \forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq x) \to \exists y \in ℝ \forall k \in Z \exists j \in ℤ_{\geq k} y \leq - F (j)$
51	50	rexlimdva2	$⊢ φ \to (\exists x \in ℝ \forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq x \to \exists y \in ℝ \forall k \in Z \exists j \in ℤ_{\geq k} y \leq - F (j))$
52	36 51	impbid	$⊢ φ \to (\exists y \in ℝ \forall k \in Z \exists j \in ℤ_{\geq k} y \leq - F (j) \leftrightarrow \exists x \in ℝ \forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq x)$
53	18	ad2antlr	$⊢ ((φ \land y \in ℝ) \land \forall j \in Z - F (j) \leq y) \to - y \in ℝ$
54	15	adantlr	$⊢ ((φ \land y \in ℝ) \land j \in Z) \to F (j) \in ℝ$
55		simplr	$⊢ ((φ \land y \in ℝ) \land j \in Z) \to y \in ℝ$
56	54 55	leneg3d	$⊢ ((φ \land y \in ℝ) \land j \in Z) \to (- F (j) \leq y \leftrightarrow - y \leq F (j))$
57	56	ralbidva	$⊢ (φ \land y \in ℝ) \to (\forall j \in Z - F (j) \leq y \leftrightarrow \forall j \in Z - y \leq F (j))$
58	57	biimpd	$⊢ (φ \land y \in ℝ) \to (\forall j \in Z - F (j) \leq y \to \forall j \in Z - y \leq F (j))$
59	58	imp	$⊢ ((φ \land y \in ℝ) \land \forall j \in Z - F (j) \leq y) \to \forall j \in Z - y \leq F (j)$
60		breq1	$⊢ x = - y \to (x \leq F (j) \leftrightarrow - y \leq F (j))$
61	60	ralbidv	$⊢ x = - y \to (\forall j \in Z x \leq F (j) \leftrightarrow \forall j \in Z - y \leq F (j))$
62	61	rspcev	$⊢ (- y \in ℝ \land \forall j \in Z - y \leq F (j)) \to \exists x \in ℝ \forall j \in Z x \leq F (j)$
63	53 59 62	syl2anc	$⊢ ((φ \land y \in ℝ) \land \forall j \in Z - F (j) \leq y) \to \exists x \in ℝ \forall j \in Z x \leq F (j)$
64	63	rexlimdva2	$⊢ φ \to (\exists y \in ℝ \forall j \in Z - F (j) \leq y \to \exists x \in ℝ \forall j \in Z x \leq F (j))$
65	37	ad2antlr	$⊢ ((φ \land x \in ℝ) \land \forall j \in Z x \leq F (j)) \to - x \in ℝ$
66		simplr	$⊢ ((φ \land x \in ℝ) \land j \in Z) \to x \in ℝ$
67	15	adantlr	$⊢ ((φ \land x \in ℝ) \land j \in Z) \to F (j) \in ℝ$
68	66 67	lenegd	$⊢ ((φ \land x \in ℝ) \land j \in Z) \to (x \leq F (j) \leftrightarrow - F (j) \leq - x)$
69	68	ralbidva	$⊢ (φ \land x \in ℝ) \to (\forall j \in Z x \leq F (j) \leftrightarrow \forall j \in Z - F (j) \leq - x)$
70	69	biimpd	$⊢ (φ \land x \in ℝ) \to (\forall j \in Z x \leq F (j) \to \forall j \in Z - F (j) \leq - x)$
71	70	imp	$⊢ ((φ \land x \in ℝ) \land \forall j \in Z x \leq F (j)) \to \forall j \in Z - F (j) \leq - x$
72		brralrspcev	$⊢ (- x \in ℝ \land \forall j \in Z - F (j) \leq - x) \to \exists y \in ℝ \forall j \in Z - F (j) \leq y$
73	65 71 72	syl2anc	$⊢ ((φ \land x \in ℝ) \land \forall j \in Z x \leq F (j)) \to \exists y \in ℝ \forall j \in Z - F (j) \leq y$
74	73	rexlimdva2	$⊢ φ \to (\exists x \in ℝ \forall j \in Z x \leq F (j) \to \exists y \in ℝ \forall j \in Z - F (j) \leq y)$
75	64 74	impbid	$⊢ φ \to (\exists y \in ℝ \forall j \in Z - F (j) \leq y \leftrightarrow \exists x \in ℝ \forall j \in Z x \leq F (j))$
76	52 75	anbi12d	$⊢ φ \to ((\exists y \in ℝ \forall k \in Z \exists j \in ℤ_{\geq k} y \leq - F (j) \land \exists y \in ℝ \forall j \in Z - F (j) \leq y) \leftrightarrow (\exists x \in ℝ \forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq x \land \exists x \in ℝ \forall j \in Z x \leq F (j)))$
77	17 76	bitrd	$⊢ φ \to (lim sup ((j \in Z ⟼ - F (j))) \in ℝ \leftrightarrow (\exists x \in ℝ \forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq x \land \exists x \in ℝ \forall j \in Z x \leq F (j)))$
78	14 77	bitrd	$⊢ φ \to (lim inf (F) \in ℝ \leftrightarrow (\exists x \in ℝ \forall k \in Z \exists j \in ℤ_{\geq k} F (j) \leq x \land \exists x \in ℝ \forall j \in Z x \leq F (j)))$

Metamath Proof Explorer

Theorem liminfreuzlem

Proof