Metamath Proof Explorer

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 ⊢M=C+B+C−B2
pythagtriplem15.2 ⊢N=C+B−C−B2
Assertion pythagtriplem15 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→A=M2−N2

Proof

Step Hyp Ref Expression
1 pythagtriplem15.1 ⊢M=C+B+C−B2
2 pythagtriplem15.2 ⊢N=C+B−C−B2
3 1 pythagtriplem12 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→M2=C+A2
4 2 pythagtriplem14 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→N2=C−A2
5 3 4 oveq12d ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→M2−N2=C+A2−C−A2
6 simp3 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→C∈ℕ
7 simp1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→A∈ℕ
8 6 7 nnaddcld ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→C+A∈ℕ
9 8 nncnd ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→C+A∈ℂ
10 9 3ad2ant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+A∈ℂ
11 nnz ⊢C∈ℕ→C∈ℤ
12 11 3ad2ant3 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→C∈ℤ
13 nnz ⊢A∈ℕ→A∈ℤ
14 13 3ad2ant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→A∈ℤ
15 12 14 zsubcld ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→C−A∈ℤ
16 15 zcnd ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→C−A∈ℂ
17 16 3ad2ant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C−A∈ℂ
18 2cnne0 ⊢2∈ℂ∧2≠0
19 divsubdir ⊢C+A∈ℂ∧C−A∈ℂ∧2∈ℂ∧2≠0→C+A-C−A2=C+A2−C−A2
20 18 19 mp3an3 ⊢C+A∈ℂ∧C−A∈ℂ→C+A-C−A2=C+A2−C−A2
21 10 17 20 syl2anc ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+A-C−A2=C+A2−C−A2
22 5 21 eqtr4d ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→M2−N2=C+A-C−A2
23 nncn ⊢C∈ℕ→C∈ℂ
24 23 3ad2ant3 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→C∈ℂ
25 24 3ad2ant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C∈ℂ
26 nncn ⊢A∈ℕ→A∈ℂ
27 26 3ad2ant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→A∈ℂ
28 27 3ad2ant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→A∈ℂ
29 25 28 28 pnncand ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+A-C−A=A+A
30 28 2timesd ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→2⁢A=A+A
31 29 30 eqtr4d ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+A-C−A=2⁢A
32 31 oveq1d ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+A-C−A2=2⁢A2
33 2cn ⊢2∈ℂ
34 2ne0 ⊢2≠0
35 divcan3 ⊢A∈ℂ∧2∈ℂ∧2≠0→2⁢A2=A
36 33 34 35 mp3an23 ⊢A∈ℂ→2⁢A2=A
37 28 36 syl ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→2⁢A2=A
38 22 32 37 3eqtrrd ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→A=M2−N2