goldbachth

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

Proof

Step	Hyp	Ref	Expression
1		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
2		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
3		lttri4	$⊢ (N \in ℝ \land M \in ℝ) \to (N < M \lor N = M \lor M < N)$
4	1 2 3	syl2an	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0}) \to (N < M \lor N = M \lor M < N)$
5	4	3adant3	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land N \neq M) \to (N < M \lor N = M \lor M < N)$
6		fmtnonn	$⊢ N \in ℕ_{0} \to FermatNo (N) \in ℕ$
7	6	nnzd	$⊢ N \in ℕ_{0} \to FermatNo (N) \in ℤ$
8		fmtnonn	$⊢ M \in ℕ_{0} \to FermatNo (M) \in ℕ$
9	8	nnzd	$⊢ M \in ℕ_{0} \to FermatNo (M) \in ℤ$
10		gcdcom	$⊢ (FermatNo (N) \in ℤ \land FermatNo (M) \in ℤ) \to FermatNo (N) \gcd FermatNo (M) = FermatNo (M) \gcd FermatNo (N)$
11	7 9 10	syl2anr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to FermatNo (N) \gcd FermatNo (M) = FermatNo (M) \gcd FermatNo (N)$
12	11	3adant3	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0} \land N < M) \to FermatNo (N) \gcd FermatNo (M) = FermatNo (M) \gcd FermatNo (N)$
13		goldbachthlem2	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0} \land N < M) \to FermatNo (M) \gcd FermatNo (N) = 1$
14	12 13	eqtrd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0} \land N < M) \to FermatNo (N) \gcd FermatNo (M) = 1$
15	14	3exp	$⊢ M \in ℕ_{0} \to (N \in ℕ_{0} \to (N < M \to FermatNo (N) \gcd FermatNo (M) = 1))$
16	15	impcom	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0}) \to (N < M \to FermatNo (N) \gcd FermatNo (M) = 1)$
17	16	3adant3	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land N \neq M) \to (N < M \to FermatNo (N) \gcd FermatNo (M) = 1)$
18		eqneqall	$⊢ N = M \to (N \neq M \to FermatNo (N) \gcd FermatNo (M) = 1)$
19	18	com12	$⊢ N \neq M \to (N = M \to FermatNo (N) \gcd FermatNo (M) = 1)$
20	19	3ad2ant3	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land N \neq M) \to (N = M \to FermatNo (N) \gcd FermatNo (M) = 1)$
21		goldbachthlem2	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land M < N) \to FermatNo (N) \gcd FermatNo (M) = 1$
22	21	3expia	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0}) \to (M < N \to FermatNo (N) \gcd FermatNo (M) = 1)$
23	22	3adant3	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land N \neq M) \to (M < N \to FermatNo (N) \gcd FermatNo (M) = 1)$
24	17 20 23	3jaod	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land N \neq M) \to ((N < M \lor N = M \lor M < N) \to FermatNo (N) \gcd FermatNo (M) = 1)$
25	5 24	mpd	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0} \land N \neq M) \to FermatNo (N) \gcd FermatNo (M) = 1$

Metamath Proof Explorer

Theorem goldbachth

Proof