lighneallem4b

		Ref	Expression
	Assertion	lighneallem4b	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k} \in ℤ_{\geq 2}$

Proof

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2	1	a1i	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to 2 \in ℤ$
3		fzfid	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2}) \to (0 \dots M - 1) \in Fin$
4		neg1z	$⊢ - 1 \in ℤ$
5		elfznn0	$⊢ k \in (0 \dots M - 1) \to k \in ℕ_{0}$
6		zexpcl	$⊢ (- 1 \in ℤ \land k \in ℕ_{0}) \to {(- 1)}^{k} \in ℤ$
7	4 5 6	sylancr	$⊢ k \in (0 \dots M - 1) \to {(- 1)}^{k} \in ℤ$
8	7	adantl	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2}) \land k \in (0 \dots M - 1)) \to {(- 1)}^{k} \in ℤ$
9		eluzge2nn0	$⊢ A \in ℤ_{\geq 2} \to A \in ℕ_{0}$
10	9	adantr	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2}) \to A \in ℕ_{0}$
11	10	adantr	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2}) \land k \in (0 \dots M - 1)) \to A \in ℕ_{0}$
12	5	adantl	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2}) \land k \in (0 \dots M - 1)) \to k \in ℕ_{0}$
13	11 12	nn0expcld	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2}) \land k \in (0 \dots M - 1)) \to A^{k} \in ℕ_{0}$
14	13	nn0zd	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2}) \land k \in (0 \dots M - 1)) \to A^{k} \in ℤ$
15	8 14	zmulcld	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2}) \land k \in (0 \dots M - 1)) \to {(- 1)}^{k} A^{k} \in ℤ$
16	3 15	fsumzcl	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2}) \to \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k} \in ℤ$
17	16	3adant3	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k} \in ℤ$
18		simp1	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to A \in ℤ_{\geq 2}$
19		3z	$⊢ 3 \in ℤ$
20	19	a1i	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to 3 \in ℤ$
21		eluzelz	$⊢ M \in ℤ_{\geq 2} \to M \in ℤ$
22	21	3ad2ant2	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to M \in ℤ$
23		eluz2	$⊢ M \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land M \in ℤ \land 2 \leq M)$
24		2re	$⊢ 2 \in ℝ$
25	24	a1i	$⊢ M \in ℤ \to 2 \in ℝ$
26		zre	$⊢ M \in ℤ \to M \in ℝ$
27	25 26	leloed	$⊢ M \in ℤ \to (2 \leq M \leftrightarrow (2 < M \lor 2 = M))$
28		zltp1le	$⊢ (2 \in ℤ \land M \in ℤ) \to (2 < M \leftrightarrow 2 + 1 \leq M)$
29	1 28	mpan	$⊢ M \in ℤ \to (2 < M \leftrightarrow 2 + 1 \leq M)$
30	29	biimpd	$⊢ M \in ℤ \to (2 < M \to 2 + 1 \leq M)$
31		df-3	$⊢ 3 = 2 + 1$
32	31	breq1i	$⊢ 3 \leq M \leftrightarrow 2 + 1 \leq M$
33	30 32	imbitrrdi	$⊢ M \in ℤ \to (2 < M \to 3 \leq M)$
34	33	a1i	$⊢ \neg 2 ∥ M \to (M \in ℤ \to (2 < M \to 3 \leq M))$
35	34	com13	$⊢ 2 < M \to (M \in ℤ \to (\neg 2 ∥ M \to 3 \leq M))$
36		z2even	$⊢ 2 ∥ 2$
37		breq2	$⊢ 2 = M \to (2 ∥ 2 \leftrightarrow 2 ∥ M)$
38	36 37	mpbii	$⊢ 2 = M \to 2 ∥ M$
39	38	pm2.24d	$⊢ 2 = M \to (\neg 2 ∥ M \to 3 \leq M)$
40	39	a1d	$⊢ 2 = M \to (M \in ℤ \to (\neg 2 ∥ M \to 3 \leq M))$
41	35 40	jaoi	$⊢ (2 < M \lor 2 = M) \to (M \in ℤ \to (\neg 2 ∥ M \to 3 \leq M))$
42	41	com12	$⊢ M \in ℤ \to ((2 < M \lor 2 = M) \to (\neg 2 ∥ M \to 3 \leq M))$
43	27 42	sylbid	$⊢ M \in ℤ \to (2 \leq M \to (\neg 2 ∥ M \to 3 \leq M))$
44	43	imp	$⊢ (M \in ℤ \land 2 \leq M) \to (\neg 2 ∥ M \to 3 \leq M)$
45	44	3adant1	$⊢ (2 \in ℤ \land M \in ℤ \land 2 \leq M) \to (\neg 2 ∥ M \to 3 \leq M)$
46	23 45	sylbi	$⊢ M \in ℤ_{\geq 2} \to (\neg 2 ∥ M \to 3 \leq M)$
47	46	imp	$⊢ (M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to 3 \leq M$
48	47	3adant1	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to 3 \leq M$
49		eluz2	$⊢ M \in ℤ_{\geq 3} \leftrightarrow (3 \in ℤ \land M \in ℤ \land 3 \leq M)$
50	20 22 48 49	syl3anbrc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to M \in ℤ_{\geq 3}$
51		eluzelcn	$⊢ A \in ℤ_{\geq 2} \to A \in ℂ$
52	51	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to A \in ℂ$
53		eluz2nn	$⊢ M \in ℤ_{\geq 2} \to M \in ℕ$
54	53	3ad2ant2	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to M \in ℕ$
55		simp3	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to \neg 2 ∥ M$
56	52 54 55	oddpwp1fsum	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to A^{M} + 1 = (A + 1) \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k}$
57	56	eqcomd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to (A + 1) \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k} = A^{M} + 1$
58		eluzge2nn0	$⊢ M \in ℤ_{\geq 2} \to M \in ℕ_{0}$
59	58	adantl	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2}) \to M \in ℕ_{0}$
60	10 59	nn0expcld	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2}) \to A^{M} \in ℕ_{0}$
61	60	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2}) \to A^{M} \in ℂ$
62		peano2cn	$⊢ A^{M} \in ℂ \to A^{M} + 1 \in ℂ$
63	61 62	syl	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2}) \to A^{M} + 1 \in ℂ$
64	63	3adant3	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to A^{M} + 1 \in ℂ$
65	17	zcnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k} \in ℂ$
66		eluz2nn	$⊢ A \in ℤ_{\geq 2} \to A \in ℕ$
67	66	peano2nnd	$⊢ A \in ℤ_{\geq 2} \to A + 1 \in ℕ$
68	67	nncnd	$⊢ A \in ℤ_{\geq 2} \to A + 1 \in ℂ$
69	67	nnne0d	$⊢ A \in ℤ_{\geq 2} \to A + 1 \neq 0$
70	68 69	jca	$⊢ A \in ℤ_{\geq 2} \to (A + 1 \in ℂ \land A + 1 \neq 0)$
71	70	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to (A + 1 \in ℂ \land A + 1 \neq 0)$
72		divmul	$⊢ (A^{M} + 1 \in ℂ \land \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k} \in ℂ \land (A + 1 \in ℂ \land A + 1 \neq 0)) \to (\frac{A^{M} + 1}{A + 1} = \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k} \leftrightarrow (A + 1) \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k} = A^{M} + 1)$
73	64 65 71 72	syl3anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to (\frac{A^{M} + 1}{A + 1} = \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k} \leftrightarrow (A + 1) \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k} = A^{M} + 1)$
74	57 73	mpbird	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to \frac{A^{M} + 1}{A + 1} = \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k}$
75	74	eqcomd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k} = \frac{A^{M} + 1}{A + 1}$
76		lighneallem4a	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 3} \land \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k} = \frac{A^{M} + 1}{A + 1}) \to 2 \leq \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k}$
77	18 50 75 76	syl3anc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to 2 \leq \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k}$
78		eluz2	$⊢ \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k} \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k} \in ℤ \land 2 \leq \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k})$
79	2 17 77 78	syl3anbrc	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to \sum_{k = 0}^{M - 1} {(- 1)}^{k} A^{k} \in ℤ_{\geq 2}$

Metamath Proof Explorer

Theorem lighneallem4b

Proof