Theorem lighneallem1

Description: Lemma 1 for lighneal . (Contributed by AV, 11-Aug-2021)

	Ref	Expression
Assertion	lighneallem1	⊢ ( ( 𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 2 ↑ 𝑁 ) − 1 ) ≠ ( 𝑃 ↑ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2		simp2	⊢ ( ( 𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℕ )
3		iddvdsexp	⊢ ( ( 2 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → 2 ∥ ( 2 ↑ 𝑀 ) )
4	1 2 3	sylancr	⊢ ( ( 𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 2 ∥ ( 2 ↑ 𝑀 ) )
5		oveq1	⊢ ( 𝑃 = 2 → ( 𝑃 ↑ 𝑀 ) = ( 2 ↑ 𝑀 ) )
6	5	breq2d	⊢ ( 𝑃 = 2 → ( 2 ∥ ( 𝑃 ↑ 𝑀 ) ↔ 2 ∥ ( 2 ↑ 𝑀 ) ) )
7	6	3ad2ant1	⊢ ( ( 𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 ∥ ( 𝑃 ↑ 𝑀 ) ↔ 2 ∥ ( 2 ↑ 𝑀 ) ) )
8	4 7	mpbird	⊢ ( ( 𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 2 ∥ ( 𝑃 ↑ 𝑀 ) )
9		iddvdsexp	⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 2 ∥ ( 2 ↑ 𝑁 ) )
10	1 9	mpan	⊢ ( 𝑁 ∈ ℕ → 2 ∥ ( 2 ↑ 𝑁 ) )
11	10	notnotd	⊢ ( 𝑁 ∈ ℕ → ¬ ¬ 2 ∥ ( 2 ↑ 𝑁 ) )
12		2nn	⊢ 2 ∈ ℕ
13	12	a1i	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℕ )
14		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
15	13 14	nnexpcld	⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ 𝑁 ) ∈ ℕ )
16	15	nnzd	⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ 𝑁 ) ∈ ℤ )
17		oddm1even	⊢ ( ( 2 ↑ 𝑁 ) ∈ ℤ → ( ¬ 2 ∥ ( 2 ↑ 𝑁 ) ↔ 2 ∥ ( ( 2 ↑ 𝑁 ) − 1 ) ) )
18	16 17	syl	⊢ ( 𝑁 ∈ ℕ → ( ¬ 2 ∥ ( 2 ↑ 𝑁 ) ↔ 2 ∥ ( ( 2 ↑ 𝑁 ) − 1 ) ) )
19	11 18	mtbid	⊢ ( 𝑁 ∈ ℕ → ¬ 2 ∥ ( ( 2 ↑ 𝑁 ) − 1 ) )
20	19	3ad2ant3	⊢ ( ( 𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ¬ 2 ∥ ( ( 2 ↑ 𝑁 ) − 1 ) )
21		nbrne1	⊢ ( ( 2 ∥ ( 𝑃 ↑ 𝑀 ) ∧ ¬ 2 ∥ ( ( 2 ↑ 𝑁 ) − 1 ) ) → ( 𝑃 ↑ 𝑀 ) ≠ ( ( 2 ↑ 𝑁 ) − 1 ) )
22	8 20 21	syl2anc	⊢ ( ( 𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑃 ↑ 𝑀 ) ≠ ( ( 2 ↑ 𝑁 ) − 1 ) )
23	22	necomd	⊢ ( ( 𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 2 ↑ 𝑁 ) − 1 ) ≠ ( 𝑃 ↑ 𝑀 ) )