Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Short Studies
Additions for square root; absolute value
resqrtvalex
Next ⟩
imsqrtvalex
Metamath Proof Explorer
Ascii
Unicode
Theorem
resqrtvalex
Description:
Example for
resqrtval
.
(Contributed by
RP
, 21-May-2024)
Ref
Expression
Assertion
resqrtvalex
⊢
ℜ
⁡
15
+
i
⋅
8
=
4
Proof
Step
Hyp
Ref
Expression
1
1nn0
⊢
1
∈
ℕ
0
2
5nn0
⊢
5
∈
ℕ
0
3
1
2
deccl
⊢
15
∈
ℕ
0
4
3
nn0cni
⊢
15
∈
ℂ
5
ax-icn
⊢
i
∈
ℂ
6
8cn
⊢
8
∈
ℂ
7
5
6
mulcli
⊢
i
⋅
8
∈
ℂ
8
4
7
addcli
⊢
15
+
i
⋅
8
∈
ℂ
9
resqrtval
⊢
15
+
i
⋅
8
∈
ℂ
→
ℜ
⁡
15
+
i
⋅
8
=
15
+
i
⋅
8
+
ℜ
⁡
15
+
i
⋅
8
2
10
8
9
ax-mp
⊢
ℜ
⁡
15
+
i
⋅
8
=
15
+
i
⋅
8
+
ℜ
⁡
15
+
i
⋅
8
2
11
7nn0
⊢
7
∈
ℕ
0
12
3
nn0rei
⊢
15
∈
ℝ
13
8re
⊢
8
∈
ℝ
14
absreim
⊢
15
∈
ℝ
∧
8
∈
ℝ
→
15
+
i
⋅
8
=
15
2
+
8
2
15
12
13
14
mp2an
⊢
15
+
i
⋅
8
=
15
2
+
8
2
16
4
sqvali
⊢
15
2
=
15
⋅
15
17
eqid
⊢
15
=
15
18
4
mulid2i
⊢
1
⋅
15
=
15
19
1p1e2
⊢
1
+
1
=
2
20
2nn0
⊢
2
∈
ℕ
0
21
11
nn0cni
⊢
7
∈
ℂ
22
2
nn0cni
⊢
5
∈
ℂ
23
7p5e12
⊢
7
+
5
=
12
24
21
22
23
addcomli
⊢
5
+
7
=
12
25
1
2
11
18
19
20
24
decaddci
⊢
1
⋅
15
+
7
=
22
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
=
25
31
2
1
2
17
2
20
29
30
decmul2c
⊢
5
⋅
15
=
75
32
3
1
2
17
2
11
25
31
decmul1c
⊢
15
⋅
15
=
225
33
16
32
eqtri
⊢
15
2
=
225
34
6
sqvali
⊢
8
2
=
8
⋅
8
35
8t8e64
⊢
8
⋅
8
=
64
36
34
35
eqtri
⊢
8
2
=
64
37
33
36
oveq12i
⊢
15
2
+
8
2
=
225
+
64
38
20
20
deccl
⊢
22
∈
ℕ
0
39
6nn0
⊢
6
∈
ℕ
0
40
4nn0
⊢
4
∈
ℕ
0
41
eqid
⊢
225
=
225
42
eqid
⊢
64
=
64
43
eqid
⊢
22
=
22
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
⊢
22
+
6
=
28
49
5p4e9
⊢
5
+
4
=
9
50
38
2
39
40
41
42
48
49
decadd
⊢
225
+
64
=
289
51
1
11
deccl
⊢
17
∈
ℕ
0
52
51
nn0cni
⊢
17
∈
ℂ
53
52
sqvali
⊢
17
2
=
17
⋅
17
54
eqid
⊢
17
=
17
55
9nn0
⊢
9
∈
ℕ
0
56
1
1
deccl
⊢
11
∈
ℕ
0
57
52
mulid2i
⊢
1
⋅
17
=
17
58
eqid
⊢
11
=
11
59
7p1e8
⊢
7
+
1
=
8
60
1
11
1
1
57
58
19
59
decadd
⊢
1
⋅
17
+
11
=
28
61
21
mulid1i
⊢
7
⋅
1
=
7
62
61
oveq1i
⊢
7
⋅
1
+
4
=
7
+
4
63
7p4e11
⊢
7
+
4
=
11
64
62
63
eqtri
⊢
7
⋅
1
+
4
=
11
65
7t7e49
⊢
7
⋅
7
=
49
66
11
1
11
54
55
40
64
65
decmul2c
⊢
7
⋅
17
=
119
67
51
1
11
54
55
56
60
66
decmul1c
⊢
17
⋅
17
=
289
68
53
67
eqtr2i
⊢
289
=
17
2
69
37
50
68
3eqtri
⊢
15
2
+
8
2
=
17
2
70
69
fveq2i
⊢
15
2
+
8
2
=
17
2
71
51
nn0ge0i
⊢
0
≤
17
72
51
nn0rei
⊢
17
∈
ℝ
73
72
sqrtsqi
⊢
0
≤
17
→
17
2
=
17
74
71
73
ax-mp
⊢
17
2
=
17
75
15
70
74
3eqtri
⊢
15
+
i
⋅
8
=
17
76
12
13
crrei
⊢
ℜ
⁡
15
+
i
⋅
8
=
15
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
⊢
15
+
i
⋅
8
+
ℜ
⁡
15
+
i
⋅
8
=
32
81
80
oveq1i
⊢
15
+
i
⋅
8
+
ℜ
⁡
15
+
i
⋅
8
2
=
32
2
82
eqid
⊢
16
=
16
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
=
12
87
44
45
86
mulcomli
⊢
2
⋅
6
=
12
88
20
1
39
82
20
1
85
87
decmul2c
⊢
2
⋅
16
=
32
89
3nn0
⊢
3
∈
ℕ
0
90
89
20
deccl
⊢
32
∈
ℕ
0
91
90
nn0cni
⊢
32
∈
ℂ
92
1
39
deccl
⊢
16
∈
ℕ
0
93
92
nn0cni
⊢
16
∈
ℂ
94
2ne0
⊢
2
≠
0
95
91
45
93
94
divmuli
⊢
32
2
=
16
↔
2
⋅
16
=
32
96
88
95
mpbir
⊢
32
2
=
16
97
40
nn0cni
⊢
4
∈
ℂ
98
97
sqvali
⊢
4
2
=
4
⋅
4
99
4t4e16
⊢
4
⋅
4
=
16
100
98
99
eqtr2i
⊢
16
=
4
2
101
81
96
100
3eqtri
⊢
15
+
i
⋅
8
+
ℜ
⁡
15
+
i
⋅
8
2
=
4
2
102
101
fveq2i
⊢
15
+
i
⋅
8
+
ℜ
⁡
15
+
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
⊢
ℜ
⁡
15
+
i
⋅
8
=
4