fmtnofac2lem

Description: Lemma for fmtnofac2 (Induction step). (Contributed by AV, 30-Jul-2021)

		Ref	Expression
	Assertion	fmtnofac2lem	$⊢ (y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to ((((N \in ℤ_{\geq 2} \land y ∥ FermatNo (N)) \to \exists k \in ℕ_{0} y = k 2^{N + 2} + 1) \land ((N \in ℤ_{\geq 2} \land z ∥ FermatNo (N)) \to \exists k \in ℕ_{0} z = k 2^{N + 2} + 1)) \to ((N \in ℤ_{\geq 2} \land y z ∥ FermatNo (N)) \to \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1))$

Proof

Step	Hyp	Ref	Expression
1		eluzelz	$⊢ y \in ℤ_{\geq 2} \to y \in ℤ$
2	1	adantr	$⊢ (y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to y \in ℤ$
3		eluzelz	$⊢ z \in ℤ_{\geq 2} \to z \in ℤ$
4	3	adantl	$⊢ (y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to z \in ℤ$
5		eluzge2nn0	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ_{0}$
6		fmtnonn	$⊢ N \in ℕ_{0} \to FermatNo (N) \in ℕ$
7	6	nnzd	$⊢ N \in ℕ_{0} \to FermatNo (N) \in ℤ$
8	5 7	syl	$⊢ N \in ℤ_{\geq 2} \to FermatNo (N) \in ℤ$
9		muldvds2	$⊢ (y \in ℤ \land z \in ℤ \land FermatNo (N) \in ℤ) \to (y z ∥ FermatNo (N) \to z ∥ FermatNo (N))$
10	2 4 8 9	syl2an3an	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land N \in ℤ_{\geq 2}) \to (y z ∥ FermatNo (N) \to z ∥ FermatNo (N))$
11		muldvds1	$⊢ (y \in ℤ \land z \in ℤ \land FermatNo (N) \in ℤ) \to (y z ∥ FermatNo (N) \to y ∥ FermatNo (N))$
12	2 4 8 11	syl2an3an	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land N \in ℤ_{\geq 2}) \to (y z ∥ FermatNo (N) \to y ∥ FermatNo (N))$
13		pm2.27	$⊢ (N \in ℤ_{\geq 2} \land y ∥ FermatNo (N)) \to (((N \in ℤ_{\geq 2} \land y ∥ FermatNo (N)) \to \exists k \in ℕ_{0} y = k 2^{N + 2} + 1) \to \exists k \in ℕ_{0} y = k 2^{N + 2} + 1)$
14	13	ad2ant2lr	$⊢ (((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land N \in ℤ_{\geq 2}) \land (y ∥ FermatNo (N) \land z ∥ FermatNo (N))) \to (((N \in ℤ_{\geq 2} \land y ∥ FermatNo (N)) \to \exists k \in ℕ_{0} y = k 2^{N + 2} + 1) \to \exists k \in ℕ_{0} y = k 2^{N + 2} + 1)$
15		pm2.27	$⊢ (N \in ℤ_{\geq 2} \land z ∥ FermatNo (N)) \to (((N \in ℤ_{\geq 2} \land z ∥ FermatNo (N)) \to \exists k \in ℕ_{0} z = k 2^{N + 2} + 1) \to \exists k \in ℕ_{0} z = k 2^{N + 2} + 1)$
16	15	ad2ant2l	$⊢ (((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land N \in ℤ_{\geq 2}) \land (y ∥ FermatNo (N) \land z ∥ FermatNo (N))) \to (((N \in ℤ_{\geq 2} \land z ∥ FermatNo (N)) \to \exists k \in ℕ_{0} z = k 2^{N + 2} + 1) \to \exists k \in ℕ_{0} z = k 2^{N + 2} + 1)$
17		oveq1	$⊢ k = m \to k 2^{N + 2} = m 2^{N + 2}$
18	17	oveq1d	$⊢ k = m \to k 2^{N + 2} + 1 = m 2^{N + 2} + 1$
19	18	eqeq2d	$⊢ k = m \to (y = k 2^{N + 2} + 1 \leftrightarrow y = m 2^{N + 2} + 1)$
20	19	cbvrexvw	$⊢ \exists k \in ℕ_{0} y = k 2^{N + 2} + 1 \leftrightarrow \exists m \in ℕ_{0} y = m 2^{N + 2} + 1$
21		oveq1	$⊢ k = n \to k 2^{N + 2} = n 2^{N + 2}$
22	21	oveq1d	$⊢ k = n \to k 2^{N + 2} + 1 = n 2^{N + 2} + 1$
23	22	eqeq2d	$⊢ k = n \to (z = k 2^{N + 2} + 1 \leftrightarrow z = n 2^{N + 2} + 1)$
24	23	cbvrexvw	$⊢ \exists k \in ℕ_{0} z = k 2^{N + 2} + 1 \leftrightarrow \exists n \in ℕ_{0} z = n 2^{N + 2} + 1$
25		simpl	$⊢ (m \in ℕ_{0} \land n \in ℕ_{0}) \to m \in ℕ_{0}$
26	25	adantl	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to m \in ℕ_{0}$
27		2nn0	$⊢ 2 \in ℕ_{0}$
28	27	a1i	$⊢ N \in ℤ_{\geq 2} \to 2 \in ℕ_{0}$
29	5 28	nn0addcld	$⊢ N \in ℤ_{\geq 2} \to N + 2 \in ℕ_{0}$
30	28 29	nn0expcld	$⊢ N \in ℤ_{\geq 2} \to 2^{N + 2} \in ℕ_{0}$
31	30	adantr	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to 2^{N + 2} \in ℕ_{0}$
32	26 31	nn0mulcld	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to m 2^{N + 2} \in ℕ_{0}$
33		simpr	$⊢ (m \in ℕ_{0} \land n \in ℕ_{0}) \to n \in ℕ_{0}$
34	33	adantl	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to n \in ℕ_{0}$
35	32 34	nn0mulcld	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to m 2^{N + 2} n \in ℕ_{0}$
36		nn0addcl	$⊢ (m \in ℕ_{0} \land n \in ℕ_{0}) \to m + n \in ℕ_{0}$
37	36	adantl	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to m + n \in ℕ_{0}$
38	35 37	nn0addcld	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to m 2^{N + 2} n + m + n \in ℕ_{0}$
39		oveq1	$⊢ k = m 2^{N + 2} n + m + n \to k 2^{N + 2} = (m 2^{N + 2} n + m + n) 2^{N + 2}$
40	39	oveq1d	$⊢ k = m 2^{N + 2} n + m + n \to k 2^{N + 2} + 1 = (m 2^{N + 2} n + m + n) 2^{N + 2} + 1$
41	40	eqeq2d	$⊢ k = m 2^{N + 2} n + m + n \to ((m 2^{N + 2} n + m + n) 2^{N + 2} + 1 = k 2^{N + 2} + 1 \leftrightarrow (m 2^{N + 2} n + m + n) 2^{N + 2} + 1 = (m 2^{N + 2} n + m + n) 2^{N + 2} + 1)$
42	41	adantl	$⊢ ((N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land k = m 2^{N + 2} n + m + n) \to ((m 2^{N + 2} n + m + n) 2^{N + 2} + 1 = k 2^{N + 2} + 1 \leftrightarrow (m 2^{N + 2} n + m + n) 2^{N + 2} + 1 = (m 2^{N + 2} n + m + n) 2^{N + 2} + 1)$
43		eqidd	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to (m 2^{N + 2} n + m + n) 2^{N + 2} + 1 = (m 2^{N + 2} n + m + n) 2^{N + 2} + 1$
44	38 42 43	rspcedvd	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to \exists k \in ℕ_{0} (m 2^{N + 2} n + m + n) 2^{N + 2} + 1 = k 2^{N + 2} + 1$
45		nn0cn	$⊢ m \in ℕ_{0} \to m \in ℂ$
46	45	adantr	$⊢ (m \in ℕ_{0} \land n \in ℕ_{0}) \to m \in ℂ$
47	46	adantl	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to m \in ℂ$
48	30	nn0cnd	$⊢ N \in ℤ_{\geq 2} \to 2^{N + 2} \in ℂ$
49	48	adantr	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to 2^{N + 2} \in ℂ$
50	47 49	mulcld	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to m 2^{N + 2} \in ℂ$
51	33	nn0cnd	$⊢ (m \in ℕ_{0} \land n \in ℕ_{0}) \to n \in ℂ$
52	51	adantl	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to n \in ℂ$
53	52 49	mulcld	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to n 2^{N + 2} \in ℂ$
54	50 53	jca	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to (m 2^{N + 2} \in ℂ \land n 2^{N + 2} \in ℂ)$
55	54	adantr	$⊢ ((N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land k \in ℕ_{0}) \to (m 2^{N + 2} \in ℂ \land n 2^{N + 2} \in ℂ)$
56		muladd11r	$⊢ (m 2^{N + 2} \in ℂ \land n 2^{N + 2} \in ℂ) \to (m 2^{N + 2} + 1) (n 2^{N + 2} + 1) = m 2^{N + 2} n 2^{N + 2} + (m 2^{N + 2} + n 2^{N + 2}) + 1$
57	55 56	syl	$⊢ ((N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land k \in ℕ_{0}) \to (m 2^{N + 2} + 1) (n 2^{N + 2} + 1) = m 2^{N + 2} n 2^{N + 2} + (m 2^{N + 2} + n 2^{N + 2}) + 1$
58	25	nn0cnd	$⊢ (m \in ℕ_{0} \land n \in ℕ_{0}) \to m \in ℂ$
59	58	adantl	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to m \in ℂ$
60	59 52 49	3jca	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to (m \in ℂ \land n \in ℂ \land 2^{N + 2} \in ℂ)$
61	60	adantr	$⊢ ((N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land k \in ℕ_{0}) \to (m \in ℂ \land n \in ℂ \land 2^{N + 2} \in ℂ)$
62		adddir	$⊢ (m \in ℂ \land n \in ℂ \land 2^{N + 2} \in ℂ) \to (m + n) 2^{N + 2} = m 2^{N + 2} + n 2^{N + 2}$
63	61 62	syl	$⊢ ((N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land k \in ℕ_{0}) \to (m + n) 2^{N + 2} = m 2^{N + 2} + n 2^{N + 2}$
64	63	eqcomd	$⊢ ((N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land k \in ℕ_{0}) \to m 2^{N + 2} + n 2^{N + 2} = (m + n) 2^{N + 2}$
65	64	oveq2d	$⊢ ((N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land k \in ℕ_{0}) \to m 2^{N + 2} n 2^{N + 2} + m 2^{N + 2} + n 2^{N + 2} = m 2^{N + 2} n 2^{N + 2} + (m + n) 2^{N + 2}$
66	50	adantr	$⊢ ((N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land k \in ℕ_{0}) \to m 2^{N + 2} \in ℂ$
67	52	adantr	$⊢ ((N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land k \in ℕ_{0}) \to n \in ℂ$
68	49	adantr	$⊢ ((N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land k \in ℕ_{0}) \to 2^{N + 2} \in ℂ$
69	66 67 68	mulassd	$⊢ ((N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land k \in ℕ_{0}) \to m 2^{N + 2} n 2^{N + 2} = m 2^{N + 2} n 2^{N + 2}$
70	69	eqcomd	$⊢ ((N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land k \in ℕ_{0}) \to m 2^{N + 2} n 2^{N + 2} = m 2^{N + 2} n 2^{N + 2}$
71	70	oveq1d	$⊢ ((N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land k \in ℕ_{0}) \to m 2^{N + 2} n 2^{N + 2} + m 2^{N + 2} + n 2^{N + 2} = m 2^{N + 2} n 2^{N + 2} + m 2^{N + 2} + n 2^{N + 2}$
72	50 52	mulcld	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to m 2^{N + 2} n \in ℂ$
73	36	nn0cnd	$⊢ (m \in ℕ_{0} \land n \in ℕ_{0}) \to m + n \in ℂ$
74	73	adantl	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to m + n \in ℂ$
75	72 74 49	3jca	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to (m 2^{N + 2} n \in ℂ \land m + n \in ℂ \land 2^{N + 2} \in ℂ)$
76	75	adantr	$⊢ ((N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land k \in ℕ_{0}) \to (m 2^{N + 2} n \in ℂ \land m + n \in ℂ \land 2^{N + 2} \in ℂ)$
77		adddir	$⊢ (m 2^{N + 2} n \in ℂ \land m + n \in ℂ \land 2^{N + 2} \in ℂ) \to (m 2^{N + 2} n + m + n) 2^{N + 2} = m 2^{N + 2} n 2^{N + 2} + (m + n) 2^{N + 2}$
78	76 77	syl	$⊢ ((N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land k \in ℕ_{0}) \to (m 2^{N + 2} n + m + n) 2^{N + 2} = m 2^{N + 2} n 2^{N + 2} + (m + n) 2^{N + 2}$
79	65 71 78	3eqtr4d	$⊢ ((N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land k \in ℕ_{0}) \to m 2^{N + 2} n 2^{N + 2} + m 2^{N + 2} + n 2^{N + 2} = (m 2^{N + 2} n + m + n) 2^{N + 2}$
80	79	oveq1d	$⊢ ((N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land k \in ℕ_{0}) \to m 2^{N + 2} n 2^{N + 2} + (m 2^{N + 2} + n 2^{N + 2}) + 1 = (m 2^{N + 2} n + m + n) 2^{N + 2} + 1$
81	57 80	eqtrd	$⊢ ((N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land k \in ℕ_{0}) \to (m 2^{N + 2} + 1) (n 2^{N + 2} + 1) = (m 2^{N + 2} n + m + n) 2^{N + 2} + 1$
82	81	eqeq1d	$⊢ ((N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land k \in ℕ_{0}) \to ((m 2^{N + 2} + 1) (n 2^{N + 2} + 1) = k 2^{N + 2} + 1 \leftrightarrow (m 2^{N + 2} n + m + n) 2^{N + 2} + 1 = k 2^{N + 2} + 1)$
83	82	rexbidva	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to (\exists k \in ℕ_{0} (m 2^{N + 2} + 1) (n 2^{N + 2} + 1) = k 2^{N + 2} + 1 \leftrightarrow \exists k \in ℕ_{0} (m 2^{N + 2} n + m + n) 2^{N + 2} + 1 = k 2^{N + 2} + 1)$
84	44 83	mpbird	$⊢ (N \in ℤ_{\geq 2} \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to \exists k \in ℕ_{0} (m 2^{N + 2} + 1) (n 2^{N + 2} + 1) = k 2^{N + 2} + 1$
85	84	adantll	$⊢ (((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land N \in ℤ_{\geq 2}) \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to \exists k \in ℕ_{0} (m 2^{N + 2} + 1) (n 2^{N + 2} + 1) = k 2^{N + 2} + 1$
86		oveq12	$⊢ (y = m 2^{N + 2} + 1 \land z = n 2^{N + 2} + 1) \to y z = (m 2^{N + 2} + 1) (n 2^{N + 2} + 1)$
87	86	ancoms	$⊢ (z = n 2^{N + 2} + 1 \land y = m 2^{N + 2} + 1) \to y z = (m 2^{N + 2} + 1) (n 2^{N + 2} + 1)$
88	87	eqeq1d	$⊢ (z = n 2^{N + 2} + 1 \land y = m 2^{N + 2} + 1) \to (y z = k 2^{N + 2} + 1 \leftrightarrow (m 2^{N + 2} + 1) (n 2^{N + 2} + 1) = k 2^{N + 2} + 1)$
89	88	rexbidv	$⊢ (z = n 2^{N + 2} + 1 \land y = m 2^{N + 2} + 1) \to (\exists k \in ℕ_{0} y z = k 2^{N + 2} + 1 \leftrightarrow \exists k \in ℕ_{0} (m 2^{N + 2} + 1) (n 2^{N + 2} + 1) = k 2^{N + 2} + 1)$
90	85 89	syl5ibrcom	$⊢ (((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land N \in ℤ_{\geq 2}) \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to ((z = n 2^{N + 2} + 1 \land y = m 2^{N + 2} + 1) \to \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1)$
91	90	expd	$⊢ (((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land N \in ℤ_{\geq 2}) \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to (z = n 2^{N + 2} + 1 \to (y = m 2^{N + 2} + 1 \to \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1))$
92	91	anassrs	$⊢ ((((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land N \in ℤ_{\geq 2}) \land m \in ℕ_{0}) \land n \in ℕ_{0}) \to (z = n 2^{N + 2} + 1 \to (y = m 2^{N + 2} + 1 \to \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1))$
93	92	rexlimdva	$⊢ (((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land N \in ℤ_{\geq 2}) \land m \in ℕ_{0}) \to (\exists n \in ℕ_{0} z = n 2^{N + 2} + 1 \to (y = m 2^{N + 2} + 1 \to \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1))$
94	24 93	biimtrid	$⊢ (((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land N \in ℤ_{\geq 2}) \land m \in ℕ_{0}) \to (\exists k \in ℕ_{0} z = k 2^{N + 2} + 1 \to (y = m 2^{N + 2} + 1 \to \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1))$
95	94	com23	$⊢ (((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land N \in ℤ_{\geq 2}) \land m \in ℕ_{0}) \to (y = m 2^{N + 2} + 1 \to (\exists k \in ℕ_{0} z = k 2^{N + 2} + 1 \to \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1))$
96	95	rexlimdva	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land N \in ℤ_{\geq 2}) \to (\exists m \in ℕ_{0} y = m 2^{N + 2} + 1 \to (\exists k \in ℕ_{0} z = k 2^{N + 2} + 1 \to \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1))$
97	20 96	biimtrid	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land N \in ℤ_{\geq 2}) \to (\exists k \in ℕ_{0} y = k 2^{N + 2} + 1 \to (\exists k \in ℕ_{0} z = k 2^{N + 2} + 1 \to \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1))$
98	97	impd	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land N \in ℤ_{\geq 2}) \to ((\exists k \in ℕ_{0} y = k 2^{N + 2} + 1 \land \exists k \in ℕ_{0} z = k 2^{N + 2} + 1) \to \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1)$
99	98	adantr	$⊢ (((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land N \in ℤ_{\geq 2}) \land (y ∥ FermatNo (N) \land z ∥ FermatNo (N))) \to ((\exists k \in ℕ_{0} y = k 2^{N + 2} + 1 \land \exists k \in ℕ_{0} z = k 2^{N + 2} + 1) \to \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1)$
100	14 16 99	syl2and	$⊢ (((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land N \in ℤ_{\geq 2}) \land (y ∥ FermatNo (N) \land z ∥ FermatNo (N))) \to ((((N \in ℤ_{\geq 2} \land y ∥ FermatNo (N)) \to \exists k \in ℕ_{0} y = k 2^{N + 2} + 1) \land ((N \in ℤ_{\geq 2} \land z ∥ FermatNo (N)) \to \exists k \in ℕ_{0} z = k 2^{N + 2} + 1)) \to \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1)$
101	100	exp32	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land N \in ℤ_{\geq 2}) \to (y ∥ FermatNo (N) \to (z ∥ FermatNo (N) \to ((((N \in ℤ_{\geq 2} \land y ∥ FermatNo (N)) \to \exists k \in ℕ_{0} y = k 2^{N + 2} + 1) \land ((N \in ℤ_{\geq 2} \land z ∥ FermatNo (N)) \to \exists k \in ℕ_{0} z = k 2^{N + 2} + 1)) \to \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1)))$
102	12 101	syld	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land N \in ℤ_{\geq 2}) \to (y z ∥ FermatNo (N) \to (z ∥ FermatNo (N) \to ((((N \in ℤ_{\geq 2} \land y ∥ FermatNo (N)) \to \exists k \in ℕ_{0} y = k 2^{N + 2} + 1) \land ((N \in ℤ_{\geq 2} \land z ∥ FermatNo (N)) \to \exists k \in ℕ_{0} z = k 2^{N + 2} + 1)) \to \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1)))$
103	10 102	mpdd	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land N \in ℤ_{\geq 2}) \to (y z ∥ FermatNo (N) \to ((((N \in ℤ_{\geq 2} \land y ∥ FermatNo (N)) \to \exists k \in ℕ_{0} y = k 2^{N + 2} + 1) \land ((N \in ℤ_{\geq 2} \land z ∥ FermatNo (N)) \to \exists k \in ℕ_{0} z = k 2^{N + 2} + 1)) \to \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1))$
104	103	expimpd	$⊢ (y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to ((N \in ℤ_{\geq 2} \land y z ∥ FermatNo (N)) \to ((((N \in ℤ_{\geq 2} \land y ∥ FermatNo (N)) \to \exists k \in ℕ_{0} y = k 2^{N + 2} + 1) \land ((N \in ℤ_{\geq 2} \land z ∥ FermatNo (N)) \to \exists k \in ℕ_{0} z = k 2^{N + 2} + 1)) \to \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1))$
105	104	com23	$⊢ (y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to ((((N \in ℤ_{\geq 2} \land y ∥ FermatNo (N)) \to \exists k \in ℕ_{0} y = k 2^{N + 2} + 1) \land ((N \in ℤ_{\geq 2} \land z ∥ FermatNo (N)) \to \exists k \in ℕ_{0} z = k 2^{N + 2} + 1)) \to ((N \in ℤ_{\geq 2} \land y z ∥ FermatNo (N)) \to \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1))$

Metamath Proof Explorer

Theorem fmtnofac2lem

Proof