Metamath Proof Explorer


Theorem limsupgre

Description: If a sequence of real numbers has upper bounded limit supremum, then all the partial suprema are real. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 12-Sep-2020)

Ref Expression
Hypotheses limsupval.1 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
limsupgre.z 𝑍 = ( ℤ𝑀 )
Assertion limsupgre ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) → 𝐺 : ℝ ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 limsupval.1 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
2 limsupgre.z 𝑍 = ( ℤ𝑀 )
3 xrltso < Or ℝ*
4 3 supex sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ V
5 4 a1i ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑘 ∈ ℝ ) → sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ V )
6 1 a1i ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) → 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
7 1 limsupgval ( 𝑎 ∈ ℝ → ( 𝐺𝑎 ) = sup ( ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
8 7 adantl ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( 𝐺𝑎 ) = sup ( ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
9 simpl3 ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( lim sup ‘ 𝐹 ) < +∞ )
10 uzssz ( ℤ𝑀 ) ⊆ ℤ
11 2 10 eqsstri 𝑍 ⊆ ℤ
12 zssre ℤ ⊆ ℝ
13 11 12 sstri 𝑍 ⊆ ℝ
14 13 a1i ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → 𝑍 ⊆ ℝ )
15 simpl2 ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → 𝐹 : 𝑍 ⟶ ℝ )
16 ressxr ℝ ⊆ ℝ*
17 fss ( ( 𝐹 : 𝑍 ⟶ ℝ ∧ ℝ ⊆ ℝ* ) → 𝐹 : 𝑍 ⟶ ℝ* )
18 15 16 17 sylancl ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → 𝐹 : 𝑍 ⟶ ℝ* )
19 pnfxr +∞ ∈ ℝ*
20 19 a1i ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → +∞ ∈ ℝ* )
21 1 limsuplt ( ( 𝑍 ⊆ ℝ ∧ 𝐹 : 𝑍 ⟶ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( lim sup ‘ 𝐹 ) < +∞ ↔ ∃ 𝑛 ∈ ℝ ( 𝐺𝑛 ) < +∞ ) )
22 14 18 20 21 syl3anc ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( ( lim sup ‘ 𝐹 ) < +∞ ↔ ∃ 𝑛 ∈ ℝ ( 𝐺𝑛 ) < +∞ ) )
23 9 22 mpbid ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ∃ 𝑛 ∈ ℝ ( 𝐺𝑛 ) < +∞ )
24 fzfi ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ∈ Fin
25 15 adantr ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) → 𝐹 : 𝑍 ⟶ ℝ )
26 elfzuz ( 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) → 𝑚 ∈ ( ℤ𝑀 ) )
27 26 2 eleqtrrdi ( 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) → 𝑚𝑍 )
28 ffvelrn ( ( 𝐹 : 𝑍 ⟶ ℝ ∧ 𝑚𝑍 ) → ( 𝐹𝑚 ) ∈ ℝ )
29 25 27 28 syl2an ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ) → ( 𝐹𝑚 ) ∈ ℝ )
30 29 ralrimiva ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) → ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ∈ ℝ )
31 fimaxre3 ( ( ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ∈ Fin ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ∈ ℝ ) → ∃ 𝑟 ∈ ℝ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 )
32 24 30 31 sylancr ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) → ∃ 𝑟 ∈ ℝ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 )
33 simpr ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ )
34 33 ad2antrr ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → 𝑎 ∈ ℝ )
35 1 limsupgf 𝐺 : ℝ ⟶ ℝ*
36 35 ffvelrni ( 𝑎 ∈ ℝ → ( 𝐺𝑎 ) ∈ ℝ* )
37 34 36 syl ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → ( 𝐺𝑎 ) ∈ ℝ* )
38 simprl ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → 𝑟 ∈ ℝ )
39 16 38 sselid ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → 𝑟 ∈ ℝ* )
40 simprl ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) → 𝑛 ∈ ℝ )
41 40 adantr ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → 𝑛 ∈ ℝ )
42 35 ffvelrni ( 𝑛 ∈ ℝ → ( 𝐺𝑛 ) ∈ ℝ* )
43 41 42 syl ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → ( 𝐺𝑛 ) ∈ ℝ* )
44 39 43 ifcld ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ∈ ℝ* )
45 19 a1i ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → +∞ ∈ ℝ* )
46 40 ad2antrr ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → 𝑛 ∈ ℝ )
47 13 a1i ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → 𝑍 ⊆ ℝ )
48 47 sselda ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → 𝑖 ∈ ℝ )
49 43 xrleidd ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → ( 𝐺𝑛 ) ≤ ( 𝐺𝑛 ) )
50 18 ad2antrr ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → 𝐹 : 𝑍 ⟶ ℝ* )
51 1 limsupgle ( ( ( 𝑍 ⊆ ℝ ∧ 𝐹 : 𝑍 ⟶ ℝ* ) ∧ 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) ∈ ℝ* ) → ( ( 𝐺𝑛 ) ≤ ( 𝐺𝑛 ) ↔ ∀ 𝑖𝑍 ( 𝑛𝑖 → ( 𝐹𝑖 ) ≤ ( 𝐺𝑛 ) ) ) )
52 47 50 41 43 51 syl211anc ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → ( ( 𝐺𝑛 ) ≤ ( 𝐺𝑛 ) ↔ ∀ 𝑖𝑍 ( 𝑛𝑖 → ( 𝐹𝑖 ) ≤ ( 𝐺𝑛 ) ) ) )
53 49 52 mpbid ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → ∀ 𝑖𝑍 ( 𝑛𝑖 → ( 𝐹𝑖 ) ≤ ( 𝐺𝑛 ) ) )
54 53 r19.21bi ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → ( 𝑛𝑖 → ( 𝐹𝑖 ) ≤ ( 𝐺𝑛 ) ) )
55 54 imp ( ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) ∧ 𝑛𝑖 ) → ( 𝐹𝑖 ) ≤ ( 𝐺𝑛 ) )
56 46 42 syl ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → ( 𝐺𝑛 ) ∈ ℝ* )
57 39 adantr ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → 𝑟 ∈ ℝ* )
58 xrmax1 ( ( ( 𝐺𝑛 ) ∈ ℝ*𝑟 ∈ ℝ* ) → ( 𝐺𝑛 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) )
59 56 57 58 syl2anc ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → ( 𝐺𝑛 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) )
60 50 ffvelrnda ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → ( 𝐹𝑖 ) ∈ ℝ* )
61 44 adantr ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ∈ ℝ* )
62 xrletr ( ( ( 𝐹𝑖 ) ∈ ℝ* ∧ ( 𝐺𝑛 ) ∈ ℝ* ∧ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ∈ ℝ* ) → ( ( ( 𝐹𝑖 ) ≤ ( 𝐺𝑛 ) ∧ ( 𝐺𝑛 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ) → ( 𝐹𝑖 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ) )
63 60 56 61 62 syl3anc ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → ( ( ( 𝐹𝑖 ) ≤ ( 𝐺𝑛 ) ∧ ( 𝐺𝑛 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ) → ( 𝐹𝑖 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ) )
64 59 63 mpan2d ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → ( ( 𝐹𝑖 ) ≤ ( 𝐺𝑛 ) → ( 𝐹𝑖 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ) )
65 64 adantr ( ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) ∧ 𝑛𝑖 ) → ( ( 𝐹𝑖 ) ≤ ( 𝐺𝑛 ) → ( 𝐹𝑖 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ) )
66 55 65 mpd ( ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) ∧ 𝑛𝑖 ) → ( 𝐹𝑖 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) )
67 fveq2 ( 𝑚 = 𝑖 → ( 𝐹𝑚 ) = ( 𝐹𝑖 ) )
68 67 breq1d ( 𝑚 = 𝑖 → ( ( 𝐹𝑚 ) ≤ 𝑟 ↔ ( 𝐹𝑖 ) ≤ 𝑟 ) )
69 simprr ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 )
70 69 ad2antrr ( ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) ∧ 𝑖𝑛 ) → ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 )
71 simpr ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → 𝑖𝑍 )
72 71 2 eleqtrdi ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → 𝑖 ∈ ( ℤ𝑀 ) )
73 41 flcld ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → ( ⌊ ‘ 𝑛 ) ∈ ℤ )
74 73 adantr ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → ( ⌊ ‘ 𝑛 ) ∈ ℤ )
75 elfz5 ( ( 𝑖 ∈ ( ℤ𝑀 ) ∧ ( ⌊ ‘ 𝑛 ) ∈ ℤ ) → ( 𝑖 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ↔ 𝑖 ≤ ( ⌊ ‘ 𝑛 ) ) )
76 72 74 75 syl2anc ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → ( 𝑖 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ↔ 𝑖 ≤ ( ⌊ ‘ 𝑛 ) ) )
77 11 71 sselid ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → 𝑖 ∈ ℤ )
78 flge ( ( 𝑛 ∈ ℝ ∧ 𝑖 ∈ ℤ ) → ( 𝑖𝑛𝑖 ≤ ( ⌊ ‘ 𝑛 ) ) )
79 46 77 78 syl2anc ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → ( 𝑖𝑛𝑖 ≤ ( ⌊ ‘ 𝑛 ) ) )
80 76 79 bitr4d ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → ( 𝑖 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ↔ 𝑖𝑛 ) )
81 80 biimpar ( ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) ∧ 𝑖𝑛 ) → 𝑖 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) )
82 68 70 81 rspcdva ( ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) ∧ 𝑖𝑛 ) → ( 𝐹𝑖 ) ≤ 𝑟 )
83 xrmax2 ( ( ( 𝐺𝑛 ) ∈ ℝ*𝑟 ∈ ℝ* ) → 𝑟 ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) )
84 43 39 83 syl2anc ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → 𝑟 ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) )
85 84 adantr ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → 𝑟 ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) )
86 xrletr ( ( ( 𝐹𝑖 ) ∈ ℝ*𝑟 ∈ ℝ* ∧ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ∈ ℝ* ) → ( ( ( 𝐹𝑖 ) ≤ 𝑟𝑟 ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ) → ( 𝐹𝑖 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ) )
87 60 57 61 86 syl3anc ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → ( ( ( 𝐹𝑖 ) ≤ 𝑟𝑟 ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ) → ( 𝐹𝑖 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ) )
88 85 87 mpan2d ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → ( ( 𝐹𝑖 ) ≤ 𝑟 → ( 𝐹𝑖 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ) )
89 88 adantr ( ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) ∧ 𝑖𝑛 ) → ( ( 𝐹𝑖 ) ≤ 𝑟 → ( 𝐹𝑖 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ) )
90 82 89 mpd ( ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) ∧ 𝑖𝑛 ) → ( 𝐹𝑖 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) )
91 46 48 66 90 lecasei ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → ( 𝐹𝑖 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) )
92 91 a1d ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖𝑍 ) → ( 𝑎𝑖 → ( 𝐹𝑖 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ) )
93 92 ralrimiva ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → ∀ 𝑖𝑍 ( 𝑎𝑖 → ( 𝐹𝑖 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ) )
94 1 limsupgle ( ( ( 𝑍 ⊆ ℝ ∧ 𝐹 : 𝑍 ⟶ ℝ* ) ∧ 𝑎 ∈ ℝ ∧ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ∈ ℝ* ) → ( ( 𝐺𝑎 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ↔ ∀ 𝑖𝑍 ( 𝑎𝑖 → ( 𝐹𝑖 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ) ) )
95 47 50 34 44 94 syl211anc ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → ( ( 𝐺𝑎 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ↔ ∀ 𝑖𝑍 ( 𝑎𝑖 → ( 𝐹𝑖 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) ) ) )
96 93 95 mpbird ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → ( 𝐺𝑎 ) ≤ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) )
97 38 ltpnfd ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → 𝑟 < +∞ )
98 simplrr ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → ( 𝐺𝑛 ) < +∞ )
99 breq1 ( 𝑟 = if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) → ( 𝑟 < +∞ ↔ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) < +∞ ) )
100 breq1 ( ( 𝐺𝑛 ) = if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) → ( ( 𝐺𝑛 ) < +∞ ↔ if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) < +∞ ) )
101 99 100 ifboth ( ( 𝑟 < +∞ ∧ ( 𝐺𝑛 ) < +∞ ) → if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) < +∞ )
102 97 98 101 syl2anc ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → if ( ( 𝐺𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺𝑛 ) ) < +∞ )
103 37 44 45 96 102 xrlelttrd ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹𝑚 ) ≤ 𝑟 ) ) → ( 𝐺𝑎 ) < +∞ )
104 32 103 rexlimddv ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺𝑛 ) < +∞ ) ) → ( 𝐺𝑎 ) < +∞ )
105 23 104 rexlimddv ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( 𝐺𝑎 ) < +∞ )
106 8 105 eqbrtrrd ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → sup ( ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) < +∞ )
107 imassrn ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ⊆ ran 𝐹
108 15 frnd ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ran 𝐹 ⊆ ℝ )
109 107 108 sstrid ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ⊆ ℝ )
110 109 16 sstrdi ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ⊆ ℝ* )
111 df-ss ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ⊆ ℝ* ↔ ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) = ( 𝐹 “ ( 𝑎 [,) +∞ ) ) )
112 110 111 sylib ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) = ( 𝐹 “ ( 𝑎 [,) +∞ ) ) )
113 112 109 eqsstrd ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ )
114 simpl1 ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → 𝑀 ∈ ℤ )
115 flcl ( 𝑎 ∈ ℝ → ( ⌊ ‘ 𝑎 ) ∈ ℤ )
116 115 adantl ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( ⌊ ‘ 𝑎 ) ∈ ℤ )
117 116 peano2zd ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( ( ⌊ ‘ 𝑎 ) + 1 ) ∈ ℤ )
118 117 114 ifcld ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ℤ )
119 114 zred ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → 𝑀 ∈ ℝ )
120 117 zred ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( ( ⌊ ‘ 𝑎 ) + 1 ) ∈ ℝ )
121 max1 ( ( 𝑀 ∈ ℝ ∧ ( ( ⌊ ‘ 𝑎 ) + 1 ) ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) )
122 119 120 121 syl2anc ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) )
123 eluz2 ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ( ℤ𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ℤ ∧ 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ) )
124 114 118 122 123 syl3anbrc ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ( ℤ𝑀 ) )
125 124 2 eleqtrrdi ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ 𝑍 )
126 15 fdmd ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → dom 𝐹 = 𝑍 )
127 125 126 eleqtrrd ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ dom 𝐹 )
128 118 zred ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ℝ )
129 fllep1 ( 𝑎 ∈ ℝ → 𝑎 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) )
130 129 adantl ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → 𝑎 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) )
131 max2 ( ( 𝑀 ∈ ℝ ∧ ( ( ⌊ ‘ 𝑎 ) + 1 ) ∈ ℝ ) → ( ( ⌊ ‘ 𝑎 ) + 1 ) ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) )
132 119 120 131 syl2anc ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( ( ⌊ ‘ 𝑎 ) + 1 ) ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) )
133 33 120 128 130 132 letrd ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → 𝑎 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) )
134 elicopnf ( 𝑎 ∈ ℝ → ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ( 𝑎 [,) +∞ ) ↔ ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ℝ ∧ 𝑎 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ) ) )
135 134 adantl ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ( 𝑎 [,) +∞ ) ↔ ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ℝ ∧ 𝑎 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ) ) )
136 128 133 135 mpbir2and ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ( 𝑎 [,) +∞ ) )
137 inelcm ( ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ dom 𝐹 ∧ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ( 𝑎 [,) +∞ ) ) → ( dom 𝐹 ∩ ( 𝑎 [,) +∞ ) ) ≠ ∅ )
138 127 136 137 syl2anc ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( dom 𝐹 ∩ ( 𝑎 [,) +∞ ) ) ≠ ∅ )
139 imadisj ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) = ∅ ↔ ( dom 𝐹 ∩ ( 𝑎 [,) +∞ ) ) = ∅ )
140 139 necon3bii ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ≠ ∅ ↔ ( dom 𝐹 ∩ ( 𝑎 [,) +∞ ) ) ≠ ∅ )
141 138 140 sylibr ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ≠ ∅ )
142 112 141 eqnetrd ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ )
143 supxrre1 ( ( ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ ∧ ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) → ( sup ( ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ ↔ sup ( ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) < +∞ ) )
144 113 142 143 syl2anc ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( sup ( ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ ↔ sup ( ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) < +∞ ) )
145 106 144 mpbird ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → sup ( ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ )
146 8 145 eqeltrd ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( 𝐺𝑎 ) ∈ ℝ )
147 5 6 146 fmpt2d ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) → 𝐺 : ℝ ⟶ ℝ )