Proof of Theorem efif1olem4
Step | Hyp | Ref
| Expression |
1 | | efif1olem4.3 |
. . . . . 6
⊢ (𝜑 → 𝐷 ⊆ ℝ) |
2 | 1 | sselda 3568 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → 𝑤 ∈ ℝ) |
3 | | ax-icn 9874 |
. . . . . . . . 9
⊢ i ∈
ℂ |
4 | | recn 9905 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℝ → 𝑤 ∈
ℂ) |
5 | | mulcl 9899 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝑤
∈ ℂ) → (i · 𝑤) ∈ ℂ) |
6 | 3, 4, 5 | sylancr 694 |
. . . . . . . 8
⊢ (𝑤 ∈ ℝ → (i
· 𝑤) ∈
ℂ) |
7 | | efcl 14652 |
. . . . . . . 8
⊢ ((i
· 𝑤) ∈ ℂ
→ (exp‘(i · 𝑤)) ∈ ℂ) |
8 | 6, 7 | syl 17 |
. . . . . . 7
⊢ (𝑤 ∈ ℝ →
(exp‘(i · 𝑤))
∈ ℂ) |
9 | | absefi 14765 |
. . . . . . 7
⊢ (𝑤 ∈ ℝ →
(abs‘(exp‘(i · 𝑤))) = 1) |
10 | | absf 13925 |
. . . . . . . . 9
⊢
abs:ℂ⟶ℝ |
11 | | ffn 5958 |
. . . . . . . . 9
⊢
(abs:ℂ⟶ℝ → abs Fn ℂ) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . 8
⊢ abs Fn
ℂ |
13 | | fniniseg 6246 |
. . . . . . . 8
⊢ (abs Fn
ℂ → ((exp‘(i · 𝑤)) ∈ (◡abs “ {1}) ↔ ((exp‘(i
· 𝑤)) ∈ ℂ
∧ (abs‘(exp‘(i · 𝑤))) = 1))) |
14 | 12, 13 | ax-mp 5 |
. . . . . . 7
⊢
((exp‘(i · 𝑤)) ∈ (◡abs “ {1}) ↔ ((exp‘(i
· 𝑤)) ∈ ℂ
∧ (abs‘(exp‘(i · 𝑤))) = 1)) |
15 | 8, 9, 14 | sylanbrc 695 |
. . . . . 6
⊢ (𝑤 ∈ ℝ →
(exp‘(i · 𝑤))
∈ (◡abs “
{1})) |
16 | | efif1o.2 |
. . . . . 6
⊢ 𝐶 = (◡abs “ {1}) |
17 | 15, 16 | syl6eleqr 2699 |
. . . . 5
⊢ (𝑤 ∈ ℝ →
(exp‘(i · 𝑤))
∈ 𝐶) |
18 | 2, 17 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐷) → (exp‘(i · 𝑤)) ∈ 𝐶) |
19 | | efif1o.1 |
. . . 4
⊢ 𝐹 = (𝑤 ∈ 𝐷 ↦ (exp‘(i · 𝑤))) |
20 | 18, 19 | fmptd 6292 |
. . 3
⊢ (𝜑 → 𝐹:𝐷⟶𝐶) |
21 | 1 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝐷 ⊆ ℝ) |
22 | | simplrl 796 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑥 ∈ 𝐷) |
23 | 21, 22 | sseldd 3569 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑥 ∈ ℝ) |
24 | 23 | recnd 9947 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑥 ∈ ℂ) |
25 | | simplrr 797 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑦 ∈ 𝐷) |
26 | 21, 25 | sseldd 3569 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑦 ∈ ℝ) |
27 | 26 | recnd 9947 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑦 ∈ ℂ) |
28 | 24, 27 | subcld 10271 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (𝑥 − 𝑦) ∈ ℂ) |
29 | | 2re 10967 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
30 | | pire 24014 |
. . . . . . . . . . . 12
⊢ π
∈ ℝ |
31 | 29, 30 | remulcli 9933 |
. . . . . . . . . . 11
⊢ (2
· π) ∈ ℝ |
32 | 31 | recni 9931 |
. . . . . . . . . 10
⊢ (2
· π) ∈ ℂ |
33 | | 2pos 10989 |
. . . . . . . . . . . 12
⊢ 0 <
2 |
34 | | pipos 24016 |
. . . . . . . . . . . 12
⊢ 0 <
π |
35 | 29, 30, 33, 34 | mulgt0ii 10049 |
. . . . . . . . . . 11
⊢ 0 < (2
· π) |
36 | 31, 35 | gt0ne0ii 10443 |
. . . . . . . . . 10
⊢ (2
· π) ≠ 0 |
37 | | divcl 10570 |
. . . . . . . . . 10
⊢ (((𝑥 − 𝑦) ∈ ℂ ∧ (2 · π)
∈ ℂ ∧ (2 · π) ≠ 0) → ((𝑥 − 𝑦) / (2 · π)) ∈
ℂ) |
38 | 32, 36, 37 | mp3an23 1408 |
. . . . . . . . 9
⊢ ((𝑥 − 𝑦) ∈ ℂ → ((𝑥 − 𝑦) / (2 · π)) ∈
ℂ) |
39 | 28, 38 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → ((𝑥 − 𝑦) / (2 · π)) ∈
ℂ) |
40 | | absdiv 13883 |
. . . . . . . . . . . . 13
⊢ (((𝑥 − 𝑦) ∈ ℂ ∧ (2 · π)
∈ ℂ ∧ (2 · π) ≠ 0) → (abs‘((𝑥 − 𝑦) / (2 · π))) = ((abs‘(𝑥 − 𝑦)) / (abs‘(2 ·
π)))) |
41 | 32, 36, 40 | mp3an23 1408 |
. . . . . . . . . . . 12
⊢ ((𝑥 − 𝑦) ∈ ℂ → (abs‘((𝑥 − 𝑦) / (2 · π))) = ((abs‘(𝑥 − 𝑦)) / (abs‘(2 ·
π)))) |
42 | 28, 41 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (abs‘((𝑥 − 𝑦) / (2 · π))) = ((abs‘(𝑥 − 𝑦)) / (abs‘(2 ·
π)))) |
43 | | 0re 9919 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
44 | 43, 31, 35 | ltleii 10039 |
. . . . . . . . . . . . 13
⊢ 0 ≤ (2
· π) |
45 | | absid 13884 |
. . . . . . . . . . . . 13
⊢ (((2
· π) ∈ ℝ ∧ 0 ≤ (2 · π)) →
(abs‘(2 · π)) = (2 · π)) |
46 | 31, 44, 45 | mp2an 704 |
. . . . . . . . . . . 12
⊢
(abs‘(2 · π)) = (2 · π) |
47 | 46 | oveq2i 6560 |
. . . . . . . . . . 11
⊢
((abs‘(𝑥
− 𝑦)) / (abs‘(2
· π))) = ((abs‘(𝑥 − 𝑦)) / (2 · π)) |
48 | 42, 47 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (abs‘((𝑥 − 𝑦) / (2 · π))) = ((abs‘(𝑥 − 𝑦)) / (2 · π))) |
49 | | efif1olem4.4 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → (abs‘(𝑥 − 𝑦)) < (2 · π)) |
50 | 49 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (abs‘(𝑥 − 𝑦)) < (2 · π)) |
51 | 32 | mulid1i 9921 |
. . . . . . . . . . . 12
⊢ ((2
· π) · 1) = (2 · π) |
52 | 50, 51 | syl6breqr 4625 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (abs‘(𝑥 − 𝑦)) < ((2 · π) ·
1)) |
53 | 28 | abscld 14023 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (abs‘(𝑥 − 𝑦)) ∈ ℝ) |
54 | | 1re 9918 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
55 | 31, 35 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ ((2
· π) ∈ ℝ ∧ 0 < (2 · π)) |
56 | | ltdivmul 10777 |
. . . . . . . . . . . . 13
⊢
(((abs‘(𝑥
− 𝑦)) ∈ ℝ
∧ 1 ∈ ℝ ∧ ((2 · π) ∈ ℝ ∧ 0 < (2
· π))) → (((abs‘(𝑥 − 𝑦)) / (2 · π)) < 1 ↔
(abs‘(𝑥 − 𝑦)) < ((2 · π)
· 1))) |
57 | 54, 55, 56 | mp3an23 1408 |
. . . . . . . . . . . 12
⊢
((abs‘(𝑥
− 𝑦)) ∈ ℝ
→ (((abs‘(𝑥
− 𝑦)) / (2 ·
π)) < 1 ↔ (abs‘(𝑥 − 𝑦)) < ((2 · π) ·
1))) |
58 | 53, 57 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (((abs‘(𝑥 − 𝑦)) / (2 · π)) < 1 ↔
(abs‘(𝑥 − 𝑦)) < ((2 · π)
· 1))) |
59 | 52, 58 | mpbird 246 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → ((abs‘(𝑥 − 𝑦)) / (2 · π)) <
1) |
60 | 48, 59 | eqbrtrd 4605 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (abs‘((𝑥 − 𝑦) / (2 · π))) <
1) |
61 | 32, 36 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ ((2
· π) ∈ ℂ ∧ (2 · π) ≠ 0) |
62 | | ine0 10344 |
. . . . . . . . . . . . . . 15
⊢ i ≠
0 |
63 | 3, 62 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (i ∈
ℂ ∧ i ≠ 0) |
64 | | divcan5 10606 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 − 𝑦) ∈ ℂ ∧ ((2 · π)
∈ ℂ ∧ (2 · π) ≠ 0) ∧ (i ∈ ℂ ∧ i
≠ 0)) → ((i · (𝑥 − 𝑦)) / (i · (2 · π))) =
((𝑥 − 𝑦) / (2 ·
π))) |
65 | 61, 63, 64 | mp3an23 1408 |
. . . . . . . . . . . . 13
⊢ ((𝑥 − 𝑦) ∈ ℂ → ((i · (𝑥 − 𝑦)) / (i · (2 · π))) =
((𝑥 − 𝑦) / (2 ·
π))) |
66 | 28, 65 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → ((i · (𝑥 − 𝑦)) / (i · (2 · π))) =
((𝑥 − 𝑦) / (2 ·
π))) |
67 | 3 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → i ∈ ℂ) |
68 | 67, 24, 27 | subdid 10365 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (i · (𝑥 − 𝑦)) = ((i · 𝑥) − (i · 𝑦))) |
69 | 68 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (exp‘(i · (𝑥 − 𝑦))) = (exp‘((i · 𝑥) − (i · 𝑦)))) |
70 | | mulcl 9899 |
. . . . . . . . . . . . . . . 16
⊢ ((i
∈ ℂ ∧ 𝑥
∈ ℂ) → (i · 𝑥) ∈ ℂ) |
71 | 3, 24, 70 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (i · 𝑥) ∈ ℂ) |
72 | | mulcl 9899 |
. . . . . . . . . . . . . . . 16
⊢ ((i
∈ ℂ ∧ 𝑦
∈ ℂ) → (i · 𝑦) ∈ ℂ) |
73 | 3, 27, 72 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (i · 𝑦) ∈ ℂ) |
74 | | efsub 14669 |
. . . . . . . . . . . . . . 15
⊢ (((i
· 𝑥) ∈ ℂ
∧ (i · 𝑦) ∈
ℂ) → (exp‘((i · 𝑥) − (i · 𝑦))) = ((exp‘(i · 𝑥)) / (exp‘(i ·
𝑦)))) |
75 | 71, 73, 74 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (exp‘((i · 𝑥) − (i · 𝑦))) = ((exp‘(i ·
𝑥)) / (exp‘(i
· 𝑦)))) |
76 | | efcl 14652 |
. . . . . . . . . . . . . . . 16
⊢ ((i
· 𝑦) ∈ ℂ
→ (exp‘(i · 𝑦)) ∈ ℂ) |
77 | 73, 76 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (exp‘(i · 𝑦)) ∈
ℂ) |
78 | | efne0 14666 |
. . . . . . . . . . . . . . . 16
⊢ ((i
· 𝑦) ∈ ℂ
→ (exp‘(i · 𝑦)) ≠ 0) |
79 | 73, 78 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (exp‘(i · 𝑦)) ≠ 0) |
80 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (𝐹‘𝑥) = (𝐹‘𝑦)) |
81 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑥 → (i · 𝑤) = (i · 𝑥)) |
82 | 81 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑥 → (exp‘(i · 𝑤)) = (exp‘(i ·
𝑥))) |
83 | | fvex 6113 |
. . . . . . . . . . . . . . . . . 18
⊢
(exp‘(i · 𝑥)) ∈ V |
84 | 82, 19, 83 | fvmpt 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝐷 → (𝐹‘𝑥) = (exp‘(i · 𝑥))) |
85 | 22, 84 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (𝐹‘𝑥) = (exp‘(i · 𝑥))) |
86 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑦 → (i · 𝑤) = (i · 𝑦)) |
87 | 86 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑦 → (exp‘(i · 𝑤)) = (exp‘(i ·
𝑦))) |
88 | | fvex 6113 |
. . . . . . . . . . . . . . . . . 18
⊢
(exp‘(i · 𝑦)) ∈ V |
89 | 87, 19, 88 | fvmpt 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝐷 → (𝐹‘𝑦) = (exp‘(i · 𝑦))) |
90 | 25, 89 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (𝐹‘𝑦) = (exp‘(i · 𝑦))) |
91 | 80, 85, 90 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (exp‘(i · 𝑥)) = (exp‘(i ·
𝑦))) |
92 | 77, 79, 91 | diveq1bd 10728 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → ((exp‘(i · 𝑥)) / (exp‘(i ·
𝑦))) = 1) |
93 | 69, 75, 92 | 3eqtrd 2648 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (exp‘(i · (𝑥 − 𝑦))) = 1) |
94 | | mulcl 9899 |
. . . . . . . . . . . . . . 15
⊢ ((i
∈ ℂ ∧ (𝑥
− 𝑦) ∈ ℂ)
→ (i · (𝑥
− 𝑦)) ∈
ℂ) |
95 | 3, 28, 94 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (i · (𝑥 − 𝑦)) ∈ ℂ) |
96 | | efeq1 24079 |
. . . . . . . . . . . . . 14
⊢ ((i
· (𝑥 − 𝑦)) ∈ ℂ →
((exp‘(i · (𝑥
− 𝑦))) = 1 ↔ ((i
· (𝑥 − 𝑦)) / (i · (2 ·
π))) ∈ ℤ)) |
97 | 95, 96 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → ((exp‘(i · (𝑥 − 𝑦))) = 1 ↔ ((i · (𝑥 − 𝑦)) / (i · (2 · π))) ∈
ℤ)) |
98 | 93, 97 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → ((i · (𝑥 − 𝑦)) / (i · (2 · π))) ∈
ℤ) |
99 | 66, 98 | eqeltrrd 2689 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → ((𝑥 − 𝑦) / (2 · π)) ∈
ℤ) |
100 | | nn0abscl 13900 |
. . . . . . . . . . 11
⊢ (((𝑥 − 𝑦) / (2 · π)) ∈ ℤ →
(abs‘((𝑥 −
𝑦) / (2 · π)))
∈ ℕ0) |
101 | 99, 100 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (abs‘((𝑥 − 𝑦) / (2 · π))) ∈
ℕ0) |
102 | | nn0lt10b 11316 |
. . . . . . . . . 10
⊢
((abs‘((𝑥
− 𝑦) / (2 ·
π))) ∈ ℕ0 → ((abs‘((𝑥 − 𝑦) / (2 · π))) < 1 ↔
(abs‘((𝑥 −
𝑦) / (2 · π))) =
0)) |
103 | 101, 102 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → ((abs‘((𝑥 − 𝑦) / (2 · π))) < 1 ↔
(abs‘((𝑥 −
𝑦) / (2 · π))) =
0)) |
104 | 60, 103 | mpbid 221 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (abs‘((𝑥 − 𝑦) / (2 · π))) = 0) |
105 | 39, 104 | abs00d 14033 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → ((𝑥 − 𝑦) / (2 · π)) = 0) |
106 | | diveq0 10574 |
. . . . . . . . 9
⊢ (((𝑥 − 𝑦) ∈ ℂ ∧ (2 · π)
∈ ℂ ∧ (2 · π) ≠ 0) → (((𝑥 − 𝑦) / (2 · π)) = 0 ↔ (𝑥 − 𝑦) = 0)) |
107 | 32, 36, 106 | mp3an23 1408 |
. . . . . . . 8
⊢ ((𝑥 − 𝑦) ∈ ℂ → (((𝑥 − 𝑦) / (2 · π)) = 0 ↔ (𝑥 − 𝑦) = 0)) |
108 | 28, 107 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (((𝑥 − 𝑦) / (2 · π)) = 0 ↔ (𝑥 − 𝑦) = 0)) |
109 | 105, 108 | mpbid 221 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (𝑥 − 𝑦) = 0) |
110 | 24, 27, 109 | subeq0d 10279 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑥 = 𝑦) |
111 | 110 | ex 449 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
112 | 111 | ralrimivva 2954 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
113 | | dff13 6416 |
. . 3
⊢ (𝐹:𝐷–1-1→𝐶 ↔ (𝐹:𝐷⟶𝐶 ∧ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
114 | 20, 112, 113 | sylanbrc 695 |
. 2
⊢ (𝜑 → 𝐹:𝐷–1-1→𝐶) |
115 | | neghalfpire 24021 |
. . . . . . . . 9
⊢ -(π /
2) ∈ ℝ |
116 | | halfpire 24020 |
. . . . . . . . 9
⊢ (π /
2) ∈ ℝ |
117 | | iccssre 12126 |
. . . . . . . . 9
⊢ ((-(π
/ 2) ∈ ℝ ∧ (π / 2) ∈ ℝ) → (-(π /
2)[,](π / 2)) ⊆ ℝ) |
118 | 115, 116,
117 | mp2an 704 |
. . . . . . . 8
⊢ (-(π /
2)[,](π / 2)) ⊆ ℝ |
119 | 19, 16 | efif1olem3 24094 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (ℑ‘(√‘𝑥)) ∈
(-1[,]1)) |
120 | | resinf1o 24086 |
. . . . . . . . . . . 12
⊢ (sin
↾ (-(π / 2)[,](π / 2))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) |
121 | | efif1olem4.6 |
. . . . . . . . . . . . 13
⊢ 𝑆 = (sin ↾ (-(π /
2)[,](π / 2))) |
122 | | f1oeq1 6040 |
. . . . . . . . . . . . 13
⊢ (𝑆 = (sin ↾ (-(π /
2)[,](π / 2))) → (𝑆:(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) ↔ (sin ↾ (-(π /
2)[,](π / 2))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1))) |
123 | 121, 122 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝑆:(-(π / 2)[,](π /
2))–1-1-onto→(-1[,]1) ↔ (sin ↾ (-(π /
2)[,](π / 2))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1)) |
124 | 120, 123 | mpbir 220 |
. . . . . . . . . . 11
⊢ 𝑆:(-(π / 2)[,](π /
2))–1-1-onto→(-1[,]1) |
125 | | f1ocnv 6062 |
. . . . . . . . . . 11
⊢ (𝑆:(-(π / 2)[,](π /
2))–1-1-onto→(-1[,]1) → ◡𝑆:(-1[,]1)–1-1-onto→(-(π / 2)[,](π / 2))) |
126 | | f1of 6050 |
. . . . . . . . . . 11
⊢ (◡𝑆:(-1[,]1)–1-1-onto→(-(π / 2)[,](π / 2)) → ◡𝑆:(-1[,]1)⟶(-(π / 2)[,](π /
2))) |
127 | 124, 125,
126 | mp2b 10 |
. . . . . . . . . 10
⊢ ◡𝑆:(-1[,]1)⟶(-(π / 2)[,](π /
2)) |
128 | 127 | ffvelrni 6266 |
. . . . . . . . 9
⊢
((ℑ‘(√‘𝑥)) ∈ (-1[,]1) → (◡𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π
/ 2))) |
129 | 119, 128 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (◡𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π
/ 2))) |
130 | 118, 129 | sseldi 3566 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (◡𝑆‘(ℑ‘(√‘𝑥))) ∈
ℝ) |
131 | | remulcl 9900 |
. . . . . . 7
⊢ ((2
∈ ℝ ∧ (◡𝑆‘(ℑ‘(√‘𝑥))) ∈ ℝ) → (2
· (◡𝑆‘(ℑ‘(√‘𝑥)))) ∈
ℝ) |
132 | 29, 130, 131 | sylancr 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) ∈
ℝ) |
133 | | efif1olem4.5 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈
ℤ) |
134 | 133 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑧 ∈ ℝ ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈
ℤ) |
135 | 134 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∀𝑧 ∈ ℝ ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈
ℤ) |
136 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑧 = (2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) → (𝑧 − 𝑦) = ((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) |
137 | 136 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑧 = (2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) → ((𝑧 − 𝑦) / (2 · π)) = (((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π))) |
138 | 137 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑧 = (2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) → (((𝑧 − 𝑦) / (2 · π)) ∈ ℤ ↔
(((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈
ℤ)) |
139 | 138 | rexbidv 3034 |
. . . . . . 7
⊢ (𝑧 = (2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) → (∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈ ℤ ↔
∃𝑦 ∈ 𝐷 (((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈
ℤ)) |
140 | 139 | rspcv 3278 |
. . . . . 6
⊢ ((2
· (◡𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ →
(∀𝑧 ∈ ℝ
∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈ ℤ →
∃𝑦 ∈ 𝐷 (((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈
ℤ)) |
141 | 132, 135,
140 | sylc 63 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∃𝑦 ∈ 𝐷 (((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈
ℤ) |
142 | | oveq1 6556 |
. . . . . . . 8
⊢
((exp‘(i · ((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1 → ((exp‘(i · ((2
· (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))) = (1 · (exp‘(i
· 𝑦)))) |
143 | 3 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → i ∈ ℂ) |
144 | 132 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → (2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) ∈
ℝ) |
145 | 144 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → (2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) ∈
ℂ) |
146 | 1 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → 𝐷 ⊆ ℝ) |
147 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ 𝐷) |
148 | 146, 147 | sseldd 3569 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ ℝ) |
149 | 148 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ ℂ) |
150 | 143, 145,
149 | subdid 10365 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → (i · ((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) = ((i · (2 · (◡𝑆‘(ℑ‘(√‘𝑥))))) − (i · 𝑦))) |
151 | 150 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → ((i · ((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦)) = (((i · (2 · (◡𝑆‘(ℑ‘(√‘𝑥))))) − (i · 𝑦)) + (i · 𝑦))) |
152 | | mulcl 9899 |
. . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ (2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ) → (i
· (2 · (◡𝑆‘(ℑ‘(√‘𝑥))))) ∈
ℂ) |
153 | 3, 145, 152 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → (i · (2 · (◡𝑆‘(ℑ‘(√‘𝑥))))) ∈
ℂ) |
154 | 3, 149, 72 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → (i · 𝑦) ∈ ℂ) |
155 | 153, 154 | npcand 10275 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → (((i · (2 · (◡𝑆‘(ℑ‘(√‘𝑥))))) − (i · 𝑦)) + (i · 𝑦)) = (i · (2 ·
(◡𝑆‘(ℑ‘(√‘𝑥)))))) |
156 | 151, 155 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → ((i · ((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦)) = (i · (2 · (◡𝑆‘(ℑ‘(√‘𝑥)))))) |
157 | 156 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → (exp‘((i · ((2
· (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦))) = (exp‘(i · (2 ·
(◡𝑆‘(ℑ‘(√‘𝑥))))))) |
158 | 145, 149 | subcld 10271 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → ((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ) |
159 | | mulcl 9899 |
. . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ ((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ) → (i · ((2
· (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ) |
160 | 3, 158, 159 | sylancr 694 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → (i · ((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ) |
161 | | efadd 14663 |
. . . . . . . . . . 11
⊢ (((i
· ((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) →
(exp‘((i · ((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦))) = ((exp‘(i · ((2 ·
(◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦)))) |
162 | 160, 154,
161 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → (exp‘((i · ((2
· (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦))) = ((exp‘(i · ((2 ·
(◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦)))) |
163 | 130 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (◡𝑆‘(ℑ‘(√‘𝑥))) ∈
ℂ) |
164 | | 2cn 10968 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℂ |
165 | | mul12 10081 |
. . . . . . . . . . . . . . . 16
⊢ ((i
∈ ℂ ∧ 2 ∈ ℂ ∧ (◡𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ) → (i
· (2 · (◡𝑆‘(ℑ‘(√‘𝑥))))) = (2 · (i ·
(◡𝑆‘(ℑ‘(√‘𝑥)))))) |
166 | 3, 164, 165 | mp3an12 1406 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ → (i
· (2 · (◡𝑆‘(ℑ‘(√‘𝑥))))) = (2 · (i ·
(◡𝑆‘(ℑ‘(√‘𝑥)))))) |
167 | 163, 166 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (i · (2 · (◡𝑆‘(ℑ‘(√‘𝑥))))) = (2 · (i ·
(◡𝑆‘(ℑ‘(√‘𝑥)))))) |
168 | 167 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (exp‘(i · (2 ·
(◡𝑆‘(ℑ‘(√‘𝑥)))))) = (exp‘(2 ·
(i · (◡𝑆‘(ℑ‘(√‘𝑥))))))) |
169 | | mulcl 9899 |
. . . . . . . . . . . . . . 15
⊢ ((i
∈ ℂ ∧ (◡𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ) → (i
· (◡𝑆‘(ℑ‘(√‘𝑥)))) ∈
ℂ) |
170 | 3, 163, 169 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (i · (◡𝑆‘(ℑ‘(√‘𝑥)))) ∈
ℂ) |
171 | | 2z 11286 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
172 | | efexp 14670 |
. . . . . . . . . . . . . 14
⊢ (((i
· (◡𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ ∧ 2
∈ ℤ) → (exp‘(2 · (i · (◡𝑆‘(ℑ‘(√‘𝑥)))))) = ((exp‘(i ·
(◡𝑆‘(ℑ‘(√‘𝑥)))))↑2)) |
173 | 170, 171,
172 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (exp‘(2 · (i ·
(◡𝑆‘(ℑ‘(√‘𝑥)))))) = ((exp‘(i ·
(◡𝑆‘(ℑ‘(√‘𝑥)))))↑2)) |
174 | 168, 173 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (exp‘(i · (2 ·
(◡𝑆‘(ℑ‘(√‘𝑥)))))) = ((exp‘(i ·
(◡𝑆‘(ℑ‘(√‘𝑥)))))↑2)) |
175 | 130 | recoscld 14713 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (cos‘(◡𝑆‘(ℑ‘(√‘𝑥)))) ∈
ℝ) |
176 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐶) |
177 | 176, 16 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ (◡abs “ {1})) |
178 | | fniniseg 6246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (abs Fn
ℂ → (𝑥 ∈
(◡abs “ {1}) ↔ (𝑥 ∈ ℂ ∧
(abs‘𝑥) =
1))) |
179 | 12, 178 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (◡abs “ {1}) ↔ (𝑥 ∈ ℂ ∧ (abs‘𝑥) = 1)) |
180 | 177, 179 | sylib 207 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ ℂ ∧ (abs‘𝑥) = 1)) |
181 | 180 | simpld 474 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℂ) |
182 | 181 | sqrtcld 14024 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (√‘𝑥) ∈ ℂ) |
183 | 182 | recld 13782 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (ℜ‘(√‘𝑥)) ∈
ℝ) |
184 | | cosq14ge0 24067 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π
/ 2)) → 0 ≤ (cos‘(◡𝑆‘(ℑ‘(√‘𝑥))))) |
185 | 129, 184 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 0 ≤ (cos‘(◡𝑆‘(ℑ‘(√‘𝑥))))) |
186 | 181 | sqrtrege0d 14025 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 0 ≤
(ℜ‘(√‘𝑥))) |
187 | | sincossq 14745 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((◡𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ →
(((sin‘(◡𝑆‘(ℑ‘(√‘𝑥))))↑2) +
((cos‘(◡𝑆‘(ℑ‘(√‘𝑥))))↑2)) =
1) |
188 | 163, 187 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((sin‘(◡𝑆‘(ℑ‘(√‘𝑥))))↑2) +
((cos‘(◡𝑆‘(ℑ‘(√‘𝑥))))↑2)) =
1) |
189 | 181 | sqsqrtd 14026 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((√‘𝑥)↑2) = 𝑥) |
190 | 189 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (abs‘((√‘𝑥)↑2)) = (abs‘𝑥)) |
191 | | 2nn0 11186 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℕ0 |
192 | | absexp 13892 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((√‘𝑥)
∈ ℂ ∧ 2 ∈ ℕ0) →
(abs‘((√‘𝑥)↑2)) = ((abs‘(√‘𝑥))↑2)) |
193 | 182, 191,
192 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (abs‘((√‘𝑥)↑2)) =
((abs‘(√‘𝑥))↑2)) |
194 | 180 | simprd 478 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (abs‘𝑥) = 1) |
195 | 190, 193,
194 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((abs‘(√‘𝑥))↑2) = 1) |
196 | 182 | absvalsq2d 14030 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((abs‘(√‘𝑥))↑2) =
(((ℜ‘(√‘𝑥))↑2) +
((ℑ‘(√‘𝑥))↑2))) |
197 | 188, 195,
196 | 3eqtr2d 2650 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((sin‘(◡𝑆‘(ℑ‘(√‘𝑥))))↑2) +
((cos‘(◡𝑆‘(ℑ‘(√‘𝑥))))↑2)) =
(((ℜ‘(√‘𝑥))↑2) +
((ℑ‘(√‘𝑥))↑2))) |
198 | 121 | fveq1i 6104 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆‘(◡𝑆‘(ℑ‘(√‘𝑥)))) = ((sin ↾ (-(π /
2)[,](π / 2)))‘(◡𝑆‘(ℑ‘(√‘𝑥)))) |
199 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((◡𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π
/ 2)) → ((sin ↾ (-(π / 2)[,](π / 2)))‘(◡𝑆‘(ℑ‘(√‘𝑥)))) = (sin‘(◡𝑆‘(ℑ‘(√‘𝑥))))) |
200 | 129, 199 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((sin ↾ (-(π / 2)[,](π
/ 2)))‘(◡𝑆‘(ℑ‘(√‘𝑥)))) = (sin‘(◡𝑆‘(ℑ‘(√‘𝑥))))) |
201 | 198, 200 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑆‘(◡𝑆‘(ℑ‘(√‘𝑥)))) = (sin‘(◡𝑆‘(ℑ‘(√‘𝑥))))) |
202 | | f1ocnvfv2 6433 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑆:(-(π / 2)[,](π /
2))–1-1-onto→(-1[,]1) ∧
(ℑ‘(√‘𝑥)) ∈ (-1[,]1)) → (𝑆‘(◡𝑆‘(ℑ‘(√‘𝑥)))) =
(ℑ‘(√‘𝑥))) |
203 | 124, 119,
202 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑆‘(◡𝑆‘(ℑ‘(√‘𝑥)))) =
(ℑ‘(√‘𝑥))) |
204 | 201, 203 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (sin‘(◡𝑆‘(ℑ‘(√‘𝑥)))) =
(ℑ‘(√‘𝑥))) |
205 | 204 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((sin‘(◡𝑆‘(ℑ‘(√‘𝑥))))↑2) =
((ℑ‘(√‘𝑥))↑2)) |
206 | 197, 205 | oveq12d 6567 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((((sin‘(◡𝑆‘(ℑ‘(√‘𝑥))))↑2) +
((cos‘(◡𝑆‘(ℑ‘(√‘𝑥))))↑2)) −
((sin‘(◡𝑆‘(ℑ‘(√‘𝑥))))↑2)) =
((((ℜ‘(√‘𝑥))↑2) +
((ℑ‘(√‘𝑥))↑2)) −
((ℑ‘(√‘𝑥))↑2))) |
207 | 163 | sincld 14699 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (sin‘(◡𝑆‘(ℑ‘(√‘𝑥)))) ∈
ℂ) |
208 | 207 | sqcld 12868 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((sin‘(◡𝑆‘(ℑ‘(√‘𝑥))))↑2) ∈
ℂ) |
209 | 163 | coscld 14700 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (cos‘(◡𝑆‘(ℑ‘(√‘𝑥)))) ∈
ℂ) |
210 | 209 | sqcld 12868 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((cos‘(◡𝑆‘(ℑ‘(√‘𝑥))))↑2) ∈
ℂ) |
211 | 208, 210 | pncan2d 10273 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((((sin‘(◡𝑆‘(ℑ‘(√‘𝑥))))↑2) +
((cos‘(◡𝑆‘(ℑ‘(√‘𝑥))))↑2)) −
((sin‘(◡𝑆‘(ℑ‘(√‘𝑥))))↑2)) =
((cos‘(◡𝑆‘(ℑ‘(√‘𝑥))))↑2)) |
212 | 183 | recnd 9947 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (ℜ‘(√‘𝑥)) ∈
ℂ) |
213 | 212 | sqcld 12868 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((ℜ‘(√‘𝑥))↑2) ∈
ℂ) |
214 | 205, 208 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) →
((ℑ‘(√‘𝑥))↑2) ∈ ℂ) |
215 | 213, 214 | pncand 10272 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) →
((((ℜ‘(√‘𝑥))↑2) +
((ℑ‘(√‘𝑥))↑2)) −
((ℑ‘(√‘𝑥))↑2)) =
((ℜ‘(√‘𝑥))↑2)) |
216 | 206, 211,
215 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((cos‘(◡𝑆‘(ℑ‘(√‘𝑥))))↑2) =
((ℜ‘(√‘𝑥))↑2)) |
217 | 175, 183,
185, 186, 216 | sq11d 12907 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (cos‘(◡𝑆‘(ℑ‘(√‘𝑥)))) =
(ℜ‘(√‘𝑥))) |
218 | 204 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (i · (sin‘(◡𝑆‘(ℑ‘(√‘𝑥))))) = (i ·
(ℑ‘(√‘𝑥)))) |
219 | 217, 218 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((cos‘(◡𝑆‘(ℑ‘(√‘𝑥)))) + (i ·
(sin‘(◡𝑆‘(ℑ‘(√‘𝑥)))))) =
((ℜ‘(√‘𝑥)) + (i ·
(ℑ‘(√‘𝑥))))) |
220 | | efival 14721 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ →
(exp‘(i · (◡𝑆‘(ℑ‘(√‘𝑥))))) = ((cos‘(◡𝑆‘(ℑ‘(√‘𝑥)))) + (i ·
(sin‘(◡𝑆‘(ℑ‘(√‘𝑥))))))) |
221 | 163, 220 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (exp‘(i · (◡𝑆‘(ℑ‘(√‘𝑥))))) = ((cos‘(◡𝑆‘(ℑ‘(√‘𝑥)))) + (i ·
(sin‘(◡𝑆‘(ℑ‘(√‘𝑥))))))) |
222 | 182 | replimd 13785 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (√‘𝑥) = ((ℜ‘(√‘𝑥)) + (i ·
(ℑ‘(√‘𝑥))))) |
223 | 219, 221,
222 | 3eqtr4d 2654 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (exp‘(i · (◡𝑆‘(ℑ‘(√‘𝑥))))) = (√‘𝑥)) |
224 | 223 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((exp‘(i · (◡𝑆‘(ℑ‘(√‘𝑥)))))↑2) =
((√‘𝑥)↑2)) |
225 | 174, 224,
189 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (exp‘(i · (2 ·
(◡𝑆‘(ℑ‘(√‘𝑥)))))) = 𝑥) |
226 | 225 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → (exp‘(i · (2 ·
(◡𝑆‘(ℑ‘(√‘𝑥)))))) = 𝑥) |
227 | 157, 162,
226 | 3eqtr3d 2652 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → ((exp‘(i · ((2
· (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))) = 𝑥) |
228 | 154, 76 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → (exp‘(i · 𝑦)) ∈
ℂ) |
229 | 228 | mulid2d 9937 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → (1 · (exp‘(i ·
𝑦))) = (exp‘(i
· 𝑦))) |
230 | 227, 229 | eqeq12d 2625 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → (((exp‘(i · ((2
· (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))) = (1 · (exp‘(i
· 𝑦))) ↔ 𝑥 = (exp‘(i · 𝑦)))) |
231 | 142, 230 | syl5ib 233 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → ((exp‘(i · ((2
· (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1 → 𝑥 = (exp‘(i · 𝑦)))) |
232 | | efeq1 24079 |
. . . . . . . . 9
⊢ ((i
· ((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ → ((exp‘(i
· ((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1 ↔ ((i · ((2 ·
(◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) ∈
ℤ)) |
233 | 160, 232 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → ((exp‘(i · ((2
· (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1 ↔ ((i · ((2 ·
(◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) ∈
ℤ)) |
234 | | divcan5 10606 |
. . . . . . . . . . 11
⊢ ((((2
· (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ ∧ ((2 · π)
∈ ℂ ∧ (2 · π) ≠ 0) ∧ (i ∈ ℂ ∧ i
≠ 0)) → ((i · ((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) = (((2
· (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π))) |
235 | 61, 63, 234 | mp3an23 1408 |
. . . . . . . . . 10
⊢ (((2
· (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ → ((i · ((2
· (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) = (((2
· (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π))) |
236 | 158, 235 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → ((i · ((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) = (((2
· (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π))) |
237 | 236 | eleq1d 2672 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → (((i · ((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) ∈
ℤ ↔ (((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈
ℤ)) |
238 | 233, 237 | bitr2d 268 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → ((((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ ↔
(exp‘(i · ((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1)) |
239 | 89 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → (𝐹‘𝑦) = (exp‘(i · 𝑦))) |
240 | 239 | eqeq2d 2620 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → (𝑥 = (𝐹‘𝑦) ↔ 𝑥 = (exp‘(i · 𝑦)))) |
241 | 231, 238,
240 | 3imtr4d 282 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ 𝐷) → ((((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ →
𝑥 = (𝐹‘𝑦))) |
242 | 241 | reximdva 3000 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (∃𝑦 ∈ 𝐷 (((2 · (◡𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ →
∃𝑦 ∈ 𝐷 𝑥 = (𝐹‘𝑦))) |
243 | 141, 242 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∃𝑦 ∈ 𝐷 𝑥 = (𝐹‘𝑦)) |
244 | 243 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝑥 = (𝐹‘𝑦)) |
245 | | dffo3 6282 |
. . 3
⊢ (𝐹:𝐷–onto→𝐶 ↔ (𝐹:𝐷⟶𝐶 ∧ ∀𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝑥 = (𝐹‘𝑦))) |
246 | 20, 244, 245 | sylanbrc 695 |
. 2
⊢ (𝜑 → 𝐹:𝐷–onto→𝐶) |
247 | | df-f1o 5811 |
. 2
⊢ (𝐹:𝐷–1-1-onto→𝐶 ↔ (𝐹:𝐷–1-1→𝐶 ∧ 𝐹:𝐷–onto→𝐶)) |
248 | 114, 246,
247 | sylanbrc 695 |
1
⊢ (𝜑 → 𝐹:𝐷–1-1-onto→𝐶) |