Metamath Proof Explorer

Theorem resqrtvalex

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

Ref Expression
Assertion resqrtvalex 
|- ( Re ` ( sqrt ` ( ; 1 5 + ( _i x. 8 ) ) ) ) = 4

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 resqrtval 
 |-  ( ( ; 1 5 + ( _i x. 8 ) ) e. CC -> ( Re ` ( sqrt ` ( ; 1 5 + ( _i x. 8 ) ) ) ) = ( sqrt ` ( ( ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) + ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) / 2 ) ) )
10 8 9 ax-mp 
 |-  ( Re ` ( sqrt ` ( ; 1 5 + ( _i x. 8 ) ) ) ) = ( sqrt ` ( ( ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) + ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) / 2 ) )
11 7nn0 
 |-  7 e. NN0
12 3 nn0rei 
 |-  ; 1 5 e. RR
13 8re 
 |-  8 e. RR
14 absreim 
 |-  ( ( ; 1 5 e. RR /\ 8 e. RR ) -> ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) = ( sqrt ` ( ( ; 1 5 ^ 2 ) + ( 8 ^ 2 ) ) ) )
15 12 13 14 mp2an 
 |-  ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) = ( sqrt ` ( ( ; 1 5 ^ 2 ) + ( 8 ^ 2 ) ) )
16 4 sqvali 
 |-  ( ; 1 5 ^ 2 ) = ( ; 1 5 x. ; 1 5 )
17 eqid 
 |-  ; 1 5 = ; 1 5
18 4 mullidi 
 |-  ( 1 x. ; 1 5 ) = ; 1 5
19 1p1e2 
 |-  ( 1 + 1 ) = 2
20 2nn0 
 |-  2 e. NN0
21 11 nn0cni 
 |-  7 e. CC
22 2 nn0cni 
 |-  5 e. CC
23 7p5e12 
 |-  ( 7 + 5 ) = ; 1 2
24 21 22 23 addcomli 
 |-  ( 5 + 7 ) = ; 1 2
25 1 2 11 18 19 20 24 decaddci 
 |-  ( ( 1 x. ; 1 5 ) + 7 ) = ; 2 2
26 22 mulridi 
 |-  ( 5 x. 1 ) = 5
27 26 oveq1i 
 |-  ( ( 5 x. 1 ) + 2 ) = ( 5 + 2 )
28 5p2e7 
 |-  ( 5 + 2 ) = 7
29 27 28 eqtri 
 |-  ( ( 5 x. 1 ) + 2 ) = 7
30 5t5e25 
 |-  ( 5 x. 5 ) = ; 2 5
31 2 1 2 17 2 20 29 30 decmul2c 
 |-  ( 5 x. ; 1 5 ) = ; 7 5
32 3 1 2 17 2 11 25 31 decmul1c 
 |-  ( ; 1 5 x. ; 1 5 ) = ; ; 2 2 5
33 16 32 eqtri 
 |-  ( ; 1 5 ^ 2 ) = ; ; 2 2 5
34 6 sqvali 
 |-  ( 8 ^ 2 ) = ( 8 x. 8 )
35 8t8e64 
 |-  ( 8 x. 8 ) = ; 6 4
36 34 35 eqtri 
 |-  ( 8 ^ 2 ) = ; 6 4
37 33 36 oveq12i 
 |-  ( ( ; 1 5 ^ 2 ) + ( 8 ^ 2 ) ) = ( ; ; 2 2 5 + ; 6 4 )
38 20 20 deccl 
 |-  ; 2 2 e. NN0
39 6nn0 
 |-  6 e. NN0
40 4nn0 
 |-  4 e. NN0
41 eqid 
 |-  ; ; 2 2 5 = ; ; 2 2 5
42 eqid 
 |-  ; 6 4 = ; 6 4
43 eqid 
 |-  ; 2 2 = ; 2 2
44 39 nn0cni 
 |-  6 e. CC
45 2cn 
 |-  2 e. CC
46 6p2e8 
 |-  ( 6 + 2 ) = 8
47 44 45 46 addcomli 
 |-  ( 2 + 6 ) = 8
48 20 20 39 43 47 decaddi 
 |-  ( ; 2 2 + 6 ) = ; 2 8
49 5p4e9 
 |-  ( 5 + 4 ) = 9
50 38 2 39 40 41 42 48 49 decadd 
 |-  ( ; ; 2 2 5 + ; 6 4 ) = ; ; 2 8 9
51 1 11 deccl 
 |-  ; 1 7 e. NN0
52 51 nn0cni 
 |-  ; 1 7 e. CC
53 52 sqvali 
 |-  ( ; 1 7 ^ 2 ) = ( ; 1 7 x. ; 1 7 )
54 eqid 
 |-  ; 1 7 = ; 1 7
55 9nn0 
 |-  9 e. NN0
56 1 1 deccl 
 |-  ; 1 1 e. NN0
57 52 mullidi 
 |-  ( 1 x. ; 1 7 ) = ; 1 7
58 eqid 
 |-  ; 1 1 = ; 1 1
59 7p1e8 
 |-  ( 7 + 1 ) = 8
