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

Theorem cncfco 22445
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 22431 . . . 4 (𝐺 ∈ (𝐵cn𝐶) → 𝐺:𝐵𝐶)
31, 2syl 17 . . 3 (𝜑𝐺:𝐵𝐶)
4 cncfco.4 . . . 4 (𝜑𝐹 ∈ (𝐴cn𝐵))
5 cncff 22431 . . . 4 (𝐹 ∈ (𝐴cn𝐵) → 𝐹:𝐴𝐵)
64, 5syl 17 . . 3 (𝜑𝐹:𝐴𝐵)
7 fco 5953 . . 3 ((𝐺:𝐵𝐶𝐹:𝐴𝐵) → (𝐺𝐹):𝐴𝐶)
83, 6, 7syl2anc 690 . 2 (𝜑 → (𝐺𝐹):𝐴𝐶)
91adantr 479 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) → 𝐺 ∈ (𝐵cn𝐶))
106adantr 479 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) → 𝐹:𝐴𝐵)
11 simprl 789 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) → 𝑥𝐴)
1210, 11ffvelrnd 6249 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) → (𝐹𝑥) ∈ 𝐵)
13 simprr 791 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) → 𝑦 ∈ ℝ+)
14 cncfi 22432 . . . . 5 ((𝐺 ∈ (𝐵cn𝐶) ∧ (𝐹𝑥) ∈ 𝐵𝑦 ∈ ℝ+) → ∃𝑢 ∈ ℝ+𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦))
159, 12, 13, 14syl3anc 1317 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) → ∃𝑢 ∈ ℝ+𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦))
164ad2antrr 757 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) → 𝐹 ∈ (𝐴cn𝐵))
17 simplrl 795 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) → 𝑥𝐴)
18 simpr 475 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) → 𝑢 ∈ ℝ+)
19 cncfi 22432 . . . . . . 7 ((𝐹 ∈ (𝐴cn𝐵) ∧ 𝑥𝐴𝑢 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢))
2016, 17, 18, 19syl3anc 1317 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢))
216ad3antrrr 761 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → 𝐹:𝐴𝐵)
22 simprr 791 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → 𝑤𝐴)
2321, 22ffvelrnd 6249 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → (𝐹𝑤) ∈ 𝐵)
24 oveq1 6530 . . . . . . . . . . . . . . . . . . 19 (𝑣 = (𝐹𝑤) → (𝑣 − (𝐹𝑥)) = ((𝐹𝑤) − (𝐹𝑥)))
2524fveq2d 6088 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝐹𝑤) → (abs‘(𝑣 − (𝐹𝑥))) = (abs‘((𝐹𝑤) − (𝐹𝑥))))
2625breq1d 4583 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝐹𝑤) → ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 ↔ (abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢))
27 fveq2 6084 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = (𝐹𝑤) → (𝐺𝑣) = (𝐺‘(𝐹𝑤)))
2827oveq1d 6538 . . . . . . . . . . . . . . . . . . 19 (𝑣 = (𝐹𝑤) → ((𝐺𝑣) − (𝐺‘(𝐹𝑥))) = ((𝐺‘(𝐹𝑤)) − (𝐺‘(𝐹𝑥))))
2928fveq2d 6088 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝐹𝑤) → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) = (abs‘((𝐺‘(𝐹𝑤)) − (𝐺‘(𝐹𝑥)))))
3029breq1d 4583 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝐹𝑤) → ((abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦 ↔ (abs‘((𝐺‘(𝐹𝑤)) − (𝐺‘(𝐹𝑥)))) < 𝑦))
3126, 30imbi12d 332 . . . . . . . . . . . . . . . 16 (𝑣 = (𝐹𝑤) → (((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦) ↔ ((abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹𝑤)) − (𝐺‘(𝐹𝑥)))) < 𝑦)))
3231rspcv 3273 . . . . . . . . . . . . . . 15 ((𝐹𝑤) ∈ 𝐵 → (∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹𝑤)) − (𝐺‘(𝐹𝑥)))) < 𝑦)))
3323, 32syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → (∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹𝑤)) − (𝐺‘(𝐹𝑥)))) < 𝑦)))
34 fvco3 6166 . . . . . . . . . . . . . . . . . . 19 ((𝐹:𝐴𝐵𝑤𝐴) → ((𝐺𝐹)‘𝑤) = (𝐺‘(𝐹𝑤)))
3521, 22, 34syl2anc 690 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → ((𝐺𝐹)‘𝑤) = (𝐺‘(𝐹𝑤)))
3617adantr 479 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → 𝑥𝐴)
37 fvco3 6166 . . . . . . . . . . . . . . . . . . 19 ((𝐹:𝐴𝐵𝑥𝐴) → ((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)))
3821, 36, 37syl2anc 690 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → ((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)))
3935, 38oveq12d 6541 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → (((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥)) = ((𝐺‘(𝐹𝑤)) − (𝐺‘(𝐹𝑥))))
4039fveq2d 6088 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) = (abs‘((𝐺‘(𝐹𝑤)) − (𝐺‘(𝐹𝑥)))))
4140breq1d 4583 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → ((abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦 ↔ (abs‘((𝐺‘(𝐹𝑤)) − (𝐺‘(𝐹𝑥)))) < 𝑦))
4241imbi2d 328 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → (((abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦) ↔ ((abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹𝑤)) − (𝐺‘(𝐹𝑥)))) < 𝑦)))
4333, 42sylibrd 247 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → (∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦)))
4443imp 443 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) ∧ ∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦)) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦))
4544an32s 841 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦)) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → ((abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦))
4645imim2d 54 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦)) ∧ (𝑧 ∈ ℝ+𝑤𝐴)) → (((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢) → ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦)))
4746anassrs 677 . . . . . . . . 9 ((((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤𝐴) → (((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢) → ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦)))
4847ralimdva 2940 . . . . . . . 8 (((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦)) ∧ 𝑧 ∈ ℝ+) → (∀𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢) → ∀𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦)))
4948reximdva 2995 . . . . . . 7 ((((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦)) → (∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦)))
5049ex 448 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) → (∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦) → (∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘((𝐹𝑤) − (𝐹𝑥))) < 𝑢) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦))))
5120, 50mpid 42 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+) → (∀𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦)))
5251rexlimdva 3008 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) → (∃𝑢 ∈ ℝ+𝑣𝐵 ((abs‘(𝑣 − (𝐹𝑥))) < 𝑢 → (abs‘((𝐺𝑣) − (𝐺‘(𝐹𝑥)))) < 𝑦) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦)))
5315, 52mpd 15 . . 3 ((𝜑 ∧ (𝑥𝐴𝑦 ∈ ℝ+)) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦))
5453ralrimivva 2949 . 2 (𝜑 → ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦))
55 cncfrss 22429 . . . 4 (𝐹 ∈ (𝐴cn𝐵) → 𝐴 ⊆ ℂ)
564, 55syl 17 . . 3 (𝜑𝐴 ⊆ ℂ)
57 cncfrss2 22430 . . . 4 (𝐺 ∈ (𝐵cn𝐶) → 𝐶 ⊆ ℂ)
581, 57syl 17 . . 3 (𝜑𝐶 ⊆ ℂ)
59 elcncf2 22428 . . 3 ((𝐴 ⊆ ℂ ∧ 𝐶 ⊆ ℂ) → ((𝐺𝐹) ∈ (𝐴cn𝐶) ↔ ((𝐺𝐹):𝐴𝐶 ∧ ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦))))
6056, 58, 59syl2anc 690 . 2 (𝜑 → ((𝐺𝐹) ∈ (𝐴cn𝐶) ↔ ((𝐺𝐹):𝐴𝐶 ∧ ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((abs‘(𝑤𝑥)) < 𝑧 → (abs‘(((𝐺𝐹)‘𝑤) − ((𝐺𝐹)‘𝑥))) < 𝑦))))
618, 54, 60mpbir2and 958 1 (𝜑 → (𝐺𝐹) ∈ (𝐴cn𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1975  wral 2891  wrex 2892  wss 3535   class class class wbr 4573  ccom 5028  wf 5782  cfv 5786  (class class class)co 6523  cc 9786   < clt 9926  cmin 10113  +crp 11660  abscabs 13764  cnccncf 22414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820  ax-cnex 9844  ax-resscn 9845  ax-1cn 9846  ax-icn 9847  ax-addcl 9848  ax-addrcl 9849  ax-mulcl 9850  ax-mulrcl 9851  ax-mulcom 9852  ax-addass 9853  ax-mulass 9854  ax-distr 9855  ax-i2m1 9856  ax-1ne0 9857  ax-1rid 9858  ax-rnegex 9859  ax-rrecex 9860  ax-cnre 9861  ax-pre-lttri 9862  ax-pre-lttrn 9863  ax-pre-ltadd 9864  ax-pre-mulgt0 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-nel 2778  df-ral 2896  df-rex 2897  df-reu 2898  df-rmo 2899  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-br 4574  df-opab 4634  df-mpt 4635  df-id 4939  df-po 4945  df-so 4946  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-riota 6485  df-ov 6526  df-oprab 6527  df-mpt2 6528  df-er 7602  df-map 7719  df-en 7815  df-dom 7816  df-sdom 7817  df-pnf 9928  df-mnf 9929  df-xr 9930  df-ltxr 9931  df-le 9932  df-sub 10115  df-neg 10116  df-div 10530  df-2 10922  df-cj 13629  df-re 13630  df-im 13631  df-abs 13766  df-cncf 22416
This theorem is referenced by:  cncfmpt1f  22451  negfcncf  22457  cniccbdd  22950  cncombf  23144  cnmbf  23145  dvlip  23473  dvlipcn  23474  itgsubstlem  23528  sincn  23915  coscn  23916  logcn  24106  lgamgulmlem2  24469  ftalem3  24514  evthiccabs  38365  mulc1cncfg  38456  expcnfg  38458  cncfcompt  38568  divcncf  38569  cncficcgt0  38574  cncfcompt2  38585  dirkercncflem2  38797  dirkercncflem4  38799  fourierdlem18  38818  fourierdlem93  38892  fourierdlem101  38900  fourierdlem111  38910
  Copyright terms: Public domain W3C validator