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

Theorem efif1olem4 26499
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 3982 . . . . 5 ((𝜑𝑤𝐷) → 𝑤 ∈ ℝ)
3 ax-icn 11205 . . . . . . . . 9 i ∈ ℂ
4 recn 11236 . . . . . . . . 9 (𝑤 ∈ ℝ → 𝑤 ∈ ℂ)
5 mulcl 11230 . . . . . . . . 9 ((i ∈ ℂ ∧ 𝑤 ∈ ℂ) → (i · 𝑤) ∈ ℂ)
63, 4, 5sylancr 585 . . . . . . . 8 (𝑤 ∈ ℝ → (i · 𝑤) ∈ ℂ)
7 efcl 16066 . . . . . . . 8 ((i · 𝑤) ∈ ℂ → (exp‘(i · 𝑤)) ∈ ℂ)
86, 7syl 17 . . . . . . 7 (𝑤 ∈ ℝ → (exp‘(i · 𝑤)) ∈ ℂ)
9 absefi 16180 . . . . . . 7 (𝑤 ∈ ℝ → (abs‘(exp‘(i · 𝑤))) = 1)
10 absf 15324 . . . . . . . . 9 abs:ℂ⟶ℝ
11 ffn 6727 . . . . . . . . 9 (abs:ℂ⟶ℝ → abs Fn ℂ)
1210, 11ax-mp 5 . . . . . . . 8 abs Fn ℂ
13 fniniseg 7074 . . . . . . . 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 581 . . . . . 6 (𝑤 ∈ ℝ → (exp‘(i · 𝑤)) ∈ (abs “ {1}))
16 efif1o.2 . . . . . 6 𝐶 = (abs “ {1})
1715, 16eleqtrrdi 2840 . . . . 5 (𝑤 ∈ ℝ → (exp‘(i · 𝑤)) ∈ 𝐶)
182, 17syl 17 . . . 4 ((𝜑𝑤𝐷) → (exp‘(i · 𝑤)) ∈ 𝐶)
19 efif1o.1 . . . 4 𝐹 = (𝑤𝐷 ↦ (exp‘(i · 𝑤)))
2018, 19fmptd 7129 . . 3 (𝜑𝐹:𝐷𝐶)
211ad2antrr 724 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝐷 ⊆ ℝ)
22 simplrl 775 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥𝐷)
2321, 22sseldd 3983 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 ∈ ℝ)
2423recnd 11280 . . . . . 6 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 ∈ ℂ)
25 simplrr 776 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑦𝐷)
2621, 25sseldd 3983 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑦 ∈ ℝ)
2726recnd 11280 . . . . . 6 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑦 ∈ ℂ)
2824, 27subcld 11609 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝑥𝑦) ∈ ℂ)
29 2re 12324 . . . . . . . . . . . 12 2 ∈ ℝ
30 pire 26413 . . . . . . . . . . . 12 π ∈ ℝ
3129, 30remulcli 11268 . . . . . . . . . . 11 (2 · π) ∈ ℝ
3231recni 11266 . . . . . . . . . 10 (2 · π) ∈ ℂ
33 2pos 12353 . . . . . . . . . . . 12 0 < 2
34 pipos 26415 . . . . . . . . . . . 12 0 < π
3529, 30, 33, 34mulgt0ii 11385 . . . . . . . . . . 11 0 < (2 · π)
3631, 35gt0ne0ii 11788 . . . . . . . . . 10 (2 · π) ≠ 0
37 divcl 11916 . . . . . . . . . 10 (((𝑥𝑦) ∈ ℂ ∧ (2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) → ((𝑥𝑦) / (2 · π)) ∈ ℂ)
3832, 36, 37mp3an23 1449 . . . . . . . . 9 ((𝑥𝑦) ∈ ℂ → ((𝑥𝑦) / (2 · π)) ∈ ℂ)
3928, 38syl 17 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((𝑥𝑦) / (2 · π)) ∈ ℂ)
40 absdiv 15282 . . . . . . . . . . . . 13 (((𝑥𝑦) ∈ ℂ ∧ (2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (abs‘(2 · π))))
4132, 36, 40mp3an23 1449 . . . . . . . . . . . 12 ((𝑥𝑦) ∈ ℂ → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (abs‘(2 · π))))
4228, 41syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (abs‘(2 · π))))
43 0re 11254 . . . . . . . . . . . . . 14 0 ∈ ℝ
4443, 31, 35ltleii 11375 . . . . . . . . . . . . 13 0 ≤ (2 · π)
45 absid 15283 . . . . . . . . . . . . 13 (((2 · π) ∈ ℝ ∧ 0 ≤ (2 · π)) → (abs‘(2 · π)) = (2 · π))
4631, 44, 45mp2an 690 . . . . . . . . . . . 12 (abs‘(2 · π)) = (2 · π)
4746oveq2i 7437 . . . . . . . . . . 11 ((abs‘(𝑥𝑦)) / (abs‘(2 · π))) = ((abs‘(𝑥𝑦)) / (2 · π))
4842, 47eqtrdi 2784 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (2 · π)))
49 efif1olem4.4 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐷𝑦𝐷)) → (abs‘(𝑥𝑦)) < (2 · π))
5049adantr 479 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘(𝑥𝑦)) < (2 · π))
5132mulridi 11256 . . . . . . . . . . . 12 ((2 · π) · 1) = (2 · π)
5250, 51breqtrrdi 5194 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘(𝑥𝑦)) < ((2 · π) · 1))
5328abscld 15423 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘(𝑥𝑦)) ∈ ℝ)
54 1re 11252 . . . . . . . . . . . . 13 1 ∈ ℝ
5531, 35pm3.2i 469 . . . . . . . . . . . . 13 ((2 · π) ∈ ℝ ∧ 0 < (2 · π))
56 ltdivmul 12127 . . . . . . . . . . . . 13 (((abs‘(𝑥𝑦)) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((2 · π) ∈ ℝ ∧ 0 < (2 · π))) → (((abs‘(𝑥𝑦)) / (2 · π)) < 1 ↔ (abs‘(𝑥𝑦)) < ((2 · π) · 1)))
5754, 55, 56mp3an23 1449 . . . . . . . . . . . 12 ((abs‘(𝑥𝑦)) ∈ ℝ → (((abs‘(𝑥𝑦)) / (2 · π)) < 1 ↔ (abs‘(𝑥𝑦)) < ((2 · π) · 1)))
5853, 57syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (((abs‘(𝑥𝑦)) / (2 · π)) < 1 ↔ (abs‘(𝑥𝑦)) < ((2 · π) · 1)))
5952, 58mpbird 256 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((abs‘(𝑥𝑦)) / (2 · π)) < 1)
6048, 59eqbrtrd 5174 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) < 1)
6132, 36pm3.2i 469 . . . . . . . . . . . . . 14 ((2 · π) ∈ ℂ ∧ (2 · π) ≠ 0)
62 ine0 11687 . . . . . . . . . . . . . . 15 i ≠ 0
633, 62pm3.2i 469 . . . . . . . . . . . . . 14 (i ∈ ℂ ∧ i ≠ 0)
64 divcan5 11954 . . . . . . . . . . . . . 14 (((𝑥𝑦) ∈ ℂ ∧ ((2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) ∧ (i ∈ ℂ ∧ i ≠ 0)) → ((i · (𝑥𝑦)) / (i · (2 · π))) = ((𝑥𝑦) / (2 · π)))
6561, 63, 64mp3an23 1449 . . . . . . . . . . . . 13 ((𝑥𝑦) ∈ ℂ → ((i · (𝑥𝑦)) / (i · (2 · π))) = ((𝑥𝑦) / (2 · π)))
6628, 65syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((i · (𝑥𝑦)) / (i · (2 · π))) = ((𝑥𝑦) / (2 · π)))
673a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → i ∈ ℂ)
6867, 24, 27subdid 11708 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · (𝑥𝑦)) = ((i · 𝑥) − (i · 𝑦)))
6968fveq2d 6906 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · (𝑥𝑦))) = (exp‘((i · 𝑥) − (i · 𝑦))))
70 mulcl 11230 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
713, 24, 70sylancr 585 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · 𝑥) ∈ ℂ)
72 mulcl 11230 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝑦 ∈ ℂ) → (i · 𝑦) ∈ ℂ)
733, 27, 72sylancr 585 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · 𝑦) ∈ ℂ)
74 efsub 16084 . . . . . . . . . . . . . . 15 (((i · 𝑥) ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → (exp‘((i · 𝑥) − (i · 𝑦))) = ((exp‘(i · 𝑥)) / (exp‘(i · 𝑦))))
7571, 73, 74syl2anc 582 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘((i · 𝑥) − (i · 𝑦))) = ((exp‘(i · 𝑥)) / (exp‘(i · 𝑦))))
76 efcl 16066 . . . . . . . . . . . . . . . 16 ((i · 𝑦) ∈ ℂ → (exp‘(i · 𝑦)) ∈ ℂ)
7773, 76syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · 𝑦)) ∈ ℂ)
78 efne0 16081 . . . . . . . . . . . . . . . 16 ((i · 𝑦) ∈ ℂ → (exp‘(i · 𝑦)) ≠ 0)
7973, 78syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · 𝑦)) ≠ 0)
80 simpr 483 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝐹𝑥) = (𝐹𝑦))
81 oveq2 7434 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑥 → (i · 𝑤) = (i · 𝑥))
8281fveq2d 6906 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑥 → (exp‘(i · 𝑤)) = (exp‘(i · 𝑥)))
83 fvex 6915 . . . . . . . . . . . . . . . . . 18 (exp‘(i · 𝑥)) ∈ V
8482, 19, 83fvmpt 7010 . . . . . . . . . . . . . . . . 17 (𝑥𝐷 → (𝐹𝑥) = (exp‘(i · 𝑥)))
8522, 84syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝐹𝑥) = (exp‘(i · 𝑥)))
86 oveq2 7434 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑦 → (i · 𝑤) = (i · 𝑦))
8786fveq2d 6906 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑦 → (exp‘(i · 𝑤)) = (exp‘(i · 𝑦)))
88 fvex 6915 . . . . . . . . . . . . . . . . . 18 (exp‘(i · 𝑦)) ∈ V
8987, 19, 88fvmpt 7010 . . . . . . . . . . . . . . . . 17 (𝑦𝐷 → (𝐹𝑦) = (exp‘(i · 𝑦)))
9025, 89syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝐹𝑦) = (exp‘(i · 𝑦)))
9180, 85, 903eqtr3d 2776 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · 𝑥)) = (exp‘(i · 𝑦)))
9277, 79, 91diveq1bd 12076 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((exp‘(i · 𝑥)) / (exp‘(i · 𝑦))) = 1)
9369, 75, 923eqtrd 2772 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · (𝑥𝑦))) = 1)
94 mulcl 11230 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ (𝑥𝑦) ∈ ℂ) → (i · (𝑥𝑦)) ∈ ℂ)
953, 28, 94sylancr 585 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · (𝑥𝑦)) ∈ ℂ)
96 efeq1 26482 . . . . . . . . . . . . . 14 ((i · (𝑥𝑦)) ∈ ℂ → ((exp‘(i · (𝑥𝑦))) = 1 ↔ ((i · (𝑥𝑦)) / (i · (2 · π))) ∈ ℤ))
9795, 96syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((exp‘(i · (𝑥𝑦))) = 1 ↔ ((i · (𝑥𝑦)) / (i · (2 · π))) ∈ ℤ))
9893, 97mpbid 231 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((i · (𝑥𝑦)) / (i · (2 · π))) ∈ ℤ)
9966, 98eqeltrrd 2830 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((𝑥𝑦) / (2 · π)) ∈ ℤ)
100 nn0abscl 15299 . . . . . . . . . . 11 (((𝑥𝑦) / (2 · π)) ∈ ℤ → (abs‘((𝑥𝑦) / (2 · π))) ∈ ℕ0)
10199, 100syl 17 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) ∈ ℕ0)
102 nn0lt10b 12662 . . . . . . . . . 10 ((abs‘((𝑥𝑦) / (2 · π))) ∈ ℕ0 → ((abs‘((𝑥𝑦) / (2 · π))) < 1 ↔ (abs‘((𝑥𝑦) / (2 · π))) = 0))
103101, 102syl 17 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((abs‘((𝑥𝑦) / (2 · π))) < 1 ↔ (abs‘((𝑥𝑦) / (2 · π))) = 0))
10460, 103mpbid 231 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) = 0)
10539, 104abs00d 15433 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((𝑥𝑦) / (2 · π)) = 0)
106 diveq0 11920 . . . . . . . . 9 (((𝑥𝑦) ∈ ℂ ∧ (2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) → (((𝑥𝑦) / (2 · π)) = 0 ↔ (𝑥𝑦) = 0))
10732, 36, 106mp3an23 1449 . . . . . . . 8 ((𝑥𝑦) ∈ ℂ → (((𝑥𝑦) / (2 · π)) = 0 ↔ (𝑥𝑦) = 0))
10828, 107syl 17 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (((𝑥𝑦) / (2 · π)) = 0 ↔ (𝑥𝑦) = 0))
109105, 108mpbid 231 . . . . . 6 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝑥𝑦) = 0)
11024, 27, 109subeq0d 11617 . . . . 5 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 = 𝑦)
111110ex 411 . . . 4 ((𝜑 ∧ (𝑥𝐷𝑦𝐷)) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
112111ralrimivva 3198 . . 3 (𝜑 → ∀𝑥𝐷𝑦𝐷 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
113 dff13 7271 . . 3 (𝐹:𝐷1-1𝐶 ↔ (𝐹:𝐷𝐶 ∧ ∀𝑥𝐷𝑦𝐷 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
11420, 112, 113sylanbrc 581 . 2 (𝜑𝐹:𝐷1-1𝐶)
115 oveq1 7433 . . . . . . . . 9 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → (𝑧𝑦) = ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))
116115oveq1d 7441 . . . . . . . 8 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → ((𝑧𝑦) / (2 · π)) = (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)))
117116eleq1d 2814 . . . . . . 7 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → (((𝑧𝑦) / (2 · π)) ∈ ℤ ↔ (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ))
118117rexbidv 3176 . . . . . 6 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → (∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ ↔ ∃𝑦𝐷 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ))
119 efif1olem4.5 . . . . . . . 8 ((𝜑𝑧 ∈ ℝ) → ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ)
120119ralrimiva 3143 . . . . . . 7 (𝜑 → ∀𝑧 ∈ ℝ ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ)
121120adantr 479 . . . . . 6 ((𝜑𝑥𝐶) → ∀𝑧 ∈ ℝ ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ)
122 neghalfpire 26420 . . . . . . . . 9 -(π / 2) ∈ ℝ
123 halfpire 26419 . . . . . . . . 9 (π / 2) ∈ ℝ
124 iccssre 13446 . . . . . . . . 9 ((-(π / 2) ∈ ℝ ∧ (π / 2) ∈ ℝ) → (-(π / 2)[,](π / 2)) ⊆ ℝ)
125122, 123, 124mp2an 690 . . . . . . . 8 (-(π / 2)[,](π / 2)) ⊆ ℝ
12619, 16efif1olem3 26498 . . . . . . . . 9 ((𝜑𝑥𝐶) → (ℑ‘(√‘𝑥)) ∈ (-1[,]1))
127 resinf1o 26490 . . . . . . . . . . . 12 (sin ↾ (-(π / 2)[,](π / 2))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1)
128 efif1olem4.6 . . . . . . . . . . . . 13 𝑆 = (sin ↾ (-(π / 2)[,](π / 2)))
129 f1oeq1 6832 . . . . . . . . . . . . 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 230 . . . . . . . . . . 11 𝑆:(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1)
132 f1ocnv 6856 . . . . . . . . . . 11 (𝑆:(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) → 𝑆:(-1[,]1)–1-1-onto→(-(π / 2)[,](π / 2)))
133 f1of 6844 . . . . . . . . . . 11 (𝑆:(-1[,]1)–1-1-onto→(-(π / 2)[,](π / 2)) → 𝑆:(-1[,]1)⟶(-(π / 2)[,](π / 2)))
134131, 132, 133mp2b 10 . . . . . . . . . 10 𝑆:(-1[,]1)⟶(-(π / 2)[,](π / 2))
135134ffvelcdmi 7098 . . . . . . . . 9 ((ℑ‘(√‘𝑥)) ∈ (-1[,]1) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π / 2)))
136126, 135syl 17 . . . . . . . 8 ((𝜑𝑥𝐶) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π / 2)))
137125, 136sselid 3980 . . . . . . 7 ((𝜑𝑥𝐶) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℝ)
138 remulcl 11231 . . . . . . 7 ((2 ∈ ℝ ∧ (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℝ) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
13929, 137, 138sylancr 585 . . . . . 6 ((𝜑𝑥𝐶) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
140118, 121, 139rspcdva 3612 . . . . 5 ((𝜑𝑥𝐶) → ∃𝑦𝐷 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ)
141 oveq1 7433 . . . . . . . 8 ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1 → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))) = (1 · (exp‘(i · 𝑦))))
1423a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → i ∈ ℂ)
143139adantr 479 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
144143recnd 11280 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
1451ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝐷 ⊆ ℝ)
146 simpr 483 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝑦𝐷)
147145, 146sseldd 3983 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝑦 ∈ ℝ)
148147recnd 11280 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝑦 ∈ ℂ)
149142, 144, 148subdid 11708 . . . . . . . . . . . . 13 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) = ((i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) − (i · 𝑦)))
150149oveq1d 7441 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦)) = (((i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) − (i · 𝑦)) + (i · 𝑦)))
151 mulcl 11230 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) ∈ ℂ)
1523, 144, 151sylancr 585 . . . . . . . . . . . . 13 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) ∈ ℂ)
1533, 148, 72sylancr 585 . . . . . . . . . . . . 13 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · 𝑦) ∈ ℂ)
154152, 153npcand 11613 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (((i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) − (i · 𝑦)) + (i · 𝑦)) = (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))))
155150, 154eqtrd 2768 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦)) = (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))))
156155fveq2d 6906 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦))) = (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))))
157144, 148subcld 11609 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ)
158 mulcl 11230 . . . . . . . . . . . 12 ((i ∈ ℂ ∧ ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ) → (i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ)
1593, 157, 158sylancr 585 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ)
160 efadd 16078 . . . . . . . . . . 11 (((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → (exp‘((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦))) = ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))))
161159, 153, 160syl2anc 582 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦))) = ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))))
162 2cn 12325 . . . . . . . . . . . . . . 15 2 ∈ ℂ
163137recnd 11280 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ)
164 mul12 11417 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ 2 ∈ ℂ ∧ (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) = (2 · (i · (𝑆‘(ℑ‘(√‘𝑥))))))
1653, 162, 163, 164mp3an12i 1461 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) = (2 · (i · (𝑆‘(ℑ‘(√‘𝑥))))))
166165fveq2d 6906 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = (exp‘(2 · (i · (𝑆‘(ℑ‘(√‘𝑥)))))))
167 mulcl 11230 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ) → (i · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
1683, 163, 167sylancr 585 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (i · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
169 2z 12632 . . . . . . . . . . . . . 14 2 ∈ ℤ
170 efexp 16085 . . . . . . . . . . . . . 14 (((i · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ ∧ 2 ∈ ℤ) → (exp‘(2 · (i · (𝑆‘(ℑ‘(√‘𝑥)))))) = ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2))
171168, 169, 170sylancl 584 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → (exp‘(2 · (i · (𝑆‘(ℑ‘(√‘𝑥)))))) = ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2))
172166, 171eqtrd 2768 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2))
173137recoscld 16128 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → (cos‘(𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
174 simpr 483 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥𝐶) → 𝑥𝐶)
175174, 16eleqtrdi 2839 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝑥 ∈ (abs “ {1}))
176 fniniseg 7074 . . . . . . . . . . . . . . . . . . . . 21 (abs Fn ℂ → (𝑥 ∈ (abs “ {1}) ↔ (𝑥 ∈ ℂ ∧ (abs‘𝑥) = 1)))
17712, 176ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (abs “ {1}) ↔ (𝑥 ∈ ℂ ∧ (abs‘𝑥) = 1))
178175, 177sylib 217 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (𝑥 ∈ ℂ ∧ (abs‘𝑥) = 1))
179178simpld 493 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → 𝑥 ∈ ℂ)
180179sqrtcld 15424 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → (√‘𝑥) ∈ ℂ)
181180recld 15181 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → (ℜ‘(√‘𝑥)) ∈ ℝ)
182 cosq14ge0 26466 . . . . . . . . . . . . . . . . 17 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π / 2)) → 0 ≤ (cos‘(𝑆‘(ℑ‘(√‘𝑥)))))
183136, 182syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → 0 ≤ (cos‘(𝑆‘(ℑ‘(√‘𝑥)))))
184179sqrtrege0d 15425 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → 0 ≤ (ℜ‘(√‘𝑥)))
185 sincossq 16160 . . . . . . . . . . . . . . . . . . . 20 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ → (((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = 1)
186163, 185syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = 1)
187179sqsqrtd 15426 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥𝐶) → ((√‘𝑥)↑2) = 𝑥)
188187fveq2d 6906 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (abs‘((√‘𝑥)↑2)) = (abs‘𝑥))
189 2nn0 12527 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℕ0
190 absexp 15291 . . . . . . . . . . . . . . . . . . . . 21 (((√‘𝑥) ∈ ℂ ∧ 2 ∈ ℕ0) → (abs‘((√‘𝑥)↑2)) = ((abs‘(√‘𝑥))↑2))
191180, 189, 190sylancl 584 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (abs‘((√‘𝑥)↑2)) = ((abs‘(√‘𝑥))↑2))
192178simprd 494 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (abs‘𝑥) = 1)
193188, 191, 1923eqtr3d 2776 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → ((abs‘(√‘𝑥))↑2) = 1)
194180absvalsq2d 15430 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → ((abs‘(√‘𝑥))↑2) = (((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)))
195186, 193, 1943eqtr2d 2774 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → (((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = (((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)))
196128fveq1i 6903 . . . . . . . . . . . . . . . . . . . . 21 (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = ((sin ↾ (-(π / 2)[,](π / 2)))‘(𝑆‘(ℑ‘(√‘𝑥))))
197136fvresd 6922 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥𝐶) → ((sin ↾ (-(π / 2)[,](π / 2)))‘(𝑆‘(ℑ‘(√‘𝑥)))) = (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))
198196, 197eqtrid 2780 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))
199 f1ocnvfv2 7292 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆:(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) ∧ (ℑ‘(√‘𝑥)) ∈ (-1[,]1)) → (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℑ‘(√‘𝑥)))
200131, 126, 199sylancr 585 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℑ‘(√‘𝑥)))
201198, 200eqtr3d 2770 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (sin‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℑ‘(√‘𝑥)))
202201oveq1d 7441 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) = ((ℑ‘(√‘𝑥))↑2))
203195, 202oveq12d 7444 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) − ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = ((((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)) − ((ℑ‘(√‘𝑥))↑2)))
204163sincld 16114 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (sin‘(𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
205204sqcld 14148 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) ∈ ℂ)
206163coscld 16115 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (cos‘(𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
207206sqcld 14148 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) ∈ ℂ)
208205, 207pncan2d 11611 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) − ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2))
209181recnd 11280 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (ℜ‘(√‘𝑥)) ∈ ℂ)
210209sqcld 14148 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((ℜ‘(√‘𝑥))↑2) ∈ ℂ)
211202, 205eqeltrrd 2830 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((ℑ‘(√‘𝑥))↑2) ∈ ℂ)
212210, 211pncand 11610 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)) − ((ℑ‘(√‘𝑥))↑2)) = ((ℜ‘(√‘𝑥))↑2))
213203, 208, 2123eqtr3d 2776 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) = ((ℜ‘(√‘𝑥))↑2))
214173, 181, 183, 184, 213sq11d 14260 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (cos‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℜ‘(√‘𝑥)))
215201oveq2d 7442 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥))))) = (i · (ℑ‘(√‘𝑥))))
216214, 215oveq12d 7444 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → ((cos‘(𝑆‘(ℑ‘(√‘𝑥)))) + (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))) = ((ℜ‘(√‘𝑥)) + (i · (ℑ‘(√‘𝑥)))))
217 efival 16136 . . . . . . . . . . . . . . 15 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ → (exp‘(i · (𝑆‘(ℑ‘(√‘𝑥))))) = ((cos‘(𝑆‘(ℑ‘(√‘𝑥)))) + (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))))
218163, 217syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (exp‘(i · (𝑆‘(ℑ‘(√‘𝑥))))) = ((cos‘(𝑆‘(ℑ‘(√‘𝑥)))) + (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))))
219180replimd 15184 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (√‘𝑥) = ((ℜ‘(√‘𝑥)) + (i · (ℑ‘(√‘𝑥)))))
220216, 218, 2193eqtr4d 2778 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → (exp‘(i · (𝑆‘(ℑ‘(√‘𝑥))))) = (√‘𝑥))
221220oveq1d 7441 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2) = ((√‘𝑥)↑2))
222172, 221, 1873eqtrd 2772 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = 𝑥)
223222adantr 479 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = 𝑥)
224156, 161, 2233eqtr3d 2776 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))) = 𝑥)
225153, 76syl 17 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘(i · 𝑦)) ∈ ℂ)
226225mullidd 11270 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (1 · (exp‘(i · 𝑦))) = (exp‘(i · 𝑦)))
227224, 226eqeq12d 2744 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))) = (1 · (exp‘(i · 𝑦))) ↔ 𝑥 = (exp‘(i · 𝑦))))
228141, 227imbitrid 243 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1 → 𝑥 = (exp‘(i · 𝑦))))
229 efeq1 26482 . . . . . . . . 9 ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1 ↔ ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) ∈ ℤ))
230159, 229syl 17 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1 ↔ ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) ∈ ℤ))
231 divcan5 11954 . . . . . . . . . . 11 ((((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ ∧ ((2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) ∧ (i ∈ ℂ ∧ i ≠ 0)) → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) = (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)))
23261, 63, 231mp3an23 1449 . . . . . . . . . 10 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) = (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)))
233157, 232syl 17 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) = (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)))
234233eleq1d 2814 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) ∈ ℤ ↔ (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ))
235230, 234bitr2d 279 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ ↔ (exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1))
23689adantl 480 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (𝐹𝑦) = (exp‘(i · 𝑦)))
237236eqeq2d 2739 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (𝑥 = (𝐹𝑦) ↔ 𝑥 = (exp‘(i · 𝑦))))
238228, 235, 2373imtr4d 293 . . . . . 6 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ → 𝑥 = (𝐹𝑦)))
239238reximdva 3165 . . . . 5 ((𝜑𝑥𝐶) → (∃𝑦𝐷 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ → ∃𝑦𝐷 𝑥 = (𝐹𝑦)))
240140, 239mpd 15 . . . 4 ((𝜑𝑥𝐶) → ∃𝑦𝐷 𝑥 = (𝐹𝑦))
241240ralrimiva 3143 . . 3 (𝜑 → ∀𝑥𝐶𝑦𝐷 𝑥 = (𝐹𝑦))
242 dffo3 7117 . . 3 (𝐹:𝐷onto𝐶 ↔ (𝐹:𝐷𝐶 ∧ ∀𝑥𝐶𝑦𝐷 𝑥 = (𝐹𝑦)))
24320, 241, 242sylanbrc 581 . 2 (𝜑𝐹:𝐷onto𝐶)
244 df-f1o 6560 . 2 (𝐹:𝐷1-1-onto𝐶 ↔ (𝐹:𝐷1-1𝐶𝐹:𝐷onto𝐶))
245114, 243, 244sylanbrc 581 1 (𝜑𝐹:𝐷1-1-onto𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098  wne 2937  wral 3058  wrex 3067  wss 3949  {csn 4632   class class class wbr 5152  cmpt 5235  ccnv 5681  cres 5684  cima 5685   Fn wfn 6548  wf 6549  1-1wf1 6550  ontowfo 6551  1-1-ontowf1o 6552  cfv 6553  (class class class)co 7426  cc 11144  cr 11145  0cc0 11146  1c1 11147  ici 11148   + caddc 11149   · cmul 11151   < clt 11286  cle 11287  cmin 11482  -cneg 11483   / cdiv 11909  2c2 12305  0cn0 12510  cz 12596  [,]cicc 13367  cexp 14066  cre 15084  cim 15085  csqrt 15220  abscabs 15221  expce 16045  sincsin 16047  cosccos 16048  πcpi 16050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-inf2 9672  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223  ax-pre-sup 11224  ax-addf 11225
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-iin 5003  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-of 7691  df-om 7877  df-1st 7999  df-2nd 8000  df-supp 8172  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-1o 8493  df-2o 8494  df-er 8731  df-map 8853  df-pm 8854  df-ixp 8923  df-en 8971  df-dom 8972  df-sdom 8973  df-fin 8974  df-fsupp 9394  df-fi 9442  df-sup 9473  df-inf 9474  df-oi 9541  df-card 9970  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-div 11910  df-nn 12251  df-2 12313  df-3 12314  df-4 12315  df-5 12316  df-6 12317  df-7 12318  df-8 12319  df-9 12320  df-n0 12511  df-z 12597  df-dec 12716  df-uz 12861  df-q 12971  df-rp 13015  df-xneg 13132  df-xadd 13133  df-xmul 13134  df-ioo 13368  df-ioc 13369  df-ico 13370  df-icc 13371  df-fz 13525  df-fzo 13668  df-fl 13797  df-mod 13875  df-seq 14007  df-exp 14067  df-fac 14273  df-bc 14302  df-hash 14330  df-shft 15054  df-cj 15086  df-re 15087  df-im 15088  df-sqrt 15222  df-abs 15223  df-limsup 15455  df-clim 15472  df-rlim 15473  df-sum 15673  df-ef 16051  df-sin 16053  df-cos 16054  df-pi 16056  df-struct 17123  df-sets 17140  df-slot 17158  df-ndx 17170  df-base 17188  df-ress 17217  df-plusg 17253  df-mulr 17254  df-starv 17255  df-sca 17256  df-vsca 17257  df-ip 17258  df-tset 17259  df-ple 17260  df-ds 17262  df-unif 17263  df-hom 17264  df-cco 17265  df-rest 17411  df-topn 17412  df-0g 17430  df-gsum 17431  df-topgen 17432  df-pt 17433  df-prds 17436  df-xrs 17491  df-qtop 17496  df-imas 17497  df-xps 17499  df-mre 17573  df-mrc 17574  df-acs 17576  df-mgm 18607  df-sgrp 18686  df-mnd 18702  df-submnd 18748  df-mulg 19031  df-cntz 19275  df-cmn 19744  df-psmet 21278  df-xmet 21279  df-met 21280  df-bl 21281  df-mopn 21282  df-fbas 21283  df-fg 21284  df-cnfld 21287  df-top 22816  df-topon 22833  df-topsp 22855  df-bases 22869  df-cld 22943  df-ntr 22944  df-cls 22945  df-nei 23022  df-lp 23060  df-perf 23061  df-cn 23151  df-cnp 23152  df-haus 23239  df-tx 23486  df-hmeo 23679  df-fil 23770  df-fm 23862  df-flim 23863  df-flf 23864  df-xms 24246  df-ms 24247  df-tms 24248  df-cncf 24818  df-limc 25815  df-dv 25816
This theorem is referenced by:  efif1o  26500  eff1olem  26502
  Copyright terms: Public domain W3C validator