pythagtriplem14 - Metamath Proof Explorer

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

Theorem pythagtriplem14 16862

Description: Lemma for pythagtrip 16868. Calculate the square of 𝑁. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)

**Hypothesis**
Ref	Expression
pythagtriplem13.1	⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)

**Assertion**
Ref	Expression
pythagtriplem14	⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑁↑2) = ((𝐶 − 𝐴) / 2))

**Proof of Theorem pythagtriplem14**
Step	Hyp	Ref	Expression
1		pythagtriplem13.1	. . 3 ⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)
2	1	oveq1i 7441	. 2 ⊢ (𝑁↑2) = ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)↑2)
3		nncn 12272	. . . . . . . . 9 ⊢ (𝐶 ∈ ℕ → 𝐶 ∈ ℂ)
4		nncn 12272	. . . . . . . . 9 ⊢ (𝐵 ∈ ℕ → 𝐵 ∈ ℂ)
5		addcl 11235	. . . . . . . . 9 ⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐶 + 𝐵) ∈ ℂ)
6	3, 4, 5	syl2anr 597	. . . . . . . 8 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 + 𝐵) ∈ ℂ)
7	6	sqrtcld 15473	. . . . . . 7 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (√‘(𝐶 + 𝐵)) ∈ ℂ)
8		subcl 11505	. . . . . . . . 9 ⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐶 − 𝐵) ∈ ℂ)
9	3, 4, 8	syl2anr 597	. . . . . . . 8 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 − 𝐵) ∈ ℂ)
10	9	sqrtcld 15473	. . . . . . 7 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (√‘(𝐶 − 𝐵)) ∈ ℂ)
11	7, 10	subcld 11618	. . . . . 6 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) ∈ ℂ)
12	11	3adant1 1129	. . . . 5 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) ∈ ℂ)
13	12	3ad2ant1 1132	. . . 4 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) ∈ ℂ)
14		2cn 12339	. . . . 5 ⊢ 2 ∈ ℂ
15		2ne0 12368	. . . . 5 ⊢ 2 ≠ 0
16		sqdiv 14158	. . . . 5 ⊢ ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)↑2) = ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / (2↑2)))
17	14, 15, 16	mp3an23 1452	. . . 4 ⊢ (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) ∈ ℂ → ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)↑2) = ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / (2↑2)))
18	13, 17	syl 17	. . 3 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)↑2) = ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / (2↑2)))
19	14	sqvali 14216	. . . . 5 ⊢ (2↑2) = (2 · 2)
20	19	oveq2i 7442	. . . 4 ⊢ ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / (2↑2)) = ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / (2 · 2))
21	13	sqcld 14181	. . . . . 6 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) ∈ ℂ)
22		2cnne0 12474	. . . . . . 7 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
23		divdiv1 11976	. . . . . . 7 ⊢ (((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / 2) / 2) = ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / (2 · 2)))
24	22, 22, 23	mp3an23 1452	. . . . . 6 ⊢ ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) ∈ ℂ → (((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / 2) / 2) = ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / (2 · 2)))
25	21, 24	syl 17	. . . . 5 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / 2) / 2) = ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / (2 · 2)))
26		simp12 1203	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐵 ∈ ℕ)
27		simp13 1204	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐶 ∈ ℕ)
28	26, 27, 7	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 + 𝐵)) ∈ ℂ)
29	26, 27, 10	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 − 𝐵)) ∈ ℂ)
30		binom2sub 14256	. . . . . . . . . 10 ⊢ (((√‘(𝐶 + 𝐵)) ∈ ℂ ∧ (√‘(𝐶 − 𝐵)) ∈ ℂ) → (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) = ((((√‘(𝐶 + 𝐵))↑2) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) + ((√‘(𝐶 − 𝐵))↑2)))
31	28, 29, 30	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) = ((((√‘(𝐶 + 𝐵))↑2) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) + ((√‘(𝐶 − 𝐵))↑2)))
32		nnre 12271	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∈ ℕ → 𝐶 ∈ ℝ)
33		nnre 12271	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ ℕ → 𝐵 ∈ ℝ)
34		readdcl 11236	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 + 𝐵) ∈ ℝ)
35	32, 33, 34	syl2anr 597	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 + 𝐵) ∈ ℝ)
36	35	3adant1 1129	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 + 𝐵) ∈ ℝ)
37	36	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 + 𝐵) ∈ ℝ)
38	37	recnd 11287	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 + 𝐵) ∈ ℂ)
39		resubcl 11571	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 − 𝐵) ∈ ℝ)
40	32, 33, 39	syl2anr 597	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 − 𝐵) ∈ ℝ)
41	40	3adant1 1129	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 − 𝐵) ∈ ℝ)
42	41	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 − 𝐵) ∈ ℝ)
43	42	recnd 11287	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 − 𝐵) ∈ ℂ)
44	7	3adant1 1129	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (√‘(𝐶 + 𝐵)) ∈ ℂ)
45	10	3adant1 1129	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (√‘(𝐶 − 𝐵)) ∈ ℂ)
46	44, 45	mulcld 11279	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))) ∈ ℂ)
47		mulcl 11237	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))) ∈ ℂ) → (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵)))) ∈ ℂ)
48	14, 46, 47	sylancr 587	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵)))) ∈ ℂ)
49	48	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵)))) ∈ ℂ)
50	38, 43, 49	addsubd 11639	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((𝐶 + 𝐵) + (𝐶 − 𝐵)) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) = (((𝐶 + 𝐵) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) + (𝐶 − 𝐵)))
51	27	nncnd 12280	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐶 ∈ ℂ)
52		simp11 1202	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐴 ∈ ℕ)
53	52	nncnd 12280	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐴 ∈ ℂ)
54		subdi 11694	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (2 · (𝐶 − 𝐴)) = ((2 · 𝐶) − (2 · 𝐴)))
55	14, 51, 53, 54	mp3an2i 1465	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (2 · (𝐶 − 𝐴)) = ((2 · 𝐶) − (2 · 𝐴)))
56		ppncan 11549	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐶 + 𝐵) + (𝐶 − 𝐵)) = (𝐶 + 𝐶))
57	56	3anidm13 1419	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐶 + 𝐵) + (𝐶 − 𝐵)) = (𝐶 + 𝐶))
58		2times 12400	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 ∈ ℂ → (2 · 𝐶) = (𝐶 + 𝐶))
59	58	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2 · 𝐶) = (𝐶 + 𝐶))
60	57, 59	eqtr4d 2778	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐶 + 𝐵) + (𝐶 − 𝐵)) = (2 · 𝐶))
61	3, 4, 60	syl2anr 597	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐶 + 𝐵) + (𝐶 − 𝐵)) = (2 · 𝐶))
62	61	3adant1 1129	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐶 + 𝐵) + (𝐶 − 𝐵)) = (2 · 𝐶))
63	62	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((𝐶 + 𝐵) + (𝐶 − 𝐵)) = (2 · 𝐶))
64	26	nncnd 12280	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐵 ∈ ℂ)
65		subsq 14246	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐶↑2) − (𝐵↑2)) = ((𝐶 + 𝐵) · (𝐶 − 𝐵)))
66	51, 64, 65	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((𝐶↑2) − (𝐵↑2)) = ((𝐶 + 𝐵) · (𝐶 − 𝐵)))
67		oveq1 7438	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) → (((𝐴↑2) + (𝐵↑2)) − (𝐵↑2)) = ((𝐶↑2) − (𝐵↑2)))
68	67	3ad2ant2 1133	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((𝐴↑2) + (𝐵↑2)) − (𝐵↑2)) = ((𝐶↑2) − (𝐵↑2)))
69		nncn 12272	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
70	69	sqcld 14181	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ ℕ → (𝐴↑2) ∈ ℂ)
71	70	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴↑2) ∈ ℂ)
72	4	sqcld 14181	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐵 ∈ ℕ → (𝐵↑2) ∈ ℂ)
73	72	3ad2ant2 1133	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐵↑2) ∈ ℂ)
74	71, 73	pncand 11619	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (((𝐴↑2) + (𝐵↑2)) − (𝐵↑2)) = (𝐴↑2))
75	74	3ad2ant1 1132	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((𝐴↑2) + (𝐵↑2)) − (𝐵↑2)) = (𝐴↑2))
76	68, 75	eqtr3d 2777	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((𝐶↑2) − (𝐵↑2)) = (𝐴↑2))
77	66, 76	eqtr3d 2777	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((𝐶 + 𝐵) · (𝐶 − 𝐵)) = (𝐴↑2))
78	77	fveq2d 6911	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘((𝐶 + 𝐵) · (𝐶 − 𝐵))) = (√‘(𝐴↑2)))
79	32	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐶 ∈ ℝ)
80	33	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐵 ∈ ℝ)
81		nngt0 12295	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐶 ∈ ℕ → 0 < 𝐶)
82	81	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 < 𝐶)
83		nngt0 12295	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐵 ∈ ℕ → 0 < 𝐵)
84	83	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 < 𝐵)
85	79, 80, 82, 84	addgt0d 11836	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 < (𝐶 + 𝐵))
86		0re 11261	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ ℝ
87		ltle 11347	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((0 ∈ ℝ ∧ (𝐶 + 𝐵) ∈ ℝ) → (0 < (𝐶 + 𝐵) → 0 ≤ (𝐶 + 𝐵)))
88	86, 87	mpan 690	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 + 𝐵) ∈ ℝ → (0 < (𝐶 + 𝐵) → 0 ≤ (𝐶 + 𝐵)))
89	35, 85, 88	sylc 65	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 ≤ (𝐶 + 𝐵))
90	89	3adant1 1129	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 ≤ (𝐶 + 𝐵))
91	90	3ad2ant1 1132	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 0 ≤ (𝐶 + 𝐵))
92		pythagtriplem10 16854	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → 0 < (𝐶 − 𝐵))
93	92	3adant3 1131	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 0 < (𝐶 − 𝐵))
94		ltle 11347	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℝ ∧ (𝐶 − 𝐵) ∈ ℝ) → (0 < (𝐶 − 𝐵) → 0 ≤ (𝐶 − 𝐵)))
95	86, 94	mpan 690	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 − 𝐵) ∈ ℝ → (0 < (𝐶 − 𝐵) → 0 ≤ (𝐶 − 𝐵)))
96	42, 93, 95	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 0 ≤ (𝐶 − 𝐵))
97	37, 91, 42, 96	sqrtmuld 15460	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘((𝐶 + 𝐵) · (𝐶 − 𝐵))) = ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))
98	78, 97	eqtr3d 2777	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐴↑2)) = ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))
99		nnre 12271	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
100	99	3ad2ant1 1132	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐴 ∈ ℝ)
101	100	3ad2ant1 1132	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐴 ∈ ℝ)
102		nnnn0 12531	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ₀)
103	102	nn0ge0d 12588	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℕ → 0 ≤ 𝐴)
104	103	3ad2ant1 1132	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 ≤ 𝐴)
105	104	3ad2ant1 1132	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 0 ≤ 𝐴)
106	101, 105	sqrtsqd 15455	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐴↑2)) = 𝐴)
107	98, 106	eqtr3d 2777	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))) = 𝐴)
108	107	oveq2d 7447	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵)))) = (2 · 𝐴))
109	63, 108	oveq12d 7449	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((𝐶 + 𝐵) + (𝐶 − 𝐵)) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) = ((2 · 𝐶) − (2 · 𝐴)))
110	55, 109	eqtr4d 2778	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (2 · (𝐶 − 𝐴)) = (((𝐶 + 𝐵) + (𝐶 − 𝐵)) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))))
111		resqrtth 15291	. . . . . . . . . . . . 13 ⊢ (((𝐶 + 𝐵) ∈ ℝ ∧ 0 ≤ (𝐶 + 𝐵)) → ((√‘(𝐶 + 𝐵))↑2) = (𝐶 + 𝐵))
112	37, 91, 111	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((√‘(𝐶 + 𝐵))↑2) = (𝐶 + 𝐵))
113	112	oveq1d 7446	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((√‘(𝐶 + 𝐵))↑2) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) = ((𝐶 + 𝐵) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))))
114		resqrtth 15291	. . . . . . . . . . . 12 ⊢ (((𝐶 − 𝐵) ∈ ℝ ∧ 0 ≤ (𝐶 − 𝐵)) → ((√‘(𝐶 − 𝐵))↑2) = (𝐶 − 𝐵))
115	42, 96, 114	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((√‘(𝐶 − 𝐵))↑2) = (𝐶 − 𝐵))
116	113, 115	oveq12d 7449	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((((√‘(𝐶 + 𝐵))↑2) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) + ((√‘(𝐶 − 𝐵))↑2)) = (((𝐶 + 𝐵) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) + (𝐶 − 𝐵)))
117	50, 110, 116	3eqtr4rd 2786	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((((√‘(𝐶 + 𝐵))↑2) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) + ((√‘(𝐶 − 𝐵))↑2)) = (2 · (𝐶 − 𝐴)))
118	31, 117	eqtrd 2775	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) = (2 · (𝐶 − 𝐴)))
119	118	oveq1d 7446	. . . . . . 7 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / 2) = ((2 · (𝐶 − 𝐴)) / 2))
120		subcl 11505	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐶 − 𝐴) ∈ ℂ)
121	3, 69, 120	syl2anr 597	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 − 𝐴) ∈ ℂ)
122	121	3adant2 1130	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 − 𝐴) ∈ ℂ)
123	122	3ad2ant1 1132	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 − 𝐴) ∈ ℂ)
124		divcan3 11946	. . . . . . . . 9 ⊢ (((𝐶 − 𝐴) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → ((2 · (𝐶 − 𝐴)) / 2) = (𝐶 − 𝐴))
125	14, 15, 124	mp3an23 1452	. . . . . . . 8 ⊢ ((𝐶 − 𝐴) ∈ ℂ → ((2 · (𝐶 − 𝐴)) / 2) = (𝐶 − 𝐴))
126	123, 125	syl 17	. . . . . . 7 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((2 · (𝐶 − 𝐴)) / 2) = (𝐶 − 𝐴))
127	119, 126	eqtrd 2775	. . . . . 6 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / 2) = (𝐶 − 𝐴))
128	127	oveq1d 7446	. . . . 5 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / 2) / 2) = ((𝐶 − 𝐴) / 2))
129	25, 128	eqtr3d 2777	. . . 4 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / (2 · 2)) = ((𝐶 − 𝐴) / 2))
130	20, 129	eqtrid 2787	. . 3 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / (2↑2)) = ((𝐶 − 𝐴) / 2))
131	18, 130	eqtrd 2775	. 2 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)↑2) = ((𝐶 − 𝐴) / 2))
132	2, 131	eqtrid 2787	1 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑁↑2) = ((𝐶 − 𝐴) / 2))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1537 ∈ wcel 2106 ≠ wne 2938 class class class wbr 5148 ‘cfv 6563 (class class class)co 7431 ℂcc 11151 ℝcr 11152 0cc0 11153 1c1 11154 + caddc 11156 · cmul 11158 < clt 11293 ≤ cle 11294 − cmin 11490 / cdiv 11918 ℕcn 12264 2c2 12319 ↑cexp 14099 √csqrt 15269 ∥ cdvds 16287 gcd cgcd 16528

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 ax-cnex 11209 ax-resscn 11210 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-addrcl 11214 ax-mulcl 11215 ax-mulrcl 11216 ax-mulcom 11217 ax-addass 11218 ax-mulass 11219 ax-distr 11220 ax-i2m1 11221 ax-1ne0 11222 ax-1rid 11223 ax-rnegex 11224 ax-rrecex 11225 ax-cnre 11226 ax-pre-lttri 11227 ax-pre-lttrn 11228 ax-pre-ltadd 11229 ax-pre-mulgt0 11230 ax-pre-sup 11231

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3378 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-2nd 8014 df-frecs 8305 df-wrecs 8336 df-recs 8410 df-rdg 8449 df-er 8744 df-en 8985 df-dom 8986 df-sdom 8987 df-sup 9480 df-pnf 11295 df-mnf 11296 df-xr 11297 df-ltxr 11298 df-le 11299 df-sub 11492 df-neg 11493 df-div 11919 df-nn 12265 df-2 12327 df-3 12328 df-n0 12525 df-z 12612 df-uz 12877 df-rp 13033 df-seq 14040 df-exp 14100 df-cj 15135 df-re 15136 df-im 15137 df-sqrt 15271 df-abs 15272

This theorem is referenced by: pythagtriplem15 16863 pythagtriplem17 16865

W3C validator