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	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	dvdivbd.a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
	dvdivbd.adv	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) )
	dvdivbd.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
	dvdivbd.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ )
	dvdivbd.u	⊢ ( 𝜑 → 𝑈 ∈ ℝ )
	dvdivbd.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
	dvdivbd.t	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
	dvdivbd.q	⊢ ( 𝜑 → 𝑄 ∈ ℝ )
	dvdivbd.cbd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐶 ) ≤ 𝑈 )
	dvdivbd.bbd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐵 ) ≤ 𝑅 )
	dvdivbd.dbd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐷 ) ≤ 𝑇 )
	dvdivbd.abd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐴 ) ≤ 𝑄 )
	dvdivbd.bdv	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) )
	dvdivbd.d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ ℂ )
	dvdivbd.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ⁺ )
	dvdivbd.ele	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐸 ≤ ( abs ‘ 𝐵 ) )
	dvdivbd.f	⊢ 𝐹 = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐵 ) ) )
Assertion	dvdivbd	⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )

Proof

Step	Hyp	Ref	Expression
1		dvdivbd.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		dvdivbd.a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
3		dvdivbd.adv	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) )
4		dvdivbd.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
5		dvdivbd.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ )
6		dvdivbd.u	⊢ ( 𝜑 → 𝑈 ∈ ℝ )
7		dvdivbd.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
8		dvdivbd.t	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
9		dvdivbd.q	⊢ ( 𝜑 → 𝑄 ∈ ℝ )
10		dvdivbd.cbd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐶 ) ≤ 𝑈 )
11		dvdivbd.bbd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐵 ) ≤ 𝑅 )
12		dvdivbd.dbd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐷 ) ≤ 𝑇 )
13		dvdivbd.abd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐴 ) ≤ 𝑄 )
14		dvdivbd.bdv	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) )
15		dvdivbd.d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ ℂ )
16		dvdivbd.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ⁺ )
17		dvdivbd.ele	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐸 ≤ ( abs ‘ 𝐵 ) )
18		dvdivbd.f	⊢ 𝐹 = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐵 ) ) )
19	6 7	remulcld	⊢ ( 𝜑 → ( 𝑈 · 𝑅 ) ∈ ℝ )
20	8 9	remulcld	⊢ ( 𝜑 → ( 𝑇 · 𝑄 ) ∈ ℝ )
21	19 20	readdcld	⊢ ( 𝜑 → ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) ∈ ℝ )
22	16	rpred	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
23	22	resqcld	⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℝ )
24	16	rpcnd	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
25	16	rpgt0d	⊢ ( 𝜑 → 0 < 𝐸 )
26	25	gt0ne0d	⊢ ( 𝜑 → 𝐸 ≠ 0 )
27		2z	⊢ 2 ∈ ℤ
28	27	a1i	⊢ ( 𝜑 → 2 ∈ ℤ )
29	24 26 28	expne0d	⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ≠ 0 )
30	21 23 29	redivcld	⊢ ( 𝜑 → ( ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) / ( 𝐸 ↑ 2 ) ) ∈ ℝ )
31		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝐵 = 0 ) → 𝐵 = 0 )
32	31	abs00bd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝐵 = 0 ) → ( abs ‘ 𝐵 ) = 0 )
33		0red	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ∈ ℝ )
34	22	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐸 ∈ ℝ )
35	5	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
36	25	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 < 𝐸 )
37	17	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐸 ≤ ( abs ‘ 𝐵 ) )
38	33 34 35 36 37	ltletrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 < ( abs ‘ 𝐵 ) )
39	38	gt0ne0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐵 ) ≠ 0 )
40	39	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝐵 = 0 ) → ( abs ‘ 𝐵 ) ≠ 0 )
41	40	neneqd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝐵 = 0 ) → ¬ ( abs ‘ 𝐵 ) = 0 )
42	32 41	pm2.65da	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ¬ 𝐵 = 0 )
43	42	neqned	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ≠ 0 )
44		eldifsn	⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
45	5 43 44	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ( ℂ ∖ { 0 } ) )
46	1 2 4 3 45 15 14	dvmptdiv	⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐵 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) / ( 𝐵 ↑ 2 ) ) ) )
47	18 46	eqtrid	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) / ( 𝐵 ↑ 2 ) ) ) )
48	4 5	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
49	15 2	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐷 · 𝐴 ) ∈ ℂ )
50	48 49	subcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) ∈ ℂ )
51	5	sqcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
52		sqne0	⊢ ( 𝐵 ∈ ℂ → ( ( 𝐵 ↑ 2 ) ≠ 0 ↔ 𝐵 ≠ 0 ) )
53	5 52	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐵 ↑ 2 ) ≠ 0 ↔ 𝐵 ≠ 0 ) )
54	43 53	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐵 ↑ 2 ) ≠ 0 )
55	50 51 54	divcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) / ( 𝐵 ↑ 2 ) ) ∈ ℂ )
56	47 55	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) = ( ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) / ( 𝐵 ↑ 2 ) ) )
57	56	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) = ( abs ‘ ( ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) / ( 𝐵 ↑ 2 ) ) ) )
58	50 51 54	absdivd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) / ( 𝐵 ↑ 2 ) ) ) = ( ( abs ‘ ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) ) / ( abs ‘ ( 𝐵 ↑ 2 ) ) ) )
59	50	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) ) ∈ ℝ )
60	21	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) ∈ ℝ )
61	16	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐸 ∈ ℝ⁺ )
62	27	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 2 ∈ ℤ )
63	61 62	rpexpcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐸 ↑ 2 ) ∈ ℝ⁺ )
64	51	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐵 ↑ 2 ) ) ∈ ℝ )
65	50	absge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( abs ‘ ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) ) )
66	48	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐶 · 𝐵 ) ) ∈ ℝ )
67	49	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐷 · 𝐴 ) ) ∈ ℝ )
68	66 67	readdcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( abs ‘ ( 𝐶 · 𝐵 ) ) + ( abs ‘ ( 𝐷 · 𝐴 ) ) ) ∈ ℝ )
69	48 49	abs2dif2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) ) ≤ ( ( abs ‘ ( 𝐶 · 𝐵 ) ) + ( abs ‘ ( 𝐷 · 𝐴 ) ) ) )
70	19	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑈 · 𝑅 ) ∈ ℝ )
71	20	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑇 · 𝑄 ) ∈ ℝ )
72	4 5	absmuld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐶 · 𝐵 ) ) = ( ( abs ‘ 𝐶 ) · ( abs ‘ 𝐵 ) ) )
73	4	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐶 ) ∈ ℝ )
74	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑈 ∈ ℝ )
75	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑅 ∈ ℝ )
76	4	absge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( abs ‘ 𝐶 ) )
77	5	absge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( abs ‘ 𝐵 ) )
78	73 74 35 75 76 77 10 11	lemul12ad	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( abs ‘ 𝐶 ) · ( abs ‘ 𝐵 ) ) ≤ ( 𝑈 · 𝑅 ) )
79	72 78	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐶 · 𝐵 ) ) ≤ ( 𝑈 · 𝑅 ) )
80	15 2	absmuld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐷 · 𝐴 ) ) = ( ( abs ‘ 𝐷 ) · ( abs ‘ 𝐴 ) ) )
81	15	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐷 ) ∈ ℝ )
82	8	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑇 ∈ ℝ )
83	2	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
84	9	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑄 ∈ ℝ )
85	15	absge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( abs ‘ 𝐷 ) )
86	2	absge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( abs ‘ 𝐴 ) )
87	81 82 83 84 85 86 12 13	lemul12ad	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( abs ‘ 𝐷 ) · ( abs ‘ 𝐴 ) ) ≤ ( 𝑇 · 𝑄 ) )
88	80 87	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐷 · 𝐴 ) ) ≤ ( 𝑇 · 𝑄 ) )
89	66 67 70 71 79 88	le2addd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( abs ‘ ( 𝐶 · 𝐵 ) ) + ( abs ‘ ( 𝐷 · 𝐴 ) ) ) ≤ ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) )
90	59 68 60 69 89	letrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) ) ≤ ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) )
91		2nn0	⊢ 2 ∈ ℕ₀
92	91	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 2 ∈ ℕ₀ )
93	33 34 36	ltled	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ 𝐸 )
94		leexp1a	⊢ ( ( ( 𝐸 ∈ ℝ ∧ ( abs ‘ 𝐵 ) ∈ ℝ ∧ 2 ∈ ℕ₀ ) ∧ ( 0 ≤ 𝐸 ∧ 𝐸 ≤ ( abs ‘ 𝐵 ) ) ) → ( 𝐸 ↑ 2 ) ≤ ( ( abs ‘ 𝐵 ) ↑ 2 ) )
95	34 35 92 93 37 94	syl32anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐸 ↑ 2 ) ≤ ( ( abs ‘ 𝐵 ) ↑ 2 ) )
96	5 92	absexpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐵 ↑ 2 ) ) = ( ( abs ‘ 𝐵 ) ↑ 2 ) )
97	95 96	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐸 ↑ 2 ) ≤ ( abs ‘ ( 𝐵 ↑ 2 ) ) )
98	59 60 63 64 65 90 97	lediv12ad	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( abs ‘ ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) ) / ( abs ‘ ( 𝐵 ↑ 2 ) ) ) ≤ ( ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) / ( 𝐸 ↑ 2 ) ) )
99	58 98	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( ( ( 𝐶 · 𝐵 ) − ( 𝐷 · 𝐴 ) ) / ( 𝐵 ↑ 2 ) ) ) ≤ ( ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) / ( 𝐸 ↑ 2 ) ) )
100	57 99	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) / ( 𝐸 ↑ 2 ) ) )
101	100	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) / ( 𝐸 ↑ 2 ) ) )
102		brralrspcev	⊢ ( ( ( ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) / ( 𝐸 ↑ 2 ) ) ∈ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( ( ( 𝑈 · 𝑅 ) + ( 𝑇 · 𝑄 ) ) / ( 𝐸 ↑ 2 ) ) ) → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )
103	30 101 102	syl2anc	⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )

Metamath Proof Explorer

Theorem dvdivbd

Proof