Proof of Theorem cphsqrtcl2
Step | Hyp | Ref
| Expression |
1 | | sqrt0 14462 |
. . . . 5
⊢
(√‘0) = 0 |
2 | | fveq2 6499 |
. . . . 5
⊢ (𝐴 = 0 → (√‘𝐴) =
(√‘0)) |
3 | | id 22 |
. . . . 5
⊢ (𝐴 = 0 → 𝐴 = 0) |
4 | 1, 2, 3 | 3eqtr4a 2840 |
. . . 4
⊢ (𝐴 = 0 → (√‘𝐴) = 𝐴) |
5 | 4 | adantl 474 |
. . 3
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 = 0) →
(√‘𝐴) = 𝐴) |
6 | | simpl2 1172 |
. . 3
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 = 0) → 𝐴 ∈ 𝐾) |
7 | 5, 6 | eqeltrd 2866 |
. 2
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 = 0) →
(√‘𝐴) ∈
𝐾) |
8 | | simpl1 1171 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 𝑊 ∈
ℂPreHil) |
9 | | cphsca.f |
. . . . . . . 8
⊢ 𝐹 = (Scalar‘𝑊) |
10 | | cphsca.k |
. . . . . . . 8
⊢ 𝐾 = (Base‘𝐹) |
11 | 9, 10 | cphsubrg 23487 |
. . . . . . 7
⊢ (𝑊 ∈ ℂPreHil →
𝐾 ∈
(SubRing‘ℂfld)) |
12 | 8, 11 | syl 17 |
. . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 𝐾 ∈
(SubRing‘ℂfld)) |
13 | | cnfldbas 20251 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
14 | 13 | subrgss 19259 |
. . . . . 6
⊢ (𝐾 ∈
(SubRing‘ℂfld) → 𝐾 ⊆ ℂ) |
15 | 12, 14 | syl 17 |
. . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 𝐾 ⊆
ℂ) |
16 | | simpl2 1172 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 𝐴 ∈ 𝐾) |
17 | 9, 10 | cphabscl 23492 |
. . . . . . . 8
⊢ ((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾) → (abs‘𝐴) ∈ 𝐾) |
18 | 8, 16, 17 | syl2anc 576 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ 𝐾) |
19 | 15, 16 | sseldd 3859 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 𝐴 ∈
ℂ) |
20 | 19 | abscld 14657 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ) |
21 | 19 | absge0d 14665 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 0 ≤
(abs‘𝐴)) |
22 | 9, 10 | cphsqrtcl 23491 |
. . . . . . 7
⊢ ((𝑊 ∈ ℂPreHil ∧
((abs‘𝐴) ∈ 𝐾 ∧ (abs‘𝐴) ∈ ℝ ∧ 0 ≤
(abs‘𝐴))) →
(√‘(abs‘𝐴)) ∈ 𝐾) |
23 | 8, 18, 20, 21, 22 | syl13anc 1352 |
. . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(√‘(abs‘𝐴)) ∈ 𝐾) |
24 | | cnfldadd 20252 |
. . . . . . . . 9
⊢ + =
(+g‘ℂfld) |
25 | 24 | subrgacl 19269 |
. . . . . . . 8
⊢ ((𝐾 ∈
(SubRing‘ℂfld) ∧ (abs‘𝐴) ∈ 𝐾 ∧ 𝐴 ∈ 𝐾) → ((abs‘𝐴) + 𝐴) ∈ 𝐾) |
26 | 12, 18, 16, 25 | syl3anc 1351 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((abs‘𝐴) + 𝐴) ∈ 𝐾) |
27 | 9, 10 | cphabscl 23492 |
. . . . . . . 8
⊢ ((𝑊 ∈ ℂPreHil ∧
((abs‘𝐴) + 𝐴) ∈ 𝐾) → (abs‘((abs‘𝐴) + 𝐴)) ∈ 𝐾) |
28 | 8, 26, 27 | syl2anc 576 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(abs‘((abs‘𝐴) +
𝐴)) ∈ 𝐾) |
29 | 15, 26 | sseldd 3859 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((abs‘𝐴) + 𝐴) ∈
ℂ) |
30 | | simpl3 1173 |
. . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → ¬ -𝐴 ∈
ℝ+) |
31 | 20 | recnd 10468 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℂ) |
32 | 31, 19 | subnegd 10805 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((abs‘𝐴) −
-𝐴) = ((abs‘𝐴) + 𝐴)) |
33 | 32 | eqeq1d 2780 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) −
-𝐴) = 0 ↔
((abs‘𝐴) + 𝐴) = 0)) |
34 | 19 | negcld 10785 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → -𝐴 ∈
ℂ) |
35 | 31, 34 | subeq0ad 10808 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) −
-𝐴) = 0 ↔
(abs‘𝐴) = -𝐴)) |
36 | 33, 35 | bitr3d 273 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) + 𝐴) = 0 ↔ (abs‘𝐴) = -𝐴)) |
37 | | absrpcl 14509 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ+) |
38 | 19, 37 | sylancom 579 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ+) |
39 | | eleq1 2853 |
. . . . . . . . . . . 12
⊢
((abs‘𝐴) =
-𝐴 → ((abs‘𝐴) ∈ ℝ+
↔ -𝐴 ∈
ℝ+)) |
40 | 38, 39 | syl5ibcom 237 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((abs‘𝐴) = -𝐴 → -𝐴 ∈
ℝ+)) |
41 | 36, 40 | sylbid 232 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) + 𝐴) = 0 → -𝐴 ∈
ℝ+)) |
42 | 41 | necon3bd 2981 |
. . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → (¬ -𝐴 ∈ ℝ+
→ ((abs‘𝐴) +
𝐴) ≠
0)) |
43 | 30, 42 | mpd 15 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((abs‘𝐴) + 𝐴) ≠ 0) |
44 | 29, 43 | absne0d 14668 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(abs‘((abs‘𝐴) +
𝐴)) ≠
0) |
45 | 9, 10 | cphdivcl 23489 |
. . . . . . 7
⊢ ((𝑊 ∈ ℂPreHil ∧
(((abs‘𝐴) + 𝐴) ∈ 𝐾 ∧ (abs‘((abs‘𝐴) + 𝐴)) ∈ 𝐾 ∧ (abs‘((abs‘𝐴) + 𝐴)) ≠ 0)) → (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) ∈ 𝐾) |
46 | 8, 26, 28, 44, 45 | syl13anc 1352 |
. . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) ∈ 𝐾) |
47 | | cnfldmul 20253 |
. . . . . . 7
⊢ ·
= (.r‘ℂfld) |
48 | 47 | subrgmcl 19270 |
. . . . . 6
⊢ ((𝐾 ∈
(SubRing‘ℂfld) ∧ (√‘(abs‘𝐴)) ∈ 𝐾 ∧ (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) ∈ 𝐾) → ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ 𝐾) |
49 | 12, 23, 46, 48 | syl3anc 1351 |
. . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ 𝐾) |
50 | 15, 49 | sseldd 3859 |
. . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ ℂ) |
51 | | eqid 2778 |
. . . . . . 7
⊢
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) = ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) |
52 | 51 | sqreulem 14580 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
((abs‘𝐴) + 𝐴) ≠ 0) →
((((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))↑2) = 𝐴 ∧ 0 ≤
(ℜ‘((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∧ (i ·
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∉
ℝ+)) |
53 | 19, 43, 52 | syl2anc 576 |
. . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))↑2) = 𝐴 ∧ 0 ≤
(ℜ‘((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∧ (i ·
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∉
ℝ+)) |
54 | 53 | simp1d 1122 |
. . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))↑2) = 𝐴) |
55 | 53 | simp2d 1123 |
. . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 0 ≤
(ℜ‘((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))))) |
56 | 53 | simp3d 1124 |
. . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → (i ·
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∉
ℝ+) |
57 | | df-nel 3074 |
. . . . 5
⊢ ((i
· ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∉ ℝ+ ↔
¬ (i · ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∈
ℝ+) |
58 | 56, 57 | sylib 210 |
. . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → ¬ (i
· ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∈
ℝ+) |
59 | 50, 19, 54, 55, 58 | eqsqrtd 14588 |
. . 3
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) = (√‘𝐴)) |
60 | 59, 49 | eqeltrrd 2867 |
. 2
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(√‘𝐴) ∈
𝐾) |
61 | 7, 60 | pm2.61dane 3055 |
1
⊢ ((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) →
(√‘𝐴) ∈
𝐾) |