Metamath Proof Explorer

Theorem imsqrtvalex

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

Ref Expression
Assertion imsqrtvalex 
|- ( Im ` ( sqrt ` ( ; 1 5 + ( _i x. 8 ) ) ) ) = 1

Proof

Step Hyp Ref Expression
1 1nn0 
 |-  1 e. NN0
2 5nn0 
 |-  5 e. NN0
3 1 2 deccl 
 |-  ; 1 5 e. NN0
4 3 nn0cni 
 |-  ; 1 5 e. CC
5 ax-icn 
 |-  _i e. CC
6 8cn 
 |-  8 e. CC
7 5 6 mulcli 
 |-  ( _i x. 8 ) e. CC
8 4 7 addcli 
 |-  ( ; 1 5 + ( _i x. 8 ) ) e. CC
9 imsqrtval 
 |-  ( ( ; 1 5 + ( _i x. 8 ) ) e. CC -> ( Im ` ( sqrt ` ( ; 1 5 + ( _i x. 8 ) ) ) ) = ( if ( ( Im ` ( ; 1 5 + ( _i x. 8 ) ) ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) - ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) / 2 ) ) ) )
10 8 9 ax-mp 
 |-  ( Im ` ( sqrt ` ( ; 1 5 + ( _i x. 8 ) ) ) ) = ( if ( ( Im ` ( ; 1 5 + ( _i x. 8 ) ) ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) - ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) / 2 ) ) )
11 8pos 
 |-  0 < 8
12 0re 
 |-  0 e. RR
13 8re 
 |-  8 e. RR
14 12 13 ltnsymi 
 |-  ( 0 < 8 -> -. 8 < 0 )
15 3 nn0rei 
 |-  ; 1 5 e. RR
16 15 13 crimi 
 |-  ( Im ` ( ; 1 5 + ( _i x. 8 ) ) ) = 8
17 16 breq1i 
 |-  ( ( Im ` ( ; 1 5 + ( _i x. 8 ) ) ) < 0 <-> 8 < 0 )
