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 n m k A = k m 2 n 2 B = k 2 m n C = k m 2 + n 2 A 2 + B 2 = C 2

Proof

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