Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvasin Structured version   Visualization version   GIF version

Theorem dvasin 34859
Description: Derivative of arcsine. (Contributed by Brendan Leahy, 18-Dec-2018.)
Hypothesis
Ref Expression
dvasin.d 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))
Assertion
Ref Expression
dvasin (ℂ D (arcsin ↾ 𝐷)) = (𝑥𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))
Distinct variable group:   𝑥,𝐷

Proof of Theorem dvasin
Dummy variables 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-asin 25370 . . . . 5 arcsin = (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
21reseq1i 5842 . . . 4 (arcsin ↾ 𝐷) = ((𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷)
3 dvasin.d . . . . . 6 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))
4 difss 4105 . . . . . 6 (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⊆ ℂ
53, 4eqsstri 3998 . . . . 5 𝐷 ⊆ ℂ
6 resmpt 5898 . . . . 5 (𝐷 ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷) = (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))))
75, 6ax-mp 5 . . . 4 ((𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷) = (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
82, 7eqtri 2841 . . 3 (arcsin ↾ 𝐷) = (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
98oveq2i 7156 . 2 (ℂ D (arcsin ↾ 𝐷)) = (ℂ D (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))))
10 cnelprrecn 10618 . . . . 5 ℂ ∈ {ℝ, ℂ}
1110a1i 11 . . . 4 (⊤ → ℂ ∈ {ℝ, ℂ})
125sseli 3960 . . . . . . 7 (𝑥𝐷𝑥 ∈ ℂ)
13 ax-icn 10584 . . . . . . . . 9 i ∈ ℂ
14 mulcl 10609 . . . . . . . . 9 ((i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
1513, 14mpan 686 . . . . . . . 8 (𝑥 ∈ ℂ → (i · 𝑥) ∈ ℂ)
16 ax-1cn 10583 . . . . . . . . . 10 1 ∈ ℂ
17 sqcl 13472 . . . . . . . . . 10 (𝑥 ∈ ℂ → (𝑥↑2) ∈ ℂ)
18 subcl 10873 . . . . . . . . . 10 ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ)
1916, 17, 18sylancr 587 . . . . . . . . 9 (𝑥 ∈ ℂ → (1 − (𝑥↑2)) ∈ ℂ)
2019sqrtcld 14785 . . . . . . . 8 (𝑥 ∈ ℂ → (√‘(1 − (𝑥↑2))) ∈ ℂ)
2115, 20addcld 10648 . . . . . . 7 (𝑥 ∈ ℂ → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
2212, 21syl 17 . . . . . 6 (𝑥𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
23 asinlem 25373 . . . . . . 7 (𝑥 ∈ ℂ → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
2412, 23syl 17 . . . . . 6 (𝑥𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
2522, 24logcld 25081 . . . . 5 (𝑥𝐷 → (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
2625adantl 482 . . . 4 ((⊤ ∧ 𝑥𝐷) → (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
27 ovexd 7180 . . . 4 ((⊤ ∧ 𝑥𝐷) → (i / (√‘(1 − (𝑥↑2)))) ∈ V)
28 simpr 485 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)
29 asinlem3 25376 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → 0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
30 rere 14469 . . . . . . . . . . . . . . . . . . 19 (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
3130breq2d 5069 . . . . . . . . . . . . . . . . . 18 (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ↔ 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
3231biimpac 479 . . . . . . . . . . . . . . . . 17 ((0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
3329, 32sylan 580 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
3423adantr 481 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
3528, 33, 34ne0gt0d 10765 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
36 0re 10631 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ
37 ltnle 10708 . . . . . . . . . . . . . . . . 17 ((0 ∈ ℝ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
3836, 37mpan 686 . . . . . . . . . . . . . . . 16 (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
3938adantl 482 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
4035, 39mpbid 233 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0)
4140ex 413 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
4212, 41syl 17 . . . . . . . . . . . 12 (𝑥𝐷 → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
43 imor 847 . . . . . . . . . . . 12 ((((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
4442, 43sylib 219 . . . . . . . . . . 11 (𝑥𝐷 → (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
4544orcomd 865 . . . . . . . . . 10 (𝑥𝐷 → (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ))
4645olcd 870 . . . . . . . . 9 (𝑥𝐷 → (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)))
47 3ianor 1099 . . . . . . . . . . 11 (¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
48 3orrot 1084 . . . . . . . . . . 11 ((¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ))
49 3orass 1082 . . . . . . . . . . 11 ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) ↔ (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)))
5047, 48, 493bitrri 299 . . . . . . . . . 10 ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)) ↔ ¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
51 mnfxr 10686 . . . . . . . . . . 11 -∞ ∈ ℝ*
52 elioc2 12787 . . . . . . . . . . 11 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0)))
5351, 36, 52mp2an 688 . . . . . . . . . 10 (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
5450, 53xchbinxr 336 . . . . . . . . 9 ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0))
5546, 54sylib 219 . . . . . . . 8 (𝑥𝐷 → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0))
5622, 55eldifd 3944 . . . . . . 7 (𝑥𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
5756adantl 482 . . . . . 6 ((⊤ ∧ 𝑥𝐷) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
58 ovexd 7180 . . . . . 6 ((⊤ ∧ 𝑥𝐷) → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))) ∈ V)
59 eldifi 4100 . . . . . . . 8 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ∈ ℂ)
60 eldifn 4101 . . . . . . . . 9 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → ¬ 𝑦 ∈ (-∞(,]0))
61 0xr 10676 . . . . . . . . . . . 12 0 ∈ ℝ*
62 mnflt0 12508 . . . . . . . . . . . 12 -∞ < 0
63 ubioc1 12778 . . . . . . . . . . . 12 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ -∞ < 0) → 0 ∈ (-∞(,]0))
6451, 61, 62, 63mp3an 1452 . . . . . . . . . . 11 0 ∈ (-∞(,]0)
65 eleq1 2897 . . . . . . . . . . 11 (𝑦 = 0 → (𝑦 ∈ (-∞(,]0) ↔ 0 ∈ (-∞(,]0)))
6664, 65mpbiri 259 . . . . . . . . . 10 (𝑦 = 0 → 𝑦 ∈ (-∞(,]0))
6766necon3bi 3039 . . . . . . . . 9 𝑦 ∈ (-∞(,]0) → 𝑦 ≠ 0)
6860, 67syl 17 . . . . . . . 8 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ≠ 0)
6959, 68logcld 25081 . . . . . . 7 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → (log‘𝑦) ∈ ℂ)
7069adantl 482 . . . . . 6 ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ)
71 ovexd 7180 . . . . . 6 ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ V)
7213a1i 11 . . . . . . . . . 10 (𝑥𝐷 → i ∈ ℂ)
7372, 12mulcld 10649 . . . . . . . . 9 (𝑥𝐷 → (i · 𝑥) ∈ ℂ)
7473adantl 482 . . . . . . . 8 ((⊤ ∧ 𝑥𝐷) → (i · 𝑥) ∈ ℂ)
7513a1i 11 . . . . . . . 8 ((⊤ ∧ 𝑥𝐷) → i ∈ ℂ)
7612adantl 482 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝐷) → 𝑥 ∈ ℂ)
77 1cnd 10624 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝐷) → 1 ∈ ℂ)
78 simpr 485 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
79 1cnd 10624 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → 1 ∈ ℂ)
8011dvmptid 24481 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1))
815a1i 11 . . . . . . . . . . 11 (⊤ → 𝐷 ⊆ ℂ)
82 eqid 2818 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
8382cnfldtopon 23318 . . . . . . . . . . . 12 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
8483toponrestid 21457 . . . . . . . . . . 11 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
8582recld2 23349 . . . . . . . . . . . . . . 15 ℝ ∈ (Clsd‘(TopOpen‘ℂfld))
86 neg1rr 11740 . . . . . . . . . . . . . . . . . 18 -1 ∈ ℝ
87 iocmnfcld 23304 . . . . . . . . . . . . . . . . . 18 (-1 ∈ ℝ → (-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))))
8886, 87ax-mp 5 . . . . . . . . . . . . . . . . 17 (-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,)))
89 1re 10629 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
90 icopnfcld 23303 . . . . . . . . . . . . . . . . . 18 (1 ∈ ℝ → (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,))))
9189, 90ax-mp 5 . . . . . . . . . . . . . . . . 17 (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))
92 uncld 21577 . . . . . . . . . . . . . . . . 17 (((-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))) ∧ (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran (,))))
9388, 91, 92mp2an 688 . . . . . . . . . . . . . . . 16 ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran (,)))
9482tgioo2 23338 . . . . . . . . . . . . . . . . 17 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
9594fveq2i 6666 . . . . . . . . . . . . . . . 16 (Clsd‘(topGen‘ran (,))) = (Clsd‘((TopOpen‘ℂfld) ↾t ℝ))
9693, 95eleqtri 2908 . . . . . . . . . . . . . . 15 ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘((TopOpen‘ℂfld) ↾t ℝ))
97 restcldr 21710 . . . . . . . . . . . . . . 15 ((ℝ ∈ (Clsd‘(TopOpen‘ℂfld)) ∧ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘((TopOpen‘ℂfld) ↾t ℝ))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂfld)))
9885, 96, 97mp2an 688 . . . . . . . . . . . . . 14 ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂfld))
9983toponunii 21452 . . . . . . . . . . . . . . 15 ℂ = (TopOpen‘ℂfld)
10099cldopn 21567 . . . . . . . . . . . . . 14 (((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂfld)) → (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈ (TopOpen‘ℂfld))
10198, 100ax-mp 5 . . . . . . . . . . . . 13 (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈ (TopOpen‘ℂfld)
1023, 101eqeltri 2906 . . . . . . . . . . . 12 𝐷 ∈ (TopOpen‘ℂfld)
103102a1i 11 . . . . . . . . . . 11 (⊤ → 𝐷 ∈ (TopOpen‘ℂfld))
10411, 78, 79, 80, 81, 84, 82, 103dvmptres 24487 . . . . . . . . . 10 (⊤ → (ℂ D (𝑥𝐷𝑥)) = (𝑥𝐷 ↦ 1))
10513a1i 11 . . . . . . . . . 10 (⊤ → i ∈ ℂ)
10611, 76, 77, 104, 105dvmptcmul 24488 . . . . . . . . 9 (⊤ → (ℂ D (𝑥𝐷 ↦ (i · 𝑥))) = (𝑥𝐷 ↦ (i · 1)))
10713mulid1i 10633 . . . . . . . . . 10 (i · 1) = i
108107mpteq2i 5149 . . . . . . . . 9 (𝑥𝐷 ↦ (i · 1)) = (𝑥𝐷 ↦ i)
109106, 108syl6eq 2869 . . . . . . . 8 (⊤ → (ℂ D (𝑥𝐷 ↦ (i · 𝑥))) = (𝑥𝐷 ↦ i))
11012sqcld 13496 . . . . . . . . . . 11 (𝑥𝐷 → (𝑥↑2) ∈ ℂ)
11116, 110, 18sylancr 587 . . . . . . . . . 10 (𝑥𝐷 → (1 − (𝑥↑2)) ∈ ℂ)
112111sqrtcld 14785 . . . . . . . . 9 (𝑥𝐷 → (√‘(1 − (𝑥↑2))) ∈ ℂ)
113112adantl 482 . . . . . . . 8 ((⊤ ∧ 𝑥𝐷) → (√‘(1 − (𝑥↑2))) ∈ ℂ)
114 ovexd 7180 . . . . . . . 8 ((⊤ ∧ 𝑥𝐷) → (-𝑥 / (√‘(1 − (𝑥↑2)))) ∈ V)
115 elin 4166 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐷 ∩ ℝ) ↔ (𝑥𝐷𝑥 ∈ ℝ))
1163asindmre 34858 . . . . . . . . . . . . . . . . 17 (𝐷 ∩ ℝ) = (-1(,)1)
117116eqimssi 4022 . . . . . . . . . . . . . . . 16 (𝐷 ∩ ℝ) ⊆ (-1(,)1)
118117sseli 3960 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐷 ∩ ℝ) → 𝑥 ∈ (-1(,)1))
119115, 118sylbir 236 . . . . . . . . . . . . . 14 ((𝑥𝐷𝑥 ∈ ℝ) → 𝑥 ∈ (-1(,)1))
120 incom 4175 . . . . . . . . . . . . . . . 16 ((0(,)+∞) ∩ (-∞(,]0)) = ((-∞(,]0) ∩ (0(,)+∞))
121 pnfxr 10683 . . . . . . . . . . . . . . . . 17 +∞ ∈ ℝ*
122 df-ioc 12731 . . . . . . . . . . . . . . . . . 18 (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
123 df-ioo 12730 . . . . . . . . . . . . . . . . . 18 (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
124 xrltnle 10696 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℝ*𝑤 ∈ ℝ*) → (0 < 𝑤 ↔ ¬ 𝑤 ≤ 0))
125122, 123, 124ixxdisj 12741 . . . . . . . . . . . . . . . . 17 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((-∞(,]0) ∩ (0(,)+∞)) = ∅)
12651, 61, 121, 125mp3an 1452 . . . . . . . . . . . . . . . 16 ((-∞(,]0) ∩ (0(,)+∞)) = ∅
127120, 126eqtri 2841 . . . . . . . . . . . . . . 15 ((0(,)+∞) ∩ (-∞(,]0)) = ∅
128 elioore 12756 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (-1(,)1) → 𝑥 ∈ ℝ)
129128resqcld 13599 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (-1(,)1) → (𝑥↑2) ∈ ℝ)
130 resubcl 10938 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → (1 − (𝑥↑2)) ∈ ℝ)
13189, 129, 130sylancr 587 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ ℝ)
13286rexri 10687 . . . . . . . . . . . . . . . . . . 19 -1 ∈ ℝ*
133 1xr 10688 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ*
134 elioo2 12767 . . . . . . . . . . . . . . . . . . 19 ((-1 ∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 < 𝑥𝑥 < 1)))
135132, 133, 134mp2an 688 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 < 𝑥𝑥 < 1))
136 recn 10615 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
137136abscld 14784 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → (abs‘𝑥) ∈ ℝ)
138136absge0d 14792 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → 0 ≤ (abs‘𝑥))
139 0le1 11151 . . . . . . . . . . . . . . . . . . . . . . 23 0 ≤ 1
140 lt2sq 13486 . . . . . . . . . . . . . . . . . . . . . . 23 ((((abs‘𝑥) ∈ ℝ ∧ 0 ≤ (abs‘𝑥)) ∧ (1 ∈ ℝ ∧ 0 ≤ 1)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
14189, 139, 140mpanr12 701 . . . . . . . . . . . . . . . . . . . . . 22 (((abs‘𝑥) ∈ ℝ ∧ 0 ≤ (abs‘𝑥)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
142137, 138, 141syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
143 abslt 14662 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥𝑥 < 1)))
14489, 143mpan2 687 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥𝑥 < 1)))
145 absresq 14650 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → ((abs‘𝑥)↑2) = (𝑥↑2))
146 sq1 13546 . . . . . . . . . . . . . . . . . . . . . . . 24 (1↑2) = 1
147146a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → (1↑2) = 1)
148145, 147breq12d 5070 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → (((abs‘𝑥)↑2) < (1↑2) ↔ (𝑥↑2) < 1))
149 resqcl 13478 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → (𝑥↑2) ∈ ℝ)
150 posdif 11121 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥↑2) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝑥↑2) < 1 ↔ 0 < (1 − (𝑥↑2))))
151149, 89, 150sylancl 586 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → ((𝑥↑2) < 1 ↔ 0 < (1 − (𝑥↑2))))
152148, 151bitrd 280 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → (((abs‘𝑥)↑2) < (1↑2) ↔ 0 < (1 − (𝑥↑2))))
153142, 144, 1523bitr3d 310 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → ((-1 < 𝑥𝑥 < 1) ↔ 0 < (1 − (𝑥↑2))))
154153biimpd 230 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → ((-1 < 𝑥𝑥 < 1) → 0 < (1 − (𝑥↑2))))
1551543impib 1108 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ -1 < 𝑥𝑥 < 1) → 0 < (1 − (𝑥↑2)))
156135, 155sylbi 218 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (-1(,)1) → 0 < (1 − (𝑥↑2)))
157131, 156elrpd 12416 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ ℝ+)
158 ioorp 12802 . . . . . . . . . . . . . . . 16 (0(,)+∞) = ℝ+
159157, 158eleqtrrdi 2921 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ (0(,)+∞))
160 disjel 4402 . . . . . . . . . . . . . . 15 ((((0(,)+∞) ∩ (-∞(,]0)) = ∅ ∧ (1 − (𝑥↑2)) ∈ (0(,)+∞)) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
161127, 159, 160sylancr 587 . . . . . . . . . . . . . 14 (𝑥 ∈ (-1(,)1) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
162119, 161syl 17 . . . . . . . . . . . . 13 ((𝑥𝐷𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
163 elioc2 12787 . . . . . . . . . . . . . . . . . . . . . . . 24 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) → ((1 − (𝑥↑2)) ∈ (-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0)))
16451, 36, 163mp2an 688 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 − (𝑥↑2)) ∈ (-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0))
165164biimpi 217 . . . . . . . . . . . . . . . . . . . . . 22 ((1 − (𝑥↑2)) ∈ (-∞(,]0) → ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0))
166165simp1d 1134 . . . . . . . . . . . . . . . . . . . . 21 ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (𝑥↑2)) ∈ ℝ)
167 resubcl 10938 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (1 − (1 − (𝑥↑2))) ∈ ℝ)
16889, 166, 167sylancr 587 . . . . . . . . . . . . . . . . . . . 20 ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (1 − (𝑥↑2))) ∈ ℝ)
169 nncan 10903 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
17016, 169mpan 686 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥↑2) ∈ ℂ → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
171170eleq1d 2894 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥↑2) ∈ ℂ → ((1 − (1 − (𝑥↑2))) ∈ ℝ ↔ (𝑥↑2) ∈ ℝ))
172171biimpa 477 . . . . . . . . . . . . . . . . . . . 20 (((𝑥↑2) ∈ ℂ ∧ (1 − (1 − (𝑥↑2))) ∈ ℝ) → (𝑥↑2) ∈ ℝ)
173168, 172sylan2 592 . . . . . . . . . . . . . . . . . . 19 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥↑2) ∈ ℝ)
174166adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ∈ ℝ)
175165simp3d 1136 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (𝑥↑2)) ≤ 0)
176175adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ≤ 0)
177 letr 10722 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1 − (𝑥↑2)) ∈ ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ) → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1 − (𝑥↑2)) ≤ 1))
17836, 89, 177mp3an23 1444 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 − (𝑥↑2)) ∈ ℝ → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1 − (𝑥↑2)) ≤ 1))
179139, 178mpan2i 693 . . . . . . . . . . . . . . . . . . . . . 22 ((1 − (𝑥↑2)) ∈ ℝ → ((1 − (𝑥↑2)) ≤ 0 → (1 − (𝑥↑2)) ≤ 1))
180174, 176, 179sylc 65 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ≤ 1)
181 subge0 11141 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤ 1))
18289, 174, 181sylancr 587 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤ 1))
183180, 182mpbird 258 . . . . . . . . . . . . . . . . . . . 20 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 0 ≤ (1 − (1 − (𝑥↑2))))
184170adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
185183, 184breqtrd 5083 . . . . . . . . . . . . . . . . . . 19 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 0 ≤ (𝑥↑2))
186173, 185resqrtcld 14765 . . . . . . . . . . . . . . . . . 18 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ)
18717, 186sylan 580 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ)
188 eleq1 2897 . . . . . . . . . . . . . . . . 17 (𝑥 = (√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔ (√‘(𝑥↑2)) ∈ ℝ))
189187, 188syl5ibrcom 248 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = (√‘(𝑥↑2)) → 𝑥 ∈ ℝ))
190187renegcld 11055 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → -(√‘(𝑥↑2)) ∈ ℝ)
191 eleq1 2897 . . . . . . . . . . . . . . . . 17 (𝑥 = -(√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔ -(√‘(𝑥↑2)) ∈ ℝ))
192190, 191syl5ibrcom 248 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = -(√‘(𝑥↑2)) → 𝑥 ∈ ℝ))
193 eqid 2818 . . . . . . . . . . . . . . . . . 18 (𝑥↑2) = (𝑥↑2)
194 eqsqrtor 14714 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))))
19517, 194mpdan 683 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))))
196193, 195mpbii 234 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))
197196adantr 481 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))
198189, 192, 197mpjaod 854 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 𝑥 ∈ ℝ)
199198stoic1a 1764 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
20012, 199sylan 580 . . . . . . . . . . . . 13 ((𝑥𝐷 ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
201162, 200pm2.61dan 809 . . . . . . . . . . . 12 (𝑥𝐷 → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
202111, 201eldifd 3944 . . . . . . . . . . 11 (𝑥𝐷 → (1 − (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0)))
203202adantl 482 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝐷) → (1 − (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0)))
204 2cnd 11703 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → 2 ∈ ℂ)
205 id 22 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → 𝑥 ∈ ℂ)
206204, 205mulcld 10649 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
207206negcld 10972 . . . . . . . . . . . 12 (𝑥 ∈ ℂ → -(2 · 𝑥) ∈ ℂ)
208207adantl 482 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → -(2 · 𝑥) ∈ ℂ)
20912, 208sylan2 592 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝐷) → -(2 · 𝑥) ∈ ℂ)
21059sqrtcld 14785 . . . . . . . . . . 11 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → (√‘𝑦) ∈ ℂ)
211210adantl 482 . . . . . . . . . 10 ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (√‘𝑦) ∈ ℂ)
212 ovexd 7180 . . . . . . . . . 10 ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / (2 · (√‘𝑦))) ∈ V)
21319adantl 482 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ)
21436a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℂ) → 0 ∈ ℝ)
215 1cnd 10624 . . . . . . . . . . . . . 14 (⊤ → 1 ∈ ℂ)
21611, 215dvmptc 24482 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 1)) = (𝑥 ∈ ℂ ↦ 0))
21717adantl 482 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℂ) → (𝑥↑2) ∈ ℂ)
218 2cn 11700 . . . . . . . . . . . . . . 15 2 ∈ ℂ
219 mulcl 10609 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
220218, 219mpan 686 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
221220adantl 482 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
222 2nn 11698 . . . . . . . . . . . . . . . 16 2 ∈ ℕ
223 dvexp 24477 . . . . . . . . . . . . . . . 16 (2 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))))
224222, 223ax-mp 5 . . . . . . . . . . . . . . 15 (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1))))
225 2m1e1 11751 . . . . . . . . . . . . . . . . . . 19 (2 − 1) = 1
226225oveq2i 7156 . . . . . . . . . . . . . . . . . 18 (𝑥↑(2 − 1)) = (𝑥↑1)
227 exp1 13423 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → (𝑥↑1) = 𝑥)
228226, 227syl5eq 2865 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → (𝑥↑(2 − 1)) = 𝑥)
229228oveq2d 7161 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → (2 · (𝑥↑(2 − 1))) = (2 · 𝑥))
230229mpteq2ia 5148 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))
231224, 230eqtri 2841 . . . . . . . . . . . . . 14 (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))
232231a1i 11 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥)))
23311, 79, 214, 216, 217, 221, 232dvmptsub 24491 . . . . . . . . . . . 12 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ (0 − (2 · 𝑥))))
234 df-neg 10861 . . . . . . . . . . . . 13 -(2 · 𝑥) = (0 − (2 · 𝑥))
235234mpteq2i 5149 . . . . . . . . . . . 12 (𝑥 ∈ ℂ ↦ -(2 · 𝑥)) = (𝑥 ∈ ℂ ↦ (0 − (2 · 𝑥)))
236233, 235syl6eqr 2871 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ -(2 · 𝑥)))
23711, 213, 208, 236, 81, 84, 82, 103dvmptres 24487 . . . . . . . . . 10 (⊤ → (ℂ D (𝑥𝐷 ↦ (1 − (𝑥↑2)))) = (𝑥𝐷 ↦ -(2 · 𝑥)))
238 eqid 2818 . . . . . . . . . . . 12 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
239238dvcnsqrt 25252 . . . . . . . . . . 11 (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / (2 · (√‘𝑦))))
240239a1i 11 . . . . . . . . . 10 (⊤ → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / (2 · (√‘𝑦)))))
241 fveq2 6663 . . . . . . . . . 10 (𝑦 = (1 − (𝑥↑2)) → (√‘𝑦) = (√‘(1 − (𝑥↑2))))
242241oveq2d 7161 . . . . . . . . . . 11 (𝑦 = (1 − (𝑥↑2)) → (2 · (√‘𝑦)) = (2 · (√‘(1 − (𝑥↑2)))))
243242oveq2d 7161 . . . . . . . . . 10 (𝑦 = (1 − (𝑥↑2)) → (1 / (2 · (√‘𝑦))) = (1 / (2 · (√‘(1 − (𝑥↑2))))))
24411, 11, 203, 209, 211, 212, 237, 240, 241, 243dvmptco 24496 . . . . . . . . 9 (⊤ → (ℂ D (𝑥𝐷 ↦ (√‘(1 − (𝑥↑2))))) = (𝑥𝐷 ↦ ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))))
245 mulneg2 11065 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · -𝑥) = -(2 · 𝑥))
246218, 12, 245sylancr 587 . . . . . . . . . . . 12 (𝑥𝐷 → (2 · -𝑥) = -(2 · 𝑥))
247246oveq1d 7160 . . . . . . . . . . 11 (𝑥𝐷 → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-(2 · 𝑥) / (2 · (√‘(1 − (𝑥↑2))))))
24812negcld 10972 . . . . . . . . . . . 12 (𝑥𝐷 → -𝑥 ∈ ℂ)
249 eldifn 4101 . . . . . . . . . . . . . . 15 (𝑥 ∈ (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) → ¬ 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
250249, 3eleq2s 2928 . . . . . . . . . . . . . 14 (𝑥𝐷 → ¬ 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
251 id 22 . . . . . . . . . . . . . . . . . 18 (𝑥 = -1 → 𝑥 = -1)
252 mnflt 12506 . . . . . . . . . . . . . . . . . . . 20 (-1 ∈ ℝ → -∞ < -1)
25386, 252ax-mp 5 . . . . . . . . . . . . . . . . . . 19 -∞ < -1
254 ubioc1 12778 . . . . . . . . . . . . . . . . . . 19 ((-∞ ∈ ℝ* ∧ -1 ∈ ℝ* ∧ -∞ < -1) → -1 ∈ (-∞(,]-1))
25551, 132, 253, 254mp3an 1452 . . . . . . . . . . . . . . . . . 18 -1 ∈ (-∞(,]-1)
256251, 255syl6eqel 2918 . . . . . . . . . . . . . . . . 17 (𝑥 = -1 → 𝑥 ∈ (-∞(,]-1))
257 id 22 . . . . . . . . . . . . . . . . . 18 (𝑥 = 1 → 𝑥 = 1)
258 ltpnf 12503 . . . . . . . . . . . . . . . . . . . 20 (1 ∈ ℝ → 1 < +∞)
25989, 258ax-mp 5 . . . . . . . . . . . . . . . . . . 19 1 < +∞
260 lbico1 12779 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 1 < +∞) → 1 ∈ (1[,)+∞))
261133, 121, 259, 260mp3an 1452 . . . . . . . . . . . . . . . . . 18 1 ∈ (1[,)+∞)
262257, 261syl6eqel 2918 . . . . . . . . . . . . . . . . 17 (𝑥 = 1 → 𝑥 ∈ (1[,)+∞))
263256, 262orim12i 902 . . . . . . . . . . . . . . . 16 ((𝑥 = -1 ∨ 𝑥 = 1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
264263orcoms 868 . . . . . . . . . . . . . . 15 ((𝑥 = 1 ∨ 𝑥 = -1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
265 elun 4122 . . . . . . . . . . . . . . 15 (𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)) ↔ (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
266264, 265sylibr 235 . . . . . . . . . . . . . 14 ((𝑥 = 1 ∨ 𝑥 = -1) → 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
267250, 266nsyl 142 . . . . . . . . . . . . 13 (𝑥𝐷 → ¬ (𝑥 = 1 ∨ 𝑥 = -1))
268 1cnd 10624 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 ∈ ℂ)
26917adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) ∈ ℂ)
27019adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) ∈ ℂ)
271 simpr 485 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (√‘(1 − (𝑥↑2))) = 0)
272270, 271sqr00d 14789 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) = 0)
273268, 269, 272subeq0d 10993 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 = (𝑥↑2))
274146, 273syl5req 2866 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) = (1↑2))
275274ex 413 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥↑2) = (1↑2)))
276 sqeqor 13566 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
27716, 276mpan2 687 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
278275, 277sylibd 240 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥 = 1 ∨ 𝑥 = -1)))
279278necon3bd 3027 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → (¬ (𝑥 = 1 ∨ 𝑥 = -1) → (√‘(1 − (𝑥↑2))) ≠ 0))
28012, 267, 279sylc 65 . . . . . . . . . . . 12 (𝑥𝐷 → (√‘(1 − (𝑥↑2))) ≠ 0)
281 2cnne0 11835 . . . . . . . . . . . . 13 (2 ∈ ℂ ∧ 2 ≠ 0)
282 divcan5 11330 . . . . . . . . . . . . 13 ((-𝑥 ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
283281, 282mp3an3 1441 . . . . . . . . . . . 12 ((-𝑥 ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
284248, 112, 280, 283syl12anc 832 . . . . . . . . . . 11 (𝑥𝐷 → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
285218, 12, 219sylancr 587 . . . . . . . . . . . . 13 (𝑥𝐷 → (2 · 𝑥) ∈ ℂ)
286285negcld 10972 . . . . . . . . . . . 12 (𝑥𝐷 → -(2 · 𝑥) ∈ ℂ)
287 mulcl 10609 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (2 · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
288218, 112, 287sylancr 587 . . . . . . . . . . . 12 (𝑥𝐷 → (2 · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
289 mulne0 11270 . . . . . . . . . . . . . 14 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
290281, 289mpan 686 . . . . . . . . . . . . 13 (((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
291112, 280, 290syl2anc 584 . . . . . . . . . . . 12 (𝑥𝐷 → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
292286, 288, 291divrec2d 11408 . . . . . . . . . . 11 (𝑥𝐷 → (-(2 · 𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥)))
293247, 284, 2923eqtr3rd 2862 . . . . . . . . . 10 (𝑥𝐷 → ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥)) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
294293mpteq2ia 5148 . . . . . . . . 9 (𝑥𝐷 ↦ ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))) = (𝑥𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2)))))
295244, 294syl6eq 2869 . . . . . . . 8 (⊤ → (ℂ D (𝑥𝐷 ↦ (√‘(1 − (𝑥↑2))))) = (𝑥𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2))))))
29611, 74, 75, 109, 113, 114, 295dvmptadd 24484 . . . . . . 7 (⊤ → (ℂ D (𝑥𝐷 ↦ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))))
297 mulcl 10609 . . . . . . . . . . . 12 ((i ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
29813, 20, 297sylancr 587 . . . . . . . . . . 11 (𝑥 ∈ ℂ → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
29912, 298syl 17 . . . . . . . . . 10 (𝑥𝐷 → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
300299, 248, 112, 280divdird 11442 . . . . . . . . 9 (𝑥𝐷 → (((i · (√‘(1 − (𝑥↑2)))) + -𝑥) / (√‘(1 − (𝑥↑2)))) = (((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))))
301 ixi 11257 . . . . . . . . . . . . . . . 16 (i · i) = -1
302301eqcomi 2827 . . . . . . . . . . . . . . 15 -1 = (i · i)
303302oveq1i 7155 . . . . . . . . . . . . . 14 (-1 · 𝑥) = ((i · i) · 𝑥)
304 mulm1 11069 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → (-1 · 𝑥) = -𝑥)
305 mulass 10613 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ i ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((i · i) · 𝑥) = (i · (i · 𝑥)))
30613, 13, 305mp3an12 1442 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → ((i · i) · 𝑥) = (i · (i · 𝑥)))
307303, 304, 3063eqtr3a 2877 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → -𝑥 = (i · (i · 𝑥)))
308307oveq1d 7160 . . . . . . . . . . . 12 (𝑥 ∈ ℂ → (-𝑥 + (i · (√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i · (√‘(1 − (𝑥↑2))))))
309 negcl 10874 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → -𝑥 ∈ ℂ)
310298, 309addcomd 10830 . . . . . . . . . . . 12 (𝑥 ∈ ℂ → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (-𝑥 + (i · (√‘(1 − (𝑥↑2))))))
31113a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → i ∈ ℂ)
312311, 15, 20adddid 10653 . . . . . . . . . . . 12 (𝑥 ∈ ℂ → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i · (√‘(1 − (𝑥↑2))))))
313308, 310, 3123eqtr4d 2863 . . . . . . . . . . 11 (𝑥 ∈ ℂ → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
31412, 313syl 17 . . . . . . . . . 10 (𝑥𝐷 → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
315314oveq1d 7160 . . . . . . . . 9 (𝑥𝐷 → (((i · (√‘(1 − (𝑥↑2)))) + -𝑥) / (√‘(1 − (𝑥↑2)))) = ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
31672, 112, 280divcan4d 11410 . . . . . . . . . 10 (𝑥𝐷 → ((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) = i)
317316oveq1d 7160 . . . . . . . . 9 (𝑥𝐷 → (((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))) = (i + (-𝑥 / (√‘(1 − (𝑥↑2))))))
318300, 315, 3173eqtr3rd 2862 . . . . . . . 8 (𝑥𝐷 → (i + (-𝑥 / (√‘(1 − (𝑥↑2))))) = ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
319318mpteq2ia 5148 . . . . . . 7 (𝑥𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
320296, 319syl6eq 2869 . . . . . 6 (⊤ → (ℂ D (𝑥𝐷 ↦ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))))
321238dvlog 25161 . . . . . . 7 (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦))
322 logf1o 25075 . . . . . . . . . 10 log:(ℂ ∖ {0})–1-1-onto→ran log
323 f1of 6608 . . . . . . . . . 10 (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
324322, 323mp1i 13 . . . . . . . . 9 (⊤ → log:(ℂ ∖ {0})⟶ran log)
325 snssi 4733 . . . . . . . . . . 11 (0 ∈ (-∞(,]0) → {0} ⊆ (-∞(,]0))
32664, 325ax-mp 5 . . . . . . . . . 10 {0} ⊆ (-∞(,]0)
327 sscon 4112 . . . . . . . . . 10 ({0} ⊆ (-∞(,]0) → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}))
328326, 327mp1i 13 . . . . . . . . 9 (⊤ → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}))
329324, 328feqresmpt 6727 . . . . . . . 8 (⊤ → (log ↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦)))
330329oveq2d 7161 . . . . . . 7 (⊤ → (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))))
331321, 330syl5reqr 2868 . . . . . 6 (⊤ → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦)))
332 fveq2 6663 . . . . . 6 (𝑦 = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) → (log‘𝑦) = (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
333 oveq2 7153 . . . . . 6 (𝑦 = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) → (1 / 𝑦) = (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
33411, 11, 57, 58, 70, 71, 320, 331, 332, 333dvmptco 24496 . . . . 5 (⊤ → (ℂ D (𝑥𝐷 ↦ (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) = (𝑥𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))))
33522, 24reccld 11397 . . . . . . . 8 (𝑥𝐷 → (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
336 mulcl 10609 . . . . . . . . . 10 ((i ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ) → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
33713, 21, 336sylancr 587 . . . . . . . . 9 (𝑥 ∈ ℂ → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
33812, 337syl 17 . . . . . . . 8 (𝑥𝐷 → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
339335, 338, 112, 280divassd 11439 . . . . . . 7 (𝑥𝐷 → (((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) / (√‘(1 − (𝑥↑2)))) = ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))))
340338, 22, 24divrec2d 11408 . . . . . . . . 9 (𝑥𝐷 → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
34172, 22, 24divcan4d 11410 . . . . . . . . 9 (𝑥𝐷 → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = i)
342340, 341eqtr3d 2855 . . . . . . . 8 (𝑥𝐷 → ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = i)
343342oveq1d 7160 . . . . . . 7 (𝑥𝐷 → (((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) / (√‘(1 − (𝑥↑2)))) = (i / (√‘(1 − (𝑥↑2)))))
344339, 343eqtr3d 2855 . . . . . 6 (𝑥𝐷 → ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))) = (i / (√‘(1 − (𝑥↑2)))))
345344mpteq2ia 5148 . . . . 5 (𝑥𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ (i / (√‘(1 − (𝑥↑2)))))
346334, 345syl6eq 2869 . . . 4 (⊤ → (ℂ D (𝑥𝐷 ↦ (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) = (𝑥𝐷 ↦ (i / (√‘(1 − (𝑥↑2))))))
347 negicn 10875 . . . . 5 -i ∈ ℂ
348347a1i 11 . . . 4 (⊤ → -i ∈ ℂ)
34911, 26, 27, 346, 348dvmptcmul 24488 . . 3 (⊤ → (ℂ D (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))) = (𝑥𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2)))))))
350349mptru 1535 . 2 (ℂ D (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))) = (𝑥𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2))))))
35113, 13mulneg1i 11074 . . . . . 6 (-i · i) = -(i · i)
352301negeqi 10867 . . . . . 6 -(i · i) = --1
353 negneg1e1 11743 . . . . . 6 --1 = 1
354351, 352, 3533eqtri 2845 . . . . 5 (-i · i) = 1
355354oveq1i 7155 . . . 4 ((-i · i) / (√‘(1 − (𝑥↑2)))) = (1 / (√‘(1 − (𝑥↑2))))
356 divass 11304 . . . . . 6 ((-i ∈ ℂ ∧ i ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
357347, 13, 356mp3an12 1442 . . . . 5 (((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
358112, 280, 357syl2anc 584 . . . 4 (𝑥𝐷 → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
359355, 358syl5reqr 2868 . . 3 (𝑥𝐷 → (-i · (i / (√‘(1 − (𝑥↑2))))) = (1 / (√‘(1 − (𝑥↑2)))))
360359mpteq2ia 5148 . 2 (𝑥𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))
3619, 350, 3603eqtri 2845 1 (ℂ D (arcsin ↾ 𝐷)) = (𝑥𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841  w3o 1078  w3a 1079   = wceq 1528  wtru 1529  wcel 2105  wne 3013  Vcvv 3492  cdif 3930  cun 3931  cin 3932  wss 3933  c0 4288  {csn 4557  {cpr 4559   class class class wbr 5057  cmpt 5137  ran crn 5549  cres 5550  wf 6344  1-1-ontowf1o 6347  cfv 6348  (class class class)co 7145  cc 10523  cr 10524  0cc0 10525  1c1 10526  ici 10527   + caddc 10528   · cmul 10530  +∞cpnf 10660  -∞cmnf 10661  *cxr 10662   < clt 10663  cle 10664  cmin 10858  -cneg 10859   / cdiv 11285  cn 11626  2c2 11680  +crp 12377  (,)cioo 12726  (,]cioc 12727  [,)cico 12728  cexp 13417  cre 14444  csqrt 14580  abscabs 14581  t crest 16682  TopOpenctopn 16683  topGenctg 16699  fldccnfld 20473  Clsdccld 21552   D cdv 24388  logclog 25065  arcsincasin 25367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-inf2 9092  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603  ax-addf 10604  ax-mulf 10605
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-om 7570  df-1st 7678  df-2nd 7679  df-supp 7820  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-oadd 8095  df-er 8278  df-map 8397  df-pm 8398  df-ixp 8450  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-card 9356  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ioo 12730  df-ioc 12731  df-ico 12732  df-icc 12733  df-fz 12881  df-fzo 13022  df-fl 13150  df-mod 13226  df-seq 13358  df-exp 13418  df-fac 13622  df-bc 13651  df-hash 13679  df-shft 14414  df-cj 14446  df-re 14447  df-im 14448  df-sqrt 14582  df-abs 14583  df-limsup 14816  df-clim 14833  df-rlim 14834  df-sum 15031  df-ef 15409  df-sin 15411  df-cos 15412  df-tan 15413  df-pi 15414  df-struct 16473  df-ndx 16474  df-slot 16475  df-base 16477  df-sets 16478  df-ress 16479  df-plusg 16566  df-mulr 16567  df-starv 16568  df-sca 16569  df-vsca 16570  df-ip 16571  df-tset 16572  df-ple 16573  df-ds 16575  df-unif 16576  df-hom 16577  df-cco 16578  df-rest 16684  df-topn 16685  df-0g 16703  df-gsum 16704  df-topgen 16705  df-pt 16706  df-prds 16709  df-xrs 16763  df-qtop 16768  df-imas 16769  df-xps 16771  df-mre 16845  df-mrc 16846  df-acs 16848  df-mgm 17840  df-sgrp 17889  df-mnd 17900  df-submnd 17945  df-mulg 18163  df-cntz 18385  df-cmn 18837  df-psmet 20465  df-xmet 20466  df-met 20467  df-bl 20468  df-mopn 20469  df-fbas 20470  df-fg 20471  df-cnfld 20474  df-top 21430  df-topon 21447  df-topsp 21469  df-bases 21482  df-cld 21555  df-ntr 21556  df-cls 21557  df-nei 21634  df-lp 21672  df-perf 21673  df-cn 21763  df-cnp 21764  df-haus 21851  df-cmp 21923  df-tx 22098  df-hmeo 22291  df-fil 22382  df-fm 22474  df-flim 22475  df-flf 22476  df-xms 22857  df-ms 22858  df-tms 22859  df-cncf 23413  df-limc 24391  df-dv 24392  df-log 25067  df-cxp 25068  df-asin 25370
This theorem is referenced by:  dvacos  34860  dvreasin  34861
  Copyright terms: Public domain W3C validator