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