Theorem 3factsumint

Description: Helpful equation for lcm inequality proof. (Contributed by metakunt, 26-Apr-2024)

	Ref	Expression
Hypotheses	3factsumint.1	⊢ 𝐴 = ( 𝐿 [,] 𝑈 )
	3factsumint.2	⊢ ( 𝜑 → 𝐵 ∈ Fin )
	3factsumint.3	⊢ ( 𝜑 → 𝐿 ∈ ℝ )
	3factsumint.4	⊢ ( 𝜑 → 𝑈 ∈ ℝ )
	3factsumint.5	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( 𝐴 –cn→ ℂ ) )
	3factsumint.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐺 ∈ ℂ )
	3factsumint.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐻 ) ∈ ( 𝐴 –cn→ ℂ ) )
Assertion	3factsumint	⊢ ( 𝜑 → ∫ 𝐴 ( 𝐹 · Σ 𝑘 ∈ 𝐵 ( 𝐺 · 𝐻 ) ) d 𝑥 = Σ 𝑘 ∈ 𝐵 ( 𝐺 · ∫ 𝐴 ( 𝐹 · 𝐻 ) d 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		3factsumint.1	⊢ 𝐴 = ( 𝐿 [,] 𝑈 )
2		3factsumint.2	⊢ ( 𝜑 → 𝐵 ∈ Fin )
3		3factsumint.3	⊢ ( 𝜑 → 𝐿 ∈ ℝ )
4		3factsumint.4	⊢ ( 𝜑 → 𝑈 ∈ ℝ )
5		3factsumint.5	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( 𝐴 –cn→ ℂ ) )
6		3factsumint.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐺 ∈ ℂ )
7		3factsumint.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐻 ) ∈ ( 𝐴 –cn→ ℂ ) )
8		cncff	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( 𝐴 –cn→ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) : 𝐴 ⟶ ℂ )
9	5 8	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) : 𝐴 ⟶ ℂ )
10		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐹 )
11	10	fmpt	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐹 ∈ ℂ ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) : 𝐴 ⟶ ℂ )
12	9 11	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐹 ∈ ℂ )
13	12	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 ∈ ℂ )
14		cncff	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐻 ) ∈ ( 𝐴 –cn→ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐻 ) : 𝐴 ⟶ ℂ )
15	7 14	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐻 ) : 𝐴 ⟶ ℂ )
16		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐻 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐻 )
17	16	fmpt	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐻 ∈ ℂ ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐻 ) : 𝐴 ⟶ ℂ )
18	15 17	sylibr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝐻 ∈ ℂ )
19	18	r19.21bi	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐻 ∈ ℂ )
20		anass	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ ( 𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ) )
21		ancom	⊢ ( ( 𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) )
22	21	anbi2i	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ) ↔ ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) )
23	20 22	bitri	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) )
24	23	imbi1i	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐻 ∈ ℂ ) ↔ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐻 ∈ ℂ ) )
25	19 24	mpbi	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐻 ∈ ℂ )
26	2 13 6 25	3factsumint4	⊢ ( 𝜑 → ∫ 𝐴 Σ 𝑘 ∈ 𝐵 ( 𝐹 · ( 𝐺 · 𝐻 ) ) d 𝑥 = ∫ 𝐴 ( 𝐹 · Σ 𝑘 ∈ 𝐵 ( 𝐺 · 𝐻 ) ) d 𝑥 )
27	1 2 3 4 13 5 6 25 7	3factsumint1	⊢ ( 𝜑 → ∫ 𝐴 Σ 𝑘 ∈ 𝐵 ( 𝐹 · ( 𝐺 · 𝐻 ) ) d 𝑥 = Σ 𝑘 ∈ 𝐵 ∫ 𝐴 ( 𝐹 · ( 𝐺 · 𝐻 ) ) d 𝑥 )
28	26 27	eqtr3d	⊢ ( 𝜑 → ∫ 𝐴 ( 𝐹 · Σ 𝑘 ∈ 𝐵 ( 𝐺 · 𝐻 ) ) d 𝑥 = Σ 𝑘 ∈ 𝐵 ∫ 𝐴 ( 𝐹 · ( 𝐺 · 𝐻 ) ) d 𝑥 )
29	13 6 25	3factsumint2	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐵 ∫ 𝐴 ( 𝐹 · ( 𝐺 · 𝐻 ) ) d 𝑥 = Σ 𝑘 ∈ 𝐵 ∫ 𝐴 ( 𝐺 · ( 𝐹 · 𝐻 ) ) d 𝑥 )
30	1 3 4 13 5 6 25 7	3factsumint3	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐵 ∫ 𝐴 ( 𝐺 · ( 𝐹 · 𝐻 ) ) d 𝑥 = Σ 𝑘 ∈ 𝐵 ( 𝐺 · ∫ 𝐴 ( 𝐹 · 𝐻 ) d 𝑥 ) )
31	28 29 30	3eqtrd	⊢ ( 𝜑 → ∫ 𝐴 ( 𝐹 · Σ 𝑘 ∈ 𝐵 ( 𝐺 · 𝐻 ) ) d 𝑥 = Σ 𝑘 ∈ 𝐵 ( 𝐺 · ∫ 𝐴 ( 𝐹 · 𝐻 ) d 𝑥 ) )