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 sseldi ( ( ∀ 𝑘 ∈ ℝ ∃ 𝑗𝑍 ( 𝑘𝑗𝑥 ≤ ( 𝐹𝑗 ) ) ∧ 𝑘𝑍 ) → 𝑘 ∈ ℝ )
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 sseldi ( ( 𝜑𝑦 ∈ ℝ ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ∈ ℝ )
72 71 adantr ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ) → if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ∈ ℝ )
73 69 zred ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑗 ∈ ( ℤ ‘ if ( 𝑀 ≤ ( ⌈ ‘ 𝑦 ) , ( ⌈ ‘ 𝑦 ) , 𝑀 ) ) ) → 𝑗 ∈ ℝ )
74 6 49 sseldi ( 𝜑𝑀 ∈ ℝ )
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 ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑥 ≤ ( 𝐹𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ) ) )