cncfco - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cncfco		Structured version Visualization version GIF version

Theorem cncfco 24828

Description: The composition of two continuous maps on complex numbers is also continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 25-Aug-2014.)

**Hypotheses**
Ref	Expression
cncfco.4	⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵))
cncfco.5	⊢ (𝜑 → 𝐺 ∈ (𝐵–cn→𝐶))

**Assertion**
Ref	Expression
cncfco	⊢ (𝜑 → (𝐺 ∘ 𝐹) ∈ (𝐴–cn→𝐶))

Proof of Theorem cncfco Dummy variables 𝑤 𝑢 𝑥 𝑦 𝑧 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cncfco.5	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (𝐵–cn→𝐶))
2		cncff 24814	. . . 4 ⊢ (𝐺 ∈ (𝐵–cn→𝐶) → 𝐺:𝐵⟶𝐶)
3	1, 2	syl 17	. . 3 ⊢ (𝜑 → 𝐺:𝐵⟶𝐶)
4		cncfco.4	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵))
5		cncff 24814	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐹:𝐴⟶𝐵)
6	4, 5	syl 17	. . 3 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
7		fco 6680	. . 3 ⊢ ((𝐺:𝐵⟶𝐶 ∧ 𝐹:𝐴⟶𝐵) → (𝐺 ∘ 𝐹):𝐴⟶𝐶)
8	3, 6, 7	syl2anc 584	. 2 ⊢ (𝜑 → (𝐺 ∘ 𝐹):𝐴⟶𝐶)
9	1	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) → 𝐺 ∈ (𝐵–cn→𝐶))
10	6	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) → 𝐹:𝐴⟶𝐵)
11		simprl 770	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) → 𝑥 ∈ 𝐴)
12	10, 11	ffvelcdmd 7024	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) → (𝐹‘𝑥) ∈ 𝐵)
13		simprr 772	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) → 𝑦 ∈ ℝ⁺)
14		cncfi 24815	. . . . 5 ⊢ ((𝐺 ∈ (𝐵–cn→𝐶) ∧ (𝐹‘𝑥) ∈ 𝐵 ∧ 𝑦 ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦))
15	9, 12, 13, 14	syl3anc 1373	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦))
16	4	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) → 𝐹 ∈ (𝐴–cn→𝐵))
17		simplrl 776	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) → 𝑥 ∈ 𝐴)
18		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) → 𝑢 ∈ ℝ⁺)
19		cncfi 24815	. . . . . . 7 ⊢ ((𝐹 ∈ (𝐴–cn→𝐵) ∧ 𝑥 ∈ 𝐴 ∧ 𝑢 ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢))
20	16, 17, 18, 19	syl3anc 1373	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢))
21	6	ad3antrrr 730	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → 𝐹:𝐴⟶𝐵)
22		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → 𝑤 ∈ 𝐴)
23	21, 22	ffvelcdmd 7024	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → (𝐹‘𝑤) ∈ 𝐵)
24		fvoveq1 7375	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝐹‘𝑤) → (abs‘(𝑣 − (𝐹‘𝑥))) = (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))))
25	24	breq1d 5103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = (𝐹‘𝑤) → ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 ↔ (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢))
26	25	imbrov2fvoveq 7377	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = (𝐹‘𝑤) → (((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) ↔ ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)))
27	26	rspcv 3569	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑤) ∈ 𝐵 → (∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)))
28	23, 27	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → (∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)))
29		fvco3 6927	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑤 ∈ 𝐴) → ((𝐺 ∘ 𝐹)‘𝑤) = (𝐺‘(𝐹‘𝑤)))
30	21, 22, 29	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → ((𝐺 ∘ 𝐹)‘𝑤) = (𝐺‘(𝐹‘𝑤)))
31	17	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → 𝑥 ∈ 𝐴)
32		fvco3 6927	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥)))
33	21, 31, 32	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥)))
34	30, 33	oveq12d 7370	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → (((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥)) = ((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥))))
35	34	fveq2d 6832	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) = (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))))
36	35	breq1d 5103	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → ((abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦 ↔ (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦))
37	36	imbi2d 340	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → (((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦) ↔ ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)))
38	28, 37	sylibrd 259	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → (∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)))
39	38	imp 406	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) ∧ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))
40	39	an32s 652	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))
41	40	imim2d 57	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → (((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)))
42	41	anassrs 467	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑤 ∈ 𝐴) → (((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)))
43	42	ralimdva 3145	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)))
44	43	reximdva 3146	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) → (∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)))
45	44	ex 412	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) → (∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → (∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))))
46	20, 45	mpid 44	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) → (∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)))
47	46	rexlimdva 3134	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) → (∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)))
48	15, 47	mpd 15	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) → ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))
49	48	ralrimivva 3176	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))
50		cncfrss 24812	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
51	4, 50	syl 17	. . 3 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
52		cncfrss2 24813	. . . 4 ⊢ (𝐺 ∈ (𝐵–cn→𝐶) → 𝐶 ⊆ ℂ)
53	1, 52	syl 17	. . 3 ⊢ (𝜑 → 𝐶 ⊆ ℂ)
54		elcncf2 24811	. . 3 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐶 ⊆ ℂ) → ((𝐺 ∘ 𝐹) ∈ (𝐴–cn→𝐶) ↔ ((𝐺 ∘ 𝐹):𝐴⟶𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))))
55	51, 53, 54	syl2anc 584	. 2 ⊢ (𝜑 → ((𝐺 ∘ 𝐹) ∈ (𝐴–cn→𝐶) ↔ ((𝐺 ∘ 𝐹):𝐴⟶𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))))
56	8, 49, 55	mpbir2and 713	1 ⊢ (𝜑 → (𝐺 ∘ 𝐹) ∈ (𝐴–cn→𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2113 ∀wral 3048 ∃wrex 3057 ⊆ wss 3898 class class class wbr 5093 ∘ ccom 5623 ⟶wf 6482 ‘cfv 6486 (class class class)co 7352 ℂcc 11011 < clt 11153 − cmin 11351 ℝ⁺crp 12892 abscabs 15143 –cn→ccncf 24797

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-cnex 11069 ax-resscn 11070 ax-1cn 11071 ax-icn 11072 ax-addcl 11073 ax-addrcl 11074 ax-mulcl 11075 ax-mulrcl 11076 ax-mulcom 11077 ax-addass 11078 ax-mulass 11079 ax-distr 11080 ax-i2m1 11081 ax-1ne0 11082 ax-1rid 11083 ax-rnegex 11084 ax-rrecex 11085 ax-cnre 11086 ax-pre-lttri 11087 ax-pre-lttrn 11088 ax-pre-ltadd 11089 ax-pre-mulgt0 11090

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-op 4582 df-uni 4859 df-iun 4943 df-br 5094 df-opab 5156 df-mpt 5175 df-tr 5201 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7309 df-ov 7355 df-oprab 7356 df-mpo 7357 df-om 7803 df-2nd 7928 df-frecs 8217 df-wrecs 8248 df-recs 8297 df-rdg 8335 df-er 8628 df-map 8758 df-en 8876 df-dom 8877 df-sdom 8878 df-pnf 11155 df-mnf 11156 df-xr 11157 df-ltxr 11158 df-le 11159 df-sub 11353 df-neg 11354 df-div 11782 df-nn 12133 df-2 12195 df-cj 15008 df-re 15009 df-im 15010 df-abs 15145 df-cncf 24799

This theorem is referenced by: cncfcompt2 24829 cncfmpt1f 24835 negfcncf 24845 divcncf 25376 cniccbdd 25390 cncombf 25587 cnmbf 25588 dvlip 25926 dvlipcn 25927 itgsubstlem 25983 sincn 26382 coscn 26383 logcn 26584 lgamgulmlem2 26968 ftalem3 27013 evthiccabs 45620 mulc1cncfg 45713 expcnfg 45715 cncfcompt 46005 cncficcgt0 46010 dirkercncflem2 46226 dirkercncflem4 46228 fourierdlem18 46247 fourierdlem93 46321 fourierdlem101 46329 fourierdlem111 46339

W3C validator