pythagtriplem14 - Intuitionistic Logic Explorer

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

Theorem pythagtriplem14 13056

Description: Lemma for pythagtrip 13062. 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 6095	. 2 ⊢ (𝑁↑2) = ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)↑2)
3		simp13 1060	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐶 ∈ ℕ)
4		simp12 1059	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐵 ∈ ℕ)
5	3, 4	nnaddcld 9352	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 + 𝐵) ∈ ℕ)
6	5	nnrpd 10095	. . . . . . 7 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 + 𝐵) ∈ ℝ⁺)
7	6	rpsqrtcld 11924	. . . . . 6 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 + 𝐵)) ∈ ℝ⁺)
8	7	rpcnd 10099	. . . . 5 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 + 𝐵)) ∈ ℂ)
9	3	nnred 9317	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐶 ∈ ℝ)
10	4	nnred 9317	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐵 ∈ ℝ)
11	9, 10	resubcld 8708	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 − 𝐵) ∈ ℝ)
12		pythagtriplem10 13048	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → 0 < (𝐶 − 𝐵))
13	12	3adant3 1048	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 0 < (𝐶 − 𝐵))
14	11, 13	elrpd 10094	. . . . . . 7 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 − 𝐵) ∈ ℝ⁺)
15	14	rpsqrtcld 11924	. . . . . 6 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 − 𝐵)) ∈ ℝ⁺)
16	15	rpcnd 10099	. . . . 5 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 − 𝐵)) ∈ ℂ)
17	8, 16	subcld 8637	. . . 4 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) ∈ ℂ)
18		2cn 9375	. . . . 5 ⊢ 2 ∈ ℂ
19	18	a1i 9	. . . 4 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 2 ∈ ℂ)
20		2ap0 9397	. . . . 5 ⊢ 2 # 0
21	20	a1i 9	. . . 4 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 2 # 0)
22	17, 19, 21	sqdivapd 11124	. . 3 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)↑2) = ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / (2↑2)))
23	18	sqvali 11056	. . . . 5 ⊢ (2↑2) = (2 · 2)
24	23	oveq2i 6096	. . . 4 ⊢ ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / (2↑2)) = ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / (2 · 2))
25	17	sqcld 11109	. . . . . 6 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) ∈ ℂ)
26	25, 19, 19, 21, 21	divdivap1d 9152	. . . . 5 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / 2) / 2) = ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / (2 · 2)))
27		binom2sub 11090	. . . . . . . . . 10 ⊢ (((√‘(𝐶 + 𝐵)) ∈ ℂ ∧ (√‘(𝐶 − 𝐵)) ∈ ℂ) → (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) = ((((√‘(𝐶 + 𝐵))↑2) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) + ((√‘(𝐶 − 𝐵))↑2)))
28	8, 16, 27	syl2anc 415	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) = ((((√‘(𝐶 + 𝐵))↑2) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) + ((√‘(𝐶 − 𝐵))↑2)))
29		nnre 9311	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∈ ℕ → 𝐶 ∈ ℝ)
30		nnre 9311	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ ℕ → 𝐵 ∈ ℝ)
31		readdcl 8305	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 + 𝐵) ∈ ℝ)
32	29, 30, 31	syl2anr 290	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 + 𝐵) ∈ ℝ)
33	32	3adant1 1046	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 + 𝐵) ∈ ℝ)
34	33	3ad2ant1 1049	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 + 𝐵) ∈ ℝ)
35	34	recnd 8354	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 + 𝐵) ∈ ℂ)
36		resubcl 8590	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 − 𝐵) ∈ ℝ)
37	29, 30, 36	syl2anr 290	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 − 𝐵) ∈ ℝ)
38	37	3adant1 1046	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 − 𝐵) ∈ ℝ)
39	38	3ad2ant1 1049	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 − 𝐵) ∈ ℝ)
40	39	recnd 8354	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 − 𝐵) ∈ ℂ)
41	8, 16	mulcld 8346	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))) ∈ ℂ)
42		mulcl 8306	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))) ∈ ℂ) → (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵)))) ∈ ℂ)
43	18, 41, 42	sylancr 418	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵)))) ∈ ℂ)
44	35, 40, 43	addsubd 8658	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((𝐶 + 𝐵) + (𝐶 − 𝐵)) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) = (((𝐶 + 𝐵) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) + (𝐶 − 𝐵)))
45	3	nncnd 9318	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐶 ∈ ℂ)
46		simp11 1058	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐴 ∈ ℕ)
47	46	nncnd 9318	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐴 ∈ ℂ)
48		subdi 8712	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (2 · (𝐶 − 𝐴)) = ((2 · 𝐶) − (2 · 𝐴)))
49	18, 45, 47, 48	mp3an2i 1383	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (2 · (𝐶 − 𝐴)) = ((2 · 𝐶) − (2 · 𝐴)))
50		nncn 9312	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∈ ℕ → 𝐶 ∈ ℂ)
51		nncn 9312	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ ℕ → 𝐵 ∈ ℂ)
52		ppncan 8568	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐶 + 𝐵) + (𝐶 − 𝐵)) = (𝐶 + 𝐶))
53	52	3anidm13 1337	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐶 + 𝐵) + (𝐶 − 𝐵)) = (𝐶 + 𝐶))
54		2times 9432	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 ∈ ℂ → (2 · 𝐶) = (𝐶 + 𝐶))
55	54	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2 · 𝐶) = (𝐶 + 𝐶))
56	53, 55	eqtr4d 2274	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐶 + 𝐵) + (𝐶 − 𝐵)) = (2 · 𝐶))
57	50, 51, 56	syl2anr 290	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐶 + 𝐵) + (𝐶 − 𝐵)) = (2 · 𝐶))
58	57	3adant1 1046	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐶 + 𝐵) + (𝐶 − 𝐵)) = (2 · 𝐶))
59	58	3ad2ant1 1049	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((𝐶 + 𝐵) + (𝐶 − 𝐵)) = (2 · 𝐶))
60	4	nncnd 9318	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐵 ∈ ℂ)
61		subsq 11083	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐶↑2) − (𝐵↑2)) = ((𝐶 + 𝐵) · (𝐶 − 𝐵)))
62	45, 60, 61	syl2anc 415	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((𝐶↑2) − (𝐵↑2)) = ((𝐶 + 𝐵) · (𝐶 − 𝐵)))
63		oveq1 6092	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) → (((𝐴↑2) + (𝐵↑2)) − (𝐵↑2)) = ((𝐶↑2) − (𝐵↑2)))
64	63	3ad2ant2 1050	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((𝐴↑2) + (𝐵↑2)) − (𝐵↑2)) = ((𝐶↑2) − (𝐵↑2)))
65		nncn 9312	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
66	65	sqcld 11109	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℕ → (𝐴↑2) ∈ ℂ)
67	66	3ad2ant1 1049	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐴↑2) ∈ ℂ)
68	51	sqcld 11109	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ ℕ → (𝐵↑2) ∈ ℂ)
69	68	3ad2ant2 1050	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐵↑2) ∈ ℂ)
70	67, 69	pncand 8638	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (((𝐴↑2) + (𝐵↑2)) − (𝐵↑2)) = (𝐴↑2))
71	70	3ad2ant1 1049	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((𝐴↑2) + (𝐵↑2)) − (𝐵↑2)) = (𝐴↑2))
72	64, 71	eqtr3d 2273	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((𝐶↑2) − (𝐵↑2)) = (𝐴↑2))
73	62, 72	eqtr3d 2273	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((𝐶 + 𝐵) · (𝐶 − 𝐵)) = (𝐴↑2))
74	73	fveq2d 5699	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘((𝐶 + 𝐵) · (𝐶 − 𝐵))) = (√‘(𝐴↑2)))
75	29	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐶 ∈ ℝ)
76	30	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐵 ∈ ℝ)
77		nngt0 9329	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐶 ∈ ℕ → 0 < 𝐶)
78	77	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 < 𝐶)
79		nngt0 9329	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ ℕ → 0 < 𝐵)
80	79	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 < 𝐵)
81	75, 76, 78, 80	addgt0d 8849	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 < (𝐶 + 𝐵))
82		0re 8326	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℝ
83		ltle 8413	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 ∈ ℝ ∧ (𝐶 + 𝐵) ∈ ℝ) → (0 < (𝐶 + 𝐵) → 0 ≤ (𝐶 + 𝐵)))
84	82, 83	mpan 428	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐶 + 𝐵) ∈ ℝ → (0 < (𝐶 + 𝐵) → 0 ≤ (𝐶 + 𝐵)))
85	32, 81, 84	sylc 62	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 ≤ (𝐶 + 𝐵))
86	85	3adant1 1046	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 ≤ (𝐶 + 𝐵))
87	86	3ad2ant1 1049	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 0 ≤ (𝐶 + 𝐵))
88		ltle 8413	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ∈ ℝ ∧ (𝐶 − 𝐵) ∈ ℝ) → (0 < (𝐶 − 𝐵) → 0 ≤ (𝐶 − 𝐵)))
89	82, 88	mpan 428	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 − 𝐵) ∈ ℝ → (0 < (𝐶 − 𝐵) → 0 ≤ (𝐶 − 𝐵)))
90	39, 13, 89	sylc 62	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 0 ≤ (𝐶 − 𝐵))
91	34, 87, 39, 90	sqrtmuld 11935	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘((𝐶 + 𝐵) · (𝐶 − 𝐵))) = ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))
92		nnre 9311	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
93	92	3ad2ant1 1049	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝐴 ∈ ℝ)
94	93	3ad2ant1 1049	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐴 ∈ ℝ)
95		nnnn0 9570	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ₀)
96	95	nn0ge0d 9623	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℕ → 0 ≤ 𝐴)
97	96	3ad2ant1 1049	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 0 ≤ 𝐴)
98	97	3ad2ant1 1049	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 0 ≤ 𝐴)
99	94, 98	sqrtsqd 11931	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐴↑2)) = 𝐴)
100	74, 91, 99	3eqtr3d 2279	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))) = 𝐴)
101	100	oveq2d 6101	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵)))) = (2 · 𝐴))
102	59, 101	oveq12d 6103	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((𝐶 + 𝐵) + (𝐶 − 𝐵)) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) = ((2 · 𝐶) − (2 · 𝐴)))
103	49, 102	eqtr4d 2274	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (2 · (𝐶 − 𝐴)) = (((𝐶 + 𝐵) + (𝐶 − 𝐵)) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))))
104		resqrtth 11797	. . . . . . . . . . . . 13 ⊢ (((𝐶 + 𝐵) ∈ ℝ ∧ 0 ≤ (𝐶 + 𝐵)) → ((√‘(𝐶 + 𝐵))↑2) = (𝐶 + 𝐵))
105	34, 87, 104	syl2anc 415	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((√‘(𝐶 + 𝐵))↑2) = (𝐶 + 𝐵))
106	105	oveq1d 6100	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((√‘(𝐶 + 𝐵))↑2) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) = ((𝐶 + 𝐵) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))))
107		resqrtth 11797	. . . . . . . . . . . 12 ⊢ (((𝐶 − 𝐵) ∈ ℝ ∧ 0 ≤ (𝐶 − 𝐵)) → ((√‘(𝐶 − 𝐵))↑2) = (𝐶 − 𝐵))
108	39, 90, 107	syl2anc 415	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((√‘(𝐶 − 𝐵))↑2) = (𝐶 − 𝐵))
109	106, 108	oveq12d 6103	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((((√‘(𝐶 + 𝐵))↑2) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) + ((√‘(𝐶 − 𝐵))↑2)) = (((𝐶 + 𝐵) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) + (𝐶 − 𝐵)))
110	44, 103, 109	3eqtr4rd 2282	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((((√‘(𝐶 + 𝐵))↑2) − (2 · ((√‘(𝐶 + 𝐵)) · (√‘(𝐶 − 𝐵))))) + ((√‘(𝐶 − 𝐵))↑2)) = (2 · (𝐶 − 𝐴)))
111	28, 110	eqtrd 2271	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) = (2 · (𝐶 − 𝐴)))
112	111	oveq1d 6100	. . . . . . 7 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / 2) = ((2 · (𝐶 − 𝐴)) / 2))
113		subcl 8525	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐶 − 𝐴) ∈ ℂ)
114	50, 65, 113	syl2anr 290	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 − 𝐴) ∈ ℂ)
115	114	3adant2 1047	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 − 𝐴) ∈ ℂ)
116	115	3ad2ant1 1049	. . . . . . . 8 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐶 − 𝐴) ∈ ℂ)
117	116, 19, 21	divcanap3d 9125	. . . . . . 7 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((2 · (𝐶 − 𝐴)) / 2) = (𝐶 − 𝐴))
118	112, 117	eqtrd 2271	. . . . . 6 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / 2) = (𝐶 − 𝐴))
119	118	oveq1d 6100	. . . . 5 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / 2) / 2) = ((𝐶 − 𝐴) / 2))
120	26, 119	eqtr3d 2273	. . . 4 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / (2 · 2)) = ((𝐶 − 𝐴) / 2))
121	24, 120	eqtrid 2283	. . 3 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵)))↑2) / (2↑2)) = ((𝐶 − 𝐴) / 2))
122	22, 121	eqtrd 2271	. 2 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)↑2) = ((𝐶 − 𝐴) / 2))
123	2, 122	eqtrid 2283	1 ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑁↑2) = ((𝐶 − 𝐴) / 2))

