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

Theorem efif1olem4 24012
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 3567 . . . . 5 ((𝜑𝑤𝐷) → 𝑤 ∈ ℝ)
3 ax-icn 9851 . . . . . . . . 9 i ∈ ℂ
4 recn 9882 . . . . . . . . 9 (𝑤 ∈ ℝ → 𝑤 ∈ ℂ)
5 mulcl 9876 . . . . . . . . 9 ((i ∈ ℂ ∧ 𝑤 ∈ ℂ) → (i · 𝑤) ∈ ℂ)
63, 4, 5sylancr 693 . . . . . . . 8 (𝑤 ∈ ℝ → (i · 𝑤) ∈ ℂ)
7 efcl 14598 . . . . . . . 8 ((i · 𝑤) ∈ ℂ → (exp‘(i · 𝑤)) ∈ ℂ)
86, 7syl 17 . . . . . . 7 (𝑤 ∈ ℝ → (exp‘(i · 𝑤)) ∈ ℂ)
9 absefi 14711 . . . . . . 7 (𝑤 ∈ ℝ → (abs‘(exp‘(i · 𝑤))) = 1)
10 absf 13871 . . . . . . . . 9 abs:ℂ⟶ℝ
11 ffn 5944 . . . . . . . . 9 (abs:ℂ⟶ℝ → abs Fn ℂ)
1210, 11ax-mp 5 . . . . . . . 8 abs Fn ℂ
13 fniniseg 6231 . . . . . . . 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 694 . . . . . 6 (𝑤 ∈ ℝ → (exp‘(i · 𝑤)) ∈ (abs “ {1}))
16 efif1o.2 . . . . . 6 𝐶 = (abs “ {1})
1715, 16syl6eleqr 2698 . . . . 5 (𝑤 ∈ ℝ → (exp‘(i · 𝑤)) ∈ 𝐶)
182, 17syl 17 . . . 4 ((𝜑𝑤𝐷) → (exp‘(i · 𝑤)) ∈ 𝐶)
19 efif1o.1 . . . 4 𝐹 = (𝑤𝐷 ↦ (exp‘(i · 𝑤)))
2018, 19fmptd 6277 . . 3 (𝜑𝐹:𝐷𝐶)
211ad2antrr 757 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝐷 ⊆ ℝ)
22 simplrl 795 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥𝐷)
2321, 22sseldd 3568 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 ∈ ℝ)
2423recnd 9924 . . . . . 6 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 ∈ ℂ)
25 simplrr 796 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑦𝐷)
2621, 25sseldd 3568 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑦 ∈ ℝ)
2726recnd 9924 . . . . . 6 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑦 ∈ ℂ)
2824, 27subcld 10243 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝑥𝑦) ∈ ℂ)
29 2re 10937 . . . . . . . . . . . 12 2 ∈ ℝ
30 pire 23931 . . . . . . . . . . . 12 π ∈ ℝ
3129, 30remulcli 9910 . . . . . . . . . . 11 (2 · π) ∈ ℝ
3231recni 9908 . . . . . . . . . 10 (2 · π) ∈ ℂ
33 2pos 10959 . . . . . . . . . . . 12 0 < 2
34 pipos 23933 . . . . . . . . . . . 12 0 < π
3529, 30, 33, 34mulgt0ii 10021 . . . . . . . . . . 11 0 < (2 · π)
3631, 35gt0ne0ii 10413 . . . . . . . . . 10 (2 · π) ≠ 0
37 divcl 10540 . . . . . . . . . 10 (((𝑥𝑦) ∈ ℂ ∧ (2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) → ((𝑥𝑦) / (2 · π)) ∈ ℂ)
3832, 36, 37mp3an23 1407 . . . . . . . . 9 ((𝑥𝑦) ∈ ℂ → ((𝑥𝑦) / (2 · π)) ∈ ℂ)
3928, 38syl 17 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((𝑥𝑦) / (2 · π)) ∈ ℂ)
40 absdiv 13829 . . . . . . . . . . . . 13 (((𝑥𝑦) ∈ ℂ ∧ (2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (abs‘(2 · π))))
4132, 36, 40mp3an23 1407 . . . . . . . . . . . 12 ((𝑥𝑦) ∈ ℂ → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (abs‘(2 · π))))
4228, 41syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (abs‘(2 · π))))
43 0re 9896 . . . . . . . . . . . . . 14 0 ∈ ℝ
4443, 31, 35ltleii 10011 . . . . . . . . . . . . 13 0 ≤ (2 · π)
45 absid 13830 . . . . . . . . . . . . 13 (((2 · π) ∈ ℝ ∧ 0 ≤ (2 · π)) → (abs‘(2 · π)) = (2 · π))
4631, 44, 45mp2an 703 . . . . . . . . . . . 12 (abs‘(2 · π)) = (2 · π)
4746oveq2i 6538 . . . . . . . . . . 11 ((abs‘(𝑥𝑦)) / (abs‘(2 · π))) = ((abs‘(𝑥𝑦)) / (2 · π))
4842, 47syl6eq 2659 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (2 · π)))
49 efif1olem4.4 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐷𝑦𝐷)) → (abs‘(𝑥𝑦)) < (2 · π))
5049adantr 479 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘(𝑥𝑦)) < (2 · π))
5132mulid1i 9898 . . . . . . . . . . . 12 ((2 · π) · 1) = (2 · π)
5250, 51syl6breqr 4619 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘(𝑥𝑦)) < ((2 · π) · 1))
5328abscld 13969 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘(𝑥𝑦)) ∈ ℝ)
54 1re 9895 . . . . . . . . . . . . 13 1 ∈ ℝ
5531, 35pm3.2i 469 . . . . . . . . . . . . 13 ((2 · π) ∈ ℝ ∧ 0 < (2 · π))
56 ltdivmul 10747 . . . . . . . . . . . . 13 (((abs‘(𝑥𝑦)) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((2 · π) ∈ ℝ ∧ 0 < (2 · π))) → (((abs‘(𝑥𝑦)) / (2 · π)) < 1 ↔ (abs‘(𝑥𝑦)) < ((2 · π) · 1)))
5754, 55, 56mp3an23 1407 . . . . . . . . . . . 12 ((abs‘(𝑥𝑦)) ∈ ℝ → (((abs‘(𝑥𝑦)) / (2 · π)) < 1 ↔ (abs‘(𝑥𝑦)) < ((2 · π) · 1)))
5853, 57syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (((abs‘(𝑥𝑦)) / (2 · π)) < 1 ↔ (abs‘(𝑥𝑦)) < ((2 · π) · 1)))
5952, 58mpbird 245 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((abs‘(𝑥𝑦)) / (2 · π)) < 1)
6048, 59eqbrtrd 4599 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) < 1)
6132, 36pm3.2i 469 . . . . . . . . . . . . . 14 ((2 · π) ∈ ℂ ∧ (2 · π) ≠ 0)
62 ine0 10316 . . . . . . . . . . . . . . 15 i ≠ 0
633, 62pm3.2i 469 . . . . . . . . . . . . . 14 (i ∈ ℂ ∧ i ≠ 0)
64 divcan5 10576 . . . . . . . . . . . . . 14 (((𝑥𝑦) ∈ ℂ ∧ ((2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) ∧ (i ∈ ℂ ∧ i ≠ 0)) → ((i · (𝑥𝑦)) / (i · (2 · π))) = ((𝑥𝑦) / (2 · π)))
6561, 63, 64mp3an23 1407 . . . . . . . . . . . . 13 ((𝑥𝑦) ∈ ℂ → ((i · (𝑥𝑦)) / (i · (2 · π))) = ((𝑥𝑦) / (2 · π)))
6628, 65syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((i · (𝑥𝑦)) / (i · (2 · π))) = ((𝑥𝑦) / (2 · π)))
673a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → i ∈ ℂ)
6867, 24, 27subdid 10336 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · (𝑥𝑦)) = ((i · 𝑥) − (i · 𝑦)))
6968fveq2d 6092 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · (𝑥𝑦))) = (exp‘((i · 𝑥) − (i · 𝑦))))
70 mulcl 9876 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
713, 24, 70sylancr 693 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · 𝑥) ∈ ℂ)
72 mulcl 9876 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝑦 ∈ ℂ) → (i · 𝑦) ∈ ℂ)
733, 27, 72sylancr 693 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · 𝑦) ∈ ℂ)
74 efsub 14615 . . . . . . . . . . . . . . 15 (((i · 𝑥) ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → (exp‘((i · 𝑥) − (i · 𝑦))) = ((exp‘(i · 𝑥)) / (exp‘(i · 𝑦))))
7571, 73, 74syl2anc 690 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘((i · 𝑥) − (i · 𝑦))) = ((exp‘(i · 𝑥)) / (exp‘(i · 𝑦))))
76 efcl 14598 . . . . . . . . . . . . . . . 16 ((i · 𝑦) ∈ ℂ → (exp‘(i · 𝑦)) ∈ ℂ)
7773, 76syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · 𝑦)) ∈ ℂ)
78 efne0 14612 . . . . . . . . . . . . . . . 16 ((i · 𝑦) ∈ ℂ → (exp‘(i · 𝑦)) ≠ 0)
7973, 78syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · 𝑦)) ≠ 0)
80 simpr 475 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝐹𝑥) = (𝐹𝑦))
81 oveq2 6535 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑥 → (i · 𝑤) = (i · 𝑥))
8281fveq2d 6092 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑥 → (exp‘(i · 𝑤)) = (exp‘(i · 𝑥)))
83 fvex 6098 . . . . . . . . . . . . . . . . . 18 (exp‘(i · 𝑥)) ∈ V
8482, 19, 83fvmpt 6176 . . . . . . . . . . . . . . . . 17 (𝑥𝐷 → (𝐹𝑥) = (exp‘(i · 𝑥)))
8522, 84syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝐹𝑥) = (exp‘(i · 𝑥)))
86 oveq2 6535 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑦 → (i · 𝑤) = (i · 𝑦))
8786fveq2d 6092 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑦 → (exp‘(i · 𝑤)) = (exp‘(i · 𝑦)))
88 fvex 6098 . . . . . . . . . . . . . . . . . 18 (exp‘(i · 𝑦)) ∈ V
8987, 19, 88fvmpt 6176 . . . . . . . . . . . . . . . . 17 (𝑦𝐷 → (𝐹𝑦) = (exp‘(i · 𝑦)))
9025, 89syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝐹𝑦) = (exp‘(i · 𝑦)))
9180, 85, 903eqtr3d 2651 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · 𝑥)) = (exp‘(i · 𝑦)))
9277, 79, 91diveq1bd 10698 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((exp‘(i · 𝑥)) / (exp‘(i · 𝑦))) = 1)
9369, 75, 923eqtrd 2647 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · (𝑥𝑦))) = 1)
94 mulcl 9876 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ (𝑥𝑦) ∈ ℂ) → (i · (𝑥𝑦)) ∈ ℂ)
953, 28, 94sylancr 693 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · (𝑥𝑦)) ∈ ℂ)
96 efeq1 23996 . . . . . . . . . . . . . 14 ((i · (𝑥𝑦)) ∈ ℂ → ((exp‘(i · (𝑥𝑦))) = 1 ↔ ((i · (𝑥𝑦)) / (i · (2 · π))) ∈ ℤ))
9795, 96syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((exp‘(i · (𝑥𝑦))) = 1 ↔ ((i · (𝑥𝑦)) / (i · (2 · π))) ∈ ℤ))
9893, 97mpbid 220 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((i · (𝑥𝑦)) / (i · (2 · π))) ∈ ℤ)
9966, 98eqeltrrd 2688 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((𝑥𝑦) / (2 · π)) ∈ ℤ)
100 nn0abscl 13846 . . . . . . . . . . 11 (((𝑥𝑦) / (2 · π)) ∈ ℤ → (abs‘((𝑥𝑦) / (2 · π))) ∈ ℕ0)
10199, 100syl 17 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) ∈ ℕ0)
102 nn0lt10b 11272 . . . . . . . . . 10 ((abs‘((𝑥𝑦) / (2 · π))) ∈ ℕ0 → ((abs‘((𝑥𝑦) / (2 · π))) < 1 ↔ (abs‘((𝑥𝑦) / (2 · π))) = 0))
103101, 102syl 17 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((abs‘((𝑥𝑦) / (2 · π))) < 1 ↔ (abs‘((𝑥𝑦) / (2 · π))) = 0))
10460, 103mpbid 220 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) = 0)
10539, 104abs00d 13979 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((𝑥𝑦) / (2 · π)) = 0)
106 diveq0 10544 . . . . . . . . 9 (((𝑥𝑦) ∈ ℂ ∧ (2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) → (((𝑥𝑦) / (2 · π)) = 0 ↔ (𝑥𝑦) = 0))
10732, 36, 106mp3an23 1407 . . . . . . . 8 ((𝑥𝑦) ∈ ℂ → (((𝑥𝑦) / (2 · π)) = 0 ↔ (𝑥𝑦) = 0))
10828, 107syl 17 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (((𝑥𝑦) / (2 · π)) = 0 ↔ (𝑥𝑦) = 0))
109105, 108mpbid 220 . . . . . 6 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝑥𝑦) = 0)
11024, 27, 109subeq0d 10251 . . . . 5 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 = 𝑦)
111110ex 448 . . . 4 ((𝜑 ∧ (𝑥𝐷𝑦𝐷)) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
112111ralrimivva 2953 . . 3 (𝜑 → ∀𝑥𝐷𝑦𝐷 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
113 dff13 6394 . . 3 (𝐹:𝐷1-1𝐶 ↔ (𝐹:𝐷𝐶 ∧ ∀𝑥𝐷𝑦𝐷 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
11420, 112, 113sylanbrc 694 . 2 (𝜑𝐹:𝐷1-1𝐶)
115 neghalfpire 23938 . . . . . . . . 9 -(π / 2) ∈ ℝ
116 halfpire 23937 . . . . . . . . 9 (π / 2) ∈ ℝ
117 iccssre 12082 . . . . . . . . 9 ((-(π / 2) ∈ ℝ ∧ (π / 2) ∈ ℝ) → (-(π / 2)[,](π / 2)) ⊆ ℝ)
118115, 116, 117mp2an 703 . . . . . . . 8 (-(π / 2)[,](π / 2)) ⊆ ℝ
11919, 16efif1olem3 24011 . . . . . . . . 9 ((𝜑𝑥𝐶) → (ℑ‘(√‘𝑥)) ∈ (-1[,]1))
120 resinf1o 24003 . . . . . . . . . . . 12 (sin ↾ (-(π / 2)[,](π / 2))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1)
121 efif1olem4.6 . . . . . . . . . . . . 13 𝑆 = (sin ↾ (-(π / 2)[,](π / 2)))
122 f1oeq1 6025 . . . . . . . . . . . . 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 219 . . . . . . . . . . 11 𝑆:(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1)
125 f1ocnv 6047 . . . . . . . . . . 11 (𝑆:(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) → 𝑆:(-1[,]1)–1-1-onto→(-(π / 2)[,](π / 2)))
126 f1of 6035 . . . . . . . . . . 11 (𝑆:(-1[,]1)–1-1-onto→(-(π / 2)[,](π / 2)) → 𝑆:(-1[,]1)⟶(-(π / 2)[,](π / 2)))
127124, 125, 126mp2b 10 . . . . . . . . . 10 𝑆:(-1[,]1)⟶(-(π / 2)[,](π / 2))
128127ffvelrni 6251 . . . . . . . . 9 ((ℑ‘(√‘𝑥)) ∈ (-1[,]1) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π / 2)))
129119, 128syl 17 . . . . . . . 8 ((𝜑𝑥𝐶) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π / 2)))
130118, 129sseldi 3565 . . . . . . 7 ((𝜑𝑥𝐶) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℝ)
131 remulcl 9877 . . . . . . 7 ((2 ∈ ℝ ∧ (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℝ) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
13229, 130, 131sylancr 693 . . . . . 6 ((𝜑𝑥𝐶) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
133 efif1olem4.5 . . . . . . . 8 ((𝜑𝑧 ∈ ℝ) → ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ)
134133ralrimiva 2948 . . . . . . 7 (𝜑 → ∀𝑧 ∈ ℝ ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ)
135134adantr 479 . . . . . 6 ((𝜑𝑥𝐶) → ∀𝑧 ∈ ℝ ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ)
136 oveq1 6534 . . . . . . . . . 10 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → (𝑧𝑦) = ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))
137136oveq1d 6542 . . . . . . . . 9 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → ((𝑧𝑦) / (2 · π)) = (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)))
138137eleq1d 2671 . . . . . . . 8 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → (((𝑧𝑦) / (2 · π)) ∈ ℤ ↔ (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ))
139138rexbidv 3033 . . . . . . 7 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → (∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ ↔ ∃𝑦𝐷 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ))
140139rspcv 3277 . . . . . 6 ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ → (∀𝑧 ∈ ℝ ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ → ∃𝑦𝐷 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ))
141132, 135, 140sylc 62 . . . . 5 ((𝜑𝑥𝐶) → ∃𝑦𝐷 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ)
142 oveq1 6534 . . . . . . . 8 ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1 → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))) = (1 · (exp‘(i · 𝑦))))
1433a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → i ∈ ℂ)
144132adantr 479 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
145144recnd 9924 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
1461ad2antrr 757 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝐷 ⊆ ℝ)
147 simpr 475 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝑦𝐷)
148146, 147sseldd 3568 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝑦 ∈ ℝ)
149148recnd 9924 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝑦 ∈ ℂ)
150143, 145, 149subdid 10336 . . . . . . . . . . . . 13 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) = ((i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) − (i · 𝑦)))
151150oveq1d 6542 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦)) = (((i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) − (i · 𝑦)) + (i · 𝑦)))
152 mulcl 9876 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) ∈ ℂ)
1533, 145, 152sylancr 693 . . . . . . . . . . . . 13 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) ∈ ℂ)
1543, 149, 72sylancr 693 . . . . . . . . . . . . 13 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · 𝑦) ∈ ℂ)
155153, 154npcand 10247 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (((i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) − (i · 𝑦)) + (i · 𝑦)) = (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))))
156151, 155eqtrd 2643 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦)) = (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))))
157156fveq2d 6092 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦))) = (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))))
158145, 149subcld 10243 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ)
159 mulcl 9876 . . . . . . . . . . . 12 ((i ∈ ℂ ∧ ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ) → (i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ)
1603, 158, 159sylancr 693 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ)
161 efadd 14609 . . . . . . . . . . 11 (((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → (exp‘((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦))) = ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))))
162160, 154, 161syl2anc 690 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦))) = ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))))
163130recnd 9924 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ)
164 2cn 10938 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
165 mul12 10053 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 2 ∈ ℂ ∧ (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) = (2 · (i · (𝑆‘(ℑ‘(√‘𝑥))))))
1663, 164, 165mp3an12 1405 . . . . . . . . . . . . . . 15 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) = (2 · (i · (𝑆‘(ℑ‘(√‘𝑥))))))
167163, 166syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) = (2 · (i · (𝑆‘(ℑ‘(√‘𝑥))))))
168167fveq2d 6092 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = (exp‘(2 · (i · (𝑆‘(ℑ‘(√‘𝑥)))))))
169 mulcl 9876 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ) → (i · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
1703, 163, 169sylancr 693 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (i · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
171 2z 11242 . . . . . . . . . . . . . 14 2 ∈ ℤ
172 efexp 14616 . . . . . . . . . . . . . 14 (((i · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ ∧ 2 ∈ ℤ) → (exp‘(2 · (i · (𝑆‘(ℑ‘(√‘𝑥)))))) = ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2))
173170, 171, 172sylancl 692 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → (exp‘(2 · (i · (𝑆‘(ℑ‘(√‘𝑥)))))) = ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2))
174168, 173eqtrd 2643 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2))
175130recoscld 14659 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → (cos‘(𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
176 simpr 475 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥𝐶) → 𝑥𝐶)
177176, 16syl6eleq 2697 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝑥 ∈ (abs “ {1}))
178 fniniseg 6231 . . . . . . . . . . . . . . . . . . . . 21 (abs Fn ℂ → (𝑥 ∈ (abs “ {1}) ↔ (𝑥 ∈ ℂ ∧ (abs‘𝑥) = 1)))
17912, 178ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (abs “ {1}) ↔ (𝑥 ∈ ℂ ∧ (abs‘𝑥) = 1))
180177, 179sylib 206 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (𝑥 ∈ ℂ ∧ (abs‘𝑥) = 1))
181180simpld 473 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → 𝑥 ∈ ℂ)
182181sqrtcld 13970 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → (√‘𝑥) ∈ ℂ)
183182recld 13728 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → (ℜ‘(√‘𝑥)) ∈ ℝ)
184 cosq14ge0 23984 . . . . . . . . . . . . . . . . 17 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π / 2)) → 0 ≤ (cos‘(𝑆‘(ℑ‘(√‘𝑥)))))
185129, 184syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → 0 ≤ (cos‘(𝑆‘(ℑ‘(√‘𝑥)))))
186181sqrtrege0d 13971 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → 0 ≤ (ℜ‘(√‘𝑥)))
187 sincossq 14691 . . . . . . . . . . . . . . . . . . . 20 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ → (((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = 1)
188163, 187syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = 1)
189181sqsqrtd 13972 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥𝐶) → ((√‘𝑥)↑2) = 𝑥)
190189fveq2d 6092 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (abs‘((√‘𝑥)↑2)) = (abs‘𝑥))
191 2nn0 11156 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℕ0
192 absexp 13838 . . . . . . . . . . . . . . . . . . . . 21 (((√‘𝑥) ∈ ℂ ∧ 2 ∈ ℕ0) → (abs‘((√‘𝑥)↑2)) = ((abs‘(√‘𝑥))↑2))
193182, 191, 192sylancl 692 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (abs‘((√‘𝑥)↑2)) = ((abs‘(√‘𝑥))↑2))
194180simprd 477 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (abs‘𝑥) = 1)
195190, 193, 1943eqtr3d 2651 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → ((abs‘(√‘𝑥))↑2) = 1)
196182absvalsq2d 13976 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → ((abs‘(√‘𝑥))↑2) = (((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)))
197188, 195, 1963eqtr2d 2649 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → (((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = (((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)))
198121fveq1i 6089 . . . . . . . . . . . . . . . . . . . . 21 (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = ((sin ↾ (-(π / 2)[,](π / 2)))‘(𝑆‘(ℑ‘(√‘𝑥))))
199 fvres 6102 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π / 2)) → ((sin ↾ (-(π / 2)[,](π / 2)))‘(𝑆‘(ℑ‘(√‘𝑥)))) = (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))
200129, 199syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥𝐶) → ((sin ↾ (-(π / 2)[,](π / 2)))‘(𝑆‘(ℑ‘(√‘𝑥)))) = (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))
201198, 200syl5eq 2655 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))
202 f1ocnvfv2 6411 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆:(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) ∧ (ℑ‘(√‘𝑥)) ∈ (-1[,]1)) → (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℑ‘(√‘𝑥)))
203124, 119, 202sylancr 693 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℑ‘(√‘𝑥)))
204201, 203eqtr3d 2645 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (sin‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℑ‘(√‘𝑥)))
205204oveq1d 6542 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) = ((ℑ‘(√‘𝑥))↑2))
206197, 205oveq12d 6545 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) − ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = ((((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)) − ((ℑ‘(√‘𝑥))↑2)))
207163sincld 14645 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (sin‘(𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
208207sqcld 12823 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) ∈ ℂ)
209163coscld 14646 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (cos‘(𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
210209sqcld 12823 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) ∈ ℂ)
211208, 210pncan2d 10245 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) − ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2))
212183recnd 9924 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (ℜ‘(√‘𝑥)) ∈ ℂ)
213212sqcld 12823 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((ℜ‘(√‘𝑥))↑2) ∈ ℂ)
214205, 208eqeltrrd 2688 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((ℑ‘(√‘𝑥))↑2) ∈ ℂ)
215213, 214pncand 10244 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)) − ((ℑ‘(√‘𝑥))↑2)) = ((ℜ‘(√‘𝑥))↑2))
216206, 211, 2153eqtr3d 2651 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) = ((ℜ‘(√‘𝑥))↑2))
217175, 183, 185, 186, 216sq11d 12862 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (cos‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℜ‘(√‘𝑥)))
218204oveq2d 6543 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥))))) = (i · (ℑ‘(√‘𝑥))))
219217, 218oveq12d 6545 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → ((cos‘(𝑆‘(ℑ‘(√‘𝑥)))) + (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))) = ((ℜ‘(√‘𝑥)) + (i · (ℑ‘(√‘𝑥)))))
220 efival 14667 . . . . . . . . . . . . . . 15 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ → (exp‘(i · (𝑆‘(ℑ‘(√‘𝑥))))) = ((cos‘(𝑆‘(ℑ‘(√‘𝑥)))) + (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))))
221163, 220syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (exp‘(i · (𝑆‘(ℑ‘(√‘𝑥))))) = ((cos‘(𝑆‘(ℑ‘(√‘𝑥)))) + (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))))
222182replimd 13731 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (√‘𝑥) = ((ℜ‘(√‘𝑥)) + (i · (ℑ‘(√‘𝑥)))))
223219, 221, 2223eqtr4d 2653 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → (exp‘(i · (𝑆‘(ℑ‘(√‘𝑥))))) = (√‘𝑥))
224223oveq1d 6542 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2) = ((√‘𝑥)↑2))
225174, 224, 1893eqtrd 2647 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = 𝑥)
226225adantr 479 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = 𝑥)
227157, 162, 2263eqtr3d 2651 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))) = 𝑥)
228154, 76syl 17 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘(i · 𝑦)) ∈ ℂ)
229228mulid2d 9914 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (1 · (exp‘(i · 𝑦))) = (exp‘(i · 𝑦)))
230227, 229eqeq12d 2624 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))) = (1 · (exp‘(i · 𝑦))) ↔ 𝑥 = (exp‘(i · 𝑦))))
231142, 230syl5ib 232 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1 → 𝑥 = (exp‘(i · 𝑦))))
232 efeq1 23996 . . . . . . . . 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 10576 . . . . . . . . . . 11 ((((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ ∧ ((2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) ∧ (i ∈ ℂ ∧ i ≠ 0)) → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) = (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)))
23561, 63, 234mp3an23 1407 . . . . . . . . . 10 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) = (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)))
236158, 235syl 17 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) = (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)))
237236eleq1d 2671 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) ∈ ℤ ↔ (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ))
238233, 237bitr2d 267 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ ↔ (exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1))
23989adantl 480 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (𝐹𝑦) = (exp‘(i · 𝑦)))
240239eqeq2d 2619 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (𝑥 = (𝐹𝑦) ↔ 𝑥 = (exp‘(i · 𝑦))))
241231, 238, 2403imtr4d 281 . . . . . 6 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ → 𝑥 = (𝐹𝑦)))
242241reximdva 2999 . . . . 5 ((𝜑𝑥𝐶) → (∃𝑦𝐷 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ → ∃𝑦𝐷 𝑥 = (𝐹𝑦)))
243141, 242mpd 15 . . . 4 ((𝜑𝑥𝐶) → ∃𝑦𝐷 𝑥 = (𝐹𝑦))
244243ralrimiva 2948 . . 3 (𝜑 → ∀𝑥𝐶𝑦𝐷 𝑥 = (𝐹𝑦))
245 dffo3 6267 . . 3 (𝐹:𝐷onto𝐶 ↔ (𝐹:𝐷𝐶 ∧ ∀𝑥𝐶𝑦𝐷 𝑥 = (𝐹𝑦)))
24620, 244, 245sylanbrc 694 . 2 (𝜑𝐹:𝐷onto𝐶)
247 df-f1o 5797 . 2 (𝐹:𝐷1-1-onto𝐶 ↔ (𝐹:𝐷1-1𝐶𝐹:𝐷onto𝐶))
248114, 246, 247sylanbrc 694 1 (𝜑𝐹:𝐷1-1-onto𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wne 2779  wral 2895  wrex 2896  wss 3539  {csn 4124   class class class wbr 4577  cmpt 4637  ccnv 5027  cres 5030  cima 5031   Fn wfn 5785  wf 5786  1-1wf1 5787  ontowfo 5788  1-1-ontowf1o 5789  cfv 5790  (class class class)co 6527  cc 9790  cr 9791  0cc0 9792  1c1 9793  ici 9794   + caddc 9795   · cmul 9797   < clt 9930  cle 9931  cmin 10117  -cneg 10118   / cdiv 10533  2c2 10917  0cn0 11139  cz 11210  [,]cicc 12005  cexp 12677  cre 13631  cim 13632  csqrt 13767  abscabs 13768  expce 14577  sincsin 14579  cosccos 14580  πcpi 14582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-inf2 8398  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870  ax-addf 9871  ax-mulf 9872
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6772  df-om 6935  df-1st 7036  df-2nd 7037  df-supp 7160  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-ixp 7772  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-fsupp 8136  df-fi 8177  df-sup 8208  df-inf 8209  df-oi 8275  df-card 8625  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-2 10926  df-3 10927  df-4 10928  df-5 10929  df-6 10930  df-7 10931  df-8 10932  df-9 10933  df-n0 11140  df-z 11211  df-dec 11326  df-uz 11520  df-q 11621  df-rp 11665  df-xneg 11778  df-xadd 11779  df-xmul 11780  df-ioo 12006  df-ioc 12007  df-ico 12008  df-icc 12009  df-fz 12153  df-fzo 12290  df-fl 12410  df-mod 12486  df-seq 12619  df-exp 12678  df-fac 12878  df-bc 12907  df-hash 12935  df-shft 13601  df-cj 13633  df-re 13634  df-im 13635  df-sqrt 13769  df-abs 13770  df-limsup 13996  df-clim 14013  df-rlim 14014  df-sum 14211  df-ef 14583  df-sin 14585  df-cos 14586  df-pi 14588  df-struct 15643  df-ndx 15644  df-slot 15645  df-base 15646  df-sets 15647  df-ress 15648  df-plusg 15727  df-mulr 15728  df-starv 15729  df-sca 15730  df-vsca 15731  df-ip 15732  df-tset 15733  df-ple 15734  df-ds 15737  df-unif 15738  df-hom 15739  df-cco 15740  df-rest 15852  df-topn 15853  df-0g 15871  df-gsum 15872  df-topgen 15873  df-pt 15874  df-prds 15877  df-xrs 15931  df-qtop 15936  df-imas 15937  df-xps 15939  df-mre 16015  df-mrc 16016  df-acs 16018  df-mgm 17011  df-sgrp 17053  df-mnd 17064  df-submnd 17105  df-mulg 17310  df-cntz 17519  df-cmn 17964  df-psmet 19505  df-xmet 19506  df-met 19507  df-bl 19508  df-mopn 19509  df-fbas 19510  df-fg 19511  df-cnfld 19514  df-top 20463  df-bases 20464  df-topon 20465  df-topsp 20466  df-cld 20575  df-ntr 20576  df-cls 20577  df-nei 20654  df-lp 20692  df-perf 20693  df-cn 20783  df-cnp 20784  df-haus 20871  df-tx 21117  df-hmeo 21310  df-fil 21402  df-fm 21494  df-flim 21495  df-flf 21496  df-xms 21876  df-ms 21877  df-tms 21878  df-cncf 22420  df-limc 23353  df-dv 23354
This theorem is referenced by:  efif1o  24013  eff1olem  24015
  Copyright terms: Public domain W3C validator