Theorem ftc1anclem3 34117

Description: Lemma for ftc1anc 34123- the absolute value of the sum of a simple function and i times another simple function is itself a simple function. (Contributed by Brendan Leahy, 27-May-2018.)

Assertion

Ref	Expression
ftc1anclem3	⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (abs ∘ (𝐹 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝐺))) ∈ dom ∫1)

Proof of Theorem ftc1anclem3

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		i1ff 23884	. . . . . . . 8 ⊢ (𝐹 ∈ dom ∫1 → 𝐹:ℝ⟶ℝ)
2	1	ffvelrnda 6625	. . . . . . 7 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
3		i1ff 23884	. . . . . . . 8 ⊢ (𝐺 ∈ dom ∫1 → 𝐺:ℝ⟶ℝ)
4	3	ffvelrnda 6625	. . . . . . 7 ⊢ ((𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (𝐺‘𝑥) ∈ ℝ)
5		absreim 14444	. . . . . . 7 ⊢ (((𝐹‘𝑥) ∈ ℝ ∧ (𝐺‘𝑥) ∈ ℝ) → (abs‘((𝐹‘𝑥) + (i · (𝐺‘𝑥)))) = (√‘(((𝐹‘𝑥)↑2) + ((𝐺‘𝑥)↑2))))
6	2, 4, 5	syl2an 589	. . . . . 6 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) ∧ (𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ)) → (abs‘((𝐹‘𝑥) + (i · (𝐺‘𝑥)))) = (√‘(((𝐹‘𝑥)↑2) + ((𝐺‘𝑥)↑2))))
7	6	anandirs 669	. . . . 5 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (abs‘((𝐹‘𝑥) + (i · (𝐺‘𝑥)))) = (√‘(((𝐹‘𝑥)↑2) + ((𝐺‘𝑥)↑2))))
8	2	recnd 10407	. . . . . . . . 9 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℂ)
9	8	sqvald 13328	. . . . . . . 8 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥)↑2) = ((𝐹‘𝑥) · (𝐹‘𝑥)))
10	4	recnd 10407	. . . . . . . . 9 ⊢ ((𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (𝐺‘𝑥) ∈ ℂ)
11	10	sqvald 13328	. . . . . . . 8 ⊢ ((𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑥)↑2) = ((𝐺‘𝑥) · (𝐺‘𝑥)))
12	9, 11	oveqan12d 6943	. . . . . . 7 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) ∧ (𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ)) → (((𝐹‘𝑥)↑2) + ((𝐺‘𝑥)↑2)) = (((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥))))
13	12	anandirs 669	. . . . . 6 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑥)↑2) + ((𝐺‘𝑥)↑2)) = (((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥))))
14	13	fveq2d 6452	. . . . 5 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (√‘(((𝐹‘𝑥)↑2) + ((𝐺‘𝑥)↑2))) = (√‘(((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥)))))
15	7, 14	eqtrd 2814	. . . 4 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (abs‘((𝐹‘𝑥) + (i · (𝐺‘𝑥)))) = (√‘(((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥)))))
16	15	mpteq2dva 4981	. . 3 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (𝑥 ∈ ℝ ↦ (abs‘((𝐹‘𝑥) + (i · (𝐺‘𝑥))))) = (𝑥 ∈ ℝ ↦ (√‘(((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥))))))
17		ax-icn 10333	. . . . . . 7 ⊢ i ∈ ℂ
18		mulcl 10358	. . . . . . 7 ⊢ ((i ∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ) → (i · (𝐺‘𝑥)) ∈ ℂ)
19	17, 10, 18	sylancr 581	. . . . . 6 ⊢ ((𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (i · (𝐺‘𝑥)) ∈ ℂ)
20		addcl 10356	. . . . . 6 ⊢ (((𝐹‘𝑥) ∈ ℂ ∧ (i · (𝐺‘𝑥)) ∈ ℂ) → ((𝐹‘𝑥) + (i · (𝐺‘𝑥))) ∈ ℂ)
21	8, 19, 20	syl2an 589	. . . . 5 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) ∧ (𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ)) → ((𝐹‘𝑥) + (i · (𝐺‘𝑥))) ∈ ℂ)
22	21	anandirs 669	. . . 4 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) + (i · (𝐺‘𝑥))) ∈ ℂ)
23		reex 10365	. . . . . 6 ⊢ ℝ ∈ V
24	23	a1i 11	. . . . 5 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → ℝ ∈ V)
25	2	adantlr 705	. . . . 5 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
26		ovexd 6958	. . . . 5 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (i · (𝐺‘𝑥)) ∈ V)
27	1	feqmptd 6511	. . . . . 6 ⊢ (𝐹 ∈ dom ∫1 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥)))
28	27	adantr 474	. . . . 5 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥)))
29	23	a1i 11	. . . . . . 7 ⊢ (𝐺 ∈ dom ∫1 → ℝ ∈ V)
30	17	a1i 11	. . . . . . 7 ⊢ ((𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → i ∈ ℂ)
31		fconstmpt 5413	. . . . . . . 8 ⊢ (ℝ × {i}) = (𝑥 ∈ ℝ ↦ i)
32	31	a1i 11	. . . . . . 7 ⊢ (𝐺 ∈ dom ∫1 → (ℝ × {i}) = (𝑥 ∈ ℝ ↦ i))
33	3	feqmptd 6511	. . . . . . 7 ⊢ (𝐺 ∈ dom ∫1 → 𝐺 = (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)))
34	29, 30, 4, 32, 33	offval2 7193	. . . . . 6 ⊢ (𝐺 ∈ dom ∫1 → ((ℝ × {i}) ∘𝑓 · 𝐺) = (𝑥 ∈ ℝ ↦ (i · (𝐺‘𝑥))))
35	34	adantl 475	. . . . 5 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → ((ℝ × {i}) ∘𝑓 · 𝐺) = (𝑥 ∈ ℝ ↦ (i · (𝐺‘𝑥))))
36	24, 25, 26, 28, 35	offval2 7193	. . . 4 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (𝐹 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝐺)) = (𝑥 ∈ ℝ ↦ ((𝐹‘𝑥) + (i · (𝐺‘𝑥)))))
37		absf 14488	. . . . . 6 ⊢ abs:ℂ⟶ℝ
38	37	a1i 11	. . . . 5 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → abs:ℂ⟶ℝ)
39	38	feqmptd 6511	. . . 4 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → abs = (𝑦 ∈ ℂ ↦ (abs‘𝑦)))
40		fveq2 6448	. . . 4 ⊢ (𝑦 = ((𝐹‘𝑥) + (i · (𝐺‘𝑥))) → (abs‘𝑦) = (abs‘((𝐹‘𝑥) + (i · (𝐺‘𝑥)))))
41	22, 36, 39, 40	fmptco 6663	. . 3 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (abs ∘ (𝐹 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝐺))) = (𝑥 ∈ ℝ ↦ (abs‘((𝐹‘𝑥) + (i · (𝐺‘𝑥))))))
42	8, 8	mulcld 10399	. . . . . 6 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (𝐹‘𝑥)) ∈ ℂ)
43	10, 10	mulcld 10399	. . . . . 6 ⊢ ((𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑥) · (𝐺‘𝑥)) ∈ ℂ)
44		addcl 10356	. . . . . 6 ⊢ ((((𝐹‘𝑥) · (𝐹‘𝑥)) ∈ ℂ ∧ ((𝐺‘𝑥) · (𝐺‘𝑥)) ∈ ℂ) → (((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥))) ∈ ℂ)
45	42, 43, 44	syl2an 589	. . . . 5 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) ∧ (𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ)) → (((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥))) ∈ ℂ)
46	45	anandirs 669	. . . 4 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥))) ∈ ℂ)
47	42	adantlr 705	. . . . 5 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (𝐹‘𝑥)) ∈ ℂ)
48	43	adantll 704	. . . . 5 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑥) · (𝐺‘𝑥)) ∈ ℂ)
49	23	a1i 11	. . . . . . 7 ⊢ (𝐹 ∈ dom ∫1 → ℝ ∈ V)
50	49, 2, 2, 27, 27	offval2 7193	. . . . . 6 ⊢ (𝐹 ∈ dom ∫1 → (𝐹 ∘𝑓 · 𝐹) = (𝑥 ∈ ℝ ↦ ((𝐹‘𝑥) · (𝐹‘𝑥))))
51	50	adantr 474	. . . . 5 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (𝐹 ∘𝑓 · 𝐹) = (𝑥 ∈ ℝ ↦ ((𝐹‘𝑥) · (𝐹‘𝑥))))
52	29, 4, 4, 33, 33	offval2 7193	. . . . . 6 ⊢ (𝐺 ∈ dom ∫1 → (𝐺 ∘𝑓 · 𝐺) = (𝑥 ∈ ℝ ↦ ((𝐺‘𝑥) · (𝐺‘𝑥))))
53	52	adantl 475	. . . . 5 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (𝐺 ∘𝑓 · 𝐺) = (𝑥 ∈ ℝ ↦ ((𝐺‘𝑥) · (𝐺‘𝑥))))
54	24, 47, 48, 51, 53	offval2 7193	. . . 4 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) = (𝑥 ∈ ℝ ↦ (((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥)))))
55		sqrtf 14514	. . . . . 6 ⊢ √:ℂ⟶ℂ
56	55	a1i 11	. . . . 5 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → √:ℂ⟶ℂ)
57	56	feqmptd 6511	. . . 4 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → √ = (𝑦 ∈ ℂ ↦ (√‘𝑦)))
58		fveq2 6448	. . . 4 ⊢ (𝑦 = (((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥))) → (√‘𝑦) = (√‘(((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥)))))
59	46, 54, 57, 58	fmptco 6663	. . 3 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) = (𝑥 ∈ ℝ ↦ (√‘(((𝐹‘𝑥) · (𝐹‘𝑥)) + ((𝐺‘𝑥) · (𝐺‘𝑥))))))
60	16, 41, 59	3eqtr4d 2824	. 2 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (abs ∘ (𝐹 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝐺))) = (√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))))
61		elrege0 12596	. . . . . . 7 ⊢ (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
62		resqrtcl 14405	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (√‘𝑥) ∈ ℝ)
63	61, 62	sylbi 209	. . . . . 6 ⊢ (𝑥 ∈ (0[,)+∞) → (√‘𝑥) ∈ ℝ)
64	63	adantl 475	. . . . 5 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ (0[,)+∞)) → (√‘𝑥) ∈ ℝ)
65		id 22	. . . . . . . . 9 ⊢ (√:ℂ⟶ℂ → √:ℂ⟶ℂ)
66	65	feqmptd 6511	. . . . . . . 8 ⊢ (√:ℂ⟶ℂ → √ = (𝑥 ∈ ℂ ↦ (√‘𝑥)))
67	55, 66	ax-mp 5	. . . . . . 7 ⊢ √ = (𝑥 ∈ ℂ ↦ (√‘𝑥))
68	67	reseq1i 5640	. . . . . 6 ⊢ (√ ↾ (0[,)+∞)) = ((𝑥 ∈ ℂ ↦ (√‘𝑥)) ↾ (0[,)+∞))
69		rge0ssre 12598	. . . . . . . 8 ⊢ (0[,)+∞) ⊆ ℝ
70		ax-resscn 10331	. . . . . . . 8 ⊢ ℝ ⊆ ℂ
71	69, 70	sstri 3830	. . . . . . 7 ⊢ (0[,)+∞) ⊆ ℂ
72		resmpt 5701	. . . . . . 7 ⊢ ((0[,)+∞) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (√‘𝑥)) ↾ (0[,)+∞)) = (𝑥 ∈ (0[,)+∞) ↦ (√‘𝑥)))
73	71, 72	ax-mp 5	. . . . . 6 ⊢ ((𝑥 ∈ ℂ ↦ (√‘𝑥)) ↾ (0[,)+∞)) = (𝑥 ∈ (0[,)+∞) ↦ (√‘𝑥))
74	68, 73	eqtri 2802	. . . . 5 ⊢ (√ ↾ (0[,)+∞)) = (𝑥 ∈ (0[,)+∞) ↦ (√‘𝑥))
75	64, 74	fmptd 6650	. . . 4 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (√ ↾ (0[,)+∞)):(0[,)+∞)⟶ℝ)
76		ge0addcl 12602	. . . . . 6 ⊢ ((𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞)) → (𝑥 + 𝑦) ∈ (0[,)+∞))
77	76	adantl 475	. . . . 5 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞))) → (𝑥 + 𝑦) ∈ (0[,)+∞))
78		oveq12 6933	. . . . . . . . 9 ⊢ ((𝑧 = 𝐹 ∧ 𝑧 = 𝐹) → (𝑧 ∘𝑓 · 𝑧) = (𝐹 ∘𝑓 · 𝐹))
79	78	anidms 562	. . . . . . . 8 ⊢ (𝑧 = 𝐹 → (𝑧 ∘𝑓 · 𝑧) = (𝐹 ∘𝑓 · 𝐹))
80	79	feq1d 6278	. . . . . . 7 ⊢ (𝑧 = 𝐹 → ((𝑧 ∘𝑓 · 𝑧):ℝ⟶(0[,)+∞) ↔ (𝐹 ∘𝑓 · 𝐹):ℝ⟶(0[,)+∞)))
81		i1ff 23884	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ dom ∫1 → 𝑧:ℝ⟶ℝ)
82	81	ffvelrnda 6625	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → (𝑧‘𝑥) ∈ ℝ)
83	82, 82	remulcld 10409	. . . . . . . . . 10 ⊢ ((𝑧 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → ((𝑧‘𝑥) · (𝑧‘𝑥)) ∈ ℝ)
84	82	msqge0d 10945	. . . . . . . . . 10 ⊢ ((𝑧 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝑧‘𝑥) · (𝑧‘𝑥)))
85		elrege0 12596	. . . . . . . . . 10 ⊢ (((𝑧‘𝑥) · (𝑧‘𝑥)) ∈ (0[,)+∞) ↔ (((𝑧‘𝑥) · (𝑧‘𝑥)) ∈ ℝ ∧ 0 ≤ ((𝑧‘𝑥) · (𝑧‘𝑥))))
86	83, 84, 85	sylanbrc 578	. . . . . . . . 9 ⊢ ((𝑧 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ) → ((𝑧‘𝑥) · (𝑧‘𝑥)) ∈ (0[,)+∞))
87	86	fmpttd 6651	. . . . . . . 8 ⊢ (𝑧 ∈ dom ∫1 → (𝑥 ∈ ℝ ↦ ((𝑧‘𝑥) · (𝑧‘𝑥))):ℝ⟶(0[,)+∞))
88	23	a1i 11	. . . . . . . . . 10 ⊢ (𝑧 ∈ dom ∫1 → ℝ ∈ V)
89	81	feqmptd 6511	. . . . . . . . . 10 ⊢ (𝑧 ∈ dom ∫1 → 𝑧 = (𝑥 ∈ ℝ ↦ (𝑧‘𝑥)))
90	88, 82, 82, 89, 89	offval2 7193	. . . . . . . . 9 ⊢ (𝑧 ∈ dom ∫1 → (𝑧 ∘𝑓 · 𝑧) = (𝑥 ∈ ℝ ↦ ((𝑧‘𝑥) · (𝑧‘𝑥))))
91	90	feq1d 6278	. . . . . . . 8 ⊢ (𝑧 ∈ dom ∫1 → ((𝑧 ∘𝑓 · 𝑧):ℝ⟶(0[,)+∞) ↔ (𝑥 ∈ ℝ ↦ ((𝑧‘𝑥) · (𝑧‘𝑥))):ℝ⟶(0[,)+∞)))
92	87, 91	mpbird 249	. . . . . . 7 ⊢ (𝑧 ∈ dom ∫1 → (𝑧 ∘𝑓 · 𝑧):ℝ⟶(0[,)+∞))
93	80, 92	vtoclga 3474	. . . . . 6 ⊢ (𝐹 ∈ dom ∫1 → (𝐹 ∘𝑓 · 𝐹):ℝ⟶(0[,)+∞))
94	93	adantr 474	. . . . 5 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (𝐹 ∘𝑓 · 𝐹):ℝ⟶(0[,)+∞))
95		oveq12 6933	. . . . . . . . 9 ⊢ ((𝑧 = 𝐺 ∧ 𝑧 = 𝐺) → (𝑧 ∘𝑓 · 𝑧) = (𝐺 ∘𝑓 · 𝐺))
96	95	anidms 562	. . . . . . . 8 ⊢ (𝑧 = 𝐺 → (𝑧 ∘𝑓 · 𝑧) = (𝐺 ∘𝑓 · 𝐺))
97	96	feq1d 6278	. . . . . . 7 ⊢ (𝑧 = 𝐺 → ((𝑧 ∘𝑓 · 𝑧):ℝ⟶(0[,)+∞) ↔ (𝐺 ∘𝑓 · 𝐺):ℝ⟶(0[,)+∞)))
98	97, 92	vtoclga 3474	. . . . . 6 ⊢ (𝐺 ∈ dom ∫1 → (𝐺 ∘𝑓 · 𝐺):ℝ⟶(0[,)+∞))
99	98	adantl 475	. . . . 5 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (𝐺 ∘𝑓 · 𝐺):ℝ⟶(0[,)+∞))
100		inidm 4043	. . . . 5 ⊢ (ℝ ∩ ℝ) = ℝ
101	77, 94, 99, 24, 24, 100	off 7191	. . . 4 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)):ℝ⟶(0[,)+∞))
102		fco2 6311	. . . 4 ⊢ (((√ ↾ (0[,)+∞)):(0[,)+∞)⟶ℝ ∧ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)):ℝ⟶(0[,)+∞)) → (√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))):ℝ⟶ℝ)
103	75, 101, 102	syl2anc 579	. . 3 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))):ℝ⟶ℝ)
104		rnco 5897	. . . 4 ⊢ ran (√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) = ran (√ ↾ ran ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)))
105		ffn 6293	. . . . . . . 8 ⊢ (√:ℂ⟶ℂ → √ Fn ℂ)
106	55, 105	ax-mp 5	. . . . . . 7 ⊢ √ Fn ℂ
107		readdcl 10357	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
108	107	adantl 475	. . . . . . . . . 10 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ)
109		remulcl 10359	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ)
110	109	adantl 475	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
111	110, 1, 1, 49, 49, 100	off 7191	. . . . . . . . . . 11 ⊢ (𝐹 ∈ dom ∫1 → (𝐹 ∘𝑓 · 𝐹):ℝ⟶ℝ)
112	111	adantr 474	. . . . . . . . . 10 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (𝐹 ∘𝑓 · 𝐹):ℝ⟶ℝ)
113	109	adantl 475	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
114	113, 3, 3, 29, 29, 100	off 7191	. . . . . . . . . . 11 ⊢ (𝐺 ∈ dom ∫1 → (𝐺 ∘𝑓 · 𝐺):ℝ⟶ℝ)
115	114	adantl 475	. . . . . . . . . 10 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (𝐺 ∘𝑓 · 𝐺):ℝ⟶ℝ)
116	108, 112, 115, 24, 24, 100	off 7191	. . . . . . . . 9 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)):ℝ⟶ℝ)
117	116	frnd 6300	. . . . . . . 8 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → ran ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) ⊆ ℝ)
118	117, 70	syl6ss 3833	. . . . . . 7 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → ran ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) ⊆ ℂ)
119		fnssres 6252	. . . . . . 7 ⊢ ((√ Fn ℂ ∧ ran ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) ⊆ ℂ) → (√ ↾ ran ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) Fn ran ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)))
120	106, 118, 119	sylancr 581	. . . . . 6 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (√ ↾ ran ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) Fn ran ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)))
121		id 22	. . . . . . . . . 10 ⊢ (𝐹 ∈ dom ∫1 → 𝐹 ∈ dom ∫1)
122	121, 121	i1fmul 23904	. . . . . . . . 9 ⊢ (𝐹 ∈ dom ∫1 → (𝐹 ∘𝑓 · 𝐹) ∈ dom ∫1)
123	122	adantr 474	. . . . . . . 8 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (𝐹 ∘𝑓 · 𝐹) ∈ dom ∫1)
124		id 22	. . . . . . . . . 10 ⊢ (𝐺 ∈ dom ∫1 → 𝐺 ∈ dom ∫1)
125	124, 124	i1fmul 23904	. . . . . . . . 9 ⊢ (𝐺 ∈ dom ∫1 → (𝐺 ∘𝑓 · 𝐺) ∈ dom ∫1)
126	125	adantl 475	. . . . . . . 8 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (𝐺 ∘𝑓 · 𝐺) ∈ dom ∫1)
127	123, 126	i1fadd 23903	. . . . . . 7 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) ∈ dom ∫1)
128		i1frn 23885	. . . . . . 7 ⊢ (((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) ∈ dom ∫1 → ran ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) ∈ Fin)
129	127, 128	syl 17	. . . . . 6 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → ran ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) ∈ Fin)
130		fnfi 8528	. . . . . 6 ⊢ (((√ ↾ ran ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) Fn ran ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) ∧ ran ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) ∈ Fin) → (√ ↾ ran ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) ∈ Fin)
131	120, 129, 130	syl2anc 579	. . . . 5 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (√ ↾ ran ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) ∈ Fin)
132		rnfi 8539	. . . . 5 ⊢ ((√ ↾ ran ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) ∈ Fin → ran (√ ↾ ran ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) ∈ Fin)
133	131, 132	syl 17	. . . 4 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → ran (√ ↾ ran ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) ∈ Fin)
134	104, 133	syl5eqel 2863	. . 3 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → ran (√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) ∈ Fin)
135		cnvco 5555	. . . . . . 7 ⊢ ◡(√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) = (◡((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) ∘ ◡√)
136	135	imaeq1i 5719	. . . . . 6 ⊢ (◡(√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) “ {𝑥}) = ((◡((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) ∘ ◡√) “ {𝑥})
137		imaco 5896	. . . . . 6 ⊢ ((◡((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) ∘ ◡√) “ {𝑥}) = (◡((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) “ (◡√ “ {𝑥}))
138	136, 137	eqtri 2802	. . . . 5 ⊢ (◡(√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) “ {𝑥}) = (◡((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) “ (◡√ “ {𝑥}))
139		i1fima 23886	. . . . . 6 ⊢ (((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) ∈ dom ∫1 → (◡((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) “ (◡√ “ {𝑥})) ∈ dom vol)
140	127, 139	syl 17	. . . . 5 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (◡((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) “ (◡√ “ {𝑥})) ∈ dom vol)
141	138, 140	syl5eqel 2863	. . . 4 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (◡(√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) “ {𝑥}) ∈ dom vol)
142	141	adantr 474	. . 3 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ (ran (√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) ∖ {0})) → (◡(√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) “ {𝑥}) ∈ dom vol)
143	138	fveq2i 6451	. . . 4 ⊢ (vol‘(◡(√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) “ {𝑥})) = (vol‘(◡((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) “ (◡√ “ {𝑥})))
144		eldifsni 4553	. . . . . . . 8 ⊢ (𝑥 ∈ (ran (√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) ∖ {0}) → 𝑥 ≠ 0)
145		c0ex 10372	. . . . . . . . . . . 12 ⊢ 0 ∈ V
146	145	elsn 4413	. . . . . . . . . . 11 ⊢ (0 ∈ {𝑥} ↔ 0 = 𝑥)
147		eqcom 2785	. . . . . . . . . . 11 ⊢ (0 = 𝑥 ↔ 𝑥 = 0)
148	146, 147	bitri 267	. . . . . . . . . 10 ⊢ (0 ∈ {𝑥} ↔ 𝑥 = 0)
149	148	necon3bbii 3016	. . . . . . . . 9 ⊢ (¬ 0 ∈ {𝑥} ↔ 𝑥 ≠ 0)
150		sqrt0 14393	. . . . . . . . . 10 ⊢ (√‘0) = 0
151	150	eleq1i 2850	. . . . . . . . 9 ⊢ ((√‘0) ∈ {𝑥} ↔ 0 ∈ {𝑥})
152	149, 151	xchnxbir 325	. . . . . . . 8 ⊢ (¬ (√‘0) ∈ {𝑥} ↔ 𝑥 ≠ 0)
153	144, 152	sylibr 226	. . . . . . 7 ⊢ (𝑥 ∈ (ran (√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) ∖ {0}) → ¬ (√‘0) ∈ {𝑥})
154	153	olcd 863	. . . . . 6 ⊢ (𝑥 ∈ (ran (√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) ∖ {0}) → (¬ 0 ∈ ℂ ∨ ¬ (√‘0) ∈ {𝑥}))
155		ianor 967	. . . . . . 7 ⊢ (¬ (0 ∈ ℂ ∧ (√‘0) ∈ {𝑥}) ↔ (¬ 0 ∈ ℂ ∨ ¬ (√‘0) ∈ {𝑥}))
156		elpreima 6602	. . . . . . . 8 ⊢ (√ Fn ℂ → (0 ∈ (◡√ “ {𝑥}) ↔ (0 ∈ ℂ ∧ (√‘0) ∈ {𝑥})))
157	55, 105, 156	mp2b 10	. . . . . . 7 ⊢ (0 ∈ (◡√ “ {𝑥}) ↔ (0 ∈ ℂ ∧ (√‘0) ∈ {𝑥}))
158	155, 157	xchnxbir 325	. . . . . 6 ⊢ (¬ 0 ∈ (◡√ “ {𝑥}) ↔ (¬ 0 ∈ ℂ ∨ ¬ (√‘0) ∈ {𝑥}))
159	154, 158	sylibr 226	. . . . 5 ⊢ (𝑥 ∈ (ran (√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) ∖ {0}) → ¬ 0 ∈ (◡√ “ {𝑥}))
160		i1fima2 23887	. . . . 5 ⊢ ((((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) ∈ dom ∫1 ∧ ¬ 0 ∈ (◡√ “ {𝑥})) → (vol‘(◡((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) “ (◡√ “ {𝑥}))) ∈ ℝ)
161	127, 159, 160	syl2an 589	. . . 4 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ (ran (√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) ∖ {0})) → (vol‘(◡((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺)) “ (◡√ “ {𝑥}))) ∈ ℝ)
162	143, 161	syl5eqel 2863	. . 3 ⊢ (((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ (ran (√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) ∖ {0})) → (vol‘(◡(√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) “ {𝑥})) ∈ ℝ)
163	103, 134, 142, 162	i1fd 23889	. 2 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (√ ∘ ((𝐹 ∘𝑓 · 𝐹) ∘𝑓 + (𝐺 ∘𝑓 · 𝐺))) ∈ dom ∫1)
164	60, 163	eqeltrd 2859	1 ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (abs ∘ (𝐹 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝐺))) ∈ dom ∫1)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∨ wo 836   = wceq 1601   ∈ wcel 2107   ≠ wne 2969  Vcvv 3398   ∖ cdif 3789   ⊆ wss 3792  {csn 4398   class class class wbr 4888   ↦ cmpt 4967   × cxp 5355  ^◡ccnv 5356  dom cdm 5357  ran crn 5358   ↾ cres 5359   “ cima 5360   ∘ ccom 5361   Fn wfn 6132  ⟶wf 6133  ‘cfv 6137  (class class class)co 6924   ∘_𝑓 cof 7174  Fincfn 8243  ℂcc 10272  ℝcr 10273  0cc0 10274  ici 10276   + caddc 10277   · cmul 10279  +∞cpnf 10410   ≤ cle 10414  2c2 11434  [,)cico 12493  ↑cexp 13182  √csqrt 14384  abscabs 14385  volcvol 23671  ∫₁citg1 23823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-inf2 8837  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351  ax-pre-sup 10352

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-se 5317  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-isom 6146  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-of 7176  df-om 7346  df-1st 7447  df-2nd 7448  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-2o 7846  df-oadd 7849  df-er 8028  df-map 8144  df-pm 8145  df-en 8244  df-dom 8245  df-sdom 8246  df-fin 8247  df-sup 8638  df-inf 8639  df-oi 8706  df-card 9100  df-cda 9327  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-div 11035  df-nn 11379  df-2 11442  df-3 11443  df-n0 11647  df-z 11733  df-uz 11997  df-q 12100  df-rp 12142  df-xadd 12262  df-ioo 12495  df-ico 12497  df-icc 12498  df-fz 12648  df-fzo 12789  df-fl 12916  df-seq 13124  df-exp 13183  df-hash 13440  df-cj 14250  df-re 14251  df-im 14252  df-sqrt 14386  df-abs 14387  df-clim 14631  df-sum 14829  df-xmet 20139  df-met 20140  df-ovol 23672  df-vol 23673  df-mbf 23827  df-itg1 23828

This theorem is referenced by:  ftc1anclem7  34121  ftc1anclem8  34122