pythagtriplem13

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

		Ref	Expression
	Hypothesis	pythagtriplem13.1	$⊢ N = \frac{\sqrt{C + B} - \sqrt{C - B}}{2}$
	Assertion	pythagtriplem13	$⊢ ((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 N \in ℕ$

Proof

Step	Hyp	Ref	Expression
1		pythagtriplem13.1	$⊢ N = \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		simp3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C \in ℕ$
7		simp2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B \in ℕ$
8	6 7	nnaddcld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C + B \in ℕ$
9	8	nnzd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C + B \in ℤ$
10	9	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 ℤ$
11		nnz	$⊢ A \in ℕ \to A \in ℤ$
12	11	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℤ$
13	12	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 ℤ$
14		dvdsgcdb	$⊢ (2 \in ℤ \land C + B \in ℤ \land A \in ℤ) \to ((2 ∥ (C + B) \land 2 ∥ A) \leftrightarrow 2 ∥ ((C + B) \gcd A))$
15	5 10 13 14	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))$
16	15	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)$
17	16	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$
18	4 17	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)$
19		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$
20	19	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))$
21	18 20	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}$
22		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 ℕ$
23	22	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 ℤ$
24		nnz	$⊢ C \in ℕ \to C \in ℤ$
25	24	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C \in ℤ$
26		nnz	$⊢ B \in ℕ \to B \in ℤ$
27	26	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B \in ℤ$
28	25 27	zsubcld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C - B \in ℤ$
29	28	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 ℤ$
30		dvdsgcdb	$⊢ (2 \in ℤ \land C - B \in ℤ \land A \in ℤ) \to ((2 ∥ (C - B) \land 2 ∥ A) \leftrightarrow 2 ∥ ((C - B) \gcd A))$
31	5 29 13 30	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))$
32	31	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)$
33	32	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$
34	4 33	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)$
35		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$
36	35	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))$
37	34 36	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}$
38		omoe	$⊢ ((\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})$
39	3 21 23 37 38	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})$
40	28	zred	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C - B \in ℝ$
41	40	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 ℝ$
42		simp13	$⊢ ((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 \in ℕ$
43	42	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 C \in ℝ$
44	8	nnred	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C + B \in ℝ$
45	44	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 ℝ$
46		nnrp	$⊢ B \in ℕ \to B \in ℝ^{+}$
47	46	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B \in ℝ^{+}$
48	47	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 B \in ℝ^{+}$
49	43 48	ltsubrpd	$⊢ ((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 < C$
50		nngt0	$⊢ B \in ℕ \to 0 < B$
51	50	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 < B$
52	51	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 0 < B$
53		simp12	$⊢ ((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 B \in ℕ$
54	53	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 B \in ℝ$
55	54 43	ltaddposd	$⊢ ((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 < B \leftrightarrow C < C + B)$
56	52 55	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 C < C + B$
57	41 43 45 49 56	lttrd	$⊢ ((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 < C + B$
58		pythagtriplem10	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to 0 < C - B$
59	58	3adant3	$⊢ ((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 < C - B$
60		0re	$⊢ 0 \in ℝ$
61		ltle	$⊢ (0 \in ℝ \land C - B \in ℝ) \to (0 < C - B \to 0 \leq C - B)$
62	60 61	mpan	$⊢ C - B \in ℝ \to (0 < C - B \to 0 \leq C - B)$
63	41 59 62	sylc	$⊢ ((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 \leq C - B$
64		nngt0	$⊢ C \in ℕ \to 0 < C$
65	64	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 < C$
66	65	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 0 < C$
67	43 54 66 52	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 < C + B$
68		ltle	$⊢ (0 \in ℝ \land C + B \in ℝ) \to (0 < C + B \to 0 \leq C + B)$
69	60 68	mpan	$⊢ C + B \in ℝ \to (0 < C + B \to 0 \leq C + B)$
70	45 67 69	sylc	$⊢ ((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 \leq C + B$
71	41 63 45 70	sqrtltd	$⊢ ((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 < C + B \leftrightarrow \sqrt{C - B} < \sqrt{C + B})$
72	57 71	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 \sqrt{C - B} < \sqrt{C + B}$
73		nnsub	$⊢ (\sqrt{C - B} \in ℕ \land \sqrt{C + B} \in ℕ) \to (\sqrt{C - B} < \sqrt{C + B} \leftrightarrow \sqrt{C + B} - \sqrt{C - B} \in ℕ)$
74	22 2 73	syl2anc	$⊢ ((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} \leftrightarrow \sqrt{C + B} - \sqrt{C - B} \in ℕ)$
75	72 74	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 \sqrt{C + B} - \sqrt{C - B} \in ℕ$
76	75	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 ℤ$
77		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 ℤ)$
78	76 77	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 ℤ)$
79	39 78	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 ℤ$
80	75	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} - \sqrt{C - B}$
81	75	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 ℝ$
82		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})$
83	81 82	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})$
84	80 83	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}$
85		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})$
86	79 84 85	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 ℕ$
87	1 86	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 N \in ℕ$

Metamath Proof Explorer

Theorem pythagtriplem13

Proof