This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limsupmnfuzlem

Description: The superior limit of a function is -oo if and only if every real number is the upper bound of the restriction of the function to a set of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupmnfuzlem.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
limsupmnfuzlem.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
limsupmnfuzlem.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
Assertion limsupmnfuzlem ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 limsupmnfuzlem.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 limsupmnfuzlem.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 limsupmnfuzlem.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
4 nfcv ⊢ Ⅎ 𝑗 𝐹
5 uzssre ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℝ
6 2 5 eqsstri ⊢ 𝑍 ⊆ ℝ
7 6 a1i ⊢ ( 𝜑 → 𝑍 ⊆ ℝ )
8 4 7 3 limsupmnf ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
9 breq1 ⊢ ( 𝑘 = 𝑖 → ( 𝑘 ≤ 𝑗 ↔ 𝑖 ≤ 𝑗 ) )
10 9 imbi1d ⊢ ( 𝑘 = 𝑖 → ( ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
11 10 ralbidv ⊢ ( 𝑘 = 𝑖 → ( ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∀ 𝑗 ∈ 𝑍 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
12 11 cbvrexvw ⊢ ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∃ 𝑖 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
13 12 biimpi ⊢ ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∃ 𝑖 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
14 iftrue ⊢ ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) = ( ⌈ ‘ 𝑖 ) )
15 14 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑀 ≤ ( ⌈ ‘ 𝑖 ) ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) = ( ⌈ ‘ 𝑖 ) )
16 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑀 ≤ ( ⌈ ‘ 𝑖 ) ) → 𝑀 ∈ ℤ )
17 ceilcl ⊢ ( 𝑖 ∈ ℝ → ( ⌈ ‘ 𝑖 ) ∈ ℤ )
18 17 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑀 ≤ ( ⌈ ‘ 𝑖 ) ) → ( ⌈ ‘ 𝑖 ) ∈ ℤ )
19 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑀 ≤ ( ⌈ ‘ 𝑖 ) ) → 𝑀 ≤ ( ⌈ ‘ 𝑖 ) )
20 2 16 18 19 eluzd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑀 ≤ ( ⌈ ‘ 𝑖 ) ) → ( ⌈ ‘ 𝑖 ) ∈ 𝑍 )
21 15 20 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑀 ≤ ( ⌈ ‘ 𝑖 ) ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ∈ 𝑍 )
22 iffalse ⊢ ( ¬ 𝑀 ≤ ( ⌈ ‘ 𝑖 ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) = 𝑀 )
23 22 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ ¬ 𝑀 ≤ ( ⌈ ‘ 𝑖 ) ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) = 𝑀 )
24 1 2 uzidd2 ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
25 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ ¬ 𝑀 ≤ ( ⌈ ‘ 𝑖 ) ) → 𝑀 ∈ 𝑍 )
26 23 25 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ ¬ 𝑀 ≤ ( ⌈ ‘ 𝑖 ) ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ∈ 𝑍 )
27 21 26 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ∈ 𝑍 )
28 27 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ∈ 𝑍 )
29 nfv ⊢ Ⅎ 𝑗 𝜑
30 nfv ⊢ Ⅎ 𝑗 𝑖 ∈ ℝ
31 nfra1 ⊢ Ⅎ 𝑗 ∀ 𝑗 ∈ 𝑍 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
32 29 30 31 nf3an ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
33 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ) → 𝑖 ∈ ℝ )
34 6 27 sselid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ∈ ℝ )
35 34 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ∈ ℝ )
36 eluzelre ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) → 𝑗 ∈ ℝ )
37 36 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ) → 𝑗 ∈ ℝ )
38 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → 𝑖 ∈ ℝ )
39 17 zred ⊢ ( 𝑖 ∈ ℝ → ( ⌈ ‘ 𝑖 ) ∈ ℝ )
40 39 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → ( ⌈ ‘ 𝑖 ) ∈ ℝ )
41 ceilge ⊢ ( 𝑖 ∈ ℝ → 𝑖 ≤ ( ⌈ ‘ 𝑖 ) )
42 41 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → 𝑖 ≤ ( ⌈ ‘ 𝑖 ) )
43 6 24 sselid ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
44 43 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → 𝑀 ∈ ℝ )
45 max2 ⊢ ( ( 𝑀 ∈ ℝ ∧ ( ⌈ ‘ 𝑖 ) ∈ ℝ ) → ( ⌈ ‘ 𝑖 ) ≤ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) )
46 44 40 45 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → ( ⌈ ‘ 𝑖 ) ≤ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) )
47 38 40 34 42 46 letrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → 𝑖 ≤ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) )
48 47 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ) → 𝑖 ≤ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) )
49 eluzle ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ≤ 𝑗 )
50 49 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ≤ 𝑗 )
51 33 35 37 48 50 letrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ) → 𝑖 ≤ 𝑗 )
52 51 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ) → 𝑖 ≤ 𝑗 )
53 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ) → ∀ 𝑗 ∈ 𝑍 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
54 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ) → 𝑀 ∈ ℤ )
55 eluzelz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) → 𝑗 ∈ ℤ )
56 55 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ) → 𝑗 ∈ ℤ )
57 44 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ) → 𝑀 ∈ ℝ )
58 max1 ⊢ ( ( 𝑀 ∈ ℝ ∧ ( ⌈ ‘ 𝑖 ) ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) )
59 43 39 58 syl2an ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) )
60 59 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ) → 𝑀 ≤ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) )
61 57 35 37 60 50 letrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ) → 𝑀 ≤ 𝑗 )
62 2 54 56 61 eluzd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ) → 𝑗 ∈ 𝑍 )
63 62 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ) → 𝑗 ∈ 𝑍 )
64 rspa ⊢ ( ( ∀ 𝑗 ∈ 𝑍 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ∧ 𝑗 ∈ 𝑍 ) → ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
65 53 63 64 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ) → ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
66 52 65 mpd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
67 66 ex ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ( 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
68 32 67 ralrimi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ∀ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
69 fveq2 ⊢ ( 𝑘 = if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) → ( ℤ≥ ‘ 𝑘 ) = ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) )
70 69 raleqdv ⊢ ( 𝑘 = if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) → ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
71 70 rspcev ⊢ ( ( if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑖 ) , ( ⌈ ‘ 𝑖 ) , 𝑀 ) ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
72 28 68 71 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
73 72 3exp ⊢ ( 𝜑 → ( 𝑖 ∈ ℝ → ( ∀ 𝑗 ∈ 𝑍 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
74 73 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
75 74 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
76 13 75 sylan2 ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
77 76 ex ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
78 rexss ⊢ ( 𝑍 ⊆ ℝ → ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∃ 𝑘 ∈ ℝ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
79 6 78 ax-mp ⊢ ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∃ 𝑘 ∈ ℝ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
80 79 biimpi ⊢ ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 → ∃ 𝑘 ∈ ℝ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
81 nfv ⊢ Ⅎ 𝑗 𝑘 ∈ 𝑍
82 nfra1 ⊢ Ⅎ 𝑗 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥
83 81 82 nfan ⊢ Ⅎ 𝑗 ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
84 simp1r ⊢ ( ( ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗 ) → ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
85 eqid ⊢ ( ℤ≥ ‘ 𝑘 ) = ( ℤ≥ ‘ 𝑘 )
86 2 eluzelz2 ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ )
87 86 3ad2ant1 ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗 ) → 𝑘 ∈ ℤ )
88 2 eluzelz2 ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ )
89 88 3ad2ant2 ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗 ) → 𝑗 ∈ ℤ )
90 simp3 ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗 ) → 𝑘 ≤ 𝑗 )
91 85 87 89 90 eluzd ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) )
92 91 3adant1r ⊢ ( ( ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) )
93 rspa ⊢ ( ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
94 84 92 93 syl2anc ⊢ ( ( ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
95 94 3exp ⊢ ( ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ( 𝑗 ∈ 𝑍 → ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
96 83 95 ralrimi ⊢ ( ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
97 96 a1i ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
98 97 reximdv ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℝ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
99 98 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ ℝ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
100 80 99 sylan2 ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
101 100 ex ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
102 77 101 impbid ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
103 102 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
104 8 103 bitrd ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )