pythagtriplem19

Description: Lemma for pythagtrip . Introduce k and remove the relative primality requirement. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	pythagtriplem19	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to \exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2}))$

Proof

Step	Hyp	Ref	Expression
1		gcdnncl	$⊢ (A \in ℕ \land B \in ℕ) \to A \gcd B \in ℕ$
2	1	3adant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \gcd B \in ℕ$
3	2	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to A \gcd B \in ℕ$
4		nnz	$⊢ A \in ℕ \to A \in ℤ$
5		nnz	$⊢ B \in ℕ \to B \in ℤ$
6		gcddvds	$⊢ (A \in ℤ \land B \in ℤ) \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
7	4 5 6	syl2an	$⊢ (A \in ℕ \land B \in ℕ) \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
8	7	3adant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
9	8	simpld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to (A \gcd B) ∥ A$
10	2	nnzd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \gcd B \in ℤ$
11	2	nnne0d	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \gcd B \neq 0$
12	4	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℤ$
13		dvdsval2	$⊢ (A \gcd B \in ℤ \land A \gcd B \neq 0 \land A \in ℤ) \to ((A \gcd B) ∥ A \leftrightarrow \frac{A}{A \gcd B} \in ℤ)$
14	10 11 12 13	syl3anc	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to ((A \gcd B) ∥ A \leftrightarrow \frac{A}{A \gcd B} \in ℤ)$
15	9 14	mpbid	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to \frac{A}{A \gcd B} \in ℤ$
16		nnre	$⊢ A \in ℕ \to A \in ℝ$
17	16	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℝ$
18	2	nnred	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \gcd B \in ℝ$
19		nngt0	$⊢ A \in ℕ \to 0 < A$
20	19	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 < A$
21	2	nngt0d	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 < A \gcd B$
22	17 18 20 21	divgt0d	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 < \frac{A}{A \gcd B}$
23		elnnz	$⊢ \frac{A}{A \gcd B} \in ℕ \leftrightarrow (\frac{A}{A \gcd B} \in ℤ \land 0 < \frac{A}{A \gcd B})$
24	15 22 23	sylanbrc	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to \frac{A}{A \gcd B} \in ℕ$
25	24	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to \frac{A}{A \gcd B} \in ℕ$
26	8	simprd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to (A \gcd B) ∥ B$
27	5	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B \in ℤ$
28		dvdsval2	$⊢ (A \gcd B \in ℤ \land A \gcd B \neq 0 \land B \in ℤ) \to ((A \gcd B) ∥ B \leftrightarrow \frac{B}{A \gcd B} \in ℤ)$
29	10 11 27 28	syl3anc	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to ((A \gcd B) ∥ B \leftrightarrow \frac{B}{A \gcd B} \in ℤ)$
30	26 29	mpbid	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to \frac{B}{A \gcd B} \in ℤ$
31		nnre	$⊢ B \in ℕ \to B \in ℝ$
32	31	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B \in ℝ$
33		nngt0	$⊢ B \in ℕ \to 0 < B$
34	33	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 < B$
35	32 18 34 21	divgt0d	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 < \frac{B}{A \gcd B}$
36		elnnz	$⊢ \frac{B}{A \gcd B} \in ℕ \leftrightarrow (\frac{B}{A \gcd B} \in ℤ \land 0 < \frac{B}{A \gcd B})$
37	30 35 36	sylanbrc	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to \frac{B}{A \gcd B} \in ℕ$
38	37	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to \frac{B}{A \gcd B} \in ℕ$
39		dvdssq	$⊢ (A \gcd B \in ℤ \land A \in ℤ) \to ((A \gcd B) ∥ A \leftrightarrow {(A \gcd B)}^{2} ∥ A^{2})$
40	10 12 39	syl2anc	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to ((A \gcd B) ∥ A \leftrightarrow {(A \gcd B)}^{2} ∥ A^{2})$
41		dvdssq	$⊢ (A \gcd B \in ℤ \land B \in ℤ) \to ((A \gcd B) ∥ B \leftrightarrow {(A \gcd B)}^{2} ∥ B^{2})$
42	10 27 41	syl2anc	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to ((A \gcd B) ∥ B \leftrightarrow {(A \gcd B)}^{2} ∥ B^{2})$
43	40 42	anbi12d	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to (((A \gcd B) ∥ A \land (A \gcd B) ∥ B) \leftrightarrow ({(A \gcd B)}^{2} ∥ A^{2} \land {(A \gcd B)}^{2} ∥ B^{2}))$
44	8 43	mpbid	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to ({(A \gcd B)}^{2} ∥ A^{2} \land {(A \gcd B)}^{2} ∥ B^{2})$
45	2	nnsqcld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to {(A \gcd B)}^{2} \in ℕ$
46	45	nnzd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to {(A \gcd B)}^{2} \in ℤ$
47		nnsqcl	$⊢ A \in ℕ \to A^{2} \in ℕ$
48	47	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A^{2} \in ℕ$
49	48	nnzd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A^{2} \in ℤ$
50		nnsqcl	$⊢ B \in ℕ \to B^{2} \in ℕ$
51	50	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B^{2} \in ℕ$
52	51	nnzd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B^{2} \in ℤ$
53		dvds2add	$⊢ ({(A \gcd B)}^{2} \in ℤ \land A^{2} \in ℤ \land B^{2} \in ℤ) \to (({(A \gcd B)}^{2} ∥ A^{2} \land {(A \gcd B)}^{2} ∥ B^{2}) \to {(A \gcd B)}^{2} ∥ (A^{2} + B^{2}))$
54	46 49 52 53	syl3anc	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to (({(A \gcd B)}^{2} ∥ A^{2} \land {(A \gcd B)}^{2} ∥ B^{2}) \to {(A \gcd B)}^{2} ∥ (A^{2} + B^{2}))$
55	44 54	mpd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to {(A \gcd B)}^{2} ∥ (A^{2} + B^{2})$
56	55	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to {(A \gcd B)}^{2} ∥ (A^{2} + B^{2})$
57		simpr	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to A^{2} + B^{2} = C^{2}$
58	56 57	breqtrd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to {(A \gcd B)}^{2} ∥ C^{2}$
59		nnz	$⊢ C \in ℕ \to C \in ℤ$
60	59	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C \in ℤ$
61		dvdssq	$⊢ (A \gcd B \in ℤ \land C \in ℤ) \to ((A \gcd B) ∥ C \leftrightarrow {(A \gcd B)}^{2} ∥ C^{2})$
62	10 60 61	syl2anc	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to ((A \gcd B) ∥ C \leftrightarrow {(A \gcd B)}^{2} ∥ C^{2})$
63	62	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to ((A \gcd B) ∥ C \leftrightarrow {(A \gcd B)}^{2} ∥ C^{2})$
64	58 63	mpbird	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to (A \gcd B) ∥ C$
65		dvdsval2	$⊢ (A \gcd B \in ℤ \land A \gcd B \neq 0 \land C \in ℤ) \to ((A \gcd B) ∥ C \leftrightarrow \frac{C}{A \gcd B} \in ℤ)$
66	10 11 60 65	syl3anc	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to ((A \gcd B) ∥ C \leftrightarrow \frac{C}{A \gcd B} \in ℤ)$
67	66	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to ((A \gcd B) ∥ C \leftrightarrow \frac{C}{A \gcd B} \in ℤ)$
68	64 67	mpbid	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to \frac{C}{A \gcd B} \in ℤ$
69		nnre	$⊢ C \in ℕ \to C \in ℝ$
70	69	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C \in ℝ$
71		nngt0	$⊢ C \in ℕ \to 0 < C$
72	71	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 < C$
73	70 18 72 21	divgt0d	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 < \frac{C}{A \gcd B}$
74	73	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to 0 < \frac{C}{A \gcd B}$
75		elnnz	$⊢ \frac{C}{A \gcd B} \in ℕ \leftrightarrow (\frac{C}{A \gcd B} \in ℤ \land 0 < \frac{C}{A \gcd B})$
76	68 74 75	sylanbrc	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to \frac{C}{A \gcd B} \in ℕ$
77	76	3adant3	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to \frac{C}{A \gcd B} \in ℕ$
78	48	nncnd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A^{2} \in ℂ$
79	51	nncnd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B^{2} \in ℂ$
80	45	nncnd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to {(A \gcd B)}^{2} \in ℂ$
81	45	nnne0d	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to {(A \gcd B)}^{2} \neq 0$
82	78 79 80 81	divdird	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to \frac{A^{2} + B^{2}}{{(A \gcd B)}^{2}} = (\frac{A^{2}}{{(A \gcd B)}^{2}}) + (\frac{B^{2}}{{(A \gcd B)}^{2}})$
83	82	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to \frac{A^{2} + B^{2}}{{(A \gcd B)}^{2}} = (\frac{A^{2}}{{(A \gcd B)}^{2}}) + (\frac{B^{2}}{{(A \gcd B)}^{2}})$
84		nncn	$⊢ C \in ℕ \to C \in ℂ$
85	84	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C \in ℂ$
86	2	nncnd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \gcd B \in ℂ$
87	85 86 11	sqdivd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to {(\frac{C}{A \gcd B})}^{2} = \frac{C^{2}}{{(A \gcd B)}^{2}}$
88	87	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to {(\frac{C}{A \gcd B})}^{2} = \frac{C^{2}}{{(A \gcd B)}^{2}}$
89		oveq1	$⊢ A^{2} + B^{2} = C^{2} \to \frac{A^{2} + B^{2}}{{(A \gcd B)}^{2}} = \frac{C^{2}}{{(A \gcd B)}^{2}}$
90	89	3ad2ant2	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to \frac{A^{2} + B^{2}}{{(A \gcd B)}^{2}} = \frac{C^{2}}{{(A \gcd B)}^{2}}$
91	88 90	eqtr4d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to {(\frac{C}{A \gcd B})}^{2} = \frac{A^{2} + B^{2}}{{(A \gcd B)}^{2}}$
92		nncn	$⊢ A \in ℕ \to A \in ℂ$
93	92	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℂ$
94	93 86 11	sqdivd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to {(\frac{A}{A \gcd B})}^{2} = \frac{A^{2}}{{(A \gcd B)}^{2}}$
95		nncn	$⊢ B \in ℕ \to B \in ℂ$
96	95	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B \in ℂ$
97	96 86 11	sqdivd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to {(\frac{B}{A \gcd B})}^{2} = \frac{B^{2}}{{(A \gcd B)}^{2}}$
98	94 97	oveq12d	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to {(\frac{A}{A \gcd B})}^{2} + {(\frac{B}{A \gcd B})}^{2} = (\frac{A^{2}}{{(A \gcd B)}^{2}}) + (\frac{B^{2}}{{(A \gcd B)}^{2}})$
99	98	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to {(\frac{A}{A \gcd B})}^{2} + {(\frac{B}{A \gcd B})}^{2} = (\frac{A^{2}}{{(A \gcd B)}^{2}}) + (\frac{B^{2}}{{(A \gcd B)}^{2}})$
100	83 91 99	3eqtr4rd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to {(\frac{A}{A \gcd B})}^{2} + {(\frac{B}{A \gcd B})}^{2} = {(\frac{C}{A \gcd B})}^{2}$
101		gcddiv	$⊢ ((A \in ℤ \land B \in ℤ \land A \gcd B \in ℕ) \land ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)) \to \frac{A \gcd B}{A \gcd B} = (\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B})$
102	12 27 2 8 101	syl31anc	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to \frac{A \gcd B}{A \gcd B} = (\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B})$
103	86 11	dividd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to \frac{A \gcd B}{A \gcd B} = 1$
104	102 103	eqtr3d	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to (\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B}) = 1$
105	104	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to (\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B}) = 1$
106		simp3	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to \neg 2 ∥ (\frac{A}{A \gcd B})$
107		pythagtriplem18	$⊢ ((\frac{A}{A \gcd B} \in ℕ \land \frac{B}{A \gcd B} \in ℕ \land \frac{C}{A \gcd B} \in ℕ) \land {(\frac{A}{A \gcd B})}^{2} + {(\frac{B}{A \gcd B})}^{2} = {(\frac{C}{A \gcd B})}^{2} \land ((\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B}) = 1 \land \neg 2 ∥ (\frac{A}{A \gcd B}))) \to \exists n \in ℕ \exists m \in ℕ (\frac{A}{A \gcd B} = m^{2} - n^{2} \land \frac{B}{A \gcd B} = 2 m n \land \frac{C}{A \gcd B} = m^{2} + n^{2})$
108	25 38 77 100 105 106 107	syl312anc	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to \exists n \in ℕ \exists m \in ℕ (\frac{A}{A \gcd B} = m^{2} - n^{2} \land \frac{B}{A \gcd B} = 2 m n \land \frac{C}{A \gcd B} = m^{2} + n^{2})$
109	93 86 11	divcan2d	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to (A \gcd B) (\frac{A}{A \gcd B}) = A$
110	109	eqcomd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A = (A \gcd B) (\frac{A}{A \gcd B})$
111	96 86 11	divcan2d	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to (A \gcd B) (\frac{B}{A \gcd B}) = B$
112	111	eqcomd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B = (A \gcd B) (\frac{B}{A \gcd B})$
113	85 86 11	divcan2d	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to (A \gcd B) (\frac{C}{A \gcd B}) = C$
114	113	eqcomd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C = (A \gcd B) (\frac{C}{A \gcd B})$
115	110 112 114	3jca	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to (A = (A \gcd B) (\frac{A}{A \gcd B}) \land B = (A \gcd B) (\frac{B}{A \gcd B}) \land C = (A \gcd B) (\frac{C}{A \gcd B}))$
116	115	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to (A = (A \gcd B) (\frac{A}{A \gcd B}) \land B = (A \gcd B) (\frac{B}{A \gcd B}) \land C = (A \gcd B) (\frac{C}{A \gcd B}))$
117		oveq2	$⊢ \frac{A}{A \gcd B} = m^{2} - n^{2} \to (A \gcd B) (\frac{A}{A \gcd B}) = (A \gcd B) (m^{2} - n^{2})$
118	117	eqeq2d	$⊢ \frac{A}{A \gcd B} = m^{2} - n^{2} \to (A = (A \gcd B) (\frac{A}{A \gcd B}) \leftrightarrow A = (A \gcd B) (m^{2} - n^{2}))$
119	118	3ad2ant1	$⊢ (\frac{A}{A \gcd B} = m^{2} - n^{2} \land \frac{B}{A \gcd B} = 2 m n \land \frac{C}{A \gcd B} = m^{2} + n^{2}) \to (A = (A \gcd B) (\frac{A}{A \gcd B}) \leftrightarrow A = (A \gcd B) (m^{2} - n^{2}))$
120		oveq2	$⊢ \frac{B}{A \gcd B} = 2 m n \to (A \gcd B) (\frac{B}{A \gcd B}) = (A \gcd B) 2 m n$
121	120	eqeq2d	$⊢ \frac{B}{A \gcd B} = 2 m n \to (B = (A \gcd B) (\frac{B}{A \gcd B}) \leftrightarrow B = (A \gcd B) 2 m n)$
122	121	3ad2ant2	$⊢ (\frac{A}{A \gcd B} = m^{2} - n^{2} \land \frac{B}{A \gcd B} = 2 m n \land \frac{C}{A \gcd B} = m^{2} + n^{2}) \to (B = (A \gcd B) (\frac{B}{A \gcd B}) \leftrightarrow B = (A \gcd B) 2 m n)$
123		oveq2	$⊢ \frac{C}{A \gcd B} = m^{2} + n^{2} \to (A \gcd B) (\frac{C}{A \gcd B}) = (A \gcd B) (m^{2} + n^{2})$
124	123	eqeq2d	$⊢ \frac{C}{A \gcd B} = m^{2} + n^{2} \to (C = (A \gcd B) (\frac{C}{A \gcd B}) \leftrightarrow C = (A \gcd B) (m^{2} + n^{2}))$
125	124	3ad2ant3	$⊢ (\frac{A}{A \gcd B} = m^{2} - n^{2} \land \frac{B}{A \gcd B} = 2 m n \land \frac{C}{A \gcd B} = m^{2} + n^{2}) \to (C = (A \gcd B) (\frac{C}{A \gcd B}) \leftrightarrow C = (A \gcd B) (m^{2} + n^{2}))$
126	119 122 125	3anbi123d	$⊢ (\frac{A}{A \gcd B} = m^{2} - n^{2} \land \frac{B}{A \gcd B} = 2 m n \land \frac{C}{A \gcd B} = m^{2} + n^{2}) \to ((A = (A \gcd B) (\frac{A}{A \gcd B}) \land B = (A \gcd B) (\frac{B}{A \gcd B}) \land C = (A \gcd B) (\frac{C}{A \gcd B})) \leftrightarrow (A = (A \gcd B) (m^{2} - n^{2}) \land B = (A \gcd B) 2 m n \land C = (A \gcd B) (m^{2} + n^{2})))$
127	116 126	syl5ibcom	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to ((\frac{A}{A \gcd B} = m^{2} - n^{2} \land \frac{B}{A \gcd B} = 2 m n \land \frac{C}{A \gcd B} = m^{2} + n^{2}) \to (A = (A \gcd B) (m^{2} - n^{2}) \land B = (A \gcd B) 2 m n \land C = (A \gcd B) (m^{2} + n^{2})))$
128	127	reximdv	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to (\exists m \in ℕ (\frac{A}{A \gcd B} = m^{2} - n^{2} \land \frac{B}{A \gcd B} = 2 m n \land \frac{C}{A \gcd B} = m^{2} + n^{2}) \to \exists m \in ℕ (A = (A \gcd B) (m^{2} - n^{2}) \land B = (A \gcd B) 2 m n \land C = (A \gcd B) (m^{2} + n^{2})))$
129	128	reximdv	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to (\exists n \in ℕ \exists m \in ℕ (\frac{A}{A \gcd B} = m^{2} - n^{2} \land \frac{B}{A \gcd B} = 2 m n \land \frac{C}{A \gcd B} = m^{2} + n^{2}) \to \exists n \in ℕ \exists m \in ℕ (A = (A \gcd B) (m^{2} - n^{2}) \land B = (A \gcd B) 2 m n \land C = (A \gcd B) (m^{2} + n^{2})))$
130	108 129	mpd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to \exists n \in ℕ \exists m \in ℕ (A = (A \gcd B) (m^{2} - n^{2}) \land B = (A \gcd B) 2 m n \land C = (A \gcd B) (m^{2} + n^{2}))$
131		oveq1	$⊢ k = A \gcd B \to k (m^{2} - n^{2}) = (A \gcd B) (m^{2} - n^{2})$
132	131	eqeq2d	$⊢ k = A \gcd B \to (A = k (m^{2} - n^{2}) \leftrightarrow A = (A \gcd B) (m^{2} - n^{2}))$
133		oveq1	$⊢ k = A \gcd B \to k 2 m n = (A \gcd B) 2 m n$
134	133	eqeq2d	$⊢ k = A \gcd B \to (B = k 2 m n \leftrightarrow B = (A \gcd B) 2 m n)$
135		oveq1	$⊢ k = A \gcd B \to k (m^{2} + n^{2}) = (A \gcd B) (m^{2} + n^{2})$
136	135	eqeq2d	$⊢ k = A \gcd B \to (C = k (m^{2} + n^{2}) \leftrightarrow C = (A \gcd B) (m^{2} + n^{2}))$
137	132 134 136	3anbi123d	$⊢ k = A \gcd B \to ((A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \leftrightarrow (A = (A \gcd B) (m^{2} - n^{2}) \land B = (A \gcd B) 2 m n \land C = (A \gcd B) (m^{2} + n^{2})))$
138	137	2rexbidv	$⊢ k = A \gcd B \to (\exists n \in ℕ \exists m \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \leftrightarrow \exists n \in ℕ \exists m \in ℕ (A = (A \gcd B) (m^{2} - n^{2}) \land B = (A \gcd B) 2 m n \land C = (A \gcd B) (m^{2} + n^{2})))$
139	138	rspcev	$⊢ (A \gcd B \in ℕ \land \exists n \in ℕ \exists m \in ℕ (A = (A \gcd B) (m^{2} - n^{2}) \land B = (A \gcd B) 2 m n \land C = (A \gcd B) (m^{2} + n^{2}))) \to \exists k \in ℕ \exists n \in ℕ \exists m \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2}))$
140	3 130 139	syl2anc	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to \exists k \in ℕ \exists n \in ℕ \exists m \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2}))$
141		rexcom	$⊢ \exists k \in ℕ \exists n \in ℕ \exists m \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \leftrightarrow \exists n \in ℕ \exists k \in ℕ \exists m \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2}))$
142		rexcom	$⊢ \exists k \in ℕ \exists m \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \leftrightarrow \exists m \in ℕ \exists k \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2}))$
143	142	rexbii	$⊢ \exists n \in ℕ \exists k \in ℕ \exists m \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \leftrightarrow \exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2}))$
144	141 143	bitri	$⊢ \exists k \in ℕ \exists n \in ℕ \exists m \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \leftrightarrow \exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2}))$
145	140 144	sylib	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \to \exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2}))$

Metamath Proof Explorer

Theorem pythagtriplem19

Proof