Theorem avglts1d

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

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

Proof

Step	Hyp	Ref	Expression
1		avgs.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		avgs.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3	1 2 1	ltadds2d	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 ↔ ( 𝐴 +s 𝐴 ) <s ( 𝐴 +s 𝐵 ) ) )
4		no2times	⊢ ( 𝐴 ∈ No → ( 2s ·s 𝐴 ) = ( 𝐴 +s 𝐴 ) )
5	1 4	syl	⊢ ( 𝜑 → ( 2s ·s 𝐴 ) = ( 𝐴 +s 𝐴 ) )
6	5	breq1d	⊢ ( 𝜑 → ( ( 2s ·s 𝐴 ) <s ( 𝐴 +s 𝐵 ) ↔ ( 𝐴 +s 𝐴 ) <s ( 𝐴 +s 𝐵 ) ) )
7	3 6	bitr4d	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 ↔ ( 2s ·s 𝐴 ) <s ( 𝐴 +s 𝐵 ) ) )
8		2no	⊢ 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	breq1i	⊢ ( ( ( 2s ↑s 1s ) ·s 𝐴 ) <s ( 𝐴 +s 𝐵 ) ↔ ( 2s ·s 𝐴 ) <s ( 𝐴 +s 𝐵 ) )
13	7 12	bitr4di	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 ↔ ( ( 2s ↑s 1s ) ·s 𝐴 ) <s ( 𝐴 +s 𝐵 ) ) )
14	1 2	addscld	⊢ ( 𝜑 → ( 𝐴 +s 𝐵 ) ∈ No )
15		1n0s	⊢ 1s ∈ ℕ0s
16	15	a1i	⊢ ( 𝜑 → 1s ∈ ℕ0s )
17	1 14 16	pw2ltmuldivs2d	⊢ ( 𝜑 → ( ( ( 2s ↑s 1s ) ·s 𝐴 ) <s ( 𝐴 +s 𝐵 ) ↔ 𝐴 <s ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s 1s ) ) ) )
18	10	oveq2i	⊢ ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s 1s ) ) = ( ( 𝐴 +s 𝐵 ) /su 2s )
19	18	breq2i	⊢ ( 𝐴 <s ( ( 𝐴 +s 𝐵 ) /su ( 2s ↑s 1s ) ) ↔ 𝐴 <s ( ( 𝐴 +s 𝐵 ) /su 2s ) )
20	17 19	bitrdi	⊢ ( 𝜑 → ( ( ( 2s ↑s 1s ) ·s 𝐴 ) <s ( 𝐴 +s 𝐵 ) ↔ 𝐴 <s ( ( 𝐴 +s 𝐵 ) /su 2s ) ) )
21	13 20	bitrd	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 ↔ 𝐴 <s ( ( 𝐴 +s 𝐵 ) /su 2s ) ) )