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 ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( 𝐴 = ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ∧ 𝐵 = ( 2 · ( 𝑚 · 𝑛 ) ) ∧ 𝐶 = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
2 1 pythagtriplem13 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ∈ ℕ )
3 eqid ⊢ ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 )
4 3 pythagtriplem11 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ∈ ℕ )
5 3 1 pythagtriplem15 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐴 = ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) − ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) )
6 3 1 pythagtriplem16 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐵 = ( 2 · ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) ) )
7 3 1 pythagtriplem17 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐶 = ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) + ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) )
8 oveq1 ⊢ ( 𝑛 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) → ( 𝑛 ↑ 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) )
9 8 oveq2d ⊢ ( 𝑛 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) → ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) = ( ( 𝑚 ↑ 2 ) − ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) )
10 9 eqeq2d ⊢ ( 𝑛 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) → ( 𝐴 = ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ↔ 𝐴 = ( ( 𝑚 ↑ 2 ) − ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) ) )
11 oveq2 ⊢ ( 𝑛 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) → ( 𝑚 · 𝑛 ) = ( 𝑚 · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) )
12 11 oveq2d ⊢ ( 𝑛 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) → ( 2 · ( 𝑚 · 𝑛 ) ) = ( 2 · ( 𝑚 · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) ) )
13 12 eqeq2d ⊢ ( 𝑛 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) → ( 𝐵 = ( 2 · ( 𝑚 · 𝑛 ) ) ↔ 𝐵 = ( 2 · ( 𝑚 · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) ) ) )
14 8 oveq2d ⊢ ( 𝑛 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) → ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) = ( ( 𝑚 ↑ 2 ) + ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) )
15 14 eqeq2d ⊢ ( 𝑛 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) → ( 𝐶 = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ↔ 𝐶 = ( ( 𝑚 ↑ 2 ) + ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) ) )
16 10 13 15 3anbi123d ⊢ ( 𝑛 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) → ( ( 𝐴 = ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ∧ 𝐵 = ( 2 · ( 𝑚 · 𝑛 ) ) ∧ 𝐶 = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ↔ ( 𝐴 = ( ( 𝑚 ↑ 2 ) − ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) ∧ 𝐵 = ( 2 · ( 𝑚 · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) ) ∧ 𝐶 = ( ( 𝑚 ↑ 2 ) + ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) ) ) )
17 oveq1 ⊢ ( 𝑚 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) → ( 𝑚 ↑ 2 ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) )
18 17 oveq1d ⊢ ( 𝑚 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) → ( ( 𝑚 ↑ 2 ) − ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) − ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) )
19 18 eqeq2d ⊢ ( 𝑚 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) → ( 𝐴 = ( ( 𝑚 ↑ 2 ) − ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) ↔ 𝐴 = ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) − ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) ) )
20 oveq1 ⊢ ( 𝑚 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) → ( 𝑚 · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) = ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) )
21 20 oveq2d ⊢ ( 𝑚 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) → ( 2 · ( 𝑚 · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) ) = ( 2 · ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) ) )
22 21 eqeq2d ⊢ ( 𝑚 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) → ( 𝐵 = ( 2 · ( 𝑚 · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) ) ↔ 𝐵 = ( 2 · ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) ) ) )
23 17 oveq1d ⊢ ( 𝑚 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) → ( ( 𝑚 ↑ 2 ) + ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) + ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) )
24 23 eqeq2d ⊢ ( 𝑚 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) → ( 𝐶 = ( ( 𝑚 ↑ 2 ) + ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) ↔ 𝐶 = ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) + ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) ) )
25 19 22 24 3anbi123d ⊢ ( 𝑚 = ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) → ( ( 𝐴 = ( ( 𝑚 ↑ 2 ) − ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) ∧ 𝐵 = ( 2 · ( 𝑚 · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) ) ∧ 𝐶 = ( ( 𝑚 ↑ 2 ) + ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) ) ↔ ( 𝐴 = ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) − ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) ∧ 𝐵 = ( 2 · ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) ) ∧ 𝐶 = ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) + ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) ) ) )
26 16 25 rspc2ev ⊢ ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ∈ ℕ ∧ ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ∈ ℕ ∧ ( 𝐴 = ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) − ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) ∧ 𝐵 = ( 2 · ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) · ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ) ) ∧ 𝐶 = ( ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) + ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) + ( ( ( ( √ ‘ ( 𝐶 + 𝐵 ) ) − ( √ ‘ ( 𝐶 − 𝐵 ) ) ) / 2 ) ↑ 2 ) ) ) ) → ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( 𝐴 = ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ∧ 𝐵 = ( 2 · ( 𝑚 · 𝑛 ) ) ∧ 𝐶 = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) )
27 2 4 5 6 7 26 syl113anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( 𝐴 = ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ∧ 𝐵 = ( 2 · ( 𝑚 · 𝑛 ) ) ∧ 𝐶 = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) )