Proof of Theorem imsqrtvalex
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1nn0 12544 | . . . . . 6
⊢ 1 ∈
ℕ0 | 
| 2 |  | 5nn0 12548 | . . . . . 6
⊢ 5 ∈
ℕ0 | 
| 3 | 1, 2 | deccl 12750 | . . . . 5
⊢ ;15 ∈
ℕ0 | 
| 4 | 3 | nn0cni 12540 | . . . 4
⊢ ;15 ∈ ℂ | 
| 5 |  | ax-icn 11215 | . . . . 5
⊢ i ∈
ℂ | 
| 6 |  | 8cn 12364 | . . . . 5
⊢ 8 ∈
ℂ | 
| 7 | 5, 6 | mulcli 11269 | . . . 4
⊢ (i
· 8) ∈ ℂ | 
| 8 | 4, 7 | addcli 11268 | . . 3
⊢ (;15 + (i · 8)) ∈
ℂ | 
| 9 |  | imsqrtval 43662 | . . 3
⊢ ((;15 + (i · 8)) ∈ ℂ
→ (ℑ‘(√‘(;15 + (i · 8)))) = (if((ℑ‘(;15 + (i · 8))) < 0, -1, 1)
· (√‘(((abs‘(;15 + (i · 8))) − (ℜ‘(;15 + (i · 8)))) /
2)))) | 
| 10 | 8, 9 | ax-mp 5 | . 2
⊢
(ℑ‘(√‘(;15 + (i · 8)))) = (if((ℑ‘(;15 + (i · 8))) < 0, -1, 1)
· (√‘(((abs‘(;15 + (i · 8))) − (ℜ‘(;15 + (i · 8)))) /
2))) | 
| 11 |  | 8pos 12379 | . . . . 5
⊢ 0 <
8 | 
| 12 |  | 0re 11264 | . . . . . . 7
⊢ 0 ∈
ℝ | 
| 13 |  | 8re 12363 | . . . . . . 7
⊢ 8 ∈
ℝ | 
| 14 | 12, 13 | ltnsymi 11381 | . . . . . 6
⊢ (0 < 8
→ ¬ 8 < 0) | 
| 15 | 3 | nn0rei 12539 | . . . . . . . 8
⊢ ;15 ∈ ℝ | 
| 16 | 15, 13 | crimi 15233 | . . . . . . 7
⊢
(ℑ‘(;15 + (i
· 8))) = 8 | 
| 17 | 16 | breq1i 5149 | . . . . . 6
⊢
((ℑ‘(;15 + (i
· 8))) < 0 ↔ 8 < 0) | 
| 18 | 14, 17 | sylnibr 329 | . . . . 5
⊢ (0 < 8
→ ¬ (ℑ‘(;15 +
(i · 8))) < 0) | 
| 19 | 11, 18 | ax-mp 5 | . . . 4
⊢  ¬
(ℑ‘(;15 + (i ·
8))) < 0 | 
| 20 | 19 | iffalsei 4534 | . . 3
⊢
if((ℑ‘(;15 + (i
· 8))) < 0, -1, 1) = 1 | 
| 21 |  | absreim 15333 | . . . . . . . . . . 11
⊢ ((;15 ∈ ℝ ∧ 8 ∈
ℝ) → (abs‘(;15 +
(i · 8))) = (√‘((;15↑2) + (8↑2)))) | 
| 22 | 15, 13, 21 | mp2an 692 | . . . . . . . . . 10
⊢
(abs‘(;15 + (i
· 8))) = (√‘((;15↑2) + (8↑2))) | 
| 23 | 4 | sqvali 14220 | . . . . . . . . . . . . . 14
⊢ (;15↑2) = (;15 · ;15) | 
| 24 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ ;15 = ;15 | 
| 25 |  | 7nn0 12550 | . . . . . . . . . . . . . . 15
⊢ 7 ∈
ℕ0 | 
| 26 | 4 | mullidi 11267 | . . . . . . . . . . . . . . . 16
⊢ (1
· ;15) = ;15 | 
| 27 |  | 1p1e2 12392 | . . . . . . . . . . . . . . . 16
⊢ (1 + 1) =
2 | 
| 28 |  | 2nn0 12545 | . . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ0 | 
| 29 | 25 | nn0cni 12540 | . . . . . . . . . . . . . . . . 17
⊢ 7 ∈
ℂ | 
| 30 | 2 | nn0cni 12540 | . . . . . . . . . . . . . . . . 17
⊢ 5 ∈
ℂ | 
| 31 |  | 7p5e12 12812 | . . . . . . . . . . . . . . . . 17
⊢ (7 + 5) =
;12 | 
| 32 | 29, 30, 31 | addcomli 11454 | . . . . . . . . . . . . . . . 16
⊢ (5 + 7) =
;12 | 
| 33 | 1, 2, 25, 26, 27, 28, 32 | decaddci 12796 | . . . . . . . . . . . . . . 15
⊢ ((1
· ;15) + 7) = ;22 | 
| 34 | 30 | mulridi 11266 | . . . . . . . . . . . . . . . . . 18
⊢ (5
· 1) = 5 | 
| 35 | 34 | oveq1i 7442 | . . . . . . . . . . . . . . . . 17
⊢ ((5
· 1) + 2) = (5 + 2) | 
| 36 |  | 5p2e7 12423 | . . . . . . . . . . . . . . . . 17
⊢ (5 + 2) =
7 | 
| 37 | 35, 36 | eqtri 2764 | . . . . . . . . . . . . . . . 16
⊢ ((5
· 1) + 2) = 7 | 
| 38 |  | 5t5e25 12838 | . . . . . . . . . . . . . . . 16
⊢ (5
· 5) = ;25 | 
| 39 | 2, 1, 2, 24, 2, 28, 37, 38 | decmul2c 12801 | . . . . . . . . . . . . . . 15
⊢ (5
· ;15) = ;75 | 
| 40 | 3, 1, 2, 24, 2, 25, 33, 39 | decmul1c 12800 | . . . . . . . . . . . . . 14
⊢ (;15 · ;15) = ;;225 | 
| 41 | 23, 40 | eqtri 2764 | . . . . . . . . . . . . 13
⊢ (;15↑2) = ;;225 | 
| 42 | 6 | sqvali 14220 | . . . . . . . . . . . . . 14
⊢
(8↑2) = (8 · 8) | 
| 43 |  | 8t8e64 12856 | . . . . . . . . . . . . . 14
⊢ (8
· 8) = ;64 | 
| 44 | 42, 43 | eqtri 2764 | . . . . . . . . . . . . 13
⊢
(8↑2) = ;64 | 
| 45 | 41, 44 | oveq12i 7444 | . . . . . . . . . . . 12
⊢ ((;15↑2) + (8↑2)) = (;;225 + ;64) | 
| 46 | 28, 28 | deccl 12750 | . . . . . . . . . . . . 13
⊢ ;22 ∈
ℕ0 | 
| 47 |  | 6nn0 12549 | . . . . . . . . . . . . 13
⊢ 6 ∈
ℕ0 | 
| 48 |  | 4nn0 12547 | . . . . . . . . . . . . 13
⊢ 4 ∈
ℕ0 | 
| 49 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ ;;225 = ;;225 | 
| 50 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ ;64 = ;64 | 
| 51 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ ;22 = ;22 | 
| 52 | 47 | nn0cni 12540 | . . . . . . . . . . . . . . 15
⊢ 6 ∈
ℂ | 
| 53 | 28 | nn0cni 12540 | . . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ | 
| 54 |  | 6p2e8 12426 | . . . . . . . . . . . . . . 15
⊢ (6 + 2) =
8 | 
| 55 | 52, 53, 54 | addcomli 11454 | . . . . . . . . . . . . . 14
⊢ (2 + 6) =
8 | 
| 56 | 28, 28, 47, 51, 55 | decaddi 12795 | . . . . . . . . . . . . 13
⊢ (;22 + 6) = ;28 | 
| 57 |  | 5p4e9 12425 | . . . . . . . . . . . . 13
⊢ (5 + 4) =
9 | 
| 58 | 46, 2, 47, 48, 49, 50, 56, 57 | decadd 12789 | . . . . . . . . . . . 12
⊢ (;;225 + ;64) = ;;289 | 
| 59 | 1, 25 | deccl 12750 | . . . . . . . . . . . . . . 15
⊢ ;17 ∈
ℕ0 | 
| 60 | 59 | nn0cni 12540 | . . . . . . . . . . . . . 14
⊢ ;17 ∈ ℂ | 
| 61 | 60 | sqvali 14220 | . . . . . . . . . . . . 13
⊢ (;17↑2) = (;17 · ;17) | 
| 62 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ ;17 = ;17 | 
| 63 |  | 9nn0 12552 | . . . . . . . . . . . . . 14
⊢ 9 ∈
ℕ0 | 
| 64 | 1, 1 | deccl 12750 | . . . . . . . . . . . . . 14
⊢ ;11 ∈
ℕ0 | 
| 65 | 60 | mullidi 11267 | . . . . . . . . . . . . . . 15
⊢ (1
· ;17) = ;17 | 
| 66 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ ;11 = ;11 | 
| 67 |  | 7p1e8 12416 | . . . . . . . . . . . . . . 15
⊢ (7 + 1) =
8 | 
| 68 | 1, 25, 1, 1, 65, 66, 27, 67 | decadd 12789 | . . . . . . . . . . . . . 14
⊢ ((1
· ;17) + ;11) = ;28 | 
| 69 | 29 | mulridi 11266 | . . . . . . . . . . . . . . . . 17
⊢ (7
· 1) = 7 | 
| 70 | 69 | oveq1i 7442 | . . . . . . . . . . . . . . . 16
⊢ ((7
· 1) + 4) = (7 + 4) | 
| 71 |  | 7p4e11 12811 | . . . . . . . . . . . . . . . 16
⊢ (7 + 4) =
;11 | 
| 72 | 70, 71 | eqtri 2764 | . . . . . . . . . . . . . . 15
⊢ ((7
· 1) + 4) = ;11 | 
| 73 |  | 7t7e49 12849 | . . . . . . . . . . . . . . 15
⊢ (7
· 7) = ;49 | 
| 74 | 25, 1, 25, 62, 63, 48, 72, 73 | decmul2c 12801 | . . . . . . . . . . . . . 14
⊢ (7
· ;17) = ;;119 | 
| 75 | 59, 1, 25, 62, 63, 64, 68, 74 | decmul1c 12800 | . . . . . . . . . . . . 13
⊢ (;17 · ;17) = ;;289 | 
| 76 | 61, 75 | eqtr2i 2765 | . . . . . . . . . . . 12
⊢ ;;289 = (;17↑2) | 
| 77 | 45, 58, 76 | 3eqtri 2768 | . . . . . . . . . . 11
⊢ ((;15↑2) + (8↑2)) = (;17↑2) | 
| 78 | 77 | fveq2i 6908 | . . . . . . . . . 10
⊢
(√‘((;15↑2) + (8↑2))) = (√‘(;17↑2)) | 
| 79 | 59 | nn0ge0i 12555 | . . . . . . . . . . 11
⊢ 0 ≤
;17 | 
| 80 | 59 | nn0rei 12539 | . . . . . . . . . . . 12
⊢ ;17 ∈ ℝ | 
| 81 | 80 | sqrtsqi 15414 | . . . . . . . . . . 11
⊢ (0 ≤
;17 → (√‘(;17↑2)) = ;17) | 
| 82 | 79, 81 | ax-mp 5 | . . . . . . . . . 10
⊢
(√‘(;17↑2)) = ;17 | 
| 83 | 22, 78, 82 | 3eqtri 2768 | . . . . . . . . 9
⊢
(abs‘(;15 + (i
· 8))) = ;17 | 
| 84 | 15, 13 | crrei 15232 | . . . . . . . . 9
⊢
(ℜ‘(;15 + (i
· 8))) = ;15 | 
| 85 | 83, 84 | oveq12i 7444 | . . . . . . . 8
⊢
((abs‘(;15 + (i
· 8))) − (ℜ‘(;15 + (i · 8)))) = (;17 − ;15) | 
| 86 | 1, 2, 28, 24, 36 | decaddi 12795 | . . . . . . . . 9
⊢ (;15 + 2) = ;17 | 
| 87 | 60, 4, 53, 86 | subaddrii 11599 | . . . . . . . 8
⊢ (;17 − ;15) = 2 | 
| 88 | 85, 87 | eqtri 2764 | . . . . . . 7
⊢
((abs‘(;15 + (i
· 8))) − (ℜ‘(;15 + (i · 8)))) = 2 | 
| 89 | 88 | oveq1i 7442 | . . . . . 6
⊢
(((abs‘(;15 + (i
· 8))) − (ℜ‘(;15 + (i · 8)))) / 2) = (2 /
2) | 
| 90 |  | 2div2e1 12408 | . . . . . 6
⊢ (2 / 2) =
1 | 
| 91 | 89, 90 | eqtri 2764 | . . . . 5
⊢
(((abs‘(;15 + (i
· 8))) − (ℜ‘(;15 + (i · 8)))) / 2) = 1 | 
| 92 | 91 | fveq2i 6908 | . . . 4
⊢
(√‘(((abs‘(;15 + (i · 8))) − (ℜ‘(;15 + (i · 8)))) / 2)) =
(√‘1) | 
| 93 |  | sqrt1 15311 | . . . 4
⊢
(√‘1) = 1 | 
| 94 | 92, 93 | eqtri 2764 | . . 3
⊢
(√‘(((abs‘(;15 + (i · 8))) − (ℜ‘(;15 + (i · 8)))) / 2)) =
1 | 
| 95 | 20, 94 | oveq12i 7444 | . 2
⊢
(if((ℑ‘(;15 +
(i · 8))) < 0, -1, 1) · (√‘(((abs‘(;15 + (i · 8))) −
(ℜ‘(;15 + (i ·
8)))) / 2))) = (1 · 1) | 
| 96 |  | 1t1e1 12429 | . 2
⊢ (1
· 1) = 1 | 
| 97 | 10, 95, 96 | 3eqtri 2768 | 1
⊢
(ℑ‘(√‘(;15 + (i · 8)))) = 1 |