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

Theorem efif1olem4 24095
Description: The exponential function of an imaginary number maps any interval of length one-to-one onto the unit circle. (Contributed by Paul Chapman, 16-Mar-2008.) (Proof shortened by Mario Carneiro, 13-May-2014.)
Hypotheses
Ref Expression
efif1o.1 𝐹 = (𝑤𝐷 ↦ (exp‘(i · 𝑤)))
efif1o.2 𝐶 = (abs “ {1})
efif1olem4.3 (𝜑𝐷 ⊆ ℝ)
efif1olem4.4 ((𝜑 ∧ (𝑥𝐷𝑦𝐷)) → (abs‘(𝑥𝑦)) < (2 · π))
efif1olem4.5 ((𝜑𝑧 ∈ ℝ) → ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ)
efif1olem4.6 𝑆 = (sin ↾ (-(π / 2)[,](π / 2)))
Assertion
Ref Expression
efif1olem4 (𝜑𝐹:𝐷1-1-onto𝐶)
Distinct variable groups:   𝑥,𝑤,𝑦,𝑧   𝑤,𝐶,𝑥,𝑦   𝑥,𝐹,𝑦   𝜑,𝑤,𝑥,𝑦,𝑧   𝑦,𝑆,𝑧   𝑤,𝐷,𝑥,𝑦,𝑧
Allowed substitution hints:   𝐶(𝑧)   𝑆(𝑥,𝑤)   𝐹(𝑧,𝑤)

