pythagtriplem4

Description: Lemma for pythagtrip . Show that C - B and C + B are relatively prime. (Contributed by Scott Fenton, 12-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	pythagtriplem4	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( C - B ) gcd ( C + B ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		simp3r	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> -. 2 \|\| A )
2		nnz	\|- ( C e. NN -> C e. ZZ )
3		nnz	\|- ( B e. NN -> B e. ZZ )
4		zsubcl	\|- ( ( C e. ZZ /\ B e. ZZ ) -> ( C - B ) e. ZZ )
5	2 3 4	syl2anr	\|- ( ( B e. NN /\ C e. NN ) -> ( C - B ) e. ZZ )
6	5	3adant1	\|- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C - B ) e. ZZ )
7	6	3ad2ant1	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( C - B ) e. ZZ )
8		simp13	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> C e. NN )
9		simp12	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> B e. NN )
10	8 9	nnaddcld	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( C + B ) e. NN )
11	10	nnzd	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( C + B ) e. ZZ )
12		gcddvds	\|- ( ( ( C - B ) e. ZZ /\ ( C + B ) e. ZZ ) -> ( ( ( C - B ) gcd ( C + B ) ) \|\| ( C - B ) /\ ( ( C - B ) gcd ( C + B ) ) \|\| ( C + B ) ) )
13	7 11 12	syl2anc	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( ( C - B ) gcd ( C + B ) ) \|\| ( C - B ) /\ ( ( C - B ) gcd ( C + B ) ) \|\| ( C + B ) ) )
14	13	simprd	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( C - B ) gcd ( C + B ) ) \|\| ( C + B ) )
15		breq1	\|- ( ( ( C - B ) gcd ( C + B ) ) = 2 -> ( ( ( C - B ) gcd ( C + B ) ) \|\| ( C + B ) <-> 2 \|\| ( C + B ) ) )
16	15	biimpd	\|- ( ( ( C - B ) gcd ( C + B ) ) = 2 -> ( ( ( C - B ) gcd ( C + B ) ) \|\| ( C + B ) -> 2 \|\| ( C + B ) ) )
17	14 16	mpan9	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> 2 \|\| ( C + B ) )
18		2z	\|- 2 e. ZZ
19		simpl13	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> C e. NN )
20	19	nnzd	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> C e. ZZ )
21		simpl12	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> B e. NN )
22	21	nnzd	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> B e. ZZ )
23	20 22	zaddcld	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> ( C + B ) e. ZZ )
24	20 22	zsubcld	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> ( C - B ) e. ZZ )
25		dvdsmultr1	\|- ( ( 2 e. ZZ /\ ( C + B ) e. ZZ /\ ( C - B ) e. ZZ ) -> ( 2 \|\| ( C + B ) -> 2 \|\| ( ( C + B ) x. ( C - B ) ) ) )
26	18 23 24 25	mp3an2i	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> ( 2 \|\| ( C + B ) -> 2 \|\| ( ( C + B ) x. ( C - B ) ) ) )
27	17 26	mpd	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> 2 \|\| ( ( C + B ) x. ( C - B ) ) )
28	19	nncnd	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> C e. CC )
29	21	nncnd	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> B e. CC )
30		subsq	\|- ( ( C e. CC /\ B e. CC ) -> ( ( C ^ 2 ) - ( B ^ 2 ) ) = ( ( C + B ) x. ( C - B ) ) )
31	28 29 30	syl2anc	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> ( ( C ^ 2 ) - ( B ^ 2 ) ) = ( ( C + B ) x. ( C - B ) ) )
32	27 31	breqtrrd	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> 2 \|\| ( ( C ^ 2 ) - ( B ^ 2 ) ) )
33		simpl2	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) )
34	33	oveq1d	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( B ^ 2 ) ) = ( ( C ^ 2 ) - ( B ^ 2 ) ) )
35		simpl11	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> A e. NN )
36	35	nnsqcld	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> ( A ^ 2 ) e. NN )
37	36	nncnd	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> ( A ^ 2 ) e. CC )
38	21	nnsqcld	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> ( B ^ 2 ) e. NN )
39	38	nncnd	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> ( B ^ 2 ) e. CC )
40	37 39	pncand	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( B ^ 2 ) ) = ( A ^ 2 ) )
41	34 40	eqtr3d	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> ( ( C ^ 2 ) - ( B ^ 2 ) ) = ( A ^ 2 ) )
42	32 41	breqtrd	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> 2 \|\| ( A ^ 2 ) )
43		nnz	\|- ( A e. NN -> A e. ZZ )
44	43	3ad2ant1	\|- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. ZZ )
45	44	3ad2ant1	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> A e. ZZ )
46	45	adantr	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> A e. ZZ )
47		2prm	\|- 2 e. Prime
48		2nn	\|- 2 e. NN
49		prmdvdsexp	\|- ( ( 2 e. Prime /\ A e. ZZ /\ 2 e. NN ) -> ( 2 \|\| ( A ^ 2 ) <-> 2 \|\| A ) )
50	47 48 49	mp3an13	\|- ( A e. ZZ -> ( 2 \|\| ( A ^ 2 ) <-> 2 \|\| A ) )
51	46 50	syl	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> ( 2 \|\| ( A ^ 2 ) <-> 2 \|\| A ) )
52	42 51	mpbid	\|- ( ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) /\ ( ( C - B ) gcd ( C + B ) ) = 2 ) -> 2 \|\| A )
53	1 52	mtand	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> -. ( ( C - B ) gcd ( C + B ) ) = 2 )
54		neg1z	\|- -u 1 e. ZZ
55		gcdaddm	\|- ( ( -u 1 e. ZZ /\ ( C - B ) e. ZZ /\ ( C + B ) e. ZZ ) -> ( ( C - B ) gcd ( C + B ) ) = ( ( C - B ) gcd ( ( C + B ) + ( -u 1 x. ( C - B ) ) ) ) )
56	54 7 11 55	mp3an2i	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( C - B ) gcd ( C + B ) ) = ( ( C - B ) gcd ( ( C + B ) + ( -u 1 x. ( C - B ) ) ) ) )
57	8	nncnd	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> C e. CC )
58	9	nncnd	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> B e. CC )
59		pnncan	\|- ( ( C e. CC /\ B e. CC /\ B e. CC ) -> ( ( C + B ) - ( C - B ) ) = ( B + B ) )
60	59	3anidm23	\|- ( ( C e. CC /\ B e. CC ) -> ( ( C + B ) - ( C - B ) ) = ( B + B ) )
61		subcl	\|- ( ( C e. CC /\ B e. CC ) -> ( C - B ) e. CC )
62	61	mulm1d	\|- ( ( C e. CC /\ B e. CC ) -> ( -u 1 x. ( C - B ) ) = -u ( C - B ) )
63	62	oveq2d	\|- ( ( C e. CC /\ B e. CC ) -> ( ( C + B ) + ( -u 1 x. ( C - B ) ) ) = ( ( C + B ) + -u ( C - B ) ) )
64		addcl	\|- ( ( C e. CC /\ B e. CC ) -> ( C + B ) e. CC )
65	64 61	negsubd	\|- ( ( C e. CC /\ B e. CC ) -> ( ( C + B ) + -u ( C - B ) ) = ( ( C + B ) - ( C - B ) ) )
66	63 65	eqtrd	\|- ( ( C e. CC /\ B e. CC ) -> ( ( C + B ) + ( -u 1 x. ( C - B ) ) ) = ( ( C + B ) - ( C - B ) ) )
67		2times	\|- ( B e. CC -> ( 2 x. B ) = ( B + B ) )
68	67	adantl	\|- ( ( C e. CC /\ B e. CC ) -> ( 2 x. B ) = ( B + B ) )
69	60 66 68	3eqtr4d	\|- ( ( C e. CC /\ B e. CC ) -> ( ( C + B ) + ( -u 1 x. ( C - B ) ) ) = ( 2 x. B ) )
70	69	oveq2d	\|- ( ( C e. CC /\ B e. CC ) -> ( ( C - B ) gcd ( ( C + B ) + ( -u 1 x. ( C - B ) ) ) ) = ( ( C - B ) gcd ( 2 x. B ) ) )
71	57 58 70	syl2anc	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( C - B ) gcd ( ( C + B ) + ( -u 1 x. ( C - B ) ) ) ) = ( ( C - B ) gcd ( 2 x. B ) ) )
72	56 71	eqtrd	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( C - B ) gcd ( C + B ) ) = ( ( C - B ) gcd ( 2 x. B ) ) )
73	9	nnzd	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> B e. ZZ )
74		zmulcl	\|- ( ( 2 e. ZZ /\ B e. ZZ ) -> ( 2 x. B ) e. ZZ )
75	18 73 74	sylancr	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( 2 x. B ) e. ZZ )
76		gcddvds	\|- ( ( ( C - B ) e. ZZ /\ ( 2 x. B ) e. ZZ ) -> ( ( ( C - B ) gcd ( 2 x. B ) ) \|\| ( C - B ) /\ ( ( C - B ) gcd ( 2 x. B ) ) \|\| ( 2 x. B ) ) )
77	7 75 76	syl2anc	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( ( C - B ) gcd ( 2 x. B ) ) \|\| ( C - B ) /\ ( ( C - B ) gcd ( 2 x. B ) ) \|\| ( 2 x. B ) ) )
78	77	simprd	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( C - B ) gcd ( 2 x. B ) ) \|\| ( 2 x. B ) )
79	72 78	eqbrtrd	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( C - B ) gcd ( C + B ) ) \|\| ( 2 x. B ) )
80		1z	\|- 1 e. ZZ
81		gcdaddm	\|- ( ( 1 e. ZZ /\ ( C - B ) e. ZZ /\ ( C + B ) e. ZZ ) -> ( ( C - B ) gcd ( C + B ) ) = ( ( C - B ) gcd ( ( C + B ) + ( 1 x. ( C - B ) ) ) ) )
82	80 7 11 81	mp3an2i	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( C - B ) gcd ( C + B ) ) = ( ( C - B ) gcd ( ( C + B ) + ( 1 x. ( C - B ) ) ) ) )
83		ppncan	\|- ( ( C e. CC /\ B e. CC /\ C e. CC ) -> ( ( C + B ) + ( C - B ) ) = ( C + C ) )
84	83	3anidm13	\|- ( ( C e. CC /\ B e. CC ) -> ( ( C + B ) + ( C - B ) ) = ( C + C ) )
85	61	mullidd	\|- ( ( C e. CC /\ B e. CC ) -> ( 1 x. ( C - B ) ) = ( C - B ) )
86	85	oveq2d	\|- ( ( C e. CC /\ B e. CC ) -> ( ( C + B ) + ( 1 x. ( C - B ) ) ) = ( ( C + B ) + ( C - B ) ) )
87		2times	\|- ( C e. CC -> ( 2 x. C ) = ( C + C ) )
88	87	adantr	\|- ( ( C e. CC /\ B e. CC ) -> ( 2 x. C ) = ( C + C ) )
89	84 86 88	3eqtr4d	\|- ( ( C e. CC /\ B e. CC ) -> ( ( C + B ) + ( 1 x. ( C - B ) ) ) = ( 2 x. C ) )
90	57 58 89	syl2anc	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( C + B ) + ( 1 x. ( C - B ) ) ) = ( 2 x. C ) )
91	90	oveq2d	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( C - B ) gcd ( ( C + B ) + ( 1 x. ( C - B ) ) ) ) = ( ( C - B ) gcd ( 2 x. C ) ) )
92	82 91	eqtrd	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( C - B ) gcd ( C + B ) ) = ( ( C - B ) gcd ( 2 x. C ) ) )
93	8	nnzd	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> C e. ZZ )
94		zmulcl	\|- ( ( 2 e. ZZ /\ C e. ZZ ) -> ( 2 x. C ) e. ZZ )
95	18 93 94	sylancr	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( 2 x. C ) e. ZZ )
96		gcddvds	\|- ( ( ( C - B ) e. ZZ /\ ( 2 x. C ) e. ZZ ) -> ( ( ( C - B ) gcd ( 2 x. C ) ) \|\| ( C - B ) /\ ( ( C - B ) gcd ( 2 x. C ) ) \|\| ( 2 x. C ) ) )
97	7 95 96	syl2anc	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( ( C - B ) gcd ( 2 x. C ) ) \|\| ( C - B ) /\ ( ( C - B ) gcd ( 2 x. C ) ) \|\| ( 2 x. C ) ) )
98	97	simprd	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( C - B ) gcd ( 2 x. C ) ) \|\| ( 2 x. C ) )
99	92 98	eqbrtrd	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( C - B ) gcd ( C + B ) ) \|\| ( 2 x. C ) )
100		nnaddcl	\|- ( ( C e. NN /\ B e. NN ) -> ( C + B ) e. NN )
101	100	nnne0d	\|- ( ( C e. NN /\ B e. NN ) -> ( C + B ) =/= 0 )
102	101	ancoms	\|- ( ( B e. NN /\ C e. NN ) -> ( C + B ) =/= 0 )
103	102	3adant1	\|- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C + B ) =/= 0 )
104	103	3ad2ant1	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( C + B ) =/= 0 )
105	104	neneqd	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> -. ( C + B ) = 0 )
106	105	intnand	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> -. ( ( C - B ) = 0 /\ ( C + B ) = 0 ) )
107		gcdn0cl	\|- ( ( ( ( C - B ) e. ZZ /\ ( C + B ) e. ZZ ) /\ -. ( ( C - B ) = 0 /\ ( C + B ) = 0 ) ) -> ( ( C - B ) gcd ( C + B ) ) e. NN )
108	7 11 106 107	syl21anc	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( C - B ) gcd ( C + B ) ) e. NN )
109	108	nnzd	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( C - B ) gcd ( C + B ) ) e. ZZ )
110		dvdsgcd	\|- ( ( ( ( C - B ) gcd ( C + B ) ) e. ZZ /\ ( 2 x. B ) e. ZZ /\ ( 2 x. C ) e. ZZ ) -> ( ( ( ( C - B ) gcd ( C + B ) ) \|\| ( 2 x. B ) /\ ( ( C - B ) gcd ( C + B ) ) \|\| ( 2 x. C ) ) -> ( ( C - B ) gcd ( C + B ) ) \|\| ( ( 2 x. B ) gcd ( 2 x. C ) ) ) )
111	109 75 95 110	syl3anc	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( ( ( C - B ) gcd ( C + B ) ) \|\| ( 2 x. B ) /\ ( ( C - B ) gcd ( C + B ) ) \|\| ( 2 x. C ) ) -> ( ( C - B ) gcd ( C + B ) ) \|\| ( ( 2 x. B ) gcd ( 2 x. C ) ) ) )
112	79 99 111	mp2and	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( C - B ) gcd ( C + B ) ) \|\| ( ( 2 x. B ) gcd ( 2 x. C ) ) )
113		2nn0	\|- 2 e. NN0
114		mulgcd	\|- ( ( 2 e. NN0 /\ B e. ZZ /\ C e. ZZ ) -> ( ( 2 x. B ) gcd ( 2 x. C ) ) = ( 2 x. ( B gcd C ) ) )
115	113 73 93 114	mp3an2i	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( 2 x. B ) gcd ( 2 x. C ) ) = ( 2 x. ( B gcd C ) ) )
116		pythagtriplem3	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( B gcd C ) = 1 )
117	116	oveq2d	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( 2 x. ( B gcd C ) ) = ( 2 x. 1 ) )
118		2t1e2	\|- ( 2 x. 1 ) = 2
119	117 118	eqtrdi	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( 2 x. ( B gcd C ) ) = 2 )
120	115 119	eqtrd	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( 2 x. B ) gcd ( 2 x. C ) ) = 2 )
121	112 120	breqtrd	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( C - B ) gcd ( C + B ) ) \|\| 2 )
122		dvdsprime	\|- ( ( 2 e. Prime /\ ( ( C - B ) gcd ( C + B ) ) e. NN ) -> ( ( ( C - B ) gcd ( C + B ) ) \|\| 2 <-> ( ( ( C - B ) gcd ( C + B ) ) = 2 \/ ( ( C - B ) gcd ( C + B ) ) = 1 ) ) )
123	47 108 122	sylancr	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( ( C - B ) gcd ( C + B ) ) \|\| 2 <-> ( ( ( C - B ) gcd ( C + B ) ) = 2 \/ ( ( C - B ) gcd ( C + B ) ) = 1 ) ) )
124	121 123	mpbid	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( ( C - B ) gcd ( C + B ) ) = 2 \/ ( ( C - B ) gcd ( C + B ) ) = 1 ) )
125		orel1	\|- ( -. ( ( C - B ) gcd ( C + B ) ) = 2 -> ( ( ( ( C - B ) gcd ( C + B ) ) = 2 \/ ( ( C - B ) gcd ( C + B ) ) = 1 ) -> ( ( C - B ) gcd ( C + B ) ) = 1 ) )
126	53 124 125	sylc	\|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 \|\| A ) ) -> ( ( C - B ) gcd ( C + B ) ) = 1 )

Metamath Proof Explorer

Theorem pythagtriplem4

Proof