Theorem expnngt1

Description: If an integer power with a positive integer base is greater than 1, then the exponent is positive. (Contributed by AV, 28-Dec-2022)

	Ref	Expression
Assertion	expnngt1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 1 < ( 𝐴 ↑ 𝐵 ) ) → 𝐵 ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		elznn	⊢ ( 𝐵 ∈ ℤ ↔ ( 𝐵 ∈ ℝ ∧ ( 𝐵 ∈ ℕ ∨ - 𝐵 ∈ ℕ0 ) ) )
2		2a1	⊢ ( 𝐵 ∈ ℕ → ( 𝐴 ∈ ℕ → ( 1 < ( 𝐴 ↑ 𝐵 ) → 𝐵 ∈ ℕ ) ) )
3	2	a1d	⊢ ( 𝐵 ∈ ℕ → ( 𝐵 ∈ ℝ → ( 𝐴 ∈ ℕ → ( 1 < ( 𝐴 ↑ 𝐵 ) → 𝐵 ∈ ℕ ) ) ) )
4		nncn	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
5	4	3ad2ant3	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℕ ) → 𝐴 ∈ ℂ )
6		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
7	6	3ad2ant2	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℕ ) → 𝐵 ∈ ℂ )
8		simp1	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℕ ) → - 𝐵 ∈ ℕ0 )
9		expneg2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ - 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐵 ) = ( 1 / ( 𝐴 ↑ - 𝐵 ) ) )
10	5 7 8 9	syl3anc	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℕ ) → ( 𝐴 ↑ 𝐵 ) = ( 1 / ( 𝐴 ↑ - 𝐵 ) ) )
11	10	breq2d	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℕ ) → ( 1 < ( 𝐴 ↑ 𝐵 ) ↔ 1 < ( 1 / ( 𝐴 ↑ - 𝐵 ) ) ) )
12		nnre	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ )
13		reexpcl	⊢ ( ( 𝐴 ∈ ℝ ∧ - 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝐵 ) ∈ ℝ )
14	12 13	sylan	⊢ ( ( 𝐴 ∈ ℕ ∧ - 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝐵 ) ∈ ℝ )
15	14	ancoms	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ) → ( 𝐴 ↑ - 𝐵 ) ∈ ℝ )
16	12	adantl	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ) → 𝐴 ∈ ℝ )
17		nn0z	⊢ ( - 𝐵 ∈ ℕ0 → - 𝐵 ∈ ℤ )
18	17	adantr	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ) → - 𝐵 ∈ ℤ )
19		nngt0	⊢ ( 𝐴 ∈ ℕ → 0 < 𝐴 )
20	19	adantl	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ) → 0 < 𝐴 )
21		expgt0	⊢ ( ( 𝐴 ∈ ℝ ∧ - 𝐵 ∈ ℤ ∧ 0 < 𝐴 ) → 0 < ( 𝐴 ↑ - 𝐵 ) )
22	16 18 20 21	syl3anc	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ) → 0 < ( 𝐴 ↑ - 𝐵 ) )
23	15 22	jca	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ) → ( ( 𝐴 ↑ - 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐴 ↑ - 𝐵 ) ) )
24	23	3adant2	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℕ ) → ( ( 𝐴 ↑ - 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐴 ↑ - 𝐵 ) ) )
25		reclt1	⊢ ( ( ( 𝐴 ↑ - 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐴 ↑ - 𝐵 ) ) → ( ( 𝐴 ↑ - 𝐵 ) < 1 ↔ 1 < ( 1 / ( 𝐴 ↑ - 𝐵 ) ) ) )
26	24 25	syl	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℕ ) → ( ( 𝐴 ↑ - 𝐵 ) < 1 ↔ 1 < ( 1 / ( 𝐴 ↑ - 𝐵 ) ) ) )
27	12	3ad2ant3	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℕ ) → 𝐴 ∈ ℝ )
28		nnge1	⊢ ( 𝐴 ∈ ℕ → 1 ≤ 𝐴 )
29	28	3ad2ant3	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℕ ) → 1 ≤ 𝐴 )
30	27 8 29	expge1d	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℕ ) → 1 ≤ ( 𝐴 ↑ - 𝐵 ) )
31		1red	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℕ ) → 1 ∈ ℝ )
32	15	3adant2	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℕ ) → ( 𝐴 ↑ - 𝐵 ) ∈ ℝ )
33	31 32	lenltd	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℕ ) → ( 1 ≤ ( 𝐴 ↑ - 𝐵 ) ↔ ¬ ( 𝐴 ↑ - 𝐵 ) < 1 ) )
34		pm2.21	⊢ ( ¬ ( 𝐴 ↑ - 𝐵 ) < 1 → ( ( 𝐴 ↑ - 𝐵 ) < 1 → 𝐵 ∈ ℕ ) )
35	33 34	syl6bi	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℕ ) → ( 1 ≤ ( 𝐴 ↑ - 𝐵 ) → ( ( 𝐴 ↑ - 𝐵 ) < 1 → 𝐵 ∈ ℕ ) ) )
36	30 35	mpd	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℕ ) → ( ( 𝐴 ↑ - 𝐵 ) < 1 → 𝐵 ∈ ℕ ) )
37	26 36	sylbird	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℕ ) → ( 1 < ( 1 / ( 𝐴 ↑ - 𝐵 ) ) → 𝐵 ∈ ℕ ) )
38	11 37	sylbid	⊢ ( ( - 𝐵 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℕ ) → ( 1 < ( 𝐴 ↑ 𝐵 ) → 𝐵 ∈ ℕ ) )
39	38	3exp	⊢ ( - 𝐵 ∈ ℕ0 → ( 𝐵 ∈ ℝ → ( 𝐴 ∈ ℕ → ( 1 < ( 𝐴 ↑ 𝐵 ) → 𝐵 ∈ ℕ ) ) ) )
40	3 39	jaoi	⊢ ( ( 𝐵 ∈ ℕ ∨ - 𝐵 ∈ ℕ0 ) → ( 𝐵 ∈ ℝ → ( 𝐴 ∈ ℕ → ( 1 < ( 𝐴 ↑ 𝐵 ) → 𝐵 ∈ ℕ ) ) ) )
41	40	impcom	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐵 ∈ ℕ ∨ - 𝐵 ∈ ℕ0 ) ) → ( 𝐴 ∈ ℕ → ( 1 < ( 𝐴 ↑ 𝐵 ) → 𝐵 ∈ ℕ ) ) )
42	1 41	sylbi	⊢ ( 𝐵 ∈ ℤ → ( 𝐴 ∈ ℕ → ( 1 < ( 𝐴 ↑ 𝐵 ) → 𝐵 ∈ ℕ ) ) )
43	42	3imp21	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 1 < ( 𝐴 ↑ 𝐵 ) ) → 𝐵 ∈ ℕ )