Theorem pythagtrip 16746

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 16621	. . . . . . 7 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵)) ∨ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))))
2	1	3adant3 1132	. . . . . 6 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵)) ∨ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))))
3	2	adantr 480	. . . . 5 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵)) ∨ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))))
4		pythagtriplem19 16745	. . . . . . 7 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
5	4	3expia 1121	. . . . . 6 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵)) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
6		simp12 1205	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) → 𝐵 ∈ ℕ)
7		simp11 1204	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) → 𝐴 ∈ ℕ)
8		simp13 1206	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) → 𝐶 ∈ ℕ)
9		nnsqcl 14035	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℕ → (𝐴↑2) ∈ ℕ)
10	9	nncnd 12144	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℕ → (𝐴↑2) ∈ ℂ)
11	10	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴↑2) ∈ ℂ)
12		nnsqcl 14035	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ℕ → (𝐵↑2) ∈ ℕ)
13	12	nncnd 12144	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℕ → (𝐵↑2) ∈ ℂ)
14	13	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐵↑2) ∈ ℂ)
15	11, 14	addcomd 11318	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴↑2) + (𝐵↑2)) = ((𝐵↑2) + (𝐴↑2)))
16	15	eqeq1d 2731	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ↔ ((𝐵↑2) + (𝐴↑2)) = (𝐶↑2)))
17	16	biimpa 476	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → ((𝐵↑2) + (𝐴↑2)) = (𝐶↑2))
18	17	3adant3 1132	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) → ((𝐵↑2) + (𝐴↑2)) = (𝐶↑2))
19		nnz 12492	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℤ)
20	19	3ad2ant1 1133	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐴 ∈ ℤ)
21		nnz 12492	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ ℕ → 𝐵 ∈ ℤ)
22	21	3ad2ant2 1134	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐵 ∈ ℤ)
23	22	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → 𝐵 ∈ ℤ)
24		gcdcom 16424	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴))
25	20, 23, 24	syl2an2r 685	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴))
26	25	oveq2d 7365	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (𝐵 / (𝐴 gcd 𝐵)) = (𝐵 / (𝐵 gcd 𝐴)))
27	26	breq2d 5104	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (2 ∥ (𝐵 / (𝐴 gcd 𝐵)) ↔ 2 ∥ (𝐵 / (𝐵 gcd 𝐴))))
28	27	notbid 318	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵)) ↔ ¬ 2 ∥ (𝐵 / (𝐵 gcd 𝐴))))
29	28	biimp3a 1471	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) → ¬ 2 ∥ (𝐵 / (𝐵 gcd 𝐴)))
30		pythagtriplem19 16745	. . . . . . . 8 ⊢ (((𝐵 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐵↑2) + (𝐴↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐵 / (𝐵 gcd 𝐴))) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
31	6, 7, 8, 18, 29, 30	syl311anc 1386	. . . . . . 7 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
32	31	3expia 1121	. . . . . 6 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵)) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
33	5, 32	orim12d 966	. . . . 5 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → ((¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵)) ∨ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))))
34	3, 33	mpd 15	. . . 4 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
35		ovex 7382	. . . . . . . . . . 11 ⊢ (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∈ V
36		ovex 7382	. . . . . . . . . . 11 ⊢ (𝑘 · (2 · (𝑚 · 𝑛))) ∈ V
37		preq12bg 4804	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ ((𝑘 · ((𝑚↑2) − (𝑛↑2))) ∈ V ∧ (𝑘 · (2 · (𝑚 · 𝑛))) ∈ V)) → ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ↔ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2)))))))
38	35, 36, 37	mpanr12 705	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ↔ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2)))))))
39	38	anbi1d 631	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ (((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
40	39	rexbidv 3153	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ ∃𝑘 ∈ ℕ (((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
41	40	2rexbidv 3194	. . . . . . 7 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
42		andir 1010	. . . . . . . . . . 11 ⊢ ((((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ (((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ((𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2)))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
43		df-3an 1088	. . . . . . . . . . . 12 ⊢ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
44		df-3an 1088	. . . . . . . . . . . 12 ⊢ ((𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ ((𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2)))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
45	43, 44	orbi12i 914	. . . . . . . . . . 11 ⊢ (((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))) ↔ (((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ((𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2)))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
46		3ancoma 1097	. . . . . . . . . . . 12 ⊢ ((𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
47	46	orbi2i 912	. . . . . . . . . . 11 ⊢ (((𝐴 = (𝑘 · ((𝑚↑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 299	. . . . . . . . . 10 ⊢ ((((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
49	48	rexbii 3076	. . . . . . . . 9 ⊢ (∃𝑘 ∈ ℕ (((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ ∃𝑘 ∈ ℕ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
50	49	2rexbii 3105	. . . . . . . 8 ⊢ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
51		r19.43 3097	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ ℕ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))) ↔ (∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
52	51	2rexbii 3105	. . . . . . . . 9 ⊢ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))) ↔ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ (∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
53		r19.43 3097	. . . . . . . . . . 11 ⊢ (∃𝑚 ∈ ℕ (∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))) ↔ (∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
54	53	rexbii 3076	. . . . . . . . . 10 ⊢ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ (∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))) ↔ ∃𝑛 ∈ ℕ (∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
55		r19.43 3097	. . . . . . . . . 10 ⊢ (∃𝑛 ∈ ℕ (∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))) ↔ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
56	54, 55	bitri 275	. . . . . . . . 9 ⊢ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ (∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))) ↔ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
57	52, 56	bitri 275	. . . . . . . 8 ⊢ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))) ↔ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
58	50, 57	bitri 275	. . . . . . 7 ⊢ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) ∨ (𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
59	41, 58	bitrdi 287	. . . . . 6 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))))
60	59	3adant3 1132	. . . . 5 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))))
61	60	adantr 480	. . . 4 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ↔ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) ∨ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐵 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐴 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))))
62	34, 61	mpbird 257	. . 3 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
63	62	ex 412	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
64		pythagtriplem2 16729	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)))
65	64	3adant3 1132	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)))
66	63, 65	impbid 212	1 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ↔ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∃wrex 3053  Vcvv 3436  {cpr 4579   class class class wbr 5092  (class class class)co 7349  ℂcc 11007   + caddc 11012   · cmul 11014   − cmin 11347   / cdiv 11777  ℕcn 12128  2c2 12183  ℤcz 12471  ↑cexp 13968   ∥ cdvds 16163   gcd cgcd 16405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086  ax-pre-sup 11087

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-1st 7924  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-1o 8388  df-2o 8389  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-fin 8876  df-sup 9332  df-inf 9333  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-div 11778  df-nn 12129  df-2 12191  df-3 12192  df-4 12193  df-n0 12385  df-z 12472  df-uz 12736  df-rp 12894  df-fz 13411  df-fl 13696  df-mod 13774  df-seq 13909  df-exp 13969  df-cj 15006  df-re 15007  df-im 15008  df-sqrt 15142  df-abs 15143  df-dvds 16164  df-gcd 16406  df-prm 16583

This theorem is referenced by: (None)