Theorem avgslt2d

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

	Ref	Expression
Hypotheses	avgs.1	$$⊢\phi \to A\in \mathrm{No}$$
	avgs.2	$$⊢\phi \to B\in \mathrm{No}$$
Assertion	avgslt2d	Could not format assertion : No typesetting found for |- ( ph -> ( A ( ( A +s B ) /su 2s )

Proof

Step	Hyp	Ref	Expression
1		avgs.1	$$⊢\phi \to A\in \mathrm{No}$$
2		avgs.2	$$⊢\phi \to B\in \mathrm{No}$$
3	1 2 2	sltadd1d	$$⊢\phi \to \left(A{<}_{s}B\leftrightarrow \left(A{+}_{s}B\right){<}_s\left(B{+}_{s}B\right)\right)$$
4		no2times	Could not format ( B e. No -> ( 2s x.s B ) = ( B +s B ) ) : No typesetting found for |- ( B e. No -> ( 2s x.s B ) = ( B +s B ) ) with typecode |-
5	2 4	syl	Could not format ( ph -> ( 2s x.s B ) = ( B +s B ) ) : No typesetting found for |- ( ph -> ( 2s x.s B ) = ( B +s B ) ) with typecode |-
6	5	breq2d	Could not format ( ph -> ( ( A +s B ) ( A +s B ) ( ( A +s B ) ( A +s B )
7	3 6	bitr4d	Could not format ( ph -> ( A ( A +s B ) ( A ( A +s B )
8		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
9		exps1	Could not format ( 2s e. No -> ( 2s ^su 1s ) = 2s ) : No typesetting found for |- ( 2s e. No -> ( 2s ^su 1s ) = 2s ) with typecode |-
10	8 9	ax-mp	Could not format ( 2s ^su 1s ) = 2s : No typesetting found for |- ( 2s ^su 1s ) = 2s with typecode |-
11	10	oveq1i	Could not format ( ( 2s ^su 1s ) x.s B ) = ( 2s x.s B ) : No typesetting found for |- ( ( 2s ^su 1s ) x.s B ) = ( 2s x.s B ) with typecode |-
12	11	breq2i	Could not format ( ( A +s B ) ( A +s B ) ( A +s B )
13	7 12	bitr4di	Could not format ( ph -> ( A ( A +s B ) ( A ( A +s B )
14	1 2	addscld	$$⊢\phi \to A{+}_{s}B\in \mathrm{No}$$
15		1n0s	$$⊢1_s\in {\mathbb{N}}_{\mathrm{0s}}$$
16	15	a1i	$$⊢\phi \to 1_s\in {\mathbb{N}}_{\mathrm{0s}}$$
17	14 2 16	pw2sltdivmuld	Could not format ( ph -> ( ( ( A +s B ) /su ( 2s ^su 1s ) ) ( A +s B ) ( ( ( A +s B ) /su ( 2s ^su 1s ) ) ( A +s B )
18	13 17	bitr4d	Could not format ( ph -> ( A ( ( A +s B ) /su ( 2s ^su 1s ) ) ( A ( ( A +s B ) /su ( 2s ^su 1s ) )
19	10	oveq2i	Could not format ( ( A +s B ) /su ( 2s ^su 1s ) ) = ( ( A +s B ) /su 2s ) : No typesetting found for |- ( ( A +s B ) /su ( 2s ^su 1s ) ) = ( ( A +s B ) /su 2s ) with typecode |-
20	19	breq1i	Could not format ( ( ( A +s B ) /su ( 2s ^su 1s ) ) ( ( A +s B ) /su 2s ) ( ( A +s B ) /su 2s )
21	18 20	bitrdi	Could not format ( ph -> ( A ( ( A +s B ) /su 2s ) ( A ( ( A +s B ) /su 2s )