Theorem expsgt0

Description: A non-negative surreal integer power is positive if its base is positive. (Contributed by Scott Fenton, 7-Aug-2025)

	Ref	Expression
Assertion	expsgt0	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕ0s ∧ 0s <s 𝐴 ) → 0s <s ( 𝐴 ↑s 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑚 = 0s → ( 𝐴 ↑s 𝑚 ) = ( 𝐴 ↑s 0s ) )
2	1	breq2d	⊢ ( 𝑚 = 0s → ( 0s <s ( 𝐴 ↑s 𝑚 ) ↔ 0s <s ( 𝐴 ↑s 0s ) ) )
3	2	imbi2d	⊢ ( 𝑚 = 0s → ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) → 0s <s ( 𝐴 ↑s 𝑚 ) ) ↔ ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) → 0s <s ( 𝐴 ↑s 0s ) ) ) )
4		oveq2	⊢ ( 𝑚 = 𝑛 → ( 𝐴 ↑s 𝑚 ) = ( 𝐴 ↑s 𝑛 ) )
5	4	breq2d	⊢ ( 𝑚 = 𝑛 → ( 0s <s ( 𝐴 ↑s 𝑚 ) ↔ 0s <s ( 𝐴 ↑s 𝑛 ) ) )
6	5	imbi2d	⊢ ( 𝑚 = 𝑛 → ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) → 0s <s ( 𝐴 ↑s 𝑚 ) ) ↔ ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) → 0s <s ( 𝐴 ↑s 𝑛 ) ) ) )
7		oveq2	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 𝐴 ↑s 𝑚 ) = ( 𝐴 ↑s ( 𝑛 +s 1s ) ) )
8	7	breq2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 0s <s ( 𝐴 ↑s 𝑚 ) ↔ 0s <s ( 𝐴 ↑s ( 𝑛 +s 1s ) ) ) )
9	8	imbi2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) → 0s <s ( 𝐴 ↑s 𝑚 ) ) ↔ ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) → 0s <s ( 𝐴 ↑s ( 𝑛 +s 1s ) ) ) ) )
10		oveq2	⊢ ( 𝑚 = 𝑁 → ( 𝐴 ↑s 𝑚 ) = ( 𝐴 ↑s 𝑁 ) )
11	10	breq2d	⊢ ( 𝑚 = 𝑁 → ( 0s <s ( 𝐴 ↑s 𝑚 ) ↔ 0s <s ( 𝐴 ↑s 𝑁 ) ) )
12	11	imbi2d	⊢ ( 𝑚 = 𝑁 → ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) → 0s <s ( 𝐴 ↑s 𝑚 ) ) ↔ ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) → 0s <s ( 𝐴 ↑s 𝑁 ) ) ) )
13		0slt1s	⊢ 0s <s 1s
14		exps0	⊢ ( 𝐴 ∈ No → ( 𝐴 ↑s 0s ) = 1s )
15	13 14	breqtrrid	⊢ ( 𝐴 ∈ No → 0s <s ( 𝐴 ↑s 0s ) )
16	15	adantr	⊢ ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) → 0s <s ( 𝐴 ↑s 0s ) )
17		simp2l	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ 0s <s ( 𝐴 ↑s 𝑛 ) ) → 𝐴 ∈ No )
18		simp1	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ 0s <s ( 𝐴 ↑s 𝑛 ) ) → 𝑛 ∈ ℕ0s )
19		expscl	⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( 𝐴 ↑s 𝑛 ) ∈ No )
20	17 18 19	syl2anc	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ 0s <s ( 𝐴 ↑s 𝑛 ) ) → ( 𝐴 ↑s 𝑛 ) ∈ No )
21		simp3	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ 0s <s ( 𝐴 ↑s 𝑛 ) ) → 0s <s ( 𝐴 ↑s 𝑛 ) )
22		simp2r	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ 0s <s ( 𝐴 ↑s 𝑛 ) ) → 0s <s 𝐴 )
23	20 17 21 22	mulsgt0d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ 0s <s ( 𝐴 ↑s 𝑛 ) ) → 0s <s ( ( 𝐴 ↑s 𝑛 ) ·s 𝐴 ) )
24		expsp1	⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = ( ( 𝐴 ↑s 𝑛 ) ·s 𝐴 ) )
25	17 18 24	syl2anc	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ 0s <s ( 𝐴 ↑s 𝑛 ) ) → ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = ( ( 𝐴 ↑s 𝑛 ) ·s 𝐴 ) )
26	23 25	breqtrrd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ 0s <s ( 𝐴 ↑s 𝑛 ) ) → 0s <s ( 𝐴 ↑s ( 𝑛 +s 1s ) ) )
27	26	3exp	⊢ ( 𝑛 ∈ ℕ0s → ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) → ( 0s <s ( 𝐴 ↑s 𝑛 ) → 0s <s ( 𝐴 ↑s ( 𝑛 +s 1s ) ) ) ) )
28	27	a2d	⊢ ( 𝑛 ∈ ℕ0s → ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) → 0s <s ( 𝐴 ↑s 𝑛 ) ) → ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) → 0s <s ( 𝐴 ↑s ( 𝑛 +s 1s ) ) ) ) )
29	3 6 9 12 16 28	n0sind	⊢ ( 𝑁 ∈ ℕ0s → ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) → 0s <s ( 𝐴 ↑s 𝑁 ) ) )
30	29	expd	⊢ ( 𝑁 ∈ ℕ0s → ( 𝐴 ∈ No → ( 0s <s 𝐴 → 0s <s ( 𝐴 ↑s 𝑁 ) ) ) )
31	30	3imp21	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕ0s ∧ 0s <s 𝐴 ) → 0s <s ( 𝐴 ↑s 𝑁 ) )