18 14 17 sylnibr 
 |-  ( 0 < 8 -> -. ( Im ` ( ; 1 5 + ( _i x. 8 ) ) ) < 0 )
19 11 18 ax-mp 
 |-  -. ( Im ` ( ; 1 5 + ( _i x. 8 ) ) ) < 0
20 19 iffalsei 
 |-  if ( ( Im ` ( ; 1 5 + ( _i x. 8 ) ) ) < 0 , -u 1 , 1 ) = 1
21 absreim 
 |-  ( ( ; 1 5 e. RR /\ 8 e. RR ) -> ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) = ( sqrt ` ( ( ; 1 5 ^ 2 ) + ( 8 ^ 2 ) ) ) )
22 15 13 21 mp2an 
 |-  ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) = ( sqrt ` ( ( ; 1 5 ^ 2 ) + ( 8 ^ 2 ) ) )
23 4 sqvali 
 |-  ( ; 1 5 ^ 2 ) = ( ; 1 5 x. ; 1 5 )
24 eqid 
 |-  ; 1 5 = ; 1 5
25 7nn0 
 |-  7 e. NN0
26 4 mullidi 
 |-  ( 1 x. ; 1 5 ) = ; 1 5
27 1p1e2 
 |-  ( 1 + 1 ) = 2
28 2nn0 
 |-  2 e. NN0
29 25 nn0cni 
 |-  7 e. CC
30 2 nn0cni 
 |-  5 e. CC
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 x. ; 1 5 ) + 7 ) = ; 2 2
34 30 mulridi 
 |-  ( 5 x. 1 ) = 5
35 34 oveq1i 
 |-  ( ( 5 x. 1 ) + 2 ) = ( 5 + 2 )
36 5p2e7 
 |-  ( 5 + 2 ) = 7
37 35 36 eqtri 
 |-  ( ( 5 x. 1 ) + 2 ) = 7
38 5t5e25 
 |-  ( 5 x. 5 ) = ; 2 5
39 2 1 2 24 2 28 37 38 decmul2c 
 |-  ( 5 x. ; 1 5 ) = ; 7 5
40 3 1 2 24 2 25 33 39 decmul1c 
 |-  ( ; 1 5 x. ; 1 5 ) = ; ; 2 2 5
41 23 40 eqtri 
 |-  ( ; 1 5 ^ 2 ) = ; ; 2 2 5
42 6 sqvali 
 |-  ( 8 ^ 2 ) = ( 8 x. 8 )
43 8t8e64 
 |-  ( 8 x. 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 e. NN0
47 6nn0 
 |-  6 e. NN0
48 4nn0 
 |-  4 e. NN0
49 eqid 
 |-  ; ; 2 2 5 = ; ; 2 2 5
50 eqid 
 |-  ; 6 4 = ; 6 4
51 eqid 
 |-  ; 2 2 = ; 2 2
52 47 nn0cni 
 |-  6 e. CC
53 28 nn0cni 
 |-  2 e. CC
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 e. NN0
60 59 nn0cni 
 |-  ; 1 7 e. CC
61 60 sqvali 
 |-  ( ; 1 7 ^ 2 ) = ( ; 1 7 x. ; 1 7 )
62 eqid 
 |-  ; 1 7 = ; 1 7
63 9nn0 
 |-  9 e. NN0
64 1 1 deccl 
 |-  ; 1 1 e. NN0
65 60 mullidi 
 |-  ( 1 x. ; 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 x. ; 1 7 ) + ; 1 1 ) = ; 2 8
69 29 mulridi 
 |-  ( 7 x. 1 ) = 7
70 69 oveq1i 
 |-  ( ( 7 x. 1 ) + 4 ) = ( 7 + 4 )
71 7p4e11 
 |-  ( 7 + 4 ) = ; 1 1
72 70 71 eqtri 
 |-  ( ( 7 x. 1 ) + 4 ) = ; 1 1
73 7t7e49 
 |-  ( 7 x. 7 ) = ; 4 9
74 25 1 25 62 63 48 72 73 decmul2c 
 |-  ( 7 x. ; 1 7 ) = ; ; 1 1 9
75 59 1 25 62 63 64 68 74 decmul1c 
 |-  ( ; 1 7 x. ; 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 
 |-  ( sqrt ` ( ( ; 1 5 ^ 2 ) + ( 8 ^ 2 ) ) ) = ( sqrt ` ( ; 1 7 ^ 2 ) )
79 59 nn0ge0i 
 |-  0 <_ ; 1 7
80 59 nn0rei 
 |-  ; 1 7 e. RR
81 80 sqrtsqi 
 |-  ( 0 <_ ; 1 7 -> ( sqrt ` ( ; 1 7 ^ 2 ) ) = ; 1 7 )
82 79 81 ax-mp 
 |-  ( sqrt ` ( ; 1 7 ^ 2 ) ) = ; 1 7
83 22 78 82 3eqtri 
 |-  ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) = ; 1 7
84 15 13 crrei 
 |-  ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) = ; 1 5
85 83 84 oveq12i 
 |-  ( ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) - ( Re ` ( ; 1 5 + ( _i x. 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 x. 8 ) ) ) - ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) = 2
89 88 oveq1i 
 |-  ( ( ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) - ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) / 2 ) = ( 2 / 2 )
90 2div2e1 
 |-  ( 2 / 2 ) = 1
91 89 90 eqtri 
 |-  ( ( ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) - ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) / 2 ) = 1
92 91 fveq2i 
 |-  ( sqrt ` ( ( ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) - ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) / 2 ) ) = ( sqrt ` 1 )
93 sqrt1 
 |-  ( sqrt ` 1 ) = 1
94 92 93 eqtri 
 |-  ( sqrt ` ( ( ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) - ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) / 2 ) ) = 1
95 20 94 oveq12i 
 |-  ( if ( ( Im ` ( ; 1 5 + ( _i x. 8 ) ) ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) - ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) / 2 ) ) ) = ( 1 x. 1 )
96 1t1e1 
 |-  ( 1 x. 1 ) = 1
97 10 95 96 3eqtri 
 |-  ( Im ` ( sqrt ` ( ; 1 5 + ( _i x. 8 ) ) ) ) = 1