Metamath Proof Explorer


Theorem imsqrtvalex

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

Ref Expression
Assertion imsqrtvalex 15 + i 8 = 1

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 imsqrtval 15 + i 8 15 + i 8 = if 15 + i 8 < 0 1 1 15 + i 8 15 + i 8 2
10 8 9 ax-mp 15 + i 8 = if 15 + i 8 < 0 1 1 15 + i 8 15 + i 8 2
11 8pos 0 < 8
12 0re 0
13 8re 8
14 12 13 ltnsymi 0 < 8 ¬ 8 < 0
15 3 nn0rei 15
16 15 13 crimi 15 + i 8 = 8
17 16 breq1i 15 + i 8 < 0 8 < 0
18 14 17 sylnibr 0 < 8 ¬ 15 + i 8 < 0
19 11 18 ax-mp ¬ 15 + i 8 < 0
20 19 iffalsei if 15 + i 8 < 0 1 1 = 1
21 absreim 15 8 15 + i 8 = 15 2 + 8 2
22 15 13 21 mp2an 15 + i 8 = 15 2 + 8 2
23 4 sqvali 15 2 = 15 15
24 eqid 15 = 15
25 7nn0 7 0
26 4 mulid2i 1 15 = 15
27 1p1e2 1 + 1 = 2
28 2nn0 2 0
29 25 nn0cni 7
30 2 nn0cni 5
31 7p5e12 7 + 5 = 12
32 29 30 31 addcomli 5 + 7 = 12
33 1 2 25 26 27 28 32 decaddci 1 15 + 7 = 22
34 30 mulid1i 5 1 = 5
35 34 oveq1i 5 1 + 2 = 5 + 2
36 5p2e7 5 + 2 = 7
37 35 36 eqtri 5 1 + 2 = 7
38 5t5e25 5 5 = 25
39 2 1 2 24 2 28 37 38 decmul2c 5 15 = 75
40 3 1 2 24 2 25 33 39 decmul1c 15 15 = 225
41 23 40 eqtri 15 2 = 225
42 6 sqvali 8 2 = 8 8
43 8t8e64 8 8 = 64
44 42 43 eqtri 8 2 = 64
45 41 44 oveq12i 15 2 + 8 2 = 225 + 64
46 28 28 deccl 22 0
47 6nn0 6 0
48 4nn0 4 0
49 eqid 225 = 225
50 eqid 64 = 64
51 eqid 22 = 22
52 47 nn0cni 6
53 28 nn0cni 2
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 0
60 59 nn0cni 17
61 60 sqvali 17 2 = 17 17
62 eqid 17 = 17
63 9nn0 9 0
64 1 1 deccl 11 0
65 60 mulid2i 1 17 = 17
66 eqid 11 = 11
67 7p1e8 7 + 1 = 8
68 1 25 1 1 65 66 27 67 decadd 1 17 + 11 = 28
69 29 mulid1i 7 1 = 7
70 69 oveq1i 7 1 + 4 = 7 + 4
71 7p4e11 7 + 4 = 11
72 70 71 eqtri 7 1 + 4 = 11
73 7t7e49 7 7 = 49
74 25 1 25 62 63 48 72 73 decmul2c 7 17 = 119
75 59 1 25 62 63 64 68 74 decmul1c 17 17 = 289
76 61 75 eqtr2i 289 = 17 2
77 45 58 76 3eqtri 15 2 + 8 2 = 17 2
78 77 fveq2i 15 2 + 8 2 = 17 2
79 59 nn0ge0i 0 17
80 59 nn0rei 17
81 80 sqrtsqi 0 17 17 2 = 17
82 79 81 ax-mp 17 2 = 17
83 22 78 82 3eqtri 15 + i 8 = 17
84 15 13 crrei 15 + i 8 = 15
85 83 84 oveq12i 15 + i 8 15 + i 8 = 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 15 + i 8 15 + i 8 = 2
89 88 oveq1i 15 + i 8 15 + i 8 2 = 2 2
90 2div2e1 2 2 = 1
91 89 90 eqtri 15 + i 8 15 + i 8 2 = 1
92 91 fveq2i 15 + i 8 15 + i 8 2 = 1
93 sqrt1 1 = 1
94 92 93 eqtri 15 + i 8 15 + i 8 2 = 1
95 20 94 oveq12i if 15 + i 8 < 0 1 1 15 + i 8 15 + i 8 2 = 1 1
96 1t1e1 1 1 = 1
97 10 95 96 3eqtri 15 + i 8 = 1