pythagtriplem14

Description: Lemma for pythagtrip . Calculate the square of N . (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Hypothesis	pythagtriplem13.1	$⊢ N = \frac{\sqrt{C + B} - \sqrt{C - B}}{2}$
	Assertion	pythagtriplem14	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to N^{2} = \frac{C - A}{2}$

Proof

Step	Hyp	Ref	Expression
1		pythagtriplem13.1	$⊢ N = \frac{\sqrt{C + B} - \sqrt{C - B}}{2}$
2	1	oveq1i	$⊢ N^{2} = {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2}$
3		nncn	$⊢ C \in ℕ \to C \in ℂ$
4		nncn	$⊢ B \in ℕ \to B \in ℂ$
5		addcl	$⊢ (C \in ℂ \land B \in ℂ) \to C + B \in ℂ$
6	3 4 5	syl2anr	$⊢ (B \in ℕ \land C \in ℕ) \to C + B \in ℂ$
7	6	sqrtcld	$⊢ (B \in ℕ \land C \in ℕ) \to \sqrt{C + B} \in ℂ$
8		subcl	$⊢ (C \in ℂ \land B \in ℂ) \to C - B \in ℂ$
9	3 4 8	syl2anr	$⊢ (B \in ℕ \land C \in ℕ) \to C - B \in ℂ$
10	9	sqrtcld	$⊢ (B \in ℕ \land C \in ℕ) \to \sqrt{C - B} \in ℂ$
11	7 10	subcld	$⊢ (B \in ℕ \land C \in ℕ) \to \sqrt{C + B} - \sqrt{C - B} \in ℂ$
12	11	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to \sqrt{C + B} - \sqrt{C - B} \in ℂ$
13	12	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{C + B} - \sqrt{C - B} \in ℂ$
14		2cn	$⊢ 2 \in ℂ$
15		2ne0	$⊢ 2 \neq 0$
16		sqdiv	$⊢ (\sqrt{C + B} - \sqrt{C - B} \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2} = \frac{{(\sqrt{C + B} - \sqrt{C - B})}^{2}}{2^{2}}$
17	14 15 16	mp3an23	$⊢ \sqrt{C + B} - \sqrt{C - B} \in ℂ \to {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2} = \frac{{(\sqrt{C + B} - \sqrt{C - B})}^{2}}{2^{2}}$
18	13 17	syl	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2} = \frac{{(\sqrt{C + B} - \sqrt{C - B})}^{2}}{2^{2}}$
19	14	sqvali	$⊢ 2^{2} = 2 \cdot 2$
20	19	oveq2i	$⊢ \frac{{(\sqrt{C + B} - \sqrt{C - B})}^{2}}{2^{2}} = \frac{{(\sqrt{C + B} - \sqrt{C - B})}^{2}}{2 \cdot 2}$
21	13	sqcld	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to {(\sqrt{C + B} - \sqrt{C - B})}^{2} \in ℂ$
22		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
23		divdiv1	$⊢ ({(\sqrt{C + B} - \sqrt{C - B})}^{2} \in ℂ \land (2 \in ℂ \land 2 \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{\frac{{(\sqrt{C + B} - \sqrt{C - B})}^{2}}{2}}{2} = \frac{{(\sqrt{C + B} - \sqrt{C - B})}^{2}}{2 \cdot 2}$
24	22 22 23	mp3an23	$⊢ {(\sqrt{C + B} - \sqrt{C - B})}^{2} \in ℂ \to \frac{\frac{{(\sqrt{C + B} - \sqrt{C - B})}^{2}}{2}}{2} = \frac{{(\sqrt{C + B} - \sqrt{C - B})}^{2}}{2 \cdot 2}$
25	21 24	syl	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \frac{\frac{{(\sqrt{C + B} - \sqrt{C - B})}^{2}}{2}}{2} = \frac{{(\sqrt{C + B} - \sqrt{C - B})}^{2}}{2 \cdot 2}$
26		simp12	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to B \in ℕ$
27		simp13	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to C \in ℕ$
28	26 27 7	syl2anc	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{C + B} \in ℂ$
29	26 27 10	syl2anc	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{C - B} \in ℂ$
30		binom2sub	$⊢ (\sqrt{C + B} \in ℂ \land \sqrt{C - B} \in ℂ) \to {(\sqrt{C + B} - \sqrt{C - B})}^{2} = {\sqrt{C + B}}^{2} - 2 \sqrt{C + B} \sqrt{C - B} + {\sqrt{C - B}}^{2}$
31	28 29 30	syl2anc	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to {(\sqrt{C + B} - \sqrt{C - B})}^{2} = {\sqrt{C + B}}^{2} - 2 \sqrt{C + B} \sqrt{C - B} + {\sqrt{C - B}}^{2}$
32		nnre	$⊢ C \in ℕ \to C \in ℝ$
33		nnre	$⊢ B \in ℕ \to B \in ℝ$
34		readdcl	$⊢ (C \in ℝ \land B \in ℝ) \to C + B \in ℝ$
35	32 33 34	syl2anr	$⊢ (B \in ℕ \land C \in ℕ) \to C + B \in ℝ$
36	35	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C + B \in ℝ$
37	36	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to C + B \in ℝ$
38	37	recnd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to C + B \in ℂ$
39		resubcl	$⊢ (C \in ℝ \land B \in ℝ) \to C - B \in ℝ$
40	32 33 39	syl2anr	$⊢ (B \in ℕ \land C \in ℕ) \to C - B \in ℝ$
41	40	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C - B \in ℝ$
42	41	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to C - B \in ℝ$
43	42	recnd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to C - B \in ℂ$
44	7	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to \sqrt{C + B} \in ℂ$
45	10	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to \sqrt{C - B} \in ℂ$
46	44 45	mulcld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to \sqrt{C + B} \sqrt{C - B} \in ℂ$
47		mulcl	$⊢ (2 \in ℂ \land \sqrt{C + B} \sqrt{C - B} \in ℂ) \to 2 \sqrt{C + B} \sqrt{C - B} \in ℂ$
48	14 46 47	sylancr	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 2 \sqrt{C + B} \sqrt{C - B} \in ℂ$
49	48	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to 2 \sqrt{C + B} \sqrt{C - B} \in ℂ$
50	38 43 49	addsubd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to (C + B) + (C - B) - 2 \sqrt{C + B} \sqrt{C - B} = (C + B - 2 \sqrt{C + B} \sqrt{C - B}) + C - B$
51	27	nncnd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to C \in ℂ$
52		simp11	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to A \in ℕ$
53	52	nncnd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to A \in ℂ$
54		subdi	$⊢ (2 \in ℂ \land C \in ℂ \land A \in ℂ) \to 2 (C - A) = 2 C - 2 A$
55	14 51 53 54	mp3an2i	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to 2 (C - A) = 2 C - 2 A$
56		ppncan	$⊢ (C \in ℂ \land B \in ℂ \land C \in ℂ) \to C + B + (C - B) = C + C$
57	56	3anidm13	$⊢ (C \in ℂ \land B \in ℂ) \to C + B + (C - B) = C + C$
58		2times	$⊢ C \in ℂ \to 2 C = C + C$
59	58	adantr	$⊢ (C \in ℂ \land B \in ℂ) \to 2 C = C + C$
60	57 59	eqtr4d	$⊢ (C \in ℂ \land B \in ℂ) \to C + B + (C - B) = 2 C$
61	3 4 60	syl2anr	$⊢ (B \in ℕ \land C \in ℕ) \to C + B + (C - B) = 2 C$
62	61	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C + B + (C - B) = 2 C$
63	62	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to C + B + (C - B) = 2 C$
64	26	nncnd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to B \in ℂ$
65		subsq	$⊢ (C \in ℂ \land B \in ℂ) \to C^{2} - B^{2} = (C + B) (C - B)$
66	51 64 65	syl2anc	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to C^{2} - B^{2} = (C + B) (C - B)$
67		oveq1	$⊢ A^{2} + B^{2} = C^{2} \to A^{2} + B^{2} - B^{2} = C^{2} - B^{2}$
68	67	3ad2ant2	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to A^{2} + B^{2} - B^{2} = C^{2} - B^{2}$
69		nncn	$⊢ A \in ℕ \to A \in ℂ$
70	69	sqcld	$⊢ A \in ℕ \to A^{2} \in ℂ$
71	70	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A^{2} \in ℂ$
72	4	sqcld	$⊢ B \in ℕ \to B^{2} \in ℂ$
73	72	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B^{2} \in ℂ$
74	71 73	pncand	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A^{2} + B^{2} - B^{2} = A^{2}$
75	74	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to A^{2} + B^{2} - B^{2} = A^{2}$
76	68 75	eqtr3d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to C^{2} - B^{2} = A^{2}$
77	66 76	eqtr3d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to (C + B) (C - B) = A^{2}$
78	77	fveq2d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{(C + B) (C - B)} = \sqrt{A^{2}}$
79	32	adantl	$⊢ (B \in ℕ \land C \in ℕ) \to C \in ℝ$
80	33	adantr	$⊢ (B \in ℕ \land C \in ℕ) \to B \in ℝ$
81		nngt0	$⊢ C \in ℕ \to 0 < C$
82	81	adantl	$⊢ (B \in ℕ \land C \in ℕ) \to 0 < C$
83		nngt0	$⊢ B \in ℕ \to 0 < B$
84	83	adantr	$⊢ (B \in ℕ \land C \in ℕ) \to 0 < B$
85	79 80 82 84	addgt0d	$⊢ (B \in ℕ \land C \in ℕ) \to 0 < C + B$
86		0re	$⊢ 0 \in ℝ$
87		ltle	$⊢ (0 \in ℝ \land C + B \in ℝ) \to (0 < C + B \to 0 \leq C + B)$
88	86 87	mpan	$⊢ C + B \in ℝ \to (0 < C + B \to 0 \leq C + B)$
89	35 85 88	sylc	$⊢ (B \in ℕ \land C \in ℕ) \to 0 \leq C + B$
90	89	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 \leq C + B$
91	90	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to 0 \leq C + B$
92		pythagtriplem10	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to 0 < C - B$
93	92	3adant3	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to 0 < C - B$
94		ltle	$⊢ (0 \in ℝ \land C - B \in ℝ) \to (0 < C - B \to 0 \leq C - B)$
95	86 94	mpan	$⊢ C - B \in ℝ \to (0 < C - B \to 0 \leq C - B)$
96	42 93 95	sylc	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to 0 \leq C - B$
97	37 91 42 96	sqrtmuld	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{(C + B) (C - B)} = \sqrt{C + B} \sqrt{C - B}$
98	78 97	eqtr3d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{A^{2}} = \sqrt{C + B} \sqrt{C - B}$
99		nnre	$⊢ A \in ℕ \to A \in ℝ$
100	99	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℝ$
101	100	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to A \in ℝ$
102		nnnn0	$⊢ A \in ℕ \to A \in ℕ_{0}$
103	102	nn0ge0d	$⊢ A \in ℕ \to 0 \leq A$
104	103	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 \leq A$
105	104	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to 0 \leq A$
106	101 105	sqrtsqd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{A^{2}} = A$
107	98 106	eqtr3d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{C + B} \sqrt{C - B} = A$
108	107	oveq2d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to 2 \sqrt{C + B} \sqrt{C - B} = 2 A$
109	63 108	oveq12d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to (C + B) + (C - B) - 2 \sqrt{C + B} \sqrt{C - B} = 2 C - 2 A$
110	55 109	eqtr4d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to 2 (C - A) = (C + B) + (C - B) - 2 \sqrt{C + B} \sqrt{C - B}$
111		resqrtth	$⊢ (C + B \in ℝ \land 0 \leq C + B) \to {\sqrt{C + B}}^{2} = C + B$
112	37 91 111	syl2anc	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to {\sqrt{C + B}}^{2} = C + B$
113	112	oveq1d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to {\sqrt{C + B}}^{2} - 2 \sqrt{C + B} \sqrt{C - B} = C + B - 2 \sqrt{C + B} \sqrt{C - B}$
114		resqrtth	$⊢ (C - B \in ℝ \land 0 \leq C - B) \to {\sqrt{C - B}}^{2} = C - B$
115	42 96 114	syl2anc	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to {\sqrt{C - B}}^{2} = C - B$
116	113 115	oveq12d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to {\sqrt{C + B}}^{2} - 2 \sqrt{C + B} \sqrt{C - B} + {\sqrt{C - B}}^{2} = (C + B - 2 \sqrt{C + B} \sqrt{C - B}) + C - B$
117	50 110 116	3eqtr4rd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to {\sqrt{C + B}}^{2} - 2 \sqrt{C + B} \sqrt{C - B} + {\sqrt{C - B}}^{2} = 2 (C - A)$
118	31 117	eqtrd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to {(\sqrt{C + B} - \sqrt{C - B})}^{2} = 2 (C - A)$
119	118	oveq1d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \frac{{(\sqrt{C + B} - \sqrt{C - B})}^{2}}{2} = \frac{2 (C - A)}{2}$
120		subcl	$⊢ (C \in ℂ \land A \in ℂ) \to C - A \in ℂ$
121	3 69 120	syl2anr	$⊢ (A \in ℕ \land C \in ℕ) \to C - A \in ℂ$
122	121	3adant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C - A \in ℂ$
123	122	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to C - A \in ℂ$
124		divcan3	$⊢ (C - A \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to \frac{2 (C - A)}{2} = C - A$
125	14 15 124	mp3an23	$⊢ C - A \in ℂ \to \frac{2 (C - A)}{2} = C - A$
126	123 125	syl	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \frac{2 (C - A)}{2} = C - A$
127	119 126	eqtrd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \frac{{(\sqrt{C + B} - \sqrt{C - B})}^{2}}{2} = C - A$
128	127	oveq1d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \frac{\frac{{(\sqrt{C + B} - \sqrt{C - B})}^{2}}{2}}{2} = \frac{C - A}{2}$
129	25 128	eqtr3d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \frac{{(\sqrt{C + B} - \sqrt{C - B})}^{2}}{2 \cdot 2} = \frac{C - A}{2}$
130	20 129	syl5eq	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \frac{{(\sqrt{C + B} - \sqrt{C - B})}^{2}}{2^{2}} = \frac{C - A}{2}$
131	18 130	eqtrd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2} = \frac{C - A}{2}$
132	2 131	syl5eq	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to N^{2} = \frac{C - A}{2}$

Metamath Proof Explorer

Theorem pythagtriplem14

Proof