Metamath Proof Explorer

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 ⊢M=C+B+C−B2
pythagtriplem15.2 ⊢N=C+B−C−B2
Assertion pythagtriplem17 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C=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 nncn ⊢C∈ℕ→C∈ℂ
7 6 3ad2ant3 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→C∈ℂ
8 7 3ad2ant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C∈ℂ
9 nncn ⊢A∈ℕ→A∈ℂ
10 9 3ad2ant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→A∈ℂ
11 10 3ad2ant1 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→A∈ℂ
12 8 11 addcld ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+A∈ℂ
13 8 11 subcld ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C−A∈ℂ
14 2cnne0 ⊢2∈ℂ∧2≠0
15 divdir ⊢C+A∈ℂ∧C−A∈ℂ∧2∈ℂ∧2≠0→C+A+C−A2=C+A2+C−A2
16 14 15 mp3an3 ⊢C+A∈ℂ∧C−A∈ℂ→C+A+C−A2=C+A2+C−A2
17 12 13 16 syl2anc ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+A+C−A2=C+A2+C−A2
18 5 17 eqtr4d ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→M2+N2=C+A+C−A2
19 8 11 8 ppncand ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+A+C−A=C+C
20 8 2timesd ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→2⁢C=C+C
21 19 20 eqtr4d ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+A+C−A=2⁢C
22 21 oveq1d ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+A+C−A2=2⁢C2
23 2cn ⊢2∈ℂ
24 2ne0 ⊢2≠0
25 divcan3 ⊢C∈ℂ∧2∈ℂ∧2≠0→2⁢C2=C
26 23 24 25 mp3an23 ⊢C∈ℂ→2⁢C2=C
27 8 26 syl ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→2⁢C2=C
28 18 22 27 3eqtrrd ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C=M2+N2