Theorem iblcnlem1 25152

Description: Lemma for iblcnlem 25153. (Contributed by Mario Carneiro, 6-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)

Hypotheses

Ref	Expression
itgcnlem.r	⊢ 𝑅 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0)))
itgcnlem.s	⊢ 𝑆 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0)))
itgcnlem.t	⊢ 𝑇 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0)))
itgcnlem.u	⊢ 𝑈 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0)))
itgcnlem1.v	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
iblcnlem1	⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ))))

Distinct variable groups:   𝑥,𝐴   𝜑,𝑥

Allowed substitution hints:   𝐵(𝑥)   𝑅(𝑥)   𝑆(𝑥)   𝑇(𝑥)   𝑈(𝑥)

Proof of Theorem iblcnlem1

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqidd 2737	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))
2		eqidd 2737	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐵 / (i↑𝑘))) = (ℜ‘(𝐵 / (i↑𝑘))))
3		itgcnlem1.v	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
4	1, 2, 3	isibl2 25131	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ)))
5		c0ex 11149	. . . . . . . 8 ⊢ 0 ∈ V
6		1ex 11151	. . . . . . . 8 ⊢ 1 ∈ V
7		ax-icn 11110	. . . . . . . . . . 11 ⊢ i ∈ ℂ
8		exp0 13971	. . . . . . . . . . 11 ⊢ (i ∈ ℂ → (i↑0) = 1)
9	7, 8	ax-mp 5	. . . . . . . . . 10 ⊢ (i↑0) = 1
10	9	itgvallem 25149	. . . . . . . . 9 ⊢ (𝑘 = 0 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))))
11	10	eleq1d 2822	. . . . . . . 8 ⊢ (𝑘 = 0 → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) ∈ ℝ))
12		exp1 13973	. . . . . . . . . . 11 ⊢ (i ∈ ℂ → (i↑1) = i)
13	7, 12	ax-mp 5	. . . . . . . . . 10 ⊢ (i↑1) = i
14	13	itgvallem 25149	. . . . . . . . 9 ⊢ (𝑘 = 1 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))))
15	14	eleq1d 2822	. . . . . . . 8 ⊢ (𝑘 = 1 → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) ∈ ℝ))
16	5, 6, 11, 15	ralpr 4661	. . . . . . 7 ⊢ (∀𝑘 ∈ {0, 1} (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) ∈ ℝ))
17	3	div1d 11923	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 / 1) = 𝐵)
18	17	fveq2d 6846	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐵 / 1)) = (ℜ‘𝐵))
19	18	ibllem 25129	. . . . . . . . . . . 12 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0))
20	19	mpteq2dv 5207	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0)))
21	20	fveq2d 6846	. . . . . . . . . 10 ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0))))
22		itgcnlem.r	. . . . . . . . . 10 ⊢ 𝑅 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0)))
23	21, 22	eqtr4di 2794	. . . . . . . . 9 ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) = 𝑅)
24	23	eleq1d 2822	. . . . . . . 8 ⊢ (𝜑 → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) ∈ ℝ ↔ 𝑅 ∈ ℝ))
25		itgcnlem.t	. . . . . . . . . 10 ⊢ 𝑇 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0)))
26		imval 14992	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ℂ → (ℑ‘𝐵) = (ℜ‘(𝐵 / i)))
27	3, 26	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) = (ℜ‘(𝐵 / i)))
28	27	ibllem 25129	. . . . . . . . . . . 12 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))
29	28	mpteq2dv 5207	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0)))
30	29	fveq2d 6846	. . . . . . . . . 10 ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))))
31	25, 30	eqtr2id 2789	. . . . . . . . 9 ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) = 𝑇)
32	31	eleq1d 2822	. . . . . . . 8 ⊢ (𝜑 → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) ∈ ℝ ↔ 𝑇 ∈ ℝ))
33	24, 32	anbi12d 631	. . . . . . 7 ⊢ (𝜑 → (((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) ∈ ℝ) ↔ (𝑅 ∈ ℝ ∧ 𝑇 ∈ ℝ)))
34	16, 33	bitrid 282	. . . . . 6 ⊢ (𝜑 → (∀𝑘 ∈ {0, 1} (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ (𝑅 ∈ ℝ ∧ 𝑇 ∈ ℝ)))
35		2ex 12230	. . . . . . . 8 ⊢ 2 ∈ V
36		3ex 12235	. . . . . . . 8 ⊢ 3 ∈ V
37		i2 14106	. . . . . . . . . 10 ⊢ (i↑2) = -1
38	37	itgvallem 25149	. . . . . . . . 9 ⊢ (𝑘 = 2 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))))
39	38	eleq1d 2822	. . . . . . . 8 ⊢ (𝑘 = 2 → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))) ∈ ℝ))
40		i3 14107	. . . . . . . . . 10 ⊢ (i↑3) = -i
41	40	itgvallem 25149	. . . . . . . . 9 ⊢ (𝑘 = 3 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))))
42	41	eleq1d 2822	. . . . . . . 8 ⊢ (𝑘 = 3 → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))) ∈ ℝ))
43	35, 36, 39, 42	ralpr 4661	. . . . . . 7 ⊢ (∀𝑘 ∈ {2, 3} (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))) ∈ ℝ))
44		itgcnlem.s	. . . . . . . . . 10 ⊢ 𝑆 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0)))
45	3	renegd 15094	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘-𝐵) = -(ℜ‘𝐵))
46		ax-1cn 11109	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℂ
47	46	negnegi 11471	. . . . . . . . . . . . . . . . . 18 ⊢ --1 = 1
48	47	oveq2i 7368	. . . . . . . . . . . . . . . . 17 ⊢ (-𝐵 / --1) = (-𝐵 / 1)
49	3	negcld 11499	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℂ)
50	49	div1d 11923	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / 1) = -𝐵)
51	48, 50	eqtrid 2788	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / --1) = -𝐵)
52	46	negcli 11469	. . . . . . . . . . . . . . . . . 18 ⊢ -1 ∈ ℂ
53		neg1ne0 12269	. . . . . . . . . . . . . . . . . 18 ⊢ -1 ≠ 0
54		div2neg 11878	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ ℂ ∧ -1 ∈ ℂ ∧ -1 ≠ 0) → (-𝐵 / --1) = (𝐵 / -1))
55	52, 53, 54	mp3an23 1453	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ ℂ → (-𝐵 / --1) = (𝐵 / -1))
56	3, 55	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / --1) = (𝐵 / -1))
57	51, 56	eqtr3d 2778	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 = (𝐵 / -1))
58	57	fveq2d 6846	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘-𝐵) = (ℜ‘(𝐵 / -1)))
59	45, 58	eqtr3d 2778	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℜ‘𝐵) = (ℜ‘(𝐵 / -1)))
60	59	ibllem 25129	. . . . . . . . . . . 12 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))
61	60	mpteq2dv 5207	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0)))
62	61	fveq2d 6846	. . . . . . . . . 10 ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))))
63	44, 62	eqtr2id 2789	. . . . . . . . 9 ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))) = 𝑆)
64	63	eleq1d 2822	. . . . . . . 8 ⊢ (𝜑 → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))) ∈ ℝ ↔ 𝑆 ∈ ℝ))
65		itgcnlem.u	. . . . . . . . . 10 ⊢ 𝑈 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0)))
66		imval 14992	. . . . . . . . . . . . . . 15 ⊢ (-𝐵 ∈ ℂ → (ℑ‘-𝐵) = (ℜ‘(-𝐵 / i)))
67	49, 66	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘-𝐵) = (ℜ‘(-𝐵 / i)))
68	3	imnegd 15095	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘-𝐵) = -(ℑ‘𝐵))
69	7	negnegi 11471	. . . . . . . . . . . . . . . . . 18 ⊢ --i = i
70	69	eqcomi 2745	. . . . . . . . . . . . . . . . 17 ⊢ i = --i
71	70	oveq2i 7368	. . . . . . . . . . . . . . . 16 ⊢ (-𝐵 / i) = (-𝐵 / --i)
72	7	negcli 11469	. . . . . . . . . . . . . . . . . 18 ⊢ -i ∈ ℂ
73		ine0 11590	. . . . . . . . . . . . . . . . . . 19 ⊢ i ≠ 0
74	7, 73	negne0i 11476	. . . . . . . . . . . . . . . . . 18 ⊢ -i ≠ 0
75		div2neg 11878	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ ℂ ∧ -i ∈ ℂ ∧ -i ≠ 0) → (-𝐵 / --i) = (𝐵 / -i))
76	72, 74, 75	mp3an23 1453	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ ℂ → (-𝐵 / --i) = (𝐵 / -i))
77	3, 76	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / --i) = (𝐵 / -i))
78	71, 77	eqtrid 2788	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / i) = (𝐵 / -i))
79	78	fveq2d 6846	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(-𝐵 / i)) = (ℜ‘(𝐵 / -i)))
80	67, 68, 79	3eqtr3d 2784	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℑ‘𝐵) = (ℜ‘(𝐵 / -i)))
81	80	ibllem 25129	. . . . . . . . . . . 12 ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))
82	81	mpteq2dv 5207	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0)))
83	82	fveq2d 6846	. . . . . . . . . 10 ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))))
84	65, 83	eqtr2id 2789	. . . . . . . . 9 ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))) = 𝑈)
85	84	eleq1d 2822	. . . . . . . 8 ⊢ (𝜑 → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))) ∈ ℝ ↔ 𝑈 ∈ ℝ))
86	64, 85	anbi12d 631	. . . . . . 7 ⊢ (𝜑 → (((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))) ∈ ℝ) ↔ (𝑆 ∈ ℝ ∧ 𝑈 ∈ ℝ)))
87	43, 86	bitrid 282	. . . . . 6 ⊢ (𝜑 → (∀𝑘 ∈ {2, 3} (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ (𝑆 ∈ ℝ ∧ 𝑈 ∈ ℝ)))
88	34, 87	anbi12d 631	. . . . 5 ⊢ (𝜑 → ((∀𝑘 ∈ {0, 1} (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ∧ ∀𝑘 ∈ {2, 3} (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ) ↔ ((𝑅 ∈ ℝ ∧ 𝑇 ∈ ℝ) ∧ (𝑆 ∈ ℝ ∧ 𝑈 ∈ ℝ))))
89		fz0to3un2pr 13543	. . . . . . 7 ⊢ (0...3) = ({0, 1} ∪ {2, 3})
90	89	raleqi 3311	. . . . . 6 ⊢ (∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ ∀𝑘 ∈ ({0, 1} ∪ {2, 3})(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ)
91		ralunb 4151	. . . . . 6 ⊢ (∀𝑘 ∈ ({0, 1} ∪ {2, 3})(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ (∀𝑘 ∈ {0, 1} (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ∧ ∀𝑘 ∈ {2, 3} (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ))
92	90, 91	bitri 274	. . . . 5 ⊢ (∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ (∀𝑘 ∈ {0, 1} (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ∧ ∀𝑘 ∈ {2, 3} (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ))
93		an4 654	. . . . 5 ⊢ (((𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ)) ↔ ((𝑅 ∈ ℝ ∧ 𝑇 ∈ ℝ) ∧ (𝑆 ∈ ℝ ∧ 𝑈 ∈ ℝ)))
94	88, 92, 93	3bitr4g 313	. . . 4 ⊢ (𝜑 → (∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ ((𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ))))
95	94	anbi2d 629	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ((𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ)))))
96		3anass 1095	. . 3 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ)) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ((𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ))))
97	95, 96	bitr4di 288	. 2 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ))))
98	4, 97	bitrd 278	1 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064   ∪ cun 3908  ifcif 4486  {cpr 4588   class class class wbr 5105   ↦ cmpt 5188  ‘cfv 6496  (class class class)co 7357  ℂcc 11049  ℝcr 11050  0cc0 11051  1c1 11052  ici 11053   ≤ cle 11190  -cneg 11386   / cdiv 11812  2c2 12208  3c3 12209  ...cfz 13424  ↑cexp 13967  ℜcre 14982  ℑcim 14983  MblFncmbf 24978  ∫₂citg2 24980  𝐿¹cibl 24981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-z 12500  df-uz 12764  df-fz 13425  df-seq 13907  df-exp 13968  df-cj 14984  df-re 14985  df-im 14986  df-ibl 24986

This theorem is referenced by:  iblcnlem  25153  iblcn  25163  bddiblnc  25206