pythagtrip - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > pythagtrip		GIF version

Theorem pythagtrip 12297

Description: Parameterize the Pythagorean triples. If 𝐴, 𝐵, and 𝐶 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.)

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

Distinct variable groups: 𝐴,𝑘,𝑚,𝑛 𝐵,𝑘,𝑚,𝑛 𝐶,𝑘,𝑚,𝑛

**Proof of Theorem pythagtrip**
Step	Hyp	Ref	Expression
1		divgcdodd 12157	. . . . . . 7 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵)) ∨ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))))
2	1	3adant3 1018	. . . . . 6 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵)) ∨ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))))
3	2	adantr 276	. . . . 5 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵)) ∨ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))))
4		pythagtriplem19 12296	. . . . . . 7 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
5	4	3expia 1206	. . . . . 6 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵)) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
6		simp12 1029	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) → 𝐵 ∈ ℕ)
7		simp11 1028	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) → 𝐴 ∈ ℕ)
8		simp13 1030	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) → 𝐶 ∈ ℕ)
9		nnsqcl 10604	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℕ → (𝐴↑2) ∈ ℕ)
10	9	nncnd 8947	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℕ → (𝐴↑2) ∈ ℂ)
11	10	3ad2ant1 1019	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴↑2) ∈ ℂ)
12		nnsqcl 10604	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ℕ → (𝐵↑2) ∈ ℕ)
13	12	nncnd 8947	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℕ → (𝐵↑2) ∈ ℂ)
14	13	3ad2ant2 1020	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐵↑2) ∈ ℂ)
15	11, 14	addcomd 8122	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴↑2) + (𝐵↑2)) = ((𝐵↑2) + (𝐴↑2)))
16	15	eqeq1d 2196	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ↔ ((𝐵↑2) + (𝐴↑2)) = (𝐶↑2)))
17	16	biimpa 296	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → ((𝐵↑2) + (𝐴↑2)) = (𝐶↑2))
18	17	3adant3 1018	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) → ((𝐵↑2) + (𝐴↑2)) = (𝐶↑2))
19		nnz 9286	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℤ)
20	19	3ad2ant1 1019	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐴 ∈ ℤ)
21		nnz 9286	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ ℕ → 𝐵 ∈ ℤ)
22	21	3ad2ant2 1020	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐵 ∈ ℤ)
23	22	adantr 276	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → 𝐵 ∈ ℤ)
24		gcdcom 11988	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴))
25	20, 23, 24	syl2an2r 595	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴))
26	25	oveq2d 5904	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (𝐵 / (𝐴 gcd 𝐵)) = (𝐵 / (𝐵 gcd 𝐴)))
27	26	breq2d 4027	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (2 ∥ (𝐵 / (𝐴 gcd 𝐵)) ↔ 2 ∥ (𝐵 / (𝐵 gcd 𝐴))))
28	27	notbid 668	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵)) ↔ ¬ 2 ∥ (𝐵 / (𝐵 gcd 𝐴))))
29	28	biimp3a 1355	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) → ¬ 2 ∥ (𝐵 / (𝐵 gcd 𝐴)))
30		pythagtriplem19 12296	. . . . . . . 8 ⊢ (((𝐵 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐵↑2) + (𝐴↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐵 / (𝐵 gcd 𝐴))) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
31	6, 7, 8, 18, 29, 30	syl311anc 1262	. . . . . . 7 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
32	31	3expia 1206	. . . . . 6 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵)) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
33	5, 32	orim12d 787	. . . . 5 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → ((¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵)) ∨ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))))
34	3, 33	mpd 13	. . . 4 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
35		simplll 533	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℕ)
36		simpllr 534	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℕ)
37		nnz 9286	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
38	37	adantl 277	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
39		simplrr 536	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ ℕ) → 𝑚 ∈ ℕ)
40	39	nnzd 9388	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ ℕ) → 𝑚 ∈ ℤ)
41		zsqcl 10605	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℤ → (𝑚↑2) ∈ ℤ)
42	40, 41	syl 14	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ ℕ) → (𝑚↑2) ∈ ℤ)
43		simplrl 535	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ ℕ) → 𝑛 ∈ ℕ)
44	43	nnzd 9388	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ ℕ) → 𝑛 ∈ ℤ)
45		zsqcl 10605	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℤ → (𝑛↑2) ∈ ℤ)
46	44, 45	syl 14	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ ℕ) → (𝑛↑2) ∈ ℤ)
47	42, 46	zsubcld 9394	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ ℕ) → ((𝑚↑2) − (𝑛↑2)) ∈ ℤ)
48	38, 47	zmulcld 9395	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ ℕ) → (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∈ ℤ)
49		2z 9295	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℤ
50	49	a1i 9	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ ℕ) → 2 ∈ ℤ)
51	40, 44	zmulcld 9395	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ ℕ) → (𝑚 · 𝑛) ∈ ℤ)
52	50, 51	zmulcld 9395	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ ℕ) → (2 · (𝑚 · 𝑛)) ∈ ℤ)
53	38, 52	zmulcld 9395	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ ℕ) → (𝑘 · (2 · (𝑚 · 𝑛))) ∈ ℤ)
54		preq12bg 3785	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ ((𝑘 · ((𝑚↑2) − (𝑛↑2))) ∈ ℤ ∧ (𝑘 · (2 · (𝑚 · 𝑛))) ∈ ℤ)) → ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ↔ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2)))))))
55	35, 36, 48, 53, 54	syl22anc 1249	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ ℕ) → ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ↔ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2)))))))
56	55	anbi1d 465	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ ℕ) → (({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ (((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
57	56	rexbidva 2484	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) → (∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ ∃𝑘 ∈ ℕ (((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
58	57	2rexbidva 2510	. . . . . . 7 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
59		andir 820	. . . . . . . . . . 11 ⊢ ((((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ (((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ((𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2)))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
60		df-3an 981	. . . . . . . . . . . 12 ⊢ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
61		df-3an 981	. . . . . . . . . . . 12 ⊢ ((𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ ((𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2)))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
62	60, 61	orbi12i 765	. . . . . . . . . . 11 ⊢ (((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))) ↔ (((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ((𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2)))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
63		3ancoma 986	. . . . . . . . . . . 12 ⊢ ((𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
64	63	orbi2i 763	. . . . . . . . . . 11 ⊢ (((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))) ↔ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
65	59, 62, 64	3bitr2i 208	. . . . . . . . . 10 ⊢ ((((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
66	65	rexbii 2494	. . . . . . . . 9 ⊢ (∃𝑘 ∈ ℕ (((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ ∃𝑘 ∈ ℕ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
67	66	2rexbii 2496	. . . . . . . 8 ⊢ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
68		r19.43 2645	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ ℕ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))) ↔ (∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
69	68	2rexbii 2496	. . . . . . . . 9 ⊢ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))) ↔ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ (∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
70		r19.43 2645	. . . . . . . . . . 11 ⊢ (∃𝑚 ∈ ℕ (∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))) ↔ (∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
71	70	rexbii 2494	. . . . . . . . . 10 ⊢ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ (∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))) ↔ ∃𝑛 ∈ ℕ (∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
72		r19.43 2645	. . . . . . . . . 10 ⊢ (∃𝑛 ∈ ℕ (∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))) ↔ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
73	71, 72	bitri 184	. . . . . . . . 9 ⊢ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ (∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))) ↔ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
74	69, 73	bitri 184	. . . . . . . 8 ⊢ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))) ↔ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
75	67, 74	bitri 184	. . . . . . 7 ⊢ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
76	58, 75	bitrdi 196	. . . . . 6 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))))
77	76	3adant3 1018	. . . . 5 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))))
78	77	adantr 276	. . . 4 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))))
79	34, 78	mpbird 167	. . 3 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
80	79	ex 115	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
81		pythagtriplem2 12280	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)))
82	81	3adant3 1018	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)))
83	80, 82	impbid 129	1 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ↔ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 709 ∧ w3a 979 = wceq 1363 ∈ wcel 2158 ∃wrex 2466 {cpr 3605 class class class wbr 4015 (class class class)co 5888 ℂcc 7823 + caddc 7828 · cmul 7830 − cmin 8142 / cdiv 8643 ℕcn 8933 2c2 8984 ℤcz 9267 ↑cexp 10533 ∥ cdvds 11808 gcd cgcd 11957

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-13 2160 ax-14 2161 ax-ext 2169 ax-coll 4130 ax-sep 4133 ax-nul 4141 ax-pow 4186 ax-pr 4221 ax-un 4445 ax-setind 4548 ax-iinf 4599 ax-cnex 7916 ax-resscn 7917 ax-1cn 7918 ax-1re 7919 ax-icn 7920 ax-addcl 7921 ax-addrcl 7922 ax-mulcl 7923 ax-mulrcl 7924 ax-addcom 7925 ax-mulcom 7926 ax-addass 7927 ax-mulass 7928 ax-distr 7929 ax-i2m1 7930 ax-0lt1 7931 ax-1rid 7932 ax-0id 7933 ax-rnegex 7934 ax-precex 7935 ax-cnre 7936 ax-pre-ltirr 7937 ax-pre-ltwlin 7938 ax-pre-lttrn 7939 ax-pre-apti 7940 ax-pre-ltadd 7941 ax-pre-mulgt0 7942 ax-pre-mulext 7943 ax-arch 7944 ax-caucvg 7945

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 980 df-3an 981 df-tru 1366 df-fal 1369 df-xor 1386 df-nf 1471 df-sb 1773 df-eu 2039 df-mo 2040 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ne 2358 df-nel 2453 df-ral 2470 df-rex 2471 df-reu 2472 df-rmo 2473 df-rab 2474 df-v 2751 df-sbc 2975 df-csb 3070 df-dif 3143 df-un 3145 df-in 3147 df-ss 3154 df-nul 3435 df-if 3547 df-pw 3589 df-sn 3610 df-pr 3611 df-op 3613 df-uni 3822 df-int 3857 df-iun 3900 df-br 4016 df-opab 4077 df-mpt 4078 df-tr 4114 df-id 4305 df-po 4308 df-iso 4309 df-iord 4378 df-on 4380 df-ilim 4381 df-suc 4383 df-iom 4602 df-xp 4644 df-rel 4645 df-cnv 4646 df-co 4647 df-dm 4648 df-rn 4649 df-res 4650 df-ima 4651 df-iota 5190 df-fun 5230 df-fn 5231 df-f 5232 df-f1 5233 df-fo 5234 df-f1o 5235 df-fv 5236 df-riota 5844 df-ov 5891 df-oprab 5892 df-mpo 5893 df-1st 6155 df-2nd 6156 df-recs 6320 df-frec 6406 df-1o 6431 df-2o 6432 df-er 6549 df-en 6755 df-sup 6997 df-pnf 8008 df-mnf 8009 df-xr 8010 df-ltxr 8011 df-le 8012 df-sub 8144 df-neg 8145 df-reap 8546 df-ap 8553 df-div 8644 df-inn 8934 df-2 8992 df-3 8993 df-4 8994 df-n0 9191 df-z 9268 df-uz 9543 df-q 9634 df-rp 9668 df-fz 10023 df-fzo 10157 df-fl 10284 df-mod 10337 df-seqfrec 10460 df-exp 10534 df-cj 10865 df-re 10866 df-im 10867 df-rsqrt 11021 df-abs 11022 df-dvds 11809 df-gcd 11958 df-prm 12122

This theorem is referenced by: (None)

W3C validator