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 syl5ibr ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( 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 ) ) )