Step |
Hyp |
Ref |
Expression |
1 |
|
1nn0 |
|- 1 e. NN0 |
2 |
|
5nn0 |
|- 5 e. NN0 |
3 |
1 2
|
deccl |
|- ; 1 5 e. NN0 |
4 |
3
|
nn0cni |
|- ; 1 5 e. CC |
5 |
|
ax-icn |
|- _i e. CC |
6 |
|
8cn |
|- 8 e. CC |
7 |
5 6
|
mulcli |
|- ( _i x. 8 ) e. CC |
8 |
4 7
|
addcli |
|- ( ; 1 5 + ( _i x. 8 ) ) e. CC |
9 |
|
resqrtval |
|- ( ( ; 1 5 + ( _i x. 8 ) ) e. CC -> ( Re ` ( sqrt ` ( ; 1 5 + ( _i x. 8 ) ) ) ) = ( sqrt ` ( ( ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) + ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) / 2 ) ) ) |
10 |
8 9
|
ax-mp |
|- ( Re ` ( sqrt ` ( ; 1 5 + ( _i x. 8 ) ) ) ) = ( sqrt ` ( ( ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) + ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) / 2 ) ) |
11 |
|
7nn0 |
|- 7 e. NN0 |
12 |
3
|
nn0rei |
|- ; 1 5 e. RR |
13 |
|
8re |
|- 8 e. RR |
14 |
|
absreim |
|- ( ( ; 1 5 e. RR /\ 8 e. RR ) -> ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) = ( sqrt ` ( ( ; 1 5 ^ 2 ) + ( 8 ^ 2 ) ) ) ) |
15 |
12 13 14
|
mp2an |
|- ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) = ( sqrt ` ( ( ; 1 5 ^ 2 ) + ( 8 ^ 2 ) ) ) |
16 |
4
|
sqvali |
|- ( ; 1 5 ^ 2 ) = ( ; 1 5 x. ; 1 5 ) |
17 |
|
eqid |
|- ; 1 5 = ; 1 5 |
18 |
4
|
mulid2i |
|- ( 1 x. ; 1 5 ) = ; 1 5 |
19 |
|
1p1e2 |
|- ( 1 + 1 ) = 2 |
20 |
|
2nn0 |
|- 2 e. NN0 |
21 |
11
|
nn0cni |
|- 7 e. CC |
22 |
2
|
nn0cni |
|- 5 e. CC |
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 x. ; 1 5 ) + 7 ) = ; 2 2 |
26 |
22
|
mulid1i |
|- ( 5 x. 1 ) = 5 |
27 |
26
|
oveq1i |
|- ( ( 5 x. 1 ) + 2 ) = ( 5 + 2 ) |
28 |
|
5p2e7 |
|- ( 5 + 2 ) = 7 |
29 |
27 28
|
eqtri |
|- ( ( 5 x. 1 ) + 2 ) = 7 |
30 |
|
5t5e25 |
|- ( 5 x. 5 ) = ; 2 5 |
31 |
2 1 2 17 2 20 29 30
|
decmul2c |
|- ( 5 x. ; 1 5 ) = ; 7 5 |
32 |
3 1 2 17 2 11 25 31
|
decmul1c |
|- ( ; 1 5 x. ; 1 5 ) = ; ; 2 2 5 |
33 |
16 32
|
eqtri |
|- ( ; 1 5 ^ 2 ) = ; ; 2 2 5 |
34 |
6
|
sqvali |
|- ( 8 ^ 2 ) = ( 8 x. 8 ) |
35 |
|
8t8e64 |
|- ( 8 x. 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 e. NN0 |
39 |
|
6nn0 |
|- 6 e. NN0 |
40 |
|
4nn0 |
|- 4 e. NN0 |
41 |
|
eqid |
|- ; ; 2 2 5 = ; ; 2 2 5 |
42 |
|
eqid |
|- ; 6 4 = ; 6 4 |
43 |
|
eqid |
|- ; 2 2 = ; 2 2 |
44 |
39
|
nn0cni |
|- 6 e. CC |
45 |
|
2cn |
|- 2 e. CC |
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 e. NN0 |
52 |
51
|
nn0cni |
|- ; 1 7 e. CC |
53 |
52
|
sqvali |
|- ( ; 1 7 ^ 2 ) = ( ; 1 7 x. ; 1 7 ) |
54 |
|
eqid |
|- ; 1 7 = ; 1 7 |
55 |
|
9nn0 |
|- 9 e. NN0 |
56 |
1 1
|
deccl |
|- ; 1 1 e. NN0 |
57 |
52
|
mulid2i |
|- ( 1 x. ; 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 x. ; 1 7 ) + ; 1 1 ) = ; 2 8 |
61 |
21
|
mulid1i |
|- ( 7 x. 1 ) = 7 |
62 |
61
|
oveq1i |
|- ( ( 7 x. 1 ) + 4 ) = ( 7 + 4 ) |
63 |
|
7p4e11 |
|- ( 7 + 4 ) = ; 1 1 |
64 |
62 63
|
eqtri |
|- ( ( 7 x. 1 ) + 4 ) = ; 1 1 |
65 |
|
7t7e49 |
|- ( 7 x. 7 ) = ; 4 9 |
66 |
11 1 11 54 55 40 64 65
|
decmul2c |
|- ( 7 x. ; 1 7 ) = ; ; 1 1 9 |
67 |
51 1 11 54 55 56 60 66
|
decmul1c |
|- ( ; 1 7 x. ; 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 |
|- ( sqrt ` ( ( ; 1 5 ^ 2 ) + ( 8 ^ 2 ) ) ) = ( sqrt ` ( ; 1 7 ^ 2 ) ) |
71 |
51
|
nn0ge0i |
|- 0 <_ ; 1 7 |
72 |
51
|
nn0rei |
|- ; 1 7 e. RR |
73 |
72
|
sqrtsqi |
|- ( 0 <_ ; 1 7 -> ( sqrt ` ( ; 1 7 ^ 2 ) ) = ; 1 7 ) |
74 |
71 73
|
ax-mp |
|- ( sqrt ` ( ; 1 7 ^ 2 ) ) = ; 1 7 |
75 |
15 70 74
|
3eqtri |
|- ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) = ; 1 7 |
76 |
12 13
|
crrei |
|- ( Re ` ( ; 1 5 + ( _i x. 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 x. 8 ) ) ) + ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) = ; 3 2 |
81 |
80
|
oveq1i |
|- ( ( ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) + ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) / 2 ) = ( ; 3 2 / 2 ) |
82 |
|
eqid |
|- ; 1 6 = ; 1 6 |
83 |
45
|
mulid1i |
|- ( 2 x. 1 ) = 2 |
84 |
83
|
oveq1i |
|- ( ( 2 x. 1 ) + 1 ) = ( 2 + 1 ) |
85 |
84 78
|
eqtri |
|- ( ( 2 x. 1 ) + 1 ) = 3 |
86 |
|
6t2e12 |
|- ( 6 x. 2 ) = ; 1 2 |
87 |
44 45 86
|
mulcomli |
|- ( 2 x. 6 ) = ; 1 2 |
88 |
20 1 39 82 20 1 85 87
|
decmul2c |
|- ( 2 x. ; 1 6 ) = ; 3 2 |
89 |
|
3nn0 |
|- 3 e. NN0 |
90 |
89 20
|
deccl |
|- ; 3 2 e. NN0 |
91 |
90
|
nn0cni |
|- ; 3 2 e. CC |
92 |
1 39
|
deccl |
|- ; 1 6 e. NN0 |
93 |
92
|
nn0cni |
|- ; 1 6 e. CC |
94 |
|
2ne0 |
|- 2 =/= 0 |
95 |
91 45 93 94
|
divmuli |
|- ( ( ; 3 2 / 2 ) = ; 1 6 <-> ( 2 x. ; 1 6 ) = ; 3 2 ) |
96 |
88 95
|
mpbir |
|- ( ; 3 2 / 2 ) = ; 1 6 |
97 |
40
|
nn0cni |
|- 4 e. CC |
98 |
97
|
sqvali |
|- ( 4 ^ 2 ) = ( 4 x. 4 ) |
99 |
|
4t4e16 |
|- ( 4 x. 4 ) = ; 1 6 |
100 |
98 99
|
eqtr2i |
|- ; 1 6 = ( 4 ^ 2 ) |
101 |
81 96 100
|
3eqtri |
|- ( ( ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) + ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) / 2 ) = ( 4 ^ 2 ) |
102 |
101
|
fveq2i |
|- ( sqrt ` ( ( ( abs ` ( ; 1 5 + ( _i x. 8 ) ) ) + ( Re ` ( ; 1 5 + ( _i x. 8 ) ) ) ) / 2 ) ) = ( sqrt ` ( 4 ^ 2 ) ) |
103 |
40
|
nn0ge0i |
|- 0 <_ 4 |
104 |
40
|
nn0rei |
|- 4 e. RR |
105 |
104
|
sqrtsqi |
|- ( 0 <_ 4 -> ( sqrt ` ( 4 ^ 2 ) ) = 4 ) |
106 |
103 105
|
ax-mp |
|- ( sqrt ` ( 4 ^ 2 ) ) = 4 |
107 |
10 102 106
|
3eqtri |
|- ( Re ` ( sqrt ` ( ; 1 5 + ( _i x. 8 ) ) ) ) = 4 |