fltaccoprm

Description: A counterexample to FLT with A , B coprime also has A , C coprime. (Contributed by SN, 20-Aug-2024)

	Ref	Expression
Hypotheses	fltabcoprmex.a	$⊢ φ \to A \in ℕ$
	fltabcoprmex.b	$⊢ φ \to B \in ℕ$
	fltabcoprmex.c	$⊢ φ \to C \in ℕ$
	fltabcoprmex.n	$⊢ φ \to N \in ℕ_{0}$
	fltabcoprmex.1	$⊢ φ \to A^{N} + B^{N} = C^{N}$
	fltaccoprm.1	$⊢ φ \to A \gcd B = 1$
Assertion	fltaccoprm	$⊢ φ \to A \gcd C = 1$

Proof

Step	Hyp	Ref	Expression
1		fltabcoprmex.a	$⊢ φ \to A \in ℕ$
2		fltabcoprmex.b	$⊢ φ \to B \in ℕ$
3		fltabcoprmex.c	$⊢ φ \to C \in ℕ$
4		fltabcoprmex.n	$⊢ φ \to N \in ℕ_{0}$
5		fltabcoprmex.1	$⊢ φ \to A^{N} + B^{N} = C^{N}$
6		fltaccoprm.1	$⊢ φ \to A \gcd B = 1$
7		coprmgcdb	$⊢ (A \in ℕ \land B \in ℕ) \to (\forall i \in ℕ ((i ∥ A \land i ∥ B) \to i = 1) \leftrightarrow A \gcd B = 1)$
8	1 2 7	syl2anc	$⊢ φ \to (\forall i \in ℕ ((i ∥ A \land i ∥ B) \to i = 1) \leftrightarrow A \gcd B = 1)$
9	6 8	mpbird	$⊢ φ \to \forall i \in ℕ ((i ∥ A \land i ∥ B) \to i = 1)$
10		simprl	$⊢ ((φ \land i \in ℕ) \land (i ∥ A \land i ∥ C)) \to i ∥ A$
11		simpr	$⊢ (φ \land i \in ℕ) \to i \in ℕ$
12	11	nnzd	$⊢ (φ \land i \in ℕ) \to i \in ℤ$
13	3	nnzd	$⊢ φ \to C \in ℤ$
14	13	adantr	$⊢ (φ \land i \in ℕ) \to C \in ℤ$
15	4	adantr	$⊢ (φ \land i \in ℕ) \to N \in ℕ_{0}$
16		dvdsexpim	$⊢ (i \in ℤ \land C \in ℤ \land N \in ℕ_{0}) \to (i ∥ C \to i^{N} ∥ C^{N})$
17	12 14 15 16	syl3anc	$⊢ (φ \land i \in ℕ) \to (i ∥ C \to i^{N} ∥ C^{N})$
18	1	nnzd	$⊢ φ \to A \in ℤ$
19	18	adantr	$⊢ (φ \land i \in ℕ) \to A \in ℤ$
20		dvdsexpim	$⊢ (i \in ℤ \land A \in ℤ \land N \in ℕ_{0}) \to (i ∥ A \to i^{N} ∥ A^{N})$
21	12 19 15 20	syl3anc	$⊢ (φ \land i \in ℕ) \to (i ∥ A \to i^{N} ∥ A^{N})$
22	17 21	anim12d	$⊢ (φ \land i \in ℕ) \to ((i ∥ C \land i ∥ A) \to (i^{N} ∥ C^{N} \land i^{N} ∥ A^{N}))$
23	22	ancomsd	$⊢ (φ \land i \in ℕ) \to ((i ∥ A \land i ∥ C) \to (i^{N} ∥ C^{N} \land i^{N} ∥ A^{N}))$
24	23	imp	$⊢ ((φ \land i \in ℕ) \land (i ∥ A \land i ∥ C)) \to (i^{N} ∥ C^{N} \land i^{N} ∥ A^{N})$
25	11 15	nnexpcld	$⊢ (φ \land i \in ℕ) \to i^{N} \in ℕ$
26	25	nnzd	$⊢ (φ \land i \in ℕ) \to i^{N} \in ℤ$
27	26	adantr	$⊢ ((φ \land i \in ℕ) \land (i ∥ A \land i ∥ C)) \to i^{N} \in ℤ$
28	3 4	nnexpcld	$⊢ φ \to C^{N} \in ℕ$
29	28	nnzd	$⊢ φ \to C^{N} \in ℤ$
30	29	ad2antrr	$⊢ ((φ \land i \in ℕ) \land (i ∥ A \land i ∥ C)) \to C^{N} \in ℤ$
31	1 4	nnexpcld	$⊢ φ \to A^{N} \in ℕ$
32	31	nnzd	$⊢ φ \to A^{N} \in ℤ$
33	32	ad2antrr	$⊢ ((φ \land i \in ℕ) \land (i ∥ A \land i ∥ C)) \to A^{N} \in ℤ$
34		dvds2sub	$⊢ (i^{N} \in ℤ \land C^{N} \in ℤ \land A^{N} \in ℤ) \to ((i^{N} ∥ C^{N} \land i^{N} ∥ A^{N}) \to i^{N} ∥ (C^{N} - A^{N}))$
35	27 30 33 34	syl3anc	$⊢ ((φ \land i \in ℕ) \land (i ∥ A \land i ∥ C)) \to ((i^{N} ∥ C^{N} \land i^{N} ∥ A^{N}) \to i^{N} ∥ (C^{N} - A^{N}))$
36	24 35	mpd	$⊢ ((φ \land i \in ℕ) \land (i ∥ A \land i ∥ C)) \to i^{N} ∥ (C^{N} - A^{N})$
37	1	nncnd	$⊢ φ \to A \in ℂ$
38	37 4	expcld	$⊢ φ \to A^{N} \in ℂ$
39	2	nncnd	$⊢ φ \to B \in ℂ$
40	39 4	expcld	$⊢ φ \to B^{N} \in ℂ$
41	38 40 5	laddrotrd	$⊢ φ \to C^{N} - A^{N} = B^{N}$
42	41	ad2antrr	$⊢ ((φ \land i \in ℕ) \land (i ∥ A \land i ∥ C)) \to C^{N} - A^{N} = B^{N}$
43	36 42	breqtrd	$⊢ ((φ \land i \in ℕ) \land (i ∥ A \land i ∥ C)) \to i^{N} ∥ B^{N}$
44		simplr	$⊢ ((φ \land i \in ℕ) \land (i ∥ A \land i ∥ C)) \to i \in ℕ$
45	2	ad2antrr	$⊢ ((φ \land i \in ℕ) \land (i ∥ A \land i ∥ C)) \to B \in ℕ$
46	3	nncnd	$⊢ φ \to C \in ℂ$
47	37 39 46 4 5	flt0	$⊢ φ \to N \in ℕ$
48	47	ad2antrr	$⊢ ((φ \land i \in ℕ) \land (i ∥ A \land i ∥ C)) \to N \in ℕ$
49		dvdsexpnn	$⊢ (i \in ℕ \land B \in ℕ \land N \in ℕ) \to (i ∥ B \leftrightarrow i^{N} ∥ B^{N})$
50	44 45 48 49	syl3anc	$⊢ ((φ \land i \in ℕ) \land (i ∥ A \land i ∥ C)) \to (i ∥ B \leftrightarrow i^{N} ∥ B^{N})$
51	43 50	mpbird	$⊢ ((φ \land i \in ℕ) \land (i ∥ A \land i ∥ C)) \to i ∥ B$
52	10 51	jca	$⊢ ((φ \land i \in ℕ) \land (i ∥ A \land i ∥ C)) \to (i ∥ A \land i ∥ B)$
53	52	ex	$⊢ (φ \land i \in ℕ) \to ((i ∥ A \land i ∥ C) \to (i ∥ A \land i ∥ B))$
54	53	imim1d	$⊢ (φ \land i \in ℕ) \to (((i ∥ A \land i ∥ B) \to i = 1) \to ((i ∥ A \land i ∥ C) \to i = 1))$
55	54	ralimdva	$⊢ φ \to (\forall i \in ℕ ((i ∥ A \land i ∥ B) \to i = 1) \to \forall i \in ℕ ((i ∥ A \land i ∥ C) \to i = 1))$
56	9 55	mpd	$⊢ φ \to \forall i \in ℕ ((i ∥ A \land i ∥ C) \to i = 1)$
57		coprmgcdb	$⊢ (A \in ℕ \land C \in ℕ) \to (\forall i \in ℕ ((i ∥ A \land i ∥ C) \to i = 1) \leftrightarrow A \gcd C = 1)$
58	1 3 57	syl2anc	$⊢ φ \to (\forall i \in ℕ ((i ∥ A \land i ∥ C) \to i = 1) \leftrightarrow A \gcd C = 1)$
59	56 58	mpbid	$⊢ φ \to A \gcd C = 1$

Metamath Proof Explorer

Theorem fltaccoprm

Proof