Theorem imsqrtvalex

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

	Ref	Expression
Assertion	imsqrtvalex	$$⊢\Im \left(\sqrt{15+\mathrm{i}\cdot 8}\right)=1$$

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		imsqrtval	$$⊢15+\mathrm{i}\cdot 8\in ℂ\to \Im \left(\sqrt{15+\mathrm{i}\cdot 8}\right)=if\left(\Im \left(15+\mathrm{i}\cdot 8\right)<0,-1,1\right)\sqrt{\frac{\left|15+\mathrm{i}\cdot 8\right|-\Re \left(15+\mathrm{i}\cdot 8\right)}{2}}$$
10	8 9	ax-mp	$$⊢\Im \left(\sqrt{15+\mathrm{i}\cdot 8}\right)=if\left(\Im \left(15+\mathrm{i}\cdot 8\right)<0,-1,1\right)\sqrt{\frac{\left|15+\mathrm{i}\cdot 8\right|-\Re \left(15+\mathrm{i}\cdot 8\right)}{2}}$$
11		8pos	$$⊢0<8$$
12		0re	$$⊢0\in ℝ$$
13		8re	$$⊢8\in ℝ$$
14	12 13	ltnsymi	$$⊢0<8\to \neg 8<0$$
15	3	nn0rei	$$⊢15\in ℝ$$
16	15 13	crimi	$$⊢\Im \left(15+\mathrm{i}\cdot 8\right)=8$$
17	16	breq1i	$$⊢\Im \left(15+\mathrm{i}\cdot 8\right)<0\leftrightarrow 8<0$$
18	14 17	sylnibr	$$⊢0<8\to \neg \Im \left(15+\mathrm{i}\cdot 8\right)<0$$
19	11 18	ax-mp	$$⊢\neg \Im \left(15+\mathrm{i}\cdot 8\right)<0$$
20	19	iffalsei	$$⊢if\left(\Im \left(15+\mathrm{i}\cdot 8\right)<0,-1,1\right)=1$$
21		absreim	$$⊢\left(15\in ℝ\wedge 8\in ℝ\right)\to \left|15+\mathrm{i}\cdot 8\right|=\sqrt{{15}^2+8^2}$$
22	15 13 21	mp2an	$$⊢\left|15+\mathrm{i}\cdot 8\right|=\sqrt{{15}^2+8^2}$$
23	4	sqvali	$$⊢{15}^2=15\cdot 15$$
24		eqid	$$⊢15=15$$
25		7nn0	$$⊢7\in {\mathbb{N}}_0$$
26	4	mulid2i	$$⊢1\cdot 15=15$$
27		1p1e2	$$⊢1+1=2$$
28		2nn0	$$⊢2\in {\mathbb{N}}_0$$
29	25	nn0cni	$$⊢7\in ℂ$$
30	2	nn0cni	$$⊢5\in ℂ$$
31		7p5e12	$$⊢7+5=12$$
32	29 30 31	addcomli	$$⊢5+7=12$$
33	1 2 25 26 27 28 32	decaddci	$$⊢1\cdot 15+7=22$$
34	30	mulid1i	$$⊢5\cdot 1=5$$
35	34	oveq1i	$$⊢5\cdot 1+2=5+2$$
36		5p2e7	$$⊢5+2=7$$
37	35 36	eqtri	$$⊢5\cdot 1+2=7$$
38		5t5e25	$$⊢5\cdot 5=25$$
39	2 1 2 24 2 28 37 38	decmul2c	$$⊢5\cdot 15=75$$
40	3 1 2 24 2 25 33 39	decmul1c	$$⊢15\cdot 15=225$$
41	23 40	eqtri	$$⊢{15}^2=225$$
42	6	sqvali	$$⊢8^2=8\cdot 8$$
43		8t8e64	$$⊢8\cdot 8=64$$
44	42 43	eqtri	$$⊢8^2=64$$
45	41 44	oveq12i	$$⊢{15}^2+8^2=225+64$$
46	28 28	deccl	$$⊢22\in {\mathbb{N}}_0$$
47		6nn0	$$⊢6\in {\mathbb{N}}_0$$
48		4nn0	$$⊢4\in {\mathbb{N}}_0$$
49		eqid	$$⊢225=225$$
50		eqid	$$⊢64=64$$
51		eqid	$$⊢22=22$$
52	47	nn0cni	$$⊢6\in ℂ$$
53	28	nn0cni	$$⊢2\in ℂ$$
54		6p2e8	$$⊢6+2=8$$
55	52 53 54	addcomli	$$⊢2+6=8$$
56	28 28 47 51 55	decaddi	$$⊢22+6=28$$
57		5p4e9	$$⊢5+4=9$$
58	46 2 47 48 49 50 56 57	decadd	$$⊢225+64=289$$
59	1 25	deccl	$$⊢17\in {\mathbb{N}}_0$$
60	59	nn0cni	$$⊢17\in ℂ$$
61	60	sqvali	$$⊢{17}^2=17\cdot 17$$
62		eqid	$$⊢17=17$$
63		9nn0	$$⊢9\in {\mathbb{N}}_0$$
64	1 1	deccl	$$⊢11\in {\mathbb{N}}_0$$
65	60	mulid2i	$$⊢1\cdot 17=17$$
66		eqid	$$⊢11=11$$
67		7p1e8	$$⊢7+1=8$$
68	1 25 1 1 65 66 27 67	decadd	$$⊢1\cdot 17+11=28$$
69	29	mulid1i	$$⊢7\cdot 1=7$$
70	69	oveq1i	$$⊢7\cdot 1+4=7+4$$
71		7p4e11	$$⊢7+4=11$$
72	70 71	eqtri	$$⊢7\cdot 1+4=11$$
73		7t7e49	$$⊢7\cdot 7=49$$
74	25 1 25 62 63 48 72 73	decmul2c	$$⊢7\cdot 17=119$$
75	59 1 25 62 63 64 68 74	decmul1c	$$⊢17\cdot 17=289$$
76	61 75	eqtr2i	$$⊢289={17}^2$$
77	45 58 76	3eqtri	$$⊢{15}^2+8^2={17}^2$$
78	77	fveq2i	$$⊢\sqrt{{15}^2+8^2}=\sqrt{{17}^2}$$
79	59	nn0ge0i	$$⊢0\le 17$$
80	59	nn0rei	$$⊢17\in ℝ$$
81	80	sqrtsqi	$$⊢0\le 17\to \sqrt{{17}^2}=17$$
82	79 81	ax-mp	$$⊢\sqrt{{17}^2}=17$$
83	22 78 82	3eqtri	$$⊢\left|15+\mathrm{i}\cdot 8\right|=17$$
84	15 13	crrei	$$⊢\Re \left(15+\mathrm{i}\cdot 8\right)=15$$
85	83 84	oveq12i	$$⊢\left|15+\mathrm{i}\cdot 8\right|-\Re \left(15+\mathrm{i}\cdot 8\right)=17-15$$
86	1 2 28 24 36	decaddi	$$⊢15+2=17$$
87	60 4 53 86	subaddrii	$$⊢17-15=2$$
88	85 87	eqtri	$$⊢\left|15+\mathrm{i}\cdot 8\right|-\Re \left(15+\mathrm{i}\cdot 8\right)=2$$
89	88	oveq1i	$$⊢\frac{\left|15+\mathrm{i}\cdot 8\right|-\Re \left(15+\mathrm{i}\cdot 8\right)}{2}=\frac{2}{2}$$
90		2div2e1	$$⊢\frac{2}{2}=1$$
91	89 90	eqtri	$$⊢\frac{\left|15+\mathrm{i}\cdot 8\right|-\Re \left(15+\mathrm{i}\cdot 8\right)}{2}=1$$
92	91	fveq2i	$$⊢\sqrt{\frac{\left|15+\mathrm{i}\cdot 8\right|-\Re \left(15+\mathrm{i}\cdot 8\right)}{2}}=\sqrt{1}$$
93		sqrt1	$$⊢\sqrt{1}=1$$
94	92 93	eqtri	$$⊢\sqrt{\frac{\left|15+\mathrm{i}\cdot 8\right|-\Re \left(15+\mathrm{i}\cdot 8\right)}{2}}=1$$
95	20 94	oveq12i	$$⊢if\left(\Im \left(15+\mathrm{i}\cdot 8\right)<0,-1,1\right)\sqrt{\frac{\left|15+\mathrm{i}\cdot 8\right|-\Re \left(15+\mathrm{i}\cdot 8\right)}{2}}=1\cdot 1$$
96		1t1e1	$$⊢1\cdot 1=1$$
97	10 95 96	3eqtri	$$⊢\Im \left(\sqrt{15+\mathrm{i}\cdot 8}\right)=1$$