pythagtriplem16

Description: Lemma for pythagtrip . Show the relationship between M , N , and B . (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	pythagtriplem15.1	$⊢ M = \frac{\sqrt{C + B} + \sqrt{C - B}}{2}$
	pythagtriplem15.2	$⊢ N = \frac{\sqrt{C + B} - \sqrt{C - B}}{2}$
Assertion	pythagtriplem16	$⊢ ((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 = 2 M \cdot N$

Proof

Step	Hyp	Ref	Expression
1		pythagtriplem15.1	$⊢ M = \frac{\sqrt{C + B} + \sqrt{C - B}}{2}$
2		pythagtriplem15.2	$⊢ N = \frac{\sqrt{C + B} - \sqrt{C - B}}{2}$
3	1 2	oveq12i	$⊢ M \cdot N = (\frac{\sqrt{C + B} + \sqrt{C - B}}{2}) (\frac{\sqrt{C + B} - \sqrt{C - B}}{2})$
4		nncn	$⊢ C \in ℕ \to C \in ℂ$
5		nncn	$⊢ B \in ℕ \to B \in ℂ$
6		addcl	$⊢ (C \in ℂ \land B \in ℂ) \to C + B \in ℂ$
7	4 5 6	syl2anr	$⊢ (B \in ℕ \land C \in ℕ) \to C + B \in ℂ$
8	7	sqrtcld	$⊢ (B \in ℕ \land C \in ℕ) \to \sqrt{C + B} \in ℂ$
9		subcl	$⊢ (C \in ℂ \land B \in ℂ) \to C - B \in ℂ$
10	4 5 9	syl2anr	$⊢ (B \in ℕ \land C \in ℕ) \to C - B \in ℂ$
11	10	sqrtcld	$⊢ (B \in ℕ \land C \in ℕ) \to \sqrt{C - B} \in ℂ$
12		addcl	$⊢ (\sqrt{C + B} \in ℂ \land \sqrt{C - B} \in ℂ) \to \sqrt{C + B} + \sqrt{C - B} \in ℂ$
13	8 11 12	syl2anc	$⊢ (B \in ℕ \land C \in ℕ) \to \sqrt{C + B} + \sqrt{C - B} \in ℂ$
14	13	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to \sqrt{C + B} + \sqrt{C - B} \in ℂ$
15	14	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 \sqrt{C + B} + \sqrt{C - B} \in ℂ$
16		subcl	$⊢ (\sqrt{C + B} \in ℂ \land \sqrt{C - B} \in ℂ) \to \sqrt{C + B} - \sqrt{C - B} \in ℂ$
17	8 11 16	syl2anc	$⊢ (B \in ℕ \land C \in ℕ) \to \sqrt{C + B} - \sqrt{C - B} \in ℂ$
18	17	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to \sqrt{C + B} - \sqrt{C - B} \in ℂ$
19	18	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 \sqrt{C + B} - \sqrt{C - B} \in ℂ$
20		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
21		divmuldiv	$⊢ ((\sqrt{C + B} + \sqrt{C - B} \in ℂ \land \sqrt{C + B} - \sqrt{C - B} \in ℂ) \land ((2 \in ℂ \land 2 \neq 0) \land (2 \in ℂ \land 2 \neq 0))) \to (\frac{\sqrt{C + B} + \sqrt{C - B}}{2}) (\frac{\sqrt{C + B} - \sqrt{C - B}}{2}) = \frac{(\sqrt{C + B} + \sqrt{C - B}) (\sqrt{C + B} - \sqrt{C - B})}{2 \cdot 2}$
22	20 20 21	mpanr12	$⊢ (\sqrt{C + B} + \sqrt{C - B} \in ℂ \land \sqrt{C + B} - \sqrt{C - B} \in ℂ) \to (\frac{\sqrt{C + B} + \sqrt{C - B}}{2}) (\frac{\sqrt{C + B} - \sqrt{C - B}}{2}) = \frac{(\sqrt{C + B} + \sqrt{C - B}) (\sqrt{C + B} - \sqrt{C - B})}{2 \cdot 2}$
23	15 19 22	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 (\frac{\sqrt{C + B} + \sqrt{C - B}}{2}) (\frac{\sqrt{C + B} - \sqrt{C - B}}{2}) = \frac{(\sqrt{C + B} + \sqrt{C - B}) (\sqrt{C + B} - \sqrt{C - B})}{2 \cdot 2}$
24	13 17	mulcld	$⊢ (B \in ℕ \land C \in ℕ) \to (\sqrt{C + B} + \sqrt{C - B}) (\sqrt{C + B} - \sqrt{C - B}) \in ℂ$
25	24	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to (\sqrt{C + B} + \sqrt{C - B}) (\sqrt{C + B} - \sqrt{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 (\sqrt{C + B} + \sqrt{C - B}) (\sqrt{C + B} - \sqrt{C - B}) \in ℂ$
27		divdiv1	$⊢ ((\sqrt{C + B} + \sqrt{C - B}) (\sqrt{C + B} - \sqrt{C - B}) \in ℂ \land (2 \in ℂ \land 2 \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{\frac{(\sqrt{C + B} + \sqrt{C - B}) (\sqrt{C + B} - \sqrt{C - B})}{2}}{2} = \frac{(\sqrt{C + B} + \sqrt{C - B}) (\sqrt{C + B} - \sqrt{C - B})}{2 \cdot 2}$
28	20 20 27	mp3an23	$⊢ (\sqrt{C + B} + \sqrt{C - B}) (\sqrt{C + B} - \sqrt{C - B}) \in ℂ \to \frac{\frac{(\sqrt{C + B} + \sqrt{C - B}) (\sqrt{C + B} - \sqrt{C - B})}{2}}{2} = \frac{(\sqrt{C + B} + \sqrt{C - B}) (\sqrt{C + B} - \sqrt{C - B})}{2 \cdot 2}$
29	26 28	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 \frac{\frac{(\sqrt{C + B} + \sqrt{C - B}) (\sqrt{C + B} - \sqrt{C - B})}{2}}{2} = \frac{(\sqrt{C + B} + \sqrt{C - B}) (\sqrt{C + B} - \sqrt{C - B})}{2 \cdot 2}$
30	23 29	eqtr4d	$⊢ ((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}) (\frac{\sqrt{C + B} - \sqrt{C - B}}{2}) = \frac{\frac{(\sqrt{C + B} + \sqrt{C - B}) (\sqrt{C + B} - \sqrt{C - B})}{2}}{2}$
31		nnre	$⊢ C \in ℕ \to C \in ℝ$
32		nnre	$⊢ B \in ℕ \to B \in ℝ$
33		readdcl	$⊢ (C \in ℝ \land B \in ℝ) \to C + B \in ℝ$
34	31 32 33	syl2anr	$⊢ (B \in ℕ \land C \in ℕ) \to C + B \in ℝ$
35	34	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C + B \in ℝ$
36	35	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 ℝ$
37	31	adantl	$⊢ (B \in ℕ \land C \in ℕ) \to C \in ℝ$
38	32	adantr	$⊢ (B \in ℕ \land C \in ℕ) \to B \in ℝ$
39		nngt0	$⊢ C \in ℕ \to 0 < C$
40	39	adantl	$⊢ (B \in ℕ \land C \in ℕ) \to 0 < C$
41		nngt0	$⊢ B \in ℕ \to 0 < B$
42	41	adantr	$⊢ (B \in ℕ \land C \in ℕ) \to 0 < B$
43	37 38 40 42	addgt0d	$⊢ (B \in ℕ \land C \in ℕ) \to 0 < C + B$
44		0re	$⊢ 0 \in ℝ$
45		ltle	$⊢ (0 \in ℝ \land C + B \in ℝ) \to (0 < C + B \to 0 \leq C + B)$
46	44 45	mpan	$⊢ C + B \in ℝ \to (0 < C + B \to 0 \leq C + B)$
47	34 43 46	sylc	$⊢ (B \in ℕ \land C \in ℕ) \to 0 \leq C + B$
48	47	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 0 \leq C + B$
49	48	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 \leq C + B$
50		resqrtth	$⊢ (C + B \in ℝ \land 0 \leq C + B) \to {\sqrt{C + B}}^{2} = C + B$
51	36 49 50	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}}^{2} = C + B$
52		resubcl	$⊢ (C \in ℝ \land B \in ℝ) \to C - B \in ℝ$
53	31 32 52	syl2anr	$⊢ (B \in ℕ \land C \in ℕ) \to C - B \in ℝ$
54	53	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C - B \in ℝ$
55	54	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 ℝ$
56		pythagtriplem10	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to 0 < C - B$
57	56	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$
58		ltle	$⊢ (0 \in ℝ \land C - B \in ℝ) \to (0 < C - B \to 0 \leq C - B)$
59	44 58	mpan	$⊢ C - B \in ℝ \to (0 < C - B \to 0 \leq C - B)$
60	55 57 59	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$
61		resqrtth	$⊢ (C - B \in ℝ \land 0 \leq C - B) \to {\sqrt{C - B}}^{2} = C - B$
62	55 60 61	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}}^{2} = C - B$
63	51 62	oveq12d	$⊢ ((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}}^{2} - {\sqrt{C - B}}^{2} = C + B - (C - B)$
64	63	oveq1d	$⊢ ((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}}^{2} - {\sqrt{C - B}}^{2}}{2} = \frac{C + B - (C - B)}{2}$
65		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 ℕ$
66		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 ℕ$
67	65 66 8	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} \in ℂ$
68	65 66 11	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} \in ℂ$
69		subsq	$⊢ (\sqrt{C + B} \in ℂ \land \sqrt{C - B} \in ℂ) \to {\sqrt{C + B}}^{2} - {\sqrt{C - B}}^{2} = (\sqrt{C + B} + \sqrt{C - B}) (\sqrt{C + B} - \sqrt{C - B})$
70	67 68 69	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}}^{2} - {\sqrt{C - B}}^{2} = (\sqrt{C + B} + \sqrt{C - B}) (\sqrt{C + B} - \sqrt{C - B})$
71	70	oveq1d	$⊢ ((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}}^{2} - {\sqrt{C - B}}^{2}}{2} = \frac{(\sqrt{C + B} + \sqrt{C - B}) (\sqrt{C + B} - \sqrt{C - B})}{2}$
72		pnncan	$⊢ (C \in ℂ \land B \in ℂ \land B \in ℂ) \to C + B - (C - B) = B + B$
73	72	3anidm23	$⊢ (C \in ℂ \land B \in ℂ) \to C + B - (C - B) = B + B$
74		2times	$⊢ B \in ℂ \to 2 B = B + B$
75	74	adantl	$⊢ (C \in ℂ \land B \in ℂ) \to 2 B = B + B$
76	73 75	eqtr4d	$⊢ (C \in ℂ \land B \in ℂ) \to C + B - (C - B) = 2 B$
77	4 5 76	syl2anr	$⊢ (B \in ℕ \land C \in ℕ) \to C + B - (C - B) = 2 B$
78	77	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C + B - (C - B) = 2 B$
79	78	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 - (C - B) = 2 B$
80	79	oveq1d	$⊢ ((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{C + B - (C - B)}{2} = \frac{2 B}{2}$
81		2cn	$⊢ 2 \in ℂ$
82		2ne0	$⊢ 2 \neq 0$
83		divcan3	$⊢ (B \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to \frac{2 B}{2} = B$
84	81 82 83	mp3an23	$⊢ B \in ℂ \to \frac{2 B}{2} = B$
85	65 5 84	3syl	$⊢ ((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{2 B}{2} = B$
86	80 85	eqtrd	$⊢ ((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{C + B - (C - B)}{2} = B$
87	64 71 86	3eqtr3d	$⊢ ((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}) (\sqrt{C + B} - \sqrt{C - B})}{2} = B$
88	87	oveq1d	$⊢ ((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{\frac{(\sqrt{C + B} + \sqrt{C - B}) (\sqrt{C + B} - \sqrt{C - B})}{2}}{2} = \frac{B}{2}$
89	30 88	eqtrd	$⊢ ((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}) (\frac{\sqrt{C + B} - \sqrt{C - B}}{2}) = \frac{B}{2}$
90	3 89	syl5eq	$⊢ ((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 \cdot N = \frac{B}{2}$
91	90	oveq2d	$⊢ ((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 M \cdot N = 2 (\frac{B}{2})$
92		divcan2	$⊢ (B \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to 2 (\frac{B}{2}) = B$
93	81 82 92	mp3an23	$⊢ B \in ℂ \to 2 (\frac{B}{2}) = B$
94	5 93	syl	$⊢ B \in ℕ \to 2 (\frac{B}{2}) = B$
95	94	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to 2 (\frac{B}{2}) = B$
96	95	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 2 (\frac{B}{2}) = B$
97	91 96	eqtr2d	$⊢ ((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 = 2 M \cdot N$

Metamath Proof Explorer

Theorem pythagtriplem16

Proof