goldbachthlem2

		Ref	Expression
	Assertion	goldbachthlem2	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to FermatNo (N) \gcd FermatNo (M) = 1$

Proof

Step	Hyp	Ref	Expression
1		fmtnonn	$⊢ N \in ℕ_{0} \to FermatNo (N) \in ℕ$
2	1	nnzd	$⊢ N \in ℕ_{0} \to FermatNo (N) \in ℤ$
3		fmtnonn	$⊢ M \in ℕ_{0} \to FermatNo (M) \in ℕ$
4	3	nnzd	$⊢ M \in ℕ_{0} \to FermatNo (M) \in ℤ$
5	2 4	anim12ci	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0}) \to (FermatNo (M) \in ℤ \land FermatNo (N) \in ℤ)$
6	5	3adant3	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to (FermatNo (M) \in ℤ \land FermatNo (N) \in ℤ)$
7		gcddvds	$⊢ (FermatNo (M) \in ℤ \land FermatNo (N) \in ℤ) \to ((FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (M) \land (FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (N))$
8	6 7	syl	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to ((FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (M) \land (FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (N))$
9		goldbachthlem1	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to FermatNo (M) ∥ (FermatNo (N) - 2)$
10		gcdcl	$⊢ (FermatNo (M) \in ℤ \land FermatNo (N) \in ℤ) \to FermatNo (M) \gcd FermatNo (N) \in ℕ_{0}$
11	6 10	syl	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to FermatNo (M) \gcd FermatNo (N) \in ℕ_{0}$
12	11	nn0zd	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to FermatNo (M) \gcd FermatNo (N) \in ℤ$
13	4	3ad2ant2	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to FermatNo (M) \in ℤ$
14		2z	$⊢ 2 \in ℤ$
15	14	a1i	$⊢ N \in ℕ_{0} \to 2 \in ℤ$
16	2 15	zsubcld	$⊢ N \in ℕ_{0} \to FermatNo (N) - 2 \in ℤ$
17	16	3ad2ant1	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to FermatNo (N) - 2 \in ℤ$
18		dvdstr	$⊢ (FermatNo (M) \gcd FermatNo (N) \in ℤ \land FermatNo (M) \in ℤ \land FermatNo (N) - 2 \in ℤ) \to (((FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (M) \land FermatNo (M) ∥ (FermatNo (N) - 2)) \to (FermatNo (M) \gcd FermatNo (N)) ∥ (FermatNo (N) - 2))$
19	12 13 17 18	syl3anc	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to (((FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (M) \land FermatNo (M) ∥ (FermatNo (N) - 2)) \to (FermatNo (M) \gcd FermatNo (N)) ∥ (FermatNo (N) - 2))$
20	9 19	mpan2d	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to ((FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (M) \to (FermatNo (M) \gcd FermatNo (N)) ∥ (FermatNo (N) - 2))$
21	2	3ad2ant1	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to FermatNo (N) \in ℤ$
22		dvds2sub	$⊢ (FermatNo (M) \gcd FermatNo (N) \in ℤ \land FermatNo (N) \in ℤ \land FermatNo (N) - 2 \in ℤ) \to (((FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (N) \land (FermatNo (M) \gcd FermatNo (N)) ∥ (FermatNo (N) - 2)) \to (FermatNo (M) \gcd FermatNo (N)) ∥ (FermatNo (N) - (FermatNo (N) - 2)))$
23	12 21 17 22	syl3anc	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to (((FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (N) \land (FermatNo (M) \gcd FermatNo (N)) ∥ (FermatNo (N) - 2)) \to (FermatNo (M) \gcd FermatNo (N)) ∥ (FermatNo (N) - (FermatNo (N) - 2)))$
24	23	ancomsd	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to (((FermatNo (M) \gcd FermatNo (N)) ∥ (FermatNo (N) - 2) \land (FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (N)) \to (FermatNo (M) \gcd FermatNo (N)) ∥ (FermatNo (N) - (FermatNo (N) - 2)))$
25	1	nncnd	$⊢ N \in ℕ_{0} \to FermatNo (N) \in ℂ$
26	25	3ad2ant1	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to FermatNo (N) \in ℂ$
27		2cnd	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to 2 \in ℂ$
28	26 27	nncand	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to FermatNo (N) - (FermatNo (N) - 2) = 2$
29	28	breq2d	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to ((FermatNo (M) \gcd FermatNo (N)) ∥ (FermatNo (N) - (FermatNo (N) - 2)) \leftrightarrow (FermatNo (M) \gcd FermatNo (N)) ∥ 2)$
30		2prm	$⊢ 2 \in ℙ$
31	1 3	anim12ci	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0}) \to (FermatNo (M) \in ℕ \land FermatNo (N) \in ℕ)$
32	31	3adant3	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to (FermatNo (M) \in ℕ \land FermatNo (N) \in ℕ)$
33		gcdnncl	$⊢ (FermatNo (M) \in ℕ \land FermatNo (N) \in ℕ) \to FermatNo (M) \gcd FermatNo (N) \in ℕ$
34	32 33	syl	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to FermatNo (M) \gcd FermatNo (N) \in ℕ$
35		dvdsprime	$⊢ (2 \in ℙ \land FermatNo (M) \gcd FermatNo (N) \in ℕ) \to ((FermatNo (M) \gcd FermatNo (N)) ∥ 2 \leftrightarrow (FermatNo (M) \gcd FermatNo (N) = 2 \lor FermatNo (M) \gcd FermatNo (N) = 1))$
36	30 34 35	sylancr	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to ((FermatNo (M) \gcd FermatNo (N)) ∥ 2 \leftrightarrow (FermatNo (M) \gcd FermatNo (N) = 2 \lor FermatNo (M) \gcd FermatNo (N) = 1))$
37	5 7	syl	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0}) \to ((FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (M) \land (FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (N))$
38		breq1	$⊢ FermatNo (M) \gcd FermatNo (N) = 2 \to ((FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (N) \leftrightarrow 2 ∥ FermatNo (N))$
39	38	adantl	$⊢ ((N \in ℕ_{0} \land M \in ℕ_{0}) \land FermatNo (M) \gcd FermatNo (N) = 2) \to ((FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (N) \leftrightarrow 2 ∥ FermatNo (N))$
40		fmtnoodd	$⊢ N \in ℕ_{0} \to \neg 2 ∥ FermatNo (N)$
41	40	pm2.21d	$⊢ N \in ℕ_{0} \to (2 ∥ FermatNo (N) \to FermatNo (N) \gcd FermatNo (M) = 1)$
42	41	ad2antrr	$⊢ ((N \in ℕ_{0} \land M \in ℕ_{0}) \land FermatNo (M) \gcd FermatNo (N) = 2) \to (2 ∥ FermatNo (N) \to FermatNo (N) \gcd FermatNo (M) = 1)$
43	39 42	sylbid	$⊢ ((N \in ℕ_{0} \land M \in ℕ_{0}) \land FermatNo (M) \gcd FermatNo (N) = 2) \to ((FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (N) \to FermatNo (N) \gcd FermatNo (M) = 1)$
44	43	ex	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0}) \to (FermatNo (M) \gcd FermatNo (N) = 2 \to ((FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (N) \to FermatNo (N) \gcd FermatNo (M) = 1))$
45	44	com23	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0}) \to ((FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (N) \to (FermatNo (M) \gcd FermatNo (N) = 2 \to FermatNo (N) \gcd FermatNo (M) = 1))$
46	45	adantld	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0}) \to (((FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (M) \land (FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (N)) \to (FermatNo (M) \gcd FermatNo (N) = 2 \to FermatNo (N) \gcd FermatNo (M) = 1))$
47	37 46	mpd	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0}) \to (FermatNo (M) \gcd FermatNo (N) = 2 \to FermatNo (N) \gcd FermatNo (M) = 1)$
48	47	3adant3	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to (FermatNo (M) \gcd FermatNo (N) = 2 \to FermatNo (N) \gcd FermatNo (M) = 1)$
49		gcdcom	$⊢ (FermatNo (M) \in ℤ \land FermatNo (N) \in ℤ) \to FermatNo (M) \gcd FermatNo (N) = FermatNo (N) \gcd FermatNo (M)$
50	6 49	syl	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to FermatNo (M) \gcd FermatNo (N) = FermatNo (N) \gcd FermatNo (M)$
51	50	eqeq1d	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to (FermatNo (M) \gcd FermatNo (N) = 1 \leftrightarrow FermatNo (N) \gcd FermatNo (M) = 1)$
52	51	biimpd	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to (FermatNo (M) \gcd FermatNo (N) = 1 \to FermatNo (N) \gcd FermatNo (M) = 1)$
53	48 52	jaod	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to ((FermatNo (M) \gcd FermatNo (N) = 2 \lor FermatNo (M) \gcd FermatNo (N) = 1) \to FermatNo (N) \gcd FermatNo (M) = 1)$
54	36 53	sylbid	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to ((FermatNo (M) \gcd FermatNo (N)) ∥ 2 \to FermatNo (N) \gcd FermatNo (M) = 1)$
55	29 54	sylbid	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to ((FermatNo (M) \gcd FermatNo (N)) ∥ (FermatNo (N) - (FermatNo (N) - 2)) \to FermatNo (N) \gcd FermatNo (M) = 1)$
56	24 55	syld	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to (((FermatNo (M) \gcd FermatNo (N)) ∥ (FermatNo (N) - 2) \land (FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (N)) \to FermatNo (N) \gcd FermatNo (M) = 1)$
57	20 56	syland	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to (((FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (M) \land (FermatNo (M) \gcd FermatNo (N)) ∥ FermatNo (N)) \to FermatNo (N) \gcd FermatNo (M) = 1)$
58	8 57	mpd	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to FermatNo (N) \gcd FermatNo (M) = 1$

Metamath Proof Explorer

Theorem goldbachthlem2

Proof