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 mullidi ⊢ ( 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 mulridi ⊢ ( 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 mullidi ⊢ ( 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 mulridi ⊢ ( 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 mulridi ⊢ ( 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