Metamath Proof Explorer

Theorem pythagtriplem2

Description: Lemma for pythagtrip . Prove the full version of one direction of the theorem. (Contributed by Scott Fenton, 28-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion pythagtriplem2 ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 ovex ⊢ ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∈ V
2 ovex ⊢ ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∈ V
3 preq12bg ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∈ V ∧ ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∈ V ) ) → ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ↔ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ) ) )
4 1 2 3 mpanr12 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ↔ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ) ) )
5 4 anbi1d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ( ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
6 andir ⊢ ( ( ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ( ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
7 df-3an ⊢ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
8 df-3an ⊢ ( ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ( ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
9 7 8 orbi12i ⊢ ( ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ↔ ( ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
10 6 9 bitr4i ⊢ ( ( ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
11 5 10 bitrdi ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ) )
12 11 rexbidv ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑘 ∈ ℕ ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ∃ 𝑘 ∈ ℕ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ) )
13 12 2rexbidv ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ) )
14 r19.43 ⊢ ( ∃ 𝑘 ∈ ℕ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ↔ ( ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
15 14 2rexbii ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
16 r19.43 ⊢ ( ∃ 𝑚 ∈ ℕ ( ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ↔ ( ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
17 16 rexbii ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ ( ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
18 r19.43 ⊢ ( ∃ 𝑛 ∈ ℕ ( ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ↔ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
19 15 17 18 3bitri ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ↔ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
20 13 19 bitrdi ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ) )
21 pythagtriplem1 ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
22 21 a1i ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) )
23 3ancoma ⊢ ( ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
24 23 rexbii ⊢ ( ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
25 24 2rexbii ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
26 pythagtriplem1 ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) → ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
27 25 26 sylbi ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) → ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
28 nncn ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
29 28 sqcld ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 ↑ 2 ) ∈ ℂ )
30 nncn ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
31 30 sqcld ⊢ ( 𝐵 ∈ ℕ → ( 𝐵 ↑ 2 ) ∈ ℂ )
32 addcom ⊢ ( ( ( 𝐴 ↑ 2 ) ∈ ℂ ∧ ( 𝐵 ↑ 2 ) ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) )
33 29 31 32 syl2an ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) )
34 33 eqeq1d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ↔ ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) )
35 27 34 imbitrrid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) )
36 22 35 jaod ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) )
37 20 36 sylbid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) )