Metamath Proof Explorer

Theorem imsqrtvalex

Description: Example for imsqrtval . (Contributed by RP, 21-May-2024)

Ref Expression
Assertion imsqrtvalex ( ℑ ‘ ( √ ‘ ( 1 5 + ( i · 8 ) ) ) ) = 1

Proof

Step Hyp Ref Expression
1 1nn0 ⊢ 1 ∈ ℕ0
2 5nn0 ⊢ 5 ∈ ℕ0
3 1 2 deccl ⊢ 1 5 ∈ ℕ0
4 3 nn0cni ⊢ 1 5 ∈ ℂ
5 ax-icn ⊢ i ∈ ℂ
6 8cn ⊢ 8 ∈ ℂ
7 5 6 mulcli ⊢ ( i · 8 ) ∈ ℂ
8 4 7 addcli ⊢ ( 1 5 + ( i · 8 ) ) ∈ ℂ
9 imsqrtval ⊢ ( ( 1 5 + ( i · 8 ) ) ∈ ℂ → ( ℑ ‘ ( √ ‘ ( 1 5 + ( i · 8 ) ) ) ) = ( if ( ( ℑ ‘ ( 1 5 + ( i · 8 ) ) ) < 0 , - 1 , 1 ) · ( √ ‘ ( ( ( abs ‘ ( 1 5 + ( i · 8 ) ) ) − ( ℜ ‘ ( 1 5 + ( i · 8 ) ) ) ) / 2 ) ) ) )
10 8 9 ax-mp ⊢ ( ℑ ‘ ( √ ‘ ( 1 5 + ( i · 8 ) ) ) ) = ( if ( ( ℑ ‘ ( 1 5 + ( i · 8 ) ) ) < 0 , - 1 , 1 ) · ( √ ‘ ( ( ( abs ‘ ( 1 5 + ( i · 8 ) ) ) − ( ℜ ‘ ( 1 5 + ( i · 8 ) ) ) ) / 2 ) ) )
11 8pos ⊢ 0 < 8
12 0re ⊢ 0 ∈ ℝ
13 8re ⊢ 8 ∈ ℝ
14 12 13 ltnsymi ⊢ ( 0 < 8 → ¬ 8 < 0 )
15 3 nn0rei ⊢ 1 5 ∈ ℝ
16 15 13 crimi ⊢ ( ℑ ‘ ( 1 5 + ( i · 8 ) ) ) = 8
17 16 breq1i ⊢ ( ( ℑ ‘ ( 1 5 + ( i · 8 ) ) ) < 0 ↔ 8 < 0 )
18 14 17 sylnibr ⊢ ( 0 < 8 → ¬ ( ℑ ‘ ( 1 5 + ( i · 8 ) ) ) < 0 )
19 11 18 ax-mp ⊢ ¬ ( ℑ ‘ ( 1 5 + ( i · 8 ) ) ) < 0
20 19 iffalsei ⊢ if ( ( ℑ ‘ ( 1 5 + ( i · 8 ) ) ) < 0 , - 1 , 1 ) = 1
21 absreim ⊢ ( ( 1 5 ∈ ℝ ∧ 8 ∈ ℝ ) → ( abs ‘ ( 1 5 + ( i · 8 ) ) ) = ( √ ‘ ( ( 1 5 ↑ 2 ) + ( 8 ↑ 2 ) ) ) )
22 15 13 21 mp2an ⊢ ( abs ‘ ( 1 5 + ( i · 8 ) ) ) = ( √ ‘ ( ( 1 5 ↑ 2 ) + ( 8 ↑ 2 ) ) )
23 4 sqvali ⊢ ( 1 5 ↑ 2 ) = ( 1 5 · 1 5 )
24 eqid ⊢ 1 5 = 1 5
25 7nn0 ⊢ 7 ∈ ℕ0
26 4 mulid2i ⊢ ( 1 · 1 5 ) = 1 5
27 1p1e2 ⊢ ( 1 + 1 ) = 2
28 2nn0 ⊢ 2 ∈ ℕ0
29 25 nn0cni ⊢ 7 ∈ ℂ
30 2 nn0cni ⊢ 5 ∈ ℂ
31 7p5e12 ⊢ ( 7 + 5 ) = 1 2
32 29 30 31 addcomli ⊢ ( 5 + 7 ) = 1 2
33 1 2 25 26 27 28 32 decaddci ⊢ ( ( 1 · 1 5 ) + 7 ) = 2 2
34 30 mulid1i ⊢ ( 5 · 1 ) = 5
35 34 oveq1i ⊢ ( ( 5 · 1 ) + 2 ) = ( 5 + 2 )
36 5p2e7 ⊢ ( 5 + 2 ) = 7
37 35 36 eqtri ⊢ ( ( 5 · 1 ) + 2 ) = 7
38 5t5e25 ⊢ ( 5 · 5 ) = 2 5
39 2 1 2 24 2 28 37 38 decmul2c ⊢ ( 5 · 1 5 ) = 7 5
40 3 1 2 24 2 25 33 39 decmul1c ⊢ ( 1 5 · 1 5 ) = 2 2 5
41 23 40 eqtri ⊢ ( 1 5 ↑ 2 ) = 2 2 5
42 6 sqvali ⊢ ( 8 ↑ 2 ) = ( 8 · 8 )
43 8t8e64 ⊢ ( 8 · 8 ) = 6 4
44 42 43 eqtri ⊢ ( 8 ↑ 2 ) = 6 4
45 41 44 oveq12i ⊢ ( ( 1 5 ↑ 2 ) + ( 8 ↑ 2 ) ) = ( 2 2 5 + 6 4 )
46 28 28 deccl ⊢ 2 2 ∈ ℕ0
47 6nn0 ⊢ 6 ∈ ℕ0
48 4nn0 ⊢ 4 ∈ ℕ0
49 eqid ⊢ 2 2 5 = 2 2 5
50 eqid ⊢ 6 4 = 6 4
51 eqid ⊢ 2 2 = 2 2
52 47 nn0cni ⊢ 6 ∈ ℂ
53 28 nn0cni ⊢ 2 ∈ ℂ
54 6p2e8 ⊢ ( 6 + 2 ) = 8
55 52 53 54 addcomli ⊢ ( 2 + 6 ) = 8
56 28 28 47 51 55 decaddi ⊢ ( 2 2 + 6 ) = 2 8
57 5p4e9 ⊢ ( 5 + 4 ) = 9
58 46 2 47 48 49 50 56 57 decadd ⊢ ( 2 2 5 + 6 4 ) = 2 8 9
59 1 25 deccl ⊢ 1 7 ∈ ℕ0
60 59 nn0cni ⊢ 1 7 ∈ ℂ
61 60 sqvali ⊢ ( 1 7 ↑ 2 ) = ( 1 7 · 1 7 )
62 eqid ⊢ 1 7 = 1 7
63 9nn0 ⊢ 9 ∈ ℕ0
64 1 1 deccl ⊢ 1 1 ∈ ℕ0
65 60 mulid2i ⊢ ( 1 · 1 7 ) = 1 7
66 eqid ⊢ 1 1 = 1 1
67 7p1e8 ⊢ ( 7 + 1 ) = 8
68 1 25 1 1 65 66 27 67 decadd ⊢ ( ( 1 · 1 7 ) + 1 1 ) = 2 8
69 29 mulid1i ⊢ ( 7 · 1 ) = 7
70 69 oveq1i ⊢ ( ( 7 · 1 ) + 4 ) = ( 7 + 4 )
71 7p4e11 ⊢ ( 7 + 4 ) = 1 1
72 70 71 eqtri ⊢ ( ( 7 · 1 ) + 4 ) = 1 1
73 7t7e49 ⊢ ( 7 · 7 ) = 4 9
74 25 1 25 62 63 48 72 73 decmul2c ⊢ ( 7 · 1 7 ) = 1 1 9
75 59 1 25 62 63 64 68 74 decmul1c ⊢ ( 1 7 · 1 7 ) = 2 8 9
76 61 75 eqtr2i ⊢ 2 8 9 = ( 1 7 ↑ 2 )
77 45 58 76 3eqtri ⊢ ( ( 1 5 ↑ 2 ) + ( 8 ↑ 2 ) ) = ( 1 7 ↑ 2 )
78 77 fveq2i ⊢ ( √ ‘ ( ( 1 5 ↑ 2 ) + ( 8 ↑ 2 ) ) ) = ( √ ‘ ( 1 7 ↑ 2 ) )
79 59 nn0ge0i ⊢ 0 ≤ 1 7
80 59 nn0rei ⊢ 1 7 ∈ ℝ
81 80 sqrtsqi ⊢ ( 0 ≤ 1 7 → ( √ ‘ ( 1 7 ↑ 2 ) ) = 1 7 )
82 79 81 ax-mp ⊢ ( √ ‘ ( 1 7 ↑ 2 ) ) = 1 7
83 22 78 82 3eqtri ⊢ ( abs ‘ ( 1 5 + ( i · 8 ) ) ) = 1 7
84 15 13 crrei ⊢ ( ℜ ‘ ( 1 5 + ( i · 8 ) ) ) = 1 5
85 83 84 oveq12i ⊢ ( ( abs ‘ ( 1 5 + ( i · 8 ) ) ) − ( ℜ ‘ ( 1 5 + ( i · 8 ) ) ) ) = ( 1 7 − 1 5 )
86 1 2 28 24 36 decaddi ⊢ ( 1 5 + 2 ) = 1 7
87 60 4 53 86 subaddrii ⊢ ( 1 7 − 1 5 ) = 2
88 85 87 eqtri ⊢ ( ( abs ‘ ( 1 5 + ( i · 8 ) ) ) − ( ℜ ‘ ( 1 5 + ( i · 8 ) ) ) ) = 2
89 88 oveq1i ⊢ ( ( ( abs ‘ ( 1 5 + ( i · 8 ) ) ) − ( ℜ ‘ ( 1 5 + ( i · 8 ) ) ) ) / 2 ) = ( 2 / 2 )
90 2div2e1 ⊢ ( 2 / 2 ) = 1
91 89 90 eqtri ⊢ ( ( ( abs ‘ ( 1 5 + ( i · 8 ) ) ) − ( ℜ ‘ ( 1 5 + ( i · 8 ) ) ) ) / 2 ) = 1
92 91 fveq2i ⊢ ( √ ‘ ( ( ( abs ‘ ( 1 5 + ( i · 8 ) ) ) − ( ℜ ‘ ( 1 5 + ( i · 8 ) ) ) ) / 2 ) ) = ( √ ‘ 1 )
93 sqrt1 ⊢ ( √ ‘ 1 ) = 1
94 92 93 eqtri ⊢ ( √ ‘ ( ( ( abs ‘ ( 1 5 + ( i · 8 ) ) ) − ( ℜ ‘ ( 1 5 + ( i · 8 ) ) ) ) / 2 ) ) = 1
95 20 94 oveq12i ⊢ ( if ( ( ℑ ‘ ( 1 5 + ( i · 8 ) ) ) < 0 , - 1 , 1 ) · ( √ ‘ ( ( ( abs ‘ ( 1 5 + ( i · 8 ) ) ) − ( ℜ ‘ ( 1 5 + ( i · 8 ) ) ) ) / 2 ) ) ) = ( 1 · 1 )
96 1t1e1 ⊢ ( 1 · 1 ) = 1
97 10 95 96 3eqtri ⊢ ( ℑ ‘ ( √ ‘ ( 1 5 + ( i · 8 ) ) ) ) = 1