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 𝐹 ) )