Theorem limsupbnd2

Description: If a sequence is eventually greater than A , then the limsup is also greater than A . (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 12-Sep-2020)

	Ref	Expression
Hypotheses	limsupbnd.1	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
	limsupbnd.2	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℝ* )
	limsupbnd.3	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	limsupbnd2.4	⊢ ( 𝜑 → sup ( 𝐵 , ℝ* , < ) = +∞ )
	limsupbnd2.5	⊢ ( 𝜑 → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ) )
Assertion	limsupbnd2	⊢ ( 𝜑 → 𝐴 ≤ ( lim sup ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		limsupbnd.1	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
2		limsupbnd.2	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℝ* )
3		limsupbnd.3	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
4		limsupbnd2.4	⊢ ( 𝜑 → sup ( 𝐵 , ℝ* , < ) = +∞ )
5		limsupbnd2.5	⊢ ( 𝜑 → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ) )
6		ressxr	⊢ ℝ ⊆ ℝ*
7	1 6	sstrdi	⊢ ( 𝜑 → 𝐵 ⊆ ℝ* )
8		supxrunb1	⊢ ( 𝐵 ⊆ ℝ* → ( ∀ 𝑛 ∈ ℝ ∃ 𝑗 ∈ 𝐵 𝑛 ≤ 𝑗 ↔ sup ( 𝐵 , ℝ* , < ) = +∞ ) )
9	7 8	syl	⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ℝ ∃ 𝑗 ∈ 𝐵 𝑛 ≤ 𝑗 ↔ sup ( 𝐵 , ℝ* , < ) = +∞ ) )
10	4 9	mpbird	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℝ ∃ 𝑗 ∈ 𝐵 𝑛 ≤ 𝑗 )
11		ifcl	⊢ ( ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ∈ ℝ )
12		breq1	⊢ ( 𝑛 = if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) → ( 𝑛 ≤ 𝑗 ↔ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 ) )
13	12	rexbidv	⊢ ( 𝑛 = if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) → ( ∃ 𝑗 ∈ 𝐵 𝑛 ≤ 𝑗 ↔ ∃ 𝑗 ∈ 𝐵 if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 ) )
14	13	rspccva	⊢ ( ( ∀ 𝑛 ∈ ℝ ∃ 𝑗 ∈ 𝐵 𝑛 ≤ 𝑗 ∧ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ∈ ℝ ) → ∃ 𝑗 ∈ 𝐵 if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 )
15	10 11 14	syl2an	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) → ∃ 𝑗 ∈ 𝐵 if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 )
16		r19.29	⊢ ( ( ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ ∃ 𝑗 ∈ 𝐵 if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 ) → ∃ 𝑗 ∈ 𝐵 ( ( 𝑘 ≤ 𝑗 → 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 ) )
17		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → 𝑘 ∈ ℝ )
18		simprl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) → 𝑚 ∈ ℝ )
19	18	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → 𝑚 ∈ ℝ )
20		max1	⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑚 ∈ ℝ ) → 𝑘 ≤ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) )
21	17 19 20	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → 𝑘 ≤ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) )
22	19 17 11	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ∈ ℝ )
23	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) → 𝐵 ⊆ ℝ )
24	23	sselda	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → 𝑗 ∈ ℝ )
25		letr	⊢ ( ( 𝑘 ∈ ℝ ∧ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ∈ ℝ ∧ 𝑗 ∈ ℝ ) → ( ( 𝑘 ≤ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ∧ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 ) → 𝑘 ≤ 𝑗 ) )
26	17 22 24 25	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ( 𝑘 ≤ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ∧ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 ) → 𝑘 ≤ 𝑗 ) )
27	21 26	mpand	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → ( if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 → 𝑘 ≤ 𝑗 ) )
28	27	imim1d	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ( 𝑘 ≤ 𝑗 → 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ) → ( if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 → 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
29	28	impd	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ( ( 𝑘 ≤ 𝑗 → 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 ) → 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ) )
30		max2	⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑚 ∈ ℝ ) → 𝑚 ≤ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) )
31	17 19 30	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → 𝑚 ≤ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) )
32		letr	⊢ ( ( 𝑚 ∈ ℝ ∧ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ∈ ℝ ∧ 𝑗 ∈ ℝ ) → ( ( 𝑚 ≤ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ∧ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 ) → 𝑚 ≤ 𝑗 ) )
33	19 22 24 32	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ( 𝑚 ≤ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ∧ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 ) → 𝑚 ≤ 𝑗 ) )
34	31 33	mpand	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → ( if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 → 𝑚 ≤ 𝑗 ) )
35	34	adantld	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ( ( 𝑘 ≤ 𝑗 → 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 ) → 𝑚 ≤ 𝑗 ) )
36		eqid	⊢ ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
37	36	limsupgf	⊢ ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) : ℝ ⟶ ℝ*
38	37	ffvelcdmi	⊢ ( 𝑚 ∈ ℝ → ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ∈ ℝ* )
39	38	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ∈ ℝ* )
40	39	xrleidd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) )
41	40	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) → ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) )
42	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) → 𝐹 : 𝐵 ⟶ ℝ* )
43	18 38	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) → ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ∈ ℝ* )
44	36	limsupgle	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝑚 ∈ ℝ ∧ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ∈ ℝ* ) → ( ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ↔ ∀ 𝑗 ∈ 𝐵 ( 𝑚 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ) ) )
45	23 42 18 43 44	syl211anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) → ( ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ↔ ∀ 𝑗 ∈ 𝐵 ( 𝑚 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ) ) )
46	41 45	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) → ∀ 𝑗 ∈ 𝐵 ( 𝑚 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ) )
47	46	r19.21bi	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → ( 𝑚 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ) )
48	35 47	syld	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ( ( 𝑘 ≤ 𝑗 → 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ) )
49	29 48	jcad	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ( ( 𝑘 ≤ 𝑗 → 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 ) → ( 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ) ) )
50	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → 𝐴 ∈ ℝ* )
51	42	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
52	43	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ∈ ℝ* )
53		xrletr	⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℝ* ∧ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ∈ ℝ* ) → ( ( 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ) → 𝐴 ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ) )
54	50 51 52 53	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ( 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ( 𝐹 ‘ 𝑗 ) ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ) → 𝐴 ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ) )
55	49 54	syld	⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ( ( 𝑘 ≤ 𝑗 → 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 ) → 𝐴 ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ) )
56	55	rexlimdva	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) → ( ∃ 𝑗 ∈ 𝐵 ( ( 𝑘 ≤ 𝑗 → 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 ) → 𝐴 ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ) )
57	16 56	syl5	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) → ( ( ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ ∃ 𝑗 ∈ 𝐵 if ( 𝑘 ≤ 𝑚 , 𝑚 , 𝑘 ) ≤ 𝑗 ) → 𝐴 ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ) )
58	15 57	mpan2d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ ) ) → ( ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ) → 𝐴 ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ) )
59	58	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ) → 𝐴 ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ) )
60	59	rexlimdva	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ) → 𝐴 ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ) )
61	60	ralrimdva	⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → 𝐴 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∀ 𝑚 ∈ ℝ 𝐴 ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ) )
62	5 61	mpd	⊢ ( 𝜑 → ∀ 𝑚 ∈ ℝ 𝐴 ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) )
63	36	limsuple	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝐴 ≤ ( lim sup ‘ 𝐹 ) ↔ ∀ 𝑚 ∈ ℝ 𝐴 ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ) )
64	1 2 3 63	syl3anc	⊢ ( 𝜑 → ( 𝐴 ≤ ( lim sup ‘ 𝐹 ) ↔ ∀ 𝑚 ∈ ℝ 𝐴 ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑚 ) ) )
65	62 64	mpbird	⊢ ( 𝜑 → 𝐴 ≤ ( lim sup ‘ 𝐹 ) )