Theorem pythagtriplem15

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

	Ref	Expression
Hypotheses	pythagtriplem15.1	⊢ 𝑀 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
	pythagtriplem15.2	⊢ 𝑁 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
Assertion	pythagtriplem15	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 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		simp3	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐶 ∈ ℕ )
7		simp1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐴 ∈ ℕ )
8	6 7	nnaddcld	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 + 𝐴 ) ∈ ℕ )
9	8	nncnd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 + 𝐴 ) ∈ ℂ )
10	9	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 + 𝐴 ) ∈ ℂ )
11		nnz	⊢ ( 𝐶 ∈ ℕ → 𝐶 ∈ ℤ )
12	11	3ad2ant3	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐶 ∈ ℤ )
13		nnz	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
14	13	3ad2ant1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐴 ∈ ℤ )
15	12 14	zsubcld	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 − 𝐴 ) ∈ ℤ )
16	15	zcnd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 − 𝐴 ) ∈ ℂ )
17	16	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 − 𝐴 ) ∈ ℂ )
18		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
19		divsubdir	⊢ ( ( ( 𝐶 + 𝐴 ) ∈ ℂ ∧ ( 𝐶 − 𝐴 ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( 𝐶 + 𝐴 ) − ( 𝐶 − 𝐴 ) ) / 2 ) = ( ( ( 𝐶 + 𝐴 ) / 2 ) − ( ( 𝐶 − 𝐴 ) / 2 ) ) )
20	18 19	mp3an3	⊢ ( ( ( 𝐶 + 𝐴 ) ∈ ℂ ∧ ( 𝐶 − 𝐴 ) ∈ ℂ ) → ( ( ( 𝐶 + 𝐴 ) − ( 𝐶 − 𝐴 ) ) / 2 ) = ( ( ( 𝐶 + 𝐴 ) / 2 ) − ( ( 𝐶 − 𝐴 ) / 2 ) ) )
21	10 17 20	syl2anc	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( 𝐶 + 𝐴 ) − ( 𝐶 − 𝐴 ) ) / 2 ) = ( ( ( 𝐶 + 𝐴 ) / 2 ) − ( ( 𝐶 − 𝐴 ) / 2 ) ) )
22	5 21	eqtr4d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝑀 ↑ 2 ) − ( 𝑁 ↑ 2 ) ) = ( ( ( 𝐶 + 𝐴 ) − ( 𝐶 − 𝐴 ) ) / 2 ) )
23		nncn	⊢ ( 𝐶 ∈ ℕ → 𝐶 ∈ ℂ )
24	23	3ad2ant3	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐶 ∈ ℂ )
25	24	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐶 ∈ ℂ )
26		nncn	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
27	26	3ad2ant1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐴 ∈ ℂ )
28	27	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐴 ∈ ℂ )
29	25 28 28	pnncand	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝐶 + 𝐴 ) − ( 𝐶 − 𝐴 ) ) = ( 𝐴 + 𝐴 ) )
30	28	2timesd	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
31	29 30	eqtr4d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝐶 + 𝐴 ) − ( 𝐶 − 𝐴 ) ) = ( 2 · 𝐴 ) )
32	31	oveq1d	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( 𝐶 + 𝐴 ) − ( 𝐶 − 𝐴 ) ) / 2 ) = ( ( 2 · 𝐴 ) / 2 ) )
33		2cn	⊢ 2 ∈ ℂ
34		2ne0	⊢ 2 ≠ 0
35		divcan3	⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · 𝐴 ) / 2 ) = 𝐴 )
36	33 34 35	mp3an23	⊢ ( 𝐴 ∈ ℂ → ( ( 2 · 𝐴 ) / 2 ) = 𝐴 )
37	28 36	syl	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 2 · 𝐴 ) / 2 ) = 𝐴 )
38	22 32 37	3eqtrrd	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐴 = ( ( 𝑀 ↑ 2 ) − ( 𝑁 ↑ 2 ) ) )