Theorem 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	⊢ 𝑀 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
Assertion	pythagtriplem12	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝑀 ↑ 2 ) = ( ( 𝐶 + 𝐴 ) / 2 ) )

Proof

Step	Hyp	Ref	Expression
1		pythagtriplem11.1	⊢ 𝑀 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
2	1	oveq1i	⊢ ( 𝑀 ↑ 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 )
3		nncn	⊢ ( 𝐶 ∈ ℕ → 𝐶 ∈ ℂ )
4		nncn	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
5		addcl	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 + 𝐵 ) ∈ ℂ )
6	3 4 5	syl2anr	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 + 𝐵 ) ∈ ℂ )
7	6	3adant1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 + 𝐵 ) ∈ ℂ )
8	7	sqrtcld	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( √ ‘ ( 𝐶 + 𝐵 ) ) ∈ ℂ )
9		subcl	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
10	3 4 9	syl2anr	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
11	10	3adant1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
12	11	sqrtcld	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( √ ‘ ( 𝐶 − 𝐵 ) ) ∈ ℂ )
13	8 12	addcld	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ )
14	13	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ )
15		2cn	⊢ 2 ∈ ℂ
16		2ne0	⊢ 2 ≠ 0
17		sqdiv	⊢ ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / ( 2 ↑ 2 ) ) )
18	15 16 17	mp3an23	⊢ ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / ( 2 ↑ 2 ) ) )
19	15	sqvali	⊢ ( 2 ↑ 2 ) = ( 2 · 2 )
20	19	oveq2i	⊢ ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / ( 2 ↑ 2 ) ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / ( 2 · 2 ) )
21	18 20	eqtrdi	⊢ ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / ( 2 · 2 ) ) )
22	14 21	syl	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / ( 2 · 2 ) ) )
23	8	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( 𝐶 + 𝐵 ) ) ∈ ℂ )
24	12	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( 𝐶 − 𝐵 ) ) ∈ ℂ )
25		binom2	⊢ ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ∈ ℂ ∧ ( √ ‘ ( 𝐶 − 𝐵 ) ) ∈ ℂ ) → ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) + ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) + ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ↑ 2 ) ) )
26	23 24 25	syl2anc	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) + ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) + ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ↑ 2 ) ) )
27		nnre	⊢ ( 𝐶 ∈ ℕ → 𝐶 ∈ ℝ )
28		nnre	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
29		readdcl	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
30	27 28 29	syl2anr	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
31	30	3adant1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
32	31	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
33	27	3ad2ant3	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐶 ∈ ℝ )
34	28	3ad2ant2	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐵 ∈ ℝ )
35		nngt0	⊢ ( 𝐶 ∈ ℕ → 0 < 𝐶 )
36	35	3ad2ant3	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 < 𝐶 )
37		nngt0	⊢ ( 𝐵 ∈ ℕ → 0 < 𝐵 )
38	37	3ad2ant2	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 < 𝐵 )
39	33 34 36 38	addgt0d	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 < ( 𝐶 + 𝐵 ) )
40	39	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 < ( 𝐶 + 𝐵 ) )
41		0re	⊢ 0 ∈ ℝ
42		ltle	⊢ ( ( 0 ∈ ℝ ∧ ( 𝐶 + 𝐵 ) ∈ ℝ ) → ( 0 < ( 𝐶 + 𝐵 ) → 0 ≤ ( 𝐶 + 𝐵 ) ) )
43	41 42	mpan	⊢ ( ( 𝐶 + 𝐵 ) ∈ ℝ → ( 0 < ( 𝐶 + 𝐵 ) → 0 ≤ ( 𝐶 + 𝐵 ) ) )
44	32 40 43	sylc	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 ≤ ( 𝐶 + 𝐵 ) )
45		resqrtth	⊢ ( ( ( 𝐶 + 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐶 + 𝐵 ) ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) = ( 𝐶 + 𝐵 ) )
46	32 44 45	syl2anc	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) = ( 𝐶 + 𝐵 ) )
47	46	oveq1d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) + ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) = ( ( 𝐶 + 𝐵 ) + ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) )
48		resubcl	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
49	27 28 48	syl2anr	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
50	49	3adant1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
51	50	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
52		pythagtriplem10	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → 0 < ( 𝐶 − 𝐵 ) )
53	52	3adant3	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 < ( 𝐶 − 𝐵 ) )
54		ltle	⊢ ( ( 0 ∈ ℝ ∧ ( 𝐶 − 𝐵 ) ∈ ℝ ) → ( 0 < ( 𝐶 − 𝐵 ) → 0 ≤ ( 𝐶 − 𝐵 ) ) )
55	41 54	mpan	⊢ ( ( 𝐶 − 𝐵 ) ∈ ℝ → ( 0 < ( 𝐶 − 𝐵 ) → 0 ≤ ( 𝐶 − 𝐵 ) ) )
56	51 53 55	sylc	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 ≤ ( 𝐶 − 𝐵 ) )
57		resqrtth	⊢ ( ( ( 𝐶 − 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐶 − 𝐵 ) ) → ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ↑ 2 ) = ( 𝐶 − 𝐵 ) )
58	51 56 57	syl2anc	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ↑ 2 ) = ( 𝐶 − 𝐵 ) )
59	47 58	oveq12d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) ↑ 2 ) + ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) + ( ( √ ‘ ( 𝐶 − 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝐶 + 𝐵 ) + ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) + ( 𝐶 − 𝐵 ) ) )
60	7	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 + 𝐵 ) ∈ ℂ )
61	8 12	mulcld	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ )
62		mulcl	⊢ ( ( 2 ∈ ℂ ∧ ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ∈ ℂ ) → ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ∈ ℂ )
63	15 61 62	sylancr	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ∈ ℂ )
64	63	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ∈ ℂ )
65	11	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
66	60 64 65	add32d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( 𝐶 + 𝐵 ) + ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) + ( 𝐶 − 𝐵 ) ) = ( ( ( 𝐶 + 𝐵 ) + ( 𝐶 − 𝐵 ) ) + ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) )
67	3	3ad2ant3	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐶 ∈ ℂ )
68	67	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐶 ∈ ℂ )
69		nncn	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
70	69	3ad2ant1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐴 ∈ ℂ )
71	70	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐴 ∈ ℂ )
72		adddi	⊢ ( ( 2 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 2 · ( 𝐶 + 𝐴 ) ) = ( ( 2 · 𝐶 ) + ( 2 · 𝐴 ) ) )
73	15 68 71 72	mp3an2i	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 2 · ( 𝐶 + 𝐴 ) ) = ( ( 2 · 𝐶 ) + ( 2 · 𝐴 ) ) )
74	4	3ad2ant2	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐵 ∈ ℂ )
75	74	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐵 ∈ ℂ )
76	68 75 68	ppncand	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝐶 + 𝐵 ) + ( 𝐶 − 𝐵 ) ) = ( 𝐶 + 𝐶 ) )
77	68	2timesd	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 2 · 𝐶 ) = ( 𝐶 + 𝐶 ) )
78	76 77	eqtr4d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝐶 + 𝐵 ) + ( 𝐶 − 𝐵 ) ) = ( 2 · 𝐶 ) )
79		oveq1	⊢ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( 𝐵 ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) )
80	79	3ad2ant2	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( 𝐵 ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) )
81	71	sqcld	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
82	75	sqcld	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
83	81 82	pncand	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( 𝐵 ↑ 2 ) ) = ( 𝐴 ↑ 2 ) )
84		subsq	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = ( ( 𝐶 + 𝐵 ) · ( 𝐶 − 𝐵 ) ) )
85	68 75 84	syl2anc	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = ( ( 𝐶 + 𝐵 ) · ( 𝐶 − 𝐵 ) ) )
86	80 83 85	3eqtr3rd	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝐶 + 𝐵 ) · ( 𝐶 − 𝐵 ) ) = ( 𝐴 ↑ 2 ) )
87	86	fveq2d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( ( 𝐶 + 𝐵 ) · ( 𝐶 − 𝐵 ) ) ) = ( √ ‘ ( 𝐴 ↑ 2 ) ) )
88	32 44 51 56	sqrtmuld	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( ( 𝐶 + 𝐵 ) · ( 𝐶 − 𝐵 ) ) ) = ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) )
89		nnre	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ )
90	89	3ad2ant1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐴 ∈ ℝ )
91	90	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐴 ∈ ℝ )
92		nnnn0	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℕ0 )
93	92	nn0ge0d	⊢ ( 𝐴 ∈ ℕ → 0 ≤ 𝐴 )
94	93	3ad2ant1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 ≤ 𝐴 )
95	94	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 0 ≤ 𝐴 )
96	91 95	sqrtsqd	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( 𝐴 ↑ 2 ) ) = 𝐴 )
97	87 88 96	3eqtr3d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) = 𝐴 )
98	97	oveq2d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) = ( 2 · 𝐴 ) )
99	78 98	oveq12d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( 𝐶 + 𝐵 ) + ( 𝐶 − 𝐵 ) ) + ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) = ( ( 2 · 𝐶 ) + ( 2 · 𝐴 ) ) )
100	73 99	eqtr4d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 2 · ( 𝐶 + 𝐴 ) ) = ( ( ( 𝐶 + 𝐵 ) + ( 𝐶 − 𝐵 ) ) + ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) )
101	66 100	eqtr4d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( 𝐶 + 𝐵 ) + ( 2 · ( ( √ ‘ ( 𝐶 + 𝐵 ) ) · ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ) ) + ( 𝐶 − 𝐵 ) ) = ( 2 · ( 𝐶 + 𝐴 ) ) )
102	26 59 101	3eqtrd	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) = ( 2 · ( 𝐶 + 𝐴 ) ) )
103	102	oveq1d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / ( 2 · 2 ) ) = ( ( 2 · ( 𝐶 + 𝐴 ) ) / ( 2 · 2 ) ) )
104		addcl	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐶 + 𝐴 ) ∈ ℂ )
105	3 69 104	syl2anr	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 + 𝐴 ) ∈ ℂ )
106	105	3adant2	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 + 𝐴 ) ∈ ℂ )
107	106	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 + 𝐴 ) ∈ ℂ )
108		mulcl	⊢ ( ( 2 ∈ ℂ ∧ ( 𝐶 + 𝐴 ) ∈ ℂ ) → ( 2 · ( 𝐶 + 𝐴 ) ) ∈ ℂ )
109	15 107 108	sylancr	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 2 · ( 𝐶 + 𝐴 ) ) ∈ ℂ )
110		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
111		divdiv1	⊢ ( ( ( 2 · ( 𝐶 + 𝐴 ) ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( 2 · ( 𝐶 + 𝐴 ) ) / 2 ) / 2 ) = ( ( 2 · ( 𝐶 + 𝐴 ) ) / ( 2 · 2 ) ) )
112	110 110 111	mp3an23	⊢ ( ( 2 · ( 𝐶 + 𝐴 ) ) ∈ ℂ → ( ( ( 2 · ( 𝐶 + 𝐴 ) ) / 2 ) / 2 ) = ( ( 2 · ( 𝐶 + 𝐴 ) ) / ( 2 · 2 ) ) )
113	109 112	syl	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( 2 · ( 𝐶 + 𝐴 ) ) / 2 ) / 2 ) = ( ( 2 · ( 𝐶 + 𝐴 ) ) / ( 2 · 2 ) ) )
114	103 113	eqtr4d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) ↑ 2 ) / ( 2 · 2 ) ) = ( ( ( 2 · ( 𝐶 + 𝐴 ) ) / 2 ) / 2 ) )
115		divcan3	⊢ ( ( ( 𝐶 + 𝐴 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · ( 𝐶 + 𝐴 ) ) / 2 ) = ( 𝐶 + 𝐴 ) )
116	15 16 115	mp3an23	⊢ ( ( 𝐶 + 𝐴 ) ∈ ℂ → ( ( 2 · ( 𝐶 + 𝐴 ) ) / 2 ) = ( 𝐶 + 𝐴 ) )
117	107 116	syl	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 2 · ( 𝐶 + 𝐴 ) ) / 2 ) = ( 𝐶 + 𝐴 ) )
118	117	oveq1d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( 2 · ( 𝐶 + 𝐴 ) ) / 2 ) / 2 ) = ( ( 𝐶 + 𝐴 ) / 2 ) )
119	22 114 118	3eqtrd	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) = ( ( 𝐶 + 𝐴 ) / 2 ) )
120	2 119	eqtrid	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝑀 ↑ 2 ) = ( ( 𝐶 + 𝐴 ) / 2 ) )