Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pythagtriplem3 Structured version   Unicode version

Theorem pythagtriplem3 13194
 Description: Lemma for pythagtrip 13210. Show that and are relatively prime under some conditions. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
Assertion
Ref Expression
pythagtriplem3

Proof of Theorem pythagtriplem3
StepHypRef Expression
1 oveq2 6091 . . . . . . 7
21adantl 454 . . . . . 6
3 nnz 10305 . . . . . . . . . . 11
4 zsqcl 11454 . . . . . . . . . . 11
53, 4syl 16 . . . . . . . . . 10
653ad2ant2 980 . . . . . . . . 9
7 nnz 10305 . . . . . . . . . . 11
8 zsqcl 11454 . . . . . . . . . . 11
97, 8syl 16 . . . . . . . . . 10
1093ad2ant1 979 . . . . . . . . 9
11 gcdadd 13032 . . . . . . . . 9
126, 10, 11syl2anc 644 . . . . . . . 8
13 gcdcom 13022 . . . . . . . . 9
146, 10, 13syl2anc 644 . . . . . . . 8
1512, 14eqtr3d 2472 . . . . . . 7
1615adantr 453 . . . . . 6
172, 16eqtr3d 2472 . . . . 5
18 simpl2 962 . . . . . 6
19 simpl3 963 . . . . . 6
20 sqgcd 13060 . . . . . 6
2118, 19, 20syl2anc 644 . . . . 5
22 simpl1 961 . . . . . 6
23 sqgcd 13060 . . . . . 6
2422, 18, 23syl2anc 644 . . . . 5
2517, 21, 243eqtr4d 2480 . . . 4
27 simp3l 986 . . . 4
2827oveq1d 6098 . . 3
2926, 28eqtrd 2470 . 2
3033ad2ant2 980 . . . . . 6
31 nnz 10305 . . . . . . 7
32313ad2ant3 981 . . . . . 6
3330, 32gcdcld 13020 . . . . 5
3433nn0red 10277 . . . 4