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

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 ffvelcdm ⊢ ( ( 𝐹 : 𝑍 ⟶ ℝ ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ℝ )
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 ffvelcdmi ⊢ ( 𝑎 ∈ ℝ → ( 𝐺 ‘ 𝑎 ) ∈ ℝ* )
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 ffvelcdmi ⊢ ( 𝑛 ∈ ℝ → ( 𝐺 ‘ 𝑛 ) ∈ ℝ* )
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 ffvelcdmda ⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( 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 dfss2 ⊢ ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ⊆ ℝ* ↔ ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) = ( 𝐹 “ ( 𝑎 [,) +∞ ) ) )
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 ‘ 𝐹 ) < +∞ ) → 𝐺 : ℝ ⟶ ℝ )