This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pythagtriplem19

Description: Lemma for pythagtrip . Introduce k and remove the relative primality requirement. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion pythagtriplem19 ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gcdnncl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
2 1 3adant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
3 2 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
4 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
5 nnz ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
6 gcddvds ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
7 4 5 6 syl2an ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
8 7 3adant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
9 8 simpld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐴 )
10 2 nnzd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℤ )
11 2 nnne0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ≠ 0 )
12 4 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐴 ∈ ℤ )
13 dvdsval2 ⊢ ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ ( 𝐴 gcd 𝐵 ) ≠ 0 ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ↔ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ) )
14 10 11 12 13 syl3anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ↔ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ) )
15 9 14 mpbid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ )
16 nnre ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ )
17 16 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐴 ∈ ℝ )
18 2 nnred ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℝ )
19 nngt0 ⊢ ( 𝐴 ∈ ℕ → 0 < 𝐴 )
20 19 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 < 𝐴 )
21 2 nngt0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 < ( 𝐴 gcd 𝐵 ) )
22 17 18 20 21 divgt0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 < ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) )
23 elnnz ⊢ ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ ↔ ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ∧ 0 < ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) )
24 15 22 23 sylanbrc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ )
25 24 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ )
26 8 simprd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐵 )
27 5 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐵 ∈ ℤ )
28 dvdsval2 ⊢ ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ ( 𝐴 gcd 𝐵 ) ≠ 0 ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ↔ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ) )
29 10 11 27 28 syl3anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ↔ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ) )
30 26 29 mpbid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ )
31 nnre ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
32 31 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐵 ∈ ℝ )
33 nngt0 ⊢ ( 𝐵 ∈ ℕ → 0 < 𝐵 )
34 33 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 < 𝐵 )
35 32 18 34 21 divgt0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 < ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) )
36 elnnz ⊢ ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ ↔ ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ∧ 0 < ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )
37 30 35 36 sylanbrc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ )
38 37 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ )
39 dvdssq ⊢ ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ↔ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ) )
40 10 12 39 syl2anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ↔ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ) )
41 dvdssq ⊢ ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ↔ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) ) )
42 10 27 41 syl2anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ↔ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) ) )
43 40 42 anbi12d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) ↔ ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) ) ) )
44 8 43 mpbid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) ) )
45 2 nnsqcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℕ )
46 45 nnzd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℤ )
47 nnsqcl ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 ↑ 2 ) ∈ ℕ )
48 47 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 ↑ 2 ) ∈ ℕ )
49 48 nnzd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 ↑ 2 ) ∈ ℤ )
50 nnsqcl ⊢ ( 𝐵 ∈ ℕ → ( 𝐵 ↑ 2 ) ∈ ℕ )
51 50 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐵 ↑ 2 ) ∈ ℕ )
52 51 nnzd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐵 ↑ 2 ) ∈ ℤ )
53 dvds2add ⊢ ( ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℤ ∧ ( 𝐴 ↑ 2 ) ∈ ℤ ∧ ( 𝐵 ↑ 2 ) ∈ ℤ ) → ( ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )
54 46 49 52 53 syl3anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )
55 44 54 mpd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
56 55 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
57 simpr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
58 56 57 breqtrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐶 ↑ 2 ) )
59 nnz ⊢ ( 𝐶 ∈ ℕ → 𝐶 ∈ ℤ )
60 59 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐶 ∈ ℤ )
61 dvdssq ⊢ ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐶 ↔ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐶 ↑ 2 ) ) )
62 10 60 61 syl2anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐶 ↔ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐶 ↑ 2 ) ) )
63 62 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐶 ↔ ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∥ ( 𝐶 ↑ 2 ) ) )
64 58 63 mpbird ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐶 )
65 dvdsval2 ⊢ ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ ( 𝐴 gcd 𝐵 ) ≠ 0 ∧ 𝐶 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐶 ↔ ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ) )
66 10 11 60 65 syl3anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐶 ↔ ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ) )
67 66 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐶 ↔ ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ) )
68 64 67 mpbid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ )
69 nnre ⊢ ( 𝐶 ∈ ℕ → 𝐶 ∈ ℝ )
70 69 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐶 ∈ ℝ )
71 nngt0 ⊢ ( 𝐶 ∈ ℕ → 0 < 𝐶 )
72 71 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 < 𝐶 )
73 70 18 72 21 divgt0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 0 < ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) )
74 73 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → 0 < ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) )
75 elnnz ⊢ ( ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ ↔ ( ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ∧ 0 < ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ) )
76 68 74 75 sylanbrc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) → ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ )
77 76 3adant3 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ )
78 48 nncnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
79 51 nncnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
80 45 nncnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ∈ ℂ )
81 45 nnne0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ≠ 0 )
82 78 79 80 81 divdird ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) ) )
83 82 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) ) )
84 nncn ⊢ ( 𝐶 ∈ ℕ → 𝐶 ∈ ℂ )
85 84 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐶 ∈ ℂ )
86 2 nncnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℂ )
87 85 86 11 sqdivd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ↑ 2 ) = ( ( 𝐶 ↑ 2 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) )
88 87 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ( ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ↑ 2 ) = ( ( 𝐶 ↑ 2 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) )
89 oveq1 ⊢ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) )
90 89 3ad2ant2 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) )
91 88 90 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ( ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) )
92 nncn ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
93 92 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐴 ∈ ℂ )
94 93 86 11 sqdivd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) )
95 nncn ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
96 95 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐵 ∈ ℂ )
97 96 86 11 sqdivd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) )
98 94 97 oveq12d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 2 ) + ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) ) )
99 98 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 2 ) + ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) / ( ( 𝐴 gcd 𝐵 ) ↑ 2 ) ) ) )
100 83 91 99 3eqtr4rd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 2 ) + ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 2 ) ) = ( ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ↑ 2 ) )
101 gcddiv ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝐴 gcd 𝐵 ) ∈ ℕ ) ∧ ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) ) → ( ( 𝐴 gcd 𝐵 ) / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) gcd ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )
102 12 27 2 8 101 syl31anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) gcd ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )
103 86 11 dividd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) / ( 𝐴 gcd 𝐵 ) ) = 1 )
104 102 103 eqtr3d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) gcd ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) = 1 )
105 104 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) gcd ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) = 1 )
106 simp3 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) )
107 pythagtriplem18 ⊢ ( ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ ∧ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ ∧ ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ ) ∧ ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 2 ) + ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 2 ) ) = ( ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ↑ 2 ) ∧ ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) gcd ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) = 1 ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) ) → ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ∧ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) = ( 2 · ( 𝑚 · 𝑛 ) ) ∧ ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) )
108 25 38 77 100 105 106 107 syl312anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ∧ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) = ( 2 · ( 𝑚 · 𝑛 ) ) ∧ ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) )
109 93 86 11 divcan2d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) · ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) = 𝐴 )
110 109 eqcomd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐴 = ( ( 𝐴 gcd 𝐵 ) · ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) )
111 96 86 11 divcan2d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) · ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) = 𝐵 )
112 111 eqcomd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐵 = ( ( 𝐴 gcd 𝐵 ) · ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )
113 85 86 11 divcan2d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) · ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ) = 𝐶 )
114 113 eqcomd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐶 = ( ( 𝐴 gcd 𝐵 ) · ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ) )
115 110 112 114 3jca ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 = ( ( 𝐴 gcd 𝐵 ) · ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) ∧ 𝐵 = ( ( 𝐴 gcd 𝐵 ) · ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) ∧ 𝐶 = ( ( 𝐴 gcd 𝐵 ) · ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ) ) )
116 115 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ( 𝐴 = ( ( 𝐴 gcd 𝐵 ) · ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) ∧ 𝐵 = ( ( 𝐴 gcd 𝐵 ) · ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) ∧ 𝐶 = ( ( 𝐴 gcd 𝐵 ) · ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ) ) )
117 oveq2 ⊢ ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) → ( ( 𝐴 gcd 𝐵 ) · ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) )
118 117 eqeq2d ⊢ ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) → ( 𝐴 = ( ( 𝐴 gcd 𝐵 ) · ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) ↔ 𝐴 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) )
119 118 3ad2ant1 ⊢ ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ∧ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) = ( 2 · ( 𝑚 · 𝑛 ) ) ∧ ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) → ( 𝐴 = ( ( 𝐴 gcd 𝐵 ) · ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) ↔ 𝐴 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) )
120 oveq2 ⊢ ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) = ( 2 · ( 𝑚 · 𝑛 ) ) → ( ( 𝐴 gcd 𝐵 ) · ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) = ( ( 𝐴 gcd 𝐵 ) · ( 2 · ( 𝑚 · 𝑛 ) ) ) )
121 120 eqeq2d ⊢ ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) = ( 2 · ( 𝑚 · 𝑛 ) ) → ( 𝐵 = ( ( 𝐴 gcd 𝐵 ) · ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) ↔ 𝐵 = ( ( 𝐴 gcd 𝐵 ) · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) )
122 121 3ad2ant2 ⊢ ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ∧ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) = ( 2 · ( 𝑚 · 𝑛 ) ) ∧ ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) → ( 𝐵 = ( ( 𝐴 gcd 𝐵 ) · ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) ↔ 𝐵 = ( ( 𝐴 gcd 𝐵 ) · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) )
123 oveq2 ⊢ ( ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) → ( ( 𝐴 gcd 𝐵 ) · ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ) = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) )
124 123 eqeq2d ⊢ ( ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) → ( 𝐶 = ( ( 𝐴 gcd 𝐵 ) · ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ) ↔ 𝐶 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
125 124 3ad2ant3 ⊢ ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ∧ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) = ( 2 · ( 𝑚 · 𝑛 ) ) ∧ ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) → ( 𝐶 = ( ( 𝐴 gcd 𝐵 ) · ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ) ↔ 𝐶 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
126 119 122 125 3anbi123d ⊢ ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ∧ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) = ( 2 · ( 𝑚 · 𝑛 ) ) ∧ ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) → ( ( 𝐴 = ( ( 𝐴 gcd 𝐵 ) · ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) ∧ 𝐵 = ( ( 𝐴 gcd 𝐵 ) · ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) ∧ 𝐶 = ( ( 𝐴 gcd 𝐵 ) · ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ) ) ↔ ( 𝐴 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( ( 𝐴 gcd 𝐵 ) · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
127 116 126 syl5ibcom ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ∧ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) = ( 2 · ( 𝑚 · 𝑛 ) ) ∧ ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) → ( 𝐴 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( ( 𝐴 gcd 𝐵 ) · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
128 127 reximdv ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ( ∃ 𝑚 ∈ ℕ ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ∧ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) = ( 2 · ( 𝑚 · 𝑛 ) ) ∧ ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) → ∃ 𝑚 ∈ ℕ ( 𝐴 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( ( 𝐴 gcd 𝐵 ) · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
129 128 reximdv ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ∧ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) = ( 2 · ( 𝑚 · 𝑛 ) ) ∧ ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) → ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( 𝐴 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( ( 𝐴 gcd 𝐵 ) · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
130 108 129 mpd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( 𝐴 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( ( 𝐴 gcd 𝐵 ) · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
131 oveq1 ⊢ ( 𝑘 = ( 𝐴 gcd 𝐵 ) → ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) )
132 131 eqeq2d ⊢ ( 𝑘 = ( 𝐴 gcd 𝐵 ) → ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ↔ 𝐴 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ) )
133 oveq1 ⊢ ( 𝑘 = ( 𝐴 gcd 𝐵 ) → ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) = ( ( 𝐴 gcd 𝐵 ) · ( 2 · ( 𝑚 · 𝑛 ) ) ) )
134 133 eqeq2d ⊢ ( 𝑘 = ( 𝐴 gcd 𝐵 ) → ( 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ↔ 𝐵 = ( ( 𝐴 gcd 𝐵 ) · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) )
135 oveq1 ⊢ ( 𝑘 = ( 𝐴 gcd 𝐵 ) → ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) )
136 135 eqeq2d ⊢ ( 𝑘 = ( 𝐴 gcd 𝐵 ) → ( 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ↔ 𝐶 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
137 132 134 136 3anbi123d ⊢ ( 𝑘 = ( 𝐴 gcd 𝐵 ) → ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ( 𝐴 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( ( 𝐴 gcd 𝐵 ) · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
138 137 2rexbidv ⊢ ( 𝑘 = ( 𝐴 gcd 𝐵 ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( 𝐴 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( ( 𝐴 gcd 𝐵 ) · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) )
139 138 rspcev ⊢ ( ( ( 𝐴 gcd 𝐵 ) ∈ ℕ ∧ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( 𝐴 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( ( 𝐴 gcd 𝐵 ) · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( ( 𝐴 gcd 𝐵 ) · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ) → ∃ 𝑘 ∈ ℕ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
140 3 130 139 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ∃ 𝑘 ∈ ℕ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
141 rexcom ⊢ ( ∃ 𝑘 ∈ ℕ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑘 ∈ ℕ ∃ 𝑚 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
142 rexcom ⊢ ( ∃ 𝑘 ∈ ℕ ∃ 𝑚 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
143 142 rexbii ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑘 ∈ ℕ ∃ 𝑚 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
144 141 143 bitri ⊢ ( ∃ 𝑘 ∈ ℕ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )
145 140 144 sylib ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) )