flt4lem5

Description: In the context of the lemmas of pythagtrip , M and N are coprime. (Contributed by SN, 23-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		flt4lem5.1	$⊢ M = \frac{\sqrt{C + B} + \sqrt{C - B}}{2}$
2		flt4lem5.2	$⊢ N = \frac{\sqrt{C + B} - \sqrt{C - B}}{2}$
3		simp3l	$⊢ ((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 \gcd B = 1$
4		simp11	$⊢ ((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 ℕ$
5		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 ℕ$
6		coprmgcdb	$⊢ (A \in ℕ \land B \in ℕ) \to (\forall i \in ℕ ((i ∥ A \land i ∥ B) \to i = 1) \leftrightarrow A \gcd B = 1)$
7	4 5 6	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 (\forall i \in ℕ ((i ∥ A \land i ∥ B) \to i = 1) \leftrightarrow A \gcd B = 1)$
8	3 7	mpbird	$⊢ ((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 \forall i \in ℕ ((i ∥ A \land i ∥ B) \to i = 1)$
9		simplr	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to i \in ℕ$
10	9	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)) \land i \in ℕ) \land (i ∥ M \land i ∥ N)) \to i \in ℤ$
11	1	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 ℕ$
12	11	ad2antrr	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to M \in ℕ$
13	12	nnsqcld	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to M^{2} \in ℕ$
14	13	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)) \land i \in ℕ) \land (i ∥ M \land i ∥ N)) \to M^{2} \in ℤ$
15	2	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 ℕ$
16	15	ad2antrr	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to N \in ℕ$
17	16	nnsqcld	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to N^{2} \in ℕ$
18	17	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)) \land i \in ℕ) \land (i ∥ M \land i ∥ N)) \to N^{2} \in ℤ$
19		simprl	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to i ∥ M$
20	12	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)) \land i \in ℕ) \land (i ∥ M \land i ∥ N)) \to M \in ℤ$
21		2nn	$⊢ 2 \in ℕ$
22	21	a1i	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to 2 \in ℕ$
23		dvdsexp2im	$⊢ (i \in ℤ \land M \in ℤ \land 2 \in ℕ) \to (i ∥ M \to i ∥ M^{2})$
24	10 20 22 23	syl3anc	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to (i ∥ M \to i ∥ M^{2})$
25	19 24	mpd	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to i ∥ M^{2}$
26		simprr	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to i ∥ N$
27	16	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)) \land i \in ℕ) \land (i ∥ M \land i ∥ N)) \to N \in ℤ$
28		dvdsexp2im	$⊢ (i \in ℤ \land N \in ℤ \land 2 \in ℕ) \to (i ∥ N \to i ∥ N^{2})$
29	10 27 22 28	syl3anc	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to (i ∥ N \to i ∥ N^{2})$
30	26 29	mpd	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to i ∥ N^{2}$
31	10 14 18 25 30	dvds2subd	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to i ∥ (M^{2} - N^{2})$
32	1 2	pythagtriplem15	$⊢ ((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 = M^{2} - N^{2}$
33	32	ad2antrr	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to A = M^{2} - N^{2}$
34	31 33	breqtrrd	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to i ∥ A$
35		2z	$⊢ 2 \in ℤ$
36	35	a1i	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to 2 \in ℤ$
37	12 16	nnmulcld	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to M \cdot N \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)) \land i \in ℕ) \land (i ∥ M \land i ∥ N)) \to M \cdot N \in ℤ$
39	10 20 27 26	dvdsmultr2d	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to i ∥ M \cdot N$
40	10 36 38 39	dvdsmultr2d	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to i ∥ 2 M \cdot N$
41	1 2	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$
42	41	ad2antrr	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to B = 2 M \cdot N$
43	40 42	breqtrrd	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to i ∥ B$
44	34 43	jca	$⊢ ((((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 i \in ℕ) \land (i ∥ M \land i ∥ N)) \to (i ∥ A \land i ∥ B)$
45	44	ex	$⊢ (((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 i \in ℕ) \to ((i ∥ M \land i ∥ N) \to (i ∥ A \land i ∥ B))$
46	45	imim1d	$⊢ (((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 i \in ℕ) \to (((i ∥ A \land i ∥ B) \to i = 1) \to ((i ∥ M \land i ∥ N) \to i = 1))$
47	46	ralimdva	$⊢ ((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 (\forall i \in ℕ ((i ∥ A \land i ∥ B) \to i = 1) \to \forall i \in ℕ ((i ∥ M \land i ∥ N) \to i = 1))$
48	8 47	mpd	$⊢ ((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 \forall i \in ℕ ((i ∥ M \land i ∥ N) \to i = 1)$
49		coprmgcdb	$⊢ (M \in ℕ \land N \in ℕ) \to (\forall i \in ℕ ((i ∥ M \land i ∥ N) \to i = 1) \leftrightarrow M \gcd N = 1)$
50	11 15 49	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 (\forall i \in ℕ ((i ∥ M \land i ∥ N) \to i = 1) \leftrightarrow M \gcd N = 1)$
51	48 50	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 M \gcd N = 1$

Metamath Proof Explorer

Theorem flt4lem5

Proof