Proof of Theorem cphsqrtcl2
Step | Hyp | Ref
| Expression |
1 | | sqrt0 14595 |
. . . . 5
⊢
(√‘0) = 0 |
2 | | fveq2 6664 |
. . . . 5
⊢ (𝐴 = 0 → (√‘𝐴) =
(√‘0)) |
3 | | id 22 |
. . . . 5
⊢ (𝐴 = 0 → 𝐴 = 0) |
4 | 1, 2, 3 | 3eqtr4a 2882 |
. . . 4
⊢ (𝐴 = 0 → (√‘𝐴) = 𝐴) |
5 | 4 | adantl 484 |
. . 3
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 = 0) →
(√‘𝐴) = 𝐴) |
6 | | simpl2 1188 |
. . 3
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 = 0) → 𝐴 ∈ 𝐾) |
7 | 5, 6 | eqeltrd 2913 |
. 2
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 = 0) →
(√‘𝐴) ∈
𝐾) |
8 | | simpl1 1187 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 𝑊 ∈
ℂPreHil) |
9 | | cphsca.f |
. . . . . . . 8
⊢ 𝐹 = (Scalar‘𝑊) |
10 | | cphsca.k |
. . . . . . . 8
⊢ 𝐾 = (Base‘𝐹) |
11 | 9, 10 | cphsubrg 23778 |
. . . . . . 7
⊢ (𝑊 ∈ ℂPreHil →
𝐾 ∈
(SubRing‘ℂfld)) |
12 | 8, 11 | syl 17 |
. . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 𝐾 ∈
(SubRing‘ℂfld)) |
13 | | cnfldbas 20543 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
14 | 13 | subrgss 19530 |
. . . . . 6
⊢ (𝐾 ∈
(SubRing‘ℂfld) → 𝐾 ⊆ ℂ) |
15 | 12, 14 | syl 17 |
. . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 𝐾 ⊆
ℂ) |
16 | | simpl2 1188 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 𝐴 ∈ 𝐾) |
17 | 9, 10 | cphabscl 23783 |
. . . . . . . 8
⊢ ((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾) → (abs‘𝐴) ∈ 𝐾) |
18 | 8, 16, 17 | syl2anc 586 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ 𝐾) |
19 | 15, 16 | sseldd 3967 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 𝐴 ∈
ℂ) |
20 | 19 | abscld 14790 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ) |
21 | 19 | absge0d 14798 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 0 ≤
(abs‘𝐴)) |
22 | 9, 10 | cphsqrtcl 23782 |
. . . . . . 7
⊢ ((𝑊 ∈ ℂPreHil ∧
((abs‘𝐴) ∈ 𝐾 ∧ (abs‘𝐴) ∈ ℝ ∧ 0 ≤
(abs‘𝐴))) →
(√‘(abs‘𝐴)) ∈ 𝐾) |
23 | 8, 18, 20, 21, 22 | syl13anc 1368 |
. . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(√‘(abs‘𝐴)) ∈ 𝐾) |
24 | | cnfldadd 20544 |
. . . . . . . . 9
⊢ + =
(+g‘ℂfld) |
25 | 24 | subrgacl 19540 |
. . . . . . . 8
⊢ ((𝐾 ∈
(SubRing‘ℂfld) ∧ (abs‘𝐴) ∈ 𝐾 ∧ 𝐴 ∈ 𝐾) → ((abs‘𝐴) + 𝐴) ∈ 𝐾) |
26 | 12, 18, 16, 25 | syl3anc 1367 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((abs‘𝐴) + 𝐴) ∈ 𝐾) |
27 | 9, 10 | cphabscl 23783 |
. . . . . . . 8
⊢ ((𝑊 ∈ ℂPreHil ∧
((abs‘𝐴) + 𝐴) ∈ 𝐾) → (abs‘((abs‘𝐴) + 𝐴)) ∈ 𝐾) |
28 | 8, 26, 27 | syl2anc 586 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(abs‘((abs‘𝐴) +
𝐴)) ∈ 𝐾) |
29 | 15, 26 | sseldd 3967 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((abs‘𝐴) + 𝐴) ∈
ℂ) |
30 | | simpl3 1189 |
. . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → ¬ -𝐴 ∈
ℝ+) |
31 | 20 | recnd 10663 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℂ) |
32 | 31, 19 | subnegd 10998 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((abs‘𝐴) −
-𝐴) = ((abs‘𝐴) + 𝐴)) |
33 | 32 | eqeq1d 2823 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) −
-𝐴) = 0 ↔
((abs‘𝐴) + 𝐴) = 0)) |
34 | 19 | negcld 10978 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → -𝐴 ∈
ℂ) |
35 | 31, 34 | subeq0ad 11001 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) −
-𝐴) = 0 ↔
(abs‘𝐴) = -𝐴)) |
36 | 33, 35 | bitr3d 283 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) + 𝐴) = 0 ↔ (abs‘𝐴) = -𝐴)) |
37 | | absrpcl 14642 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ+) |
38 | 19, 37 | sylancom 590 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ+) |
39 | | eleq1 2900 |
. . . . . . . . . . . 12
⊢
((abs‘𝐴) =
-𝐴 → ((abs‘𝐴) ∈ ℝ+
↔ -𝐴 ∈
ℝ+)) |
40 | 38, 39 | syl5ibcom 247 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((abs‘𝐴) = -𝐴 → -𝐴 ∈
ℝ+)) |
41 | 36, 40 | sylbid 242 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) + 𝐴) = 0 → -𝐴 ∈
ℝ+)) |
42 | 41 | necon3bd 3030 |
. . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → (¬ -𝐴 ∈ ℝ+
→ ((abs‘𝐴) +
𝐴) ≠
0)) |
43 | 30, 42 | mpd 15 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((abs‘𝐴) + 𝐴) ≠ 0) |
44 | 29, 43 | absne0d 14801 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(abs‘((abs‘𝐴) +
𝐴)) ≠
0) |
45 | 9, 10 | cphdivcl 23780 |
. . . . . . 7
⊢ ((𝑊 ∈ ℂPreHil ∧
(((abs‘𝐴) + 𝐴) ∈ 𝐾 ∧ (abs‘((abs‘𝐴) + 𝐴)) ∈ 𝐾 ∧ (abs‘((abs‘𝐴) + 𝐴)) ≠ 0)) → (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) ∈ 𝐾) |
46 | 8, 26, 28, 44, 45 | syl13anc 1368 |
. . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) ∈ 𝐾) |
47 | | cnfldmul 20545 |
. . . . . . 7
⊢ ·
= (.r‘ℂfld) |
48 | 47 | subrgmcl 19541 |
. . . . . 6
⊢ ((𝐾 ∈
(SubRing‘ℂfld) ∧ (√‘(abs‘𝐴)) ∈ 𝐾 ∧ (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) ∈ 𝐾) → ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ 𝐾) |
49 | 12, 23, 46, 48 | syl3anc 1367 |
. . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ 𝐾) |
50 | 15, 49 | sseldd 3967 |
. . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ ℂ) |
51 | | eqid 2821 |
. . . . . . 7
⊢
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) = ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) |
52 | 51 | sqreulem 14713 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
((abs‘𝐴) + 𝐴) ≠ 0) →
((((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))↑2) = 𝐴 ∧ 0 ≤
(ℜ‘((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∧ (i ·
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∉
ℝ+)) |
53 | 19, 43, 52 | syl2anc 586 |
. . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))↑2) = 𝐴 ∧ 0 ≤
(ℜ‘((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∧ (i ·
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∉
ℝ+)) |
54 | 53 | simp1d 1138 |
. . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))↑2) = 𝐴) |
55 | 53 | simp2d 1139 |
. . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 0 ≤
(ℜ‘((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))))) |
56 | 53 | simp3d 1140 |
. . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → (i ·
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∉
ℝ+) |
57 | | df-nel 3124 |
. . . . 5
⊢ ((i
· ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∉ ℝ+ ↔
¬ (i · ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∈
ℝ+) |
58 | 56, 57 | sylib 220 |
. . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → ¬ (i
· ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∈
ℝ+) |
59 | 50, 19, 54, 55, 58 | eqsqrtd 14721 |
. . 3
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) = (√‘𝐴)) |
60 | 59, 49 | eqeltrrd 2914 |
. 2
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(√‘𝐴) ∈
𝐾) |
61 | 7, 60 | pm2.61dane 3104 |
1
⊢ ((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) →
(√‘𝐴) ∈
𝐾) |