Metamath Proof Explorer


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