expgt0b

Description: A real number A raised to an odd integer power is positive iff it is positive. (Contributed by SN, 4-Mar-2023) Use the more standard -. 2 || N (Revised by Thierry Arnoux, 14-Jun-2025)

	Ref	Expression
Hypotheses	expgt0b.n	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	expgt0b.m	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	expgt0b.1	⊢ ( 𝜑 → ¬ 2 ∥ 𝑁 )
Assertion	expgt0b	⊢ ( 𝜑 → ( 0 < 𝐴 ↔ 0 < ( 𝐴 ↑ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		expgt0b.n	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		expgt0b.m	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3		expgt0b.1	⊢ ( 𝜑 → ¬ 2 ∥ 𝑁 )
4	1	adantr	⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 𝐴 ∈ ℝ )
5	2	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
6	5	adantr	⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 𝑁 ∈ ℤ )
7		simpr	⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 0 < 𝐴 )
8		expgt0	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 0 < 𝐴 ) → 0 < ( 𝐴 ↑ 𝑁 ) )
9	4 6 7 8	syl3anc	⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 0 < ( 𝐴 ↑ 𝑁 ) )
10	9	ex	⊢ ( 𝜑 → ( 0 < 𝐴 → 0 < ( 𝐴 ↑ 𝑁 ) ) )
11		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
12	11 1	lttrid	⊢ ( 𝜑 → ( 0 < 𝐴 ↔ ¬ ( 0 = 𝐴 ∨ 𝐴 < 0 ) ) )
13	12	notbid	⊢ ( 𝜑 → ( ¬ 0 < 𝐴 ↔ ¬ ¬ ( 0 = 𝐴 ∨ 𝐴 < 0 ) ) )
14		notnotr	⊢ ( ¬ ¬ ( 0 = 𝐴 ∨ 𝐴 < 0 ) → ( 0 = 𝐴 ∨ 𝐴 < 0 ) )
15		0re	⊢ 0 ∈ ℝ
16	15	ltnri	⊢ ¬ 0 < 0
17	2	0expd	⊢ ( 𝜑 → ( 0 ↑ 𝑁 ) = 0 )
18	17	breq2d	⊢ ( 𝜑 → ( 0 < ( 0 ↑ 𝑁 ) ↔ 0 < 0 ) )
19	16 18	mtbiri	⊢ ( 𝜑 → ¬ 0 < ( 0 ↑ 𝑁 ) )
20	19	adantr	⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → ¬ 0 < ( 0 ↑ 𝑁 ) )
21		simpr	⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → 0 = 𝐴 )
22	21	eqcomd	⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → 𝐴 = 0 )
23	22	oveq1d	⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → ( 𝐴 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
24	23	breq2d	⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → ( 0 < ( 𝐴 ↑ 𝑁 ) ↔ 0 < ( 0 ↑ 𝑁 ) ) )
25	20 24	mtbird	⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → ¬ 0 < ( 𝐴 ↑ 𝑁 ) )
26	25	ex	⊢ ( 𝜑 → ( 0 = 𝐴 → ¬ 0 < ( 𝐴 ↑ 𝑁 ) ) )
27	1	renegcld	⊢ ( 𝜑 → - 𝐴 ∈ ℝ )
28	27	adantr	⊢ ( ( 𝜑 ∧ 0 < - 𝐴 ) → - 𝐴 ∈ ℝ )
29	5	adantr	⊢ ( ( 𝜑 ∧ 0 < - 𝐴 ) → 𝑁 ∈ ℤ )
30		simpr	⊢ ( ( 𝜑 ∧ 0 < - 𝐴 ) → 0 < - 𝐴 )
31		expgt0	⊢ ( ( - 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 0 < - 𝐴 ) → 0 < ( - 𝐴 ↑ 𝑁 ) )
32	28 29 30 31	syl3anc	⊢ ( ( 𝜑 ∧ 0 < - 𝐴 ) → 0 < ( - 𝐴 ↑ 𝑁 ) )
33	32	ex	⊢ ( 𝜑 → ( 0 < - 𝐴 → 0 < ( - 𝐴 ↑ 𝑁 ) ) )
34	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
35		oexpneg	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( - 𝐴 ↑ 𝑁 ) = - ( 𝐴 ↑ 𝑁 ) )
36	34 2 3 35	syl3anc	⊢ ( 𝜑 → ( - 𝐴 ↑ 𝑁 ) = - ( 𝐴 ↑ 𝑁 ) )
37	36	breq2d	⊢ ( 𝜑 → ( 0 < ( - 𝐴 ↑ 𝑁 ) ↔ 0 < - ( 𝐴 ↑ 𝑁 ) ) )
38	37	biimpd	⊢ ( 𝜑 → ( 0 < ( - 𝐴 ↑ 𝑁 ) → 0 < - ( 𝐴 ↑ 𝑁 ) ) )
39	2	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
40	1 39	reexpcld	⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℝ )
41	40	renegcld	⊢ ( 𝜑 → - ( 𝐴 ↑ 𝑁 ) ∈ ℝ )
42	11 41	lttrid	⊢ ( 𝜑 → ( 0 < - ( 𝐴 ↑ 𝑁 ) ↔ ¬ ( 0 = - ( 𝐴 ↑ 𝑁 ) ∨ - ( 𝐴 ↑ 𝑁 ) < 0 ) ) )
43		pm2.46	⊢ ( ¬ ( 0 = - ( 𝐴 ↑ 𝑁 ) ∨ - ( 𝐴 ↑ 𝑁 ) < 0 ) → ¬ - ( 𝐴 ↑ 𝑁 ) < 0 )
44	42 43	biimtrdi	⊢ ( 𝜑 → ( 0 < - ( 𝐴 ↑ 𝑁 ) → ¬ - ( 𝐴 ↑ 𝑁 ) < 0 ) )
45	33 38 44	3syld	⊢ ( 𝜑 → ( 0 < - 𝐴 → ¬ - ( 𝐴 ↑ 𝑁 ) < 0 ) )
46	1	lt0neg1d	⊢ ( 𝜑 → ( 𝐴 < 0 ↔ 0 < - 𝐴 ) )
47	40	lt0neg2d	⊢ ( 𝜑 → ( 0 < ( 𝐴 ↑ 𝑁 ) ↔ - ( 𝐴 ↑ 𝑁 ) < 0 ) )
48	47	notbid	⊢ ( 𝜑 → ( ¬ 0 < ( 𝐴 ↑ 𝑁 ) ↔ ¬ - ( 𝐴 ↑ 𝑁 ) < 0 ) )
49	45 46 48	3imtr4d	⊢ ( 𝜑 → ( 𝐴 < 0 → ¬ 0 < ( 𝐴 ↑ 𝑁 ) ) )
50	26 49	jaod	⊢ ( 𝜑 → ( ( 0 = 𝐴 ∨ 𝐴 < 0 ) → ¬ 0 < ( 𝐴 ↑ 𝑁 ) ) )
51	14 50	syl5	⊢ ( 𝜑 → ( ¬ ¬ ( 0 = 𝐴 ∨ 𝐴 < 0 ) → ¬ 0 < ( 𝐴 ↑ 𝑁 ) ) )
52	13 51	sylbid	⊢ ( 𝜑 → ( ¬ 0 < 𝐴 → ¬ 0 < ( 𝐴 ↑ 𝑁 ) ) )
53	10 52	impcon4bid	⊢ ( 𝜑 → ( 0 < 𝐴 ↔ 0 < ( 𝐴 ↑ 𝑁 ) ) )

Metamath Proof Explorer

Theorem expgt0b

Proof