MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pythagtriplem19 Structured version   Visualization version   GIF version

Theorem pythagtriplem19 15908
Description: Lemma for pythagtrip 15909. Introduce 𝑘 and remove the relative primality requirement. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
Assertion
Ref Expression
pythagtriplem19 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
Distinct variable groups:   𝐴,𝑚,𝑛,𝑘   𝐵,𝑚,𝑛,𝑘   𝐶,𝑚,𝑛,𝑘

Proof of Theorem pythagtriplem19
StepHypRef Expression
1 nnz 11726 . . . . . . 7 (𝐴 ∈ ℕ → 𝐴 ∈ ℤ)
2 nnz 11726 . . . . . . 7 (𝐵 ∈ ℕ → 𝐵 ∈ ℤ)
31, 2anim12i 608 . . . . . 6 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ))
4 nnne0 11385 . . . . . . . . 9 (𝐴 ∈ ℕ → 𝐴 ≠ 0)
54neneqd 3003 . . . . . . . 8 (𝐴 ∈ ℕ → ¬ 𝐴 = 0)
65intnanrd 485 . . . . . . 7 (𝐴 ∈ ℕ → ¬ (𝐴 = 0 ∧ 𝐵 = 0))
76adantr 474 . . . . . 6 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ¬ (𝐴 = 0 ∧ 𝐵 = 0))
8 gcdn0cl 15596 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℕ)
93, 7, 8syl2anc 581 . . . . 5 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℕ)
1093adant3 1168 . . . 4 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℕ)
11103ad2ant1 1169 . . 3 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → (𝐴 gcd 𝐵) ∈ ℕ)
12 gcddvds 15597 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵))
131, 2, 12syl2an 591 . . . . . . . . . 10 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵))
14133adant3 1168 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵))
1514simpld 490 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴 gcd 𝐵) ∥ 𝐴)
1610nnzd 11808 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℤ)
1710nnne0d 11400 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴 gcd 𝐵) ≠ 0)
1813ad2ant1 1169 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐴 ∈ ℤ)
19 dvdsval2 15359 . . . . . . . . 9 (((𝐴 gcd 𝐵) ∈ ℤ ∧ (𝐴 gcd 𝐵) ≠ 0 ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ))
2016, 17, 18, 19syl3anc 1496 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ))
2115, 20mpbid 224 . . . . . . 7 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ)
22 nnre 11357 . . . . . . . . 9 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
23223ad2ant1 1169 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐴 ∈ ℝ)
2410nnred 11366 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℝ)
25 nngt0 11382 . . . . . . . . 9 (𝐴 ∈ ℕ → 0 < 𝐴)
26253ad2ant1 1169 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 < 𝐴)
2710nngt0d 11399 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 < (𝐴 gcd 𝐵))
2823, 24, 26, 27divgt0d 11288 . . . . . . 7 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 < (𝐴 / (𝐴 gcd 𝐵)))
29 elnnz 11713 . . . . . . 7 ((𝐴 / (𝐴 gcd 𝐵)) ∈ ℕ ↔ ((𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ ∧ 0 < (𝐴 / (𝐴 gcd 𝐵))))
3021, 28, 29sylanbrc 580 . . . . . 6 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴 / (𝐴 gcd 𝐵)) ∈ ℕ)
31303ad2ant1 1169 . . . . 5 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → (𝐴 / (𝐴 gcd 𝐵)) ∈ ℕ)
3214simprd 491 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴 gcd 𝐵) ∥ 𝐵)
3323ad2ant2 1170 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐵 ∈ ℤ)
34 dvdsval2 15359 . . . . . . . . 9 (((𝐴 gcd 𝐵) ∈ ℤ ∧ (𝐴 gcd 𝐵) ≠ 0 ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℤ))
3516, 17, 33, 34syl3anc 1496 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℤ))
3632, 35mpbid 224 . . . . . . 7 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐵 / (𝐴 gcd 𝐵)) ∈ ℤ)
37 nnre 11357 . . . . . . . . 9 (𝐵 ∈ ℕ → 𝐵 ∈ ℝ)
38373ad2ant2 1170 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐵 ∈ ℝ)
39 nngt0 11382 . . . . . . . . 9 (𝐵 ∈ ℕ → 0 < 𝐵)
40393ad2ant2 1170 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 < 𝐵)
4138, 24, 40, 27divgt0d 11288 . . . . . . 7 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 < (𝐵 / (𝐴 gcd 𝐵)))
42 elnnz 11713 . . . . . . 7 ((𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ ↔ ((𝐵 / (𝐴 gcd 𝐵)) ∈ ℤ ∧ 0 < (𝐵 / (𝐴 gcd 𝐵))))
4336, 41, 42sylanbrc 580 . . . . . 6 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ)
44433ad2ant1 1169 . . . . 5 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ)
45 dvdssq 15652 . . . . . . . . . . . . . . 15 (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ ((𝐴 gcd 𝐵)↑2) ∥ (𝐴↑2)))
4616, 18, 45syl2anc 581 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ ((𝐴 gcd 𝐵)↑2) ∥ (𝐴↑2)))
47 dvdssq 15652 . . . . . . . . . . . . . . 15 (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ ((𝐴 gcd 𝐵)↑2) ∥ (𝐵↑2)))
4816, 33, 47syl2anc 581 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ ((𝐴 gcd 𝐵)↑2) ∥ (𝐵↑2)))
4946, 48anbi12d 626 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵) ↔ (((𝐴 gcd 𝐵)↑2) ∥ (𝐴↑2) ∧ ((𝐴 gcd 𝐵)↑2) ∥ (𝐵↑2))))
5014, 49mpbid 224 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (((𝐴 gcd 𝐵)↑2) ∥ (𝐴↑2) ∧ ((𝐴 gcd 𝐵)↑2) ∥ (𝐵↑2)))
5110nnsqcld 13324 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 gcd 𝐵)↑2) ∈ ℕ)
5251nnzd 11808 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 gcd 𝐵)↑2) ∈ ℤ)
53 nnsqcl 13226 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℕ → (𝐴↑2) ∈ ℕ)
54533ad2ant1 1169 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴↑2) ∈ ℕ)
5554nnzd 11808 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴↑2) ∈ ℤ)
56 nnsqcl 13226 . . . . . . . . . . . . . . 15 (𝐵 ∈ ℕ → (𝐵↑2) ∈ ℕ)
57563ad2ant2 1170 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐵↑2) ∈ ℕ)
5857nnzd 11808 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐵↑2) ∈ ℤ)
59 dvds2add 15391 . . . . . . . . . . . . 13 ((((𝐴 gcd 𝐵)↑2) ∈ ℤ ∧ (𝐴↑2) ∈ ℤ ∧ (𝐵↑2) ∈ ℤ) → ((((𝐴 gcd 𝐵)↑2) ∥ (𝐴↑2) ∧ ((𝐴 gcd 𝐵)↑2) ∥ (𝐵↑2)) → ((𝐴 gcd 𝐵)↑2) ∥ ((𝐴↑2) + (𝐵↑2))))
6052, 55, 58, 59syl3anc 1496 . . . . . . . . . . . 12 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((((𝐴 gcd 𝐵)↑2) ∥ (𝐴↑2) ∧ ((𝐴 gcd 𝐵)↑2) ∥ (𝐵↑2)) → ((𝐴 gcd 𝐵)↑2) ∥ ((𝐴↑2) + (𝐵↑2))))
6150, 60mpd 15 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 gcd 𝐵)↑2) ∥ ((𝐴↑2) + (𝐵↑2)))
6261adantr 474 . . . . . . . . . 10 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → ((𝐴 gcd 𝐵)↑2) ∥ ((𝐴↑2) + (𝐵↑2)))
63 simpr 479 . . . . . . . . . 10 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))
6462, 63breqtrd 4898 . . . . . . . . 9 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → ((𝐴 gcd 𝐵)↑2) ∥ (𝐶↑2))
65 nnz 11726 . . . . . . . . . . . 12 (𝐶 ∈ ℕ → 𝐶 ∈ ℤ)
66653ad2ant3 1171 . . . . . . . . . . 11 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐶 ∈ ℤ)
67 dvdssq 15652 . . . . . . . . . . 11 (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐶 ↔ ((𝐴 gcd 𝐵)↑2) ∥ (𝐶↑2)))
6816, 66, 67syl2anc 581 . . . . . . . . . 10 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐶 ↔ ((𝐴 gcd 𝐵)↑2) ∥ (𝐶↑2)))
6968adantr 474 . . . . . . . . 9 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → ((𝐴 gcd 𝐵) ∥ 𝐶 ↔ ((𝐴 gcd 𝐵)↑2) ∥ (𝐶↑2)))
7064, 69mpbird 249 . . . . . . . 8 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (𝐴 gcd 𝐵) ∥ 𝐶)
71 dvdsval2 15359 . . . . . . . . . 10 (((𝐴 gcd 𝐵) ∈ ℤ ∧ (𝐴 gcd 𝐵) ≠ 0 ∧ 𝐶 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐶 ↔ (𝐶 / (𝐴 gcd 𝐵)) ∈ ℤ))
7216, 17, 66, 71syl3anc 1496 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐶 ↔ (𝐶 / (𝐴 gcd 𝐵)) ∈ ℤ))
7372adantr 474 . . . . . . . 8 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → ((𝐴 gcd 𝐵) ∥ 𝐶 ↔ (𝐶 / (𝐴 gcd 𝐵)) ∈ ℤ))
7470, 73mpbid 224 . . . . . . 7 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (𝐶 / (𝐴 gcd 𝐵)) ∈ ℤ)
75 nnre 11357 . . . . . . . . . 10 (𝐶 ∈ ℕ → 𝐶 ∈ ℝ)
76753ad2ant3 1171 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐶 ∈ ℝ)
77 nngt0 11382 . . . . . . . . . 10 (𝐶 ∈ ℕ → 0 < 𝐶)
78773ad2ant3 1171 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 < 𝐶)
7976, 24, 78, 27divgt0d 11288 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 < (𝐶 / (𝐴 gcd 𝐵)))
8079adantr 474 . . . . . . 7 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → 0 < (𝐶 / (𝐴 gcd 𝐵)))
81 elnnz 11713 . . . . . . 7 ((𝐶 / (𝐴 gcd 𝐵)) ∈ ℕ ↔ ((𝐶 / (𝐴 gcd 𝐵)) ∈ ℤ ∧ 0 < (𝐶 / (𝐴 gcd 𝐵))))
8274, 80, 81sylanbrc 580 . . . . . 6 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (𝐶 / (𝐴 gcd 𝐵)) ∈ ℕ)
83823adant3 1168 . . . . 5 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → (𝐶 / (𝐴 gcd 𝐵)) ∈ ℕ)
84 nncn 11358 . . . . . . . . . . 11 (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
85843ad2ant1 1169 . . . . . . . . . 10 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐴 ∈ ℂ)
8610nncnd 11367 . . . . . . . . . 10 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℂ)
8785, 86, 17sqdivd 13314 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 / (𝐴 gcd 𝐵))↑2) = ((𝐴↑2) / ((𝐴 gcd 𝐵)↑2)))
88 nncn 11358 . . . . . . . . . . 11 (𝐵 ∈ ℕ → 𝐵 ∈ ℂ)
89883ad2ant2 1170 . . . . . . . . . 10 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐵 ∈ ℂ)
9089, 86, 17sqdivd 13314 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐵 / (𝐴 gcd 𝐵))↑2) = ((𝐵↑2) / ((𝐴 gcd 𝐵)↑2)))
9187, 90oveq12d 6922 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (((𝐴 / (𝐴 gcd 𝐵))↑2) + ((𝐵 / (𝐴 gcd 𝐵))↑2)) = (((𝐴↑2) / ((𝐴 gcd 𝐵)↑2)) + ((𝐵↑2) / ((𝐴 gcd 𝐵)↑2))))
92913ad2ant1 1169 . . . . . . 7 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → (((𝐴 / (𝐴 gcd 𝐵))↑2) + ((𝐵 / (𝐴 gcd 𝐵))↑2)) = (((𝐴↑2) / ((𝐴 gcd 𝐵)↑2)) + ((𝐵↑2) / ((𝐴 gcd 𝐵)↑2))))
9354nncnd 11367 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴↑2) ∈ ℂ)
9457nncnd 11367 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐵↑2) ∈ ℂ)
9551nncnd 11367 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 gcd 𝐵)↑2) ∈ ℂ)
9651nnne0d 11400 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 gcd 𝐵)↑2) ≠ 0)
9793, 94, 95, 96divdird 11164 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (((𝐴↑2) + (𝐵↑2)) / ((𝐴 gcd 𝐵)↑2)) = (((𝐴↑2) / ((𝐴 gcd 𝐵)↑2)) + ((𝐵↑2) / ((𝐴 gcd 𝐵)↑2))))
98973ad2ant1 1169 . . . . . . 7 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → (((𝐴↑2) + (𝐵↑2)) / ((𝐴 gcd 𝐵)↑2)) = (((𝐴↑2) / ((𝐴 gcd 𝐵)↑2)) + ((𝐵↑2) / ((𝐴 gcd 𝐵)↑2))))
9992, 98eqtr4d 2863 . . . . . 6 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → (((𝐴 / (𝐴 gcd 𝐵))↑2) + ((𝐵 / (𝐴 gcd 𝐵))↑2)) = (((𝐴↑2) + (𝐵↑2)) / ((𝐴 gcd 𝐵)↑2)))
100 nncn 11358 . . . . . . . . . 10 (𝐶 ∈ ℕ → 𝐶 ∈ ℂ)
1011003ad2ant3 1171 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐶 ∈ ℂ)
102101, 86, 17sqdivd 13314 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐶 / (𝐴 gcd 𝐵))↑2) = ((𝐶↑2) / ((𝐴 gcd 𝐵)↑2)))
1031023ad2ant1 1169 . . . . . . 7 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → ((𝐶 / (𝐴 gcd 𝐵))↑2) = ((𝐶↑2) / ((𝐴 gcd 𝐵)↑2)))
104 oveq1 6911 . . . . . . . 8 (((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) → (((𝐴↑2) + (𝐵↑2)) / ((𝐴 gcd 𝐵)↑2)) = ((𝐶↑2) / ((𝐴 gcd 𝐵)↑2)))
1051043ad2ant2 1170 . . . . . . 7 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → (((𝐴↑2) + (𝐵↑2)) / ((𝐴 gcd 𝐵)↑2)) = ((𝐶↑2) / ((𝐴 gcd 𝐵)↑2)))
106103, 105eqtr4d 2863 . . . . . 6 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → ((𝐶 / (𝐴 gcd 𝐵))↑2) = (((𝐴↑2) + (𝐵↑2)) / ((𝐴 gcd 𝐵)↑2)))
10799, 106eqtr4d 2863 . . . . 5 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → (((𝐴 / (𝐴 gcd 𝐵))↑2) + ((𝐵 / (𝐴 gcd 𝐵))↑2)) = ((𝐶 / (𝐴 gcd 𝐵))↑2))
108 gcddiv 15640 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝐴 gcd 𝐵) ∈ ℕ) ∧ ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) → ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))))
10918, 33, 10, 14, 108syl31anc 1498 . . . . . . 7 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))))
11086, 17dividd 11124 . . . . . . 7 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = 1)
111109, 110eqtr3d 2862 . . . . . 6 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1)
1121113ad2ant1 1169 . . . . 5 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1)
113 simp3 1174 . . . . 5 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵)))
114 pythagtriplem18 15907 . . . . 5 ((((𝐴 / (𝐴 gcd 𝐵)) ∈ ℕ ∧ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ ∧ (𝐶 / (𝐴 gcd 𝐵)) ∈ ℕ) ∧ (((𝐴 / (𝐴 gcd 𝐵))↑2) + ((𝐵 / (𝐴 gcd 𝐵))↑2)) = ((𝐶 / (𝐴 gcd 𝐵))↑2) ∧ (((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1 ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵)))) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ((𝐴 / (𝐴 gcd 𝐵)) = ((𝑚↑2) − (𝑛↑2)) ∧ (𝐵 / (𝐴 gcd 𝐵)) = (2 · (𝑚 · 𝑛)) ∧ (𝐶 / (𝐴 gcd 𝐵)) = ((𝑚↑2) + (𝑛↑2))))
11531, 44, 83, 107, 112, 113, 114syl312anc 1516 . . . 4 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ((𝐴 / (𝐴 gcd 𝐵)) = ((𝑚↑2) − (𝑛↑2)) ∧ (𝐵 / (𝐴 gcd 𝐵)) = (2 · (𝑚 · 𝑛)) ∧ (𝐶 / (𝐴 gcd 𝐵)) = ((𝑚↑2) + (𝑛↑2))))
11685, 86, 17divcan2d 11128 . . . . . . . . . 10 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 gcd 𝐵) · (𝐴 / (𝐴 gcd 𝐵))) = 𝐴)
117116eqcomd 2830 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐴 = ((𝐴 gcd 𝐵) · (𝐴 / (𝐴 gcd 𝐵))))
11889, 86, 17divcan2d 11128 . . . . . . . . . 10 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 gcd 𝐵) · (𝐵 / (𝐴 gcd 𝐵))) = 𝐵)
119118eqcomd 2830 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐵 = ((𝐴 gcd 𝐵) · (𝐵 / (𝐴 gcd 𝐵))))
120101, 86, 17divcan2d 11128 . . . . . . . . . 10 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 gcd 𝐵) · (𝐶 / (𝐴 gcd 𝐵))) = 𝐶)
121120eqcomd 2830 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐶 = ((𝐴 gcd 𝐵) · (𝐶 / (𝐴 gcd 𝐵))))
122117, 119, 1213jca 1164 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴 = ((𝐴 gcd 𝐵) · (𝐴 / (𝐴 gcd 𝐵))) ∧ 𝐵 = ((𝐴 gcd 𝐵) · (𝐵 / (𝐴 gcd 𝐵))) ∧ 𝐶 = ((𝐴 gcd 𝐵) · (𝐶 / (𝐴 gcd 𝐵)))))
1231223ad2ant1 1169 . . . . . . 7 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → (𝐴 = ((𝐴 gcd 𝐵) · (𝐴 / (𝐴 gcd 𝐵))) ∧ 𝐵 = ((𝐴 gcd 𝐵) · (𝐵 / (𝐴 gcd 𝐵))) ∧ 𝐶 = ((𝐴 gcd 𝐵) · (𝐶 / (𝐴 gcd 𝐵)))))
124 oveq2 6912 . . . . . . . . . 10 ((𝐴 / (𝐴 gcd 𝐵)) = ((𝑚↑2) − (𝑛↑2)) → ((𝐴 gcd 𝐵) · (𝐴 / (𝐴 gcd 𝐵))) = ((𝐴 gcd 𝐵) · ((𝑚↑2) − (𝑛↑2))))
125124eqeq2d 2834 . . . . . . . . 9 ((𝐴 / (𝐴 gcd 𝐵)) = ((𝑚↑2) − (𝑛↑2)) → (𝐴 = ((𝐴 gcd 𝐵) · (𝐴 / (𝐴 gcd 𝐵))) ↔ 𝐴 = ((𝐴 gcd 𝐵) · ((𝑚↑2) − (𝑛↑2)))))
1261253ad2ant1 1169 . . . . . . . 8 (((𝐴 / (𝐴 gcd 𝐵)) = ((𝑚↑2) − (𝑛↑2)) ∧ (𝐵 / (𝐴 gcd 𝐵)) = (2 · (𝑚 · 𝑛)) ∧ (𝐶 / (𝐴 gcd 𝐵)) = ((𝑚↑2) + (𝑛↑2))) → (𝐴 = ((𝐴 gcd 𝐵) · (𝐴 / (𝐴 gcd 𝐵))) ↔ 𝐴 = ((𝐴 gcd 𝐵) · ((𝑚↑2) − (𝑛↑2)))))
127 oveq2 6912 . . . . . . . . . 10 ((𝐵 / (𝐴 gcd 𝐵)) = (2 · (𝑚 · 𝑛)) → ((𝐴 gcd 𝐵) · (𝐵 / (𝐴 gcd 𝐵))) = ((𝐴 gcd 𝐵) · (2 · (𝑚 · 𝑛))))
128127eqeq2d 2834 . . . . . . . . 9 ((𝐵 / (𝐴 gcd 𝐵)) = (2 · (𝑚 · 𝑛)) → (𝐵 = ((𝐴 gcd 𝐵) · (𝐵 / (𝐴 gcd 𝐵))) ↔ 𝐵 = ((𝐴 gcd 𝐵) · (2 · (𝑚 · 𝑛)))))
1291283ad2ant2 1170 . . . . . . . 8 (((𝐴 / (𝐴 gcd 𝐵)) = ((𝑚↑2) − (𝑛↑2)) ∧ (𝐵 / (𝐴 gcd 𝐵)) = (2 · (𝑚 · 𝑛)) ∧ (𝐶 / (𝐴 gcd 𝐵)) = ((𝑚↑2) + (𝑛↑2))) → (𝐵 = ((𝐴 gcd 𝐵) · (𝐵 / (𝐴 gcd 𝐵))) ↔ 𝐵 = ((𝐴 gcd 𝐵) · (2 · (𝑚 · 𝑛)))))
130 oveq2 6912 . . . . . . . . . 10 ((𝐶 / (𝐴 gcd 𝐵)) = ((𝑚↑2) + (𝑛↑2)) → ((𝐴 gcd 𝐵) · (𝐶 / (𝐴 gcd 𝐵))) = ((𝐴 gcd 𝐵) · ((𝑚↑2) + (𝑛↑2))))
131130eqeq2d 2834 . . . . . . . . 9 ((𝐶 / (𝐴 gcd 𝐵)) = ((𝑚↑2) + (𝑛↑2)) → (𝐶 = ((𝐴 gcd 𝐵) · (𝐶 / (𝐴 gcd 𝐵))) ↔ 𝐶 = ((𝐴 gcd 𝐵) · ((𝑚↑2) + (𝑛↑2)))))
1321313ad2ant3 1171 . . . . . . . 8 (((𝐴 / (𝐴 gcd 𝐵)) = ((𝑚↑2) − (𝑛↑2)) ∧ (𝐵 / (𝐴 gcd 𝐵)) = (2 · (𝑚 · 𝑛)) ∧ (𝐶 / (𝐴 gcd 𝐵)) = ((𝑚↑2) + (𝑛↑2))) → (𝐶 = ((𝐴 gcd 𝐵) · (𝐶 / (𝐴 gcd 𝐵))) ↔ 𝐶 = ((𝐴 gcd 𝐵) · ((𝑚↑2) + (𝑛↑2)))))
133126, 129, 1323anbi123d 1566 . . . . . . 7 (((𝐴 / (𝐴 gcd 𝐵)) = ((𝑚↑2) − (𝑛↑2)) ∧ (𝐵 / (𝐴 gcd 𝐵)) = (2 · (𝑚 · 𝑛)) ∧ (𝐶 / (𝐴 gcd 𝐵)) = ((𝑚↑2) + (𝑛↑2))) → ((𝐴 = ((𝐴 gcd 𝐵) · (𝐴 / (𝐴 gcd 𝐵))) ∧ 𝐵 = ((𝐴 gcd 𝐵) · (𝐵 / (𝐴 gcd 𝐵))) ∧ 𝐶 = ((𝐴 gcd 𝐵) · (𝐶 / (𝐴 gcd 𝐵)))) ↔ (𝐴 = ((𝐴 gcd 𝐵) · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = ((𝐴 gcd 𝐵) · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = ((𝐴 gcd 𝐵) · ((𝑚↑2) + (𝑛↑2))))))
134123, 133syl5ibcom 237 . . . . . 6 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → (((𝐴 / (𝐴 gcd 𝐵)) = ((𝑚↑2) − (𝑛↑2)) ∧ (𝐵 / (𝐴 gcd 𝐵)) = (2 · (𝑚 · 𝑛)) ∧ (𝐶 / (𝐴 gcd 𝐵)) = ((𝑚↑2) + (𝑛↑2))) → (𝐴 = ((𝐴 gcd 𝐵) · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = ((𝐴 gcd 𝐵) · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = ((𝐴 gcd 𝐵) · ((𝑚↑2) + (𝑛↑2))))))
135134reximdv 3223 . . . . 5 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → (∃𝑚 ∈ ℕ ((𝐴 / (𝐴 gcd 𝐵)) = ((𝑚↑2) − (𝑛↑2)) ∧ (𝐵 / (𝐴 gcd 𝐵)) = (2 · (𝑚 · 𝑛)) ∧ (𝐶 / (𝐴 gcd 𝐵)) = ((𝑚↑2) + (𝑛↑2))) → ∃𝑚 ∈ ℕ (𝐴 = ((𝐴 gcd 𝐵) · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = ((𝐴 gcd 𝐵) · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = ((𝐴 gcd 𝐵) · ((𝑚↑2) + (𝑛↑2))))))
136135reximdv 3223 . . . 4 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ((𝐴 / (𝐴 gcd 𝐵)) = ((𝑚↑2) − (𝑛↑2)) ∧ (𝐵 / (𝐴 gcd 𝐵)) = (2 · (𝑚 · 𝑛)) ∧ (𝐶 / (𝐴 gcd 𝐵)) = ((𝑚↑2) + (𝑛↑2))) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ (𝐴 = ((𝐴 gcd 𝐵) · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = ((𝐴 gcd 𝐵) · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = ((𝐴 gcd 𝐵) · ((𝑚↑2) + (𝑛↑2))))))
137115, 136mpd 15 . . 3 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ (𝐴 = ((𝐴 gcd 𝐵) · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = ((𝐴 gcd 𝐵) · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = ((𝐴 gcd 𝐵) · ((𝑚↑2) + (𝑛↑2)))))
138 oveq1 6911 . . . . . . 7 (𝑘 = (𝐴 gcd 𝐵) → (𝑘 · ((𝑚↑2) − (𝑛↑2))) = ((𝐴 gcd 𝐵) · ((𝑚↑2) − (𝑛↑2))))
139138eqeq2d 2834 . . . . . 6 (𝑘 = (𝐴 gcd 𝐵) → (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ↔ 𝐴 = ((𝐴 gcd 𝐵) · ((𝑚↑2) − (𝑛↑2)))))
140 oveq1 6911 . . . . . . 7 (𝑘 = (𝐴 gcd 𝐵) → (𝑘 · (2 · (𝑚 · 𝑛))) = ((𝐴 gcd 𝐵) · (2 · (𝑚 · 𝑛))))
141140eqeq2d 2834 . . . . . 6 (𝑘 = (𝐴 gcd 𝐵) → (𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ↔ 𝐵 = ((𝐴 gcd 𝐵) · (2 · (𝑚 · 𝑛)))))
142 oveq1 6911 . . . . . . 7 (𝑘 = (𝐴 gcd 𝐵) → (𝑘 · ((𝑚↑2) + (𝑛↑2))) = ((𝐴 gcd 𝐵) · ((𝑚↑2) + (𝑛↑2))))
143142eqeq2d 2834 . . . . . 6 (𝑘 = (𝐴 gcd 𝐵) → (𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))) ↔ 𝐶 = ((𝐴 gcd 𝐵) · ((𝑚↑2) + (𝑛↑2)))))
144139, 141, 1433anbi123d 1566 . . . . 5 (𝑘 = (𝐴 gcd 𝐵) → ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ (𝐴 = ((𝐴 gcd 𝐵) · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = ((𝐴 gcd 𝐵) · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = ((𝐴 gcd 𝐵) · ((𝑚↑2) + (𝑛↑2))))))
1451442rexbidv 3266 . . . 4 (𝑘 = (𝐴 gcd 𝐵) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ (𝐴 = ((𝐴 gcd 𝐵) · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = ((𝐴 gcd 𝐵) · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = ((𝐴 gcd 𝐵) · ((𝑚↑2) + (𝑛↑2))))))
146145rspcev 3525 . . 3 (((𝐴 gcd 𝐵) ∈ ℕ ∧ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ (𝐴 = ((𝐴 gcd 𝐵) · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = ((𝐴 gcd 𝐵) · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = ((𝐴 gcd 𝐵) · ((𝑚↑2) + (𝑛↑2))))) → ∃𝑘 ∈ ℕ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
14711, 137, 146syl2anc 581 . 2 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → ∃𝑘 ∈ ℕ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
148 rexcom 3308 . . 3 (∃𝑘 ∈ ℕ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ ∃𝑛 ∈ ℕ ∃𝑘 ∈ ℕ ∃𝑚 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
149 rexcom 3308 . . . 4 (∃𝑘 ∈ ℕ ∃𝑚 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
150149rexbii 3250 . . 3 (∃𝑛 ∈ ℕ ∃𝑘 ∈ ℕ ∃𝑚 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
151148, 150bitri 267 . 2 (∃𝑘 ∈ ℕ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
152147, 151sylib 210 1 (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  w3a 1113   = wceq 1658  wcel 2166  wne 2998  wrex 3117   class class class wbr 4872  (class class class)co 6904  cc 10249  cr 10250  0cc0 10251  1c1 10252   + caddc 10254   · cmul 10256   < clt 10390  cmin 10584   / cdiv 11008  cn 11349  2c2 11405  cz 11703  cexp 13153  cdvds 15356   gcd cgcd 15588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802  ax-sep 5004  ax-nul 5012  ax-pow 5064  ax-pr 5126  ax-un 7208  ax-cnex 10307  ax-resscn 10308  ax-1cn 10309  ax-icn 10310  ax-addcl 10311  ax-addrcl 10312  ax-mulcl 10313  ax-mulrcl 10314  ax-mulcom 10315  ax-addass 10316  ax-mulass 10317  ax-distr 10318  ax-i2m1 10319  ax-1ne0 10320  ax-1rid 10321  ax-rnegex 10322  ax-rrecex 10323  ax-cnre 10324  ax-pre-lttri 10325  ax-pre-lttrn 10326  ax-pre-ltadd 10327  ax-pre-mulgt0 10328  ax-pre-sup 10329
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2604  df-eu 2639  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-ne 2999  df-nel 3102  df-ral 3121  df-rex 3122  df-reu 3123  df-rmo 3124  df-rab 3125  df-v 3415  df-sbc 3662  df-csb 3757  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-pss 3813  df-nul 4144  df-if 4306  df-pw 4379  df-sn 4397  df-pr 4399  df-tp 4401  df-op 4403  df-uni 4658  df-iun 4741  df-br 4873  df-opab 4935  df-mpt 4952  df-tr 4975  df-id 5249  df-eprel 5254  df-po 5262  df-so 5263  df-fr 5300  df-we 5302  df-xp 5347  df-rel 5348  df-cnv 5349  df-co 5350  df-dm 5351  df-rn 5352  df-res 5353  df-ima 5354  df-pred 5919  df-ord 5965  df-on 5966  df-lim 5967  df-suc 5968  df-iota 6085  df-fun 6124  df-fn 6125  df-f 6126  df-f1 6127  df-fo 6128  df-f1o 6129  df-fv 6130  df-riota 6865  df-ov 6907  df-oprab 6908  df-mpt2 6909  df-om 7326  df-1st 7427  df-2nd 7428  df-wrecs 7671  df-recs 7733  df-rdg 7771  df-1o 7825  df-2o 7826  df-er 8008  df-en 8222  df-dom 8223  df-sdom 8224  df-fin 8225  df-sup 8616  df-inf 8617  df-pnf 10392  df-mnf 10393  df-xr 10394  df-ltxr 10395  df-le 10396  df-sub 10586  df-neg 10587  df-div 11009  df-nn 11350  df-2 11413  df-3 11414  df-n0 11618  df-z 11704  df-uz 11968  df-rp 12112  df-fz 12619  df-fl 12887  df-mod 12963  df-seq 13095  df-exp 13154  df-cj 14215  df-re 14216  df-im 14217  df-sqrt 14351  df-abs 14352  df-dvds 15357  df-gcd 15589  df-prm 15757
This theorem is referenced by:  pythagtrip  15909
  Copyright terms: Public domain W3C validator