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

Theorem efif1olem4 24229
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 3588 . . . . 5 ((𝜑𝑤𝐷) → 𝑤 ∈ ℝ)
3 ax-icn 9955 . . . . . . . . 9 i ∈ ℂ
4 recn 9986 . . . . . . . . 9 (𝑤 ∈ ℝ → 𝑤 ∈ ℂ)
5 mulcl 9980 . . . . . . . . 9 ((i ∈ ℂ ∧ 𝑤 ∈ ℂ) → (i · 𝑤) ∈ ℂ)
63, 4, 5sylancr 694 . . . . . . . 8 (𝑤 ∈ ℝ → (i · 𝑤) ∈ ℂ)
7 efcl 14757 . . . . . . . 8 ((i · 𝑤) ∈ ℂ → (exp‘(i · 𝑤)) ∈ ℂ)
86, 7syl 17 . . . . . . 7 (𝑤 ∈ ℝ → (exp‘(i · 𝑤)) ∈ ℂ)
9 absefi 14870 . . . . . . 7 (𝑤 ∈ ℝ → (abs‘(exp‘(i · 𝑤))) = 1)
10 absf 14027 . . . . . . . . 9 abs:ℂ⟶ℝ
11 ffn 6012 . . . . . . . . 9 (abs:ℂ⟶ℝ → abs Fn ℂ)
1210, 11ax-mp 5 . . . . . . . 8 abs Fn ℂ
13 fniniseg 6304 . . . . . . . 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 697 . . . . . 6 (𝑤 ∈ ℝ → (exp‘(i · 𝑤)) ∈ (abs “ {1}))
16 efif1o.2 . . . . . 6 𝐶 = (abs “ {1})
1715, 16syl6eleqr 2709 . . . . 5 (𝑤 ∈ ℝ → (exp‘(i · 𝑤)) ∈ 𝐶)
182, 17syl 17 . . . 4 ((𝜑𝑤𝐷) → (exp‘(i · 𝑤)) ∈ 𝐶)
19 efif1o.1 . . . 4 𝐹 = (𝑤𝐷 ↦ (exp‘(i · 𝑤)))
2018, 19fmptd 6351 . . 3 (𝜑𝐹:𝐷𝐶)
211ad2antrr 761 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝐷 ⊆ ℝ)
22 simplrl 799 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥𝐷)
2321, 22sseldd 3589 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 ∈ ℝ)
2423recnd 10028 . . . . . 6 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 ∈ ℂ)
25 simplrr 800 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑦𝐷)
2621, 25sseldd 3589 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑦 ∈ ℝ)
2726recnd 10028 . . . . . 6 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑦 ∈ ℂ)
2824, 27subcld 10352 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝑥𝑦) ∈ ℂ)
29 2re 11050 . . . . . . . . . . . 12 2 ∈ ℝ
30 pire 24148 . . . . . . . . . . . 12 π ∈ ℝ
3129, 30remulcli 10014 . . . . . . . . . . 11 (2 · π) ∈ ℝ
3231recni 10012 . . . . . . . . . 10 (2 · π) ∈ ℂ
33 2pos 11072 . . . . . . . . . . . 12 0 < 2
34 pipos 24150 . . . . . . . . . . . 12 0 < π
3529, 30, 33, 34mulgt0ii 10130 . . . . . . . . . . 11 0 < (2 · π)
3631, 35gt0ne0ii 10524 . . . . . . . . . 10 (2 · π) ≠ 0
37 divcl 10651 . . . . . . . . . 10 (((𝑥𝑦) ∈ ℂ ∧ (2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) → ((𝑥𝑦) / (2 · π)) ∈ ℂ)
3832, 36, 37mp3an23 1413 . . . . . . . . 9 ((𝑥𝑦) ∈ ℂ → ((𝑥𝑦) / (2 · π)) ∈ ℂ)
3928, 38syl 17 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((𝑥𝑦) / (2 · π)) ∈ ℂ)
40 absdiv 13985 . . . . . . . . . . . . 13 (((𝑥𝑦) ∈ ℂ ∧ (2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (abs‘(2 · π))))
4132, 36, 40mp3an23 1413 . . . . . . . . . . . 12 ((𝑥𝑦) ∈ ℂ → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (abs‘(2 · π))))
4228, 41syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (abs‘(2 · π))))
43 0re 10000 . . . . . . . . . . . . . 14 0 ∈ ℝ
4443, 31, 35ltleii 10120 . . . . . . . . . . . . 13 0 ≤ (2 · π)
45 absid 13986 . . . . . . . . . . . . 13 (((2 · π) ∈ ℝ ∧ 0 ≤ (2 · π)) → (abs‘(2 · π)) = (2 · π))
4631, 44, 45mp2an 707 . . . . . . . . . . . 12 (abs‘(2 · π)) = (2 · π)
4746oveq2i 6626 . . . . . . . . . . 11 ((abs‘(𝑥𝑦)) / (abs‘(2 · π))) = ((abs‘(𝑥𝑦)) / (2 · π))
4842, 47syl6eq 2671 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) = ((abs‘(𝑥𝑦)) / (2 · π)))
49 efif1olem4.4 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐷𝑦𝐷)) → (abs‘(𝑥𝑦)) < (2 · π))
5049adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘(𝑥𝑦)) < (2 · π))
5132mulid1i 10002 . . . . . . . . . . . 12 ((2 · π) · 1) = (2 · π)
5250, 51syl6breqr 4665 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘(𝑥𝑦)) < ((2 · π) · 1))
5328abscld 14125 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘(𝑥𝑦)) ∈ ℝ)
54 1re 9999 . . . . . . . . . . . . 13 1 ∈ ℝ
5531, 35pm3.2i 471 . . . . . . . . . . . . 13 ((2 · π) ∈ ℝ ∧ 0 < (2 · π))
56 ltdivmul 10858 . . . . . . . . . . . . 13 (((abs‘(𝑥𝑦)) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((2 · π) ∈ ℝ ∧ 0 < (2 · π))) → (((abs‘(𝑥𝑦)) / (2 · π)) < 1 ↔ (abs‘(𝑥𝑦)) < ((2 · π) · 1)))
5754, 55, 56mp3an23 1413 . . . . . . . . . . . 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 4645 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) < 1)
6132, 36pm3.2i 471 . . . . . . . . . . . . . 14 ((2 · π) ∈ ℂ ∧ (2 · π) ≠ 0)
62 ine0 10425 . . . . . . . . . . . . . . 15 i ≠ 0
633, 62pm3.2i 471 . . . . . . . . . . . . . 14 (i ∈ ℂ ∧ i ≠ 0)
64 divcan5 10687 . . . . . . . . . . . . . 14 (((𝑥𝑦) ∈ ℂ ∧ ((2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) ∧ (i ∈ ℂ ∧ i ≠ 0)) → ((i · (𝑥𝑦)) / (i · (2 · π))) = ((𝑥𝑦) / (2 · π)))
6561, 63, 64mp3an23 1413 . . . . . . . . . . . . 13 ((𝑥𝑦) ∈ ℂ → ((i · (𝑥𝑦)) / (i · (2 · π))) = ((𝑥𝑦) / (2 · π)))
6628, 65syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((i · (𝑥𝑦)) / (i · (2 · π))) = ((𝑥𝑦) / (2 · π)))
673a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → i ∈ ℂ)
6867, 24, 27subdid 10446 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · (𝑥𝑦)) = ((i · 𝑥) − (i · 𝑦)))
6968fveq2d 6162 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · (𝑥𝑦))) = (exp‘((i · 𝑥) − (i · 𝑦))))
70 mulcl 9980 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
713, 24, 70sylancr 694 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · 𝑥) ∈ ℂ)
72 mulcl 9980 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝑦 ∈ ℂ) → (i · 𝑦) ∈ ℂ)
733, 27, 72sylancr 694 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · 𝑦) ∈ ℂ)
74 efsub 14774 . . . . . . . . . . . . . . 15 (((i · 𝑥) ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → (exp‘((i · 𝑥) − (i · 𝑦))) = ((exp‘(i · 𝑥)) / (exp‘(i · 𝑦))))
7571, 73, 74syl2anc 692 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘((i · 𝑥) − (i · 𝑦))) = ((exp‘(i · 𝑥)) / (exp‘(i · 𝑦))))
76 efcl 14757 . . . . . . . . . . . . . . . 16 ((i · 𝑦) ∈ ℂ → (exp‘(i · 𝑦)) ∈ ℂ)
7773, 76syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · 𝑦)) ∈ ℂ)
78 efne0 14771 . . . . . . . . . . . . . . . 16 ((i · 𝑦) ∈ ℂ → (exp‘(i · 𝑦)) ≠ 0)
7973, 78syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · 𝑦)) ≠ 0)
80 simpr 477 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝐹𝑥) = (𝐹𝑦))
81 oveq2 6623 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑥 → (i · 𝑤) = (i · 𝑥))
8281fveq2d 6162 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑥 → (exp‘(i · 𝑤)) = (exp‘(i · 𝑥)))
83 fvex 6168 . . . . . . . . . . . . . . . . . 18 (exp‘(i · 𝑥)) ∈ V
8482, 19, 83fvmpt 6249 . . . . . . . . . . . . . . . . 17 (𝑥𝐷 → (𝐹𝑥) = (exp‘(i · 𝑥)))
8522, 84syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝐹𝑥) = (exp‘(i · 𝑥)))
86 oveq2 6623 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑦 → (i · 𝑤) = (i · 𝑦))
8786fveq2d 6162 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑦 → (exp‘(i · 𝑤)) = (exp‘(i · 𝑦)))
88 fvex 6168 . . . . . . . . . . . . . . . . . 18 (exp‘(i · 𝑦)) ∈ V
8987, 19, 88fvmpt 6249 . . . . . . . . . . . . . . . . 17 (𝑦𝐷 → (𝐹𝑦) = (exp‘(i · 𝑦)))
9025, 89syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝐹𝑦) = (exp‘(i · 𝑦)))
9180, 85, 903eqtr3d 2663 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · 𝑥)) = (exp‘(i · 𝑦)))
9277, 79, 91diveq1bd 10809 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((exp‘(i · 𝑥)) / (exp‘(i · 𝑦))) = 1)
9369, 75, 923eqtrd 2659 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (exp‘(i · (𝑥𝑦))) = 1)
94 mulcl 9980 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ (𝑥𝑦) ∈ ℂ) → (i · (𝑥𝑦)) ∈ ℂ)
953, 28, 94sylancr 694 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (i · (𝑥𝑦)) ∈ ℂ)
96 efeq1 24213 . . . . . . . . . . . . . 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 2699 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((𝑥𝑦) / (2 · π)) ∈ ℤ)
100 nn0abscl 14002 . . . . . . . . . . 11 (((𝑥𝑦) / (2 · π)) ∈ ℤ → (abs‘((𝑥𝑦) / (2 · π))) ∈ ℕ0)
10199, 100syl 17 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (abs‘((𝑥𝑦) / (2 · π))) ∈ ℕ0)
102 nn0lt10b 11399 . . . . . . . . . 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 14135 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ((𝑥𝑦) / (2 · π)) = 0)
106 diveq0 10655 . . . . . . . . 9 (((𝑥𝑦) ∈ ℂ ∧ (2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) → (((𝑥𝑦) / (2 · π)) = 0 ↔ (𝑥𝑦) = 0))
10732, 36, 106mp3an23 1413 . . . . . . . 8 ((𝑥𝑦) ∈ ℂ → (((𝑥𝑦) / (2 · π)) = 0 ↔ (𝑥𝑦) = 0))
10828, 107syl 17 . . . . . . 7 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (((𝑥𝑦) / (2 · π)) = 0 ↔ (𝑥𝑦) = 0))
109105, 108mpbid 222 . . . . . 6 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝑥𝑦) = 0)
11024, 27, 109subeq0d 10360 . . . . 5 (((𝜑 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 = 𝑦)
111110ex 450 . . . 4 ((𝜑 ∧ (𝑥𝐷𝑦𝐷)) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
112111ralrimivva 2967 . . 3 (𝜑 → ∀𝑥𝐷𝑦𝐷 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
113 dff13 6477 . . 3 (𝐹:𝐷1-1𝐶 ↔ (𝐹:𝐷𝐶 ∧ ∀𝑥𝐷𝑦𝐷 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
11420, 112, 113sylanbrc 697 . 2 (𝜑𝐹:𝐷1-1𝐶)
115 neghalfpire 24155 . . . . . . . . 9 -(π / 2) ∈ ℝ
116 halfpire 24154 . . . . . . . . 9 (π / 2) ∈ ℝ
117 iccssre 12213 . . . . . . . . 9 ((-(π / 2) ∈ ℝ ∧ (π / 2) ∈ ℝ) → (-(π / 2)[,](π / 2)) ⊆ ℝ)
118115, 116, 117mp2an 707 . . . . . . . 8 (-(π / 2)[,](π / 2)) ⊆ ℝ
11919, 16efif1olem3 24228 . . . . . . . . 9 ((𝜑𝑥𝐶) → (ℑ‘(√‘𝑥)) ∈ (-1[,]1))
120 resinf1o 24220 . . . . . . . . . . . 12 (sin ↾ (-(π / 2)[,](π / 2))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1)
121 efif1olem4.6 . . . . . . . . . . . . 13 𝑆 = (sin ↾ (-(π / 2)[,](π / 2)))
122 f1oeq1 6094 . . . . . . . . . . . . 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 221 . . . . . . . . . . 11 𝑆:(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1)
125 f1ocnv 6116 . . . . . . . . . . 11 (𝑆:(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) → 𝑆:(-1[,]1)–1-1-onto→(-(π / 2)[,](π / 2)))
126 f1of 6104 . . . . . . . . . . 11 (𝑆:(-1[,]1)–1-1-onto→(-(π / 2)[,](π / 2)) → 𝑆:(-1[,]1)⟶(-(π / 2)[,](π / 2)))
127124, 125, 126mp2b 10 . . . . . . . . . 10 𝑆:(-1[,]1)⟶(-(π / 2)[,](π / 2))
128127ffvelrni 6324 . . . . . . . . 9 ((ℑ‘(√‘𝑥)) ∈ (-1[,]1) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π / 2)))
129119, 128syl 17 . . . . . . . 8 ((𝜑𝑥𝐶) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π / 2)))
130118, 129sseldi 3586 . . . . . . 7 ((𝜑𝑥𝐶) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℝ)
131 remulcl 9981 . . . . . . 7 ((2 ∈ ℝ ∧ (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℝ) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
13229, 130, 131sylancr 694 . . . . . 6 ((𝜑𝑥𝐶) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
133 efif1olem4.5 . . . . . . . 8 ((𝜑𝑧 ∈ ℝ) → ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ)
134133ralrimiva 2962 . . . . . . 7 (𝜑 → ∀𝑧 ∈ ℝ ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ)
135134adantr 481 . . . . . 6 ((𝜑𝑥𝐶) → ∀𝑧 ∈ ℝ ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ)
136 oveq1 6622 . . . . . . . . . 10 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → (𝑧𝑦) = ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))
137136oveq1d 6630 . . . . . . . . 9 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → ((𝑧𝑦) / (2 · π)) = (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)))
138137eleq1d 2683 . . . . . . . 8 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → (((𝑧𝑦) / (2 · π)) ∈ ℤ ↔ (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ))
139138rexbidv 3047 . . . . . . 7 (𝑧 = (2 · (𝑆‘(ℑ‘(√‘𝑥)))) → (∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ ↔ ∃𝑦𝐷 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ))
140139rspcv 3295 . . . . . 6 ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ → (∀𝑧 ∈ ℝ ∃𝑦𝐷 ((𝑧𝑦) / (2 · π)) ∈ ℤ → ∃𝑦𝐷 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ))
141132, 135, 140sylc 65 . . . . 5 ((𝜑𝑥𝐶) → ∃𝑦𝐷 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ)
142 oveq1 6622 . . . . . . . 8 ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1 → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))) = (1 · (exp‘(i · 𝑦))))
1433a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → i ∈ ℂ)
144132adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
145144recnd 10028 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
1461ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝐷 ⊆ ℝ)
147 simpr 477 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝑦𝐷)
148146, 147sseldd 3589 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝑦 ∈ ℝ)
149148recnd 10028 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → 𝑦 ∈ ℂ)
150143, 145, 149subdid 10446 . . . . . . . . . . . . 13 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) = ((i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) − (i · 𝑦)))
151150oveq1d 6630 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦)) = (((i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) − (i · 𝑦)) + (i · 𝑦)))
152 mulcl 9980 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (2 · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) ∈ ℂ)
1533, 145, 152sylancr 694 . . . . . . . . . . . . 13 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) ∈ ℂ)
1543, 149, 72sylancr 694 . . . . . . . . . . . . 13 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · 𝑦) ∈ ℂ)
155153, 154npcand 10356 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (((i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) − (i · 𝑦)) + (i · 𝑦)) = (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))))
156151, 155eqtrd 2655 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦)) = (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))))
157156fveq2d 6162 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦))) = (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))))
158145, 149subcld 10352 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ)
159 mulcl 9980 . . . . . . . . . . . 12 ((i ∈ ℂ ∧ ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ) → (i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ)
1603, 158, 159sylancr 694 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ)
161 efadd 14768 . . . . . . . . . . 11 (((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → (exp‘((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦))) = ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))))
162160, 154, 161syl2anc 692 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) + (i · 𝑦))) = ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))))
163130recnd 10028 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ)
164 2cn 11051 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
165 mul12 10162 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 2 ∈ ℂ ∧ (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) = (2 · (i · (𝑆‘(ℑ‘(√‘𝑥))))))
1663, 164, 165mp3an12 1411 . . . . . . . . . . . . . . 15 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) = (2 · (i · (𝑆‘(ℑ‘(√‘𝑥))))))
167163, 166syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (i · (2 · (𝑆‘(ℑ‘(√‘𝑥))))) = (2 · (i · (𝑆‘(ℑ‘(√‘𝑥))))))
168167fveq2d 6162 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = (exp‘(2 · (i · (𝑆‘(ℑ‘(√‘𝑥)))))))
169 mulcl 9980 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ (𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ) → (i · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
1703, 163, 169sylancr 694 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (i · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
171 2z 11369 . . . . . . . . . . . . . 14 2 ∈ ℤ
172 efexp 14775 . . . . . . . . . . . . . 14 (((i · (𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ ∧ 2 ∈ ℤ) → (exp‘(2 · (i · (𝑆‘(ℑ‘(√‘𝑥)))))) = ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2))
173170, 171, 172sylancl 693 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → (exp‘(2 · (i · (𝑆‘(ℑ‘(√‘𝑥)))))) = ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2))
174168, 173eqtrd 2655 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2))
175130recoscld 14818 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → (cos‘(𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℝ)
176 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥𝐶) → 𝑥𝐶)
177176, 16syl6eleq 2708 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝑥 ∈ (abs “ {1}))
178 fniniseg 6304 . . . . . . . . . . . . . . . . . . . . 21 (abs Fn ℂ → (𝑥 ∈ (abs “ {1}) ↔ (𝑥 ∈ ℂ ∧ (abs‘𝑥) = 1)))
17912, 178ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (abs “ {1}) ↔ (𝑥 ∈ ℂ ∧ (abs‘𝑥) = 1))
180177, 179sylib 208 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (𝑥 ∈ ℂ ∧ (abs‘𝑥) = 1))
181180simpld 475 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → 𝑥 ∈ ℂ)
182181sqrtcld 14126 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → (√‘𝑥) ∈ ℂ)
183182recld 13884 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → (ℜ‘(√‘𝑥)) ∈ ℝ)
184 cosq14ge0 24201 . . . . . . . . . . . . . . . . 17 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π / 2)) → 0 ≤ (cos‘(𝑆‘(ℑ‘(√‘𝑥)))))
185129, 184syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → 0 ≤ (cos‘(𝑆‘(ℑ‘(√‘𝑥)))))
186181sqrtrege0d 14127 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → 0 ≤ (ℜ‘(√‘𝑥)))
187 sincossq 14850 . . . . . . . . . . . . . . . . . . . 20 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ → (((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = 1)
188163, 187syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = 1)
189181sqsqrtd 14128 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥𝐶) → ((√‘𝑥)↑2) = 𝑥)
190189fveq2d 6162 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (abs‘((√‘𝑥)↑2)) = (abs‘𝑥))
191 2nn0 11269 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℕ0
192 absexp 13994 . . . . . . . . . . . . . . . . . . . . 21 (((√‘𝑥) ∈ ℂ ∧ 2 ∈ ℕ0) → (abs‘((√‘𝑥)↑2)) = ((abs‘(√‘𝑥))↑2))
193182, 191, 192sylancl 693 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (abs‘((√‘𝑥)↑2)) = ((abs‘(√‘𝑥))↑2))
194180simprd 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (abs‘𝑥) = 1)
195190, 193, 1943eqtr3d 2663 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → ((abs‘(√‘𝑥))↑2) = 1)
196182absvalsq2d 14132 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → ((abs‘(√‘𝑥))↑2) = (((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)))
197188, 195, 1963eqtr2d 2661 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → (((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = (((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)))
198121fveq1i 6159 . . . . . . . . . . . . . . . . . . . . 21 (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = ((sin ↾ (-(π / 2)[,](π / 2)))‘(𝑆‘(ℑ‘(√‘𝑥))))
199 fvres 6174 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ (-(π / 2)[,](π / 2)) → ((sin ↾ (-(π / 2)[,](π / 2)))‘(𝑆‘(ℑ‘(√‘𝑥)))) = (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))
200129, 199syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥𝐶) → ((sin ↾ (-(π / 2)[,](π / 2)))‘(𝑆‘(ℑ‘(√‘𝑥)))) = (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))
201198, 200syl5eq 2667 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))
202 f1ocnvfv2 6498 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆:(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) ∧ (ℑ‘(√‘𝑥)) ∈ (-1[,]1)) → (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℑ‘(√‘𝑥)))
203124, 119, 202sylancr 694 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → (𝑆‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℑ‘(√‘𝑥)))
204201, 203eqtr3d 2657 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (sin‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℑ‘(√‘𝑥)))
205204oveq1d 6630 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) = ((ℑ‘(√‘𝑥))↑2))
206197, 205oveq12d 6633 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) − ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = ((((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)) − ((ℑ‘(√‘𝑥))↑2)))
207163sincld 14804 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (sin‘(𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
208207sqcld 12962 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) ∈ ℂ)
209163coscld 14805 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (cos‘(𝑆‘(ℑ‘(√‘𝑥)))) ∈ ℂ)
210209sqcld 12962 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) ∈ ℂ)
211208, 210pncan2d 10354 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) + ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) − ((sin‘(𝑆‘(ℑ‘(√‘𝑥))))↑2)) = ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2))
212183recnd 10028 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (ℜ‘(√‘𝑥)) ∈ ℂ)
213212sqcld 12962 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((ℜ‘(√‘𝑥))↑2) ∈ ℂ)
214205, 208eqeltrrd 2699 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → ((ℑ‘(√‘𝑥))↑2) ∈ ℂ)
215213, 214pncand 10353 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((((ℜ‘(√‘𝑥))↑2) + ((ℑ‘(√‘𝑥))↑2)) − ((ℑ‘(√‘𝑥))↑2)) = ((ℜ‘(√‘𝑥))↑2))
216206, 211, 2153eqtr3d 2663 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → ((cos‘(𝑆‘(ℑ‘(√‘𝑥))))↑2) = ((ℜ‘(√‘𝑥))↑2))
217175, 183, 185, 186, 216sq11d 13001 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (cos‘(𝑆‘(ℑ‘(√‘𝑥)))) = (ℜ‘(√‘𝑥)))
218204oveq2d 6631 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥))))) = (i · (ℑ‘(√‘𝑥))))
219217, 218oveq12d 6633 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → ((cos‘(𝑆‘(ℑ‘(√‘𝑥)))) + (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))) = ((ℜ‘(√‘𝑥)) + (i · (ℑ‘(√‘𝑥)))))
220 efival 14826 . . . . . . . . . . . . . . 15 ((𝑆‘(ℑ‘(√‘𝑥))) ∈ ℂ → (exp‘(i · (𝑆‘(ℑ‘(√‘𝑥))))) = ((cos‘(𝑆‘(ℑ‘(√‘𝑥)))) + (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))))
221163, 220syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (exp‘(i · (𝑆‘(ℑ‘(√‘𝑥))))) = ((cos‘(𝑆‘(ℑ‘(√‘𝑥)))) + (i · (sin‘(𝑆‘(ℑ‘(√‘𝑥)))))))
222182replimd 13887 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (√‘𝑥) = ((ℜ‘(√‘𝑥)) + (i · (ℑ‘(√‘𝑥)))))
223219, 221, 2223eqtr4d 2665 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → (exp‘(i · (𝑆‘(ℑ‘(√‘𝑥))))) = (√‘𝑥))
224223oveq1d 6630 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → ((exp‘(i · (𝑆‘(ℑ‘(√‘𝑥)))))↑2) = ((√‘𝑥)↑2))
225174, 224, 1893eqtrd 2659 . . . . . . . . . . 11 ((𝜑𝑥𝐶) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = 𝑥)
226225adantr 481 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘(i · (2 · (𝑆‘(ℑ‘(√‘𝑥)))))) = 𝑥)
227157, 162, 2263eqtr3d 2663 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))) = 𝑥)
228154, 76syl 17 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (exp‘(i · 𝑦)) ∈ ℂ)
229228mulid2d 10018 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (1 · (exp‘(i · 𝑦))) = (exp‘(i · 𝑦)))
230227, 229eqeq12d 2636 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) · (exp‘(i · 𝑦))) = (1 · (exp‘(i · 𝑦))) ↔ 𝑥 = (exp‘(i · 𝑦))))
231142, 230syl5ib 234 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1 → 𝑥 = (exp‘(i · 𝑦))))
232 efeq1 24213 . . . . . . . . 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 10687 . . . . . . . . . . 11 ((((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ ∧ ((2 · π) ∈ ℂ ∧ (2 · π) ≠ 0) ∧ (i ∈ ℂ ∧ i ≠ 0)) → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) = (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)))
23561, 63, 234mp3an23 1413 . . . . . . . . . 10 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) ∈ ℂ → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) = (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)))
236158, 235syl 17 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) = (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)))
237236eleq1d 2683 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (((i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦)) / (i · (2 · π))) ∈ ℤ ↔ (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ))
238233, 237bitr2d 269 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ ↔ (exp‘(i · ((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦))) = 1))
23989adantl 482 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (𝐹𝑦) = (exp‘(i · 𝑦)))
240239eqeq2d 2631 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → (𝑥 = (𝐹𝑦) ↔ 𝑥 = (exp‘(i · 𝑦))))
241231, 238, 2403imtr4d 283 . . . . . 6 (((𝜑𝑥𝐶) ∧ 𝑦𝐷) → ((((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ → 𝑥 = (𝐹𝑦)))
242241reximdva 3013 . . . . 5 ((𝜑𝑥𝐶) → (∃𝑦𝐷 (((2 · (𝑆‘(ℑ‘(√‘𝑥)))) − 𝑦) / (2 · π)) ∈ ℤ → ∃𝑦𝐷 𝑥 = (𝐹𝑦)))
243141, 242mpd 15 . . . 4 ((𝜑𝑥𝐶) → ∃𝑦𝐷 𝑥 = (𝐹𝑦))
244243ralrimiva 2962 . . 3 (𝜑 → ∀𝑥𝐶𝑦𝐷 𝑥 = (𝐹𝑦))
245 dffo3 6340 . . 3 (𝐹:𝐷onto𝐶 ↔ (𝐹:𝐷𝐶 ∧ ∀𝑥𝐶𝑦𝐷 𝑥 = (𝐹𝑦)))
24620, 244, 245sylanbrc 697 . 2 (𝜑𝐹:𝐷onto𝐶)
247 df-f1o 5864 . 2 (𝐹:𝐷1-1-onto𝐶 ↔ (𝐹:𝐷1-1𝐶𝐹:𝐷onto𝐶))
248114, 246, 247sylanbrc 697 1 (𝜑𝐹:𝐷1-1-onto𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wne 2790  wral 2908  wrex 2909  wss 3560  {csn 4155   class class class wbr 4623  cmpt 4683  ccnv 5083  cres 5086  cima 5087   Fn wfn 5852  wf 5853  1-1wf1 5854  ontowfo 5855  1-1-ontowf1o 5856  cfv 5857  (class class class)co 6615  cc 9894  cr 9895  0cc0 9896  1c1 9897  ici 9898   + caddc 9899   · cmul 9901   < clt 10034  cle 10035  cmin 10226  -cneg 10227   / cdiv 10644  2c2 11030  0cn0 11252  cz 11337  [,]cicc 12136  cexp 12816  cre 13787  cim 13788  csqrt 13923  abscabs 13924  expce 14736  sincsin 14738  cosccos 14739  πcpi 14741
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-inf2 8498  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-pre-sup 9974  ax-addf 9975  ax-mulf 9976
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-iin 4495  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-se 5044  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-isom 5866  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-of 6862  df-om 7028  df-1st 7128  df-2nd 7129  df-supp 7256  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-2o 7521  df-oadd 7524  df-er 7702  df-map 7819  df-pm 7820  df-ixp 7869  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-fsupp 8236  df-fi 8277  df-sup 8308  df-inf 8309  df-oi 8375  df-card 8725  df-cda 8950  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-4 11041  df-5 11042  df-6 11043  df-7 11044  df-8 11045  df-9 11046  df-n0 11253  df-z 11338  df-dec 11454  df-uz 11648  df-q 11749  df-rp 11793  df-xneg 11906  df-xadd 11907  df-xmul 11908  df-ioo 12137  df-ioc 12138  df-ico 12139  df-icc 12140  df-fz 12285  df-fzo 12423  df-fl 12549  df-mod 12625  df-seq 12758  df-exp 12817  df-fac 13017  df-bc 13046  df-hash 13074  df-shft 13757  df-cj 13789  df-re 13790  df-im 13791  df-sqrt 13925  df-abs 13926  df-limsup 14152  df-clim 14169  df-rlim 14170  df-sum 14367  df-ef 14742  df-sin 14744  df-cos 14745  df-pi 14747  df-struct 15802  df-ndx 15803  df-slot 15804  df-base 15805  df-sets 15806  df-ress 15807  df-plusg 15894  df-mulr 15895  df-starv 15896  df-sca 15897  df-vsca 15898  df-ip 15899  df-tset 15900  df-ple 15901  df-ds 15904  df-unif 15905  df-hom 15906  df-cco 15907  df-rest 16023  df-topn 16024  df-0g 16042  df-gsum 16043  df-topgen 16044  df-pt 16045  df-prds 16048  df-xrs 16102  df-qtop 16107  df-imas 16108  df-xps 16110  df-mre 16186  df-mrc 16187  df-acs 16189  df-mgm 17182  df-sgrp 17224  df-mnd 17235  df-submnd 17276  df-mulg 17481  df-cntz 17690  df-cmn 18135  df-psmet 19678  df-xmet 19679  df-met 19680  df-bl 19681  df-mopn 19682  df-fbas 19683  df-fg 19684  df-cnfld 19687  df-top 20639  df-topon 20656  df-topsp 20677  df-bases 20690  df-cld 20763  df-ntr 20764  df-cls 20765  df-nei 20842  df-lp 20880  df-perf 20881  df-cn 20971  df-cnp 20972  df-haus 21059  df-tx 21305  df-hmeo 21498  df-fil 21590  df-fm 21682  df-flim 21683  df-flf 21684  df-xms 22065  df-ms 22066  df-tms 22067  df-cncf 22621  df-limc 23570  df-dv 23571
This theorem is referenced by:  efif1o  24230  eff1olem  24232
  Copyright terms: Public domain W3C validator