60 1 11 1 1 57 58 19 59 decadd 
 |-  ( ( 1 x. ; 1 7 ) + ; 1 1 ) = ; 2 8
61 21 mulridi 
 |-  ( 7 x. 1 ) = 7
62 61 oveq1i 
 |-  ( ( 7 x. 1 ) + 4 ) = ( 7 + 4 )
63 7p4e11 
 |-  ( 7 + 4 ) = ; 1 1
64 62 63 eqtri 
 |-  ( ( 7 x. 1 ) + 4 ) = ; 1 1
65 7t7e49 
 |-  ( 7 x. 7 ) = ; 4 9
66 11 1 11 54 55 40 64 65 decmul2c 
 |-  ( 7 x. ; 1 7 ) = ; ; 1 1 9
67 51 1 11 54 55 56 60 66 decmul1c 
 |-  ( ; 1 7 x. ; 1 7 ) = ; ; 2 8 9
68 53 67 eqtr2i 
 |-  ; ; 2 8 9 = ( ; 1 7 ^ 2 )
69 37 50 68 3eqtri 
 |-  ( ( ; 1 5 ^ 2 ) + ( 8 ^ 2 ) ) = ( ; 1 7 ^ 2 )
70 69 fveq2i 
 |-  ( sqrt ` ( ( ; 1 5 ^ 2 ) + ( 8 ^ 2 ) ) ) = ( sqrt ` ( ; 1 7 ^ 2 ) )
71 51 nn0ge0i 
 |-  0 <_ ; 1 7
72 51 nn0rei 
 |-  ; 1 7 e. RR
73 72 sqrtsqi 
 |-  ( 0 <_ ; 1 7 -> ( sqrt ` ( ; 1 7 ^ 2 ) ) = ; 1 7 )
74 71 73 ax-mp 
 |-  ( sqrt ` ( ; 1 7 ^ 2 ) ) = ; 1 7
75 15 70 74 3eqtri 
 |-  ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) = ; 1 7
76 12 13 crrei 
 |-  ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) = ; 1 5
77 19 oveq1i 
 |-  ( ( 1 + 1 ) + 1 ) = ( 2 + 1 )
78 2p1e3 
 |-  ( 2 + 1 ) = 3
79 77 78 eqtri 
 |-  ( ( 1 + 1 ) + 1 ) = 3
80 1 11 1 2 75 76 79 20 23 decaddc 
 |-  ( ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) + ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) = ; 3 2
81 80 oveq1i 
 |-  ( ( ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) + ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) / 2 ) = ( ; 3 2 / 2 )
82 eqid 
 |-  ; 1 6 = ; 1 6
83 45 mulridi 
 |-  ( 2 x. 1 ) = 2
84 83 oveq1i 
 |-  ( ( 2 x. 1 ) + 1 ) = ( 2 + 1 )
85 84 78 eqtri 
 |-  ( ( 2 x. 1 ) + 1 ) = 3
86 6t2e12 
 |-  ( 6 x. 2 ) = ; 1 2
87 44 45 86 mulcomli 
 |-  ( 2 x. 6 ) = ; 1 2
88 20 1 39 82 20 1 85 87 decmul2c 
 |-  ( 2 x. ; 1 6 ) = ; 3 2
89 3nn0 
 |-  3 e. NN0
90 89 20 deccl 
 |-  ; 3 2 e. NN0
91 90 nn0cni 
 |-  ; 3 2 e. CC
92 1 39 deccl 
 |-  ; 1 6 e. NN0
93 92 nn0cni 
 |-  ; 1 6 e. CC
94 2ne0 
 |-  2 =/= 0
95 91 45 93 94 divmuli 
 |-  ( ( ; 3 2 / 2 ) = ; 1 6 <-> ( 2 x. ; 1 6 ) = ; 3 2 )
96 88 95 mpbir 
 |-  ( ; 3 2 / 2 ) = ; 1 6
97 40 nn0cni 
 |-  4 e. CC
98 97 sqvali 
 |-  ( 4 ^ 2 ) = ( 4 x. 4 )
99 4t4e16 
 |-  ( 4 x. 4 ) = ; 1 6
100 98 99 eqtr2i 
 |-  ; 1 6 = ( 4 ^ 2 )
101 81 96 100 3eqtri 
 |-  ( ( ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) + ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) / 2 ) = ( 4 ^ 2 )
102 101 fveq2i 
 |-  ( sqrt ` ( ( ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) + ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) / 2 ) ) = ( sqrt ` ( 4 ^ 2 ) )
103 40 nn0ge0i 
 |-  0 <_ 4
104 40 nn0rei 
 |-  4 e. RR
105 104 sqrtsqi 
 |-  ( 0 <_ 4 -> ( sqrt ` ( 4 ^ 2 ) ) = 4 )
106 103 105 ax-mp 
 |-  ( sqrt ` ( 4 ^ 2 ) ) = 4
107 10 102 106 3eqtri 
 |-  ( Re ` ( sqrt ` ( ; 1 5 + ( _i x. 8 ) ) ) ) = 4