Metamath Proof Explorer


Theorem resqrtvalex

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

Ref Expression
Assertion resqrtvalex ( ℜ ‘ ( √ ‘ ( 1 5 + ( i · 8 ) ) ) ) = 4

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 resqrtval ( ( 1 5 + ( i · 8 ) ) ∈ ℂ → ( ℜ ‘ ( √ ‘ ( 1 5 + ( i · 8 ) ) ) ) = ( √ ‘ ( ( ( abs ‘ ( 1 5 + ( i · 8 ) ) ) + ( ℜ ‘ ( 1 5 + ( i · 8 ) ) ) ) / 2 ) ) )
10 8 9 ax-mp ( ℜ ‘ ( √ ‘ ( 1 5 + ( i · 8 ) ) ) ) = ( √ ‘ ( ( ( abs ‘ ( 1 5 + ( i · 8 ) ) ) + ( ℜ ‘ ( 1 5 + ( i · 8 ) ) ) ) / 2 ) )
11 7nn0 7 ∈ ℕ0
12 3 nn0rei 1 5 ∈ ℝ
13 8re 8 ∈ ℝ
14 absreim ( ( 1 5 ∈ ℝ ∧ 8 ∈ ℝ ) → ( abs ‘ ( 1 5 + ( i · 8 ) ) ) = ( √ ‘ ( ( 1 5 ↑ 2 ) + ( 8 ↑ 2 ) ) ) )
15 12 13 14 mp2an ( abs ‘ ( 1 5 + ( i · 8 ) ) ) = ( √ ‘ ( ( 1 5 ↑ 2 ) + ( 8 ↑ 2 ) ) )
16 4 sqvali ( 1 5 ↑ 2 ) = ( 1 5 · 1 5 )
17 eqid 1 5 = 1 5
18 4 mulid2i ( 1 · 1 5 ) = 1 5
19 1p1e2 ( 1 + 1 ) = 2
20 2nn0 2 ∈ ℕ0
21 11 nn0cni 7 ∈ ℂ
22 2 nn0cni 5 ∈ ℂ
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 · 1 5 ) + 7 ) = 2 2
26 22 mulid1i ( 5 · 1 ) = 5
27 26 oveq1i ( ( 5 · 1 ) + 2 ) = ( 5 + 2 )
28 5p2e7 ( 5 + 2 ) = 7
29 27 28 eqtri ( ( 5 · 1 ) + 2 ) = 7
30 5t5e25 ( 5 · 5 ) = 2 5
31 2 1 2 17 2 20 29 30 decmul2c ( 5 · 1 5 ) = 7 5
32 3 1 2 17 2 11 25 31 decmul1c ( 1 5 · 1 5 ) = 2 2 5
33 16 32 eqtri ( 1 5 ↑ 2 ) = 2 2 5
34 6 sqvali ( 8 ↑ 2 ) = ( 8 · 8 )
35 8t8e64 ( 8 · 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 ∈ ℕ0
39 6nn0 6 ∈ ℕ0
40 4nn0 4 ∈ ℕ0
41 eqid 2 2 5 = 2 2 5
42 eqid 6 4 = 6 4
43 eqid 2 2 = 2 2
44 39 nn0cni 6 ∈ ℂ
45 2cn 2 ∈ ℂ
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 ∈ ℕ0
52 51 nn0cni 1 7 ∈ ℂ
53 52 sqvali ( 1 7 ↑ 2 ) = ( 1 7 · 1 7 )
54 eqid 1 7 = 1 7
55 9nn0 9 ∈ ℕ0
56 1 1 deccl 1 1 ∈ ℕ0
57 52 mulid2i ( 1 · 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 · 1 7 ) + 1 1 ) = 2 8
61 21 mulid1i ( 7 · 1 ) = 7
62 61 oveq1i ( ( 7 · 1 ) + 4 ) = ( 7 + 4 )
63 7p4e11 ( 7 + 4 ) = 1 1
64 62 63 eqtri ( ( 7 · 1 ) + 4 ) = 1 1
65 7t7e49 ( 7 · 7 ) = 4 9
66 11 1 11 54 55 40 64 65 decmul2c ( 7 · 1 7 ) = 1 1 9
67 51 1 11 54 55 56 60 66 decmul1c ( 1 7 · 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 ( √ ‘ ( ( 1 5 ↑ 2 ) + ( 8 ↑ 2 ) ) ) = ( √ ‘ ( 1 7 ↑ 2 ) )
71 51 nn0ge0i 0 ≤ 1 7
72 51 nn0rei 1 7 ∈ ℝ
73 72 sqrtsqi ( 0 ≤ 1 7 → ( √ ‘ ( 1 7 ↑ 2 ) ) = 1 7 )
74 71 73 ax-mp ( √ ‘ ( 1 7 ↑ 2 ) ) = 1 7
75 15 70 74 3eqtri ( abs ‘ ( 1 5 + ( i · 8 ) ) ) = 1 7
76 12 13 crrei ( ℜ ‘ ( 1 5 + ( i · 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 · 8 ) ) ) + ( ℜ ‘ ( 1 5 + ( i · 8 ) ) ) ) = 3 2
81 80 oveq1i ( ( ( abs ‘ ( 1 5 + ( i · 8 ) ) ) + ( ℜ ‘ ( 1 5 + ( i · 8 ) ) ) ) / 2 ) = ( 3 2 / 2 )
82 eqid 1 6 = 1 6
83 45 mulid1i ( 2 · 1 ) = 2
84 83 oveq1i ( ( 2 · 1 ) + 1 ) = ( 2 + 1 )
85 84 78 eqtri ( ( 2 · 1 ) + 1 ) = 3
86 6t2e12 ( 6 · 2 ) = 1 2
87 44 45 86 mulcomli ( 2 · 6 ) = 1 2
88 20 1 39 82 20 1 85 87 decmul2c ( 2 · 1 6 ) = 3 2
89 3nn0 3 ∈ ℕ0
90 89 20 deccl 3 2 ∈ ℕ0
91 90 nn0cni 3 2 ∈ ℂ
92 1 39 deccl 1 6 ∈ ℕ0
93 92 nn0cni 1 6 ∈ ℂ
94 2ne0 2 ≠ 0
95 91 45 93 94 divmuli ( ( 3 2 / 2 ) = 1 6 ↔ ( 2 · 1 6 ) = 3 2 )
96 88 95 mpbir ( 3 2 / 2 ) = 1 6
97 40 nn0cni 4 ∈ ℂ
98 97 sqvali ( 4 ↑ 2 ) = ( 4 · 4 )
99 4t4e16 ( 4 · 4 ) = 1 6
100 98 99 eqtr2i 1 6 = ( 4 ↑ 2 )
101 81 96 100 3eqtri ( ( ( abs ‘ ( 1 5 + ( i · 8 ) ) ) + ( ℜ ‘ ( 1 5 + ( i · 8 ) ) ) ) / 2 ) = ( 4 ↑ 2 )
102 101 fveq2i ( √ ‘ ( ( ( abs ‘ ( 1 5 + ( i · 8 ) ) ) + ( ℜ ‘ ( 1 5 + ( i · 8 ) ) ) ) / 2 ) ) = ( √ ‘ ( 4 ↑ 2 ) )
103 40 nn0ge0i 0 ≤ 4
104 40 nn0rei 4 ∈ ℝ
105 104 sqrtsqi ( 0 ≤ 4 → ( √ ‘ ( 4 ↑ 2 ) ) = 4 )
106 103 105 ax-mp ( √ ‘ ( 4 ↑ 2 ) ) = 4
107 10 102 106 3eqtri ( ℜ ‘ ( √ ‘ ( 1 5 + ( i · 8 ) ) ) ) = 4