Proof of Theorem resqrtvalex
Step | Hyp | Ref
| Expression |
1 | | 1nn0 11935 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
2 | | 5nn0 11939 |
. . . . . 6
⊢ 5 ∈
ℕ0 |
3 | 1, 2 | deccl 12137 |
. . . . 5
⊢ ;15 ∈
ℕ0 |
4 | 3 | nn0cni 11931 |
. . . 4
⊢ ;15 ∈ ℂ |
5 | | ax-icn 10619 |
. . . . 5
⊢ i ∈
ℂ |
6 | | 8cn 11756 |
. . . . 5
⊢ 8 ∈
ℂ |
7 | 5, 6 | mulcli 10671 |
. . . 4
⊢ (i
· 8) ∈ ℂ |
8 | 4, 7 | addcli 10670 |
. . 3
⊢ (;15 + (i · 8)) ∈
ℂ |
9 | | resqrtval 40701 |
. . 3
⊢ ((;15 + (i · 8)) ∈ ℂ
→ (ℜ‘(√‘(;15 + (i · 8)))) =
(√‘(((abs‘(;15 +
(i · 8))) + (ℜ‘(;15 + (i · 8)))) / 2))) |
10 | 8, 9 | ax-mp 5 |
. 2
⊢
(ℜ‘(√‘(;15 + (i · 8)))) =
(√‘(((abs‘(;15 +
(i · 8))) + (ℜ‘(;15 + (i · 8)))) / 2)) |
11 | | 7nn0 11941 |
. . . . . 6
⊢ 7 ∈
ℕ0 |
12 | 3 | nn0rei 11930 |
. . . . . . . 8
⊢ ;15 ∈ ℝ |
13 | | 8re 11755 |
. . . . . . . 8
⊢ 8 ∈
ℝ |
14 | | absreim 14686 |
. . . . . . . 8
⊢ ((;15 ∈ ℝ ∧ 8 ∈
ℝ) → (abs‘(;15 +
(i · 8))) = (√‘((;15↑2) + (8↑2)))) |
15 | 12, 13, 14 | mp2an 692 |
. . . . . . 7
⊢
(abs‘(;15 + (i
· 8))) = (√‘((;15↑2) + (8↑2))) |
16 | 4 | sqvali 13578 |
. . . . . . . . . . 11
⊢ (;15↑2) = (;15 · ;15) |
17 | | eqid 2759 |
. . . . . . . . . . . 12
⊢ ;15 = ;15 |
18 | 4 | mulid2i 10669 |
. . . . . . . . . . . . 13
⊢ (1
· ;15) = ;15 |
19 | | 1p1e2 11784 |
. . . . . . . . . . . . 13
⊢ (1 + 1) =
2 |
20 | | 2nn0 11936 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
21 | 11 | nn0cni 11931 |
. . . . . . . . . . . . . 14
⊢ 7 ∈
ℂ |
22 | 2 | nn0cni 11931 |
. . . . . . . . . . . . . 14
⊢ 5 ∈
ℂ |
23 | | 7p5e12 12199 |
. . . . . . . . . . . . . 14
⊢ (7 + 5) =
;12 |
24 | 21, 22, 23 | addcomli 10855 |
. . . . . . . . . . . . 13
⊢ (5 + 7) =
;12 |
25 | 1, 2, 11, 18, 19, 20, 24 | decaddci 12183 |
. . . . . . . . . . . 12
⊢ ((1
· ;15) + 7) = ;22 |
26 | 22 | mulid1i 10668 |
. . . . . . . . . . . . . . 15
⊢ (5
· 1) = 5 |
27 | 26 | oveq1i 7153 |
. . . . . . . . . . . . . 14
⊢ ((5
· 1) + 2) = (5 + 2) |
28 | | 5p2e7 11815 |
. . . . . . . . . . . . . 14
⊢ (5 + 2) =
7 |
29 | 27, 28 | eqtri 2782 |
. . . . . . . . . . . . 13
⊢ ((5
· 1) + 2) = 7 |
30 | | 5t5e25 12225 |
. . . . . . . . . . . . 13
⊢ (5
· 5) = ;25 |
31 | 2, 1, 2, 17, 2, 20, 29, 30 | decmul2c 12188 |
. . . . . . . . . . . 12
⊢ (5
· ;15) = ;75 |
32 | 3, 1, 2, 17, 2, 11, 25, 31 | decmul1c 12187 |
. . . . . . . . . . 11
⊢ (;15 · ;15) = ;;225 |
33 | 16, 32 | eqtri 2782 |
. . . . . . . . . 10
⊢ (;15↑2) = ;;225 |
34 | 6 | sqvali 13578 |
. . . . . . . . . . 11
⊢
(8↑2) = (8 · 8) |
35 | | 8t8e64 12243 |
. . . . . . . . . . 11
⊢ (8
· 8) = ;64 |
36 | 34, 35 | eqtri 2782 |
. . . . . . . . . 10
⊢
(8↑2) = ;64 |
37 | 33, 36 | oveq12i 7155 |
. . . . . . . . 9
⊢ ((;15↑2) + (8↑2)) = (;;225 + ;64) |
38 | 20, 20 | deccl 12137 |
. . . . . . . . . 10
⊢ ;22 ∈
ℕ0 |
39 | | 6nn0 11940 |
. . . . . . . . . 10
⊢ 6 ∈
ℕ0 |
40 | | 4nn0 11938 |
. . . . . . . . . 10
⊢ 4 ∈
ℕ0 |
41 | | eqid 2759 |
. . . . . . . . . 10
⊢ ;;225 = ;;225 |
42 | | eqid 2759 |
. . . . . . . . . 10
⊢ ;64 = ;64 |
43 | | eqid 2759 |
. . . . . . . . . . 11
⊢ ;22 = ;22 |
44 | 39 | nn0cni 11931 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℂ |
45 | | 2cn 11734 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
46 | | 6p2e8 11818 |
. . . . . . . . . . . 12
⊢ (6 + 2) =
8 |
47 | 44, 45, 46 | addcomli 10855 |
. . . . . . . . . . 11
⊢ (2 + 6) =
8 |
48 | 20, 20, 39, 43, 47 | decaddi 12182 |
. . . . . . . . . 10
⊢ (;22 + 6) = ;28 |
49 | | 5p4e9 11817 |
. . . . . . . . . 10
⊢ (5 + 4) =
9 |
50 | 38, 2, 39, 40, 41, 42, 48, 49 | decadd 12176 |
. . . . . . . . 9
⊢ (;;225 + ;64) = ;;289 |
51 | 1, 11 | deccl 12137 |
. . . . . . . . . . . 12
⊢ ;17 ∈
ℕ0 |
52 | 51 | nn0cni 11931 |
. . . . . . . . . . 11
⊢ ;17 ∈ ℂ |
53 | 52 | sqvali 13578 |
. . . . . . . . . 10
⊢ (;17↑2) = (;17 · ;17) |
54 | | eqid 2759 |
. . . . . . . . . . 11
⊢ ;17 = ;17 |
55 | | 9nn0 11943 |
. . . . . . . . . . 11
⊢ 9 ∈
ℕ0 |
56 | 1, 1 | deccl 12137 |
. . . . . . . . . . 11
⊢ ;11 ∈
ℕ0 |
57 | 52 | mulid2i 10669 |
. . . . . . . . . . . 12
⊢ (1
· ;17) = ;17 |
58 | | eqid 2759 |
. . . . . . . . . . . 12
⊢ ;11 = ;11 |
59 | | 7p1e8 11808 |
. . . . . . . . . . . 12
⊢ (7 + 1) =
8 |
60 | 1, 11, 1, 1, 57, 58, 19, 59 | decadd 12176 |
. . . . . . . . . . 11
⊢ ((1
· ;17) + ;11) = ;28 |
61 | 21 | mulid1i 10668 |
. . . . . . . . . . . . . 14
⊢ (7
· 1) = 7 |
62 | 61 | oveq1i 7153 |
. . . . . . . . . . . . 13
⊢ ((7
· 1) + 4) = (7 + 4) |
63 | | 7p4e11 12198 |
. . . . . . . . . . . . 13
⊢ (7 + 4) =
;11 |
64 | 62, 63 | eqtri 2782 |
. . . . . . . . . . . 12
⊢ ((7
· 1) + 4) = ;11 |
65 | | 7t7e49 12236 |
. . . . . . . . . . . 12
⊢ (7
· 7) = ;49 |
66 | 11, 1, 11, 54, 55, 40, 64, 65 | decmul2c 12188 |
. . . . . . . . . . 11
⊢ (7
· ;17) = ;;119 |
67 | 51, 1, 11, 54, 55, 56, 60, 66 | decmul1c 12187 |
. . . . . . . . . 10
⊢ (;17 · ;17) = ;;289 |
68 | 53, 67 | eqtr2i 2783 |
. . . . . . . . 9
⊢ ;;289 = (;17↑2) |
69 | 37, 50, 68 | 3eqtri 2786 |
. . . . . . . 8
⊢ ((;15↑2) + (8↑2)) = (;17↑2) |
70 | 69 | fveq2i 6654 |
. . . . . . 7
⊢
(√‘((;15↑2) + (8↑2))) = (√‘(;17↑2)) |
71 | 51 | nn0ge0i 11946 |
. . . . . . . 8
⊢ 0 ≤
;17 |
72 | 51 | nn0rei 11930 |
. . . . . . . . 9
⊢ ;17 ∈ ℝ |
73 | 72 | sqrtsqi 14767 |
. . . . . . . 8
⊢ (0 ≤
;17 → (√‘(;17↑2)) = ;17) |
74 | 71, 73 | ax-mp 5 |
. . . . . . 7
⊢
(√‘(;17↑2)) = ;17 |
75 | 15, 70, 74 | 3eqtri 2786 |
. . . . . 6
⊢
(abs‘(;15 + (i
· 8))) = ;17 |
76 | 12, 13 | crrei 14584 |
. . . . . 6
⊢
(ℜ‘(;15 + (i
· 8))) = ;15 |
77 | 19 | oveq1i 7153 |
. . . . . . 7
⊢ ((1 + 1)
+ 1) = (2 + 1) |
78 | | 2p1e3 11801 |
. . . . . . 7
⊢ (2 + 1) =
3 |
79 | 77, 78 | eqtri 2782 |
. . . . . 6
⊢ ((1 + 1)
+ 1) = 3 |
80 | 1, 11, 1, 2, 75, 76, 79, 20, 23 | decaddc 12177 |
. . . . 5
⊢
((abs‘(;15 + (i
· 8))) + (ℜ‘(;15
+ (i · 8)))) = ;32 |
81 | 80 | oveq1i 7153 |
. . . 4
⊢
(((abs‘(;15 + (i
· 8))) + (ℜ‘(;15
+ (i · 8)))) / 2) = (;32 /
2) |
82 | | eqid 2759 |
. . . . . 6
⊢ ;16 = ;16 |
83 | 45 | mulid1i 10668 |
. . . . . . . 8
⊢ (2
· 1) = 2 |
84 | 83 | oveq1i 7153 |
. . . . . . 7
⊢ ((2
· 1) + 1) = (2 + 1) |
85 | 84, 78 | eqtri 2782 |
. . . . . 6
⊢ ((2
· 1) + 1) = 3 |
86 | | 6t2e12 12226 |
. . . . . . 7
⊢ (6
· 2) = ;12 |
87 | 44, 45, 86 | mulcomli 10673 |
. . . . . 6
⊢ (2
· 6) = ;12 |
88 | 20, 1, 39, 82, 20, 1, 85, 87 | decmul2c 12188 |
. . . . 5
⊢ (2
· ;16) = ;32 |
89 | | 3nn0 11937 |
. . . . . . . 8
⊢ 3 ∈
ℕ0 |
90 | 89, 20 | deccl 12137 |
. . . . . . 7
⊢ ;32 ∈
ℕ0 |
91 | 90 | nn0cni 11931 |
. . . . . 6
⊢ ;32 ∈ ℂ |
92 | 1, 39 | deccl 12137 |
. . . . . . 7
⊢ ;16 ∈
ℕ0 |
93 | 92 | nn0cni 11931 |
. . . . . 6
⊢ ;16 ∈ ℂ |
94 | | 2ne0 11763 |
. . . . . 6
⊢ 2 ≠
0 |
95 | 91, 45, 93, 94 | divmuli 11417 |
. . . . 5
⊢ ((;32 / 2) = ;16 ↔ (2 · ;16) = ;32) |
96 | 88, 95 | mpbir 234 |
. . . 4
⊢ (;32 / 2) = ;16 |
97 | 40 | nn0cni 11931 |
. . . . . 6
⊢ 4 ∈
ℂ |
98 | 97 | sqvali 13578 |
. . . . 5
⊢
(4↑2) = (4 · 4) |
99 | | 4t4e16 12221 |
. . . . 5
⊢ (4
· 4) = ;16 |
100 | 98, 99 | eqtr2i 2783 |
. . . 4
⊢ ;16 = (4↑2) |
101 | 81, 96, 100 | 3eqtri 2786 |
. . 3
⊢
(((abs‘(;15 + (i
· 8))) + (ℜ‘(;15
+ (i · 8)))) / 2) = (4↑2) |
102 | 101 | fveq2i 6654 |
. 2
⊢
(√‘(((abs‘(;15 + (i · 8))) + (ℜ‘(;15 + (i · 8)))) / 2)) =
(√‘(4↑2)) |
103 | 40 | nn0ge0i 11946 |
. . 3
⊢ 0 ≤
4 |
104 | 40 | nn0rei 11930 |
. . . 4
⊢ 4 ∈
ℝ |
105 | 104 | sqrtsqi 14767 |
. . 3
⊢ (0 ≤ 4
→ (√‘(4↑2)) = 4) |
106 | 103, 105 | ax-mp 5 |
. 2
⊢
(√‘(4↑2)) = 4 |
107 | 10, 102, 106 | 3eqtri 2786 |
1
⊢
(ℜ‘(√‘(;15 + (i · 8)))) = 4 |