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

Theorem efif1olem4 24490
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 3744 . . . . 5 ((𝜑𝑤𝐷) → 𝑤 ∈ ℝ)
3 ax-icn 10187 . . . . . . . . 9 i ∈ ℂ
4 recn 10218 . . . . . . . . 9 (𝑤 ∈ ℝ → 𝑤 ∈ ℂ)
5 mulcl 10212 . . . . . . . . 9 ((i ∈ ℂ ∧ 𝑤 ∈ ℂ) → (i · 𝑤) ∈ ℂ)
63, 4, 5sylancr 698 . . . . . . . 8 (𝑤 ∈ ℝ → (i · 𝑤) ∈ ℂ)
7 efcl 15012 . . . . . . . 8 ((i · 𝑤) ∈ ℂ → (exp‘(i · 𝑤)) ∈ ℂ)
86, 7syl 17 . . . . . . 7 (𝑤 ∈ ℝ → (exp‘(i · 𝑤)) ∈ ℂ)
9 absefi 15125 . . . . . . 7 (𝑤 ∈ ℝ → (abs‘(exp‘(i · 𝑤))) = 1)
10 absf 14276 . . . . . . . . 9 abs:ℂ⟶ℝ
11 ffn 6206 . . . . . . . . 9 (abs:ℂ⟶ℝ → abs Fn ℂ)
1210, 11ax-mp 5 . . . . . . . 8 abs Fn ℂ
13 fniniseg 6501 . . . . . . . 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 701 . . . . . 6 (𝑤 ∈ ℝ → (exp‘(i · 𝑤)) ∈ (abs “ {1}))
16 efif1o.2 . . . . . 6 𝐶 = (abs “ {1})
1715, 16syl6eleqr 2850 . . . . 5 (𝑤 ∈ ℝ → (exp‘(i · 𝑤)) ∈ 𝐶)
182, 17syl 17 . . . 4 ((𝜑𝑤𝐷) → (exp‘(i · 𝑤)) ∈ 𝐶)
19 efif1o.1 . . . 4 𝐹 = (𝑤𝐷 ↦ (exp‘(i · 𝑤)))
2018, 19fmptd 6548 . . 3 (𝜑𝐹:𝐷𝐶)
211ad2antrr 764 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝐷 ⊆ ℝ)
22 simplrl 819 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥𝐷)
2321, 22sseldd 3745 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 ∈ ℝ)
2423recnd 10260 . . . . . 6 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 ∈ ℂ)
25 simplrr 820 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑦𝐷)
2621, 25sseldd 3745 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑦 ∈ ℝ)
2726recnd 10260 . . . . . 6 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑦 ∈ ℂ)
2824, 27subcld 10584 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝑥𝑦) ∈ ℂ)
29 2re 11282 . . . . . . . . . . . 12 2 ∈ ℝ
30 pire 24409 . . . . . . . . . . . 12 π ∈ ℝ
3129, 30remulcli 10246 . . . . . . . . . . 11 (2 · π) ∈ ℝ
3231recni 10244 . . . . . . . . . 10 (2 · π) ∈ ℂ
33 2pos 11304 . . . . . . . . . . . 12 0 < 2
34 pipos 24411 . . . . . . . . . . . 12 0 < π
3529, 30, 33, 34mulgt0ii 10362 . . . . . . . . . . 11 0 < (2 · π)
3631, 35gt0ne0ii 10756 . . . . . . . . . 10 (2 · π) ≠ 0
37 divcl 10883 . . . . . . . . . 10 (((𝑥𝑦) ∈ ℂ ∧ (2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) → ((𝑥𝑦) / (2 · π)) ∈ ℂ)
3832, 36, 37mp3an23 1565 . . . . . . . . 9 ((𝑥𝑦) ∈ ℂ → ((𝑥𝑦) / (2 · π)) ∈ ℂ)
3928, 38syl 17 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((𝑥𝑦) / (2 · π)) ∈ ℂ)
40 absdiv 14234 . . . . . . . . . . . . 13 (((𝑥𝑦) ∈ ℂ ∧ (2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (abs‘(2 · π))))
4132, 36, 40mp3an23 1565 . . . . . . . . . . . 12 ((𝑥𝑦) ∈ ℂ → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (abs‘(2 · π))))
4228, 41syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (abs‘(2 · π))))
43 0re 10232 . . . . . . . . . . . . . 14 0 ∈ ℝ
4443, 31, 35ltleii 10352 . . . . . . . . . . . . 13 0 ≤ (2 · π)
45 absid 14235 . . . . . . . . . . . . 13 (((2 · π) ∈ ℝ ∧ 0 ≤ (2 · π)) → (abs‘(2 · π)) = (2 · π))
4631, 44, 45mp2an 710 . . . . . . . . . . . 12 (abs‘(2 · π)) = (2 · π)
4746oveq2i 6824 . . . . . . . . . . 11 ((abs‘(𝑥𝑦)) / (abs‘(2 · π))) = ((abs‘(𝑥𝑦)) / (2 · π))
4842, 47syl6eq 2810 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (2 · π)))
49 efif1olem4.4 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐷𝑦𝐷)) → (abs‘(𝑥𝑦)) < (2 · π))
5049adantr 472 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘(𝑥𝑦)) < (2 · π))
5132mulid1i 10234 . . . . . . . . . . . 12 ((2 · π) · 1) = (2 · π)
5250, 51syl6breqr 4846 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘(𝑥𝑦)) < ((2 · π) · 1))
5328abscld 14374 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘(𝑥𝑦)) ∈ ℝ)
54 1re 10231 . . . . . . . . . . . . 13 1 ∈ ℝ
5531, 35pm3.2i 470 . . . . . . . . . . . . 13 ((2 · π) ∈ ℝ ∧ 0 < (2 · π))
56 ltdivmul 11090 . . . . . . . . . . . . 13 (((abs‘(𝑥𝑦)) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((2 · π) ∈ ℝ ∧ 0 < (2 · π))) → (((abs‘(𝑥𝑦)) / (2 · π)) < 1 ↔ (abs‘(𝑥𝑦)) < ((2 · π) · 1)))
5754, 55, 56mp3an23 1565 . . . . . . . . . . . 12 ((abs‘(𝑥𝑦)) ∈ ℝ → (((abs‘(𝑥𝑦)) / (2 · π)) < 1 ↔ (abs‘(𝑥𝑦)) < ((2 · π) · 1)))
5853, 57syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (((abs‘(𝑥𝑦)) / (2 · π)) < 1 ↔ (abs‘(𝑥𝑦)) < ((2 · π) · 1)))
5952, 58mpbird 247 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((abs‘(𝑥𝑦)) / (2 · π)) < 1)
6048, 59eqbrtrd 4826 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) < 1)
6132, 36pm3.2i 470 . . . . . . . . . . . . . 14 ((2 · π) ∈ ℂ ∧ (2 · π) ≠ 0)
62 ine0 10657 . . . . . . . . . . . . . . 15 i ≠ 0
633, 62pm3.2i 470 . . . . . . . . . . . . . 14 (i ∈ ℂ ∧ i ≠ 0)
64 divcan5 10919 . . . . . . . . . . . . . 14 (((𝑥𝑦) ∈ ℂ ∧ ((2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) ∧ (i ∈ ℂ ∧ i ≠ 0)) → ((i · (𝑥𝑦)) / (i · (2 · π))) = ((𝑥𝑦) / (2 · π)))
6561, 63, 64mp3an23 1565 . . . . . . . . . . . . 13 ((𝑥𝑦) ∈ ℂ → ((i · (𝑥𝑦)) / (i · (2 · π))) = ((𝑥𝑦) / (2 · π)))
6628, 65syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((i · (𝑥𝑦)) / (i · (2 · π))) = ((𝑥𝑦) / (2 · π)))
673a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → i ∈ ℂ)
6867, 24, 27subdid 10678 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · (𝑥𝑦)) = ((i · 𝑥) − (i · 𝑦)))
6968fveq2d 6356 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · (𝑥𝑦))) = (exp‘((i · 𝑥) − (i · 𝑦))))
70 mulcl 10212 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
713, 24, 70sylancr 698 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · 𝑥) ∈ ℂ)
72 mulcl 10212 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝑦 ∈ ℂ) → (i · 𝑦) ∈ ℂ)
733, 27, 72sylancr 698 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · 𝑦) ∈ ℂ)
74 efsub 15029 . . . . . . . . . . . . . . 15 (((i · 𝑥) ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → (exp‘((i · 𝑥) − (i · 𝑦))) = ((exp‘(i · 𝑥)) / (exp‘(i · 𝑦))))
7571, 73, 74syl2anc 696 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘((i · 𝑥) − (i · 𝑦))) = ((exp‘(i · 𝑥)) / (exp‘(i · 𝑦))))
76 efcl 15012 . . . . . . . . . . . . . . . 16 ((i · 𝑦) ∈ ℂ → (exp‘(i · 𝑦)) ∈ ℂ)
7773, 76syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · 𝑦)) ∈ ℂ)
78 efne0 15026 . . . . . . . . . . . . . . . 16 ((i · 𝑦) ∈ ℂ → (exp‘(i · 𝑦)) ≠ 0)
7973, 78syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · 𝑦)) ≠ 0)
80 simpr 479 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝐹𝑥) = (𝐹𝑦))
81 oveq2 6821 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑥 → (i · 𝑤) = (i · 𝑥))
8281fveq2d 6356 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑥 → (exp‘(i · 𝑤)) = (exp‘(i · 𝑥)))
83 fvex 6362 . . . . . . . . . . . . . . . . . 18 (exp‘(i · 𝑥)) ∈ V
8482, 19, 83fvmpt 6444 . . . . . . . . . . . . . . . . 17 (𝑥𝐷 → (𝐹𝑥) = (exp‘(i · 𝑥)))
8522, 84syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝐹𝑥) = (exp‘(i · 𝑥)))
86 oveq2 6821 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑦 → (i · 𝑤) = (i · 𝑦))
8786fveq2d 6356 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑦 → (exp‘(i · 𝑤)) = (exp‘(i · 𝑦)))
88 fvex 6362 . . . . . . . . . . . . . . . . . 18 (exp‘(i · 𝑦)) ∈ V
8987, 19, 88fvmpt 6444 . . . . . . . . . . . . . . . . 17 (𝑦𝐷 → (𝐹𝑦) = (exp‘(i · 𝑦)))
9025, 89syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝐹𝑦) = (exp‘(i · 𝑦)))
9180, 85, 903eqtr3d 2802 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · 𝑥)) = (exp‘(i · 𝑦)))
9277, 79, 91diveq1bd 11041 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((exp‘(i · 𝑥)) / (exp‘(i · 𝑦))) = 1)
9369, 75, 923eqtrd 2798 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · (𝑥𝑦))) = 1)
94 mulcl 10212 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ (𝑥𝑦) ∈ ℂ) → (i · (𝑥𝑦)) ∈ ℂ)
953, 28, 94sylancr 698 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · (𝑥𝑦)) ∈ ℂ)
96 efeq1 24474 . . . . . . . . . . . . . 14 ((i · (𝑥𝑦)) ∈ ℂ → ((exp‘(i · (𝑥𝑦))) = 1 ↔ ((i · (𝑥𝑦)) / (i · (2 · π))) ∈ ℤ))
9795, 96syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((exp‘(i · (𝑥𝑦))) = 1 ↔ ((i · (𝑥𝑦)) / (i · (2 · π))) ∈ ℤ))
9893, 97mpbid 222 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((i · (𝑥𝑦)) / (i · (2 · π))) ∈ ℤ)
9966, 98eqeltrrd 2840 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((𝑥𝑦) / (2 · π)) ∈ ℤ)
100 nn0abscl 14251 . . . . . . . . . . 11 (((𝑥𝑦) / (2 · π)) ∈ ℤ → (abs‘((𝑥𝑦) / (2 · π))) ∈ ℕ0)
10199, 100syl 17 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) ∈ ℕ0)
102 nn0lt10b 11631 . . . . . . . . . 10 ((abs‘((𝑥𝑦) / (2 · π))) ∈ ℕ0 → ((abs‘((𝑥𝑦) / (2 · π))) < 1 ↔ (abs‘((𝑥𝑦) / (2 · π))) = 0))
103101, 102syl 17 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((abs‘((𝑥𝑦) / (2 · π))) < 1 ↔ (abs‘((𝑥𝑦) / (2 · π))) = 0))
10460, 103mpbid 222 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) = 0)
10539, 104abs00d 14384 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((𝑥𝑦) / (2 · π)) = 0)
106 diveq0 10887 . . . . . . . . 9 (((𝑥𝑦) ∈ ℂ ∧ (2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) → (((𝑥𝑦) / (2 · π)) = 0 ↔ (𝑥𝑦) = 0))
10732, 36, 106mp3an23 1565 . . . . . . . 8 ((𝑥𝑦) ∈ ℂ → (((𝑥𝑦) / (2 · π)) = 0 ↔ (𝑥𝑦) = 0))
10828, 107syl 17 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (((𝑥𝑦) / (2 · π)) = 0 ↔ (𝑥𝑦) = 0))
109105, 108mpbid 222 . . . . . 6 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝑥𝑦) = 0)
11024, 27, 109subeq0d 10592 . . . . 5 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 = 𝑦)
111110ex 449 . . . 4 ((𝜑 ∧ (𝑥𝐷𝑦𝐷)) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
112111ralrimivva 3109 . . 3 (𝜑 → ∀𝑥𝐷𝑦𝐷 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
113 dff13 6675 . . 3 (𝐹:𝐷1-1𝐶 ↔ (𝐹:𝐷𝐶 ∧ ∀𝑥𝐷𝑦𝐷 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
11420, 112, 113sylanbrc 701 . 2 (𝜑𝐹:𝐷1-1𝐶)
115 oveq1 6820 . . . . . . . . 9 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → (𝑧𝑦) = ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))
116115oveq1d 6828 . . . . . . . 8 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → ((𝑧𝑦) / (2 · π)) = (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)))
117116eleq1d 2824 . . . . . . 7 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → (((𝑧𝑦) / (2 · π)) ∈ ℤ ↔ (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ))
118117rexbidv 3190 . . . . . 6 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → (∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ ↔ ∃𝑦𝐷 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ))
119 efif1olem4.5 . . . . . . . 8 ((𝜑𝑧 ∈ ℝ) → ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ)
120119ralrimiva 3104 . . . . . . 7 (𝜑 → ∀𝑧 ∈ ℝ ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ)
121120adantr 472 . . . . . 6 ((𝜑𝑥𝐶) → ∀𝑧 ∈ ℝ ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ)
122 neghalfpire 24416 . . . . . . . . 9 -(π / 2) ∈ ℝ
123 halfpire 24415 . . . . . . . . 9 (π / 2) ∈ ℝ
124 iccssre 12448 . . . . . . . . 9 ((-(π / 2) ∈ ℝ ∧ (π / 2) ∈ ℝ) → (-(π / 2)[,](π / 2)) ⊆ ℝ)
125122, 123, 124mp2an 710 . . . . . . . 8 (-(π / 2)[,](π / 2)) ⊆ ℝ
12619, 16efif1olem3 24489 . . . . . . . . 9 ((𝜑𝑥𝐶) → (ℑ‘(√‘𝑥)) ∈ (-1[,]1))
127 resinf1o 24481 . . . . . . . . . . . 12 (sin ↾ (-(π / 2)[,](π / 2))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1)
128 efif1olem4.6 . . . . . . . . . . . . 13 𝑆 = (sin ↾ (-(π / 2)[,](π / 2)))
129 f1oeq1 6288 . . . . . . . . . . . . 13 (𝑆 = (sin ↾ (-(π / 2)[,](π / 2))) → (𝑆:(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) ↔ (sin ↾ (-(π / 2)[,](π / 2))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1)))
130128, 129ax-mp 5 . . . . . . . . . . . 12 (𝑆:(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) ↔ (sin ↾ (-(π / 2)[,](π / 2))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1))
131127, 130mpbir 221 . . . . . . . . . . 11 𝑆:(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1)
132 f1ocnv 6310 . . . . . . . . . . 11 (𝑆:(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) → 𝑆:(-1[,]1)–1-1-onto→(-(π / 2)[,](π / 2)))
133 f1of 6298 . . . . . . . . . . 11 (𝑆:(-1[,]1)–1-1-onto→(-(π / 2)[,](π / 2)) → 𝑆:(-1[,]1)⟶(-(π / 2)[,](π / 2)))
134131, 132, 133mp2b 10 . . . . . . . . . 10 𝑆:(-1[,]1)⟶(-(π / 2)[,](π / 2))
135134ffvelrni 6521 . . . . . . . . 9 ((ℑ‘(√‘𝑥)) ∈ (-1[,]1) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π / 2)))
136126, 135syl 17 . . . . . . . 8 ((𝜑𝑥𝐶) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π / 2)))
137125, 136sseldi 3742 . . . . . . 7 ((𝜑𝑥𝐶) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℝ)
138 remulcl 10213 . . . . . . 7 ((2 ∈ ℝ ∧ (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℝ) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
13929, 137, 138sylancr 698 . . . . . 6 ((𝜑𝑥𝐶) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
140118, 121, 139rspcdva 3455 . . . . 5 ((𝜑𝑥𝐶) → ∃𝑦𝐷 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ)
141 oveq1 6820 . . . . . . . 8 ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1 → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))) = (1 · (exp‘(i · 𝑦))))
1423a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → i ∈ ℂ)
143139adantr 472 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
144143recnd 10260 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
1451ad2antrr 764 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝐷 ⊆ ℝ)
146 simpr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝑦𝐷)
147145, 146sseldd 3745 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝑦 ∈ ℝ)
148147recnd 10260 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝑦 ∈ ℂ)
149142, 144, 148subdid 10678 . . . . . . . . . . . . 13 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) = ((i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) − (i · 𝑦)))
150149oveq1d 6828 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦)) = (((i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) − (i · 𝑦)) + (i · 𝑦)))
151 mulcl 10212 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) ∈ ℂ)
1523, 144, 151sylancr 698 . . . . . . . . . . . . 13 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) ∈ ℂ)
1533, 148, 72sylancr 698 . . . . . . . . . . . . 13 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · 𝑦) ∈ ℂ)
154152, 153npcand 10588 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (((i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) − (i · 𝑦)) + (i · 𝑦)) = (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))))
155150, 154eqtrd 2794 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦)) = (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))))
156155fveq2d 6356 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦))) = (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))))
157144, 148subcld 10584 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ)
158 mulcl 10212 . . . . . . . . . . . 12 ((i ∈ ℂ ∧ ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ) → (i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ)
1593, 157, 158sylancr 698 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ)
160 efadd 15023 . . . . . . . . . . 11 (((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → (exp‘((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦))) = ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))))
161159, 153, 160syl2anc 696 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦))) = ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))))
162137recnd 10260 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ)
163 2cn 11283 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
164 mul12 10394 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 2 ∈ ℂ ∧ (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) = (2 · (i · (𝑆‘(ℑ‘(√‘𝑥))))))
1653, 163, 164mp3an12 1563 . . . . . . . . . . . . . . 15 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) = (2 · (i · (𝑆‘(ℑ‘(√‘𝑥))))))
166162, 165syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) = (2 · (i · (𝑆‘(ℑ‘(√‘𝑥))))))
167166fveq2d 6356 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = (exp‘(2 · (i · (𝑆‘(ℑ‘(√‘𝑥)))))))
168 mulcl 10212 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ) → (i · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
1693, 162, 168sylancr 698 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (i · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
170 2z 11601 . . . . . . . . . . . . . 14 2 ∈ ℤ
171 efexp 15030 . . . . . . . . . . . . . 14 (((i · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ ∧ 2 ∈ ℤ) → (exp‘(2 · (i · (𝑆‘(ℑ‘(√‘𝑥)))))) = ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2))
172169, 170, 171sylancl 697 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → (exp‘(2 · (i · (𝑆‘(ℑ‘(√‘𝑥)))))) = ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2))
173167, 172eqtrd 2794 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2))
174137recoscld 15073 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → (cos‘(𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
175 simpr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥𝐶) → 𝑥𝐶)
176175, 16syl6eleq 2849 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝑥 ∈ (abs “ {1}))
177 fniniseg 6501 . . . . . . . . . . . . . . . . . . . . 21 (abs Fn ℂ → (𝑥 ∈ (abs “ {1}) ↔ (𝑥 ∈ ℂ ∧ (abs‘𝑥) = 1)))
17812, 177ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (abs “ {1}) ↔ (𝑥 ∈ ℂ ∧ (abs‘𝑥) = 1))
179176, 178sylib 208 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (𝑥 ∈ ℂ ∧ (abs‘𝑥) = 1))
180179simpld 477 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → 𝑥 ∈ ℂ)
181180sqrtcld 14375 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → (√‘𝑥) ∈ ℂ)
182181recld 14133 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → (ℜ‘(√‘𝑥)) ∈ ℝ)
183 cosq14ge0 24462 . . . . . . . . . . . . . . . . 17 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π / 2)) → 0 ≤ (cos‘(𝑆‘(ℑ‘(√‘𝑥)))))
184136, 183syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → 0 ≤ (cos‘(𝑆‘(ℑ‘(√‘𝑥)))))
185180sqrtrege0d 14376 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → 0 ≤ (ℜ‘(√‘𝑥)))
186 sincossq 15105 . . . . . . . . . . . . . . . . . . . 20 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ → (((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = 1)
187162, 186syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = 1)
188180sqsqrtd 14377 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥𝐶) → ((√‘𝑥)↑2) = 𝑥)
189188fveq2d 6356 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (abs‘((√‘𝑥)↑2)) = (abs‘𝑥))
190 2nn0 11501 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℕ0
191 absexp 14243 . . . . . . . . . . . . . . . . . . . . 21 (((√‘𝑥) ∈ ℂ ∧ 2 ∈ ℕ0) → (abs‘((√‘𝑥)↑2)) = ((abs‘(√‘𝑥))↑2))
192181, 190, 191sylancl 697 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (abs‘((√‘𝑥)↑2)) = ((abs‘(√‘𝑥))↑2))
193179simprd 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (abs‘𝑥) = 1)
194189, 192, 1933eqtr3d 2802 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → ((abs‘(√‘𝑥))↑2) = 1)
195181absvalsq2d 14381 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → ((abs‘(√‘𝑥))↑2) = (((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)))
196187, 194, 1953eqtr2d 2800 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → (((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = (((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)))
197128fveq1i 6353 . . . . . . . . . . . . . . . . . . . . 21 (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = ((sin ↾ (-(π / 2)[,](π / 2)))‘(𝑆‘(ℑ‘(√‘𝑥))))
198 fvres 6368 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π / 2)) → ((sin ↾ (-(π / 2)[,](π / 2)))‘(𝑆‘(ℑ‘(√‘𝑥)))) = (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))
199136, 198syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥𝐶) → ((sin ↾ (-(π / 2)[,](π / 2)))‘(𝑆‘(ℑ‘(√‘𝑥)))) = (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))
200197, 199syl5eq 2806 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))
201 f1ocnvfv2 6696 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆:(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) ∧ (ℑ‘(√‘𝑥)) ∈ (-1[,]1)) → (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℑ‘(√‘𝑥)))
202131, 126, 201sylancr 698 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℑ‘(√‘𝑥)))
203200, 202eqtr3d 2796 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (sin‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℑ‘(√‘𝑥)))
204203oveq1d 6828 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) = ((ℑ‘(√‘𝑥))↑2))
205196, 204oveq12d 6831 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) − ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = ((((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)) − ((ℑ‘(√‘𝑥))↑2)))
206162sincld 15059 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (sin‘(𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
207206sqcld 13200 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) ∈ ℂ)
208162coscld 15060 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (cos‘(𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
209208sqcld 13200 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) ∈ ℂ)
210207, 209pncan2d 10586 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) − ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2))
211182recnd 10260 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (ℜ‘(√‘𝑥)) ∈ ℂ)
212211sqcld 13200 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((ℜ‘(√‘𝑥))↑2) ∈ ℂ)
213204, 207eqeltrrd 2840 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((ℑ‘(√‘𝑥))↑2) ∈ ℂ)
214212, 213pncand 10585 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)) − ((ℑ‘(√‘𝑥))↑2)) = ((ℜ‘(√‘𝑥))↑2))
215205, 210, 2143eqtr3d 2802 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) = ((ℜ‘(√‘𝑥))↑2))
216174, 182, 184, 185, 215sq11d 13239 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (cos‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℜ‘(√‘𝑥)))
217203oveq2d 6829 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥))))) = (i · (ℑ‘(√‘𝑥))))
218216, 217oveq12d 6831 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → ((cos‘(𝑆‘(ℑ‘(√‘𝑥)))) + (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))) = ((ℜ‘(√‘𝑥)) + (i · (ℑ‘(√‘𝑥)))))
219 efival 15081 . . . . . . . . . . . . . . 15 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ → (exp‘(i · (𝑆‘(ℑ‘(√‘𝑥))))) = ((cos‘(𝑆‘(ℑ‘(√‘𝑥)))) + (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))))
220162, 219syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (exp‘(i · (𝑆‘(ℑ‘(√‘𝑥))))) = ((cos‘(𝑆‘(ℑ‘(√‘𝑥)))) + (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))))
221181replimd 14136 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (√‘𝑥) = ((ℜ‘(√‘𝑥)) + (i · (ℑ‘(√‘𝑥)))))
222218, 220, 2213eqtr4d 2804 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → (exp‘(i · (𝑆‘(ℑ‘(√‘𝑥))))) = (√‘𝑥))
223222oveq1d 6828 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2) = ((√‘𝑥)↑2))
224173, 223, 1883eqtrd 2798 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = 𝑥)
225224adantr 472 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = 𝑥)
226156, 161, 2253eqtr3d 2802 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))) = 𝑥)
227153, 76syl 17 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘(i · 𝑦)) ∈ ℂ)
228227mulid2d 10250 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (1 · (exp‘(i · 𝑦))) = (exp‘(i · 𝑦)))
229226, 228eqeq12d 2775 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))) = (1 · (exp‘(i · 𝑦))) ↔ 𝑥 = (exp‘(i · 𝑦))))
230141, 229syl5ib 234 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1 → 𝑥 = (exp‘(i · 𝑦))))
231 efeq1 24474 . . . . . . . . 9 ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1 ↔ ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) ∈ ℤ))
232159, 231syl 17 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1 ↔ ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) ∈ ℤ))
233 divcan5 10919 . . . . . . . . . . 11 ((((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ ∧ ((2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) ∧ (i ∈ ℂ ∧ i ≠ 0)) → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) = (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)))
23461, 63, 233mp3an23 1565 . . . . . . . . . 10 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) = (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)))
235157, 234syl 17 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) = (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)))
236235eleq1d 2824 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) ∈ ℤ ↔ (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ))
237232, 236bitr2d 269 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ ↔ (exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1))
23889adantl 473 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (𝐹𝑦) = (exp‘(i · 𝑦)))
239238eqeq2d 2770 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (𝑥 = (𝐹𝑦) ↔ 𝑥 = (exp‘(i · 𝑦))))
240230, 237, 2393imtr4d 283 . . . . . 6 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ → 𝑥 = (𝐹𝑦)))
241240reximdva 3155 . . . . 5 ((𝜑𝑥𝐶) → (∃𝑦𝐷 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ → ∃𝑦𝐷 𝑥 = (𝐹𝑦)))
242140, 241mpd 15 . . . 4 ((𝜑𝑥𝐶) → ∃𝑦𝐷 𝑥 = (𝐹𝑦))
243242ralrimiva 3104 . . 3 (𝜑 → ∀𝑥𝐶𝑦𝐷 𝑥 = (𝐹𝑦))
244 dffo3 6537 . . 3 (𝐹:𝐷onto𝐶 ↔ (𝐹:𝐷𝐶 ∧ ∀𝑥𝐶𝑦𝐷 𝑥 = (𝐹𝑦)))
24520, 243, 244sylanbrc 701 . 2 (𝜑𝐹:𝐷onto𝐶)
246 df-f1o 6056 . 2 (𝐹:𝐷1-1-onto𝐶 ↔ (𝐹:𝐷1-1𝐶𝐹:𝐷onto𝐶))
247114, 245, 246sylanbrc 701 1 (𝜑𝐹:𝐷1-1-onto𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1632  wcel 2139  wne 2932  wral 3050  wrex 3051  wss 3715  {csn 4321   class class class wbr 4804  cmpt 4881  ccnv 5265  cres 5268  cima 5269   Fn wfn 6044  wf 6045  1-1wf1 6046  ontowfo 6047  1-1-ontowf1o 6048  cfv 6049  (class class class)co 6813  cc 10126  cr 10127  0cc0 10128  1c1 10129  ici 10130   + caddc 10131   · cmul 10133   < clt 10266  cle 10267  cmin 10458  -cneg 10459   / cdiv 10876  2c2 11262  0cn0 11484  cz 11569  [,]cicc 12371  cexp 13054  cre 14036  cim 14037  csqrt 14172  abscabs 14173  expce 14991  sincsin 14993  cosccos 14994  πcpi 14996
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206  ax-addf 10207  ax-mulf 10208
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-of 7062  df-om 7231  df-1st 7333  df-2nd 7334  df-supp 7464  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-er 7911  df-map 8025  df-pm 8026  df-ixp 8075  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-fsupp 8441  df-fi 8482  df-sup 8513  df-inf 8514  df-oi 8580  df-card 8955  df-cda 9182  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-z 11570  df-dec 11686  df-uz 11880  df-q 11982  df-rp 12026  df-xneg 12139  df-xadd 12140  df-xmul 12141  df-ioo 12372  df-ioc 12373  df-ico 12374  df-icc 12375  df-fz 12520  df-fzo 12660  df-fl 12787  df-mod 12863  df-seq 12996  df-exp 13055  df-fac 13255  df-bc 13284  df-hash 13312  df-shft 14006  df-cj 14038  df-re 14039  df-im 14040  df-sqrt 14174  df-abs 14175  df-limsup 14401  df-clim 14418  df-rlim 14419  df-sum 14616  df-ef 14997  df-sin 14999  df-cos 15000  df-pi 15002  df-struct 16061  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-ress 16067  df-plusg 16156  df-mulr 16157  df-starv 16158  df-sca 16159  df-vsca 16160  df-ip 16161  df-tset 16162  df-ple 16163  df-ds 16166  df-unif 16167  df-hom 16168  df-cco 16169  df-rest 16285  df-topn 16286  df-0g 16304  df-gsum 16305  df-topgen 16306  df-pt 16307  df-prds 16310  df-xrs 16364  df-qtop 16369  df-imas 16370  df-xps 16372  df-mre 16448  df-mrc 16449  df-acs 16451  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-submnd 17537  df-mulg 17742  df-cntz 17950  df-cmn 18395  df-psmet 19940  df-xmet 19941  df-met 19942  df-bl 19943  df-mopn 19944  df-fbas 19945  df-fg 19946  df-cnfld 19949  df-top 20901  df-topon 20918  df-topsp 20939  df-bases 20952  df-cld 21025  df-ntr 21026  df-cls 21027  df-nei 21104  df-lp 21142  df-perf 21143  df-cn 21233  df-cnp 21234  df-haus 21321  df-tx 21567  df-hmeo 21760  df-fil 21851  df-fm 21943  df-flim 21944  df-flf 21945  df-xms 22326  df-ms 22327  df-tms 22328  df-cncf 22882  df-limc 23829  df-dv 23830
This theorem is referenced by:  efif1o  24491  eff1olem  24493
  Copyright terms: Public domain W3C validator