ftc2nc

Description: Choice-free proof of ftc2 . (Contributed by Brendan Leahy, 19-Jun-2018)

	Ref	Expression
Hypotheses	ftc2nc.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	ftc2nc.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	ftc2nc.le	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	ftc2nc.c	⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
	ftc2nc.i	⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ 𝐿¹ )
	ftc2nc.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
Assertion	ftc2nc	⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ftc2nc.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		ftc2nc.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		ftc2nc.le	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4		ftc2nc.c	⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
5		ftc2nc.i	⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ 𝐿¹ )
6		ftc2nc.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
7	1	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ^* )
8	2	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ^* )
9		ubicc2	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
10	7 8 3 9	syl3anc	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
11		fvex	⊢ ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) ∈ V
12	11	fvconst2	⊢ ( 𝐵 ∈ ( 𝐴 [,] 𝐵 ) → ( ( ( 𝐴 [,] 𝐵 ) × { ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) } ) ‘ 𝐵 ) = ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) )
13	10 12	syl	⊢ ( 𝜑 → ( ( ( 𝐴 [,] 𝐵 ) × { ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) } ) ‘ 𝐵 ) = ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) )
14		eqid	⊢ ( TopOpen ‘ ℂ_fld ) = ( TopOpen ‘ ℂ_fld )
15	14	subcn	⊢ − ∈ ( ( ( TopOpen ‘ ℂ_fld ) ×_t ( TopOpen ‘ ℂ_fld ) ) Cn ( TopOpen ‘ ℂ_fld ) )
16	15	a1i	⊢ ( 𝜑 → − ∈ ( ( ( TopOpen ‘ ℂ_fld ) ×_t ( TopOpen ‘ ℂ_fld ) ) Cn ( TopOpen ‘ ℂ_fld ) ) )
17		eqid	⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
18		ssidd	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
19		ioossre	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
20	19	a1i	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
21		cncff	⊢ ( ( ℝ D 𝐹 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
22	4 21	syl	⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
23		ioof	⊢ (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ
24		ffun	⊢ ( (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ → Fun (,) )
25	23 24	ax-mp	⊢ Fun (,)
26		fvelima	⊢ ( ( Fun (,) ∧ 𝑠 ∈ ( (,) “ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ) → ∃ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ( (,) ‘ 𝑥 ) = 𝑠 )
27	25 26	mpan	⊢ ( 𝑠 ∈ ( (,) “ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ∃ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ( (,) ‘ 𝑥 ) = 𝑠 )
28		1st2nd2	⊢ ( 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
29	28	fveq2d	⊢ ( 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) → ( (,) ‘ 𝑥 ) = ( (,) ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) )
30		df-ov	⊢ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) = ( (,) ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
31	29 30	eqtr4di	⊢ ( 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) → ( (,) ‘ 𝑥 ) = ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) )
32	31	eqeq1d	⊢ ( 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) → ( ( (,) ‘ 𝑥 ) = 𝑠 ↔ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) = 𝑠 ) )
33	32	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( ( (,) ‘ 𝑥 ) = 𝑠 ↔ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) = 𝑠 ) )
34	7 8	jca	⊢ ( 𝜑 → ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) )
35	34	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) )
36		xp1st	⊢ ( 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) → ( 1^st ‘ 𝑥 ) ∈ ( 𝐴 [,] 𝐵 ) )
37		elicc1	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ( 1^st ‘ 𝑥 ) ∈ ( 𝐴 [,] 𝐵 ) ↔ ( ( 1^st ‘ 𝑥 ) ∈ ℝ^* ∧ 𝐴 ≤ ( 1^st ‘ 𝑥 ) ∧ ( 1^st ‘ 𝑥 ) ≤ 𝐵 ) ) )
38	7 8 37	syl2anc	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑥 ) ∈ ( 𝐴 [,] 𝐵 ) ↔ ( ( 1^st ‘ 𝑥 ) ∈ ℝ^* ∧ 𝐴 ≤ ( 1^st ‘ 𝑥 ) ∧ ( 1^st ‘ 𝑥 ) ≤ 𝐵 ) ) )
39	38	biimpa	⊢ ( ( 𝜑 ∧ ( 1^st ‘ 𝑥 ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 1^st ‘ 𝑥 ) ∈ ℝ^* ∧ 𝐴 ≤ ( 1^st ‘ 𝑥 ) ∧ ( 1^st ‘ 𝑥 ) ≤ 𝐵 ) )
40	39	simp2d	⊢ ( ( 𝜑 ∧ ( 1^st ‘ 𝑥 ) ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ ( 1^st ‘ 𝑥 ) )
41	36 40	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → 𝐴 ≤ ( 1^st ‘ 𝑥 ) )
42		xp2nd	⊢ ( 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) → ( 2^nd ‘ 𝑥 ) ∈ ( 𝐴 [,] 𝐵 ) )
43		iccleub	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 2^nd ‘ 𝑥 ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 2^nd ‘ 𝑥 ) ≤ 𝐵 )
44	43	3expa	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ ( 2^nd ‘ 𝑥 ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 2^nd ‘ 𝑥 ) ≤ 𝐵 )
45	34 42 44	syl2an	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( 2^nd ‘ 𝑥 ) ≤ 𝐵 )
46		ioossioo	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ ( 𝐴 ≤ ( 1^st ‘ 𝑥 ) ∧ ( 2^nd ‘ 𝑥 ) ≤ 𝐵 ) ) → ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ⊆ ( 𝐴 (,) 𝐵 ) )
47	35 41 45 46	syl12anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ⊆ ( 𝐴 (,) 𝐵 ) )
48	47	sselda	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ) → 𝑡 ∈ ( 𝐴 (,) 𝐵 ) )
49	22	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ∈ ℂ )
50	49	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ∈ ℂ )
51	48 50	syldan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ∈ ℂ )
52		ioombl	⊢ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ∈ dom vol
53	52	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ∈ dom vol )
54		fvexd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ∈ V )
55	22	feqmptd	⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) )
56	55 5	eqeltrrd	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ∈ 𝐿¹ )
57	56	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ∈ 𝐿¹ )
58	47 53 54 57	iblss	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ∈ 𝐿¹ )
59		ax-resscn	⊢ ℝ ⊆ ℂ
60		ssid	⊢ ℂ ⊆ ℂ
61		cncfss	⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℂ –cn→ ℝ ) ⊆ ( ℂ –cn→ ℂ ) )
62	59 60 61	mp2an	⊢ ( ℂ –cn→ ℝ ) ⊆ ( ℂ –cn→ ℂ )
63		abscncf	⊢ abs ∈ ( ℂ –cn→ ℝ )
64	62 63	sselii	⊢ abs ∈ ( ℂ –cn→ ℂ )
65	64	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → abs ∈ ( ℂ –cn→ ℂ ) )
66	55	reseq1d	⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ) = ( ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ↾ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ) )
67	66	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( ( ℝ D 𝐹 ) ↾ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ) = ( ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ↾ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ) )
68	47	resmptd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ↾ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ) = ( 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) )
69	67 68	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( ( ℝ D 𝐹 ) ↾ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ) = ( 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) )
70	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( ℝ D 𝐹 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
71		rescncf	⊢ ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ⊆ ( 𝐴 (,) 𝐵 ) → ( ( ℝ D 𝐹 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) → ( ( ℝ D 𝐹 ) ↾ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ) ∈ ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) –cn→ ℂ ) ) )
72	47 70 71	sylc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( ( ℝ D 𝐹 ) ↾ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ) ∈ ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) –cn→ ℂ ) )
73	69 72	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ∈ ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) –cn→ ℂ ) )
74	65 73	cncfmpt1f	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ) ∈ ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) –cn→ ℂ ) )
75		cnmbf	⊢ ( ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ∈ dom vol ∧ ( 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ) ∈ ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) –cn→ ℂ ) ) → ( 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ) ∈ MblFn )
76	52 74 75	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ) ∈ MblFn )
77	51 58	itgcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ∫ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ∈ ℂ )
78	77	cjcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( ∗ ‘ ∫ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ∈ ℂ )
79		ioossre	⊢ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ⊆ ℝ
80	79 59	sstri	⊢ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ⊆ ℂ
81		cncfmptc	⊢ ( ( ( ∗ ‘ ∫ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ∈ ℂ ∧ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑠 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↦ ( ∗ ‘ ∫ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ) ∈ ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) –cn→ ℂ ) )
82	80 60 81	mp3an23	⊢ ( ( ∗ ‘ ∫ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ∈ ℂ → ( 𝑠 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↦ ( ∗ ‘ ∫ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ) ∈ ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) –cn→ ℂ ) )
83	78 82	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑠 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↦ ( ∗ ‘ ∫ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ) ∈ ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) –cn→ ℂ ) )
84		nfcv	⊢ Ⅎ 𝑠 ( ( ℝ D 𝐹 ) ‘ 𝑡 )
85		nfcsb1v	⊢ Ⅎ 𝑡 ⦋ 𝑠 / 𝑡 ⦌ ( ( ℝ D 𝐹 ) ‘ 𝑡 )
86		csbeq1a	⊢ ( 𝑡 = 𝑠 → ( ( ℝ D 𝐹 ) ‘ 𝑡 ) = ⦋ 𝑠 / 𝑡 ⦌ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) )
87	84 85 86	cbvmpt	⊢ ( 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) = ( 𝑠 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↦ ⦋ 𝑠 / 𝑡 ⦌ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) )
88	87 73	eqeltrrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑠 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↦ ⦋ 𝑠 / 𝑡 ⦌ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ∈ ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) –cn→ ℂ ) )
89	83 88	mulcncf	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑠 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↦ ( ( ∗ ‘ ∫ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) · ⦋ 𝑠 / 𝑡 ⦌ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ) ∈ ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) –cn→ ℂ ) )
90		cnmbf	⊢ ( ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ∈ dom vol ∧ ( 𝑠 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↦ ( ( ∗ ‘ ∫ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) · ⦋ 𝑠 / 𝑡 ⦌ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ) ∈ ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) –cn→ ℂ ) ) → ( 𝑠 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↦ ( ( ∗ ‘ ∫ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) · ⦋ 𝑠 / 𝑡 ⦌ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ) ∈ MblFn )
91	52 89 90	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑠 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↦ ( ( ∗ ‘ ∫ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) · ⦋ 𝑠 / 𝑡 ⦌ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ) ∈ MblFn )
92	51 58 76 91	itgabsnc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ∫ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ≤ ∫ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) d 𝑡 )
93	51	abscld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ∈ ℝ )
94		fvexd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ∈ V )
95	94 58 76	iblabsnc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ) ∈ 𝐿¹ )
96	51	absge0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) )
97	93 95 96	itgposval	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ∫ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) d 𝑡 = ( ∫₂ ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) , ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) , 0 ) ) ) )
98	92 97	breqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ∫ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ≤ ( ∫₂ ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) , ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) , 0 ) ) ) )
99		itgeq1	⊢ ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) = 𝑠 → ∫ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ∫ 𝑠 ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
100	99	fveq2d	⊢ ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) = 𝑠 → ( abs ‘ ∫ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) = ( abs ‘ ∫ 𝑠 ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) )
101		eleq2	⊢ ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) = 𝑠 → ( 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ↔ 𝑡 ∈ 𝑠 ) )
102	101	ifbid	⊢ ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) = 𝑠 → if ( 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) , ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) , 0 ) = if ( 𝑡 ∈ 𝑠 , ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) , 0 ) )
103	102	mpteq2dv	⊢ ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) = 𝑠 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) , ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝑠 , ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) , 0 ) ) )
104	103	fveq2d	⊢ ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) = 𝑠 → ( ∫₂ ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) , ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) , 0 ) ) ) = ( ∫₂ ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝑠 , ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) , 0 ) ) ) )
105	100 104	breq12d	⊢ ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) = 𝑠 → ( ( abs ‘ ∫ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ≤ ( ∫₂ ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) , ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) , 0 ) ) ) ↔ ( abs ‘ ∫ 𝑠 ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ≤ ( ∫₂ ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝑠 , ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) , 0 ) ) ) ) )
106	98 105	syl5ibcom	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) = 𝑠 → ( abs ‘ ∫ 𝑠 ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ≤ ( ∫₂ ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝑠 , ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) , 0 ) ) ) ) )
107	33 106	sylbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( ( (,) ‘ 𝑥 ) = 𝑠 → ( abs ‘ ∫ 𝑠 ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ≤ ( ∫₂ ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝑠 , ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) , 0 ) ) ) ) )
108	107	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ( (,) ‘ 𝑥 ) = 𝑠 → ( abs ‘ ∫ 𝑠 ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ≤ ( ∫₂ ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝑠 , ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) , 0 ) ) ) ) )
109	27 108	syl5	⊢ ( 𝜑 → ( 𝑠 ∈ ( (,) “ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ∫ 𝑠 ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ≤ ( ∫₂ ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝑠 , ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) , 0 ) ) ) ) )
110	109	ralrimiv	⊢ ( 𝜑 → ∀ 𝑠 ∈ ( (,) “ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ( abs ‘ ∫ 𝑠 ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ≤ ( ∫₂ ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝑠 , ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) , 0 ) ) ) )
111	17 1 2 3 18 20 5 22 110	ftc1anc	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
112		cncff	⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
113	6 112	syl	⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
114	113	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
115	114 6	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
116	14 16 111 115	cncfmpt2f	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
117	59	a1i	⊢ ( 𝜑 → ℝ ⊆ ℂ )
118		iccssre	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
119	1 2 118	syl2anc	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
120		fvexd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑡 ∈ ( 𝐴 (,) 𝑥 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ∈ V )
121	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ )
122	121	rexrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ^* )
123		elicc2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
124	1 2 123	syl2anc	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
125	124	biimpa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
126	125	simp3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ≤ 𝐵 )
127		iooss2	⊢ ( ( 𝐵 ∈ ℝ^* ∧ 𝑥 ≤ 𝐵 ) → ( 𝐴 (,) 𝑥 ) ⊆ ( 𝐴 (,) 𝐵 ) )
128	122 126 127	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 (,) 𝑥 ) ⊆ ( 𝐴 (,) 𝐵 ) )
129		ioombl	⊢ ( 𝐴 (,) 𝑥 ) ∈ dom vol
130	129	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 (,) 𝑥 ) ∈ dom vol )
131		fvexd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ∈ V )
132	56	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ∈ 𝐿¹ )
133	128 130 131 132	iblss	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 ∈ ( 𝐴 (,) 𝑥 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ∈ 𝐿¹ )
134	120 133	itgcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ∈ ℂ )
135	113	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
136	134 135	subcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ∈ ℂ )
137	14	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂ_fld ) ↾_t ℝ )
138		iccntr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
139	1 2 138	syl2anc	⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
140	117 119 136 137 14 139	dvmptntr	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ) )
141		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
142	141	a1i	⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
143		ioossicc	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
144	143	sseli	⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
145	144 134	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ∈ ℂ )
146	22	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
147	17 1 2 3 4 5	ftc1cnnc	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ) = ( ℝ D 𝐹 ) )
148	117 119 134 137 14 139	dvmptntr	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ) = ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ) )
149	22	feqmptd	⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
150	147 148 149	3eqtr3d	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
151	144 135	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
152	114	oveq2d	⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( ℝ D ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
153	117 119 135 137 14 139	dvmptntr	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
154	152 149 153	3eqtr3rd	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
155	142 145 146 150 151 146 154	dvmptsub	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) )
156	146	subidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) = 0 )
157	156	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 ) )
158	140 155 157	3eqtrd	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 ) )
159		fconstmpt	⊢ ( ( 𝐴 (,) 𝐵 ) × { 0 } ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 )
160	158 159	eqtr4di	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ( 𝐴 (,) 𝐵 ) × { 0 } ) )
161	1 2 116 160	dveq0	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) = ( ( 𝐴 [,] 𝐵 ) × { ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) } ) )
162	161	fveq1d	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐵 ) = ( ( ( 𝐴 [,] 𝐵 ) × { ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) } ) ‘ 𝐵 ) )
163		oveq2	⊢ ( 𝑥 = 𝐵 → ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝐵 ) )
164		itgeq1	⊢ ( ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝐵 ) → ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
165	163 164	syl	⊢ ( 𝑥 = 𝐵 → ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
166		fveq2	⊢ ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) )
167	165 166	oveq12d	⊢ ( 𝑥 = 𝐵 → ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) = ( ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝐵 ) ) )
168		eqid	⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) )
169		ovex	⊢ ( ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝐵 ) ) ∈ V
170	167 168 169	fvmpt	⊢ ( 𝐵 ∈ ( 𝐴 [,] 𝐵 ) → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐵 ) = ( ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝐵 ) ) )
171	10 170	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐵 ) = ( ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝐵 ) ) )
172	162 171	eqtr3d	⊢ ( 𝜑 → ( ( ( 𝐴 [,] 𝐵 ) × { ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) } ) ‘ 𝐵 ) = ( ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝐵 ) ) )
173		lbicc2	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
174	7 8 3 173	syl3anc	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
175		oveq2	⊢ ( 𝑥 = 𝐴 → ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝐴 ) )
176		iooid	⊢ ( 𝐴 (,) 𝐴 ) = ∅
177	175 176	eqtrdi	⊢ ( 𝑥 = 𝐴 → ( 𝐴 (,) 𝑥 ) = ∅ )
178		itgeq1	⊢ ( ( 𝐴 (,) 𝑥 ) = ∅ → ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ∫ ∅ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
179	177 178	syl	⊢ ( 𝑥 = 𝐴 → ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ∫ ∅ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
180		itg0	⊢ ∫ ∅ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = 0
181	179 180	eqtrdi	⊢ ( 𝑥 = 𝐴 → ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = 0 )
182		fveq2	⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
183	181 182	oveq12d	⊢ ( 𝑥 = 𝐴 → ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) = ( 0 − ( 𝐹 ‘ 𝐴 ) ) )
184		df-neg	⊢ - ( 𝐹 ‘ 𝐴 ) = ( 0 − ( 𝐹 ‘ 𝐴 ) )
185	183 184	eqtr4di	⊢ ( 𝑥 = 𝐴 → ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) = - ( 𝐹 ‘ 𝐴 ) )
186		negex	⊢ - ( 𝐹 ‘ 𝐴 ) ∈ V
187	185 168 186	fvmpt	⊢ ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) = - ( 𝐹 ‘ 𝐴 ) )
188	174 187	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) = - ( 𝐹 ‘ 𝐴 ) )
189	13 172 188	3eqtr3d	⊢ ( 𝜑 → ( ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝐵 ) ) = - ( 𝐹 ‘ 𝐴 ) )
190	189	oveq2d	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) + ( ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝐵 ) ) ) = ( ( 𝐹 ‘ 𝐵 ) + - ( 𝐹 ‘ 𝐴 ) ) )
191	113 10	ffvelrnd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
192		fvexd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ∈ V )
193	192 56	itgcl	⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ∈ ℂ )
194	191 193	pncan3d	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) + ( ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝐵 ) ) ) = ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
195	113 174	ffvelrnd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℂ )
196	191 195	negsubd	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) + - ( 𝐹 ‘ 𝐴 ) ) = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )
197	190 194 196	3eqtr3d	⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )

Metamath Proof Explorer

Theorem ftc2nc

Proof