Theorem unbdqndv2lem1

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

	Ref	Expression
Hypotheses	unbdqndv2lem1.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	unbdqndv2lem1.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	unbdqndv2lem1.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	unbdqndv2lem1.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
	unbdqndv2lem1.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
	unbdqndv2lem1.1	⊢ ( 𝜑 → 𝐷 ≠ 0 )
	unbdqndv2lem1.2	⊢ ( 𝜑 → ( 2 · 𝐸 ) ≤ ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) )
Assertion	unbdqndv2lem1	⊢ ( 𝜑 → ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		unbdqndv2lem1.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		unbdqndv2lem1.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		unbdqndv2lem1.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4		unbdqndv2lem1.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
5		unbdqndv2lem1.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
6		unbdqndv2lem1.1	⊢ ( 𝜑 → 𝐷 ≠ 0 )
7		unbdqndv2lem1.2	⊢ ( 𝜑 → ( 2 · 𝐸 ) ≤ ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) )
8	1 2	subcld	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ )
9	8 4 6	absdivd	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) = ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / ( abs ‘ 𝐷 ) ) )
10	9	adantr	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) = ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / ( abs ‘ 𝐷 ) ) )
11	8	abscld	⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ )
12	11	adantr	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ )
13	1 3	subcld	⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) ∈ ℂ )
14	13	abscld	⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐶 ) ) ∈ ℝ )
15	2 3	subcld	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) ∈ ℂ )
16	15	abscld	⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − 𝐶 ) ) ∈ ℝ )
17	14 16	readdcld	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ∈ ℝ )
18	17	adantr	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ∈ ℝ )
19		2re	⊢ 2 ∈ ℝ
20	19	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
21	5	rpred	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
22	20 21	remulcld	⊢ ( 𝜑 → ( 2 · 𝐸 ) ∈ ℝ )
23	4	abscld	⊢ ( 𝜑 → ( abs ‘ 𝐷 ) ∈ ℝ )
24	22 23	remulcld	⊢ ( 𝜑 → ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) ∈ ℝ )
25	24	adantr	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) ∈ ℝ )
26	1 2 3	abs3difd	⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐵 ) ) ≤ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐶 − 𝐵 ) ) ) )
27	3 2	abssubd	⊢ ( 𝜑 → ( abs ‘ ( 𝐶 − 𝐵 ) ) = ( abs ‘ ( 𝐵 − 𝐶 ) ) )
28	27	oveq2d	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐶 − 𝐵 ) ) ) = ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )
29	26 28	breqtrd	⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐵 ) ) ≤ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )
30	29	adantr	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) ≤ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )
31	14	adantr	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( abs ‘ ( 𝐴 − 𝐶 ) ) ∈ ℝ )
32	16	adantr	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) ∈ ℝ )
33	21 23	remulcld	⊢ ( 𝜑 → ( 𝐸 · ( abs ‘ 𝐷 ) ) ∈ ℝ )
34	33	adantr	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐸 · ( abs ‘ 𝐷 ) ) ∈ ℝ )
35		pm2.45	⊢ ( ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) → ¬ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) )
36	35	adantl	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ¬ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) )
37	14 33	ltnled	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐸 · ( abs ‘ 𝐷 ) ) ↔ ¬ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ) )
38	37	adantr	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐸 · ( abs ‘ 𝐷 ) ) ↔ ¬ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ) )
39	36 38	mpbird	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐸 · ( abs ‘ 𝐷 ) ) )
40		pm2.46	⊢ ( ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) → ¬ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) )
41	40	adantl	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ¬ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) )
42	16 33	ltnled	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐵 − 𝐶 ) ) < ( 𝐸 · ( abs ‘ 𝐷 ) ) ↔ ¬ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )
43	42	adantr	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( ( abs ‘ ( 𝐵 − 𝐶 ) ) < ( 𝐸 · ( abs ‘ 𝐷 ) ) ↔ ¬ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )
44	41 43	mpbird	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ( 𝐸 · ( abs ‘ 𝐷 ) ) )
45	31 32 34 34 39 44	lt2addd	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) < ( ( 𝐸 · ( abs ‘ 𝐷 ) ) + ( 𝐸 · ( abs ‘ 𝐷 ) ) ) )
46	33	recnd	⊢ ( 𝜑 → ( 𝐸 · ( abs ‘ 𝐷 ) ) ∈ ℂ )
47	46	2timesd	⊢ ( 𝜑 → ( 2 · ( 𝐸 · ( abs ‘ 𝐷 ) ) ) = ( ( 𝐸 · ( abs ‘ 𝐷 ) ) + ( 𝐸 · ( abs ‘ 𝐷 ) ) ) )
48	47	eqcomd	⊢ ( 𝜑 → ( ( 𝐸 · ( abs ‘ 𝐷 ) ) + ( 𝐸 · ( abs ‘ 𝐷 ) ) ) = ( 2 · ( 𝐸 · ( abs ‘ 𝐷 ) ) ) )
49	20	recnd	⊢ ( 𝜑 → 2 ∈ ℂ )
50	21	recnd	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
51	23	recnd	⊢ ( 𝜑 → ( abs ‘ 𝐷 ) ∈ ℂ )
52	49 50 51	mulassd	⊢ ( 𝜑 → ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) = ( 2 · ( 𝐸 · ( abs ‘ 𝐷 ) ) ) )
53	52	eqcomd	⊢ ( 𝜑 → ( 2 · ( 𝐸 · ( abs ‘ 𝐷 ) ) ) = ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) )
54	48 53	eqtrd	⊢ ( 𝜑 → ( ( 𝐸 · ( abs ‘ 𝐷 ) ) + ( 𝐸 · ( abs ‘ 𝐷 ) ) ) = ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) )
55	54	adantr	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( ( 𝐸 · ( abs ‘ 𝐷 ) ) + ( 𝐸 · ( abs ‘ 𝐷 ) ) ) = ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) )
56	45 55	breqtrd	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) < ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) )
57	12 18 25 30 56	lelttrd	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) < ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) )
58		absgt0	⊢ ( 𝐷 ∈ ℂ → ( 𝐷 ≠ 0 ↔ 0 < ( abs ‘ 𝐷 ) ) )
59	4 58	syl	⊢ ( 𝜑 → ( 𝐷 ≠ 0 ↔ 0 < ( abs ‘ 𝐷 ) ) )
60	6 59	mpbid	⊢ ( 𝜑 → 0 < ( abs ‘ 𝐷 ) )
61	23 60	jca	⊢ ( 𝜑 → ( ( abs ‘ 𝐷 ) ∈ ℝ ∧ 0 < ( abs ‘ 𝐷 ) ) )
62	11 22 61	3jca	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ ∧ ( 2 · 𝐸 ) ∈ ℝ ∧ ( ( abs ‘ 𝐷 ) ∈ ℝ ∧ 0 < ( abs ‘ 𝐷 ) ) ) )
63		ltdivmul2	⊢ ( ( ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ ∧ ( 2 · 𝐸 ) ∈ ℝ ∧ ( ( abs ‘ 𝐷 ) ∈ ℝ ∧ 0 < ( abs ‘ 𝐷 ) ) ) → ( ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / ( abs ‘ 𝐷 ) ) < ( 2 · 𝐸 ) ↔ ( abs ‘ ( 𝐴 − 𝐵 ) ) < ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) ) )
64	62 63	syl	⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / ( abs ‘ 𝐷 ) ) < ( 2 · 𝐸 ) ↔ ( abs ‘ ( 𝐴 − 𝐵 ) ) < ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) ) )
65	64	adantr	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / ( abs ‘ 𝐷 ) ) < ( 2 · 𝐸 ) ↔ ( abs ‘ ( 𝐴 − 𝐵 ) ) < ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) ) )
66	57 65	mpbird	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / ( abs ‘ 𝐷 ) ) < ( 2 · 𝐸 ) )
67	10 66	eqbrtrd	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) < ( 2 · 𝐸 ) )
68	8 4 6	divcld	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) / 𝐷 ) ∈ ℂ )
69	68	abscld	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) ∈ ℝ )
70	22 69	lenltd	⊢ ( 𝜑 → ( ( 2 · 𝐸 ) ≤ ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) ↔ ¬ ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) < ( 2 · 𝐸 ) ) )
71	7 70	mpbid	⊢ ( 𝜑 → ¬ ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) < ( 2 · 𝐸 ) )
72	71	adantr	⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ¬ ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) < ( 2 · 𝐸 ) )
73	67 72	condan	⊢ ( 𝜑 → ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )