lighneallem1

		Ref	Expression
	Assertion	lighneallem1	$⊢ (P = 2 \land M \in ℕ \land N \in ℕ) \to 2^{N} - 1 \neq P^{M}$

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2		simp2	$⊢ (P = 2 \land M \in ℕ \land N \in ℕ) \to M \in ℕ$
3		iddvdsexp	$⊢ (2 \in ℤ \land M \in ℕ) \to 2 ∥ 2^{M}$
4	1 2 3	sylancr	$⊢ (P = 2 \land M \in ℕ \land N \in ℕ) \to 2 ∥ 2^{M}$
5		oveq1	$⊢ P = 2 \to P^{M} = 2^{M}$
6	5	breq2d	$⊢ P = 2 \to (2 ∥ P^{M} \leftrightarrow 2 ∥ 2^{M})$
7	6	3ad2ant1	$⊢ (P = 2 \land M \in ℕ \land N \in ℕ) \to (2 ∥ P^{M} \leftrightarrow 2 ∥ 2^{M})$
8	4 7	mpbird	$⊢ (P = 2 \land M \in ℕ \land N \in ℕ) \to 2 ∥ P^{M}$
9		iddvdsexp	$⊢ (2 \in ℤ \land N \in ℕ) \to 2 ∥ 2^{N}$
10	1 9	mpan	$⊢ N \in ℕ \to 2 ∥ 2^{N}$
11	10	notnotd	$⊢ N \in ℕ \to \neg \neg 2 ∥ 2^{N}$
12		2nn	$⊢ 2 \in ℕ$
13	12	a1i	$⊢ N \in ℕ \to 2 \in ℕ$
14		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
15	13 14	nnexpcld	$⊢ N \in ℕ \to 2^{N} \in ℕ$
16	15	nnzd	$⊢ N \in ℕ \to 2^{N} \in ℤ$
17		oddm1even	$⊢ 2^{N} \in ℤ \to (\neg 2 ∥ 2^{N} \leftrightarrow 2 ∥ (2^{N} - 1))$
18	16 17	syl	$⊢ N \in ℕ \to (\neg 2 ∥ 2^{N} \leftrightarrow 2 ∥ (2^{N} - 1))$
19	11 18	mtbid	$⊢ N \in ℕ \to \neg 2 ∥ (2^{N} - 1)$
20	19	3ad2ant3	$⊢ (P = 2 \land M \in ℕ \land N \in ℕ) \to \neg 2 ∥ (2^{N} - 1)$
21		nbrne1	$⊢ (2 ∥ P^{M} \land \neg 2 ∥ (2^{N} - 1)) \to P^{M} \neq 2^{N} - 1$
22	8 20 21	syl2anc	$⊢ (P = 2 \land M \in ℕ \land N \in ℕ) \to P^{M} \neq 2^{N} - 1$
23	22	necomd	$⊢ (P = 2 \land M \in ℕ \land N \in ℕ) \to 2^{N} - 1 \neq P^{M}$

Metamath Proof Explorer