dvdivbd

Description: A sufficient condition for the derivative to be bounded, for the quotient of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	dvdivbd.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvdivbd.a	$⊢ (φ \land x \in X) \to A \in ℂ$
	dvdivbd.adv	$⊢ φ \to \frac{d (x \in X⟼ A)}{d_{S} x} = (x \in X ⟼ C)$
	dvdivbd.c	$⊢ (φ \land x \in X) \to C \in ℂ$
	dvdivbd.b	$⊢ (φ \land x \in X) \to B \in ℂ$
	dvdivbd.u	$⊢ φ \to U \in ℝ$
	dvdivbd.r	$⊢ φ \to R \in ℝ$
	dvdivbd.t	$⊢ φ \to T \in ℝ$
	dvdivbd.q	$⊢ φ \to Q \in ℝ$
	dvdivbd.cbd	$⊢ (φ \land x \in X) \to \|C\| \leq U$
	dvdivbd.bbd	$⊢ (φ \land x \in X) \to \|B\| \leq R$
	dvdivbd.dbd	$⊢ (φ \land x \in X) \to \|D\| \leq T$
	dvdivbd.abd	$⊢ (φ \land x \in X) \to \|A\| \leq Q$
	dvdivbd.bdv	$⊢ φ \to \frac{d (x \in X⟼ B)}{d_{S} x} = (x \in X ⟼ D)$
	dvdivbd.d	$⊢ (φ \land x \in X) \to D \in ℂ$
	dvdivbd.e	$⊢ φ \to E \in ℝ^{+}$
	dvdivbd.ele	$⊢ φ \to \forall x \in X E \leq \|B\|$
	dvdivbd.f	$⊢ F = \frac{d (x \in X⟼ \frac{A}{B})}{d_{S} x}$
Assertion	dvdivbd	$⊢ φ \to \exists b \in ℝ \forall x \in X \|F (x)\| \leq b$

Proof

