pythagtriplem12

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

		Ref	Expression
	Hypothesis	pythagtriplem11.1	$⊢ M = \frac{\sqrt{C + B} + \sqrt{C - B}}{2}$
	Assertion	pythagtriplem12	$⊢ ((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 M^{2} = \frac{C + A}{2}$

Proof

Step	Hyp	Ref	Expression
1		pythagtriplem11.1	$⊢ M = \frac{\sqrt{C + B} + \sqrt{C - B}}{2}$
2	1	oveq1i	$⊢ M^{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	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C + B \in ℂ$
8	7	sqrtcld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to \sqrt{C + B} \in ℂ$
9		subcl	$⊢ (C \in ℂ \land B \in ℂ) \to C - B \in ℂ$
10	3 4 9	syl2anr	$⊢ (B \in ℕ \land C \in ℕ) \to C - B \in ℂ$
11	10	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C - B \in ℂ$
12	11	sqrtcld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to \sqrt{C - B} \in ℂ$
13	8 12	addcld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to \sqrt{C + B} + \sqrt{C - B} \in ℂ$
14	13	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 ℂ$
15		2cn	$⊢ 2 \in ℂ$
16		2ne0	$⊢ 2 \neq 0$
17		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}}$
18	15 16 17	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}}$
19	15	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	18 20	eqtrdi	$⊢ \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 \cdot 2}$
22	14 21	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 \cdot 2}$
23	8	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} \in ℂ$
24	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} \in ℂ$
25		binom2	$⊢ (\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}$
26	23 24 25	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}$
27		nnre	$⊢ C \in ℕ \to C \in ℝ$
28		nnre	$⊢ B \in ℕ \to B \in ℝ$
29		readdcl	$⊢ (C \in ℝ \land B \in ℝ) \to C + B \in ℝ$
30	27 28 29	syl2anr	$⊢ (B \in ℕ \land C \in ℕ) \to C + B \in ℝ$
31	30	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C + B \in ℝ$
32	31	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 ℝ$
33	27	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C \in ℝ$
34	28	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B \in ℝ$
35		nngt0	$⊢ C \in ℕ \to 0 < C$
36	35	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 < C$
37		nngt0	$⊢ B \in ℕ \to 0 < B$
38	37	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 < B$
39	33 34 36 38	addgt0d	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 < C + B$
40	39	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 < C + B$
41		0re	$⊢ 0 \in ℝ$
42		ltle	$⊢ (0 \in ℝ \land C + B \in ℝ) \to (0 < C + B \to 0 \leq C + B)$
43	41 42	mpan	$⊢ C + B \in ℝ \to (0 < C + B \to 0 \leq C + B)$
44	32 40 43	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$
45		resqrtth	$⊢ (C + B \in ℝ \land 0 \leq C + B) \to {\sqrt{C + B}}^{2} = C + B$
46	32 44 45	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$
47	46	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}$
48		resubcl	$⊢ (C \in ℝ \land B \in ℝ) \to C - B \in ℝ$
49	27 28 48	syl2anr	$⊢ (B \in ℕ \land C \in ℕ) \to C - B \in ℝ$
50	49	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C - B \in ℝ$
51	50	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 ℝ$
52		pythagtriplem10	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to 0 < C - B$
53	52	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$
54		ltle	$⊢ (0 \in ℝ \land C - B \in ℝ) \to (0 < C - B \to 0 \leq C - B)$
55	41 54	mpan	$⊢ C - B \in ℝ \to (0 < C - B \to 0 \leq C - B)$
56	51 53 55	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$
57		resqrtth	$⊢ (C - B \in ℝ \land 0 \leq C - B) \to {\sqrt{C - B}}^{2} = C - B$
58	51 56 57	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$
59	47 58	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)$
60	7	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 ℂ$
61	8 12	mulcld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to \sqrt{C + B} \sqrt{C - B} \in ℂ$
62		mulcl	$⊢ (2 \in ℂ \land \sqrt{C + B} \sqrt{C - B} \in ℂ) \to 2 \sqrt{C + B} \sqrt{C - B} \in ℂ$
63	15 61 62	sylancr	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 2 \sqrt{C + B} \sqrt{C - B} \in ℂ$
64	63	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 ℂ$
65	11	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 ℂ$
66	60 64 65	add32d	$⊢ ((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) + 2 \sqrt{C + B} \sqrt{C - B} + (C - B) = (C + B) + (C - B) + 2 \sqrt{C + B} \sqrt{C - B}$
67	3	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C \in ℂ$
68	67	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 \in ℂ$
69		nncn	$⊢ A \in ℕ \to A \in ℂ$
70	69	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℂ$
71	70	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 ℂ$
72		adddi	$⊢ (2 \in ℂ \land C \in ℂ \land A \in ℂ) \to 2 (C + A) = 2 C + 2 A$
73	15 68 71 72	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$
74	4	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B \in ℂ$
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 B \in ℂ$
76	68 75 68	ppncand	$⊢ ((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) = C + C$
77	68	2timesd	$⊢ ((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 = C + C$
78	76 77	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 C + B + (C - B) = 2 C$
79		oveq1	$⊢ A^{2} + B^{2} = C^{2} \to A^{2} + B^{2} - B^{2} = C^{2} - B^{2}$
80	79	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}$
81	71	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 A^{2} \in ℂ$
82	75	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 B^{2} \in ℂ$
83	81 82	pncand	$⊢ ((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}$
84		subsq	$⊢ (C \in ℂ \land B \in ℂ) \to C^{2} - B^{2} = (C + B) (C - B)$
85	68 75 84	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)$
86	80 83 85	3eqtr3rd	$⊢ ((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}$
87	86	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}}$
88	32 44 51 56	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}$
89		nnre	$⊢ A \in ℕ \to A \in ℝ$
90	89	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℝ$
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 A \in ℝ$
92		nnnn0	$⊢ A \in ℕ \to A \in ℕ_{0}$
93	92	nn0ge0d	$⊢ A \in ℕ \to 0 \leq A$
94	93	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 \leq A$
95	94	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$
96	91 95	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$
97	87 88 96	3eqtr3d	$⊢ ((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$
98	97	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$
99	78 98	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$
100	73 99	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}$
101	66 100	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 (C + B) + 2 \sqrt{C + B} \sqrt{C - B} + (C - B) = 2 (C + A)$
102	26 59 101	3eqtrd	$⊢ ((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)$
103	102	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 \cdot 2} = \frac{2 (C + A)}{2 \cdot 2}$
104		addcl	$⊢ (C \in ℂ \land A \in ℂ) \to C + A \in ℂ$
105	3 69 104	syl2anr	$⊢ (A \in ℕ \land C \in ℕ) \to C + A \in ℂ$
106	105	3adant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C + A \in ℂ$
107	106	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 ℂ$
108		mulcl	$⊢ (2 \in ℂ \land C + A \in ℂ) \to 2 (C + A) \in ℂ$
109	15 107 108	sylancr	$⊢ ((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) \in ℂ$
110		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
111		divdiv1	$⊢ (2 (C + A) \in ℂ \land (2 \in ℂ \land 2 \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{\frac{2 (C + A)}{2}}{2} = \frac{2 (C + A)}{2 \cdot 2}$
112	110 110 111	mp3an23	$⊢ 2 (C + A) \in ℂ \to \frac{\frac{2 (C + A)}{2}}{2} = \frac{2 (C + A)}{2 \cdot 2}$
113	109 112	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{2 (C + A)}{2}}{2} = \frac{2 (C + A)}{2 \cdot 2}$
114	103 113	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 \frac{{(\sqrt{C + B} + \sqrt{C - B})}^{2}}{2 \cdot 2} = \frac{\frac{2 (C + A)}{2}}{2}$
115		divcan3	$⊢ (C + A \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to \frac{2 (C + A)}{2} = C + A$
116	15 16 115	mp3an23	$⊢ C + A \in ℂ \to \frac{2 (C + A)}{2} = C + A$
117	107 116	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$
118	117	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{2 (C + A)}{2}}{2} = \frac{C + A}{2}$
119	22 114 118	3eqtrd	$⊢ ((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}$
120	2 119	eqtrid	$⊢ ((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 M^{2} = \frac{C + A}{2}$

Metamath Proof Explorer

Theorem pythagtriplem12

Proof