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

Theorem cncfco 24270
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.
StepHypRef Expression
1 cncfco.5 . . . 4 (𝜑𝐺 ∈ (𝐵cn𝐶))
2 cncff 24256 . . . 4 (𝐺 ∈ (𝐵cn𝐶) → 𝐺:𝐵𝐶)
31, 2syl 17 . . 3 (𝜑𝐺:𝐵𝐶)
4 cncfco.4 . . . 4 (𝜑𝐹 ∈ (𝐴cn𝐵))
5 cncff 24256 . . . 4 (𝐹 ∈ (𝐴cn𝐵) → 𝐹:𝐴𝐵)
64, 5syl 17 . . 3 (𝜑𝐹:𝐴𝐵)
7 fco 6692 . . 3 ((𝐺:𝐵𝐶𝐹:𝐴𝐵) → (𝐺𝐹):𝐴𝐶)
83, 6, 7syl2anc 584 . 2 (𝜑 → (𝐺𝐹):𝐴𝐶)
91adantr 481 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) → 𝐺 ∈ (𝐵cn𝐶))
106adantr 481 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) → 𝐹:𝐴𝐵)
11 simprl 769 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) → 𝑥𝐴)
1210, 11ffvelcdmd 7036 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) → (𝐹𝑥) ∈ 𝐵)
13 simprr 771 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) → 𝑦 ∈ ℝ+)
14 cncfi 24257 . . . . 5 ((𝐺 ∈ (𝐵cn𝐶) ∧ (𝐹𝑥) ∈ 𝐵𝑦 ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦))
159, 12, 13, 14syl3anc 1371 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) → ∃𝑢 ∈ ℝ+𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦))
164ad2antrr 724 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) → 𝐹 ∈ (𝐴cn𝐵))
17 simplrl 775 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) → 𝑥𝐴)
18 simpr 485 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) → 𝑢 ∈ ℝ+)
19 cncfi 24257 . . . . . . 7 ((𝐹 ∈ (𝐴cn𝐵) ∧ 𝑥𝐴𝑢 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢))
2016, 17, 18, 19syl3anc 1371 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢))
216ad3antrrr 728 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → 𝐹:𝐴𝐵)
22 simprr 771 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → 𝑤𝐴)
2321, 22ffvelcdmd 7036 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → (𝐹𝑤) ∈ 𝐵)
24 fvoveq1 7380 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝐹𝑤) → (abs‘(𝑣 − (𝐹𝑥))) = (abs‘((𝐹𝑤) − (𝐹𝑥))))
2524breq1d 5115 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝐹𝑤) → ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 ↔ (abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢))
2625imbrov2fvoveq 7382 . . . . . . . . . . . . . . . 16 (𝑣 = (𝐹𝑤) → (((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦) ↔ ((abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹𝑤)) − (𝐺‘(𝐹𝑥)))) < 𝑦)))
2726rspcv 3577 . . . . . . . . . . . . . . 15 ((𝐹𝑤) ∈ 𝐵 → (∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹𝑤)) − (𝐺‘(𝐹𝑥)))) < 𝑦)))
2823, 27syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → (∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹𝑤)) − (𝐺‘(𝐹𝑥)))) < 𝑦)))
29 fvco3 6940 . . . . . . . . . . . . . . . . . . 19 ((𝐹:𝐴𝐵𝑤𝐴) → ((𝐺𝐹)‘𝑤) = (𝐺‘(𝐹𝑤)))
3021, 22, 29syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → ((𝐺𝐹)‘𝑤) = (𝐺‘(𝐹𝑤)))
3117adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → 𝑥𝐴)
32 fvco3 6940 . . . . . . . . . . . . . . . . . . 19 ((𝐹:𝐴𝐵𝑥𝐴) → ((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)))
3321, 31, 32syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → ((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)))
3430, 33oveq12d 7375 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → (((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥)) = ((𝐺‘(𝐹𝑤)) − (𝐺‘(𝐹𝑥))))
3534fveq2d 6846 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) = (abs‘((𝐺‘(𝐹𝑤)) − (𝐺‘(𝐹𝑥)))))
3635breq1d 5115 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → ((abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦 ↔ (abs‘((𝐺‘(𝐹𝑤)) − (𝐺‘(𝐹𝑥)))) < 𝑦))
3736imbi2d 340 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → (((abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦) ↔ ((abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹𝑤)) − (𝐺‘(𝐹𝑥)))) < 𝑦)))
3828, 37sylibrd 258 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → (∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦)))
3938imp 407 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) ∧ ∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦)) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦))
4039an32s 650 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦)) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦))
4140imim2d 57 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦)) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → (((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢) → ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦)))
4241anassrs 468 . . . . . . . . 9 ((((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤𝐴) → (((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢) → ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦)))
4342ralimdva 3164 . . . . . . . 8 (((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦)) ∧ 𝑧 ∈ ℝ+) → (∀𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢) → ∀𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦)))
4443reximdva 3165 . . . . . . 7 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦)) → (∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦)))
4544ex 413 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) → (∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦) → (∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦))))
4620, 45mpid 44 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) → (∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦)))
4746rexlimdva 3152 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) → (∃𝑢 ∈ ℝ+𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦)))
4815, 47mpd 15 . . 3 ((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦))
4948ralrimivva 3197 . 2 (𝜑 → ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦))
50 cncfrss 24254 . . . 4 (𝐹 ∈ (𝐴cn𝐵) → 𝐴 ⊆ ℂ)
514, 50syl 17 . . 3 (𝜑𝐴 ⊆ ℂ)
52 cncfrss2 24255 . . . 4 (𝐺 ∈ (𝐵cn𝐶) → 𝐶 ⊆ ℂ)
531, 52syl 17 . . 3 (𝜑𝐶 ⊆ ℂ)
54 elcncf2 24253 . . 3 ((𝐴 ⊆ ℂ ∧ 𝐶 ⊆ ℂ) → ((𝐺𝐹) ∈ (𝐴cn𝐶) ↔ ((𝐺𝐹):𝐴𝐶 ∧ ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦))))
5551, 53, 54syl2anc 584 . 2 (𝜑 → ((𝐺𝐹) ∈ (𝐴cn𝐶) ↔ ((𝐺𝐹):𝐴𝐶 ∧ ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦))))
568, 49, 55mpbir2and 711 1 (𝜑 → (𝐺𝐹) ∈ (𝐴cn𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3064  wrex 3073  wss 3910   class class class wbr 5105  ccom 5637  wf 6492  cfv 6496  (class class class)co 7357  cc 11049   < clt 11189  cmin 11385  +crp 12915  abscabs 15119  cnccncf 24239
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-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-po 5545  df-so 5546  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-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-er 8648  df-map 8767  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-2 12216  df-cj 14984  df-re 14985  df-im 14986  df-abs 15121  df-cncf 24241
This theorem is referenced by:  cncfcompt2  24271  cncfmpt1f  24277  negfcncf  24286  divcncf  24811  cniccbdd  24825  cncombf  25022  cnmbf  25023  dvlip  25357  dvlipcn  25358  itgsubstlem  25412  sincn  25803  coscn  25804  logcn  26002  lgamgulmlem2  26379  ftalem3  26424  evthiccabs  43724  mulc1cncfg  43820  expcnfg  43822  cncfcompt  44114  cncficcgt0  44119  dirkercncflem2  44335  dirkercncflem4  44337  fourierdlem18  44356  fourierdlem93  44430  fourierdlem101  44438  fourierdlem111  44448
  Copyright terms: Public domain W3C validator