Colors of variables: wff set class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 104 ∧ w3a 1009 = wceq 1402 ∈ wcel 2209 class class class wbr 4130 ‘cfv 5377 (class class class)co 6085 ℂcc 8177 ℝcr 8178 0cc0 8179 1c1 8180 + caddc 8182 · cmul 8184 < clt 8360 ≤ cle 8361 − cmin 8497 # cap 8909 / cdiv 9002 ℕcn 9304 2c2 9355 ↑cexp 10975 √csqrt 11762 ∥ cdvds 12554 gcd cgcd 12730

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735 ax-cnex 8270 ax-resscn 8271 ax-1cn 8272 ax-1re 8273 ax-icn 8274 ax-addcl 8275 ax-addrcl 8276 ax-mulcl 8277 ax-mulrcl 8278 ax-addcom 8279 ax-mulcom 8280 ax-addass 8281 ax-mulass 8282 ax-distr 8283 ax-i2m1 8284 ax-0lt1 8285 ax-1rid 8286 ax-0id 8287 ax-rnegex 8288 ax-precex 8289 ax-cnre 8290 ax-pre-ltirr 8291 ax-pre-ltwlin 8292 ax-pre-lttrn 8293 ax-pre-apti 8294 ax-pre-ltadd 8295 ax-pre-mulgt0 8296 ax-pre-mulext 8297 ax-arch 8298 ax-caucvg 8299

This proof depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-po 4441 df-iso 4442 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-1st 6374 df-2nd 6375 df-recs 6576 df-frec 6662 df-pnf 8362 df-mnf 8363 df-xr 8364 df-ltxr 8365 df-le 8366 df-sub 8499 df-neg 8500 df-reap 8903 df-ap 8910 df-div 9003 df-inn 9305 df-2 9363 df-3 9364 df-4 9365 df-n0 9564 df-z 9645 df-uz 9922 df-rp 10055 df-seqfrec 10885 df-exp 10976 df-rsqrt 11764

This theorem is used by: pythagtriplem15 13057 pythagtriplem17 13059

W3C validator