odd2np1lem

		Ref	Expression
	Assertion	odd2np1lem	$⊢ N \in ℕ_{0} \to (\exists n \in ℤ 2 n + 1 = N \lor \exists k \in ℤ k \cdot 2 = N)$

Proof

Step	Hyp	Ref	Expression
1		eqeq2	$⊢ j = 0 \to (2 n + 1 = j \leftrightarrow 2 n + 1 = 0)$
2	1	rexbidv	$⊢ j = 0 \to (\exists n \in ℤ 2 n + 1 = j \leftrightarrow \exists n \in ℤ 2 n + 1 = 0)$
3		eqeq2	$⊢ j = 0 \to (k \cdot 2 = j \leftrightarrow k \cdot 2 = 0)$
4	3	rexbidv	$⊢ j = 0 \to (\exists k \in ℤ k \cdot 2 = j \leftrightarrow \exists k \in ℤ k \cdot 2 = 0)$
5	2 4	orbi12d	$⊢ j = 0 \to ((\exists n \in ℤ 2 n + 1 = j \lor \exists k \in ℤ k \cdot 2 = j) \leftrightarrow (\exists n \in ℤ 2 n + 1 = 0 \lor \exists k \in ℤ k \cdot 2 = 0))$
6		eqeq2	$⊢ j = m \to (2 n + 1 = j \leftrightarrow 2 n + 1 = m)$
7	6	rexbidv	$⊢ j = m \to (\exists n \in ℤ 2 n + 1 = j \leftrightarrow \exists n \in ℤ 2 n + 1 = m)$
8		oveq2	$⊢ n = x \to 2 n = 2 x$
9	8	oveq1d	$⊢ n = x \to 2 n + 1 = 2 x + 1$
10	9	eqeq1d	$⊢ n = x \to (2 n + 1 = m \leftrightarrow 2 x + 1 = m)$
11	10	cbvrexvw	$⊢ \exists n \in ℤ 2 n + 1 = m \leftrightarrow \exists x \in ℤ 2 x + 1 = m$
12	7 11	bitrdi	$⊢ j = m \to (\exists n \in ℤ 2 n + 1 = j \leftrightarrow \exists x \in ℤ 2 x + 1 = m)$
13		eqeq2	$⊢ j = m \to (k \cdot 2 = j \leftrightarrow k \cdot 2 = m)$
14	13	rexbidv	$⊢ j = m \to (\exists k \in ℤ k \cdot 2 = j \leftrightarrow \exists k \in ℤ k \cdot 2 = m)$
15		oveq1	$⊢ k = y \to k \cdot 2 = y \cdot 2$
16	15	eqeq1d	$⊢ k = y \to (k \cdot 2 = m \leftrightarrow y \cdot 2 = m)$
17	16	cbvrexvw	$⊢ \exists k \in ℤ k \cdot 2 = m \leftrightarrow \exists y \in ℤ y \cdot 2 = m$
18	14 17	bitrdi	$⊢ j = m \to (\exists k \in ℤ k \cdot 2 = j \leftrightarrow \exists y \in ℤ y \cdot 2 = m)$
19	12 18	orbi12d	$⊢ j = m \to ((\exists n \in ℤ 2 n + 1 = j \lor \exists k \in ℤ k \cdot 2 = j) \leftrightarrow (\exists x \in ℤ 2 x + 1 = m \lor \exists y \in ℤ y \cdot 2 = m))$
20		eqeq2	$⊢ j = m + 1 \to (2 n + 1 = j \leftrightarrow 2 n + 1 = m + 1)$
21	20	rexbidv	$⊢ j = m + 1 \to (\exists n \in ℤ 2 n + 1 = j \leftrightarrow \exists n \in ℤ 2 n + 1 = m + 1)$
22		eqeq2	$⊢ j = m + 1 \to (k \cdot 2 = j \leftrightarrow k \cdot 2 = m + 1)$
23	22	rexbidv	$⊢ j = m + 1 \to (\exists k \in ℤ k \cdot 2 = j \leftrightarrow \exists k \in ℤ k \cdot 2 = m + 1)$
24	21 23	orbi12d	$⊢ j = m + 1 \to ((\exists n \in ℤ 2 n + 1 = j \lor \exists k \in ℤ k \cdot 2 = j) \leftrightarrow (\exists n \in ℤ 2 n + 1 = m + 1 \lor \exists k \in ℤ k \cdot 2 = m + 1))$
25		eqeq2	$⊢ j = N \to (2 n + 1 = j \leftrightarrow 2 n + 1 = N)$
26	25	rexbidv	$⊢ j = N \to (\exists n \in ℤ 2 n + 1 = j \leftrightarrow \exists n \in ℤ 2 n + 1 = N)$
27		eqeq2	$⊢ j = N \to (k \cdot 2 = j \leftrightarrow k \cdot 2 = N)$
28	27	rexbidv	$⊢ j = N \to (\exists k \in ℤ k \cdot 2 = j \leftrightarrow \exists k \in ℤ k \cdot 2 = N)$
29	26 28	orbi12d	$⊢ j = N \to ((\exists n \in ℤ 2 n + 1 = j \lor \exists k \in ℤ k \cdot 2 = j) \leftrightarrow (\exists n \in ℤ 2 n + 1 = N \lor \exists k \in ℤ k \cdot 2 = N))$
30		0z	$⊢ 0 \in ℤ$
31		2cn	$⊢ 2 \in ℂ$
32	31	mul02i	$⊢ 0 \cdot 2 = 0$
33		oveq1	$⊢ k = 0 \to k \cdot 2 = 0 \cdot 2$
34	33	eqeq1d	$⊢ k = 0 \to (k \cdot 2 = 0 \leftrightarrow 0 \cdot 2 = 0)$
35	34	rspcev	$⊢ (0 \in ℤ \land 0 \cdot 2 = 0) \to \exists k \in ℤ k \cdot 2 = 0$
36	30 32 35	mp2an	$⊢ \exists k \in ℤ k \cdot 2 = 0$
37	36	olci	$⊢ (\exists n \in ℤ 2 n + 1 = 0 \lor \exists k \in ℤ k \cdot 2 = 0)$
38		orcom	$⊢ (\exists x \in ℤ 2 x + 1 = m \lor \exists y \in ℤ y \cdot 2 = m) \leftrightarrow (\exists y \in ℤ y \cdot 2 = m \lor \exists x \in ℤ 2 x + 1 = m)$
39		zcn	$⊢ y \in ℤ \to y \in ℂ$
40		mulcom	$⊢ (y \in ℂ \land 2 \in ℂ) \to y \cdot 2 = 2 y$
41	39 31 40	sylancl	$⊢ y \in ℤ \to y \cdot 2 = 2 y$
42	41	adantl	$⊢ (m \in ℕ_{0} \land y \in ℤ) \to y \cdot 2 = 2 y$
43	42	eqeq1d	$⊢ (m \in ℕ_{0} \land y \in ℤ) \to (y \cdot 2 = m \leftrightarrow 2 y = m)$
44		eqid	$⊢ 2 y + 1 = 2 y + 1$
45		oveq2	$⊢ n = y \to 2 n = 2 y$
46	45	oveq1d	$⊢ n = y \to 2 n + 1 = 2 y + 1$
47	46	eqeq1d	$⊢ n = y \to (2 n + 1 = 2 y + 1 \leftrightarrow 2 y + 1 = 2 y + 1)$
48	47	rspcev	$⊢ (y \in ℤ \land 2 y + 1 = 2 y + 1) \to \exists n \in ℤ 2 n + 1 = 2 y + 1$
49	44 48	mpan2	$⊢ y \in ℤ \to \exists n \in ℤ 2 n + 1 = 2 y + 1$
50		oveq1	$⊢ 2 y = m \to 2 y + 1 = m + 1$
51	50	eqeq2d	$⊢ 2 y = m \to (2 n + 1 = 2 y + 1 \leftrightarrow 2 n + 1 = m + 1)$
52	51	rexbidv	$⊢ 2 y = m \to (\exists n \in ℤ 2 n + 1 = 2 y + 1 \leftrightarrow \exists n \in ℤ 2 n + 1 = m + 1)$
53	49 52	syl5ibcom	$⊢ y \in ℤ \to (2 y = m \to \exists n \in ℤ 2 n + 1 = m + 1)$
54	53	adantl	$⊢ (m \in ℕ_{0} \land y \in ℤ) \to (2 y = m \to \exists n \in ℤ 2 n + 1 = m + 1)$
55	43 54	sylbid	$⊢ (m \in ℕ_{0} \land y \in ℤ) \to (y \cdot 2 = m \to \exists n \in ℤ 2 n + 1 = m + 1)$
56	55	rexlimdva	$⊢ m \in ℕ_{0} \to (\exists y \in ℤ y \cdot 2 = m \to \exists n \in ℤ 2 n + 1 = m + 1)$
57		peano2z	$⊢ x \in ℤ \to x + 1 \in ℤ$
58		zcn	$⊢ x \in ℤ \to x \in ℂ$
59		mulcom	$⊢ (x \in ℂ \land 2 \in ℂ) \to x \cdot 2 = 2 x$
60	31 59	mpan2	$⊢ x \in ℂ \to x \cdot 2 = 2 x$
61	31	mullidi	$⊢ 1 \cdot 2 = 2$
62	61	a1i	$⊢ x \in ℂ \to 1 \cdot 2 = 2$
63	60 62	oveq12d	$⊢ x \in ℂ \to x \cdot 2 + 1 \cdot 2 = 2 x + 2$
64		df-2	$⊢ 2 = 1 + 1$
65	64	oveq2i	$⊢ 2 x + 2 = 2 x + 1 + 1$
66	63 65	eqtrdi	$⊢ x \in ℂ \to x \cdot 2 + 1 \cdot 2 = 2 x + 1 + 1$
67		ax-1cn	$⊢ 1 \in ℂ$
68		adddir	$⊢ (x \in ℂ \land 1 \in ℂ \land 2 \in ℂ) \to (x + 1) \cdot 2 = x \cdot 2 + 1 \cdot 2$
69	67 31 68	mp3an23	$⊢ x \in ℂ \to (x + 1) \cdot 2 = x \cdot 2 + 1 \cdot 2$
70		mulcl	$⊢ (2 \in ℂ \land x \in ℂ) \to 2 x \in ℂ$
71	31 70	mpan	$⊢ x \in ℂ \to 2 x \in ℂ$
72		addass	$⊢ (2 x \in ℂ \land 1 \in ℂ \land 1 \in ℂ) \to 2 x + 1 + 1 = 2 x + 1 + 1$
73	67 67 72	mp3an23	$⊢ 2 x \in ℂ \to 2 x + 1 + 1 = 2 x + 1 + 1$
74	71 73	syl	$⊢ x \in ℂ \to 2 x + 1 + 1 = 2 x + 1 + 1$
75	66 69 74	3eqtr4d	$⊢ x \in ℂ \to (x + 1) \cdot 2 = 2 x + 1 + 1$
76	58 75	syl	$⊢ x \in ℤ \to (x + 1) \cdot 2 = 2 x + 1 + 1$
77	76	adantl	$⊢ (m \in ℕ_{0} \land x \in ℤ) \to (x + 1) \cdot 2 = 2 x + 1 + 1$
78		oveq1	$⊢ k = x + 1 \to k \cdot 2 = (x + 1) \cdot 2$
79	78	eqeq1d	$⊢ k = x + 1 \to (k \cdot 2 = 2 x + 1 + 1 \leftrightarrow (x + 1) \cdot 2 = 2 x + 1 + 1)$
80	79	rspcev	$⊢ (x + 1 \in ℤ \land (x + 1) \cdot 2 = 2 x + 1 + 1) \to \exists k \in ℤ k \cdot 2 = 2 x + 1 + 1$
81	57 77 80	syl2an2	$⊢ (m \in ℕ_{0} \land x \in ℤ) \to \exists k \in ℤ k \cdot 2 = 2 x + 1 + 1$
82		oveq1	$⊢ 2 x + 1 = m \to 2 x + 1 + 1 = m + 1$
83	82	eqeq2d	$⊢ 2 x + 1 = m \to (k \cdot 2 = 2 x + 1 + 1 \leftrightarrow k \cdot 2 = m + 1)$
84	83	rexbidv	$⊢ 2 x + 1 = m \to (\exists k \in ℤ k \cdot 2 = 2 x + 1 + 1 \leftrightarrow \exists k \in ℤ k \cdot 2 = m + 1)$
85	81 84	syl5ibcom	$⊢ (m \in ℕ_{0} \land x \in ℤ) \to (2 x + 1 = m \to \exists k \in ℤ k \cdot 2 = m + 1)$
86	85	rexlimdva	$⊢ m \in ℕ_{0} \to (\exists x \in ℤ 2 x + 1 = m \to \exists k \in ℤ k \cdot 2 = m + 1)$
87	56 86	orim12d	$⊢ m \in ℕ_{0} \to ((\exists y \in ℤ y \cdot 2 = m \lor \exists x \in ℤ 2 x + 1 = m) \to (\exists n \in ℤ 2 n + 1 = m + 1 \lor \exists k \in ℤ k \cdot 2 = m + 1))$
88	38 87	biimtrid	$⊢ m \in ℕ_{0} \to ((\exists x \in ℤ 2 x + 1 = m \lor \exists y \in ℤ y \cdot 2 = m) \to (\exists n \in ℤ 2 n + 1 = m + 1 \lor \exists k \in ℤ k \cdot 2 = m + 1))$
89	5 19 24 29 37 88	nn0ind	$⊢ N \in ℕ_{0} \to (\exists n \in ℤ 2 n + 1 = N \lor \exists k \in ℤ k \cdot 2 = N)$

Metamath Proof Explorer

Theorem odd2np1lem

Proof