Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  limclner Structured version   Visualization version   GIF version

Theorem limclner 43982
Description: For a limit point, both from the left and from the right, of the domain, the limit of the function exits only if the left and the right limits are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
limclner.k 𝐾 = (TopOpenβ€˜β„‚fld)
limclner.a (πœ‘ β†’ 𝐴 βŠ† ℝ)
limclner.j 𝐽 = (topGenβ€˜ran (,))
limclner.f (πœ‘ β†’ 𝐹:π΄βŸΆβ„‚)
limclner.blp1 (πœ‘ β†’ 𝐡 ∈ ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))))
limclner.blp2 (πœ‘ β†’ 𝐡 ∈ ((limPtβ€˜π½)β€˜(𝐴 ∩ (𝐡(,)+∞))))
limclner.l (πœ‘ β†’ 𝐿 ∈ ((𝐹 β†Ύ (-∞(,)𝐡)) limβ„‚ 𝐡))
limclner.r (πœ‘ β†’ 𝑅 ∈ ((𝐹 β†Ύ (𝐡(,)+∞)) limβ„‚ 𝐡))
limclner.lner (πœ‘ β†’ 𝐿 β‰  𝑅)
Assertion
Ref Expression
limclner (πœ‘ β†’ (𝐹 limβ„‚ 𝐡) = βˆ…)

