Metamath Proof Explorer

Theorem pythagtriplem1

Description: Lemma for pythagtrip . Prove a weaker version of one direction of the theorem. (Contributed by Scott Fenton, 28-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion pythagtriplem1 
|- ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) )

Proof

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