Proof of Theorem imsqrtvalex
Step | Hyp | Ref
| Expression |
1 | | 1nn0 11935 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
2 | | 5nn0 11939 |
. . . . . 6
⊢ 5 ∈
ℕ0 |
3 | 1, 2 | deccl 12137 |
. . . . 5
⊢ ;15 ∈
ℕ0 |
4 | 3 | nn0cni 11931 |
. . . 4
⊢ ;15 ∈ ℂ |
5 | | ax-icn 10619 |
. . . . 5
⊢ i ∈
ℂ |
6 | | 8cn 11756 |
. . . . 5
⊢ 8 ∈
ℂ |
7 | 5, 6 | mulcli 10671 |
. . . 4
⊢ (i
· 8) ∈ ℂ |
8 | 4, 7 | addcli 10670 |
. . 3
⊢ (;15 + (i · 8)) ∈
ℂ |
9 | | imsqrtval 40702 |
. . 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 11771 |
. . . . 5
⊢ 0 <
8 |
12 | | 0re 10666 |
. . . . . . 7
⊢ 0 ∈
ℝ |
13 | | 8re 11755 |
. . . . . . 7
⊢ 8 ∈
ℝ |
14 | 12, 13 | ltnsymi 10782 |
. . . . . 6
⊢ (0 < 8
→ ¬ 8 < 0) |
15 | 3 | nn0rei 11930 |
. . . . . . . 8
⊢ ;15 ∈ ℝ |
16 | 15, 13 | crimi 14585 |
. . . . . . 7
⊢
(ℑ‘(;15 + (i
· 8))) = 8 |
17 | 16 | breq1i 5032 |
. . . . . 6
⊢
((ℑ‘(;15 + (i
· 8))) < 0 ↔ 8 < 0) |
18 | 14, 17 | sylnibr 333 |
. . . . 5
⊢ (0 < 8
→ ¬ (ℑ‘(;15 +
(i · 8))) < 0) |
19 | 11, 18 | ax-mp 5 |
. . . 4
⊢ ¬
(ℑ‘(;15 + (i ·
8))) < 0 |
20 | 19 | iffalsei 4423 |
. . 3
⊢
if((ℑ‘(;15 + (i
· 8))) < 0, -1, 1) = 1 |
21 | | absreim 14686 |
. . . . . . . . . . 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 13578 |
. . . . . . . . . . . . . 14
⊢ (;15↑2) = (;15 · ;15) |
24 | | eqid 2759 |
. . . . . . . . . . . . . . 15
⊢ ;15 = ;15 |
25 | | 7nn0 11941 |
. . . . . . . . . . . . . . 15
⊢ 7 ∈
ℕ0 |
26 | 4 | mulid2i 10669 |
. . . . . . . . . . . . . . . 16
⊢ (1
· ;15) = ;15 |
27 | | 1p1e2 11784 |
. . . . . . . . . . . . . . . 16
⊢ (1 + 1) =
2 |
28 | | 2nn0 11936 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ0 |
29 | 25 | nn0cni 11931 |
. . . . . . . . . . . . . . . . 17
⊢ 7 ∈
ℂ |
30 | 2 | nn0cni 11931 |
. . . . . . . . . . . . . . . . 17
⊢ 5 ∈
ℂ |
31 | | 7p5e12 12199 |
. . . . . . . . . . . . . . . . 17
⊢ (7 + 5) =
;12 |
32 | 29, 30, 31 | addcomli 10855 |
. . . . . . . . . . . . . . . 16
⊢ (5 + 7) =
;12 |
33 | 1, 2, 25, 26, 27, 28, 32 | decaddci 12183 |
. . . . . . . . . . . . . . 15
⊢ ((1
· ;15) + 7) = ;22 |
34 | 30 | mulid1i 10668 |
. . . . . . . . . . . . . . . . . 18
⊢ (5
· 1) = 5 |
35 | 34 | oveq1i 7153 |
. . . . . . . . . . . . . . . . 17
⊢ ((5
· 1) + 2) = (5 + 2) |
36 | | 5p2e7 11815 |
. . . . . . . . . . . . . . . . 17
⊢ (5 + 2) =
7 |
37 | 35, 36 | eqtri 2782 |
. . . . . . . . . . . . . . . 16
⊢ ((5
· 1) + 2) = 7 |
38 | | 5t5e25 12225 |
. . . . . . . . . . . . . . . 16
⊢ (5
· 5) = ;25 |
39 | 2, 1, 2, 24, 2, 28, 37, 38 | decmul2c 12188 |
. . . . . . . . . . . . . . 15
⊢ (5
· ;15) = ;75 |
40 | 3, 1, 2, 24, 2, 25, 33, 39 | decmul1c 12187 |
. . . . . . . . . . . . . 14
⊢ (;15 · ;15) = ;;225 |
41 | 23, 40 | eqtri 2782 |
. . . . . . . . . . . . 13
⊢ (;15↑2) = ;;225 |
42 | 6 | sqvali 13578 |
. . . . . . . . . . . . . 14
⊢
(8↑2) = (8 · 8) |
43 | | 8t8e64 12243 |
. . . . . . . . . . . . . 14
⊢ (8
· 8) = ;64 |
44 | 42, 43 | eqtri 2782 |
. . . . . . . . . . . . 13
⊢
(8↑2) = ;64 |
45 | 41, 44 | oveq12i 7155 |
. . . . . . . . . . . 12
⊢ ((;15↑2) + (8↑2)) = (;;225 + ;64) |
46 | 28, 28 | deccl 12137 |
. . . . . . . . . . . . 13
⊢ ;22 ∈
ℕ0 |
47 | | 6nn0 11940 |
. . . . . . . . . . . . 13
⊢ 6 ∈
ℕ0 |
48 | | 4nn0 11938 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℕ0 |
49 | | eqid 2759 |
. . . . . . . . . . . . 13
⊢ ;;225 = ;;225 |
50 | | eqid 2759 |
. . . . . . . . . . . . 13
⊢ ;64 = ;64 |
51 | | eqid 2759 |
. . . . . . . . . . . . . 14
⊢ ;22 = ;22 |
52 | 47 | nn0cni 11931 |
. . . . . . . . . . . . . . 15
⊢ 6 ∈
ℂ |
53 | 28 | nn0cni 11931 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
54 | | 6p2e8 11818 |
. . . . . . . . . . . . . . 15
⊢ (6 + 2) =
8 |
55 | 52, 53, 54 | addcomli 10855 |
. . . . . . . . . . . . . 14
⊢ (2 + 6) =
8 |
56 | 28, 28, 47, 51, 55 | decaddi 12182 |
. . . . . . . . . . . . 13
⊢ (;22 + 6) = ;28 |
57 | | 5p4e9 11817 |
. . . . . . . . . . . . 13
⊢ (5 + 4) =
9 |
58 | 46, 2, 47, 48, 49, 50, 56, 57 | decadd 12176 |
. . . . . . . . . . . 12
⊢ (;;225 + ;64) = ;;289 |
59 | 1, 25 | deccl 12137 |
. . . . . . . . . . . . . . 15
⊢ ;17 ∈
ℕ0 |
60 | 59 | nn0cni 11931 |
. . . . . . . . . . . . . 14
⊢ ;17 ∈ ℂ |
61 | 60 | sqvali 13578 |
. . . . . . . . . . . . 13
⊢ (;17↑2) = (;17 · ;17) |
62 | | eqid 2759 |
. . . . . . . . . . . . . 14
⊢ ;17 = ;17 |
63 | | 9nn0 11943 |
. . . . . . . . . . . . . 14
⊢ 9 ∈
ℕ0 |
64 | 1, 1 | deccl 12137 |
. . . . . . . . . . . . . 14
⊢ ;11 ∈
ℕ0 |
65 | 60 | mulid2i 10669 |
. . . . . . . . . . . . . . 15
⊢ (1
· ;17) = ;17 |
66 | | eqid 2759 |
. . . . . . . . . . . . . . 15
⊢ ;11 = ;11 |
67 | | 7p1e8 11808 |
. . . . . . . . . . . . . . 15
⊢ (7 + 1) =
8 |
68 | 1, 25, 1, 1, 65, 66, 27, 67 | decadd 12176 |
. . . . . . . . . . . . . 14
⊢ ((1
· ;17) + ;11) = ;28 |
69 | 29 | mulid1i 10668 |
. . . . . . . . . . . . . . . . 17
⊢ (7
· 1) = 7 |
70 | 69 | oveq1i 7153 |
. . . . . . . . . . . . . . . 16
⊢ ((7
· 1) + 4) = (7 + 4) |
71 | | 7p4e11 12198 |
. . . . . . . . . . . . . . . 16
⊢ (7 + 4) =
;11 |
72 | 70, 71 | eqtri 2782 |
. . . . . . . . . . . . . . 15
⊢ ((7
· 1) + 4) = ;11 |
73 | | 7t7e49 12236 |
. . . . . . . . . . . . . . 15
⊢ (7
· 7) = ;49 |
74 | 25, 1, 25, 62, 63, 48, 72, 73 | decmul2c 12188 |
. . . . . . . . . . . . . 14
⊢ (7
· ;17) = ;;119 |
75 | 59, 1, 25, 62, 63, 64, 68, 74 | decmul1c 12187 |
. . . . . . . . . . . . 13
⊢ (;17 · ;17) = ;;289 |
76 | 61, 75 | eqtr2i 2783 |
. . . . . . . . . . . 12
⊢ ;;289 = (;17↑2) |
77 | 45, 58, 76 | 3eqtri 2786 |
. . . . . . . . . . 11
⊢ ((;15↑2) + (8↑2)) = (;17↑2) |
78 | 77 | fveq2i 6654 |
. . . . . . . . . 10
⊢
(√‘((;15↑2) + (8↑2))) = (√‘(;17↑2)) |
79 | 59 | nn0ge0i 11946 |
. . . . . . . . . . 11
⊢ 0 ≤
;17 |
80 | 59 | nn0rei 11930 |
. . . . . . . . . . . 12
⊢ ;17 ∈ ℝ |
81 | 80 | sqrtsqi 14767 |
. . . . . . . . . . 11
⊢ (0 ≤
;17 → (√‘(;17↑2)) = ;17) |
82 | 79, 81 | ax-mp 5 |
. . . . . . . . . 10
⊢
(√‘(;17↑2)) = ;17 |
83 | 22, 78, 82 | 3eqtri 2786 |
. . . . . . . . 9
⊢
(abs‘(;15 + (i
· 8))) = ;17 |
84 | 15, 13 | crrei 14584 |
. . . . . . . . 9
⊢
(ℜ‘(;15 + (i
· 8))) = ;15 |
85 | 83, 84 | oveq12i 7155 |
. . . . . . . 8
⊢
((abs‘(;15 + (i
· 8))) − (ℜ‘(;15 + (i · 8)))) = (;17 − ;15) |
86 | 1, 2, 28, 24, 36 | decaddi 12182 |
. . . . . . . . 9
⊢ (;15 + 2) = ;17 |
87 | 60, 4, 53, 86 | subaddrii 10998 |
. . . . . . . 8
⊢ (;17 − ;15) = 2 |
88 | 85, 87 | eqtri 2782 |
. . . . . . 7
⊢
((abs‘(;15 + (i
· 8))) − (ℜ‘(;15 + (i · 8)))) = 2 |
89 | 88 | oveq1i 7153 |
. . . . . 6
⊢
(((abs‘(;15 + (i
· 8))) − (ℜ‘(;15 + (i · 8)))) / 2) = (2 /
2) |
90 | | 2div2e1 11800 |
. . . . . 6
⊢ (2 / 2) =
1 |
91 | 89, 90 | eqtri 2782 |
. . . . 5
⊢
(((abs‘(;15 + (i
· 8))) − (ℜ‘(;15 + (i · 8)))) / 2) = 1 |
92 | 91 | fveq2i 6654 |
. . . 4
⊢
(√‘(((abs‘(;15 + (i · 8))) − (ℜ‘(;15 + (i · 8)))) / 2)) =
(√‘1) |
93 | | sqrt1 14664 |
. . . 4
⊢
(√‘1) = 1 |
94 | 92, 93 | eqtri 2782 |
. . 3
⊢
(√‘(((abs‘(;15 + (i · 8))) − (ℜ‘(;15 + (i · 8)))) / 2)) =
1 |
95 | 20, 94 | oveq12i 7155 |
. 2
⊢
(if((ℑ‘(;15 +
(i · 8))) < 0, -1, 1) · (√‘(((abs‘(;15 + (i · 8))) −
(ℜ‘(;15 + (i ·
8)))) / 2))) = (1 · 1) |
96 | | 1t1e1 11821 |
. 2
⊢ (1
· 1) = 1 |
97 | 10, 95, 96 | 3eqtri 2786 |
1
⊢
(ℑ‘(√‘(;15 + (i · 8)))) = 1 |