Proof of Theorem efif1olem4
StepHypRef Expression
1 efif1olem4.3 . . . . . 6 (𝜑𝐷 ⊆ ℝ)
21sselda 3568 . . . . 5 ((𝜑𝑤𝐷) → 𝑤 ∈ ℝ)
3 ax-icn 9874 . . . . . . . . 9 i ∈ ℂ
4 recn 9905 . . . . . . . . 9 (𝑤 ∈ ℝ → 𝑤 ∈ ℂ)
5 mulcl 9899 . . . . . . . . 9 ((i ∈ ℂ ∧ 𝑤 ∈ ℂ) → (i · 𝑤) ∈ ℂ)
63, 4, 5sylancr 694 . . . . . . . 8 (𝑤 ∈ ℝ → (i · 𝑤) ∈ ℂ)
7 efcl 14652 . . . . . . . 8 ((i · 𝑤) ∈ ℂ → (exp‘(i · 𝑤)) ∈ ℂ)
86, 7syl 17 . . . . . . 7 (𝑤 ∈ ℝ → (exp‘(i · 𝑤)) ∈ ℂ)
9 absefi 14765 . . . . . . 7 (𝑤 ∈ ℝ → (abs‘(exp‘(i · 𝑤))) = 1)
10 absf 13925 . . . . . . . . 9 abs:ℂ⟶ℝ
11 ffn 5958 . . . . . . . . 9 (abs:ℂ⟶ℝ → abs Fn ℂ)
1210, 11ax-mp 5 . . . . . . . 8 abs Fn ℂ
13 fniniseg 6246 . . . . . . . 8 (abs Fn ℂ → ((exp‘(i · 𝑤)) ∈ (abs “ {1}) ↔ ((exp‘(i · 𝑤)) ∈ ℂ ∧ (abs‘(exp‘(i · 𝑤))) = 1)))
1412, 13ax-mp 5 . . . . . . 7 ((exp‘(i · 𝑤)) ∈ (abs “ {1}) ↔ ((exp‘(i · 𝑤)) ∈ ℂ ∧ (abs‘(exp‘(i · 𝑤))) = 1))
158, 9, 14sylanbrc 695 . . . . . 6 (𝑤 ∈ ℝ → (exp‘(i · 𝑤)) ∈ (abs “ {1}))
16 efif1o.2 . . . . . 6 𝐶 = (abs “ {1})
1715, 16syl6eleqr 2699 . . . . 5 (𝑤 ∈ ℝ → (exp‘(i · 𝑤)) ∈ 𝐶)
182, 17syl 17 . . . 4 ((𝜑𝑤𝐷) → (exp‘(i · 𝑤)) ∈ 𝐶)
19 efif1o.1 . . . 4 𝐹 = (𝑤𝐷 ↦ (exp‘(i · 𝑤)))
2018, 19fmptd 6292 . . 3 (𝜑𝐹:𝐷𝐶)
211ad2antrr 758 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝐷 ⊆ ℝ)
22 simplrl 796 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥𝐷)
2321, 22sseldd 3569 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 ∈ ℝ)
2423recnd 9947 . . . . . 6 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 ∈ ℂ)
25 simplrr 797 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑦𝐷)
2621, 25sseldd 3569 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑦 ∈ ℝ)
2726recnd 9947 . . . . . 6 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑦 ∈ ℂ)
2824, 27subcld 10271 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝑥𝑦) ∈ ℂ)
29 2re 10967 . . . . . . . . . . . 12 2 ∈ ℝ
30 pire 24014 . . . . . . . . . . . 12 π ∈ ℝ
3129, 30remulcli 9933 . . . . . . . . . . 11 (2 · π) ∈ ℝ
3231recni 9931 . . . . . . . . . 10 (2 · π) ∈ ℂ
33 2pos 10989 . . . . . . . . . . . 12 0 < 2
34 pipos 24016 . . . . . . . . . . . 12 0 < π
3529, 30, 33, 34mulgt0ii 10049 . . . . . . . . . . 11 0 < (2 · π)
3631, 35gt0ne0ii 10443 . . . . . . . . . 10 (2 · π) ≠ 0
37 divcl 10570 . . . . . . . . . 10 (((𝑥𝑦) ∈ ℂ ∧ (2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) → ((𝑥𝑦) / (2 · π)) ∈ ℂ)
3832, 36, 37mp3an23 1408 . . . . . . . . 9 ((𝑥𝑦) ∈ ℂ → ((𝑥𝑦) / (2 · π)) ∈ ℂ)
3928, 38syl 17 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((𝑥𝑦) / (2 · π)) ∈ ℂ)
40 absdiv 13883 . . . . . . . . . . . . 13 (((𝑥𝑦) ∈ ℂ ∧ (2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (abs‘(2 · π))))
4132, 36, 40mp3an23 1408 . . . . . . . . . . . 12 ((𝑥𝑦) ∈ ℂ → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (abs‘(2 · π))))
4228, 41syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (abs‘(2 · π))))
43 0re 9919 . . . . . . . . . . . . . 14 0 ∈ ℝ
4443, 31, 35ltleii 10039 . . . . . . . . . . . . 13 0 ≤ (2 · π)
45 absid 13884 . . . . . . . . . . . . 13 (((2 · π) ∈ ℝ ∧ 0 ≤ (2 · π)) → (abs‘(2 · π)) = (2 · π))
4631, 44, 45mp2an 704 . . . . . . . . . . . 12 (abs‘(2 · π)) = (2 · π)
4746oveq2i 6560 . . . . . . . . . . 11 ((abs‘(𝑥𝑦)) / (abs‘(2 · π))) = ((abs‘(𝑥𝑦)) / (2 · π))
4842, 47syl6eq 2660 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (2 · π)))
49 efif1olem4.4 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐷𝑦𝐷)) → (abs‘(𝑥𝑦)) < (2 · π))
5049adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘(𝑥𝑦)) < (2 · π))
5132mulid1i 9921 . . . . . . . . . . . 12 ((2 · π) · 1) = (2 · π)
5250, 51syl6breqr 4625 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘(𝑥𝑦)) < ((2 · π) · 1))
5328abscld 14023 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘(𝑥𝑦)) ∈ ℝ)
54 1re 9918 . . . . . . . . . . . . 13 1 ∈ ℝ
5531, 35pm3.2i 470 . . . . . . . . . . . . 13 ((2 · π) ∈ ℝ ∧ 0 < (2 · π))
56 ltdivmul 10777 . . . . . . . . . . . . 13 (((abs‘(𝑥𝑦)) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((2 · π) ∈ ℝ ∧ 0 < (2 · π))) → (((abs‘(𝑥𝑦)) / (2 · π)) < 1 ↔ (abs‘(𝑥𝑦)) < ((2 · π) · 1)))
5754, 55, 56mp3an23 1408 . . . . . . . . . . . 12 ((abs‘(𝑥𝑦)) ∈ ℝ → (((abs‘(𝑥𝑦)) / (2 · π)) < 1 ↔ (abs‘(𝑥𝑦)) < ((2 · π) · 1)))
5853, 57syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (((abs‘(𝑥𝑦)) / (2 · π)) < 1 ↔ (abs‘(𝑥𝑦)) < ((2 · π) · 1)))
5952, 58mpbird 246 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((abs‘(𝑥𝑦)) / (2 · π)) < 1)
6048, 59eqbrtrd 4605 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) < 1)
6132, 36pm3.2i 470 . . . . . . . . . . . . . 14 ((2 · π) ∈ ℂ ∧ (2 · π) ≠ 0)
62 ine0 10344 . . . . . . . . . . . . . . 15 i ≠ 0
633, 62pm3.2i 470 . . . . . . . . . . . . . 14 (i ∈ ℂ ∧ i ≠ 0)
64 divcan5 10606 . . . . . . . . . . . . . 14 (((𝑥𝑦) ∈ ℂ ∧ ((2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) ∧ (i ∈ ℂ ∧ i ≠ 0)) → ((i · (𝑥𝑦)) / (i · (2 · π))) = ((𝑥𝑦) / (2 · π)))
6561, 63, 64mp3an23 1408 . . . . . . . . . . . . 13 ((𝑥𝑦) ∈ ℂ → ((i · (𝑥𝑦)) / (i · (2 · π))) = ((𝑥𝑦) / (2 · π)))
6628, 65syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((i · (𝑥𝑦)) / (i · (2 · π))) = ((𝑥𝑦) / (2 · π)))
673a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → i ∈ ℂ)
6867, 24, 27subdid 10365 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · (𝑥𝑦)) = ((i · 𝑥) − (i · 𝑦)))
6968fveq2d 6107 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · (𝑥𝑦))) = (exp‘((i · 𝑥) − (i · 𝑦))))
70 mulcl 9899 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
713, 24, 70sylancr 694 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · 𝑥) ∈ ℂ)
72 mulcl 9899 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝑦 ∈ ℂ) → (i · 𝑦) ∈ ℂ)
733, 27, 72sylancr 694 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · 𝑦) ∈ ℂ)
74 efsub 14669 . . . . . . . . . . . . . . 15 (((i · 𝑥) ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → (exp‘((i · 𝑥) − (i · 𝑦))) = ((exp‘(i · 𝑥)) / (exp‘(i · 𝑦))))
7571, 73, 74syl2anc 691 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘((i · 𝑥) − (i · 𝑦))) = ((exp‘(i · 𝑥)) / (exp‘(i · 𝑦))))
76 efcl 14652 . . . . . . . . . . . . . . . 16 ((i · 𝑦) ∈ ℂ → (exp‘(i · 𝑦)) ∈ ℂ)
7773, 76syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · 𝑦)) ∈ ℂ)
78 efne0 14666 . . . . . . . . . . . . . . . 16 ((i · 𝑦) ∈ ℂ → (exp‘(i · 𝑦)) ≠ 0)
7973, 78syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · 𝑦)) ≠ 0)
80 simpr 476 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝐹𝑥) = (𝐹𝑦))
81 oveq2 6557 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑥 → (i · 𝑤) = (i · 𝑥))
8281fveq2d 6107 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑥 → (exp‘(i · 𝑤)) = (exp‘(i · 𝑥)))
83 fvex 6113 . . . . . . . . . . . . . . . . . 18 (exp‘(i · 𝑥)) ∈ V
8482, 19, 83fvmpt 6191 . . . . . . . . . . . . . . . . 17 (𝑥𝐷 → (𝐹𝑥) = (exp‘(i · 𝑥)))
8522, 84syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝐹𝑥) = (exp‘(i · 𝑥)))
86 oveq2 6557 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑦 → (i · 𝑤) = (i · 𝑦))
8786fveq2d 6107 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑦 → (exp‘(i · 𝑤)) = (exp‘(i · 𝑦)))
88 fvex 6113 . . . . . . . . . . . . . . . . . 18 (exp‘(i · 𝑦)) ∈ V
8987, 19, 88fvmpt 6191 . . . . . . . . . . . . . . . . 17 (𝑦𝐷 → (𝐹𝑦) = (exp‘(i · 𝑦)))
9025, 89syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝐹𝑦) = (exp‘(i · 𝑦)))
9180, 85, 903eqtr3d 2652 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · 𝑥)) = (exp‘(i · 𝑦)))
9277, 79, 91diveq1bd 10728 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((exp‘(i · 𝑥)) / (exp‘(i · 𝑦))) = 1)
9369, 75, 923eqtrd 2648 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · (𝑥𝑦))) = 1)
94 mulcl 9899 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ (𝑥𝑦) ∈ ℂ) → (i · (𝑥𝑦)) ∈ ℂ)
953, 28, 94sylancr 694 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · (𝑥𝑦)) ∈ ℂ)
96 efeq1 24079 . . . . . . . . . . . . . 14 ((i · (𝑥𝑦)) ∈ ℂ → ((exp‘(i · (𝑥𝑦))) = 1 ↔ ((i · (𝑥𝑦)) / (i · (2 · π))) ∈ ℤ))
9795, 96syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((exp‘(i · (𝑥𝑦))) = 1 ↔ ((i · (𝑥𝑦)) / (i · (2 · π))) ∈ ℤ))
9893, 97mpbid 221 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((i · (𝑥𝑦)) / (i · (2 · π))) ∈ ℤ)
9966, 98eqeltrrd 2689 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((𝑥𝑦) / (2 · π)) ∈ ℤ)
100 nn0abscl 13900 . . . . . . . . . . 11 (((𝑥𝑦) / (2 · π)) ∈ ℤ → (abs‘((𝑥𝑦) / (2 · π))) ∈ ℕ0)
10199, 100syl 17 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) ∈ ℕ0)
102 nn0lt10b 11316 . . . . . . . . . 10 ((abs‘((𝑥𝑦) / (2 · π))) ∈ ℕ0 → ((abs‘((𝑥𝑦) / (2 · π))) < 1 ↔ (abs‘((𝑥𝑦) / (2 · π))) = 0))
103101, 102syl 17 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((abs‘((𝑥𝑦) / (2 · π))) < 1 ↔ (abs‘((𝑥𝑦) / (2 · π))) = 0))
10460, 103mpbid 221 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) = 0)
10539, 104abs00d 14033 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((𝑥𝑦) / (2 · π)) = 0)
106 diveq0 10574 . . . . . . . . 9 (((𝑥𝑦) ∈ ℂ ∧ (2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) → (((𝑥𝑦) / (2 · π)) = 0 ↔ (𝑥𝑦) = 0))
10732, 36, 106mp3an23 1408 . . . . . . . 8 ((𝑥𝑦) ∈ ℂ → (((𝑥𝑦) / (2 · π)) = 0 ↔ (𝑥𝑦) = 0))
10828, 107syl 17 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (((𝑥𝑦) / (2 · π)) = 0 ↔ (𝑥𝑦) = 0))
109105, 108mpbid 221 . . . . . 6 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝑥𝑦) = 0)
11024, 27, 109subeq0d 10279 . . . . 5 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 = 𝑦)
111110ex 449 . . . 4 ((𝜑 ∧ (𝑥𝐷𝑦𝐷)) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
112111ralrimivva 2954 . . 3 (𝜑 → ∀𝑥𝐷𝑦𝐷 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
113 dff13 6416 . . 3 (𝐹:𝐷1-1𝐶 ↔ (𝐹:𝐷𝐶 ∧ ∀𝑥𝐷𝑦𝐷 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
11420, 112, 113sylanbrc 695 . 2 (𝜑𝐹:𝐷1-1𝐶)
115 neghalfpire 24021 . . . . . . . . 9 -(π / 2) ∈ ℝ
116 halfpire 24020 . . . . . . . . 9 (π / 2) ∈ ℝ
117 iccssre 12126 . . . . . . . . 9 ((-(π / 2) ∈ ℝ ∧ (π / 2) ∈ ℝ) → (-(π / 2)[,](π / 2)) ⊆ ℝ)
118115, 116, 117mp2an 704 . . . . . . . 8 (-(π / 2)[,](π / 2)) ⊆ ℝ
11919, 16efif1olem3 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)))
123121, 122ax-mp 5 . . . . . . . . . . . 12 (𝑆:(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) ↔ (sin ↾ (-(π / 2)[,](π / 2))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1))
124120, 123mpbir 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)))
127124, 125, 126mp2b 10 . . . . . . . . . 10 𝑆:(-1[,]1)⟶(-(π / 2)[,](π / 2))
128127ffvelrni 6266 . . . . . . . . 9 ((ℑ‘(√‘𝑥)) ∈ (-1[,]1) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π / 2)))
129119, 128syl 17 . . . . . . . 8 ((𝜑𝑥𝐶) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π / 2)))
130118, 129sseldi 3566 . . . . . . 7 ((𝜑𝑥𝐶) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℝ)
131 remulcl 9900 . . . . . . 7 ((2 ∈ ℝ ∧ (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℝ) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
13229, 130, 131sylancr 694 . . . . . 6 ((𝜑𝑥𝐶) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
133 efif1olem4.5 . . . . . . . 8 ((𝜑𝑧 ∈ ℝ) → ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ)
134133ralrimiva 2949 . . . . . . 7 (𝜑 → ∀𝑧 ∈ ℝ ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ)
135134adantr 480 . . . . . 6 ((𝜑𝑥𝐶) → ∀𝑧 ∈ ℝ ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ)
136 oveq1 6556 . . . . . . . . . 10 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → (𝑧𝑦) = ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))
137136oveq1d 6564 . . . . . . . . 9 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → ((𝑧𝑦) / (2 · π)) = (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)))
138137eleq1d 2672 . . . . . . . 8 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → (((𝑧𝑦) / (2 · π)) ∈ ℤ ↔ (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ))
139138rexbidv 3034 . . . . . . 7 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → (∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ ↔ ∃𝑦𝐷 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ))
140139rspcv 3278 . . . . . 6 ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ → (∀𝑧 ∈ ℝ ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ → ∃𝑦𝐷 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ))
141132, 135, 140sylc 63 . . . . 5 ((𝜑𝑥𝐶) → ∃𝑦𝐷 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ)
142 oveq1 6556 . . . . . . . 8 ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1 → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))) = (1 · (exp‘(i · 𝑦))))
1433a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → i ∈ ℂ)
144132adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
145144recnd 9947 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
1461ad2antrr 758 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝐷 ⊆ ℝ)
147 simpr 476 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝑦𝐷)
148146, 147sseldd 3569 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝑦 ∈ ℝ)
149148recnd 9947 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝑦 ∈ ℂ)
150143, 145, 149subdid 10365 . . . . . . . . . . . . 13 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) = ((i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) − (i · 𝑦)))
151150oveq1d 6564 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦)) = (((i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) − (i · 𝑦)) + (i · 𝑦)))
152 mulcl 9899 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) ∈ ℂ)
1533, 145, 152sylancr 694 . . . . . . . . . . . . 13 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) ∈ ℂ)
1543, 149, 72sylancr 694 . . . . . . . . . . . . 13 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · 𝑦) ∈ ℂ)
155153, 154npcand 10275 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (((i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) − (i · 𝑦)) + (i · 𝑦)) = (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))))
156151, 155eqtrd 2644 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦)) = (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))))
157156fveq2d 6107 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦))) = (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))))
158145, 149subcld 10271 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ)
159 mulcl 9899 . . . . . . . . . . . 12 ((i ∈ ℂ ∧ ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ) → (i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ)
1603, 158, 159sylancr 694 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ)
161 efadd 14663 . . . . . . . . . . 11 (((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → (exp‘((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦))) = ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))))
162160, 154, 161syl2anc 691 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦))) = ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))))
163130recnd 9947 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ)
164 2cn 10968 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
165 mul12 10081 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 2 ∈ ℂ ∧ (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) = (2 · (i · (𝑆‘(ℑ‘(√‘𝑥))))))
1663, 164, 165mp3an12 1406 . . . . . . . . . . . . . . 15 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) = (2 · (i · (𝑆‘(ℑ‘(√‘𝑥))))))
167163, 166syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) = (2 · (i · (𝑆‘(ℑ‘(√‘𝑥))))))
168167fveq2d 6107 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = (exp‘(2 · (i · (𝑆‘(ℑ‘(√‘𝑥)))))))
169 mulcl 9899 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ) → (i · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
1703, 163, 169sylancr 694 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (i · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
171 2z 11286 . . . . . . . . . . . . . 14 2 ∈ ℤ
172 efexp 14670 . . . . . . . . . . . . . 14 (((i · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ ∧ 2 ∈ ℤ) → (exp‘(2 · (i · (𝑆‘(ℑ‘(√‘𝑥)))))) = ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2))
173170, 171, 172sylancl 693 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → (exp‘(2 · (i · (𝑆‘(ℑ‘(√‘𝑥)))))) = ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2))
174168, 173eqtrd 2644 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2))
175130recoscld 14713 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → (cos‘(𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
176 simpr 476 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥𝐶) → 𝑥𝐶)
177176, 16syl6eleq 2698 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝑥 ∈ (abs “ {1}))
178 fniniseg 6246 . . . . . . . . . . . . . . . . . . . . 21 (abs Fn ℂ → (𝑥 ∈ (abs “ {1}) ↔ (𝑥 ∈ ℂ ∧ (abs‘𝑥) = 1)))
17912, 178ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (abs “ {1}) ↔ (𝑥 ∈ ℂ ∧ (abs‘𝑥) = 1))
180177, 179sylib 207 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (𝑥 ∈ ℂ ∧ (abs‘𝑥) = 1))
181180simpld 474 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → 𝑥 ∈ ℂ)
182181sqrtcld 14024 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → (√‘𝑥) ∈ ℂ)
183182recld 13782 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → (ℜ‘(√‘𝑥)) ∈ ℝ)
184 cosq14ge0 24067 . . . . . . . . . . . . . . . . 17 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π / 2)) → 0 ≤ (cos‘(𝑆‘(ℑ‘(√‘𝑥)))))
185129, 184syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → 0 ≤ (cos‘(𝑆‘(ℑ‘(√‘𝑥)))))
186181sqrtrege0d 14025 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → 0 ≤ (ℜ‘(√‘𝑥)))
187 sincossq 14745 . . . . . . . . . . . . . . . . . . . 20 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ → (((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = 1)
188163, 187syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = 1)
189181sqsqrtd 14026 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥𝐶) → ((√‘𝑥)↑2) = 𝑥)
190189fveq2d 6107 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (abs‘((√‘𝑥)↑2)) = (abs‘𝑥))
191 2nn0 11186 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℕ0
192 absexp 13892 . . . . . . . . . . . . . . . . . . . . 21 (((√‘𝑥) ∈ ℂ ∧ 2 ∈ ℕ0) → (abs‘((√‘𝑥)↑2)) = ((abs‘(√‘𝑥))↑2))
193182, 191, 192sylancl 693 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (abs‘((√‘𝑥)↑2)) = ((abs‘(√‘𝑥))↑2))
194180simprd 478 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (abs‘𝑥) = 1)
195190, 193, 1943eqtr3d 2652 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → ((abs‘(√‘𝑥))↑2) = 1)
196182absvalsq2d 14030 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → ((abs‘(√‘𝑥))↑2) = (((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)))
197188, 195, 1963eqtr2d 2650 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → (((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = (((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)))
198121fveq1i 6104 . . . . . . . . . . . . . . . . . . . . 21 (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = ((sin ↾ (-(π / 2)[,](π / 2)))‘(𝑆‘(ℑ‘(√‘𝑥))))
199 fvres 6117 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π / 2)) → ((sin ↾ (-(π / 2)[,](π / 2)))‘(𝑆‘(ℑ‘(√‘𝑥)))) = (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))
200129, 199syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥𝐶) → ((sin ↾ (-(π / 2)[,](π / 2)))‘(𝑆‘(ℑ‘(√‘𝑥)))) = (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))
201198, 200syl5eq 2656 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))
202 f1ocnvfv2 6433 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆:(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) ∧ (ℑ‘(√‘𝑥)) ∈ (-1[,]1)) → (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℑ‘(√‘𝑥)))
203124, 119, 202sylancr 694 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℑ‘(√‘𝑥)))
204201, 203eqtr3d 2646 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (sin‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℑ‘(√‘𝑥)))
205204oveq1d 6564 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) = ((ℑ‘(√‘𝑥))↑2))
206197, 205oveq12d 6567 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) − ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = ((((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)) − ((ℑ‘(√‘𝑥))↑2)))
207163sincld 14699 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (sin‘(𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
208207sqcld 12868 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) ∈ ℂ)
209163coscld 14700 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (cos‘(𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
210209sqcld 12868 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) ∈ ℂ)
211208, 210pncan2d 10273 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) − ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2))
212183recnd 9947 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (ℜ‘(√‘𝑥)) ∈ ℂ)
213212sqcld 12868 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((ℜ‘(√‘𝑥))↑2) ∈ ℂ)
214205, 208eqeltrrd 2689 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((ℑ‘(√‘𝑥))↑2) ∈ ℂ)
215213, 214pncand 10272 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)) − ((ℑ‘(√‘𝑥))↑2)) = ((ℜ‘(√‘𝑥))↑2))
216206, 211, 2153eqtr3d 2652 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) = ((ℜ‘(√‘𝑥))↑2))
217175, 183, 185, 186, 216sq11d 12907 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (cos‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℜ‘(√‘𝑥)))
218204oveq2d 6565 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥))))) = (i · (ℑ‘(√‘𝑥))))
219217, 218oveq12d 6567 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → ((cos‘(𝑆‘(ℑ‘(√‘𝑥)))) + (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))) = ((ℜ‘(√‘𝑥)) + (i · (ℑ‘(√‘𝑥)))))
220 efival 14721 . . . . . . . . . . . . . . 15 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ → (exp‘(i · (𝑆‘(ℑ‘(√‘𝑥))))) = ((cos‘(𝑆‘(ℑ‘(√‘𝑥)))) + (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))))
221163, 220syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (exp‘(i · (𝑆‘(ℑ‘(√‘𝑥))))) = ((cos‘(𝑆‘(ℑ‘(√‘𝑥)))) + (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))))
222182replimd 13785 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (√‘𝑥) = ((ℜ‘(√‘𝑥)) + (i · (ℑ‘(√‘𝑥)))))
223219, 221, 2223eqtr4d 2654 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → (exp‘(i · (𝑆‘(ℑ‘(√‘𝑥))))) = (√‘𝑥))
224223oveq1d 6564 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2) = ((√‘𝑥)↑2))
225174, 224, 1893eqtrd 2648 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = 𝑥)
226225adantr 480 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = 𝑥)
227157, 162, 2263eqtr3d 2652 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))) = 𝑥)
228154, 76syl 17 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘(i · 𝑦)) ∈ ℂ)
229228mulid2d 9937 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (1 · (exp‘(i · 𝑦))) = (exp‘(i · 𝑦)))
230227, 229eqeq12d 2625 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))) = (1 · (exp‘(i · 𝑦))) ↔ 𝑥 = (exp‘(i · 𝑦))))
231142, 230syl5ib 233 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1 → 𝑥 = (exp‘(i · 𝑦))))
232 efeq1 24079 . . . . . . . . 9 ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1 ↔ ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) ∈ ℤ))
233160, 232syl 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 · π)))
23561, 63, 234mp3an23 1408 . . . . . . . . . 10 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) = (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)))
236158, 235syl 17 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) = (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)))
237236eleq1d 2672 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) ∈ ℤ ↔ (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ))
238233, 237bitr2d 268 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ ↔ (exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1))
23989adantl 481 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (𝐹𝑦) = (exp‘(i · 𝑦)))
240239eqeq2d 2620 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (𝑥 = (𝐹𝑦) ↔ 𝑥 = (exp‘(i · 𝑦))))
241231, 238, 2403imtr4d 282 . . . . . 6 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ → 𝑥 = (𝐹𝑦)))
242241reximdva 3000 . . . . 5 ((𝜑𝑥𝐶) → (∃𝑦𝐷 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ → ∃𝑦𝐷 𝑥 = (𝐹𝑦)))
243141, 242mpd 15 . . . 4 ((𝜑𝑥𝐶) → ∃𝑦𝐷 𝑥 = (𝐹𝑦))
244243ralrimiva 2949 . . 3 (𝜑 → ∀𝑥𝐶𝑦𝐷 𝑥 = (𝐹𝑦))
245 dffo3 6282 . . 3 (𝐹:𝐷onto𝐶 ↔ (𝐹:𝐷𝐶 ∧ ∀𝑥𝐶𝑦𝐷 𝑥 = (𝐹𝑦)))
24620, 244, 245sylanbrc 695 . 2 (𝜑𝐹:𝐷onto𝐶)
247 df-f1o 5811 . 2 (𝐹:𝐷1-1-onto𝐶 ↔ (𝐹:𝐷1-1𝐶𝐹:𝐷onto𝐶))
248114, 246, 247sylanbrc 695 1 (𝜑𝐹:𝐷1-1-onto𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383   = wceq 1475  wcel 1977  wne 2780  wral 2896  wrex 2897  wss 3540  {csn 4125   class class class wbr 4583  cmpt 4643  ccnv 5037  cres 5040  cima 5041   Fn wfn 5799  wf 5800  1-1wf1 5801  ontowfo 5802  1-1-ontowf1o 5803  cfv 5804  (class class class)co 6549  cc 9813  cr 9814  0cc0 9815  1c1 9816  ici 9817   + caddc 9818   · cmul 9820   < clt 9953  cle 9954  cmin 10145  -cneg 10146   / cdiv 10563  2c2 10947  0cn0 11169  cz 11254  [,]cicc 12049  cexp 12722  cre 13685  cim 13686  csqrt 13821  abscabs 13822  expce 14631  sincsin 14633  cosccos 14634  πcpi 14636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ioc 12051  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-fac 12923  df-bc 12952  df-hash 12980  df-shft 13655  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-limsup 14050  df-clim 14067  df-rlim 14068  df-sum 14265  df-ef 14637  df-sin 14639  df-cos 14640  df-pi 14642  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-hom 15793  df-cco 15794  df-rest 15906  df-topn 15907  df-0g 15925  df-gsum 15926  df-topgen 15927  df-pt 15928  df-prds 15931  df-xrs 15985  df-qtop 15990  df-imas 15991  df-xps 15993  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-mulg 17364  df-cntz 17573  df-cmn 18018  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-fbas 19564  df-fg 19565  df-cnfld 19568  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-cld 20633  df-ntr 20634  df-cls 20635  df-nei 20712  df-lp 20750  df-perf 20751  df-cn 20841  df-cnp 20842  df-haus 20929  df-tx 21175  df-hmeo 21368  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554  df-xms 21935  df-ms 21936  df-tms 21937  df-cncf 22489  df-limc 23436  df-dv 23437
This theorem is referenced by:  efif1o  24096  eff1olem  24098
  Copyright terms: Public domain W3C validator