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 24816

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 24802	. . . 4 ⊢ (𝐺 ∈ (𝐵–cn→𝐶) → 𝐺:𝐵⟶𝐶)
3	1, 2	syl 17	. . 3 ⊢ (𝜑 → 𝐺:𝐵⟶𝐶)
4		cncfco.4	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵))
5		cncff 24802	. . . 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 7023	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) → (𝐹‘𝑥) ∈ 𝐵)
13		simprr 772	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) → 𝑦 ∈ ℝ⁺)
14		cncfi 24803	. . . . 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 24803	. . . . . . 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 7023	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → (𝐹‘𝑤) ∈ 𝐵)
24		fvoveq1 7376	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝐹‘𝑤) → (abs‘(𝑣 − (𝐹‘𝑥))) = (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))))
25	24	breq1d 5105	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = (𝐹‘𝑤) → ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 ↔ (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢))
26	25	imbrov2fvoveq 7378	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = (𝐹‘𝑤) → (((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) ↔ ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)))
27	26	rspcv 3575	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑤) ∈ 𝐵 → (∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)))
28	23, 27	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → (∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)))
29		fvco3 6926	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑤 ∈ 𝐴) → ((𝐺 ∘ 𝐹)‘𝑤) = (𝐺‘(𝐹‘𝑤)))
30	21, 22, 29	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → ((𝐺 ∘ 𝐹)‘𝑤) = (𝐺‘(𝐹‘𝑤)))
31	17	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → 𝑥 ∈ 𝐴)
32		fvco3 6926	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥)))
33	21, 31, 32	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥)))
34	30, 33	oveq12d 7371	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → (((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥)) = ((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥))))
35	34	fveq2d 6830	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑤 ∈ 𝐴)) → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) = (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))))
36	35	breq1d 5105	. . . . . . . . . . . . . . 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 3141	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑢 ∈ ℝ⁺) ∧ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)))
44	43	reximdva 3142	. . . . . . 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 3130	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) → (∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)))
48	15, 47	mpd 15	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺)) → ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))
49	48	ralrimivva 3172	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))
50		cncfrss 24800	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
51	4, 50	syl 17	. . 3 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
52		cncfrss2 24801	. . . 4 ⊢ (𝐺 ∈ (𝐵–cn→𝐶) → 𝐶 ⊆ ℂ)
53	1, 52	syl 17	. . 3 ⊢ (𝜑 → 𝐶 ⊆ ℂ)
54		elcncf2 24799	. . 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 1540 ∈ wcel 2109 ∀wral 3044 ∃wrex 3053 ⊆ wss 3905 class class class wbr 5095 ∘ ccom 5627 ⟶wf 6482 ‘cfv 6486 (class class class)co 7353 ℂcc 11026 < clt 11168 − cmin 11365 ℝ⁺crp 12911 abscabs 15159 –cn→ccncf 24785

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-iun 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 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 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-om 7807 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-er 8632 df-map 8762 df-en 8880 df-dom 8881 df-sdom 8882 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11367 df-neg 11368 df-div 11796 df-nn 12147 df-2 12209 df-cj 15024 df-re 15025 df-im 15026 df-abs 15161 df-cncf 24787

This theorem is referenced by: cncfcompt2 24817 cncfmpt1f 24823 negfcncf 24833 divcncf 25364 cniccbdd 25378 cncombf 25575 cnmbf 25576 dvlip 25914 dvlipcn 25915 itgsubstlem 25971 sincn 26370 coscn 26371 logcn 26572 lgamgulmlem2 26956 ftalem3 27001 evthiccabs 45478 mulc1cncfg 45571 expcnfg 45573 cncfcompt 45865 cncficcgt0 45870 dirkercncflem2 46086 dirkercncflem4 46088 fourierdlem18 46107 fourierdlem93 46181 fourierdlem101 46189 fourierdlem111 46199

W3C validator