| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-5 |
|- 5 = ( 4 + 1 ) |
| 2 |
1
|
oveq1i |
|- ( 5 ^ 2 ) = ( ( 4 + 1 ) ^ 2 ) |
| 3 |
|
4cn |
|- 4 e. CC |
| 4 |
|
binom21 |
|- ( 4 e. CC -> ( ( 4 + 1 ) ^ 2 ) = ( ( ( 4 ^ 2 ) + ( 2 x. 4 ) ) + 1 ) ) |
| 5 |
3 4
|
ax-mp |
|- ( ( 4 + 1 ) ^ 2 ) = ( ( ( 4 ^ 2 ) + ( 2 x. 4 ) ) + 1 ) |
| 6 |
|
2nn0 |
|- 2 e. NN0 |
| 7 |
|
4nn0 |
|- 4 e. NN0 |
| 8 |
|
4p1e5 |
|- ( 4 + 1 ) = 5 |
| 9 |
|
sq4e2t8 |
|- ( 4 ^ 2 ) = ( 2 x. 8 ) |
| 10 |
|
8cn |
|- 8 e. CC |
| 11 |
|
2cn |
|- 2 e. CC |
| 12 |
|
8t2e16 |
|- ( 8 x. 2 ) = ; 1 6 |
| 13 |
10 11 12
|
mulcomli |
|- ( 2 x. 8 ) = ; 1 6 |
| 14 |
9 13
|
eqtri |
|- ( 4 ^ 2 ) = ; 1 6 |
| 15 |
|
4t2e8 |
|- ( 4 x. 2 ) = 8 |
| 16 |
3 11 15
|
mulcomli |
|- ( 2 x. 4 ) = 8 |
| 17 |
14 16
|
oveq12i |
|- ( ( 4 ^ 2 ) + ( 2 x. 4 ) ) = ( ; 1 6 + 8 ) |
| 18 |
|
1nn0 |
|- 1 e. NN0 |
| 19 |
|
6nn0 |
|- 6 e. NN0 |
| 20 |
|
8nn0 |
|- 8 e. NN0 |
| 21 |
|
eqid |
|- ; 1 6 = ; 1 6 |
| 22 |
|
1p1e2 |
|- ( 1 + 1 ) = 2 |
| 23 |
|
6cn |
|- 6 e. CC |
| 24 |
|
8p6e14 |
|- ( 8 + 6 ) = ; 1 4 |
| 25 |
10 23 24
|
addcomli |
|- ( 6 + 8 ) = ; 1 4 |
| 26 |
18 19 20 21 22 7 25
|
decaddci |
|- ( ; 1 6 + 8 ) = ; 2 4 |
| 27 |
17 26
|
eqtri |
|- ( ( 4 ^ 2 ) + ( 2 x. 4 ) ) = ; 2 4 |
| 28 |
6 7 8 27
|
decsuc |
|- ( ( ( 4 ^ 2 ) + ( 2 x. 4 ) ) + 1 ) = ; 2 5 |
| 29 |
5 28
|
eqtri |
|- ( ( 4 + 1 ) ^ 2 ) = ; 2 5 |
| 30 |
2 29
|
eqtri |
|- ( 5 ^ 2 ) = ; 2 5 |
| 31 |
|
3cn |
|- 3 e. CC |
| 32 |
31
|
negcli |
|- -u 3 e. CC |
| 33 |
|
expneg |
|- ( ( -u 3 e. CC /\ 2 e. NN0 ) -> ( -u 3 ^ -u 2 ) = ( 1 / ( -u 3 ^ 2 ) ) ) |
| 34 |
32 6 33
|
mp2an |
|- ( -u 3 ^ -u 2 ) = ( 1 / ( -u 3 ^ 2 ) ) |
| 35 |
|
sqneg |
|- ( 3 e. CC -> ( -u 3 ^ 2 ) = ( 3 ^ 2 ) ) |
| 36 |
31 35
|
ax-mp |
|- ( -u 3 ^ 2 ) = ( 3 ^ 2 ) |
| 37 |
|
sq3 |
|- ( 3 ^ 2 ) = 9 |
| 38 |
36 37
|
eqtri |
|- ( -u 3 ^ 2 ) = 9 |
| 39 |
38
|
oveq2i |
|- ( 1 / ( -u 3 ^ 2 ) ) = ( 1 / 9 ) |
| 40 |
34 39
|
eqtri |
|- ( -u 3 ^ -u 2 ) = ( 1 / 9 ) |
| 41 |
30 40
|
pm3.2i |
|- ( ( 5 ^ 2 ) = ; 2 5 /\ ( -u 3 ^ -u 2 ) = ( 1 / 9 ) ) |