Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  itgexpif Structured version   Visualization version   GIF version

Theorem itgexpif 31196
Description: The basis for the circle method in the form of trigonometric sums. Proposition of [Nathanson] p. 123. (Contributed by Thierry Arnoux, 2-Dec-2021.)
Assertion
Ref Expression
itgexpif (𝑁 ∈ ℤ → ∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥 = if(𝑁 = 0, 1, 0))
Distinct variable group:   𝑥,𝑁

Proof of Theorem itgexpif
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 6883 . . . . . . . . . . 11 (𝑁 = 0 → (𝑁 · 𝑥) = (0 · 𝑥))
21oveq2d 6892 . . . . . . . . . 10 (𝑁 = 0 → ((i · (2 · π)) · (𝑁 · 𝑥)) = ((i · (2 · π)) · (0 · 𝑥)))
32fveq2d 6413 . . . . . . . . 9 (𝑁 = 0 → (exp‘((i · (2 · π)) · (𝑁 · 𝑥))) = (exp‘((i · (2 · π)) · (0 · 𝑥))))
4 ioossre 12480 . . . . . . . . . . . . . . . 16 (0(,)1) ⊆ ℝ
5 ax-resscn 10279 . . . . . . . . . . . . . . . 16 ℝ ⊆ ℂ
64, 5sstri 3805 . . . . . . . . . . . . . . 15 (0(,)1) ⊆ ℂ
76sseli 3792 . . . . . . . . . . . . . 14 (𝑥 ∈ (0(,)1) → 𝑥 ∈ ℂ)
87mul02d 10522 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)1) → (0 · 𝑥) = 0)
98oveq2d 6892 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)1) → ((i · (2 · π)) · (0 · 𝑥)) = ((i · (2 · π)) · 0))
10 ax-icn 10281 . . . . . . . . . . . . . 14 i ∈ ℂ
11 2cn 11384 . . . . . . . . . . . . . . 15 2 ∈ ℂ
12 picn 24550 . . . . . . . . . . . . . . 15 π ∈ ℂ
1311, 12mulcli 10334 . . . . . . . . . . . . . 14 (2 · π) ∈ ℂ
1410, 13mulcli 10334 . . . . . . . . . . . . 13 (i · (2 · π)) ∈ ℂ
1514mul01i 10514 . . . . . . . . . . . 12 ((i · (2 · π)) · 0) = 0
169, 15syl6eq 2847 . . . . . . . . . . 11 (𝑥 ∈ (0(,)1) → ((i · (2 · π)) · (0 · 𝑥)) = 0)
1716fveq2d 6413 . . . . . . . . . 10 (𝑥 ∈ (0(,)1) → (exp‘((i · (2 · π)) · (0 · 𝑥))) = (exp‘0))
18 ef0 15154 . . . . . . . . . 10 (exp‘0) = 1
1917, 18syl6eq 2847 . . . . . . . . 9 (𝑥 ∈ (0(,)1) → (exp‘((i · (2 · π)) · (0 · 𝑥))) = 1)
203, 19sylan9eq 2851 . . . . . . . 8 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)1)) → (exp‘((i · (2 · π)) · (𝑁 · 𝑥))) = 1)
2120ralrimiva 3145 . . . . . . 7 (𝑁 = 0 → ∀𝑥 ∈ (0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) = 1)
22 itgeq2 23882 . . . . . . 7 (∀𝑥 ∈ (0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) = 1 → ∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥 = ∫(0(,)1)1 d𝑥)
2321, 22syl 17 . . . . . 6 (𝑁 = 0 → ∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥 = ∫(0(,)1)1 d𝑥)
24 ioombl 23670 . . . . . . . 8 (0(,)1) ∈ dom vol
25 0re 10328 . . . . . . . . 9 0 ∈ ℝ
26 1re 10326 . . . . . . . . 9 1 ∈ ℝ
27 ioovolcl 23675 . . . . . . . . 9 ((0 ∈ ℝ ∧ 1 ∈ ℝ) → (vol‘(0(,)1)) ∈ ℝ)
2825, 26, 27mp2an 684 . . . . . . . 8 (vol‘(0(,)1)) ∈ ℝ
29 ax-1cn 10280 . . . . . . . 8 1 ∈ ℂ
30 itgconst 23923 . . . . . . . 8 (((0(,)1) ∈ dom vol ∧ (vol‘(0(,)1)) ∈ ℝ ∧ 1 ∈ ℂ) → ∫(0(,)1)1 d𝑥 = (1 · (vol‘(0(,)1))))
3124, 28, 29, 30mp3an 1586 . . . . . . 7 ∫(0(,)1)1 d𝑥 = (1 · (vol‘(0(,)1)))
32 0le1 10841 . . . . . . . . . 10 0 ≤ 1
33 volioo 23674 . . . . . . . . . 10 ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ≤ 1) → (vol‘(0(,)1)) = (1 − 0))
3425, 26, 32, 33mp3an 1586 . . . . . . . . 9 (vol‘(0(,)1)) = (1 − 0)
3529subid1i 10643 . . . . . . . . 9 (1 − 0) = 1
3634, 35eqtri 2819 . . . . . . . 8 (vol‘(0(,)1)) = 1
3736oveq2i 6887 . . . . . . 7 (1 · (vol‘(0(,)1))) = (1 · 1)
3829mulid1i 10331 . . . . . . 7 (1 · 1) = 1
3931, 37, 383eqtri 2823 . . . . . 6 ∫(0(,)1)1 d𝑥 = 1
4023, 39syl6eq 2847 . . . . 5 (𝑁 = 0 → ∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥 = 1)
4140adantl 474 . . . 4 ((𝑁 ∈ ℤ ∧ 𝑁 = 0) → ∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥 = 1)
4241eqcomd 2803 . . 3 ((𝑁 ∈ ℤ ∧ 𝑁 = 0) → 1 = ∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥)
43 ioomax 12493 . . . . . . 7 (-∞(,)+∞) = ℝ
4443eqcomi 2806 . . . . . 6 ℝ = (-∞(,)+∞)
45 0red 10330 . . . . . 6 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → 0 ∈ ℝ)
46 1red 10327 . . . . . 6 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → 1 ∈ ℝ)
4732a1i 11 . . . . . 6 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → 0 ≤ 1)
485a1i 11 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ℝ ⊆ ℂ)
4948sselda 3796 . . . . . . . . 9 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
5010a1i 11 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → i ∈ ℂ)
51 2cnd 11387 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → 2 ∈ ℂ)
5212a1i 11 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → π ∈ ℂ)
5351, 52mulcld 10347 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (2 · π) ∈ ℂ)
5450, 53mulcld 10347 . . . . . . . . . . . . 13 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (i · (2 · π)) ∈ ℂ)
55 simpl 475 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → 𝑁 ∈ ℤ)
5655zcnd 11769 . . . . . . . . . . . . 13 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → 𝑁 ∈ ℂ)
5754, 56mulcld 10347 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ((i · (2 · π)) · 𝑁) ∈ ℂ)
5857adantr 473 . . . . . . . . . . 11 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 ∈ ℂ) → ((i · (2 · π)) · 𝑁) ∈ ℂ)
59 simpr 478 . . . . . . . . . . 11 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
6058, 59mulcld 10347 . . . . . . . . . 10 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 ∈ ℂ) → (((i · (2 · π)) · 𝑁) · 𝑦) ∈ ℂ)
6160efcld 31181 . . . . . . . . 9 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 ∈ ℂ) → (exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) ∈ ℂ)
6249, 61syldan 586 . . . . . . . 8 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 ∈ ℝ) → (exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) ∈ ℂ)
6357adantr 473 . . . . . . . 8 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 ∈ ℝ) → ((i · (2 · π)) · 𝑁) ∈ ℂ)
64 ine0 10755 . . . . . . . . . . . 12 i ≠ 0
65 2ne0 11420 . . . . . . . . . . . . 13 2 ≠ 0
66 pipos 24551 . . . . . . . . . . . . . 14 0 < π
6725, 66gtneii 10437 . . . . . . . . . . . . 13 π ≠ 0
6811, 12, 65, 67mulne0i 10960 . . . . . . . . . . . 12 (2 · π) ≠ 0
6910, 13, 64, 68mulne0i 10960 . . . . . . . . . . 11 (i · (2 · π)) ≠ 0
7069a1i 11 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (i · (2 · π)) ≠ 0)
71 simpr 478 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ¬ 𝑁 = 0)
7271neqned 2976 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → 𝑁 ≠ 0)
7354, 56, 70, 72mulne0d 10969 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ((i · (2 · π)) · 𝑁) ≠ 0)
7473adantr 473 . . . . . . . 8 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 ∈ ℝ) → ((i · (2 · π)) · 𝑁) ≠ 0)
7562, 63, 74divcld 11091 . . . . . . 7 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 ∈ ℝ) → ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)) ∈ ℂ)
7675fmpttd 6609 . . . . . 6 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁))):ℝ⟶ℂ)
77 reelprrecn 10314 . . . . . . . . . 10 ℝ ∈ {ℝ, ℂ}
7877a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ℝ ∈ {ℝ, ℂ})
79 cnelprrecn 10315 . . . . . . . . . 10 ℂ ∈ {ℝ, ℂ}
8079a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ℂ ∈ {ℝ, ℂ})
8163, 49mulcld 10347 . . . . . . . . 9 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 ∈ ℝ) → (((i · (2 · π)) · 𝑁) · 𝑦) ∈ ℂ)
82 simpr 478 . . . . . . . . . . 11 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ)
8382efcld 31181 . . . . . . . . . 10 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑧 ∈ ℂ) → (exp‘𝑧) ∈ ℂ)
8457adantr 473 . . . . . . . . . 10 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑧 ∈ ℂ) → ((i · (2 · π)) · 𝑁) ∈ ℂ)
8573adantr 473 . . . . . . . . . 10 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑧 ∈ ℂ) → ((i · (2 · π)) · 𝑁) ≠ 0)
8683, 84, 85divcld 11091 . . . . . . . . 9 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑧 ∈ ℂ) → ((exp‘𝑧) / ((i · (2 · π)) · 𝑁)) ∈ ℂ)
8726a1i 11 . . . . . . . . . . 11 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 ∈ ℝ) → 1 ∈ ℝ)
8878dvmptid 24058 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1))
8978, 49, 87, 88, 57dvmptcmul 24065 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (ℝ D (𝑦 ∈ ℝ ↦ (((i · (2 · π)) · 𝑁) · 𝑦))) = (𝑦 ∈ ℝ ↦ (((i · (2 · π)) · 𝑁) · 1)))
9063mulid1d 10344 . . . . . . . . . . 11 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 ∈ ℝ) → (((i · (2 · π)) · 𝑁) · 1) = ((i · (2 · π)) · 𝑁))
9190mpteq2dva 4935 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (𝑦 ∈ ℝ ↦ (((i · (2 · π)) · 𝑁) · 1)) = (𝑦 ∈ ℝ ↦ ((i · (2 · π)) · 𝑁)))
9289, 91eqtrd 2831 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (ℝ D (𝑦 ∈ ℝ ↦ (((i · (2 · π)) · 𝑁) · 𝑦))) = (𝑦 ∈ ℝ ↦ ((i · (2 · π)) · 𝑁)))
93 dvef 24081 . . . . . . . . . . 11 (ℂ D exp) = exp
94 eff 15145 . . . . . . . . . . . . . 14 exp:ℂ⟶ℂ
9594a1i 11 . . . . . . . . . . . . 13 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → exp:ℂ⟶ℂ)
9695feqmptd 6472 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → exp = (𝑧 ∈ ℂ ↦ (exp‘𝑧)))
9796oveq2d 6892 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (ℂ D exp) = (ℂ D (𝑧 ∈ ℂ ↦ (exp‘𝑧))))
9893, 97, 963eqtr3a 2855 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (ℂ D (𝑧 ∈ ℂ ↦ (exp‘𝑧))) = (𝑧 ∈ ℂ ↦ (exp‘𝑧)))
9980, 83, 83, 98, 57, 73dvmptdivc 24066 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (ℂ D (𝑧 ∈ ℂ ↦ ((exp‘𝑧) / ((i · (2 · π)) · 𝑁)))) = (𝑧 ∈ ℂ ↦ ((exp‘𝑧) / ((i · (2 · π)) · 𝑁))))
100 fveq2 6409 . . . . . . . . . 10 (𝑧 = (((i · (2 · π)) · 𝑁) · 𝑦) → (exp‘𝑧) = (exp‘(((i · (2 · π)) · 𝑁) · 𝑦)))
101100oveq1d 6891 . . . . . . . . 9 (𝑧 = (((i · (2 · π)) · 𝑁) · 𝑦) → ((exp‘𝑧) / ((i · (2 · π)) · 𝑁)) = ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)))
10278, 80, 81, 63, 86, 86, 92, 99, 101, 101dvmptco 24073 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (ℝ D (𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)))) = (𝑦 ∈ ℝ ↦ (((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)) · ((i · (2 · π)) · 𝑁))))
10362, 63, 74divcan1d 11092 . . . . . . . . 9 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 ∈ ℝ) → (((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)) · ((i · (2 · π)) · 𝑁)) = (exp‘(((i · (2 · π)) · 𝑁) · 𝑦)))
104103mpteq2dva 4935 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (𝑦 ∈ ℝ ↦ (((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)) · ((i · (2 · π)) · 𝑁))) = (𝑦 ∈ ℝ ↦ (exp‘(((i · (2 · π)) · 𝑁) · 𝑦))))
105102, 104eqtrd 2831 . . . . . . 7 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (ℝ D (𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)))) = (𝑦 ∈ ℝ ↦ (exp‘(((i · (2 · π)) · 𝑁) · 𝑦))))
106 efcn 24535 . . . . . . . . 9 exp ∈ (ℂ–cn→ℂ)
107106a1i 11 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → exp ∈ (ℂ–cn→ℂ))
108 resmpt 5659 . . . . . . . . . 10 (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ (((i · (2 · π)) · 𝑁) · 𝑦)) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (((i · (2 · π)) · 𝑁) · 𝑦)))
1095, 108mp1i 13 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ((𝑦 ∈ ℂ ↦ (((i · (2 · π)) · 𝑁) · 𝑦)) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (((i · (2 · π)) · 𝑁) · 𝑦)))
110 eqid 2797 . . . . . . . . . . . 12 (𝑦 ∈ ℂ ↦ (((i · (2 · π)) · 𝑁) · 𝑦)) = (𝑦 ∈ ℂ ↦ (((i · (2 · π)) · 𝑁) · 𝑦))
111110mulc1cncf 23033 . . . . . . . . . . 11 (((i · (2 · π)) · 𝑁) ∈ ℂ → (𝑦 ∈ ℂ ↦ (((i · (2 · π)) · 𝑁) · 𝑦)) ∈ (ℂ–cn→ℂ))
11257, 111syl 17 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (𝑦 ∈ ℂ ↦ (((i · (2 · π)) · 𝑁) · 𝑦)) ∈ (ℂ–cn→ℂ))
113 rescncf 23025 . . . . . . . . . . 11 (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ (((i · (2 · π)) · 𝑁) · 𝑦)) ∈ (ℂ–cn→ℂ) → ((𝑦 ∈ ℂ ↦ (((i · (2 · π)) · 𝑁) · 𝑦)) ↾ ℝ) ∈ (ℝ–cn→ℂ)))
1145, 113mp1i 13 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ((𝑦 ∈ ℂ ↦ (((i · (2 · π)) · 𝑁) · 𝑦)) ∈ (ℂ–cn→ℂ) → ((𝑦 ∈ ℂ ↦ (((i · (2 · π)) · 𝑁) · 𝑦)) ↾ ℝ) ∈ (ℝ–cn→ℂ)))
115112, 114mpd 15 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ((𝑦 ∈ ℂ ↦ (((i · (2 · π)) · 𝑁) · 𝑦)) ↾ ℝ) ∈ (ℝ–cn→ℂ))
116109, 115eqeltrrd 2877 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (𝑦 ∈ ℝ ↦ (((i · (2 · π)) · 𝑁) · 𝑦)) ∈ (ℝ–cn→ℂ))
117107, 116cncfmpt1f 23041 . . . . . . 7 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (𝑦 ∈ ℝ ↦ (exp‘(((i · (2 · π)) · 𝑁) · 𝑦))) ∈ (ℝ–cn→ℂ))
118105, 117eqeltrd 2876 . . . . . 6 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (ℝ D (𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)))) ∈ (ℝ–cn→ℂ))
11944, 45, 46, 47, 76, 118ftc2re 31188 . . . . 5 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ∫(0(,)1)((ℝ D (𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁))))‘𝑥) d𝑥 = (((𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)))‘1) − ((𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)))‘0)))
1204sseli 3792 . . . . . . . 8 (𝑥 ∈ (0(,)1) → 𝑥 ∈ ℝ)
121105adantr 473 . . . . . . . . . 10 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑥 ∈ ℝ) → (ℝ D (𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)))) = (𝑦 ∈ ℝ ↦ (exp‘(((i · (2 · π)) · 𝑁) · 𝑦))))
122121fveq1d 6411 . . . . . . . . 9 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑥 ∈ ℝ) → ((ℝ D (𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁))))‘𝑥) = ((𝑦 ∈ ℝ ↦ (exp‘(((i · (2 · π)) · 𝑁) · 𝑦)))‘𝑥))
123 oveq2 6884 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (((i · (2 · π)) · 𝑁) · 𝑦) = (((i · (2 · π)) · 𝑁) · 𝑥))
124123fveq2d 6413 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → (exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) = (exp‘(((i · (2 · π)) · 𝑁) · 𝑥)))
125124cbvmptv 4941 . . . . . . . . . . . 12 (𝑦 ∈ ℝ ↦ (exp‘(((i · (2 · π)) · 𝑁) · 𝑦))) = (𝑥 ∈ ℝ ↦ (exp‘(((i · (2 · π)) · 𝑁) · 𝑥)))
126125a1i 11 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (𝑦 ∈ ℝ ↦ (exp‘(((i · (2 · π)) · 𝑁) · 𝑦))) = (𝑥 ∈ ℝ ↦ (exp‘(((i · (2 · π)) · 𝑁) · 𝑥))))
12757adantr 473 . . . . . . . . . . . . 13 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑥 ∈ ℝ) → ((i · (2 · π)) · 𝑁) ∈ ℂ)
12848sselda 3796 . . . . . . . . . . . . 13 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
129127, 128mulcld 10347 . . . . . . . . . . . 12 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑥 ∈ ℝ) → (((i · (2 · π)) · 𝑁) · 𝑥) ∈ ℂ)
130129efcld 31181 . . . . . . . . . . 11 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑥 ∈ ℝ) → (exp‘(((i · (2 · π)) · 𝑁) · 𝑥)) ∈ ℂ)
131126, 130fvmpt2d 6516 . . . . . . . . . 10 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑥 ∈ ℝ) → ((𝑦 ∈ ℝ ↦ (exp‘(((i · (2 · π)) · 𝑁) · 𝑦)))‘𝑥) = (exp‘(((i · (2 · π)) · 𝑁) · 𝑥)))
13214a1i 11 . . . . . . . . . . . 12 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑥 ∈ ℝ) → (i · (2 · π)) ∈ ℂ)
13356adantr 473 . . . . . . . . . . . 12 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑥 ∈ ℝ) → 𝑁 ∈ ℂ)
134132, 133, 128mulassd 10350 . . . . . . . . . . 11 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑥 ∈ ℝ) → (((i · (2 · π)) · 𝑁) · 𝑥) = ((i · (2 · π)) · (𝑁 · 𝑥)))
135134fveq2d 6413 . . . . . . . . . 10 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑥 ∈ ℝ) → (exp‘(((i · (2 · π)) · 𝑁) · 𝑥)) = (exp‘((i · (2 · π)) · (𝑁 · 𝑥))))
136131, 135eqtrd 2831 . . . . . . . . 9 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑥 ∈ ℝ) → ((𝑦 ∈ ℝ ↦ (exp‘(((i · (2 · π)) · 𝑁) · 𝑦)))‘𝑥) = (exp‘((i · (2 · π)) · (𝑁 · 𝑥))))
137122, 136eqtrd 2831 . . . . . . . 8 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑥 ∈ ℝ) → ((ℝ D (𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁))))‘𝑥) = (exp‘((i · (2 · π)) · (𝑁 · 𝑥))))
138120, 137sylan2 587 . . . . . . 7 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑥 ∈ (0(,)1)) → ((ℝ D (𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁))))‘𝑥) = (exp‘((i · (2 · π)) · (𝑁 · 𝑥))))
139138ralrimiva 3145 . . . . . 6 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ∀𝑥 ∈ (0(,)1)((ℝ D (𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁))))‘𝑥) = (exp‘((i · (2 · π)) · (𝑁 · 𝑥))))
140 itgeq2 23882 . . . . . 6 (∀𝑥 ∈ (0(,)1)((ℝ D (𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁))))‘𝑥) = (exp‘((i · (2 · π)) · (𝑁 · 𝑥))) → ∫(0(,)1)((ℝ D (𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁))))‘𝑥) d𝑥 = ∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥)
141139, 140syl 17 . . . . 5 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ∫(0(,)1)((ℝ D (𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁))))‘𝑥) d𝑥 = ∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥)
142 eqidd 2798 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁))) = (𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁))))
143 simpr 478 . . . . . . . . . . . 12 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 = 1) → 𝑦 = 1)
144143oveq2d 6892 . . . . . . . . . . 11 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 = 1) → (((i · (2 · π)) · 𝑁) · 𝑦) = (((i · (2 · π)) · 𝑁) · 1))
145144fveq2d 6413 . . . . . . . . . 10 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 = 1) → (exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) = (exp‘(((i · (2 · π)) · 𝑁) · 1)))
146145oveq1d 6891 . . . . . . . . 9 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 = 1) → ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)) = ((exp‘(((i · (2 · π)) · 𝑁) · 1)) / ((i · (2 · π)) · 𝑁)))
14729a1i 11 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → 1 ∈ ℂ)
14857, 147mulcld 10347 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (((i · (2 · π)) · 𝑁) · 1) ∈ ℂ)
149148efcld 31181 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (exp‘(((i · (2 · π)) · 𝑁) · 1)) ∈ ℂ)
150149, 57, 73divcld 11091 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ((exp‘(((i · (2 · π)) · 𝑁) · 1)) / ((i · (2 · π)) · 𝑁)) ∈ ℂ)
151142, 146, 46, 150fvmptd 6511 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ((𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)))‘1) = ((exp‘(((i · (2 · π)) · 𝑁) · 1)) / ((i · (2 · π)) · 𝑁)))
15257mulid1d 10344 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (((i · (2 · π)) · 𝑁) · 1) = ((i · (2 · π)) · 𝑁))
153152fveq2d 6413 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (exp‘(((i · (2 · π)) · 𝑁) · 1)) = (exp‘((i · (2 · π)) · 𝑁)))
154 ef2kpi 24569 . . . . . . . . . . 11 (𝑁 ∈ ℤ → (exp‘((i · (2 · π)) · 𝑁)) = 1)
15555, 154syl 17 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (exp‘((i · (2 · π)) · 𝑁)) = 1)
156153, 155eqtrd 2831 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (exp‘(((i · (2 · π)) · 𝑁) · 1)) = 1)
157156oveq1d 6891 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ((exp‘(((i · (2 · π)) · 𝑁) · 1)) / ((i · (2 · π)) · 𝑁)) = (1 / ((i · (2 · π)) · 𝑁)))
158151, 157eqtrd 2831 . . . . . . 7 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ((𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)))‘1) = (1 / ((i · (2 · π)) · 𝑁)))
159 simpr 478 . . . . . . . . . . . 12 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 = 0) → 𝑦 = 0)
160159oveq2d 6892 . . . . . . . . . . 11 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 = 0) → (((i · (2 · π)) · 𝑁) · 𝑦) = (((i · (2 · π)) · 𝑁) · 0))
161160fveq2d 6413 . . . . . . . . . 10 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 = 0) → (exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) = (exp‘(((i · (2 · π)) · 𝑁) · 0)))
162161oveq1d 6891 . . . . . . . . 9 (((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) ∧ 𝑦 = 0) → ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)) = ((exp‘(((i · (2 · π)) · 𝑁) · 0)) / ((i · (2 · π)) · 𝑁)))
1635, 45sseldi 3794 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → 0 ∈ ℂ)
16457, 163mulcld 10347 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (((i · (2 · π)) · 𝑁) · 0) ∈ ℂ)
165164efcld 31181 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (exp‘(((i · (2 · π)) · 𝑁) · 0)) ∈ ℂ)
166165, 57, 73divcld 11091 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ((exp‘(((i · (2 · π)) · 𝑁) · 0)) / ((i · (2 · π)) · 𝑁)) ∈ ℂ)
167142, 162, 45, 166fvmptd 6511 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ((𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)))‘0) = ((exp‘(((i · (2 · π)) · 𝑁) · 0)) / ((i · (2 · π)) · 𝑁)))
16857mul01d 10523 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (((i · (2 · π)) · 𝑁) · 0) = 0)
169168fveq2d 6413 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (exp‘(((i · (2 · π)) · 𝑁) · 0)) = (exp‘0))
170169, 18syl6eq 2847 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (exp‘(((i · (2 · π)) · 𝑁) · 0)) = 1)
171170oveq1d 6891 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ((exp‘(((i · (2 · π)) · 𝑁) · 0)) / ((i · (2 · π)) · 𝑁)) = (1 / ((i · (2 · π)) · 𝑁)))
172167, 171eqtrd 2831 . . . . . . 7 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ((𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)))‘0) = (1 / ((i · (2 · π)) · 𝑁)))
173158, 172oveq12d 6894 . . . . . 6 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (((𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)))‘1) − ((𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)))‘0)) = ((1 / ((i · (2 · π)) · 𝑁)) − (1 / ((i · (2 · π)) · 𝑁))))
174157, 150eqeltrrd 2877 . . . . . . 7 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (1 / ((i · (2 · π)) · 𝑁)) ∈ ℂ)
175174subidd 10670 . . . . . 6 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ((1 / ((i · (2 · π)) · 𝑁)) − (1 / ((i · (2 · π)) · 𝑁))) = 0)
176173, 175eqtrd 2831 . . . . 5 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → (((𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)))‘1) − ((𝑦 ∈ ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) · 𝑁)))‘0)) = 0)
177119, 141, 1763eqtr3d 2839 . . . 4 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → ∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥 = 0)
178177eqcomd 2803 . . 3 ((𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0) → 0 = ∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥)
17942, 178ifeqda 4310 . 2 (𝑁 ∈ ℤ → if(𝑁 = 0, 1, 0) = ∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥)
180179eqcomd 2803 1 (𝑁 ∈ ℤ → ∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥 = if(𝑁 = 0, 1, 0))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 385   = wceq 1653  wcel 2157  wne 2969  wral 3087  wss 3767  ifcif 4275  {cpr 4368   class class class wbr 4841  cmpt 4920  dom cdm 5310  cres 5312  wf 6095  cfv 6099  (class class class)co 6876  cc 10220  cr 10221  0cc0 10222  1c1 10223  ici 10224   · cmul 10227  +∞cpnf 10358  -∞cmnf 10359  cle 10362  cmin 10554   / cdiv 10974  2c2 11364  cz 11662  (,)cioo 12420  expce 15125  πcpi 15130  cnccncf 23004  volcvol 23568  citg 23723   D cdv 23965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-ext 2775  ax-rep 4962  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5095  ax-un 7181  ax-inf2 8786  ax-cc 9543  ax-cnex 10278  ax-resscn 10279  ax-1cn 10280  ax-icn 10281  ax-addcl 10282  ax-addrcl 10283  ax-mulcl 10284  ax-mulrcl 10285  ax-mulcom 10286  ax-addass 10287  ax-mulass 10288  ax-distr 10289  ax-i2m1 10290  ax-1ne0 10291  ax-1rid 10292  ax-rnegex 10293  ax-rrecex 10294  ax-cnre 10295  ax-pre-lttri 10296  ax-pre-lttrn 10297  ax-pre-ltadd 10298  ax-pre-mulgt0 10299  ax-pre-sup 10300  ax-addf 10301  ax-mulf 10302
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-fal 1667  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2590  df-eu 2607  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ne 2970  df-nel 3073  df-ral 3092  df-rex 3093  df-reu 3094  df-rmo 3095  df-rab 3096  df-v 3385  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-pss 3783  df-symdif 4039  df-nul 4114  df-if 4276  df-pw 4349  df-sn 4367  df-pr 4369  df-tp 4371  df-op 4373  df-uni 4627  df-int 4666  df-iun 4710  df-iin 4711  df-disj 4810  df-br 4842  df-opab 4904  df-mpt 4921  df-tr 4944  df-id 5218  df-eprel 5223  df-po 5231  df-so 5232  df-fr 5269  df-se 5270  df-we 5271  df-xp 5316  df-rel 5317  df-cnv 5318  df-co 5319  df-dm 5320  df-rn 5321  df-res 5322  df-ima 5323  df-pred 5896  df-ord 5942  df-on 5943  df-lim 5944  df-suc 5945  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-f1 6104  df-fo 6105  df-f1o 6106  df-fv 6107  df-isom 6108  df-riota 6837  df-ov 6879  df-oprab 6880  df-mpt2 6881  df-of 7129  df-ofr 7130  df-om 7298  df-1st 7399  df-2nd 7400  df-supp 7531  df-wrecs 7643  df-recs 7705  df-rdg 7743  df-1o 7797  df-2o 7798  df-oadd 7801  df-omul 7802  df-er 7980  df-map 8095  df-pm 8096  df-ixp 8147  df-en 8194  df-dom 8195  df-sdom 8196  df-fin 8197  df-fsupp 8516  df-fi 8557  df-sup 8588  df-inf 8589  df-oi 8655  df-card 9049  df-acn 9052  df-cda 9276  df-pnf 10363  df-mnf 10364  df-xr 10365  df-ltxr 10366  df-le 10367  df-sub 10556  df-neg 10557  df-div 10975  df-nn 11311  df-2 11372  df-3 11373  df-4 11374  df-5 11375  df-6 11376  df-7 11377  df-8 11378  df-9 11379  df-n0 11577  df-z 11663  df-dec 11780  df-uz 11927  df-q 12030  df-rp 12071  df-xneg 12189  df-xadd 12190  df-xmul 12191  df-ioo 12424  df-ioc 12425  df-ico 12426  df-icc 12427  df-fz 12577  df-fzo 12717  df-fl 12844  df-mod 12920  df-seq 13052  df-exp 13111  df-fac 13310  df-bc 13339  df-hash 13367  df-shft 14145  df-cj 14177  df-re 14178  df-im 14179  df-sqrt 14313  df-abs 14314  df-limsup 14540  df-clim 14557  df-rlim 14558  df-sum 14755  df-ef 15131  df-sin 15133  df-cos 15134  df-pi 15136  df-struct 16183  df-ndx 16184  df-slot 16185  df-base 16187  df-sets 16188  df-ress 16189  df-plusg 16277  df-mulr 16278  df-starv 16279  df-sca 16280  df-vsca 16281  df-ip 16282  df-tset 16283  df-ple 16284  df-ds 16286  df-unif 16287  df-hom 16288  df-cco 16289  df-rest 16395  df-topn 16396  df-0g 16414  df-gsum 16415  df-topgen 16416  df-pt 16417  df-prds 16420  df-xrs 16474  df-qtop 16479  df-imas 16480  df-xps 16482  df-mre 16558  df-mrc 16559  df-acs 16561  df-mgm 17554  df-sgrp 17596  df-mnd 17607  df-submnd 17648  df-mulg 17854  df-cntz 18059  df-cmn 18507  df-psmet 20057  df-xmet 20058  df-met 20059  df-bl 20060  df-mopn 20061  df-fbas 20062  df-fg 20063  df-cnfld 20066  df-top 21024  df-topon 21041  df-topsp 21063  df-bases 21076  df-cld 21149  df-ntr 21150  df-cls 21151  df-nei 21228  df-lp 21266  df-perf 21267  df-cn 21357  df-cnp 21358  df-haus 21445  df-cmp 21516  df-tx 21691  df-hmeo 21884  df-fil 21975  df-fm 22067  df-flim 22068  df-flf 22069  df-xms 22450  df-ms 22451  df-tms 22452  df-cncf 23006  df-ovol 23569  df-vol 23570  df-mbf 23724  df-itg1 23725  df-itg2 23726  df-ibl 23727  df-itg 23728  df-0p 23775  df-limc 23968  df-dv 23969
This theorem is referenced by:  circlemeth  31230
  Copyright terms: Public domain W3C validator