Metamath Proof Explorer


Theorem unblimceq0lem

Description: Lemma for unblimceq0 . (Contributed by Asger C. Ipsen, 12-May-2021)

Ref Expression
Hypotheses unblimceq0lem.0 ( 𝜑𝑆 ⊆ ℂ )
unblimceq0lem.1 ( 𝜑𝐹 : 𝑆 ⟶ ℂ )
unblimceq0lem.2 ( 𝜑𝐴 ∈ ℂ )
unblimceq0lem.3 ( 𝜑 → ∀ 𝑏 ∈ ℝ+𝑑 ∈ ℝ+𝑥𝑆 ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑𝑏 ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) )
Assertion unblimceq0lem ( 𝜑 → ∀ 𝑐 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑆 ( 𝑦𝐴 ∧ ( abs ‘ ( 𝑦𝐴 ) ) < 𝑑𝑐 ≤ ( abs ‘ ( 𝐹𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 unblimceq0lem.0 ( 𝜑𝑆 ⊆ ℂ )
2 unblimceq0lem.1 ( 𝜑𝐹 : 𝑆 ⟶ ℂ )
3 unblimceq0lem.2 ( 𝜑𝐴 ∈ ℂ )
4 unblimceq0lem.3 ( 𝜑 → ∀ 𝑏 ∈ ℝ+𝑑 ∈ ℝ+𝑥𝑆 ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑𝑏 ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) )
5 breq1 ( 𝑏 = if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) → ( 𝑏 ≤ ( abs ‘ ( 𝐹𝑥 ) ) ↔ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) )
6 5 anbi2d ( 𝑏 = if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) → ( ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑𝑏 ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ↔ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) )
7 6 rexbidv ( 𝑏 = if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) → ( ∃ 𝑥𝑆 ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑𝑏 ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ↔ ∃ 𝑥𝑆 ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) )
8 7 ralbidv ( 𝑏 = if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) → ( ∀ 𝑑 ∈ ℝ+𝑥𝑆 ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑𝑏 ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ↔ ∀ 𝑑 ∈ ℝ+𝑥𝑆 ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) )
9 4 adantr ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) → ∀ 𝑏 ∈ ℝ+𝑑 ∈ ℝ+𝑥𝑆 ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑𝑏 ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) )
10 2 ad2antrr ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ 𝐴𝑆 ) → 𝐹 : 𝑆 ⟶ ℂ )
11 simpr ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ 𝐴𝑆 ) → 𝐴𝑆 )
12 10 11 ffvelrnd ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ 𝐴𝑆 ) → ( 𝐹𝐴 ) ∈ ℂ )
13 12 abscld ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ 𝐴𝑆 ) → ( abs ‘ ( 𝐹𝐴 ) ) ∈ ℝ )
14 simprl ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) → 𝑐 ∈ ℝ+ )
15 14 rpred ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) → 𝑐 ∈ ℝ )
16 15 adantr ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ 𝐴𝑆 ) → 𝑐 ∈ ℝ )
17 13 16 readdcld ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ 𝐴𝑆 ) → ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) ∈ ℝ )
18 12 absge0d ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ 𝐴𝑆 ) → 0 ≤ ( abs ‘ ( 𝐹𝐴 ) ) )
19 14 rpgt0d ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) → 0 < 𝑐 )
20 19 adantr ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ 𝐴𝑆 ) → 0 < 𝑐 )
21 13 16 18 20 addgegt0d ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ 𝐴𝑆 ) → 0 < ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) )
22 17 21 elrpd ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ 𝐴𝑆 ) → ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) ∈ ℝ+ )
23 simplrl ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ¬ 𝐴𝑆 ) → 𝑐 ∈ ℝ+ )
24 22 23 ifclda ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) → if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ∈ ℝ+ )
25 8 9 24 rspcdva ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) → ∀ 𝑑 ∈ ℝ+𝑥𝑆 ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) )
26 simprr ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) → 𝑑 ∈ ℝ+ )
27 rsp ( ∀ 𝑑 ∈ ℝ+𝑥𝑆 ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) → ( 𝑑 ∈ ℝ+ → ∃ 𝑥𝑆 ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) )
28 25 26 27 sylc ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) → ∃ 𝑥𝑆 ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) )
29 simprl ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) → 𝑥𝑆 )
30 neeq1 ( 𝑦 = 𝑥 → ( 𝑦𝐴𝑥𝐴 ) )
31 fvoveq1 ( 𝑦 = 𝑥 → ( abs ‘ ( 𝑦𝐴 ) ) = ( abs ‘ ( 𝑥𝐴 ) ) )
32 31 breq1d ( 𝑦 = 𝑥 → ( ( abs ‘ ( 𝑦𝐴 ) ) < 𝑑 ↔ ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ) )
33 2fveq3 ( 𝑦 = 𝑥 → ( abs ‘ ( 𝐹𝑦 ) ) = ( abs ‘ ( 𝐹𝑥 ) ) )
34 33 breq2d ( 𝑦 = 𝑥 → ( 𝑐 ≤ ( abs ‘ ( 𝐹𝑦 ) ) ↔ 𝑐 ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) )
35 30 32 34 3anbi123d ( 𝑦 = 𝑥 → ( ( 𝑦𝐴 ∧ ( abs ‘ ( 𝑦𝐴 ) ) < 𝑑𝑐 ≤ ( abs ‘ ( 𝐹𝑦 ) ) ) ↔ ( 𝑥𝐴 ∧ ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑𝑐 ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) )
36 35 adantl ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝑦 = 𝑥 ) → ( ( 𝑦𝐴 ∧ ( abs ‘ ( 𝑦𝐴 ) ) < 𝑑𝑐 ≤ ( abs ‘ ( 𝐹𝑦 ) ) ) ↔ ( 𝑥𝐴 ∧ ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑𝑐 ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) )
37 17 adantlr ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) ∈ ℝ )
38 2 ad2antrr ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) → 𝐹 : 𝑆 ⟶ ℂ )
39 38 29 ffvelrnd ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) → ( 𝐹𝑥 ) ∈ ℂ )
40 39 abscld ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) → ( abs ‘ ( 𝐹𝑥 ) ) ∈ ℝ )
41 40 adantr ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → ( abs ‘ ( 𝐹𝑥 ) ) ∈ ℝ )
42 simpr ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → 𝐴𝑆 )
43 42 iftrued ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) = ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) )
44 43 eqcomd ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) = if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) )
45 simprrr ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) → if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) )
46 45 adantr ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) )
47 44 46 eqbrtrd ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) )
48 37 41 47 lensymd ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → ¬ ( abs ‘ ( 𝐹𝑥 ) ) < ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) )
49 2fveq3 ( 𝑥 = 𝐴 → ( abs ‘ ( 𝐹𝑥 ) ) = ( abs ‘ ( 𝐹𝐴 ) ) )
50 49 adantl ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ 𝐴𝑆 ) ∧ 𝑥 = 𝐴 ) → ( abs ‘ ( 𝐹𝑥 ) ) = ( abs ‘ ( 𝐹𝐴 ) ) )
51 16 13 ltaddposd ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ 𝐴𝑆 ) → ( 0 < 𝑐 ↔ ( abs ‘ ( 𝐹𝐴 ) ) < ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) ) )
52 20 51 mpbid ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ 𝐴𝑆 ) → ( abs ‘ ( 𝐹𝐴 ) ) < ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) )
53 52 adantr ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ 𝐴𝑆 ) ∧ 𝑥 = 𝐴 ) → ( abs ‘ ( 𝐹𝐴 ) ) < ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) )
54 50 53 eqbrtrd ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ 𝐴𝑆 ) ∧ 𝑥 = 𝐴 ) → ( abs ‘ ( 𝐹𝑥 ) ) < ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) )
55 54 ex ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ 𝐴𝑆 ) → ( 𝑥 = 𝐴 → ( abs ‘ ( 𝐹𝑥 ) ) < ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) ) )
56 55 adantlr ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → ( 𝑥 = 𝐴 → ( abs ‘ ( 𝐹𝑥 ) ) < ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) ) )
57 56 necon3bd ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → ( ¬ ( abs ‘ ( 𝐹𝑥 ) ) < ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) → 𝑥𝐴 ) )
58 48 57 mpd ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → 𝑥𝐴 )
59 simprrl ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) → ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 )
60 59 adantr ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 )
61 16 adantlr ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → 𝑐 ∈ ℝ )
62 12 adantlr ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → ( 𝐹𝐴 ) ∈ ℂ )
63 62 absge0d ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → 0 ≤ ( abs ‘ ( 𝐹𝐴 ) ) )
64 13 adantlr ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → ( abs ‘ ( 𝐹𝐴 ) ) ∈ ℝ )
65 61 64 addge02d ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → ( 0 ≤ ( abs ‘ ( 𝐹𝐴 ) ) ↔ 𝑐 ≤ ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) ) )
66 63 65 mpbid ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → 𝑐 ≤ ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) )
67 61 37 41 66 47 letrd ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → 𝑐 ≤ ( abs ‘ ( 𝐹𝑥 ) ) )
68 58 60 67 3jca ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ 𝐴𝑆 ) → ( 𝑥𝐴 ∧ ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑𝑐 ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) )
69 simpr ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ ¬ 𝐴𝑆 ) → ¬ 𝐴𝑆 )
70 simpr ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ ¬ 𝐴𝑆 ) ∧ 𝑥 = 𝐴 ) → 𝑥 = 𝐴 )
71 29 adantr ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ ¬ 𝐴𝑆 ) → 𝑥𝑆 )
72 71 adantr ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ ¬ 𝐴𝑆 ) ∧ 𝑥 = 𝐴 ) → 𝑥𝑆 )
73 70 72 eqeltrrd ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ ¬ 𝐴𝑆 ) ∧ 𝑥 = 𝐴 ) → 𝐴𝑆 )
74 73 ex ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ ¬ 𝐴𝑆 ) → ( 𝑥 = 𝐴𝐴𝑆 ) )
75 74 necon3bd ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ ¬ 𝐴𝑆 ) → ( ¬ 𝐴𝑆𝑥𝐴 ) )
76 69 75 mpd ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ ¬ 𝐴𝑆 ) → 𝑥𝐴 )
77 59 adantr ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ ¬ 𝐴𝑆 ) → ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 )
78 69 iffalsed ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ ¬ 𝐴𝑆 ) → if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) = 𝑐 )
79 78 eqcomd ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ ¬ 𝐴𝑆 ) → 𝑐 = if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) )
80 45 adantr ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ ¬ 𝐴𝑆 ) → if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) )
81 79 80 eqbrtrd ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ ¬ 𝐴𝑆 ) → 𝑐 ≤ ( abs ‘ ( 𝐹𝑥 ) ) )
82 76 77 81 3jca ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) ∧ ¬ 𝐴𝑆 ) → ( 𝑥𝐴 ∧ ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑𝑐 ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) )
83 68 82 pm2.61dan ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) → ( 𝑥𝐴 ∧ ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑𝑐 ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) )
84 29 36 83 rspcedvd ( ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥𝑆 ∧ ( ( abs ‘ ( 𝑥𝐴 ) ) < 𝑑 ∧ if ( 𝐴𝑆 , ( ( abs ‘ ( 𝐹𝐴 ) ) + 𝑐 ) , 𝑐 ) ≤ ( abs ‘ ( 𝐹𝑥 ) ) ) ) ) → ∃ 𝑦𝑆 ( 𝑦𝐴 ∧ ( abs ‘ ( 𝑦𝐴 ) ) < 𝑑𝑐 ≤ ( abs ‘ ( 𝐹𝑦 ) ) ) )
85 28 84 rexlimddv ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ+𝑑 ∈ ℝ+ ) ) → ∃ 𝑦𝑆 ( 𝑦𝐴 ∧ ( abs ‘ ( 𝑦𝐴 ) ) < 𝑑𝑐 ≤ ( abs ‘ ( 𝐹𝑦 ) ) ) )
86 85 ralrimivva ( 𝜑 → ∀ 𝑐 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑆 ( 𝑦𝐴 ∧ ( abs ‘ ( 𝑦𝐴 ) ) < 𝑑𝑐 ≤ ( abs ‘ ( 𝐹𝑦 ) ) ) )