Step	Hyp	Ref	Expression
1		dvdivbd.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvdivbd.a	$⊢ (φ \land x \in X) \to A \in ℂ$
3		dvdivbd.adv	$⊢ φ \to \frac{d (x \in X⟼ A)}{d_{S} x} = (x \in X ⟼ C)$
4		dvdivbd.c	$⊢ (φ \land x \in X) \to C \in ℂ$
5		dvdivbd.b	$⊢ (φ \land x \in X) \to B \in ℂ$
6		dvdivbd.u	$⊢ φ \to U \in ℝ$
7		dvdivbd.r	$⊢ φ \to R \in ℝ$
8		dvdivbd.t	$⊢ φ \to T \in ℝ$
9		dvdivbd.q	$⊢ φ \to Q \in ℝ$
10		dvdivbd.cbd	$⊢ (φ \land x \in X) \to \|C\| \leq U$
11		dvdivbd.bbd	$⊢ (φ \land x \in X) \to \|B\| \leq R$
12		dvdivbd.dbd	$⊢ (φ \land x \in X) \to \|D\| \leq T$
13		dvdivbd.abd	$⊢ (φ \land x \in X) \to \|A\| \leq Q$
14		dvdivbd.bdv	$⊢ φ \to \frac{d (x \in X⟼ B)}{d_{S} x} = (x \in X ⟼ D)$
15		dvdivbd.d	$⊢ (φ \land x \in X) \to D \in ℂ$
16		dvdivbd.e	$⊢ φ \to E \in ℝ^{+}$
17		dvdivbd.ele	$⊢ φ \to \forall x \in X E \leq \|B\|$
18		dvdivbd.f	$⊢ F = \frac{d (x \in X⟼ \frac{A}{B})}{d_{S} x}$
19	6 7	remulcld	$⊢ φ \to U R \in ℝ$
20	8 9	remulcld	$⊢ φ \to T Q \in ℝ$
21	19 20	readdcld	$⊢ φ \to U R + T Q \in ℝ$
22	16	rpred	$⊢ φ \to E \in ℝ$
23	22	resqcld	$⊢ φ \to E^{2} \in ℝ$
24	16	rpcnd	$⊢ φ \to E \in ℂ$
25	16	rpgt0d	$⊢ φ \to 0 < E$
26	25	gt0ne0d	$⊢ φ \to E \neq 0$
27		2z	$⊢ 2 \in ℤ$
28	27	a1i	$⊢ φ \to 2 \in ℤ$
29	24 26 28	expne0d	$⊢ φ \to E^{2} \neq 0$
30	21 23 29	redivcld	$⊢ φ \to \frac{U R + T Q}{E^{2}} \in ℝ$
31		simpr	$⊢ ((φ \land x \in X) \land B = 0) \to B = 0$
32	31	abs00bd	$⊢ ((φ \land x \in X) \land B = 0) \to \|B\| = 0$
33		0red	$⊢ (φ \land x \in X) \to 0 \in ℝ$
34	22	adantr	$⊢ (φ \land x \in X) \to E \in ℝ$
35	5	abscld	$⊢ (φ \land x \in X) \to \|B\| \in ℝ$
36	25	adantr	$⊢ (φ \land x \in X) \to 0 < E$
37	17	r19.21bi	$⊢ (φ \land x \in X) \to E \leq \|B\|$
38	33 34 35 36 37	ltletrd	$⊢ (φ \land x \in X) \to 0 < \|B\|$
39	38	gt0ne0d	$⊢ (φ \land x \in X) \to \|B\| \neq 0$
40	39	adantr	$⊢ ((φ \land x \in X) \land B = 0) \to \|B\| \neq 0$
41	40	neneqd	$⊢ ((φ \land x \in X) \land B = 0) \to \neg \|B\| = 0$
42	32 41	pm2.65da	$⊢ (φ \land x \in X) \to \neg B = 0$
43	42	neqned	$⊢ (φ \land x \in X) \to B \neq 0$
44		eldifsn	$⊢ B \in (ℂ ∖ \{0\}) \leftrightarrow (B \in ℂ \land B \neq 0)$
45	5 43 44	sylanbrc	$⊢ (φ \land x \in X) \to B \in (ℂ ∖ \{0\})$
46	1 2 4 3 45 15 14	dvmptdiv	$⊢ φ \to \frac{d (x \in X⟼ \frac{A}{B})}{d_{S} x} = (x \in X ⟼ \frac{C B - D A}{B^{2}})$
47	18 46	eqtrid	$⊢ φ \to F = (x \in X ⟼ \frac{C B - D A}{B^{2}})$
48	4 5	mulcld	$⊢ (φ \land x \in X) \to C B \in ℂ$
49	15 2	mulcld	$⊢ (φ \land x \in X) \to D A \in ℂ$
50	48 49	subcld	$⊢ (φ \land x \in X) \to C B - D A \in ℂ$
51	5	sqcld	$⊢ (φ \land x \in X) \to B^{2} \in ℂ$
52		sqne0	$⊢ B \in ℂ \to (B^{2} \neq 0 \leftrightarrow B \neq 0)$
53	5 52	syl	$⊢ (φ \land x \in X) \to (B^{2} \neq 0 \leftrightarrow B \neq 0)$
54	43 53	mpbird	$⊢ (φ \land x \in X) \to B^{2} \neq 0$
55	50 51 54	divcld	$⊢ (φ \land x \in X) \to \frac{C B - D A}{B^{2}} \in ℂ$
56	47 55	fvmpt2d	$⊢ (φ \land x \in X) \to F (x) = \frac{C B - D A}{B^{2}}$
57	56	fveq2d	$⊢ (φ \land x \in X) \to \|F (x)\| = \|\frac{C B - D A}{B^{2}}\|$
58	50 51 54	absdivd	$⊢ (φ \land x \in X) \to \|\frac{C B - D A}{B^{2}}\| = \frac{\|C B - D A\|}{\|B^{2}\|}$
59	50	abscld	$⊢ (φ \land x \in X) \to \|C B - D A\| \in ℝ$
60	21	adantr	$⊢ (φ \land x \in X) \to U R + T Q \in ℝ$
61	16	adantr	$⊢ (φ \land x \in X) \to E \in ℝ^{+}$
62	27	a1i	$⊢ (φ \land x \in X) \to 2 \in ℤ$
63	61 62	rpexpcld	$⊢ (φ \land x \in X) \to E^{2} \in ℝ^{+}$
64	51	abscld	$⊢ (φ \land x \in X) \to \|B^{2}\| \in ℝ$
65	50	absge0d	$⊢ (φ \land x \in X) \to 0 \leq \|C B - D A\|$
66	48	abscld	$⊢ (φ \land x \in X) \to \|C B\| \in ℝ$
67	49	abscld	$⊢ (φ \land x \in X) \to \|D A\| \in ℝ$
68	66 67	readdcld	$⊢ (φ \land x \in X) \to \|C B\| + \|D A\| \in ℝ$
69	48 49	abs2dif2d	$⊢ (φ \land x \in X) \to \|C B - D A\| \leq \|C B\| + \|D A\|$
70	19	adantr	$⊢ (φ \land x \in X) \to U R \in ℝ$
71	20	adantr	$⊢ (φ \land x \in X) \to T Q \in ℝ$
72	4 5	absmuld	$⊢ (φ \land x \in X) \to \|C B\| = \|C\| \|B\|$
73	4	abscld	$⊢ (φ \land x \in X) \to \|C\| \in ℝ$
74	6	adantr	$⊢ (φ \land x \in X) \to U \in ℝ$
75	7	adantr	$⊢ (φ \land x \in X) \to R \in ℝ$
76	4	absge0d	$⊢ (φ \land x \in X) \to 0 \leq \|C\|$
77	5	absge0d	$⊢ (φ \land x \in X) \to 0 \leq \|B\|$
78	73 74 35 75 76 77 10 11	lemul12ad	$⊢ (φ \land x \in X) \to \|C\| \|B\| \leq U R$
79	72 78	eqbrtrd	$⊢ (φ \land x \in X) \to \|C B\| \leq U R$
80	15 2	absmuld	$⊢ (φ \land x \in X) \to \|D A\| = \|D\| \|A\|$
81	15	abscld	$⊢ (φ \land x \in X) \to \|D\| \in ℝ$
82	8	adantr	$⊢ (φ \land x \in X) \to T \in ℝ$
83	2	abscld	$⊢ (φ \land x \in X) \to \|A\| \in ℝ$
84	9	adantr	$⊢ (φ \land x \in X) \to Q \in ℝ$
85	15	absge0d	$⊢ (φ \land x \in X) \to 0 \leq \|D\|$
86	2	absge0d	$⊢ (φ \land x \in X) \to 0 \leq \|A\|$
87	81 82 83 84 85 86 12 13	lemul12ad	$⊢ (φ \land x \in X) \to \|D\| \|A\| \leq T Q$
88	80 87	eqbrtrd	$⊢ (φ \land x \in X) \to \|D A\| \leq T Q$
89	66 67 70 71 79 88	le2addd	$⊢ (φ \land x \in X) \to \|C B\| + \|D A\| \leq U R + T Q$
90	59 68 60 69 89	letrd	$⊢ (φ \land x \in X) \to \|C B - D A\| \leq U R + T Q$
91		2nn0	$⊢ 2 \in ℕ_{0}$
92	91	a1i	$⊢ (φ \land x \in X) \to 2 \in ℕ_{0}$
93	33 34 36	ltled	$⊢ (φ \land x \in X) \to 0 \leq E$
94		leexp1a	$⊢ ((E \in ℝ \land \|B\| \in ℝ \land 2 \in ℕ_{0}) \land (0 \leq E \land E \leq \|B\|)) \to E^{2} \leq {\|B\|}^{2}$
95	34 35 92 93 37 94	syl32anc	$⊢ (φ \land x \in X) \to E^{2} \leq {\|B\|}^{2}$
96	5 92	absexpd	$⊢ (φ \land x \in X) \to \|B^{2}\| = {\|B\|}^{2}$
97	95 96	breqtrrd	$⊢ (φ \land x \in X) \to E^{2} \leq \|B^{2}\|$
98	59 60 63 64 65 90 97	lediv12ad	$⊢ (φ \land x \in X) \to \frac{\|C B - D A\|}{\|B^{2}\|} \leq \frac{U R + T Q}{E^{2}}$
99	58 98	eqbrtrd	$⊢ (φ \land x \in X) \to \|\frac{C B - D A}{B^{2}}\| \leq \frac{U R + T Q}{E^{2}}$
100	57 99	eqbrtrd	$⊢ (φ \land x \in X) \to \|F (x)\| \leq \frac{U R + T Q}{E^{2}}$
101	100	ralrimiva	$⊢ φ \to \forall x \in X \|F (x)\| \leq \frac{U R + T Q}{E^{2}}$
102		brralrspcev	$⊢ (\frac{U R + T Q}{E^{2}} \in ℝ \land \forall x \in X \|F (x)\| \leq \frac{U R + T Q}{E^{2}}) \to \exists b \in ℝ \forall x \in X \|F (x)\| \leq b$
103	30 101 102	syl2anc	$⊢ φ \to \exists b \in ℝ \forall x \in X \|F (x)\| \leq b$

Metamath Proof Explorer

Theorem dvdivbd

Proof