MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  limsupbnd2 Structured version   Visualization version   GIF version

Theorem limsupbnd2 15431
Description: If a sequence is eventually greater than 𝐴, then the limsup is also greater than 𝐴. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.)
Hypotheses
Ref Expression
limsupbnd.1 (πœ‘ β†’ 𝐡 βŠ† ℝ)
limsupbnd.2 (πœ‘ β†’ 𝐹:π΅βŸΆβ„*)
limsupbnd.3 (πœ‘ β†’ 𝐴 ∈ ℝ*)
limsupbnd2.4 (πœ‘ β†’ sup(𝐡, ℝ*, < ) = +∞)
limsupbnd2.5 (πœ‘ β†’ βˆƒπ‘˜ ∈ ℝ βˆ€π‘— ∈ 𝐡 (π‘˜ ≀ 𝑗 β†’ 𝐴 ≀ (πΉβ€˜π‘—)))
Assertion
Ref Expression
limsupbnd2 (πœ‘ β†’ 𝐴 ≀ (lim supβ€˜πΉ))
Distinct variable groups:   𝑗,π‘˜,𝐴   𝐡,𝑗,π‘˜   𝑗,𝐹,π‘˜   πœ‘,𝑗,π‘˜

Proof of Theorem limsupbnd2
Dummy variables π‘š 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 limsupbnd2.5 . . 3 (πœ‘ β†’ βˆƒπ‘˜ ∈ ℝ βˆ€π‘— ∈ 𝐡 (π‘˜ ≀ 𝑗 β†’ 𝐴 ≀ (πΉβ€˜π‘—)))
2 limsupbnd2.4 . . . . . . . . 9 (πœ‘ β†’ sup(𝐡, ℝ*, < ) = +∞)
3 limsupbnd.1 . . . . . . . . . . 11 (πœ‘ β†’ 𝐡 βŠ† ℝ)
4 ressxr 11262 . . . . . . . . . . 11 ℝ βŠ† ℝ*
53, 4sstrdi 3993 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 βŠ† ℝ*)
6 supxrunb1 13302 . . . . . . . . . 10 (𝐡 βŠ† ℝ* β†’ (βˆ€π‘› ∈ ℝ βˆƒπ‘— ∈ 𝐡 𝑛 ≀ 𝑗 ↔ sup(𝐡, ℝ*, < ) = +∞))
75, 6syl 17 . . . . . . . . 9 (πœ‘ β†’ (βˆ€π‘› ∈ ℝ βˆƒπ‘— ∈ 𝐡 𝑛 ≀ 𝑗 ↔ sup(𝐡, ℝ*, < ) = +∞))
82, 7mpbird 256 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘› ∈ ℝ βˆƒπ‘— ∈ 𝐡 𝑛 ≀ 𝑗)
9 ifcl 4572 . . . . . . . 8 ((π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ) β†’ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ∈ ℝ)
10 breq1 5150 . . . . . . . . . 10 (𝑛 = if(π‘˜ ≀ π‘š, π‘š, π‘˜) β†’ (𝑛 ≀ 𝑗 ↔ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗))
1110rexbidv 3176 . . . . . . . . 9 (𝑛 = if(π‘˜ ≀ π‘š, π‘š, π‘˜) β†’ (βˆƒπ‘— ∈ 𝐡 𝑛 ≀ 𝑗 ↔ βˆƒπ‘— ∈ 𝐡 if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗))
1211rspccva 3610 . . . . . . . 8 ((βˆ€π‘› ∈ ℝ βˆƒπ‘— ∈ 𝐡 𝑛 ≀ 𝑗 ∧ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ∈ ℝ) β†’ βˆƒπ‘— ∈ 𝐡 if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗)
138, 9, 12syl2an 594 . . . . . . 7 ((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) β†’ βˆƒπ‘— ∈ 𝐡 if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗)
14 r19.29 3112 . . . . . . . 8 ((βˆ€π‘— ∈ 𝐡 (π‘˜ ≀ 𝑗 β†’ 𝐴 ≀ (πΉβ€˜π‘—)) ∧ βˆƒπ‘— ∈ 𝐡 if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗) β†’ βˆƒπ‘— ∈ 𝐡 ((π‘˜ ≀ 𝑗 β†’ 𝐴 ≀ (πΉβ€˜π‘—)) ∧ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗))
15 simplrr 774 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ π‘˜ ∈ ℝ)
16 simprl 767 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) β†’ π‘š ∈ ℝ)
1716adantr 479 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ π‘š ∈ ℝ)
18 max1 13168 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ ℝ ∧ π‘š ∈ ℝ) β†’ π‘˜ ≀ if(π‘˜ ≀ π‘š, π‘š, π‘˜))
1915, 17, 18syl2anc 582 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ π‘˜ ≀ if(π‘˜ ≀ π‘š, π‘š, π‘˜))
2017, 15, 9syl2anc 582 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ∈ ℝ)
213adantr 479 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) β†’ 𝐡 βŠ† ℝ)
2221sselda 3981 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ 𝑗 ∈ ℝ)
23 letr 11312 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ ℝ ∧ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ∈ ℝ ∧ 𝑗 ∈ ℝ) β†’ ((π‘˜ ≀ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ∧ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗) β†’ π‘˜ ≀ 𝑗))
2415, 20, 22, 23syl3anc 1369 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ ((π‘˜ ≀ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ∧ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗) β†’ π‘˜ ≀ 𝑗))
2519, 24mpand 691 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ (if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗 β†’ π‘˜ ≀ 𝑗))
2625imim1d 82 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ ((π‘˜ ≀ 𝑗 β†’ 𝐴 ≀ (πΉβ€˜π‘—)) β†’ (if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗 β†’ 𝐴 ≀ (πΉβ€˜π‘—))))
2726impd 409 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ (((π‘˜ ≀ 𝑗 β†’ 𝐴 ≀ (πΉβ€˜π‘—)) ∧ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗) β†’ 𝐴 ≀ (πΉβ€˜π‘—)))
28 max2 13170 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ ℝ ∧ π‘š ∈ ℝ) β†’ π‘š ≀ if(π‘˜ ≀ π‘š, π‘š, π‘˜))
2915, 17, 28syl2anc 582 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ π‘š ≀ if(π‘˜ ≀ π‘š, π‘š, π‘˜))
30 letr 11312 . . . . . . . . . . . . . . 15 ((π‘š ∈ ℝ ∧ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ∈ ℝ ∧ 𝑗 ∈ ℝ) β†’ ((π‘š ≀ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ∧ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗) β†’ π‘š ≀ 𝑗))
3117, 20, 22, 30syl3anc 1369 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ ((π‘š ≀ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ∧ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗) β†’ π‘š ≀ 𝑗))
3229, 31mpand 691 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ (if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗 β†’ π‘š ≀ 𝑗))
3332adantld 489 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ (((π‘˜ ≀ 𝑗 β†’ 𝐴 ≀ (πΉβ€˜π‘—)) ∧ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗) β†’ π‘š ≀ 𝑗))
34 eqid 2730 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < )) = (𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))
3534limsupgf 15423 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < )):β„βŸΆβ„*
3635ffvelcdmi 7084 . . . . . . . . . . . . . . . . 17 (π‘š ∈ ℝ β†’ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š) ∈ ℝ*)
3736adantl 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š) ∈ ℝ*)
3837xrleidd 13135 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š) ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š))
3938adantrr 713 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) β†’ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š) ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š))
40 limsupbnd.2 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐹:π΅βŸΆβ„*)
4140adantr 479 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) β†’ 𝐹:π΅βŸΆβ„*)
4216, 36syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) β†’ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š) ∈ ℝ*)
4334limsupgle 15425 . . . . . . . . . . . . . . 15 (((𝐡 βŠ† ℝ ∧ 𝐹:π΅βŸΆβ„*) ∧ π‘š ∈ ℝ ∧ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š) ∈ ℝ*) β†’ (((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š) ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š) ↔ βˆ€π‘— ∈ 𝐡 (π‘š ≀ 𝑗 β†’ (πΉβ€˜π‘—) ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š))))
4421, 41, 16, 42, 43syl211anc 1374 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) β†’ (((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š) ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š) ↔ βˆ€π‘— ∈ 𝐡 (π‘š ≀ 𝑗 β†’ (πΉβ€˜π‘—) ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š))))
4539, 44mpbid 231 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) β†’ βˆ€π‘— ∈ 𝐡 (π‘š ≀ 𝑗 β†’ (πΉβ€˜π‘—) ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š)))
4645r19.21bi 3246 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ (π‘š ≀ 𝑗 β†’ (πΉβ€˜π‘—) ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š)))
4733, 46syld 47 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ (((π‘˜ ≀ 𝑗 β†’ 𝐴 ≀ (πΉβ€˜π‘—)) ∧ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗) β†’ (πΉβ€˜π‘—) ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š)))
4827, 47jcad 511 . . . . . . . . . 10 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ (((π‘˜ ≀ 𝑗 β†’ 𝐴 ≀ (πΉβ€˜π‘—)) ∧ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗) β†’ (𝐴 ≀ (πΉβ€˜π‘—) ∧ (πΉβ€˜π‘—) ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š))))
49 limsupbnd.3 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 ∈ ℝ*)
5049ad2antrr 722 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ 𝐴 ∈ ℝ*)
5141ffvelcdmda 7085 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ (πΉβ€˜π‘—) ∈ ℝ*)
5242adantr 479 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š) ∈ ℝ*)
53 xrletr 13141 . . . . . . . . . . 11 ((𝐴 ∈ ℝ* ∧ (πΉβ€˜π‘—) ∈ ℝ* ∧ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š) ∈ ℝ*) β†’ ((𝐴 ≀ (πΉβ€˜π‘—) ∧ (πΉβ€˜π‘—) ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š)) β†’ 𝐴 ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š)))
5450, 51, 52, 53syl3anc 1369 . . . . . . . . . 10 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ ((𝐴 ≀ (πΉβ€˜π‘—) ∧ (πΉβ€˜π‘—) ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š)) β†’ 𝐴 ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š)))
5548, 54syld 47 . . . . . . . . 9 (((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) ∧ 𝑗 ∈ 𝐡) β†’ (((π‘˜ ≀ 𝑗 β†’ 𝐴 ≀ (πΉβ€˜π‘—)) ∧ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗) β†’ 𝐴 ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š)))
5655rexlimdva 3153 . . . . . . . 8 ((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) β†’ (βˆƒπ‘— ∈ 𝐡 ((π‘˜ ≀ 𝑗 β†’ 𝐴 ≀ (πΉβ€˜π‘—)) ∧ if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗) β†’ 𝐴 ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š)))
5714, 56syl5 34 . . . . . . 7 ((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) β†’ ((βˆ€π‘— ∈ 𝐡 (π‘˜ ≀ 𝑗 β†’ 𝐴 ≀ (πΉβ€˜π‘—)) ∧ βˆƒπ‘— ∈ 𝐡 if(π‘˜ ≀ π‘š, π‘š, π‘˜) ≀ 𝑗) β†’ 𝐴 ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š)))
5813, 57mpan2d 690 . . . . . 6 ((πœ‘ ∧ (π‘š ∈ ℝ ∧ π‘˜ ∈ ℝ)) β†’ (βˆ€π‘— ∈ 𝐡 (π‘˜ ≀ 𝑗 β†’ 𝐴 ≀ (πΉβ€˜π‘—)) β†’ 𝐴 ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š)))
5958anassrs 466 . . . . 5 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ ℝ) β†’ (βˆ€π‘— ∈ 𝐡 (π‘˜ ≀ 𝑗 β†’ 𝐴 ≀ (πΉβ€˜π‘—)) β†’ 𝐴 ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š)))
6059rexlimdva 3153 . . . 4 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ (βˆƒπ‘˜ ∈ ℝ βˆ€π‘— ∈ 𝐡 (π‘˜ ≀ 𝑗 β†’ 𝐴 ≀ (πΉβ€˜π‘—)) β†’ 𝐴 ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š)))
6160ralrimdva 3152 . . 3 (πœ‘ β†’ (βˆƒπ‘˜ ∈ ℝ βˆ€π‘— ∈ 𝐡 (π‘˜ ≀ 𝑗 β†’ 𝐴 ≀ (πΉβ€˜π‘—)) β†’ βˆ€π‘š ∈ ℝ 𝐴 ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š)))
621, 61mpd 15 . 2 (πœ‘ β†’ βˆ€π‘š ∈ ℝ 𝐴 ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š))
6334limsuple 15426 . . 3 ((𝐡 βŠ† ℝ ∧ 𝐹:π΅βŸΆβ„* ∧ 𝐴 ∈ ℝ*) β†’ (𝐴 ≀ (lim supβ€˜πΉ) ↔ βˆ€π‘š ∈ ℝ 𝐴 ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š)))
643, 40, 49, 63syl3anc 1369 . 2 (πœ‘ β†’ (𝐴 ≀ (lim supβ€˜πΉ) ↔ βˆ€π‘š ∈ ℝ 𝐴 ≀ ((𝑛 ∈ ℝ ↦ sup(((𝐹 β€œ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))β€˜π‘š)))
6562, 64mpbird 256 1 (πœ‘ β†’ 𝐴 ≀ (lim supβ€˜πΉ))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104  βˆ€wral 3059  βˆƒwrex 3068   ∩ cin 3946   βŠ† wss 3947  ifcif 4527   class class class wbr 5147   ↦ cmpt 5230   β€œ cima 5678  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411  supcsup 9437  β„cr 11111  +∞cpnf 11249  β„*cxr 11251   < clt 11252   ≀ cle 11253  [,)cico 13330  lim supclsp 15418
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-sup 9439  df-inf 9440  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-ico 13334  df-limsup 15419
This theorem is referenced by:  caucvgrlem  15623  limsupre  44655
  Copyright terms: Public domain W3C validator