Metamath Proof Explorer


Theorem 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 𝑗 𝐹
liminfreuzlem.2 ( 𝜑𝑀 ∈ ℤ )
liminfreuzlem.3 𝑍 = ( ℤ𝑀 )
liminfreuzlem.4 ( 𝜑𝐹 : 𝑍 ⟶ ℝ )
Assertion liminfreuzlem ( 𝜑 → ( ( lim inf ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗𝑍 𝑥 ≤ ( 𝐹𝑗 ) ) ) )

Proof

Step Hyp Ref Expression
1 liminfreuzlem.1 𝑗 𝐹
2 liminfreuzlem.2 ( 𝜑𝑀 ∈ ℤ )
3 liminfreuzlem.3 𝑍 = ( ℤ𝑀 )
4 liminfreuzlem.4 ( 𝜑𝐹 : 𝑍 ⟶ ℝ )
5 nfv 𝑗 𝜑
6 5 1 2 3 4 liminfvaluz4 ( 𝜑 → ( lim inf ‘ 𝐹 ) = -𝑒 ( lim sup ‘ ( 𝑗𝑍 ↦ - ( 𝐹𝑗 ) ) ) )
7 6 eleq1d ( 𝜑 → ( ( lim inf ‘ 𝐹 ) ∈ ℝ ↔ -𝑒 ( lim sup ‘ ( 𝑗𝑍 ↦ - ( 𝐹𝑗 ) ) ) ∈ ℝ ) )
8 3 fvexi 𝑍 ∈ V
9 8 mptex ( 𝑗𝑍 ↦ - ( 𝐹𝑗 ) ) ∈ V
10 limsupcl ( ( 𝑗𝑍 ↦ - ( 𝐹𝑗 ) ) ∈ V → ( lim sup ‘ ( 𝑗𝑍 ↦ - ( 𝐹𝑗 ) ) ) ∈ ℝ* )
11 9 10 ax-mp ( lim sup ‘ ( 𝑗𝑍 ↦ - ( 𝐹𝑗 ) ) ) ∈ ℝ*
12 11 a1i ( 𝜑 → ( lim sup ‘ ( 𝑗𝑍 ↦ - ( 𝐹𝑗 ) ) ) ∈ ℝ* )
13 12 xnegred ( 𝜑 → ( ( lim sup ‘ ( 𝑗𝑍 ↦ - ( 𝐹𝑗 ) ) ) ∈ ℝ ↔ -𝑒 ( lim sup ‘ ( 𝑗𝑍 ↦ - ( 𝐹𝑗 ) ) ) ∈ ℝ ) )
14 7 13 bitr4d ( 𝜑 → ( ( lim inf ‘ 𝐹 ) ∈ ℝ ↔ ( lim sup ‘ ( 𝑗𝑍 ↦ - ( 𝐹𝑗 ) ) ) ∈ ℝ ) )
15 4 ffvelrnda ( ( 𝜑𝑗𝑍 ) → ( 𝐹𝑗 ) ∈ ℝ )
16 15 renegcld ( ( 𝜑𝑗𝑍 ) → - ( 𝐹𝑗 ) ∈ ℝ )
17 5 2 3 16 limsupreuzmpt ( 𝜑 → ( ( lim sup ‘ ( 𝑗𝑍 ↦ - ( 𝐹𝑗 ) ) ) ∈ ℝ ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑦 ≤ - ( 𝐹𝑗 ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑗𝑍 - ( 𝐹𝑗 ) ≤ 𝑦 ) ) )
18 renegcl ( 𝑦 ∈ ℝ → - 𝑦 ∈ ℝ )
19 18 ad2antlr ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑦 ≤ - ( 𝐹𝑗 ) ) → - 𝑦 ∈ ℝ )
20 simpllr ( ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑘𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑘 ) ) → 𝑦 ∈ ℝ )
21 4 ad2antrr ( ( ( 𝜑𝑘𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑘 ) ) → 𝐹 : 𝑍 ⟶ ℝ )
22 3 uztrn2 ( ( 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ) → 𝑗𝑍 )
23 22 adantll ( ( ( 𝜑𝑘𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑘 ) ) → 𝑗𝑍 )
24 21 23 ffvelrnd ( ( ( 𝜑𝑘𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑘 ) ) → ( 𝐹𝑗 ) ∈ ℝ )
25 24 adantllr ( ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑘𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑘 ) ) → ( 𝐹𝑗 ) ∈ ℝ )
26 20 25 leneg2d ( ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑘𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑘 ) ) → ( 𝑦 ≤ - ( 𝐹𝑗 ) ↔ ( 𝐹𝑗 ) ≤ - 𝑦 ) )
27 26 rexbidva ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑘𝑍 ) → ( ∃ 𝑗 ∈ ( ℤ𝑘 ) 𝑦 ≤ - ( 𝐹𝑗 ) ↔ ∃ 𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ - 𝑦 ) )
28 27 ralbidva ( ( 𝜑𝑦 ∈ ℝ ) → ( ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑦 ≤ - ( 𝐹𝑗 ) ↔ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ - 𝑦 ) )
29 28 biimpd ( ( 𝜑𝑦 ∈ ℝ ) → ( ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑦 ≤ - ( 𝐹𝑗 ) → ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ - 𝑦 ) )
30 29 imp ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑦 ≤ - ( 𝐹𝑗 ) ) → ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ - 𝑦 )
31 breq2 ( 𝑥 = - 𝑦 → ( ( 𝐹𝑗 ) ≤ 𝑥 ↔ ( 𝐹𝑗 ) ≤ - 𝑦 ) )
32 31 rexbidv ( 𝑥 = - 𝑦 → ( ∃ 𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ↔ ∃ 𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ - 𝑦 ) )
33 32 ralbidv ( 𝑥 = - 𝑦 → ( ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ↔ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ - 𝑦 ) )
34 33 rspcev ( ( - 𝑦 ∈ ℝ ∧ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ - 𝑦 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 )
35 19 30 34 syl2anc ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑦 ≤ - ( 𝐹𝑗 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 )
36 35 rexlimdva2 ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑦 ≤ - ( 𝐹𝑗 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ) )
37 renegcl ( 𝑥 ∈ ℝ → - 𝑥 ∈ ℝ )
38 37 ad2antlr ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ) → - 𝑥 ∈ ℝ )
39 24 adantllr ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑘𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑘 ) ) → ( 𝐹𝑗 ) ∈ ℝ )
40 simpllr ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑘𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑘 ) ) → 𝑥 ∈ ℝ )
41 39 40 lenegd ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑘𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑘 ) ) → ( ( 𝐹𝑗 ) ≤ 𝑥 ↔ - 𝑥 ≤ - ( 𝐹𝑗 ) ) )
42 41 rexbidva ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑘𝑍 ) → ( ∃ 𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ↔ ∃ 𝑗 ∈ ( ℤ𝑘 ) - 𝑥 ≤ - ( 𝐹𝑗 ) ) )
43 42 ralbidva ( ( 𝜑𝑥 ∈ ℝ ) → ( ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ↔ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) - 𝑥 ≤ - ( 𝐹𝑗 ) ) )
44 43 biimpd ( ( 𝜑𝑥 ∈ ℝ ) → ( ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 → ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) - 𝑥 ≤ - ( 𝐹𝑗 ) ) )
45 44 imp ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ) → ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) - 𝑥 ≤ - ( 𝐹𝑗 ) )
46 breq1 ( 𝑦 = - 𝑥 → ( 𝑦 ≤ - ( 𝐹𝑗 ) ↔ - 𝑥 ≤ - ( 𝐹𝑗 ) ) )
47 46 rexbidv ( 𝑦 = - 𝑥 → ( ∃ 𝑗 ∈ ( ℤ𝑘 ) 𝑦 ≤ - ( 𝐹𝑗 ) ↔ ∃ 𝑗 ∈ ( ℤ𝑘 ) - 𝑥 ≤ - ( 𝐹𝑗 ) ) )
48 47 ralbidv ( 𝑦 = - 𝑥 → ( ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑦 ≤ - ( 𝐹𝑗 ) ↔ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) - 𝑥 ≤ - ( 𝐹𝑗 ) ) )
49 48 rspcev ( ( - 𝑥 ∈ ℝ ∧ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) - 𝑥 ≤ - ( 𝐹𝑗 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑦 ≤ - ( 𝐹𝑗 ) )
50 38 45 49 syl2anc ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑦 ≤ - ( 𝐹𝑗 ) )
51 50 rexlimdva2 ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 → ∃ 𝑦 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑦 ≤ - ( 𝐹𝑗 ) ) )
52 36 51 impbid ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑦 ≤ - ( 𝐹𝑗 ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ) )
53 18 ad2antlr ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ∀ 𝑗𝑍 - ( 𝐹𝑗 ) ≤ 𝑦 ) → - 𝑦 ∈ ℝ )
54 15 adantlr ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗𝑍 ) → ( 𝐹𝑗 ) ∈ ℝ )
55 simplr ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗𝑍 ) → 𝑦 ∈ ℝ )
56 54 55 leneg3d ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗𝑍 ) → ( - ( 𝐹𝑗 ) ≤ 𝑦 ↔ - 𝑦 ≤ ( 𝐹𝑗 ) ) )
57 56 ralbidva ( ( 𝜑𝑦 ∈ ℝ ) → ( ∀ 𝑗𝑍 - ( 𝐹𝑗 ) ≤ 𝑦 ↔ ∀ 𝑗𝑍 - 𝑦 ≤ ( 𝐹𝑗 ) ) )
58 57 biimpd ( ( 𝜑𝑦 ∈ ℝ ) → ( ∀ 𝑗𝑍 - ( 𝐹𝑗 ) ≤ 𝑦 → ∀ 𝑗𝑍 - 𝑦 ≤ ( 𝐹𝑗 ) ) )
59 58 imp ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ∀ 𝑗𝑍 - ( 𝐹𝑗 ) ≤ 𝑦 ) → ∀ 𝑗𝑍 - 𝑦 ≤ ( 𝐹𝑗 ) )
60 breq1 ( 𝑥 = - 𝑦 → ( 𝑥 ≤ ( 𝐹𝑗 ) ↔ - 𝑦 ≤ ( 𝐹𝑗 ) ) )
61 60 ralbidv ( 𝑥 = - 𝑦 → ( ∀ 𝑗𝑍 𝑥 ≤ ( 𝐹𝑗 ) ↔ ∀ 𝑗𝑍 - 𝑦 ≤ ( 𝐹𝑗 ) ) )
62 61 rspcev ( ( - 𝑦 ∈ ℝ ∧ ∀ 𝑗𝑍 - 𝑦 ≤ ( 𝐹𝑗 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗𝑍 𝑥 ≤ ( 𝐹𝑗 ) )
63 53 59 62 syl2anc ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ∀ 𝑗𝑍 - ( 𝐹𝑗 ) ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗𝑍 𝑥 ≤ ( 𝐹𝑗 ) )
64 63 rexlimdva2 ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑗𝑍 - ( 𝐹𝑗 ) ≤ 𝑦 → ∃ 𝑥 ∈ ℝ ∀ 𝑗𝑍 𝑥 ≤ ( 𝐹𝑗 ) ) )
65 37 ad2antlr ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ ∀ 𝑗𝑍 𝑥 ≤ ( 𝐹𝑗 ) ) → - 𝑥 ∈ ℝ )
66 simplr ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝑍 ) → 𝑥 ∈ ℝ )
67 15 adantlr ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝑍 ) → ( 𝐹𝑗 ) ∈ ℝ )
68 66 67 lenegd ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝑍 ) → ( 𝑥 ≤ ( 𝐹𝑗 ) ↔ - ( 𝐹𝑗 ) ≤ - 𝑥 ) )
69 68 ralbidva ( ( 𝜑𝑥 ∈ ℝ ) → ( ∀ 𝑗𝑍 𝑥 ≤ ( 𝐹𝑗 ) ↔ ∀ 𝑗𝑍 - ( 𝐹𝑗 ) ≤ - 𝑥 ) )
70 69 biimpd ( ( 𝜑𝑥 ∈ ℝ ) → ( ∀ 𝑗𝑍 𝑥 ≤ ( 𝐹𝑗 ) → ∀ 𝑗𝑍 - ( 𝐹𝑗 ) ≤ - 𝑥 ) )
71 70 imp ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ ∀ 𝑗𝑍 𝑥 ≤ ( 𝐹𝑗 ) ) → ∀ 𝑗𝑍 - ( 𝐹𝑗 ) ≤ - 𝑥 )
72 brralrspcev ( ( - 𝑥 ∈ ℝ ∧ ∀ 𝑗𝑍 - ( 𝐹𝑗 ) ≤ - 𝑥 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑗𝑍 - ( 𝐹𝑗 ) ≤ 𝑦 )
73 65 71 72 syl2anc ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ ∀ 𝑗𝑍 𝑥 ≤ ( 𝐹𝑗 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑗𝑍 - ( 𝐹𝑗 ) ≤ 𝑦 )
74 73 rexlimdva2 ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑗𝑍 𝑥 ≤ ( 𝐹𝑗 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑗𝑍 - ( 𝐹𝑗 ) ≤ 𝑦 ) )
75 64 74 impbid ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑗𝑍 - ( 𝐹𝑗 ) ≤ 𝑦 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗𝑍 𝑥 ≤ ( 𝐹𝑗 ) ) )
76 52 75 anbi12d ( 𝜑 → ( ( ∃ 𝑦 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑦 ≤ - ( 𝐹𝑗 ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑗𝑍 - ( 𝐹𝑗 ) ≤ 𝑦 ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗𝑍 𝑥 ≤ ( 𝐹𝑗 ) ) ) )
77 17 76 bitrd ( 𝜑 → ( ( lim sup ‘ ( 𝑗𝑍 ↦ - ( 𝐹𝑗 ) ) ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗𝑍 𝑥 ≤ ( 𝐹𝑗 ) ) ) )
78 14 77 bitrd ( 𝜑 → ( ( lim inf ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗𝑍 𝑥 ≤ ( 𝐹𝑗 ) ) ) )