Theorem avgslt2d

Description: Ordering property for average. (Contributed by Scott Fenton, 11-Dec-2025)

	Ref	Expression
Hypotheses	avgs.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	avgs.2	⊢ ( 𝜑 → 𝐵 ∈ No )
Assertion	avgslt2d	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 ↔ ( ( 𝐴 +s 𝐵 ) /su 2s ) <s 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		avgs.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		avgs.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3	1 2 2	sltadd1d	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 ↔ ( 𝐴 +s 𝐵 ) <s ( 𝐵 +s 𝐵 ) ) )
4		no2times	⊢ ( 𝐵 ∈ No → ( 2s ·s 𝐵 ) = ( 𝐵 +s 𝐵 ) )
5	2 4	syl	⊢ ( 𝜑 → ( 2s ·s 𝐵 ) = ( 𝐵 +s 𝐵 ) )
6	5	breq2d	⊢ ( 𝜑 → ( ( 𝐴 +s 𝐵 ) <s ( 2s ·s 𝐵 ) ↔ ( 𝐴 +s 𝐵 ) <s ( 𝐵 +s 𝐵 ) ) )
7	3 6	bitr4d	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 ↔ ( 𝐴 +s 𝐵 ) <s ( 2s ·s 𝐵 ) ) )
8		2sno	⊢ 2s ∈ No
9		exps1	⊢ ( 2s ∈ No → ( 2s ↑s 1s ) = 2s )
10	8 9	ax-mp	⊢ ( 2s ↑s 1s ) = 2s
11	10	oveq1i	⊢ ( ( 2s ↑s 1s ) ·s 𝐵 ) = ( 2s ·s 𝐵 )
12	11	breq2i	⊢ ( ( 𝐴 +s 𝐵 ) <s ( ( 2s ↑s 1s ) ·s 𝐵 ) ↔ ( 𝐴 +s 𝐵 ) <s ( 2s ·s 𝐵 ) )
13	7 12	bitr4di	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 ↔ ( 𝐴 +s 𝐵 ) <s ( ( 2s ↑s 1s ) ·s 𝐵 ) ) )
14	1 2	addscld	⊢ ( 𝜑 → ( 𝐴 +s 𝐵 ) ∈ No )
15		1n0s	⊢ 1s ∈ ℕ0s
16	15	a1i	⊢ ( 𝜑 → 1s ∈ ℕ0s )
17	14 2 16	pw2sltdivmuld	⊢ ( 𝜑 → ( ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s 1s ) ) <s 𝐵 ↔ ( 𝐴 +s 𝐵 ) <s ( ( 2s ↑s 1s ) ·s 𝐵 ) ) )
18	13 17	bitr4d	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 ↔ ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s 1s ) ) <s 𝐵 ) )
19	10	oveq2i	⊢ ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s 1s ) ) = ( ( 𝐴 +s 𝐵 ) /su 2s )
20	19	breq1i	⊢ ( ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s 1s ) ) <s 𝐵 ↔ ( ( 𝐴 +s 𝐵 ) /su 2s ) <s 𝐵 )
21	18 20	bitrdi	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 ↔ ( ( 𝐴 +s 𝐵 ) /su 2s ) <s 𝐵 ) )