Metamath Proof Explorer

Theorem pythagtriplem18

Description: Lemma for pythagtrip . Wrap the previous M and N up in quantifiers. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion pythagtriplem18 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→∃n∈ℕ∃m∈ℕA=m2−n2∧B=2⁢m⁢n∧C=m2+n2

Proof

Step Hyp Ref Expression
1 eqid ⊢C+B−C−B2=C+B−C−B2
2 1 pythagtriplem13 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B−C−B2∈ℕ
3 eqid ⊢C+B+C−B2=C+B+C−B2
4 3 pythagtriplem11 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C+B+C−B2∈ℕ
5 3 1 pythagtriplem15 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→A=C+B+C−B22−C+B−C−B22
6 3 1 pythagtriplem16 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→B=2⁢C+B+C−B2⁢C+B−C−B2
7 3 1 pythagtriplem17 ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→C=C+B+C−B22+C+B−C−B22
8 oveq1 ⊢n=C+B−C−B2→n2=C+B−C−B22
9 8 oveq2d ⊢n=C+B−C−B2→m2−n2=m2−C+B−C−B22
10 9 eqeq2d ⊢n=C+B−C−B2→A=m2−n2↔A=m2−C+B−C−B22
11 oveq2 ⊢n=C+B−C−B2→m⁢n=m⁢C+B−C−B2
12 11 oveq2d ⊢n=C+B−C−B2→2⁢m⁢n=2⁢m⁢C+B−C−B2
13 12 eqeq2d ⊢n=C+B−C−B2→B=2⁢m⁢n↔B=2⁢m⁢C+B−C−B2
14 8 oveq2d ⊢n=C+B−C−B2→m2+n2=m2+C+B−C−B22
15 14 eqeq2d ⊢n=C+B−C−B2→C=m2+n2↔C=m2+C+B−C−B22
16 10 13 15 3anbi123d ⊢n=C+B−C−B2→A=m2−n2∧B=2⁢m⁢n∧C=m2+n2↔A=m2−C+B−C−B22∧B=2⁢m⁢C+B−C−B2∧C=m2+C+B−C−B22
17 oveq1 ⊢m=C+B+C−B2→m2=C+B+C−B22
18 17 oveq1d ⊢m=C+B+C−B2→m2−C+B−C−B22=C+B+C−B22−C+B−C−B22
19 18 eqeq2d ⊢m=C+B+C−B2→A=m2−C+B−C−B22↔A=C+B+C−B22−C+B−C−B22
20 oveq1 ⊢m=C+B+C−B2→m⁢C+B−C−B2=C+B+C−B2⁢C+B−C−B2
21 20 oveq2d ⊢m=C+B+C−B2→2⁢m⁢C+B−C−B2=2⁢C+B+C−B2⁢C+B−C−B2
22 21 eqeq2d ⊢m=C+B+C−B2→B=2⁢m⁢C+B−C−B2↔B=2⁢C+B+C−B2⁢C+B−C−B2
23 17 oveq1d ⊢m=C+B+C−B2→m2+C+B−C−B22=C+B+C−B22+C+B−C−B22
24 23 eqeq2d ⊢m=C+B+C−B2→C=m2+C+B−C−B22↔C=C+B+C−B22+C+B−C−B22
25 19 22 24 3anbi123d ⊢m=C+B+C−B2→A=m2−C+B−C−B22∧B=2⁢m⁢C+B−C−B2∧C=m2+C+B−C−B22↔A=C+B+C−B22−C+B−C−B22∧B=2⁢C+B+C−B2⁢C+B−C−B2∧C=C+B+C−B22+C+B−C−B22
26 16 25 rspc2ev ⊢C+B−C−B2∈ℕ∧C+B+C−B2∈ℕ∧A=C+B+C−B22−C+B−C−B22∧B=2⁢C+B+C−B2⁢C+B−C−B2∧C=C+B+C−B22+C+B−C−B22→∃n∈ℕ∃m∈ℕA=m2−n2∧B=2⁢m⁢n∧C=m2+n2
27 2 4 5 6 7 26 syl113anc ⊢A∈ℕ∧B∈ℕ∧C∈ℕ∧A2+B2=C2∧AgcdB=1∧¬2∥A→∃n∈ℕ∃m∈ℕA=m2−n2∧B=2⁢m⁢n∧C=m2+n2