Metamath Proof Explorer

Theorem unbdqndv2

Description: Variant of unbdqndv1 with the hypothesis that ( ( ( Fy ) - ( Fx ) ) / ( y - x ) ) is unbounded where x <_ A and A <_ y . (Contributed by Asger C. Ipsen, 12-May-2021)

Ref Expression
Hypotheses unbdqndv2.x ⊢ ( 𝜑 → 𝑋 ⊆ ℝ )
unbdqndv2.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
unbdqndv2.1 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ℝ+ ∀ 𝑑 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑏 ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) )
Assertion unbdqndv2 ( 𝜑 → ¬ 𝐴 ∈ dom ( ℝ D 𝐹 ) )

Proof

Step Hyp Ref Expression
1 unbdqndv2.x ⊢ ( 𝜑 → 𝑋 ⊆ ℝ )
2 unbdqndv2.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
3 unbdqndv2.1 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ℝ+ ∀ 𝑑 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑏 ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) )
4 eqid ⊢ ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) ) = ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) )
5 ax-resscn ⊢ ℝ ⊆ ℂ
6 5 a1i ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) → ℝ ⊆ ℂ )
7 1 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) → 𝑋 ⊆ ℝ )
8 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) → 𝐹 : 𝑋 ⟶ ℂ )
9 breq1 ⊢ ( 𝑏 = ( 2 · 𝑐 ) → ( 𝑏 ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ↔ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) )
10 9 3anbi3d ⊢ ( 𝑏 = ( 2 · 𝑐 ) → ( ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑏 ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ↔ ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) )
11 10 rexbidv ⊢ ( 𝑏 = ( 2 · 𝑐 ) → ( ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑏 ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ↔ ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) )
12 11 rexbidv ⊢ ( 𝑏 = ( 2 · 𝑐 ) → ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑏 ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) )
13 12 ralbidv ⊢ ( 𝑏 = ( 2 · 𝑐 ) → ( ∀ 𝑑 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑏 ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ↔ ∀ 𝑑 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) )
14 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → ∀ 𝑏 ∈ ℝ+ ∀ 𝑑 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑏 ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) )
15 2rp ⊢ 2 ∈ ℝ+
16 15 a1i ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → 2 ∈ ℝ+ )
17 simprl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → 𝑐 ∈ ℝ+ )
18 16 17 rpmulcld ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → ( 2 · 𝑐 ) ∈ ℝ+ )
19 13 14 18 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → ∀ 𝑑 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) )
20 simprr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → 𝑑 ∈ ℝ+ )
21 rsp ⊢ ( ∀ 𝑑 ∈ ℝ+ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) → ( 𝑑 ∈ ℝ+ → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) )
22 19 20 21 sylc ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) )
23 eqid ⊢ if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) = if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 )
24 7 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) → 𝑋 ⊆ ℝ )
25 8 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) → 𝐹 : 𝑋 ⟶ ℂ )
26 6 8 7 dvbss ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) → dom ( ℝ D 𝐹 ) ⊆ 𝑋 )
27 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) → 𝐴 ∈ dom ( ℝ D 𝐹 ) )
28 26 27 sseldd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) → 𝐴 ∈ 𝑋 )
29 28 adantr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → 𝐴 ∈ 𝑋 )
30 29 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
31 30 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) → 𝐴 ∈ 𝑋 )
32 17 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) → 𝑐 ∈ ℝ+ )
33 20 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) → 𝑑 ∈ ℝ+ )
34 simplrl ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) → 𝑥 ∈ 𝑋 )
35 simplrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) → 𝑦 ∈ 𝑋 )
36 simpr2r ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) → 𝑥 ≠ 𝑦 )
37 simpr1l ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) → 𝑥 ≤ 𝐴 )
38 simpr1r ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) → 𝐴 ≤ 𝑦 )
39 simpr2l ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) → ( 𝑦 − 𝑥 ) < 𝑑 )
40 simpr3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) → ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) )
41 4 23 24 25 31 32 33 34 35 36 37 38 39 40 unbdqndv2lem2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) → ( if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) ∈ ( 𝑋 ∖ { 𝐴 } ) ∧ ( ( abs ‘ ( if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) − 𝐴 ) ) < 𝑑 ∧ 𝑐 ≤ ( abs ‘ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) ) ‘ if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) ) ) ) ) )
42 41 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) → if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) ∈ ( 𝑋 ∖ { 𝐴 } ) )
43 fvoveq1 ⊢ ( 𝑤 = if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) → ( abs ‘ ( 𝑤 − 𝐴 ) ) = ( abs ‘ ( if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) − 𝐴 ) ) )
44 43 breq1d ⊢ ( 𝑤 = if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) → ( ( abs ‘ ( 𝑤 − 𝐴 ) ) < 𝑑 ↔ ( abs ‘ ( if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) − 𝐴 ) ) < 𝑑 ) )
45 2fveq3 ⊢ ( 𝑤 = if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) → ( abs ‘ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) ) ‘ 𝑤 ) ) = ( abs ‘ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) ) ‘ if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) ) ) )
46 45 breq2d ⊢ ( 𝑤 = if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) → ( 𝑐 ≤ ( abs ‘ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) ) ‘ 𝑤 ) ) ↔ 𝑐 ≤ ( abs ‘ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) ) ‘ if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) ) ) ) )
47 44 46 anbi12d ⊢ ( 𝑤 = if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) → ( ( ( abs ‘ ( 𝑤 − 𝐴 ) ) < 𝑑 ∧ 𝑐 ≤ ( abs ‘ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) ) ‘ 𝑤 ) ) ) ↔ ( ( abs ‘ ( if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) − 𝐴 ) ) < 𝑑 ∧ 𝑐 ≤ ( abs ‘ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) ) ‘ if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) ) ) ) ) )
48 47 adantl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) ∧ 𝑤 = if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) ) → ( ( ( abs ‘ ( 𝑤 − 𝐴 ) ) < 𝑑 ∧ 𝑐 ≤ ( abs ‘ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) ) ‘ 𝑤 ) ) ) ↔ ( ( abs ‘ ( if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) − 𝐴 ) ) < 𝑑 ∧ 𝑐 ≤ ( abs ‘ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) ) ‘ if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) ) ) ) ) )
49 41 simprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) → ( ( abs ‘ ( if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) − 𝐴 ) ) < 𝑑 ∧ 𝑐 ≤ ( abs ‘ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) ) ‘ if ( ( 𝑐 · ( 𝑦 − 𝑥 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐴 ) ) ) , 𝑥 , 𝑦 ) ) ) ) )
50 42 48 49 rspcedvd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) ) → ∃ 𝑤 ∈ ( 𝑋 ∖ { 𝐴 } ) ( ( abs ‘ ( 𝑤 − 𝐴 ) ) < 𝑑 ∧ 𝑐 ≤ ( abs ‘ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) ) ‘ 𝑤 ) ) ) )
51 50 ex ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) → ∃ 𝑤 ∈ ( 𝑋 ∖ { 𝐴 } ) ( ( abs ‘ ( 𝑤 − 𝐴 ) ) < 𝑑 ∧ 𝑐 ≤ ( abs ‘ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) ) ‘ 𝑤 ) ) ) ) )
52 51 rexlimdvva ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 ≤ 𝑦 ) ∧ ( ( 𝑦 − 𝑥 ) < 𝑑 ∧ 𝑥 ≠ 𝑦 ) ∧ ( 2 · 𝑐 ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) / ( 𝑦 − 𝑥 ) ) ) → ∃ 𝑤 ∈ ( 𝑋 ∖ { 𝐴 } ) ( ( abs ‘ ( 𝑤 − 𝐴 ) ) < 𝑑 ∧ 𝑐 ≤ ( abs ‘ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) ) ‘ 𝑤 ) ) ) ) )
53 22 52 mpd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) ∧ ( 𝑐 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → ∃ 𝑤 ∈ ( 𝑋 ∖ { 𝐴 } ) ( ( abs ‘ ( 𝑤 − 𝐴 ) ) < 𝑑 ∧ 𝑐 ≤ ( abs ‘ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) ) ‘ 𝑤 ) ) ) )
54 53 ralrimivva ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) → ∀ 𝑐 ∈ ℝ+ ∀ 𝑑 ∈ ℝ+ ∃ 𝑤 ∈ ( 𝑋 ∖ { 𝐴 } ) ( ( abs ‘ ( 𝑤 − 𝐴 ) ) < 𝑑 ∧ 𝑐 ≤ ( abs ‘ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐴 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝑧 − 𝐴 ) ) ) ‘ 𝑤 ) ) ) )
55 4 6 7 8 54 unbdqndv1 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( ℝ D 𝐹 ) ) → ¬ 𝐴 ∈ dom ( ℝ D 𝐹 ) )
56 55 pm2.01da ⊢ ( 𝜑 → ¬ 𝐴 ∈ dom ( ℝ D 𝐹 ) )