Metamath Proof Explorer

Theorem limsupre3uzlem

Description: Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is less than or equal to the function, infinitely often; 2. there is a real number that is eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 limsupre3uzlem.1 ⊢ Ⅎ 𝑗 𝐹
2 limsupre3uzlem.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 limsupre3uzlem.3 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 limsupre3uzlem.4 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
5 uzssre ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℝ
6 3 5 eqsstri ⊢ 𝑍 ⊆ ℝ
7 6 a1i ⊢ ( 𝜑 → 𝑍 ⊆ ℝ )
8 1 7 4 limsupre3 ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ) )
9 breq1 ⊢ ( 𝑦 = 𝑘 → ( 𝑦 ≤ 𝑗 ↔ 𝑘 ≤ 𝑗 ) )
10 9 anbi1d ⊢ ( 𝑦 = 𝑘 → ( ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
11 10 rexbidv ⊢ ( 𝑦 = 𝑘 → ( ∃ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
12 11 cbvralvw ⊢ ( ∀ 𝑦 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
13 12 biimpi ⊢ ( ∀ 𝑦 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
14 nfra1 ⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
15 simpr ⊢ ( ( ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝑍 )
16 6 15 sselid ⊢ ( ( ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ℝ )
17 rspa ⊢ ( ( ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ∈ ℝ ) → ∃ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
18 16 17 syldan ⊢ ( ( ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ∈ 𝑍 ) → ∃ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
19 nfv ⊢ Ⅎ 𝑗 𝑘 ∈ 𝑍
20 nfre1 ⊢ Ⅎ 𝑗 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 )
21 eqid ⊢ ( ℤ≥ ‘ 𝑘 ) = ( ℤ≥ ‘ 𝑘 )
22 3 eluzelz2 ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ )
23 22 3ad2ant1 ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗 ) → 𝑘 ∈ ℤ )
24 3 eluzelz2 ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ )
25 24 3ad2ant2 ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗 ) → 𝑗 ∈ ℤ )
26 simp3 ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗 ) → 𝑘 ≤ 𝑗 )
27 21 23 25 26 eluzd ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) )
28 27 3adant3r ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ 𝑍 ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) )
29 simp3r ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ 𝑍 ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
30 rspe ⊢ ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
31 28 29 30 syl2anc ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ 𝑍 ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
32 31 3exp ⊢ ( 𝑘 ∈ 𝑍 → ( 𝑗 ∈ 𝑍 → ( ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
33 19 20 32 rexlimd ⊢ ( 𝑘 ∈ 𝑍 → ( ∃ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
34 33 imp ⊢ ( ( 𝑘 ∈ 𝑍 ∧ ∃ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
35 15 18 34 syl2anc ⊢ ( ( ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ∈ 𝑍 ) → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
36 14 35 ralrimia ⊢ ( ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
37 13 36 syl ⊢ ( ∀ 𝑦 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
38 37 a1i ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
39 iftrue ⊢ ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) = ( ⌈ ‘ 𝑦 ) )
40 39 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑀 ≤ ( ⌈ ‘ 𝑦 ) ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) = ( ⌈ ‘ 𝑦 ) )
41 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑀 ≤ ( ⌈ ‘ 𝑦 ) ) → 𝑀 ∈ ℤ )
42 ceilcl ⊢ ( 𝑦 ∈ ℝ → ( ⌈ ‘ 𝑦 ) ∈ ℤ )
43 42 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑀 ≤ ( ⌈ ‘ 𝑦 ) ) → ( ⌈ ‘ 𝑦 ) ∈ ℤ )
44 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑀 ≤ ( ⌈ ‘ 𝑦 ) ) → 𝑀 ≤ ( ⌈ ‘ 𝑦 ) )
45 3 41 43 44 eluzd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑀 ≤ ( ⌈ ‘ 𝑦 ) ) → ( ⌈ ‘ 𝑦 ) ∈ 𝑍 )
46 40 45 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑀 ≤ ( ⌈ ‘ 𝑦 ) ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ∈ 𝑍 )
47 iffalse ⊢ ( ¬ 𝑀 ≤ ( ⌈ ‘ 𝑦 ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) = 𝑀 )
48 47 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑀 ≤ ( ⌈ ‘ 𝑦 ) ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) = 𝑀 )
49 2 3 uzidd2 ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
50 49 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑀 ≤ ( ⌈ ‘ 𝑦 ) ) → 𝑀 ∈ 𝑍 )
51 48 50 eqeltrd ⊢ ( ( 𝜑 ∧ ¬ 𝑀 ≤ ( ⌈ ‘ 𝑦 ) ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ∈ 𝑍 )
52 51 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ¬ 𝑀 ≤ ( ⌈ ‘ 𝑦 ) ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ∈ 𝑍 )
53 46 52 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ∈ 𝑍 )
54 53 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑦 ∈ ℝ ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ∈ 𝑍 )
55 simplr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑦 ∈ ℝ ) → ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
56 fveq2 ⊢ ( 𝑘 = if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) → ( ℤ≥ ‘ 𝑘 ) = ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) )
57 56 rexeqdv ⊢ ( 𝑘 = if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
58 57 rspcva ⊢ ( ( if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ∈ 𝑍 ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
59 54 55 58 syl2anc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑦 ∈ ℝ ) → ∃ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
60 nfv ⊢ Ⅎ 𝑗 𝜑
61 19 nfci ⊢ Ⅎ 𝑗 𝑍
62 61 20 nfralw ⊢ Ⅎ 𝑗 ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 )
63 60 62 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
64 nfv ⊢ Ⅎ 𝑗 𝑦 ∈ ℝ
65 63 64 nfan ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑦 ∈ ℝ )
66 nfre1 ⊢ Ⅎ 𝑗 ∃ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
67 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ) → 𝑀 ∈ ℤ )
68 eluzelz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) → 𝑗 ∈ ℤ )
69 68 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ) → 𝑗 ∈ ℤ )
70 67 zred ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ) → 𝑀 ∈ ℝ )
71 6 53 sselid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ∈ ℝ )
72 71 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ∈ ℝ )
73 69 zred ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ) → 𝑗 ∈ ℝ )
74 6 49 sselid ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑀 ∈ ℝ )
76 42 zred ⊢ ( 𝑦 ∈ ℝ → ( ⌈ ‘ 𝑦 ) ∈ ℝ )
77 76 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ⌈ ‘ 𝑦 ) ∈ ℝ )
78 max1 ⊢ ( ( 𝑀 ∈ ℝ ∧ ( ⌈ ‘ 𝑦 ) ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) )
79 75 77 78 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) )
80 79 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ) → 𝑀 ≤ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) )
81 eluzle ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ≤ 𝑗 )
82 81 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ≤ 𝑗 )
83 70 72 73 80 82 letrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ) → 𝑀 ≤ 𝑗 )
84 3 67 69 83 eluzd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ) → 𝑗 ∈ 𝑍 )
85 84 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → 𝑗 ∈ 𝑍 )
86 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ) → 𝑦 ∈ ℝ )
87 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
88 ceilge ⊢ ( 𝑦 ∈ ℝ → 𝑦 ≤ ( ⌈ ‘ 𝑦 ) )
89 88 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ≤ ( ⌈ ‘ 𝑦 ) )
90 max2 ⊢ ( ( 𝑀 ∈ ℝ ∧ ( ⌈ ‘ 𝑦 ) ∈ ℝ ) → ( ⌈ ‘ 𝑦 ) ≤ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) )
91 75 77 90 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ⌈ ‘ 𝑦 ) ≤ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) )
92 87 77 71 89 91 letrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ≤ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) )
93 92 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ) → 𝑦 ≤ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) )
94 86 72 73 93 82 letrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ) → 𝑦 ≤ 𝑗 )
95 94 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → 𝑦 ≤ 𝑗 )
96 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
97 95 96 jca ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
98 rspe ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ∃ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
99 85 97 98 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
100 99 3exp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) → ( 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) → ∃ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) ) )
101 100 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑦 ∈ ℝ ) → ( 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) → ( 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) → ∃ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) ) )
102 65 66 101 rexlimd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) → ∃ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
103 59 102 mpd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑦 ∈ ℝ ) → ∃ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
104 103 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∀ 𝑦 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
105 104 ex ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) → ∀ 𝑦 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
106 38 105 impbid ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
107 106 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
108 53 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ∈ 𝑍 )
109 60 64 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑦 ∈ ℝ )
110 nfra1 ⊢ Ⅎ 𝑗 ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
111 109 110 nfan ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
112 94 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ) → 𝑦 ≤ 𝑗 )
113 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ) → ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
114 84 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ) → 𝑗 ∈ 𝑍 )
115 rspa ⊢ ( ( ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ∧ 𝑗 ∈ 𝑍 ) → ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
116 113 114 115 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ) → ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
117 112 116 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ∧ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
118 117 ex ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ( 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
119 111 118 ralrimi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ∀ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
120 56 raleqdv ⊢ ( 𝑘 = if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) → ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
121 120 rspcev ⊢ ( ( if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
122 108 119 121 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
123 122 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
124 6 sseli ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℝ )
125 124 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → 𝑘 ∈ ℝ )
126 nfra1 ⊢ Ⅎ 𝑗 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥
127 19 126 nfan ⊢ Ⅎ 𝑗 ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
128 simp1r ⊢ ( ( ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗 ) → ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
129 27 3adant1r ⊢ ( ( ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) )
130 rspa ⊢ ( ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
131 128 129 130 syl2anc ⊢ ( ( ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
132 131 3exp ⊢ ( ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ( 𝑗 ∈ 𝑍 → ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
133 127 132 ralrimi ⊢ ( ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
134 133 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
135 9 rspceaimv ⊢ ( ( 𝑘 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
136 125 134 135 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
137 136 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 → ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
138 123 137 impbid ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
139 138 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
140 107 139 anbi12d ⊢ ( 𝜑 → ( ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑦 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
141 8 140 bitrd ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )