pythagtriplem11

Description: Lemma for pythagtrip . Show that M (which will eventually be closely related to the m in the final statement) is a natural. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Hypothesis	pythagtriplem11.1	$⊢ M = \frac{\sqrt{C + B} + \sqrt{C - B}}{2}$
	Assertion	pythagtriplem11	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to M \in ℕ$

Proof

Step	Hyp	Ref	Expression
1		pythagtriplem11.1	$⊢ M = \frac{\sqrt{C + B} + \sqrt{C - B}}{2}$
2		pythagtriplem9	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{C + B} \in ℕ$
3	2	nnzd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{C + B} \in ℤ$
4		simp3r	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \neg 2 ∥ A$
5		2z	$⊢ 2 \in ℤ$
6		nnz	$⊢ C \in ℕ \to C \in ℤ$
7	6	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C \in ℤ$
8		nnz	$⊢ B \in ℕ \to B \in ℤ$
9	8	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B \in ℤ$
10	7 9	zaddcld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C + B \in ℤ$
11	10	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to C + B \in ℤ$
12		nnz	$⊢ A \in ℕ \to A \in ℤ$
13	12	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℤ$
14	13	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to A \in ℤ$
15		dvdsgcdb	$⊢ (2 \in ℤ \land C + B \in ℤ \land A \in ℤ) \to ((2 ∥ (C + B) \land 2 ∥ A) \leftrightarrow 2 ∥ ((C + B) \gcd A))$
16	5 11 14 15	mp3an2i	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to ((2 ∥ (C + B) \land 2 ∥ A) \leftrightarrow 2 ∥ ((C + B) \gcd A))$
17	16	biimpar	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land 2 ∥ ((C + B) \gcd A)) \to (2 ∥ (C + B) \land 2 ∥ A)$
18	17	simprd	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land 2 ∥ ((C + B) \gcd A)) \to 2 ∥ A$
19	4 18	mtand	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \neg 2 ∥ ((C + B) \gcd A)$
20		pythagtriplem7	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{C + B} = (C + B) \gcd A$
21	20	breq2d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to (2 ∥ \sqrt{C + B} \leftrightarrow 2 ∥ ((C + B) \gcd A))$
22	19 21	mtbird	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \neg 2 ∥ \sqrt{C + B}$
23		pythagtriplem8	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{C - B} \in ℕ$
24	23	nnzd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{C - B} \in ℤ$
25	7 9	zsubcld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C - B \in ℤ$
26	25	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to C - B \in ℤ$
27		dvdsgcdb	$⊢ (2 \in ℤ \land C - B \in ℤ \land A \in ℤ) \to ((2 ∥ (C - B) \land 2 ∥ A) \leftrightarrow 2 ∥ ((C - B) \gcd A))$
28	5 26 14 27	mp3an2i	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to ((2 ∥ (C - B) \land 2 ∥ A) \leftrightarrow 2 ∥ ((C - B) \gcd A))$
29	28	biimpar	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land 2 ∥ ((C - B) \gcd A)) \to (2 ∥ (C - B) \land 2 ∥ A)$
30	29	simprd	$⊢ (((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \land 2 ∥ ((C - B) \gcd A)) \to 2 ∥ A$
31	4 30	mtand	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \neg 2 ∥ ((C - B) \gcd A)$
32		pythagtriplem6	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{C - B} = (C - B) \gcd A$
33	32	breq2d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to (2 ∥ \sqrt{C - B} \leftrightarrow 2 ∥ ((C - B) \gcd A))$
34	31 33	mtbird	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \neg 2 ∥ \sqrt{C - B}$
35		opoe	$⊢ ((\sqrt{C + B} \in ℤ \land \neg 2 ∥ \sqrt{C + B}) \land (\sqrt{C - B} \in ℤ \land \neg 2 ∥ \sqrt{C - B})) \to 2 ∥ (\sqrt{C + B} + \sqrt{C - B})$
36	3 22 24 34 35	syl22anc	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to 2 ∥ (\sqrt{C + B} + \sqrt{C - B})$
37	2 23	nnaddcld	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{C + B} + \sqrt{C - B} \in ℕ$
38	37	nnzd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{C + B} + \sqrt{C - B} \in ℤ$
39		evend2	$⊢ \sqrt{C + B} + \sqrt{C - B} \in ℤ \to (2 ∥ (\sqrt{C + B} + \sqrt{C - B}) \leftrightarrow \frac{\sqrt{C + B} + \sqrt{C - B}}{2} \in ℤ)$
40	38 39	syl	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to (2 ∥ (\sqrt{C + B} + \sqrt{C - B}) \leftrightarrow \frac{\sqrt{C + B} + \sqrt{C - B}}{2} \in ℤ)$
41	36 40	mpbid	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \frac{\sqrt{C + B} + \sqrt{C - B}}{2} \in ℤ$
42	2	nnred	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{C + B} \in ℝ$
43	23	nnred	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{C - B} \in ℝ$
44	2	nngt0d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to 0 < \sqrt{C + B}$
45	23	nngt0d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to 0 < \sqrt{C - B}$
46	42 43 44 45	addgt0d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to 0 < \sqrt{C + B} + \sqrt{C - B}$
47	37	nnred	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{C + B} + \sqrt{C - B} \in ℝ$
48		halfpos2	$⊢ \sqrt{C + B} + \sqrt{C - B} \in ℝ \to (0 < \sqrt{C + B} + \sqrt{C - B} \leftrightarrow 0 < \frac{\sqrt{C + B} + \sqrt{C - B}}{2})$
49	47 48	syl	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to (0 < \sqrt{C + B} + \sqrt{C - B} \leftrightarrow 0 < \frac{\sqrt{C + B} + \sqrt{C - B}}{2})$
50	46 49	mpbid	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to 0 < \frac{\sqrt{C + B} + \sqrt{C - B}}{2}$
51		elnnz	$⊢ \frac{\sqrt{C + B} + \sqrt{C - B}}{2} \in ℕ \leftrightarrow (\frac{\sqrt{C + B} + \sqrt{C - B}}{2} \in ℤ \land 0 < \frac{\sqrt{C + B} + \sqrt{C - B}}{2})$
52	41 50 51	sylanbrc	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \frac{\sqrt{C + B} + \sqrt{C - B}}{2} \in ℕ$
53	1 52	eqeltrid	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to M \in ℕ$

Metamath Proof Explorer

Theorem pythagtriplem11

Proof