Proof of Theorem limclner
Dummy variables π‘Ž 𝑏 𝑒 𝑣 𝑧 𝑀 π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 limccl 25262 . . . . . . . . . . . . 13 ((𝐹 β†Ύ (𝐡(,)+∞)) limβ„‚ 𝐡) βŠ† β„‚
2 limclner.r . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑅 ∈ ((𝐹 β†Ύ (𝐡(,)+∞)) limβ„‚ 𝐡))
31, 2sselid 3946 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑅 ∈ β„‚)
43ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ 𝑅 ∈ β„‚)
5 limccl 25262 . . . . . . . . . . . . 13 ((𝐹 β†Ύ (-∞(,)𝐡)) limβ„‚ 𝐡) βŠ† β„‚
6 limclner.l . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐿 ∈ ((𝐹 β†Ύ (-∞(,)𝐡)) limβ„‚ 𝐡))
75, 6sselid 3946 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐿 ∈ β„‚)
87ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ 𝐿 ∈ β„‚)
94, 8subcld 11520 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (𝑅 βˆ’ 𝐿) ∈ β„‚)
10 limclner.lner . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐿 β‰  𝑅)
1110necomd 2996 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑅 β‰  𝐿)
1211ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ 𝑅 β‰  𝐿)
134, 8, 12subne0d 11529 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (𝑅 βˆ’ 𝐿) β‰  0)
149, 13absrpcld 15342 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ ℝ+)
15 4re 12245 . . . . . . . . . . 11 4 ∈ ℝ
16 4pos 12268 . . . . . . . . . . 11 0 < 4
1715, 16elrpii 12926 . . . . . . . . . 10 4 ∈ ℝ+
1817a1i 11 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ 4 ∈ ℝ+)
1914, 18rpdivcld 12982 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ ℝ+)
20 nfv 1918 . . . . . . . . . . 11 Ⅎ𝑦(πœ‘ ∧ π‘₯ ∈ β„‚)
21 nfra1 3266 . . . . . . . . . . 11 β„²π‘¦βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)
2220, 21nfan 1903 . . . . . . . . . 10 Ⅎ𝑦((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))
23 nfv 1918 . . . . . . . . . 10 Ⅎ𝑦(((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)))
2422, 23nfim 1900 . . . . . . . . 9 Ⅎ𝑦(((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))))
25 ovex 7394 . . . . . . . . 9 ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ V
26 eleq1 2822 . . . . . . . . . . 11 (𝑦 = ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) β†’ (𝑦 ∈ ℝ+ ↔ ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ ℝ+))
27 oveq2 7369 . . . . . . . . . . . . 13 (𝑦 = ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) β†’ (4 Β· 𝑦) = (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)))
2827breq2d 5121 . . . . . . . . . . . 12 (𝑦 = ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) β†’ ((absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦) ↔ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))))
29282rexbidv 3210 . . . . . . . . . . 11 (𝑦 = ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) β†’ (βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦) ↔ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))))
3026, 29imbi12d 345 . . . . . . . . . 10 (𝑦 = ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) β†’ ((𝑦 ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦)) ↔ (((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)))))
3130imbi2d 341 . . . . . . . . 9 (𝑦 = ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) β†’ ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (𝑦 ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦))) ↔ (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))))))
32 simpll 766 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) β†’ (πœ‘ ∧ π‘₯ ∈ β„‚))
33 simpr 486 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) β†’ 𝑦 ∈ ℝ+)
34 rspa 3230 . . . . . . . . . . . 12 ((βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) ∧ 𝑦 ∈ ℝ+) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))
3534adantll 713 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))
36 limclner.f . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝐹:π΄βŸΆβ„‚)
37 fresin 6715 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹:π΄βŸΆβ„‚ β†’ (𝐹 β†Ύ (𝐡(,)+∞)):(𝐴 ∩ (𝐡(,)+∞))βŸΆβ„‚)
3836, 37syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝐹 β†Ύ (𝐡(,)+∞)):(𝐴 ∩ (𝐡(,)+∞))βŸΆβ„‚)
39 inss2 4193 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ∩ (𝐡(,)+∞)) βŠ† (𝐡(,)+∞)
40 ioosscn 13335 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐡(,)+∞) βŠ† β„‚
4139, 40sstri 3957 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∩ (𝐡(,)+∞)) βŠ† β„‚
4241a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝐴 ∩ (𝐡(,)+∞)) βŠ† β„‚)
43 limclner.j . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝐽 = (topGenβ€˜ran (,))
44 retop 24148 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (topGenβ€˜ran (,)) ∈ Top
4543, 44eqeltri 2830 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝐽 ∈ Top
46 inss2 4193 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴 ∩ (-∞(,)𝐡)) βŠ† (-∞(,)𝐡)
47 ioossre 13334 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (-∞(,)𝐡) βŠ† ℝ
4846, 47sstri 3957 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 ∩ (-∞(,)𝐡)) βŠ† ℝ
49 uniretop 24149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℝ = βˆͺ (topGenβ€˜ran (,))
5043unieqi 4882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 βˆͺ 𝐽 = βˆͺ (topGenβ€˜ran (,))
5149, 50eqtr4i 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ℝ = βˆͺ 𝐽
5251lpss 22516 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐽 ∈ Top ∧ (𝐴 ∩ (-∞(,)𝐡)) βŠ† ℝ) β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))) βŠ† ℝ)
5345, 48, 52mp2an 691 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))) βŠ† ℝ
54 limclner.blp1 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ 𝐡 ∈ ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))))
5553, 54sselid 3946 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝐡 ∈ ℝ)
5655recnd 11191 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝐡 ∈ β„‚)
5738, 42, 56ellimc3 25266 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (𝑅 ∈ ((𝐹 β†Ύ (𝐡(,)+∞)) limβ„‚ 𝐡) ↔ (𝑅 ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))))
582, 57mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝑅 ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)))
5958simprd 497 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))
6059r19.21bi 3233 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑦 ∈ ℝ+) β†’ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))
61603ad2ant1 1134 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))
62 simp11l 1285 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ πœ‘)
63 simp12 1205 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ 𝑧 ∈ ℝ+)
64 simp2 1138 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ 𝑣 ∈ ℝ+)
65 breq2 5113 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑒 = if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑒 ↔ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)))
6665rexbidv 3172 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑒 = if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ (βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑒 ↔ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)))
67 inss1 4192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞))) ∩ ℝ) βŠ† ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞)))
6867a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞))) ∩ ℝ) βŠ† ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞))))
69 limclner.k . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝐾 = (TopOpenβ€˜β„‚fld)
7069cnfldtop 24170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝐾 ∈ Top
7170a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (πœ‘ β†’ 𝐾 ∈ Top)
72 ax-resscn 11116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℝ βŠ† β„‚
7372a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (πœ‘ β†’ ℝ βŠ† β„‚)
74 ioossre 13334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐡(,)+∞) βŠ† ℝ
7539, 74sstri 3957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐴 ∩ (𝐡(,)+∞)) βŠ† ℝ
7675a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (πœ‘ β†’ (𝐴 ∩ (𝐡(,)+∞)) βŠ† ℝ)
77 unicntop 24172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 β„‚ = βˆͺ (TopOpenβ€˜β„‚fld)
7869unieqi 4882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 βˆͺ 𝐾 = βˆͺ (TopOpenβ€˜β„‚fld)
7977, 78eqtr4i 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 β„‚ = βˆͺ 𝐾
8069tgioo2 24189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (topGenβ€˜ran (,)) = (𝐾 β†Ύt ℝ)
8143, 80eqtri 2761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝐽 = (𝐾 β†Ύt ℝ)
8279, 81restlp 22557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐾 ∈ Top ∧ ℝ βŠ† β„‚ ∧ (𝐴 ∩ (𝐡(,)+∞)) βŠ† ℝ) β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (𝐡(,)+∞))) = (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞))) ∩ ℝ))
8371, 73, 76, 82syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (𝐡(,)+∞))) = (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞))) ∩ ℝ))
8469eqcomi 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (TopOpenβ€˜β„‚fld) = 𝐾
8584fveq2i 6849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (limPtβ€˜(TopOpenβ€˜β„‚fld)) = (limPtβ€˜πΎ)
8685fveq1i 6847 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (𝐡(,)+∞))) = ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞)))
8786a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (𝐡(,)+∞))) = ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞))))
8868, 83, 873sstr4d 3995 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (𝐡(,)+∞))) βŠ† ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (𝐡(,)+∞))))
89 limclner.blp2 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ 𝐡 ∈ ((limPtβ€˜π½)β€˜(𝐴 ∩ (𝐡(,)+∞))))
9088, 89sseldd 3949 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ 𝐡 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (𝐡(,)+∞))))
9142, 56islpcn 43970 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (𝐡 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (𝐡(,)+∞))) ↔ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑒))
9290, 91mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑒)
93923ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑒)
94 ifcl 4535 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ∈ ℝ+)
95943adant1 1131 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ∈ ℝ+)
9666, 93, 95rspcdva 3584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣))
97 eldifi 4090 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) β†’ 𝑏 ∈ (𝐴 ∩ (𝐡(,)+∞)))
9875, 97sselid 3946 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) β†’ 𝑏 ∈ ℝ)
9973sselda 3948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((πœ‘ ∧ 𝑏 ∈ ℝ) β†’ 𝑏 ∈ β„‚)
10056adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((πœ‘ ∧ 𝑏 ∈ ℝ) β†’ 𝐡 ∈ β„‚)
10199, 100subcld 11520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((πœ‘ ∧ 𝑏 ∈ ℝ) β†’ (𝑏 βˆ’ 𝐡) ∈ β„‚)
102101abscld 15330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ 𝑏 ∈ ℝ) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) ∈ ℝ)
1031023ad2antl1 1186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) ∈ ℝ)
104103adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) ∈ ℝ)
10595rpred 12965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ∈ ℝ)
106105ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ∈ ℝ)
107 rpre 12931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∈ ℝ+ β†’ 𝑧 ∈ ℝ)
1081073ad2ant2 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ 𝑧 ∈ ℝ)
109108ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ 𝑧 ∈ ℝ)
110 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣))
111 rpre 12931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 ∈ ℝ+ β†’ 𝑣 ∈ ℝ)
112 min1 13117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑧)
113107, 111, 112syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑧)
1141133adant1 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑧)
115114ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑧)
116104, 106, 109, 110, 115ltletrd 11323 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧)
1171113ad2ant3 1136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ 𝑣 ∈ ℝ)
118117ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ 𝑣 ∈ ℝ)
119109, 118min2d 43798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑣)
120104, 106, 118, 110, 119ltletrd 11323 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)
121116, 120jca 513 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣))
122121ex 414 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) β†’ ((absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)))
12398, 122sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})) β†’ ((absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)))
124123reximdva 3162 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ (βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)))
12596, 124mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣))
12662, 63, 64, 125syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣))
127 nfv 1918 . . . . . . . . . . . . . . . . . . . . . . 23 Ⅎ𝑏(((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))
128 nfre1 3267 . . . . . . . . . . . . . . . . . . . . . . 23 β„²π‘βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)
12997elin1d 4162 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) β†’ 𝑏 ∈ 𝐴)
1301293ad2ant2 1135 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ 𝑏 ∈ 𝐴)
131 simp113 1305 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))
132 eldifsni 4754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) β†’ 𝑏 β‰  𝐡)
133132adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ 𝑏 β‰  𝐡)
134 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧)
135133, 134jca 513 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧))
1361353adant1 1131 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧))
137 neeq1 3003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑀 = 𝑏 β†’ (𝑀 β‰  𝐡 ↔ 𝑏 β‰  𝐡))
138 fvoveq1 7384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑀 = 𝑏 β†’ (absβ€˜(𝑀 βˆ’ 𝐡)) = (absβ€˜(𝑏 βˆ’ 𝐡)))
139138breq1d 5119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑀 = 𝑏 β†’ ((absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧 ↔ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧))
140137, 139anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑀 = 𝑏 β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) ↔ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧)))
141140imbrov2fvoveq 7386 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 = 𝑏 β†’ (((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) ↔ ((𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦)))
142141rspcva 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 ∈ 𝐴 ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ ((𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦))
143142imp 408 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑏 ∈ 𝐴 ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦)
144130, 131, 136, 143syl21anc 837 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦)
145973ad2ant2 1135 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ 𝑏 ∈ (𝐴 ∩ (𝐡(,)+∞)))
146623ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ πœ‘)
147 simp13 1206 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))
148 nfv 1918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 β„²π‘€πœ‘
149 nfra1 3266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 β„²π‘€βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)
150148, 149nfan 1903 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ⅎ𝑀(πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))
151 elinel2 4160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) β†’ 𝑀 ∈ (𝐡(,)+∞))
152151fvresd 6866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) β†’ ((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) = (πΉβ€˜π‘€))
153152eqcomd 2739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) β†’ (πΉβ€˜π‘€) = ((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€))
154153fvoveq1d 7383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) = (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)))
1551543ad2ant2 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) = (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)))
156 rspa 3230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦) ∧ 𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞))) β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))
1571563impia 1118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦) ∧ 𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)
1581573adant1l 1177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)
159155, 158eqbrtrd 5131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦)
1601593exp 1120 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ (𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦)))
161150, 160ralrimi 3239 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦))
162146, 147, 161syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦))
163132anim1i 616 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣) β†’ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣))
164163adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣))
1651643adant1 1131 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣))
166138breq1d 5119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑀 = 𝑏 β†’ ((absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣 ↔ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣))
167137, 166anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑀 = 𝑏 β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) ↔ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)))
168167imbrov2fvoveq 7386 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 = 𝑏 β†’ (((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦) ↔ ((𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)))
169168rspcva 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 ∈ (𝐴 ∩ (𝐡(,)+∞)) ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ ((𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
170169imp 408 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑏 ∈ (𝐴 ∩ (𝐡(,)+∞)) ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)
171145, 162, 165, 170syl21anc 837 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)
172 rspe 3231 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏 ∈ 𝐴 ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
173130, 144, 171, 172syl12anc 836 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
1741733exp 1120 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ (𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) β†’ (((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))))
175127, 128, 174rexlimd 3248 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ (βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)))
176126, 175mpd 15 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
1771763exp 1120 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (𝑣 ∈ ℝ+ β†’ (βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))))
178177rexlimdv 3147 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)))
17961, 178mpd 15 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
1801793exp 1120 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑦 ∈ ℝ+) β†’ (𝑧 ∈ ℝ+ β†’ (βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))))
181180rexlimdv 3147 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑦 ∈ ℝ+) β†’ (βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)))
182181imp 408 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
183182adantllr 718 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
184183ad2antrr 725 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
1853ad6antr 735 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ 𝑅 ∈ β„‚)
1867ad6antr 735 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ 𝐿 ∈ β„‚)
187185, 186subcld 11520 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (𝑅 βˆ’ 𝐿) ∈ β„‚)
188187abscld 15330 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ ℝ)
189 simp-6l 786 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ πœ‘)
190 simplr 768 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ 𝑏 ∈ 𝐴)
19136ffvelcdmda 7039 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑏 ∈ 𝐴) β†’ (πΉβ€˜π‘) ∈ β„‚)
192189, 190, 191syl2anc 585 . . . . . . . . . . . . . . . . . . . . . 22 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (πΉβ€˜π‘) ∈ β„‚)
193185, 192subcld 11520 . . . . . . . . . . . . . . . . . . . . 21 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (𝑅 βˆ’ (πΉβ€˜π‘)) ∈ β„‚)
194193abscld 15330 . . . . . . . . . . . . . . . . . . . 20 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) ∈ ℝ)
195 simp-6r 787 . . . . . . . . . . . . . . . . . . . . . 22 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ π‘₯ ∈ β„‚)
196192, 195subcld 11520 . . . . . . . . . . . . . . . . . . . . 21 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ ((πΉβ€˜π‘) βˆ’ π‘₯) ∈ β„‚)
197196abscld 15330 . . . . . . . . . . . . . . . . . . . 20 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) ∈ ℝ)
198194, 197readdcld 11192 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ ((absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) + (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯))) ∈ ℝ)
199 simp-4r 783 . . . . . . . . . . . . . . . . . . . . . 22 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ π‘Ž ∈ 𝐴)
20036ffvelcdmda 7039 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (πΉβ€˜π‘Ž) ∈ β„‚)
201189, 199, 200syl2anc 585 . . . . . . . . . . . . . . . . . . . . 21 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (πΉβ€˜π‘Ž) ∈ β„‚)
202195, 201subcld 11520 . . . . . . . . . . . . . . . . . . . 20 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (π‘₯ βˆ’ (πΉβ€˜π‘Ž)) ∈ β„‚)
203202abscld 15330 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž))) ∈ ℝ)
204198, 203readdcld 11192 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (((absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) + (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯))) + (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž)))) ∈ ℝ)
205201, 186subcld 11520 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ ((πΉβ€˜π‘Ž) βˆ’ 𝐿) ∈ β„‚)
206205abscld 15330 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) ∈ ℝ)
207204, 206readdcld 11192 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ ((((absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) + (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯))) + (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž)))) + (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿))) ∈ ℝ)
20815a1i 11 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ 4 ∈ ℝ)
209 rpre 12931 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+ β†’ 𝑦 ∈ ℝ)
210209ad5antlr 734 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ 𝑦 ∈ ℝ)
211208, 210remulcld 11193 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (4 Β· 𝑦) ∈ ℝ)
212185, 192, 195, 201, 186absnpncan3d 43632 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ≀ ((((absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) + (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯))) + (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž)))) + (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿))))
213185, 192abssubd 15347 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) = (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)))
214 simprr 772 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)
215213, 214eqbrtrd 5131 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) < 𝑦)
216 simprl 770 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦)
217 simp-5r 785 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ π‘₯ ∈ β„‚)
218200ad5ant14 757 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) β†’ (πΉβ€˜π‘Ž) ∈ β„‚)
219218adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (πΉβ€˜π‘Ž) ∈ β„‚)
220217, 219abssubd 15347 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž))) = (absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)))
221 simplrl 776 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦)
222220, 221eqbrtrd 5131 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž))) < 𝑦)
223222adantr 482 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž))) < 𝑦)
224 simplrr 777 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)
225224adantr 482 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)
226194, 197, 203, 206, 210, 215, 216, 223, 225lt4addmuld 43631 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ ((((absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) + (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯))) + (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž)))) + (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿))) < (4 Β· 𝑦))
227188, 207, 211, 212, 226lelttrd 11321 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦))
228227ex 414 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦)))
229228adantl3r 749 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦)))
230229reximdva 3162 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) β†’ (βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦) β†’ βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦)))
231184, 230mpd 15 . . . . . . . . . . . 12 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦))
232 fresin 6715 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:π΄βŸΆβ„‚ β†’ (𝐹 β†Ύ (-∞(,)𝐡)):(𝐴 ∩ (-∞(,)𝐡))βŸΆβ„‚)
23336, 232syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝐹 β†Ύ (-∞(,)𝐡)):(𝐴 ∩ (-∞(,)𝐡))βŸΆβ„‚)
234 ioosscn 13335 . . . . . . . . . . . . . . . . . . . . . . . 24 (-∞(,)𝐡) βŠ† β„‚
23546, 234sstri 3957 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 ∩ (-∞(,)𝐡)) βŠ† β„‚
236235a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝐴 ∩ (-∞(,)𝐡)) βŠ† β„‚)
237233, 236, 56ellimc3 25266 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝐿 ∈ ((𝐹 β†Ύ (-∞(,)𝐡)) limβ„‚ 𝐡) ↔ (𝐿 ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))))
2386, 237mpbid 231 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (𝐿 ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)))
239238simprd 497 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))
240239r19.21bi 3233 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑦 ∈ ℝ+) β†’ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))
2412403ad2ant1 1134 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))
242 simp11l 1285 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ πœ‘)
243 simp12 1205 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ 𝑧 ∈ ℝ+)
244 simp2 1138 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ 𝑣 ∈ ℝ+)
245 breq2 5113 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑒 = if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑒 ↔ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)))
246245rexbidv 3172 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ (βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑒 ↔ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)))
247 inss1 4192 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡))) ∩ ℝ) βŠ† ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡)))
248247a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡))) ∩ ℝ) βŠ† ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡))))
24948a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ (𝐴 ∩ (-∞(,)𝐡)) βŠ† ℝ)
25079, 81restlp 22557 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐾 ∈ Top ∧ ℝ βŠ† β„‚ ∧ (𝐴 ∩ (-∞(,)𝐡)) βŠ† ℝ) β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))) = (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡))) ∩ ℝ))
25171, 73, 249, 250syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))) = (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡))) ∩ ℝ))
25285fveq1i 6847 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (-∞(,)𝐡))) = ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡)))
253252a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (-∞(,)𝐡))) = ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡))))
254248, 251, 2533sstr4d 3995 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))) βŠ† ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (-∞(,)𝐡))))
255254, 54sseldd 3949 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝐡 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (-∞(,)𝐡))))
256236, 56islpcn 43970 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (𝐡 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (-∞(,)𝐡))) ↔ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑒))
257255, 256mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑒)
2582573ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑒)
259246, 258, 95rspcdva 3584 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣))
260 eldifi 4090 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) β†’ π‘Ž ∈ (𝐴 ∩ (-∞(,)𝐡)))
26148, 260sselid 3946 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) β†’ π‘Ž ∈ ℝ)
26273sselda 3948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ π‘Ž ∈ β„‚)
26356adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ 𝐡 ∈ β„‚)
264262, 263subcld 11520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ (π‘Ž βˆ’ 𝐡) ∈ β„‚)
265264abscld 15330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) ∈ ℝ)
2662653ad2antl1 1186 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) ∈ ℝ)
267266adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) ∈ ℝ)
268105ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ∈ ℝ)
269108ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ 𝑧 ∈ ℝ)
270 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣))
271114ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑧)
272267, 268, 269, 270, 271ltletrd 11323 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧)
273117ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ 𝑣 ∈ ℝ)
274 min2 13118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑣)
275107, 111, 274syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑣)
2762753adant1 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑣)
277276ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑣)
278267, 268, 273, 270, 277ltletrd 11323 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)
279272, 278jca 513 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣))
280279ex 414 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) β†’ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)))
281261, 280sylan2 594 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})) β†’ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)))
282281reximdva 3162 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ (βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)))
283259, 282mpd 15 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣))
284242, 243, 244, 283syl3anc 1372 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣))
285 nfv 1918 . . . . . . . . . . . . . . . . . . . . 21 β„²π‘Ž(((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))
286 nfre1 3267 . . . . . . . . . . . . . . . . . . . . 21 β„²π‘Žβˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)
287260elin1d 4162 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) β†’ π‘Ž ∈ 𝐴)
2882873ad2ant2 1135 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ π‘Ž ∈ 𝐴)
289 simp113 1305 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))
290 eldifsni 4754 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) β†’ π‘Ž β‰  𝐡)
291290adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ π‘Ž β‰  𝐡)
292 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧)
293291, 292jca 513 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧))
2942933adant1 1131 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧))
295 neeq1 3003 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 = π‘Ž β†’ (𝑀 β‰  𝐡 ↔ π‘Ž β‰  𝐡))
296 fvoveq1 7384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑀 = π‘Ž β†’ (absβ€˜(𝑀 βˆ’ 𝐡)) = (absβ€˜(π‘Ž βˆ’ 𝐡)))
297296breq1d 5119 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 = π‘Ž β†’ ((absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧 ↔ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧))
298295, 297anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 = π‘Ž β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) ↔ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧)))
299298imbrov2fvoveq 7386 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 = π‘Ž β†’ (((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) ↔ ((π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦)))
300299rspcva 3581 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘Ž ∈ 𝐴 ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ ((π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦))
301300imp 408 . . . . . . . . . . . . . . . . . . . . . . . 24 (((π‘Ž ∈ 𝐴 ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧)) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦)
302288, 289, 294, 301syl21anc 837 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦)
3032603ad2ant2 1135 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ π‘Ž ∈ (𝐴 ∩ (-∞(,)𝐡)))
3042423ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ πœ‘)
305 simp13 1206 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))
306 nfra1 3266 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 β„²π‘€βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)
307148, 306nfan 1903 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ⅎ𝑀(πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))
308 elinel2 4160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) β†’ 𝑀 ∈ (-∞(,)𝐡))
309308fvresd 6866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) β†’ ((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) = (πΉβ€˜π‘€))
310309eqcomd 2739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) β†’ (πΉβ€˜π‘€) = ((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€))
311310fvoveq1d 7383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) = (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)))
3123113ad2ant2 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) = (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)))
313 rspa 3230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦) ∧ 𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡))) β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))
3143133impia 1118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦) ∧ 𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)
3153143adant1l 1177 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)
316312, 315eqbrtrd 5131 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦)
3173163exp 1120 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ (𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦)))
318307, 317ralrimi 3239 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦))
319304, 305, 318syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦))
320290anim1i 616 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣) β†’ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣))
321320adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣))
3223213adant1 1131 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣))
323296breq1d 5119 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 = π‘Ž β†’ ((absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣 ↔ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣))
324295, 323anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 = π‘Ž β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) ↔ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)))
325324imbrov2fvoveq 7386 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 = π‘Ž β†’ (((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦) ↔ ((π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)))
326325rspcva 3581 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘Ž ∈ (𝐴 ∩ (-∞(,)𝐡)) ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ ((π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
327326imp 408 . . . . . . . . . . . . . . . . . . . . . . . 24 (((π‘Ž ∈ (𝐴 ∩ (-∞(,)𝐡)) ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)
328303, 319, 322, 327syl21anc 837 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)
329 rspe 3231 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘Ž ∈ 𝐴 ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
330288, 302, 328, 329syl12anc 836 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
3313303exp 1120 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ (π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) β†’ (((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))))
332285, 286, 331rexlimd 3248 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ (βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)))
333284, 332mpd 15 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
3343333exp 1120 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (𝑣 ∈ ℝ+ β†’ (βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))))
335334rexlimdv 3147 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)))
336241, 335mpd 15 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
3373363exp 1120 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑦 ∈ ℝ+) β†’ (𝑧 ∈ ℝ+ β†’ (βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))))
338337rexlimdv 3147 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑦 ∈ ℝ+) β†’ (βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)))
339338imp 408 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
340339adantllr 718 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
341231, 340reximddv3 43453 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦))
34232, 33, 35, 341syl21anc 837 . . . . . . . . . 10 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦))
343342ex 414 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (𝑦 ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦)))
34424, 25, 31, 343vtoclf 3518 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))))
34519, 344mpd 15 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)))
346 simpr 486 . . . . . . . . . . . 12 ((πœ‘ ∧ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)))
347 abssubrp 43600 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ β„‚ ∧ 𝐿 ∈ β„‚ ∧ 𝑅 β‰  𝐿) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ ℝ+)
3483, 7, 11, 347syl3anc 1372 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ ℝ+)
349348rpcnd 12967 . . . . . . . . . . . . . 14 (πœ‘ β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ β„‚)
350349adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ β„‚)
351 4cn 12246 . . . . . . . . . . . . . 14 4 ∈ β„‚
352351a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))) β†’ 4 ∈ β„‚)
353 4ne0 12269 . . . . . . . . . . . . . 14 4 β‰  0
354353a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))) β†’ 4 β‰  0)
355350, 352, 354divcan2d 11941 . . . . . . . . . . . 12 ((πœ‘ ∧ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))) β†’ (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)) = (absβ€˜(𝑅 βˆ’ 𝐿)))
356346, 355breqtrd 5135 . . . . . . . . . . 11 ((πœ‘ ∧ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿)))
357356ex 414 . . . . . . . . . 10 (πœ‘ β†’ ((absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿))))
358357a1d 25 . . . . . . . . 9 (πœ‘ β†’ ((π‘Ž ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) β†’ ((absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿)))))
359358ad2antrr 725 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ ((π‘Ž ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) β†’ ((absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿)))))
360359rexlimdvv 3201 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿))))
361345, 360mpd 15 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿)))
3629abscld 15330 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ ℝ)
363362ltnrd 11297 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ Β¬ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿)))
364361, 363pm2.65da 816 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ β„‚) β†’ Β¬ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))
365364ex 414 . . . 4 (πœ‘ β†’ (π‘₯ ∈ β„‚ β†’ Β¬ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)))
366 imnan 401 . . . 4 ((π‘₯ ∈ β„‚ β†’ Β¬ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ↔ Β¬ (π‘₯ ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)))
367365, 366sylib 217 . . 3 (πœ‘ β†’ Β¬ (π‘₯ ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)))
368 limclner.a . . . . 5 (πœ‘ β†’ 𝐴 βŠ† ℝ)
369368, 73sstrd 3958 . . . 4 (πœ‘ β†’ 𝐴 βŠ† β„‚)
37036, 369, 56ellimc3 25266 . . 3 (πœ‘ β†’ (π‘₯ ∈ (𝐹 limβ„‚ 𝐡) ↔ (π‘₯ ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))))
371367, 370mtbird 325 . 2 (πœ‘ β†’ Β¬ π‘₯ ∈ (𝐹 limβ„‚ 𝐡))
372371eq0rdv 4368 1 (πœ‘ β†’ (𝐹 limβ„‚ 𝐡) = βˆ…)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070   βˆ– cdif 3911   ∩ cin 3913   βŠ† wss 3914  βˆ…c0 4286  ifcif 4490  {csn 4590  βˆͺ cuni 4869   class class class wbr 5109  ran crn 5638   β†Ύ cres 5639  βŸΆwf 6496  β€˜cfv 6500  (class class class)co 7361  β„‚cc 11057  β„cr 11058  0cc0 11059   + caddc 11062   Β· cmul 11064  +∞cpnf 11194  -∞cmnf 11195   < clt 11197   ≀ cle 11198   βˆ’ cmin 11393   / cdiv 11820  4c4 12218  β„+crp 12923  (,)cioo 13273  abscabs 15128   β†Ύt crest 17310  TopOpenctopn 17311  topGenctg 17327  β„‚fldccnfld 20819  Topctop 22265  limPtclp 22508   limβ„‚ climc 25249
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-rep 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136  ax-pre-sup 11137
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-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-tp 4595  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-iin 4961  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7807  df-1st 7925  df-2nd 7926  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-1o 8416  df-er 8654  df-map 8773  df-pm 8774  df-en 8890  df-dom 8891  df-sdom 8892  df-fin 8893  df-fi 9355  df-sup 9386  df-inf 9387  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-div 11821  df-nn 12162  df-2 12224  df-3 12225  df-4 12226  df-5 12227  df-6 12228  df-7 12229  df-8 12230  df-9 12231  df-n0 12422  df-z 12508  df-dec 12627  df-uz 12772  df-q 12882  df-rp 12924  df-xneg 13041  df-xadd 13042  df-xmul 13043  df-ioo 13277  df-fz 13434  df-seq 13916  df-exp 13977  df-cj 14993  df-re 14994  df-im 14995  df-sqrt 15129  df-abs 15130  df-struct 17027  df-slot 17062  df-ndx 17074  df-base 17092  df-plusg 17154  df-mulr 17155  df-starv 17156  df-tset 17160  df-ple 17161  df-ds 17163  df-unif 17164  df-rest 17312  df-topn 17313  df-topgen 17333  df-psmet 20811  df-xmet 20812  df-met 20813  df-bl 20814  df-mopn 20815  df-cnfld 20820  df-top 22266  df-topon 22283  df-topsp 22305  df-bases 22319  df-cld 22393  df-ntr 22394  df-cls 22395  df-nei 22472  df-lp 22510  df-cnp 22602  df-xms 23696  df-ms 23697  df-limc 25253
This theorem is referenced by:  limclr  43986  jumpncnp  44229
  Copyright terms: Public domain W3C validator