Metamath Proof Explorer


Theorem pythagtriplem7

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 ABCA2+B2=C2AgcdB=1¬2AC+B=C+BgcdA

Proof

Step Hyp Ref Expression
1 simp3 ABCC
2 1 nnzd ABCC
3 simp2 ABCB
4 3 nnzd ABCB
5 2 4 zsubcld ABCCB
6 5 3ad2ant1 ABCA2+B2=C2AgcdB=1¬2ACB
7 1 3 nnaddcld ABCC+B
8 7 nnnn0d ABCC+B0
9 8 3ad2ant1 ABCA2+B2=C2AgcdB=1¬2AC+B0
10 nnnn0 AA0
11 10 3ad2ant1 ABCA0
12 11 3ad2ant1 ABCA2+B2=C2AgcdB=1¬2AA0
13 6 9 12 3jca ABCA2+B2=C2AgcdB=1¬2ACBC+B0A0
14 pythagtriplem4 ABCA2+B2=C2AgcdB=1¬2ACBgcdC+B=1
15 14 oveq1d ABCA2+B2=C2AgcdB=1¬2ACBgcdC+BgcdA=1gcdA
16 nnz AA
17 16 3ad2ant1 ABCA
18 17 3ad2ant1 ABCA2+B2=C2AgcdB=1¬2AA
19 1gcd A1gcdA=1
20 18 19 syl ABCA2+B2=C2AgcdB=1¬2A1gcdA=1
21 15 20 eqtrd ABCA2+B2=C2AgcdB=1¬2ACBgcdC+BgcdA=1
22 13 21 jca ABCA2+B2=C2AgcdB=1¬2ACBC+B0A0CBgcdC+BgcdA=1
23 oveq1 A2+B2=C2A2+B2-B2=C2B2
24 23 3ad2ant2 ABCA2+B2=C2AgcdB=1¬2AA2+B2-B2=C2B2
25 nncn AA
26 25 3ad2ant1 ABCA
27 26 sqcld ABCA2
28 3 nncnd ABCB
29 28 sqcld ABCB2
30 27 29 pncand ABCA2+B2-B2=A2
31 30 3ad2ant1 ABCA2+B2=C2AgcdB=1¬2AA2+B2-B2=A2
32 1 nncnd ABCC
33 subsq CBC2B2=C+BCB
34 32 28 33 syl2anc ABCC2B2=C+BCB
35 7 nncnd ABCC+B
36 5 zcnd ABCCB
37 35 36 mulcomd ABCC+BCB=CBC+B
38 34 37 eqtrd ABCC2B2=CBC+B
39 38 3ad2ant1 ABCA2+B2=C2AgcdB=1¬2AC2B2=CBC+B
40 24 31 39 3eqtr3d ABCA2+B2=C2AgcdB=1¬2AA2=CBC+B
41 coprimeprodsq2 CBC+B0A0CBgcdC+BgcdA=1A2=CBC+BC+B=C+BgcdA2
42 22 40 41 sylc ABCA2+B2=C2AgcdB=1¬2AC+B=C+BgcdA2
43 42 fveq2d ABCA2+B2=C2AgcdB=1¬2AC+B=C+BgcdA2
44 7 nnzd ABCC+B
45 44 3ad2ant1 ABCA2+B2=C2AgcdB=1¬2AC+B
46 45 18 gcdcld ABCA2+B2=C2AgcdB=1¬2AC+BgcdA0
47 46 nn0red ABCA2+B2=C2AgcdB=1¬2AC+BgcdA
48 46 nn0ge0d ABCA2+B2=C2AgcdB=1¬2A0C+BgcdA
49 47 48 sqrtsqd ABCA2+B2=C2AgcdB=1¬2AC+BgcdA2=C+BgcdA
50 43 49 eqtrd ABCA2+B2=C2AgcdB=1¬2AC+B=C+BgcdA