Theorem resqrtvalex

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

	Ref	Expression
Assertion	resqrtvalex	$$⊢\Re \left(\sqrt{15+\mathrm{i}\cdot 8}\right)=4$$

Proof

Step	Hyp	Ref	Expression
1		1nn0	$$⊢1\in {\mathbb{N}}_0$$
2		5nn0	$$⊢5\in {\mathbb{N}}_0$$
3	1 2	deccl	$$⊢15\in {\mathbb{N}}_0$$
4	3	nn0cni	$$⊢15\in ℂ$$
5		ax-icn	$$⊢\mathrm{i}\in ℂ$$
6		8cn	$$⊢8\in ℂ$$
7	5 6	mulcli	$$⊢\mathrm{i}\cdot 8\in ℂ$$
8	4 7	addcli	$$⊢15+\mathrm{i}\cdot 8\in ℂ$$
9		resqrtval	$$⊢15+\mathrm{i}\cdot 8\in ℂ\to \Re \left(\sqrt{15+\mathrm{i}\cdot 8}\right)=\sqrt{\frac{\left|15+\mathrm{i}\cdot 8\right|+\Re \left(15+\mathrm{i}\cdot 8\right)}{2}}$$
10	8 9	ax-mp	$$⊢\Re \left(\sqrt{15+\mathrm{i}\cdot 8}\right)=\sqrt{\frac{\left|15+\mathrm{i}\cdot 8\right|+\Re \left(15+\mathrm{i}\cdot 8\right)}{2}}$$
11		7nn0	$$⊢7\in {\mathbb{N}}_0$$
12	3	nn0rei	$$⊢15\in ℝ$$
13		8re	$$⊢8\in ℝ$$
14		absreim	$$⊢\left(15\in ℝ\wedge 8\in ℝ\right)\to \left|15+\mathrm{i}\cdot 8\right|=\sqrt{{15}^2+8^2}$$
15	12 13 14	mp2an	$$⊢\left|15+\mathrm{i}\cdot 8\right|=\sqrt{{15}^2+8^2}$$
16	4	sqvali	$$⊢{15}^2=15\cdot 15$$
17		eqid	$$⊢15=15$$
18	4	mullidi	$$⊢1\cdot 15=15$$
19		1p1e2	$$⊢1+1=2$$
20		2nn0	$$⊢2\in {\mathbb{N}}_0$$
21	11	nn0cni	$$⊢7\in ℂ$$
22	2	nn0cni	$$⊢5\in ℂ$$
23		7p5e12	$$⊢7+5=12$$
24	21 22 23	addcomli	$$⊢5+7=12$$
25	1 2 11 18 19 20 24	decaddci	$$⊢1\cdot 15+7=22$$
26	22	mulridi	$$⊢5\cdot 1=5$$
27	26	oveq1i	$$⊢5\cdot 1+2=5+2$$
28		5p2e7	$$⊢5+2=7$$
29	27 28	eqtri	$$⊢5\cdot 1+2=7$$
30		5t5e25	$$⊢5\cdot 5=25$$
31	2 1 2 17 2 20 29 30	decmul2c	$$⊢5\cdot 15=75$$
32	3 1 2 17 2 11 25 31	decmul1c	$$⊢15\cdot 15=225$$
33	16 32	eqtri	$$⊢{15}^2=225$$
34	6	sqvali	$$⊢8^2=8\cdot 8$$
35		8t8e64	$$⊢8\cdot 8=64$$
36	34 35	eqtri	$$⊢8^2=64$$
37	33 36	oveq12i	$$⊢{15}^2+8^2=225+64$$
38	20 20	deccl	$$⊢22\in {\mathbb{N}}_0$$
39		6nn0	$$⊢6\in {\mathbb{N}}_0$$
40		4nn0	$$⊢4\in {\mathbb{N}}_0$$
41		eqid	$$⊢225=225$$
42		eqid	$$⊢64=64$$
43		eqid	$$⊢22=22$$
44	39	nn0cni	$$⊢6\in ℂ$$
45		2cn	$$⊢2\in ℂ$$
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\in {\mathbb{N}}_0$$
52	51	nn0cni	$$⊢17\in ℂ$$
53	52	sqvali	$$⊢{17}^2=17\cdot 17$$
54		eqid	$$⊢17=17$$
55		9nn0	$$⊢9\in {\mathbb{N}}_0$$
56	1 1	deccl	$$⊢11\in {\mathbb{N}}_0$$
57	52	mullidi	$$⊢1\cdot 17=17$$
58		eqid	$$⊢11=11$$
59		7p1e8	$$⊢7+1=8$$
60	1 11 1 1 57 58 19 59	decadd	$$⊢1\cdot 17+11=28$$
61	21	mulridi	$$⊢7\cdot 1=7$$
62	61	oveq1i	$$⊢7\cdot 1+4=7+4$$
63		7p4e11	$$⊢7+4=11$$
64	62 63	eqtri	$$⊢7\cdot 1+4=11$$
65		7t7e49	$$⊢7\cdot 7=49$$
66	11 1 11 54 55 40 64 65	decmul2c	$$⊢7\cdot 17=119$$
67	51 1 11 54 55 56 60 66	decmul1c	$$⊢17\cdot 17=289$$
68	53 67	eqtr2i	$$⊢289={17}^2$$
69	37 50 68	3eqtri	$$⊢{15}^2+8^2={17}^2$$
70	69	fveq2i	$$⊢\sqrt{{15}^2+8^2}=\sqrt{{17}^2}$$
71	51	nn0ge0i	$$⊢0\le 17$$
72	51	nn0rei	$$⊢17\in ℝ$$
73	72	sqrtsqi	$$⊢0\le 17\to \sqrt{{17}^2}=17$$
74	71 73	ax-mp	$$⊢\sqrt{{17}^2}=17$$
75	15 70 74	3eqtri	$$⊢\left|15+\mathrm{i}\cdot 8\right|=17$$
76	12 13	crrei	$$⊢\Re \left(15+\mathrm{i}\cdot 8\right)=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	$$⊢\left|15+\mathrm{i}\cdot 8\right|+\Re \left(15+\mathrm{i}\cdot 8\right)=32$$
81	80	oveq1i	$$⊢\frac{\left|15+\mathrm{i}\cdot 8\right|+\Re \left(15+\mathrm{i}\cdot 8\right)}{2}=\frac{32}{2}$$
82		eqid	$$⊢16=16$$
83	45	mulridi	$$⊢2\cdot 1=2$$
84	83	oveq1i	$$⊢2\cdot 1+1=2+1$$
85	84 78	eqtri	$$⊢2\cdot 1+1=3$$
86		6t2e12	$$⊢6\cdot 2=12$$
87	44 45 86	mulcomli	$$⊢2\cdot 6=12$$
88	20 1 39 82 20 1 85 87	decmul2c	$$⊢2\cdot 16=32$$
89		3nn0	$$⊢3\in {\mathbb{N}}_0$$
90	89 20	deccl	$$⊢32\in {\mathbb{N}}_0$$
91	90	nn0cni	$$⊢32\in ℂ$$
92	1 39	deccl	$$⊢16\in {\mathbb{N}}_0$$
93	92	nn0cni	$$⊢16\in ℂ$$
94		2ne0	$$⊢2\ne 0$$
95	91 45 93 94	divmuli	$$⊢\frac{32}{2}=16\leftrightarrow 2\cdot 16=32$$
96	88 95	mpbir	$$⊢\frac{32}{2}=16$$
97	40	nn0cni	$$⊢4\in ℂ$$
98	97	sqvali	$$⊢4^2=4\cdot 4$$
99		4t4e16	$$⊢4\cdot 4=16$$
100	98 99	eqtr2i	$$⊢16=4^2$$
101	81 96 100	3eqtri	$$⊢\frac{\left|15+\mathrm{i}\cdot 8\right|+\Re \left(15+\mathrm{i}\cdot 8\right)}{2}=4^2$$
102	101	fveq2i	$$⊢\sqrt{\frac{\left|15+\mathrm{i}\cdot 8\right|+\Re \left(15+\mathrm{i}\cdot 8\right)}{2}}=\sqrt{4^2}$$
103	40	nn0ge0i	$$⊢0\le 4$$
104	40	nn0rei	$$⊢4\in ℝ$$
105	104	sqrtsqi	$$⊢0\le 4\to \sqrt{4^2}=4$$
106	103 105	ax-mp	$$⊢\sqrt{4^2}=4$$
107	10 102 106	3eqtri	$$⊢\Re \left(\sqrt{15+\mathrm{i}\cdot 8}\right)=4$$