Theorem dvle2

Description: Collapsed dvle . (Contributed by metakunt, 19-Aug-2024)

	Ref	Expression
Hypotheses	dvle2.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	dvle2.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	dvle2.3	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐸 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
	dvle2.4	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐺 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
	dvle2.5	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐸 ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐹 ) )
	dvle2.6	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐺 ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐻 ) )
	dvle2.7	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐹 ≤ 𝐻 )
	dvle2.8	⊢ ( 𝑥 = 𝐴 → 𝐸 = 𝑃 )
	dvle2.9	⊢ ( 𝑥 = 𝐴 → 𝐺 = 𝑄 )
	dvle2.10	⊢ ( 𝑥 = 𝐵 → 𝐸 = 𝑅 )
	dvle2.11	⊢ ( 𝑥 = 𝐵 → 𝐺 = 𝑆 )
	dvle2.12	⊢ ( 𝜑 → 𝑃 ≤ 𝑄 )
	dvle2.13	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
Assertion	dvle2	⊢ ( 𝜑 → 𝑅 ≤ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		dvle2.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		dvle2.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		dvle2.3	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐸 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
4		dvle2.4	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐺 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
5		dvle2.5	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐸 ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐹 ) )
6		dvle2.6	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐺 ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐻 ) )
7		dvle2.7	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐹 ≤ 𝐻 )
8		dvle2.8	⊢ ( 𝑥 = 𝐴 → 𝐸 = 𝑃 )
9		dvle2.9	⊢ ( 𝑥 = 𝐴 → 𝐺 = 𝑄 )
10		dvle2.10	⊢ ( 𝑥 = 𝐵 → 𝐸 = 𝑅 )
11		dvle2.11	⊢ ( 𝑥 = 𝐵 → 𝐺 = 𝑆 )
12		dvle2.12	⊢ ( 𝜑 → 𝑃 ≤ 𝑄 )
13		dvle2.13	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
14	10	eleq1d	⊢ ( 𝑥 = 𝐵 → ( 𝐸 ∈ ℝ ↔ 𝑅 ∈ ℝ ) )
15		cncff	⊢ ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐸 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐸 ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
16	3 15	syl	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐸 ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
17		eqid	⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐸 ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐸 )
18	17	fmpt	⊢ ( ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) 𝐸 ∈ ℝ ↔ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐸 ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
19	16 18	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) 𝐸 ∈ ℝ )
20	2	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
21	2	leidd	⊢ ( 𝜑 → 𝐵 ≤ 𝐵 )
22	20 13 21	3jca	⊢ ( 𝜑 → ( 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵 ) )
23	1	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
24		elicc1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵 ) ) )
25	23 20 24	syl2anc	⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵 ) ) )
26	22 25	mpbird	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
27	14 19 26	rspcdva	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
28	8	eleq1d	⊢ ( 𝑥 = 𝐴 → ( 𝐸 ∈ ℝ ↔ 𝑃 ∈ ℝ ) )
29	1	leidd	⊢ ( 𝜑 → 𝐴 ≤ 𝐴 )
30	23 29 13	3jca	⊢ ( 𝜑 → ( 𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) )
31		elicc1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) ) )
32	23 20 31	syl2anc	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) ) )
33	30 32	mpbird	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
34	28 19 33	rspcdva	⊢ ( 𝜑 → 𝑃 ∈ ℝ )
35	27 34	resubcld	⊢ ( 𝜑 → ( 𝑅 − 𝑃 ) ∈ ℝ )
36	11	eleq1d	⊢ ( 𝑥 = 𝐵 → ( 𝐺 ∈ ℝ ↔ 𝑆 ∈ ℝ ) )
37		cncff	⊢ ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐺 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐺 ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
38	4 37	syl	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐺 ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
39		eqid	⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐺 ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐺 )
40	39	fmpt	⊢ ( ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) 𝐺 ∈ ℝ ↔ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐺 ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
41	38 40	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) 𝐺 ∈ ℝ )
42	36 41 26	rspcdva	⊢ ( 𝜑 → 𝑆 ∈ ℝ )
43	9	eleq1d	⊢ ( 𝑥 = 𝐴 → ( 𝐺 ∈ ℝ ↔ 𝑄 ∈ ℝ ) )
44	43 41 33	rspcdva	⊢ ( 𝜑 → 𝑄 ∈ ℝ )
45	42 44	resubcld	⊢ ( 𝜑 → ( 𝑆 − 𝑄 ) ∈ ℝ )
46	1 2 3 5 4 6 7 33 26 13 8 9 10 11	dvle	⊢ ( 𝜑 → ( 𝑅 − 𝑃 ) ≤ ( 𝑆 − 𝑄 ) )
47	35 34 45 44 46 12	le2addd	⊢ ( 𝜑 → ( ( 𝑅 − 𝑃 ) + 𝑃 ) ≤ ( ( 𝑆 − 𝑄 ) + 𝑄 ) )
48	27	recnd	⊢ ( 𝜑 → 𝑅 ∈ ℂ )
49	34	recnd	⊢ ( 𝜑 → 𝑃 ∈ ℂ )
50	48 49	npcand	⊢ ( 𝜑 → ( ( 𝑅 − 𝑃 ) + 𝑃 ) = 𝑅 )
51	42	recnd	⊢ ( 𝜑 → 𝑆 ∈ ℂ )
52	44	recnd	⊢ ( 𝜑 → 𝑄 ∈ ℂ )
53	51 52	npcand	⊢ ( 𝜑 → ( ( 𝑆 − 𝑄 ) + 𝑄 ) = 𝑆 )
54	50 53	breq12d	⊢ ( 𝜑 → ( ( ( 𝑅 − 𝑃 ) + 𝑃 ) ≤ ( ( 𝑆 − 𝑄 ) + 𝑄 ) ↔ 𝑅 ≤ 𝑆 ) )
55	47 54	mpbid	⊢ ( 𝜑 → 𝑅 ≤ 𝑆 )