Description: Lemma for pythagtrip . Calculate ( sqrt( C + B ) ) . (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | pythagtriplem7 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3 | |
|
2 | 1 | nnzd | |
3 | simp2 | |
|
4 | 3 | nnzd | |
5 | 2 4 | zsubcld | |
6 | 5 | 3ad2ant1 | |
7 | 1 3 | nnaddcld | |
8 | 7 | nnnn0d | |
9 | 8 | 3ad2ant1 | |
10 | nnnn0 | |
|
11 | 10 | 3ad2ant1 | |
12 | 11 | 3ad2ant1 | |
13 | 6 9 12 | 3jca | |
14 | pythagtriplem4 | |
|
15 | 14 | oveq1d | |
16 | nnz | |
|
17 | 16 | 3ad2ant1 | |
18 | 17 | 3ad2ant1 | |
19 | 1gcd | |
|
20 | 18 19 | syl | |
21 | 15 20 | eqtrd | |
22 | 13 21 | jca | |
23 | oveq1 | |
|
24 | 23 | 3ad2ant2 | |
25 | nncn | |
|
26 | 25 | 3ad2ant1 | |
27 | 26 | sqcld | |
28 | 3 | nncnd | |
29 | 28 | sqcld | |
30 | 27 29 | pncand | |
31 | 30 | 3ad2ant1 | |
32 | 1 | nncnd | |
33 | subsq | |
|
34 | 32 28 33 | syl2anc | |
35 | 7 | nncnd | |
36 | 5 | zcnd | |
37 | 35 36 | mulcomd | |
38 | 34 37 | eqtrd | |
39 | 38 | 3ad2ant1 | |
40 | 24 31 39 | 3eqtr3d | |
41 | coprimeprodsq2 | |
|
42 | 22 40 41 | sylc | |
43 | 42 | fveq2d | |
44 | 7 | nnzd | |
45 | 44 | 3ad2ant1 | |
46 | 45 18 | gcdcld | |
47 | 46 | nn0red | |
48 | 46 | nn0ge0d | |
49 | 47 48 | sqrtsqd | |
50 | 43 49 | eqtrd | |