Theorem lighneallem1

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

	Ref	Expression
Assertion	lighneallem1	|- ( ( P = 2 /\ M e. NN /\ N e. NN ) -> ( ( 2 ^ N ) - 1 ) =/= ( P ^ M ) )

Proof

Step	Hyp	Ref	Expression
1		2z	|- 2 e. ZZ
2		simp2	|- ( ( P = 2 /\ M e. NN /\ N e. NN ) -> M e. NN )
3		iddvdsexp	|- ( ( 2 e. ZZ /\ M e. NN ) -> 2 || ( 2 ^ M ) )
4	1 2 3	sylancr	|- ( ( P = 2 /\ M e. NN /\ N e. NN ) -> 2 || ( 2 ^ M ) )
5		oveq1	|- ( P = 2 -> ( P ^ M ) = ( 2 ^ M ) )
6	5	breq2d	|- ( P = 2 -> ( 2 || ( P ^ M ) <-> 2 || ( 2 ^ M ) ) )
7	6	3ad2ant1	|- ( ( P = 2 /\ M e. NN /\ N e. NN ) -> ( 2 || ( P ^ M ) <-> 2 || ( 2 ^ M ) ) )
8	4 7	mpbird	|- ( ( P = 2 /\ M e. NN /\ N e. NN ) -> 2 || ( P ^ M ) )
9		iddvdsexp	|- ( ( 2 e. ZZ /\ N e. NN ) -> 2 || ( 2 ^ N ) )
10	1 9	mpan	|- ( N e. NN -> 2 || ( 2 ^ N ) )
11	10	notnotd	|- ( N e. NN -> -. -. 2 || ( 2 ^ N ) )
12		2nn	|- 2 e. NN
13	12	a1i	|- ( N e. NN -> 2 e. NN )
14		nnnn0	|- ( N e. NN -> N e. NN0 )
15	13 14	nnexpcld	|- ( N e. NN -> ( 2 ^ N ) e. NN )
16	15	nnzd	|- ( N e. NN -> ( 2 ^ N ) e. ZZ )
17		oddm1even	|- ( ( 2 ^ N ) e. ZZ -> ( -. 2 || ( 2 ^ N ) <-> 2 || ( ( 2 ^ N ) - 1 ) ) )
18	16 17	syl	|- ( N e. NN -> ( -. 2 || ( 2 ^ N ) <-> 2 || ( ( 2 ^ N ) - 1 ) ) )
19	11 18	mtbid	|- ( N e. NN -> -. 2 || ( ( 2 ^ N ) - 1 ) )
20	19	3ad2ant3	|- ( ( P = 2 /\ M e. NN /\ N e. NN ) -> -. 2 || ( ( 2 ^ N ) - 1 ) )
21		nbrne1	|- ( ( 2 || ( P ^ M ) /\ -. 2 || ( ( 2 ^ N ) - 1 ) ) -> ( P ^ M ) =/= ( ( 2 ^ N ) - 1 ) )
22	8 20 21	syl2anc	|- ( ( P = 2 /\ M e. NN /\ N e. NN ) -> ( P ^ M ) =/= ( ( 2 ^ N ) - 1 ) )
23	22	necomd	|- ( ( P = 2 /\ M e. NN /\ N e. NN ) -> ( ( 2 ^ N ) - 1 ) =/= ( P ^ M ) )