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

Theorem rlimresb 15453
Description: The restriction of a function to an unbounded-above interval converges iff the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.)
Hypotheses
Ref Expression
rlimresb.1 (πœ‘ β†’ 𝐹:π΄βŸΆβ„‚)
rlimresb.2 (πœ‘ β†’ 𝐴 βŠ† ℝ)
rlimresb.3 (πœ‘ β†’ 𝐡 ∈ ℝ)
Assertion
Ref Expression
rlimresb (πœ‘ β†’ (𝐹 β‡π‘Ÿ 𝐢 ↔ (𝐹 β†Ύ (𝐡[,)+∞)) β‡π‘Ÿ 𝐢))

Proof of Theorem rlimresb
Dummy variables π‘₯ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rlimcl 15391 . . . 4 ((π‘₯ ∈ 𝐴 ↦ (πΉβ€˜π‘₯)) β‡π‘Ÿ 𝐢 β†’ 𝐢 ∈ β„‚)
21a1i 11 . . 3 (πœ‘ β†’ ((π‘₯ ∈ 𝐴 ↦ (πΉβ€˜π‘₯)) β‡π‘Ÿ 𝐢 β†’ 𝐢 ∈ β„‚))
3 rlimcl 15391 . . . 4 ((π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞)) ↦ (πΉβ€˜π‘₯)) β‡π‘Ÿ 𝐢 β†’ 𝐢 ∈ β„‚)
43a1i 11 . . 3 (πœ‘ β†’ ((π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞)) ↦ (πΉβ€˜π‘₯)) β‡π‘Ÿ 𝐢 β†’ 𝐢 ∈ β„‚))
5 rlimresb.2 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐴 βŠ† ℝ)
65adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ (𝐡[,)+∞) ∧ (π‘₯ ∈ 𝐴 ∧ 𝑧 ≀ π‘₯))) β†’ 𝐴 βŠ† ℝ)
7 simprrl 780 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ (𝐡[,)+∞) ∧ (π‘₯ ∈ 𝐴 ∧ 𝑧 ≀ π‘₯))) β†’ π‘₯ ∈ 𝐴)
86, 7sseldd 3946 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑧 ∈ (𝐡[,)+∞) ∧ (π‘₯ ∈ 𝐴 ∧ 𝑧 ≀ π‘₯))) β†’ π‘₯ ∈ ℝ)
9 rlimresb.3 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐡 ∈ ℝ)
109adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ (𝐡[,)+∞) ∧ (π‘₯ ∈ 𝐴 ∧ 𝑧 ≀ π‘₯))) β†’ 𝐡 ∈ ℝ)
11 elicopnf 13368 . . . . . . . . . . . . . . . . . . . . . 22 (𝐡 ∈ ℝ β†’ (𝑧 ∈ (𝐡[,)+∞) ↔ (𝑧 ∈ ℝ ∧ 𝐡 ≀ 𝑧)))
129, 11syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑧 ∈ (𝐡[,)+∞) ↔ (𝑧 ∈ ℝ ∧ 𝐡 ≀ 𝑧)))
1312biimpa 478 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑧 ∈ (𝐡[,)+∞)) β†’ (𝑧 ∈ ℝ ∧ 𝐡 ≀ 𝑧))
1413adantrr 716 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑧 ∈ (𝐡[,)+∞) ∧ (π‘₯ ∈ 𝐴 ∧ 𝑧 ≀ π‘₯))) β†’ (𝑧 ∈ ℝ ∧ 𝐡 ≀ 𝑧))
1514simpld 496 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ (𝐡[,)+∞) ∧ (π‘₯ ∈ 𝐴 ∧ 𝑧 ≀ π‘₯))) β†’ 𝑧 ∈ ℝ)
1614simprd 497 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ (𝐡[,)+∞) ∧ (π‘₯ ∈ 𝐴 ∧ 𝑧 ≀ π‘₯))) β†’ 𝐡 ≀ 𝑧)
17 simprrr 781 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ (𝐡[,)+∞) ∧ (π‘₯ ∈ 𝐴 ∧ 𝑧 ≀ π‘₯))) β†’ 𝑧 ≀ π‘₯)
1810, 15, 8, 16, 17letrd 11317 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑧 ∈ (𝐡[,)+∞) ∧ (π‘₯ ∈ 𝐴 ∧ 𝑧 ≀ π‘₯))) β†’ 𝐡 ≀ π‘₯)
19 elicopnf 13368 . . . . . . . . . . . . . . . . . 18 (𝐡 ∈ ℝ β†’ (π‘₯ ∈ (𝐡[,)+∞) ↔ (π‘₯ ∈ ℝ ∧ 𝐡 ≀ π‘₯)))
2010, 19syl 17 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑧 ∈ (𝐡[,)+∞) ∧ (π‘₯ ∈ 𝐴 ∧ 𝑧 ≀ π‘₯))) β†’ (π‘₯ ∈ (𝐡[,)+∞) ↔ (π‘₯ ∈ ℝ ∧ 𝐡 ≀ π‘₯)))
218, 18, 20mpbir2and 712 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑧 ∈ (𝐡[,)+∞) ∧ (π‘₯ ∈ 𝐴 ∧ 𝑧 ≀ π‘₯))) β†’ π‘₯ ∈ (𝐡[,)+∞))
2221anassrs 469 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ (𝐡[,)+∞)) ∧ (π‘₯ ∈ 𝐴 ∧ 𝑧 ≀ π‘₯)) β†’ π‘₯ ∈ (𝐡[,)+∞))
2322anassrs 469 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑧 ∈ (𝐡[,)+∞)) ∧ π‘₯ ∈ 𝐴) ∧ 𝑧 ≀ π‘₯) β†’ π‘₯ ∈ (𝐡[,)+∞))
24 biimt 361 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝐡[,)+∞) β†’ ((absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦 ↔ (π‘₯ ∈ (𝐡[,)+∞) β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦)))
2523, 24syl 17 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑧 ∈ (𝐡[,)+∞)) ∧ π‘₯ ∈ 𝐴) ∧ 𝑧 ≀ π‘₯) β†’ ((absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦 ↔ (π‘₯ ∈ (𝐡[,)+∞) β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦)))
2625pm5.74da 803 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ (𝐡[,)+∞)) ∧ π‘₯ ∈ 𝐴) β†’ ((𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦) ↔ (𝑧 ≀ π‘₯ β†’ (π‘₯ ∈ (𝐡[,)+∞) β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦))))
27 bi2.04 389 . . . . . . . . . . . 12 ((𝑧 ≀ π‘₯ β†’ (π‘₯ ∈ (𝐡[,)+∞) β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦)) ↔ (π‘₯ ∈ (𝐡[,)+∞) β†’ (𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦)))
2826, 27bitrdi 287 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ (𝐡[,)+∞)) ∧ π‘₯ ∈ 𝐴) β†’ ((𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦) ↔ (π‘₯ ∈ (𝐡[,)+∞) β†’ (𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦))))
2928pm5.74da 803 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ (𝐡[,)+∞)) β†’ ((π‘₯ ∈ 𝐴 β†’ (𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦)) ↔ (π‘₯ ∈ 𝐴 β†’ (π‘₯ ∈ (𝐡[,)+∞) β†’ (𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦)))))
30 elin 3927 . . . . . . . . . . . 12 (π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞)) ↔ (π‘₯ ∈ 𝐴 ∧ π‘₯ ∈ (𝐡[,)+∞)))
3130imbi1i 350 . . . . . . . . . . 11 ((π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞)) β†’ (𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦)) ↔ ((π‘₯ ∈ 𝐴 ∧ π‘₯ ∈ (𝐡[,)+∞)) β†’ (𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦)))
32 impexp 452 . . . . . . . . . . 11 (((π‘₯ ∈ 𝐴 ∧ π‘₯ ∈ (𝐡[,)+∞)) β†’ (𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦)) ↔ (π‘₯ ∈ 𝐴 β†’ (π‘₯ ∈ (𝐡[,)+∞) β†’ (𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦))))
3331, 32bitri 275 . . . . . . . . . 10 ((π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞)) β†’ (𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦)) ↔ (π‘₯ ∈ 𝐴 β†’ (π‘₯ ∈ (𝐡[,)+∞) β†’ (𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦))))
3429, 33bitr4di 289 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ (𝐡[,)+∞)) β†’ ((π‘₯ ∈ 𝐴 β†’ (𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦)) ↔ (π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞)) β†’ (𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦))))
3534ralbidv2 3167 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ (𝐡[,)+∞)) β†’ (βˆ€π‘₯ ∈ 𝐴 (𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦) ↔ βˆ€π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞))(𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦)))
3635rexbidva 3170 . . . . . . 7 (πœ‘ β†’ (βˆƒπ‘§ ∈ (𝐡[,)+∞)βˆ€π‘₯ ∈ 𝐴 (𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦) ↔ βˆƒπ‘§ ∈ (𝐡[,)+∞)βˆ€π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞))(𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦)))
3736ralbidv 3171 . . . . . 6 (πœ‘ β†’ (βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ (𝐡[,)+∞)βˆ€π‘₯ ∈ 𝐴 (𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦) ↔ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ (𝐡[,)+∞)βˆ€π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞))(𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦)))
3837adantr 482 . . . . 5 ((πœ‘ ∧ 𝐢 ∈ β„‚) β†’ (βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ (𝐡[,)+∞)βˆ€π‘₯ ∈ 𝐴 (𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦) ↔ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ (𝐡[,)+∞)βˆ€π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞))(𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦)))
39 rlimresb.1 . . . . . . . . 9 (πœ‘ β†’ 𝐹:π΄βŸΆβ„‚)
4039ffvelcdmda 7036 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
4140ralrimiva 3140 . . . . . . 7 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐴 (πΉβ€˜π‘₯) ∈ β„‚)
4241adantr 482 . . . . . 6 ((πœ‘ ∧ 𝐢 ∈ β„‚) β†’ βˆ€π‘₯ ∈ 𝐴 (πΉβ€˜π‘₯) ∈ β„‚)
435adantr 482 . . . . . 6 ((πœ‘ ∧ 𝐢 ∈ β„‚) β†’ 𝐴 βŠ† ℝ)
44 simpr 486 . . . . . 6 ((πœ‘ ∧ 𝐢 ∈ β„‚) β†’ 𝐢 ∈ β„‚)
459adantr 482 . . . . . 6 ((πœ‘ ∧ 𝐢 ∈ β„‚) β†’ 𝐡 ∈ ℝ)
4642, 43, 44, 45rlim3 15386 . . . . 5 ((πœ‘ ∧ 𝐢 ∈ β„‚) β†’ ((π‘₯ ∈ 𝐴 ↦ (πΉβ€˜π‘₯)) β‡π‘Ÿ 𝐢 ↔ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ (𝐡[,)+∞)βˆ€π‘₯ ∈ 𝐴 (𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦)))
47 elinel1 4156 . . . . . . . . 9 (π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞)) β†’ π‘₯ ∈ 𝐴)
4847, 40sylan2 594 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞))) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
4948ralrimiva 3140 . . . . . . 7 (πœ‘ β†’ βˆ€π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞))(πΉβ€˜π‘₯) ∈ β„‚)
5049adantr 482 . . . . . 6 ((πœ‘ ∧ 𝐢 ∈ β„‚) β†’ βˆ€π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞))(πΉβ€˜π‘₯) ∈ β„‚)
51 inss1 4189 . . . . . . . 8 (𝐴 ∩ (𝐡[,)+∞)) βŠ† 𝐴
5251, 5sstrid 3956 . . . . . . 7 (πœ‘ β†’ (𝐴 ∩ (𝐡[,)+∞)) βŠ† ℝ)
5352adantr 482 . . . . . 6 ((πœ‘ ∧ 𝐢 ∈ β„‚) β†’ (𝐴 ∩ (𝐡[,)+∞)) βŠ† ℝ)
5450, 53, 44, 45rlim3 15386 . . . . 5 ((πœ‘ ∧ 𝐢 ∈ β„‚) β†’ ((π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞)) ↦ (πΉβ€˜π‘₯)) β‡π‘Ÿ 𝐢 ↔ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ (𝐡[,)+∞)βˆ€π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞))(𝑧 ≀ π‘₯ β†’ (absβ€˜((πΉβ€˜π‘₯) βˆ’ 𝐢)) < 𝑦)))
5538, 46, 543bitr4d 311 . . . 4 ((πœ‘ ∧ 𝐢 ∈ β„‚) β†’ ((π‘₯ ∈ 𝐴 ↦ (πΉβ€˜π‘₯)) β‡π‘Ÿ 𝐢 ↔ (π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞)) ↦ (πΉβ€˜π‘₯)) β‡π‘Ÿ 𝐢))
5655ex 414 . . 3 (πœ‘ β†’ (𝐢 ∈ β„‚ β†’ ((π‘₯ ∈ 𝐴 ↦ (πΉβ€˜π‘₯)) β‡π‘Ÿ 𝐢 ↔ (π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞)) ↦ (πΉβ€˜π‘₯)) β‡π‘Ÿ 𝐢)))
572, 4, 56pm5.21ndd 381 . 2 (πœ‘ β†’ ((π‘₯ ∈ 𝐴 ↦ (πΉβ€˜π‘₯)) β‡π‘Ÿ 𝐢 ↔ (π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞)) ↦ (πΉβ€˜π‘₯)) β‡π‘Ÿ 𝐢))
5839feqmptd 6911 . . 3 (πœ‘ β†’ 𝐹 = (π‘₯ ∈ 𝐴 ↦ (πΉβ€˜π‘₯)))
5958breq1d 5116 . 2 (πœ‘ β†’ (𝐹 β‡π‘Ÿ 𝐢 ↔ (π‘₯ ∈ 𝐴 ↦ (πΉβ€˜π‘₯)) β‡π‘Ÿ 𝐢))
60 resres 5951 . . . 4 ((𝐹 β†Ύ 𝐴) β†Ύ (𝐡[,)+∞)) = (𝐹 β†Ύ (𝐴 ∩ (𝐡[,)+∞)))
61 ffn 6669 . . . . . 6 (𝐹:π΄βŸΆβ„‚ β†’ 𝐹 Fn 𝐴)
62 fnresdm 6621 . . . . . 6 (𝐹 Fn 𝐴 β†’ (𝐹 β†Ύ 𝐴) = 𝐹)
6339, 61, 623syl 18 . . . . 5 (πœ‘ β†’ (𝐹 β†Ύ 𝐴) = 𝐹)
6463reseq1d 5937 . . . 4 (πœ‘ β†’ ((𝐹 β†Ύ 𝐴) β†Ύ (𝐡[,)+∞)) = (𝐹 β†Ύ (𝐡[,)+∞)))
6558reseq1d 5937 . . . . 5 (πœ‘ β†’ (𝐹 β†Ύ (𝐴 ∩ (𝐡[,)+∞))) = ((π‘₯ ∈ 𝐴 ↦ (πΉβ€˜π‘₯)) β†Ύ (𝐴 ∩ (𝐡[,)+∞))))
66 resmpt 5992 . . . . . 6 ((𝐴 ∩ (𝐡[,)+∞)) βŠ† 𝐴 β†’ ((π‘₯ ∈ 𝐴 ↦ (πΉβ€˜π‘₯)) β†Ύ (𝐴 ∩ (𝐡[,)+∞))) = (π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞)) ↦ (πΉβ€˜π‘₯)))
6751, 66ax-mp 5 . . . . 5 ((π‘₯ ∈ 𝐴 ↦ (πΉβ€˜π‘₯)) β†Ύ (𝐴 ∩ (𝐡[,)+∞))) = (π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞)) ↦ (πΉβ€˜π‘₯))
6865, 67eqtrdi 2789 . . . 4 (πœ‘ β†’ (𝐹 β†Ύ (𝐴 ∩ (𝐡[,)+∞))) = (π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞)) ↦ (πΉβ€˜π‘₯)))
6960, 64, 683eqtr3a 2797 . . 3 (πœ‘ β†’ (𝐹 β†Ύ (𝐡[,)+∞)) = (π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞)) ↦ (πΉβ€˜π‘₯)))
7069breq1d 5116 . 2 (πœ‘ β†’ ((𝐹 β†Ύ (𝐡[,)+∞)) β‡π‘Ÿ 𝐢 ↔ (π‘₯ ∈ (𝐴 ∩ (𝐡[,)+∞)) ↦ (πΉβ€˜π‘₯)) β‡π‘Ÿ 𝐢))
7157, 59, 703bitr4d 311 1 (πœ‘ β†’ (𝐹 β‡π‘Ÿ 𝐢 ↔ (𝐹 β†Ύ (𝐡[,)+∞)) β‡π‘Ÿ 𝐢))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3061  βˆƒwrex 3070   ∩ cin 3910   βŠ† wss 3911   class class class wbr 5106   ↦ cmpt 5189   β†Ύ cres 5636   Fn wfn 6492  βŸΆwf 6493  β€˜cfv 6497  (class class class)co 7358  β„‚cc 11054  β„cr 11055  +∞cpnf 11191   < clt 11194   ≀ cle 11195   βˆ’ cmin 11390  β„+crp 12920  [,)cico 13272  abscabs 15125   β‡π‘Ÿ crli 15373
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11112  ax-resscn 11113  ax-pre-lttri 11130  ax-pre-lttrn 11131
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-po 5546  df-so 5547  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8651  df-pm 8771  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-ico 13276  df-rlim 15377
This theorem is referenced by:  rlimeq  15457  rlimcnp2  26332  cxp2lim  26342  pnt2  26977  pnt  26978
  Copyright terms: Public domain W3C validator