Theorem pythagtriplem17

Description: Lemma for pythagtrip . Show the relationship between M , N , and C . (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	pythagtriplem15.1	⊢ 𝑀 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
	pythagtriplem15.2	⊢ 𝑁 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
Assertion	pythagtriplem17	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐶 = ( ( 𝑀 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pythagtriplem15.1	⊢ 𝑀 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
2		pythagtriplem15.2	⊢ 𝑁 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
3	1	pythagtriplem12	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝑀 ↑ 2 ) = ( ( 𝐶 + 𝐴 ) / 2 ) )
4	2	pythagtriplem14	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝑁 ↑ 2 ) = ( ( 𝐶 − 𝐴 ) / 2 ) )
5	3 4	oveq12d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝑀 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) = ( ( ( 𝐶 + 𝐴 ) / 2 ) + ( ( 𝐶 − 𝐴 ) / 2 ) ) )
6		nncn	⊢ ( 𝐶 ∈ ℕ → 𝐶 ∈ ℂ )
7	6	3ad2ant3	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐶 ∈ ℂ )
8	7	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐶 ∈ ℂ )
9		nncn	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
10	9	3ad2ant1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐴 ∈ ℂ )
11	10	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐴 ∈ ℂ )
12	8 11	addcld	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 + 𝐴 ) ∈ ℂ )
13	8 11	subcld	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 − 𝐴 ) ∈ ℂ )
14		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
15		divdir	⊢ ( ( ( 𝐶 + 𝐴 ) ∈ ℂ ∧ ( 𝐶 − 𝐴 ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( 𝐶 + 𝐴 ) + ( 𝐶 − 𝐴 ) ) / 2 ) = ( ( ( 𝐶 + 𝐴 ) / 2 ) + ( ( 𝐶 − 𝐴 ) / 2 ) ) )
16	14 15	mp3an3	⊢ ( ( ( 𝐶 + 𝐴 ) ∈ ℂ ∧ ( 𝐶 − 𝐴 ) ∈ ℂ ) → ( ( ( 𝐶 + 𝐴 ) + ( 𝐶 − 𝐴 ) ) / 2 ) = ( ( ( 𝐶 + 𝐴 ) / 2 ) + ( ( 𝐶 − 𝐴 ) / 2 ) ) )
17	12 13 16	syl2anc	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( 𝐶 + 𝐴 ) + ( 𝐶 − 𝐴 ) ) / 2 ) = ( ( ( 𝐶 + 𝐴 ) / 2 ) + ( ( 𝐶 − 𝐴 ) / 2 ) ) )
18	5 17	eqtr4d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝑀 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) = ( ( ( 𝐶 + 𝐴 ) + ( 𝐶 − 𝐴 ) ) / 2 ) )
19	8 11 8	ppncand	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝐶 + 𝐴 ) + ( 𝐶 − 𝐴 ) ) = ( 𝐶 + 𝐶 ) )
20	8	2timesd	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 2 · 𝐶 ) = ( 𝐶 + 𝐶 ) )
21	19 20	eqtr4d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝐶 + 𝐴 ) + ( 𝐶 − 𝐴 ) ) = ( 2 · 𝐶 ) )
22	21	oveq1d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( 𝐶 + 𝐴 ) + ( 𝐶 − 𝐴 ) ) / 2 ) = ( ( 2 · 𝐶 ) / 2 ) )
23		2cn	⊢ 2 ∈ ℂ
24		2ne0	⊢ 2 ≠ 0
25		divcan3	⊢ ( ( 𝐶 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · 𝐶 ) / 2 ) = 𝐶 )
26	23 24 25	mp3an23	⊢ ( 𝐶 ∈ ℂ → ( ( 2 · 𝐶 ) / 2 ) = 𝐶 )
27	8 26	syl	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 2 · 𝐶 ) / 2 ) = 𝐶 )
28	18 22 27	3eqtrrd	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐶 = ( ( 𝑀 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) )