Proof of Theorem cphsqrtcl2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sqrt0 15281 | . . . . 5
⊢
(√‘0) = 0 | 
| 2 |  | fveq2 6905 | . . . . 5
⊢ (𝐴 = 0 → (√‘𝐴) =
(√‘0)) | 
| 3 |  | id 22 | . . . . 5
⊢ (𝐴 = 0 → 𝐴 = 0) | 
| 4 | 1, 2, 3 | 3eqtr4a 2802 | . . . 4
⊢ (𝐴 = 0 → (√‘𝐴) = 𝐴) | 
| 5 | 4 | adantl 481 | . . 3
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 = 0) →
(√‘𝐴) = 𝐴) | 
| 6 |  | simpl2 1192 | . . 3
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 = 0) → 𝐴 ∈ 𝐾) | 
| 7 | 5, 6 | eqeltrd 2840 | . 2
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 = 0) →
(√‘𝐴) ∈
𝐾) | 
| 8 |  | simpl1 1191 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 𝑊 ∈
ℂPreHil) | 
| 9 |  | cphsca.f | . . . . . . . 8
⊢ 𝐹 = (Scalar‘𝑊) | 
| 10 |  | cphsca.k | . . . . . . . 8
⊢ 𝐾 = (Base‘𝐹) | 
| 11 | 9, 10 | cphsubrg 25215 | . . . . . . 7
⊢ (𝑊 ∈ ℂPreHil →
𝐾 ∈
(SubRing‘ℂfld)) | 
| 12 | 8, 11 | syl 17 | . . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 𝐾 ∈
(SubRing‘ℂfld)) | 
| 13 |  | cnfldbas 21369 | . . . . . . 7
⊢ ℂ =
(Base‘ℂfld) | 
| 14 | 13 | subrgss 20573 | . . . . . 6
⊢ (𝐾 ∈
(SubRing‘ℂfld) → 𝐾 ⊆ ℂ) | 
| 15 | 12, 14 | syl 17 | . . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 𝐾 ⊆
ℂ) | 
| 16 |  | simpl2 1192 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 𝐴 ∈ 𝐾) | 
| 17 | 9, 10 | cphabscl 25220 | . . . . . . . 8
⊢ ((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾) → (abs‘𝐴) ∈ 𝐾) | 
| 18 | 8, 16, 17 | syl2anc 584 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ 𝐾) | 
| 19 | 15, 16 | sseldd 3983 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 𝐴 ∈
ℂ) | 
| 20 | 19 | abscld 15476 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ) | 
| 21 | 19 | absge0d 15484 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 0 ≤
(abs‘𝐴)) | 
| 22 | 9, 10 | cphsqrtcl 25219 | . . . . . . 7
⊢ ((𝑊 ∈ ℂPreHil ∧
((abs‘𝐴) ∈ 𝐾 ∧ (abs‘𝐴) ∈ ℝ ∧ 0 ≤
(abs‘𝐴))) →
(√‘(abs‘𝐴)) ∈ 𝐾) | 
| 23 | 8, 18, 20, 21, 22 | syl13anc 1373 | . . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(√‘(abs‘𝐴)) ∈ 𝐾) | 
| 24 |  | cnfldadd 21371 | . . . . . . . . 9
⊢  + =
(+g‘ℂfld) | 
| 25 | 24 | subrgacl 20584 | . . . . . . . 8
⊢ ((𝐾 ∈
(SubRing‘ℂfld) ∧ (abs‘𝐴) ∈ 𝐾 ∧ 𝐴 ∈ 𝐾) → ((abs‘𝐴) + 𝐴) ∈ 𝐾) | 
| 26 | 12, 18, 16, 25 | syl3anc 1372 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((abs‘𝐴) + 𝐴) ∈ 𝐾) | 
| 27 | 9, 10 | cphabscl 25220 | . . . . . . . 8
⊢ ((𝑊 ∈ ℂPreHil ∧
((abs‘𝐴) + 𝐴) ∈ 𝐾) → (abs‘((abs‘𝐴) + 𝐴)) ∈ 𝐾) | 
| 28 | 8, 26, 27 | syl2anc 584 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(abs‘((abs‘𝐴) +
𝐴)) ∈ 𝐾) | 
| 29 | 15, 26 | sseldd 3983 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((abs‘𝐴) + 𝐴) ∈
ℂ) | 
| 30 |  | simpl3 1193 | . . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → ¬ -𝐴 ∈
ℝ+) | 
| 31 | 20 | recnd 11290 | . . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℂ) | 
| 32 | 31, 19 | subnegd 11628 | . . . . . . . . . . . . 13
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((abs‘𝐴) −
-𝐴) = ((abs‘𝐴) + 𝐴)) | 
| 33 | 32 | eqeq1d 2738 | . . . . . . . . . . . 12
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) −
-𝐴) = 0 ↔
((abs‘𝐴) + 𝐴) = 0)) | 
| 34 | 19 | negcld 11608 | . . . . . . . . . . . . 13
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → -𝐴 ∈
ℂ) | 
| 35 | 31, 34 | subeq0ad 11631 | . . . . . . . . . . . 12
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) −
-𝐴) = 0 ↔
(abs‘𝐴) = -𝐴)) | 
| 36 | 33, 35 | bitr3d 281 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) + 𝐴) = 0 ↔ (abs‘𝐴) = -𝐴)) | 
| 37 |  | absrpcl 15328 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ+) | 
| 38 | 19, 37 | sylancom 588 | . . . . . . . . . . . 12
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ+) | 
| 39 |  | eleq1 2828 | . . . . . . . . . . . 12
⊢
((abs‘𝐴) =
-𝐴 → ((abs‘𝐴) ∈ ℝ+
↔ -𝐴 ∈
ℝ+)) | 
| 40 | 38, 39 | syl5ibcom 245 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((abs‘𝐴) = -𝐴 → -𝐴 ∈
ℝ+)) | 
| 41 | 36, 40 | sylbid 240 | . . . . . . . . . 10
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) + 𝐴) = 0 → -𝐴 ∈
ℝ+)) | 
| 42 | 41 | necon3bd 2953 | . . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → (¬ -𝐴 ∈ ℝ+
→ ((abs‘𝐴) +
𝐴) ≠
0)) | 
| 43 | 30, 42 | mpd 15 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((abs‘𝐴) + 𝐴) ≠ 0) | 
| 44 | 29, 43 | absne0d 15487 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(abs‘((abs‘𝐴) +
𝐴)) ≠
0) | 
| 45 | 9, 10 | cphdivcl 25217 | . . . . . . 7
⊢ ((𝑊 ∈ ℂPreHil ∧
(((abs‘𝐴) + 𝐴) ∈ 𝐾 ∧ (abs‘((abs‘𝐴) + 𝐴)) ∈ 𝐾 ∧ (abs‘((abs‘𝐴) + 𝐴)) ≠ 0)) → (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) ∈ 𝐾) | 
| 46 | 8, 26, 28, 44, 45 | syl13anc 1373 | . . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) ∈ 𝐾) | 
| 47 |  | cnfldmul 21373 | . . . . . . 7
⊢  ·
= (.r‘ℂfld) | 
| 48 | 47 | subrgmcl 20585 | . . . . . 6
⊢ ((𝐾 ∈
(SubRing‘ℂfld) ∧ (√‘(abs‘𝐴)) ∈ 𝐾 ∧ (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) ∈ 𝐾) → ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ 𝐾) | 
| 49 | 12, 23, 46, 48 | syl3anc 1372 | . . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ 𝐾) | 
| 50 | 15, 49 | sseldd 3983 | . . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ ℂ) | 
| 51 |  | eqid 2736 | . . . . . . 7
⊢
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) = ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) | 
| 52 | 51 | sqreulem 15399 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
((abs‘𝐴) + 𝐴) ≠ 0) →
((((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))↑2) = 𝐴 ∧ 0 ≤
(ℜ‘((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∧ (i ·
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∉
ℝ+)) | 
| 53 | 19, 43, 52 | syl2anc 584 | . . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))↑2) = 𝐴 ∧ 0 ≤
(ℜ‘((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∧ (i ·
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∉
ℝ+)) | 
| 54 | 53 | simp1d 1142 | . . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))↑2) = 𝐴) | 
| 55 | 53 | simp2d 1143 | . . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → 0 ≤
(ℜ‘((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))))) | 
| 56 | 53 | simp3d 1144 | . . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → (i ·
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∉
ℝ+) | 
| 57 |  | df-nel 3046 | . . . . 5
⊢ ((i
· ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∉ ℝ+ ↔
¬ (i · ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∈
ℝ+) | 
| 58 | 56, 57 | sylib 218 | . . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) → ¬ (i
· ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) ∈
ℝ+) | 
| 59 | 50, 19, 54, 55, 58 | eqsqrtd 15407 | . . 3
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) = (√‘𝐴)) | 
| 60 | 59, 49 | eqeltrrd 2841 | . 2
⊢ (((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) ∧ 𝐴 ≠ 0) →
(√‘𝐴) ∈
𝐾) | 
| 61 | 7, 60 | pm2.61dane 3028 | 1
⊢ ((𝑊 ∈ ℂPreHil ∧
𝐴 ∈ 𝐾 ∧ ¬ -𝐴 ∈ ℝ+) →
(√‘𝐴) ∈
𝐾) |