Proof of Theorem resqrtvalex
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1nn0 12544 | . . . . . 6
⊢ 1 ∈
ℕ0 | 
| 2 |  | 5nn0 12548 | . . . . . 6
⊢ 5 ∈
ℕ0 | 
| 3 | 1, 2 | deccl 12750 | . . . . 5
⊢ ;15 ∈
ℕ0 | 
| 4 | 3 | nn0cni 12540 | . . . 4
⊢ ;15 ∈ ℂ | 
| 5 |  | ax-icn 11215 | . . . . 5
⊢ i ∈
ℂ | 
| 6 |  | 8cn 12364 | . . . . 5
⊢ 8 ∈
ℂ | 
| 7 | 5, 6 | mulcli 11269 | . . . 4
⊢ (i
· 8) ∈ ℂ | 
| 8 | 4, 7 | addcli 11268 | . . 3
⊢ (;15 + (i · 8)) ∈
ℂ | 
| 9 |  | resqrtval 43661 | . . 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 12550 | . . . . . 6
⊢ 7 ∈
ℕ0 | 
| 12 | 3 | nn0rei 12539 | . . . . . . . 8
⊢ ;15 ∈ ℝ | 
| 13 |  | 8re 12363 | . . . . . . . 8
⊢ 8 ∈
ℝ | 
| 14 |  | absreim 15333 | . . . . . . . 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 14220 | . . . . . . . . . . 11
⊢ (;15↑2) = (;15 · ;15) | 
| 17 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ ;15 = ;15 | 
| 18 | 4 | mullidi 11267 | . . . . . . . . . . . . 13
⊢ (1
· ;15) = ;15 | 
| 19 |  | 1p1e2 12392 | . . . . . . . . . . . . 13
⊢ (1 + 1) =
2 | 
| 20 |  | 2nn0 12545 | . . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 | 
| 21 | 11 | nn0cni 12540 | . . . . . . . . . . . . . 14
⊢ 7 ∈
ℂ | 
| 22 | 2 | nn0cni 12540 | . . . . . . . . . . . . . 14
⊢ 5 ∈
ℂ | 
| 23 |  | 7p5e12 12812 | . . . . . . . . . . . . . 14
⊢ (7 + 5) =
;12 | 
| 24 | 21, 22, 23 | addcomli 11454 | . . . . . . . . . . . . 13
⊢ (5 + 7) =
;12 | 
| 25 | 1, 2, 11, 18, 19, 20, 24 | decaddci 12796 | . . . . . . . . . . . 12
⊢ ((1
· ;15) + 7) = ;22 | 
| 26 | 22 | mulridi 11266 | . . . . . . . . . . . . . . 15
⊢ (5
· 1) = 5 | 
| 27 | 26 | oveq1i 7442 | . . . . . . . . . . . . . 14
⊢ ((5
· 1) + 2) = (5 + 2) | 
| 28 |  | 5p2e7 12423 | . . . . . . . . . . . . . 14
⊢ (5 + 2) =
7 | 
| 29 | 27, 28 | eqtri 2764 | . . . . . . . . . . . . 13
⊢ ((5
· 1) + 2) = 7 | 
| 30 |  | 5t5e25 12838 | . . . . . . . . . . . . 13
⊢ (5
· 5) = ;25 | 
| 31 | 2, 1, 2, 17, 2, 20, 29, 30 | decmul2c 12801 | . . . . . . . . . . . 12
⊢ (5
· ;15) = ;75 | 
| 32 | 3, 1, 2, 17, 2, 11, 25, 31 | decmul1c 12800 | . . . . . . . . . . 11
⊢ (;15 · ;15) = ;;225 | 
| 33 | 16, 32 | eqtri 2764 | . . . . . . . . . 10
⊢ (;15↑2) = ;;225 | 
| 34 | 6 | sqvali 14220 | . . . . . . . . . . 11
⊢
(8↑2) = (8 · 8) | 
| 35 |  | 8t8e64 12856 | . . . . . . . . . . 11
⊢ (8
· 8) = ;64 | 
| 36 | 34, 35 | eqtri 2764 | . . . . . . . . . 10
⊢
(8↑2) = ;64 | 
| 37 | 33, 36 | oveq12i 7444 | . . . . . . . . 9
⊢ ((;15↑2) + (8↑2)) = (;;225 + ;64) | 
| 38 | 20, 20 | deccl 12750 | . . . . . . . . . 10
⊢ ;22 ∈
ℕ0 | 
| 39 |  | 6nn0 12549 | . . . . . . . . . 10
⊢ 6 ∈
ℕ0 | 
| 40 |  | 4nn0 12547 | . . . . . . . . . 10
⊢ 4 ∈
ℕ0 | 
| 41 |  | eqid 2736 | . . . . . . . . . 10
⊢ ;;225 = ;;225 | 
| 42 |  | eqid 2736 | . . . . . . . . . 10
⊢ ;64 = ;64 | 
| 43 |  | eqid 2736 | . . . . . . . . . . 11
⊢ ;22 = ;22 | 
| 44 | 39 | nn0cni 12540 | . . . . . . . . . . . 12
⊢ 6 ∈
ℂ | 
| 45 |  | 2cn 12342 | . . . . . . . . . . . 12
⊢ 2 ∈
ℂ | 
| 46 |  | 6p2e8 12426 | . . . . . . . . . . . 12
⊢ (6 + 2) =
8 | 
| 47 | 44, 45, 46 | addcomli 11454 | . . . . . . . . . . 11
⊢ (2 + 6) =
8 | 
| 48 | 20, 20, 39, 43, 47 | decaddi 12795 | . . . . . . . . . 10
⊢ (;22 + 6) = ;28 | 
| 49 |  | 5p4e9 12425 | . . . . . . . . . 10
⊢ (5 + 4) =
9 | 
| 50 | 38, 2, 39, 40, 41, 42, 48, 49 | decadd 12789 | . . . . . . . . 9
⊢ (;;225 + ;64) = ;;289 | 
| 51 | 1, 11 | deccl 12750 | . . . . . . . . . . . 12
⊢ ;17 ∈
ℕ0 | 
| 52 | 51 | nn0cni 12540 | . . . . . . . . . . 11
⊢ ;17 ∈ ℂ | 
| 53 | 52 | sqvali 14220 | . . . . . . . . . 10
⊢ (;17↑2) = (;17 · ;17) | 
| 54 |  | eqid 2736 | . . . . . . . . . . 11
⊢ ;17 = ;17 | 
| 55 |  | 9nn0 12552 | . . . . . . . . . . 11
⊢ 9 ∈
ℕ0 | 
| 56 | 1, 1 | deccl 12750 | . . . . . . . . . . 11
⊢ ;11 ∈
ℕ0 | 
| 57 | 52 | mullidi 11267 | . . . . . . . . . . . 12
⊢ (1
· ;17) = ;17 | 
| 58 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ ;11 = ;11 | 
| 59 |  | 7p1e8 12416 | . . . . . . . . . . . 12
⊢ (7 + 1) =
8 | 
| 60 | 1, 11, 1, 1, 57, 58, 19, 59 | decadd 12789 | . . . . . . . . . . 11
⊢ ((1
· ;17) + ;11) = ;28 | 
| 61 | 21 | mulridi 11266 | . . . . . . . . . . . . . 14
⊢ (7
· 1) = 7 | 
| 62 | 61 | oveq1i 7442 | . . . . . . . . . . . . 13
⊢ ((7
· 1) + 4) = (7 + 4) | 
| 63 |  | 7p4e11 12811 | . . . . . . . . . . . . 13
⊢ (7 + 4) =
;11 | 
| 64 | 62, 63 | eqtri 2764 | . . . . . . . . . . . 12
⊢ ((7
· 1) + 4) = ;11 | 
| 65 |  | 7t7e49 12849 | . . . . . . . . . . . 12
⊢ (7
· 7) = ;49 | 
| 66 | 11, 1, 11, 54, 55, 40, 64, 65 | decmul2c 12801 | . . . . . . . . . . 11
⊢ (7
· ;17) = ;;119 | 
| 67 | 51, 1, 11, 54, 55, 56, 60, 66 | decmul1c 12800 | . . . . . . . . . 10
⊢ (;17 · ;17) = ;;289 | 
| 68 | 53, 67 | eqtr2i 2765 | . . . . . . . . 9
⊢ ;;289 = (;17↑2) | 
| 69 | 37, 50, 68 | 3eqtri 2768 | . . . . . . . 8
⊢ ((;15↑2) + (8↑2)) = (;17↑2) | 
| 70 | 69 | fveq2i 6908 | . . . . . . 7
⊢
(√‘((;15↑2) + (8↑2))) = (√‘(;17↑2)) | 
| 71 | 51 | nn0ge0i 12555 | . . . . . . . 8
⊢ 0 ≤
;17 | 
| 72 | 51 | nn0rei 12539 | . . . . . . . . 9
⊢ ;17 ∈ ℝ | 
| 73 | 72 | sqrtsqi 15414 | . . . . . . . 8
⊢ (0 ≤
;17 → (√‘(;17↑2)) = ;17) | 
| 74 | 71, 73 | ax-mp 5 | . . . . . . 7
⊢
(√‘(;17↑2)) = ;17 | 
| 75 | 15, 70, 74 | 3eqtri 2768 | . . . . . 6
⊢
(abs‘(;15 + (i
· 8))) = ;17 | 
| 76 | 12, 13 | crrei 15232 | . . . . . 6
⊢
(ℜ‘(;15 + (i
· 8))) = ;15 | 
| 77 | 19 | oveq1i 7442 | . . . . . . 7
⊢ ((1 + 1)
+ 1) = (2 + 1) | 
| 78 |  | 2p1e3 12409 | . . . . . . 7
⊢ (2 + 1) =
3 | 
| 79 | 77, 78 | eqtri 2764 | . . . . . 6
⊢ ((1 + 1)
+ 1) = 3 | 
| 80 | 1, 11, 1, 2, 75, 76, 79, 20, 23 | decaddc 12790 | . . . . 5
⊢
((abs‘(;15 + (i
· 8))) + (ℜ‘(;15
+ (i · 8)))) = ;32 | 
| 81 | 80 | oveq1i 7442 | . . . 4
⊢
(((abs‘(;15 + (i
· 8))) + (ℜ‘(;15
+ (i · 8)))) / 2) = (;32 /
2) | 
| 82 |  | eqid 2736 | . . . . . 6
⊢ ;16 = ;16 | 
| 83 | 45 | mulridi 11266 | . . . . . . . 8
⊢ (2
· 1) = 2 | 
| 84 | 83 | oveq1i 7442 | . . . . . . 7
⊢ ((2
· 1) + 1) = (2 + 1) | 
| 85 | 84, 78 | eqtri 2764 | . . . . . 6
⊢ ((2
· 1) + 1) = 3 | 
| 86 |  | 6t2e12 12839 | . . . . . . 7
⊢ (6
· 2) = ;12 | 
| 87 | 44, 45, 86 | mulcomli 11271 | . . . . . 6
⊢ (2
· 6) = ;12 | 
| 88 | 20, 1, 39, 82, 20, 1, 85, 87 | decmul2c 12801 | . . . . 5
⊢ (2
· ;16) = ;32 | 
| 89 |  | 3nn0 12546 | . . . . . . . 8
⊢ 3 ∈
ℕ0 | 
| 90 | 89, 20 | deccl 12750 | . . . . . . 7
⊢ ;32 ∈
ℕ0 | 
| 91 | 90 | nn0cni 12540 | . . . . . 6
⊢ ;32 ∈ ℂ | 
| 92 | 1, 39 | deccl 12750 | . . . . . . 7
⊢ ;16 ∈
ℕ0 | 
| 93 | 92 | nn0cni 12540 | . . . . . 6
⊢ ;16 ∈ ℂ | 
| 94 |  | 2ne0 12371 | . . . . . 6
⊢ 2 ≠
0 | 
| 95 | 91, 45, 93, 94 | divmuli 12022 | . . . . 5
⊢ ((;32 / 2) = ;16 ↔ (2 · ;16) = ;32) | 
| 96 | 88, 95 | mpbir 231 | . . . 4
⊢ (;32 / 2) = ;16 | 
| 97 | 40 | nn0cni 12540 | . . . . . 6
⊢ 4 ∈
ℂ | 
| 98 | 97 | sqvali 14220 | . . . . 5
⊢
(4↑2) = (4 · 4) | 
| 99 |  | 4t4e16 12834 | . . . . 5
⊢ (4
· 4) = ;16 | 
| 100 | 98, 99 | eqtr2i 2765 | . . . 4
⊢ ;16 = (4↑2) | 
| 101 | 81, 96, 100 | 3eqtri 2768 | . . 3
⊢
(((abs‘(;15 + (i
· 8))) + (ℜ‘(;15
+ (i · 8)))) / 2) = (4↑2) | 
| 102 | 101 | fveq2i 6908 | . 2
⊢
(√‘(((abs‘(;15 + (i · 8))) + (ℜ‘(;15 + (i · 8)))) / 2)) =
(√‘(4↑2)) | 
| 103 | 40 | nn0ge0i 12555 | . . 3
⊢ 0 ≤
4 | 
| 104 | 40 | nn0rei 12539 | . . . 4
⊢ 4 ∈
ℝ | 
| 105 | 104 | sqrtsqi 15414 | . . 3
⊢ (0 ≤ 4
→ (√‘(4↑2)) = 4) | 
| 106 | 103, 105 | ax-mp 5 | . 2
⊢
(√‘(4↑2)) = 4 | 
| 107 | 10, 102, 106 | 3eqtri 2768 | 1
⊢
(ℜ‘(√‘(;15 + (i · 8)))) = 4 |