prmdvdsfmtnof1lem2

		Ref	Expression
	Assertion	prmdvdsfmtnof1lem2	$⊢ (F \in ran FermatNo \land G \in ran FermatNo) \to ((I \in ℙ \land I ∥ F \land I ∥ G) \to F = G)$

Proof

Step	Hyp	Ref	Expression
1		fmtnorn	$⊢ F \in ran FermatNo \leftrightarrow \exists n \in ℕ_{0} FermatNo (n) = F$
2		fmtnorn	$⊢ G \in ran FermatNo \leftrightarrow \exists m \in ℕ_{0} FermatNo (m) = G$
3		2a1	$⊢ F = G \to (FermatNo (n) = F \to ((I \in ℙ \land I ∥ F \land I ∥ G) \to F = G))$
4	3	2a1d	$⊢ F = G \to ((n \in ℕ_{0} \land m \in ℕ_{0}) \to (FermatNo (m) = G \to (FermatNo (n) = F \to ((I \in ℙ \land I ∥ F \land I ∥ G) \to F = G))))$
5		fmtnonn	$⊢ n \in ℕ_{0} \to FermatNo (n) \in ℕ$
6	5	ad2antrl	$⊢ (\neg F = G \land (n \in ℕ_{0} \land m \in ℕ_{0})) \to FermatNo (n) \in ℕ$
7	6	adantr	$⊢ ((\neg F = G \land (n \in ℕ_{0} \land m \in ℕ_{0})) \land (FermatNo (m) = G \land FermatNo (n) = F)) \to FermatNo (n) \in ℕ$
8		eleq1	$⊢ FermatNo (n) = F \to (FermatNo (n) \in ℕ \leftrightarrow F \in ℕ)$
9	8	ad2antll	$⊢ ((\neg F = G \land (n \in ℕ_{0} \land m \in ℕ_{0})) \land (FermatNo (m) = G \land FermatNo (n) = F)) \to (FermatNo (n) \in ℕ \leftrightarrow F \in ℕ)$
10	7 9	mpbid	$⊢ ((\neg F = G \land (n \in ℕ_{0} \land m \in ℕ_{0})) \land (FermatNo (m) = G \land FermatNo (n) = F)) \to F \in ℕ$
11		fmtnonn	$⊢ m \in ℕ_{0} \to FermatNo (m) \in ℕ$
12	11	ad2antll	$⊢ (\neg F = G \land (n \in ℕ_{0} \land m \in ℕ_{0})) \to FermatNo (m) \in ℕ$
13	12	adantr	$⊢ ((\neg F = G \land (n \in ℕ_{0} \land m \in ℕ_{0})) \land (FermatNo (m) = G \land FermatNo (n) = F)) \to FermatNo (m) \in ℕ$
14		eleq1	$⊢ FermatNo (m) = G \to (FermatNo (m) \in ℕ \leftrightarrow G \in ℕ)$
15	14	ad2antrl	$⊢ ((\neg F = G \land (n \in ℕ_{0} \land m \in ℕ_{0})) \land (FermatNo (m) = G \land FermatNo (n) = F)) \to (FermatNo (m) \in ℕ \leftrightarrow G \in ℕ)$
16	13 15	mpbid	$⊢ ((\neg F = G \land (n \in ℕ_{0} \land m \in ℕ_{0})) \land (FermatNo (m) = G \land FermatNo (n) = F)) \to G \in ℕ$
17		simpll	$⊢ ((n \in ℕ_{0} \land m \in ℕ_{0}) \land \neg FermatNo (n) = FermatNo (m)) \to n \in ℕ_{0}$
18		simplr	$⊢ ((n \in ℕ_{0} \land m \in ℕ_{0}) \land \neg FermatNo (n) = FermatNo (m)) \to m \in ℕ_{0}$
19		fveq2	$⊢ n = m \to FermatNo (n) = FermatNo (m)$
20	19	con3i	$⊢ \neg FermatNo (n) = FermatNo (m) \to \neg n = m$
21	20	adantl	$⊢ ((n \in ℕ_{0} \land m \in ℕ_{0}) \land \neg FermatNo (n) = FermatNo (m)) \to \neg n = m$
22	21	neqned	$⊢ ((n \in ℕ_{0} \land m \in ℕ_{0}) \land \neg FermatNo (n) = FermatNo (m)) \to n \neq m$
23		goldbachth	$⊢ (n \in ℕ_{0} \land m \in ℕ_{0} \land n \neq m) \to FermatNo (n) \gcd FermatNo (m) = 1$
24	17 18 22 23	syl3anc	$⊢ ((n \in ℕ_{0} \land m \in ℕ_{0}) \land \neg FermatNo (n) = FermatNo (m)) \to FermatNo (n) \gcd FermatNo (m) = 1$
25	24	ex	$⊢ (n \in ℕ_{0} \land m \in ℕ_{0}) \to (\neg FermatNo (n) = FermatNo (m) \to FermatNo (n) \gcd FermatNo (m) = 1)$
26		eqeq12	$⊢ (FermatNo (n) = F \land FermatNo (m) = G) \to (FermatNo (n) = FermatNo (m) \leftrightarrow F = G)$
27	26	notbid	$⊢ (FermatNo (n) = F \land FermatNo (m) = G) \to (\neg FermatNo (n) = FermatNo (m) \leftrightarrow \neg F = G)$
28		oveq12	$⊢ (FermatNo (n) = F \land FermatNo (m) = G) \to FermatNo (n) \gcd FermatNo (m) = F \gcd G$
29	28	eqeq1d	$⊢ (FermatNo (n) = F \land FermatNo (m) = G) \to (FermatNo (n) \gcd FermatNo (m) = 1 \leftrightarrow F \gcd G = 1)$
30	27 29	imbi12d	$⊢ (FermatNo (n) = F \land FermatNo (m) = G) \to ((\neg FermatNo (n) = FermatNo (m) \to FermatNo (n) \gcd FermatNo (m) = 1) \leftrightarrow (\neg F = G \to F \gcd G = 1))$
31	30	ancoms	$⊢ (FermatNo (m) = G \land FermatNo (n) = F) \to ((\neg FermatNo (n) = FermatNo (m) \to FermatNo (n) \gcd FermatNo (m) = 1) \leftrightarrow (\neg F = G \to F \gcd G = 1))$
32	25 31	syl5ibcom	$⊢ (n \in ℕ_{0} \land m \in ℕ_{0}) \to ((FermatNo (m) = G \land FermatNo (n) = F) \to (\neg F = G \to F \gcd G = 1))$
33	32	com23	$⊢ (n \in ℕ_{0} \land m \in ℕ_{0}) \to (\neg F = G \to ((FermatNo (m) = G \land FermatNo (n) = F) \to F \gcd G = 1))$
34	33	impcom	$⊢ (\neg F = G \land (n \in ℕ_{0} \land m \in ℕ_{0})) \to ((FermatNo (m) = G \land FermatNo (n) = F) \to F \gcd G = 1)$
35	34	imp	$⊢ ((\neg F = G \land (n \in ℕ_{0} \land m \in ℕ_{0})) \land (FermatNo (m) = G \land FermatNo (n) = F)) \to F \gcd G = 1$
36		prmnn	$⊢ I \in ℙ \to I \in ℕ$
37		coprmdvds1	$⊢ (F \in ℕ \land G \in ℕ \land F \gcd G = 1) \to ((I \in ℕ \land I ∥ F \land I ∥ G) \to I = 1)$
38	37	imp	$⊢ ((F \in ℕ \land G \in ℕ \land F \gcd G = 1) \land (I \in ℕ \land I ∥ F \land I ∥ G)) \to I = 1$
39	36 38	syl3anr1	$⊢ ((F \in ℕ \land G \in ℕ \land F \gcd G = 1) \land (I \in ℙ \land I ∥ F \land I ∥ G)) \to I = 1$
40		eleq1	$⊢ I = 1 \to (I \in ℙ \leftrightarrow 1 \in ℙ)$
41		1nprm	$⊢ \neg 1 \in ℙ$
42	41	pm2.21i	$⊢ 1 \in ℙ \to F = G$
43	40 42	syl6bi	$⊢ I = 1 \to (I \in ℙ \to F = G)$
44	43	com12	$⊢ I \in ℙ \to (I = 1 \to F = G)$
45	44	a1d	$⊢ I \in ℙ \to ((F \in ℕ \land G \in ℕ \land F \gcd G = 1) \to (I = 1 \to F = G))$
46	45	3ad2ant1	$⊢ (I \in ℙ \land I ∥ F \land I ∥ G) \to ((F \in ℕ \land G \in ℕ \land F \gcd G = 1) \to (I = 1 \to F = G))$
47	46	impcom	$⊢ ((F \in ℕ \land G \in ℕ \land F \gcd G = 1) \land (I \in ℙ \land I ∥ F \land I ∥ G)) \to (I = 1 \to F = G)$
48	39 47	mpd	$⊢ ((F \in ℕ \land G \in ℕ \land F \gcd G = 1) \land (I \in ℙ \land I ∥ F \land I ∥ G)) \to F = G$
49	48	ex	$⊢ (F \in ℕ \land G \in ℕ \land F \gcd G = 1) \to ((I \in ℙ \land I ∥ F \land I ∥ G) \to F = G)$
50	10 16 35 49	syl3anc	$⊢ ((\neg F = G \land (n \in ℕ_{0} \land m \in ℕ_{0})) \land (FermatNo (m) = G \land FermatNo (n) = F)) \to ((I \in ℙ \land I ∥ F \land I ∥ G) \to F = G)$
51	50	exp43	$⊢ \neg F = G \to ((n \in ℕ_{0} \land m \in ℕ_{0}) \to (FermatNo (m) = G \to (FermatNo (n) = F \to ((I \in ℙ \land I ∥ F \land I ∥ G) \to F = G))))$
52	4 51	pm2.61i	$⊢ (n \in ℕ_{0} \land m \in ℕ_{0}) \to (FermatNo (m) = G \to (FermatNo (n) = F \to ((I \in ℙ \land I ∥ F \land I ∥ G) \to F = G)))$
53	52	rexlimdva	$⊢ n \in ℕ_{0} \to (\exists m \in ℕ_{0} FermatNo (m) = G \to (FermatNo (n) = F \to ((I \in ℙ \land I ∥ F \land I ∥ G) \to F = G)))$
54	53	com23	$⊢ n \in ℕ_{0} \to (FermatNo (n) = F \to (\exists m \in ℕ_{0} FermatNo (m) = G \to ((I \in ℙ \land I ∥ F \land I ∥ G) \to F = G)))$
55	54	rexlimiv	$⊢ \exists n \in ℕ_{0} FermatNo (n) = F \to (\exists m \in ℕ_{0} FermatNo (m) = G \to ((I \in ℙ \land I ∥ F \land I ∥ G) \to F = G))$
56	55	imp	$⊢ (\exists n \in ℕ_{0} FermatNo (n) = F \land \exists m \in ℕ_{0} FermatNo (m) = G) \to ((I \in ℙ \land I ∥ F \land I ∥ G) \to F = G)$
57	1 2 56	syl2anb	$⊢ (F \in ran FermatNo \land G \in ran FermatNo) \to ((I \in ℙ \land I ∥ F \land I ∥ G) \to F = G)$

Metamath Proof Explorer

Theorem prmdvdsfmtnof1lem2

Proof