Metamath Proof Explorer

Theorem pythagtrip

Description: Parameterize the Pythagorean triples. If A , B , and C are naturals, then they obey the Pythagorean triple formula iff they are parameterized by three naturals. This proof follows the Isabelle proof at http://afp.sourceforge.net/entries/Fermat3_4.shtml . This is Metamath 100 proof #23. (Contributed by Scott Fenton, 19-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 divgcdodd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∨ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )
2 1 3adant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∨ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )
3 2 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∨ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )
4 pythagtriplem19 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
5 4 3expia ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) → ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
6 simp12 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) → 𝐵 ∈ ℕ )
7 simp11 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) → 𝐴 ∈ ℕ )
8 simp13 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) → 𝐶 ∈ ℕ )
9 nnsqcl ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 ↑ 2 ) ∈ ℕ )
10 9 nncnd ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 ↑ 2 ) ∈ ℂ )
11 10 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
12 nnsqcl ⊢ ( 𝐵 ∈ ℕ → ( 𝐵 ↑ 2 ) ∈ ℕ )
13 12 nncnd ⊢ ( 𝐵 ∈ ℕ → ( 𝐵 ↑ 2 ) ∈ ℂ )
14 13 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
15 11 14 addcomd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) )
16 15 eqeq1d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ↔ ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) )
17 16 biimpa ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
18 17 3adant3 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) → ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
19 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
20 19 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐴 ∈ ℤ )
21 nnz ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
22 21 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐵 ∈ ℤ )
23 22 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → 𝐵 ∈ ℤ )
24 gcdcom ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 gcd 𝐵 ) = ( 𝐵 gcd 𝐴 ) )
25 20 23 24 syl2an2r ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( 𝐴 gcd 𝐵 ) = ( 𝐵 gcd 𝐴 ) )
26 25 oveq2d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) = ( 𝐵 / ( 𝐵 gcd 𝐴 ) ) )
27 26 breq2d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↔ 2 ∥ ( 𝐵 / ( 𝐵 gcd 𝐴 ) ) ) )
28 27 notbid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↔ ¬ 2 ∥ ( 𝐵 / ( 𝐵 gcd 𝐴 ) ) ) )
29 28 biimp3a ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) → ¬ 2 ∥ ( 𝐵 / ( 𝐵 gcd 𝐴 ) ) )
30 pythagtriplem19 ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐵 / ( 𝐵 gcd 𝐴 ) ) ) → ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
31 6 7 8 18 29 30 syl311anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) → ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
32 31 3expia ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) → ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
33 5 32 orim12d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( ( ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∨ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ) )
34 3 33 mpd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
35 ovex ⊢ ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∈ V
36 ovex ⊢ ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∈ V
37 preq12bg ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∈ V ∧ ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∈ V ) ) → ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ↔ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ) ) )
38 35 36 37 mpanr12 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ↔ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ) ) )
39 38 anbi1d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ( ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
40 39 rexbidv ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑘 ∈ ℕ ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ∃ 𝑘 ∈ ℕ ( ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
41 40 2rexbidv ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
42 andir ⊢ ( ( ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ( ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
43 df-3an ⊢ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
44 df-3an ⊢ ( ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ( ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
45 43 44 orbi12i ⊢ ( ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ↔ ( ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
46 3ancoma ⊢ ( ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
47 46 orbi2i ⊢ ( ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ↔ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
48 42 45 47 3bitr2i ⊢ ( ( ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
49 48 rexbii ⊢ ( ∃ 𝑘 ∈ ℕ ( ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ∃ 𝑘 ∈ ℕ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
50 49 2rexbii ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
51 r19.43 ⊢ ( ∃ 𝑘 ∈ ℕ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ↔ ( ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
52 51 2rexbii ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
53 r19.43 ⊢ ( ∃ 𝑚 ∈ ℕ ( ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ↔ ( ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
54 53 rexbii ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ ( ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
55 r19.43 ⊢ ( ∃ 𝑛 ∈ ℕ ( ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ↔ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
56 54 55 bitri ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ↔ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
57 52 56 bitri ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ↔ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
58 50 57 bitri ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) ∨ ( 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
59 41 58 bitrdi ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ) )
60 59 3adant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ) )
61 60 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ∨ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐵 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐴 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) ) )
62 34 61 mpbird ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
63 62 ex ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) → ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
64 pythagtriplem2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) )
65 64 3adant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) )
66 63 65 impbid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( { 𝐴 , 𝐵 } = { ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) , ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) } ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )