Step |
Hyp |
Ref |
Expression |
1 |
|
nncn |
โข ( ๐ โ โ โ ๐ โ โ ) |
2 |
|
nncn |
โข ( ๐ โ โ โ ๐ โ โ ) |
3 |
|
nncn |
โข ( ๐ โ โ โ ๐ โ โ ) |
4 |
|
sqcl |
โข ( ๐ โ โ โ ( ๐ โ 2 ) โ โ ) |
5 |
4
|
adantl |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ๐ โ 2 ) โ โ ) |
6 |
5
|
sqcld |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( ๐ โ 2 ) โ 2 ) โ โ ) |
7 |
|
2cn |
โข 2 โ โ |
8 |
|
sqcl |
โข ( ๐ โ โ โ ( ๐ โ 2 ) โ โ ) |
9 |
|
mulcl |
โข ( ( ( ๐ โ 2 ) โ โ โง ( ๐ โ 2 ) โ โ ) โ ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) โ โ ) |
10 |
4 8 9
|
syl2anr |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) โ โ ) |
11 |
|
mulcl |
โข ( ( 2 โ โ โง ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) โ โ ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) โ โ ) |
12 |
7 10 11
|
sylancr |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) โ โ ) |
13 |
6 12
|
subcld |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( ( ๐ โ 2 ) โ 2 ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) โ โ ) |
14 |
8
|
adantr |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ๐ โ 2 ) โ โ ) |
15 |
14
|
sqcld |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( ๐ โ 2 ) โ 2 ) โ โ ) |
16 |
|
mulcl |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ๐ ยท ๐ ) โ โ ) |
17 |
16
|
ancoms |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ๐ ยท ๐ ) โ โ ) |
18 |
|
mulcl |
โข ( ( 2 โ โ โง ( ๐ ยท ๐ ) โ โ ) โ ( 2 ยท ( ๐ ยท ๐ ) ) โ โ ) |
19 |
7 17 18
|
sylancr |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( 2 ยท ( ๐ ยท ๐ ) ) โ โ ) |
20 |
19
|
sqcld |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) โ โ ) |
21 |
13 15 20
|
add32d |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( ( ( ( ๐ โ 2 ) โ 2 ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) + ( ( ๐ โ 2 ) โ 2 ) ) + ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) ) = ( ( ( ( ( ๐ โ 2 ) โ 2 ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) + ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) ) + ( ( ๐ โ 2 ) โ 2 ) ) ) |
22 |
6 12 20
|
subadd23d |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( ( ( ๐ โ 2 ) โ 2 ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) + ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) ) = ( ( ( ๐ โ 2 ) โ 2 ) + ( ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) ) ) |
23 |
|
sqmul |
โข ( ( 2 โ โ โง ( ๐ ยท ๐ ) โ โ ) โ ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) = ( ( 2 โ 2 ) ยท ( ( ๐ ยท ๐ ) โ 2 ) ) ) |
24 |
7 17 23
|
sylancr |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) = ( ( 2 โ 2 ) ยท ( ( ๐ ยท ๐ ) โ 2 ) ) ) |
25 |
|
sq2 |
โข ( 2 โ 2 ) = 4 |
26 |
25
|
a1i |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( 2 โ 2 ) = 4 ) |
27 |
|
sqmul |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( ๐ ยท ๐ ) โ 2 ) = ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) |
28 |
27
|
ancoms |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( ๐ ยท ๐ ) โ 2 ) = ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) |
29 |
26 28
|
oveq12d |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( 2 โ 2 ) ยท ( ( ๐ ยท ๐ ) โ 2 ) ) = ( 4 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) |
30 |
24 29
|
eqtrd |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) = ( 4 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) |
31 |
30
|
oveq1d |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) = ( ( 4 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) ) |
32 |
|
4cn |
โข 4 โ โ |
33 |
|
subdir |
โข ( ( 4 โ โ โง 2 โ โ โง ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) โ โ ) โ ( ( 4 โ 2 ) ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) = ( ( 4 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) ) |
34 |
32 7 10 33
|
mp3an12i |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( 4 โ 2 ) ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) = ( ( 4 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) ) |
35 |
|
2p2e4 |
โข ( 2 + 2 ) = 4 |
36 |
32 7 7 35
|
subaddrii |
โข ( 4 โ 2 ) = 2 |
37 |
36
|
oveq1i |
โข ( ( 4 โ 2 ) ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) = ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) |
38 |
34 37
|
eqtr3di |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( 4 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) = ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) |
39 |
31 38
|
eqtrd |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) = ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) |
40 |
39
|
oveq2d |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( ( ๐ โ 2 ) โ 2 ) + ( ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) ) = ( ( ( ๐ โ 2 ) โ 2 ) + ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) ) |
41 |
22 40
|
eqtrd |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( ( ( ๐ โ 2 ) โ 2 ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) + ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) ) = ( ( ( ๐ โ 2 ) โ 2 ) + ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) ) |
42 |
41
|
oveq1d |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( ( ( ( ๐ โ 2 ) โ 2 ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) + ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) ) + ( ( ๐ โ 2 ) โ 2 ) ) = ( ( ( ( ๐ โ 2 ) โ 2 ) + ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) + ( ( ๐ โ 2 ) โ 2 ) ) ) |
43 |
21 42
|
eqtrd |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( ( ( ( ๐ โ 2 ) โ 2 ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) + ( ( ๐ โ 2 ) โ 2 ) ) + ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) ) = ( ( ( ( ๐ โ 2 ) โ 2 ) + ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) + ( ( ๐ โ 2 ) โ 2 ) ) ) |
44 |
|
binom2sub |
โข ( ( ( ๐ โ 2 ) โ โ โง ( ๐ โ 2 ) โ โ ) โ ( ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) โ 2 ) = ( ( ( ( ๐ โ 2 ) โ 2 ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) + ( ( ๐ โ 2 ) โ 2 ) ) ) |
45 |
4 8 44
|
syl2anr |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) โ 2 ) = ( ( ( ( ๐ โ 2 ) โ 2 ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) + ( ( ๐ โ 2 ) โ 2 ) ) ) |
46 |
45
|
oveq1d |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) โ 2 ) + ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) ) = ( ( ( ( ( ๐ โ 2 ) โ 2 ) โ ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) + ( ( ๐ โ 2 ) โ 2 ) ) + ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) ) ) |
47 |
|
binom2 |
โข ( ( ( ๐ โ 2 ) โ โ โง ( ๐ โ 2 ) โ โ ) โ ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) โ 2 ) = ( ( ( ( ๐ โ 2 ) โ 2 ) + ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) + ( ( ๐ โ 2 ) โ 2 ) ) ) |
48 |
4 8 47
|
syl2anr |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) โ 2 ) = ( ( ( ( ๐ โ 2 ) โ 2 ) + ( 2 ยท ( ( ๐ โ 2 ) ยท ( ๐ โ 2 ) ) ) ) + ( ( ๐ โ 2 ) โ 2 ) ) ) |
49 |
43 46 48
|
3eqtr4d |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) โ 2 ) + ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) โ 2 ) ) |
50 |
49
|
3adant3 |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ( ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) โ 2 ) + ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) ) = ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) โ 2 ) ) |
51 |
50
|
oveq2d |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ( ๐ โ 2 ) ยท ( ( ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) โ 2 ) + ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) ) ) = ( ( ๐ โ 2 ) ยท ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) โ 2 ) ) ) |
52 |
|
simp3 |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ๐ โ โ ) |
53 |
4
|
3ad2ant2 |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ๐ โ 2 ) โ โ ) |
54 |
8
|
3ad2ant1 |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ๐ โ 2 ) โ โ ) |
55 |
53 54
|
subcld |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) โ โ ) |
56 |
52 55
|
sqmuld |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ( ๐ ยท ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) ) โ 2 ) = ( ( ๐ โ 2 ) ยท ( ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) โ 2 ) ) ) |
57 |
17
|
3adant3 |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ๐ ยท ๐ ) โ โ ) |
58 |
7 57 18
|
sylancr |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( 2 ยท ( ๐ ยท ๐ ) ) โ โ ) |
59 |
52 58
|
sqmuld |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ( ๐ ยท ( 2 ยท ( ๐ ยท ๐ ) ) ) โ 2 ) = ( ( ๐ โ 2 ) ยท ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) ) ) |
60 |
56 59
|
oveq12d |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ( ( ๐ ยท ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) ) โ 2 ) + ( ( ๐ ยท ( 2 ยท ( ๐ ยท ๐ ) ) ) โ 2 ) ) = ( ( ( ๐ โ 2 ) ยท ( ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) โ 2 ) ) + ( ( ๐ โ 2 ) ยท ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) ) ) ) |
61 |
|
sqcl |
โข ( ๐ โ โ โ ( ๐ โ 2 ) โ โ ) |
62 |
61
|
3ad2ant3 |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ๐ โ 2 ) โ โ ) |
63 |
55
|
sqcld |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) โ 2 ) โ โ ) |
64 |
58
|
sqcld |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) โ โ ) |
65 |
62 63 64
|
adddid |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ( ๐ โ 2 ) ยท ( ( ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) โ 2 ) + ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) ) ) = ( ( ( ๐ โ 2 ) ยท ( ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) โ 2 ) ) + ( ( ๐ โ 2 ) ยท ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) ) ) ) |
66 |
60 65
|
eqtr4d |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ( ( ๐ ยท ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) ) โ 2 ) + ( ( ๐ ยท ( 2 ยท ( ๐ ยท ๐ ) ) ) โ 2 ) ) = ( ( ๐ โ 2 ) ยท ( ( ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) โ 2 ) + ( ( 2 ยท ( ๐ ยท ๐ ) ) โ 2 ) ) ) ) |
67 |
53 54
|
addcld |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) โ โ ) |
68 |
52 67
|
sqmuld |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ( ๐ ยท ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) โ 2 ) = ( ( ๐ โ 2 ) ยท ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) โ 2 ) ) ) |
69 |
51 66 68
|
3eqtr4d |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ( ( ๐ ยท ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) ) โ 2 ) + ( ( ๐ ยท ( 2 ยท ( ๐ ยท ๐ ) ) ) โ 2 ) ) = ( ( ๐ ยท ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) โ 2 ) ) |
70 |
1 2 3 69
|
syl3an |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ( ( ๐ ยท ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) ) โ 2 ) + ( ( ๐ ยท ( 2 ยท ( ๐ ยท ๐ ) ) ) โ 2 ) ) = ( ( ๐ ยท ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) โ 2 ) ) |
71 |
|
oveq1 |
โข ( ๐ด = ( ๐ ยท ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) ) โ ( ๐ด โ 2 ) = ( ( ๐ ยท ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) ) โ 2 ) ) |
72 |
|
oveq1 |
โข ( ๐ต = ( ๐ ยท ( 2 ยท ( ๐ ยท ๐ ) ) ) โ ( ๐ต โ 2 ) = ( ( ๐ ยท ( 2 ยท ( ๐ ยท ๐ ) ) ) โ 2 ) ) |
73 |
71 72
|
oveqan12d |
โข ( ( ๐ด = ( ๐ ยท ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) ) โง ๐ต = ( ๐ ยท ( 2 ยท ( ๐ ยท ๐ ) ) ) ) โ ( ( ๐ด โ 2 ) + ( ๐ต โ 2 ) ) = ( ( ( ๐ ยท ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) ) โ 2 ) + ( ( ๐ ยท ( 2 ยท ( ๐ ยท ๐ ) ) ) โ 2 ) ) ) |
74 |
73
|
3adant3 |
โข ( ( ๐ด = ( ๐ ยท ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) ) โง ๐ต = ( ๐ ยท ( 2 ยท ( ๐ ยท ๐ ) ) ) โง ๐ถ = ( ๐ ยท ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) โ ( ( ๐ด โ 2 ) + ( ๐ต โ 2 ) ) = ( ( ( ๐ ยท ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) ) โ 2 ) + ( ( ๐ ยท ( 2 ยท ( ๐ ยท ๐ ) ) ) โ 2 ) ) ) |
75 |
|
oveq1 |
โข ( ๐ถ = ( ๐ ยท ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) โ ( ๐ถ โ 2 ) = ( ( ๐ ยท ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) โ 2 ) ) |
76 |
75
|
3ad2ant3 |
โข ( ( ๐ด = ( ๐ ยท ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) ) โง ๐ต = ( ๐ ยท ( 2 ยท ( ๐ ยท ๐ ) ) ) โง ๐ถ = ( ๐ ยท ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) โ ( ๐ถ โ 2 ) = ( ( ๐ ยท ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) โ 2 ) ) |
77 |
74 76
|
eqeq12d |
โข ( ( ๐ด = ( ๐ ยท ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) ) โง ๐ต = ( ๐ ยท ( 2 ยท ( ๐ ยท ๐ ) ) ) โง ๐ถ = ( ๐ ยท ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) โ ( ( ( ๐ด โ 2 ) + ( ๐ต โ 2 ) ) = ( ๐ถ โ 2 ) โ ( ( ( ๐ ยท ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) ) โ 2 ) + ( ( ๐ ยท ( 2 ยท ( ๐ ยท ๐ ) ) ) โ 2 ) ) = ( ( ๐ ยท ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) โ 2 ) ) ) |
78 |
70 77
|
syl5ibrcom |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ( ๐ด = ( ๐ ยท ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) ) โง ๐ต = ( ๐ ยท ( 2 ยท ( ๐ ยท ๐ ) ) ) โง ๐ถ = ( ๐ ยท ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) โ ( ( ๐ด โ 2 ) + ( ๐ต โ 2 ) ) = ( ๐ถ โ 2 ) ) ) |
79 |
78
|
3expa |
โข ( ( ( ๐ โ โ โง ๐ โ โ ) โง ๐ โ โ ) โ ( ( ๐ด = ( ๐ ยท ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) ) โง ๐ต = ( ๐ ยท ( 2 ยท ( ๐ ยท ๐ ) ) ) โง ๐ถ = ( ๐ ยท ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) โ ( ( ๐ด โ 2 ) + ( ๐ต โ 2 ) ) = ( ๐ถ โ 2 ) ) ) |
80 |
79
|
rexlimdva |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( โ ๐ โ โ ( ๐ด = ( ๐ ยท ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) ) โง ๐ต = ( ๐ ยท ( 2 ยท ( ๐ ยท ๐ ) ) ) โง ๐ถ = ( ๐ ยท ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) โ ( ( ๐ด โ 2 ) + ( ๐ต โ 2 ) ) = ( ๐ถ โ 2 ) ) ) |
81 |
80
|
rexlimivv |
โข ( โ ๐ โ โ โ ๐ โ โ โ ๐ โ โ ( ๐ด = ( ๐ ยท ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) ) โง ๐ต = ( ๐ ยท ( 2 ยท ( ๐ ยท ๐ ) ) ) โง ๐ถ = ( ๐ ยท ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) ) ) โ ( ( ๐ด โ 2 ) + ( ๐ต โ 2 ) ) = ( ๐ถ โ 2 ) ) |