Theorem avgslt1d

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	avgslt1d	Could not format assertion : No typesetting found for |- ( ph -> ( A A

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 1	sltadd2d	$$⊢\phi \to \left(A{<}_{s}B\leftrightarrow \left(A{+}_{s}A\right){<}_s\left(A{+}_{s}B\right)\right)$$
4		no2times	Could not format ( A e. No -> ( 2s x.s A ) = ( A +s A ) ) : No typesetting found for |- ( A e. No -> ( 2s x.s A ) = ( A +s A ) ) with typecode |-
5	1 4	syl	Could not format ( ph -> ( 2s x.s A ) = ( A +s A ) ) : No typesetting found for |- ( ph -> ( 2s x.s A ) = ( A +s A ) ) with typecode |-
6	5	breq1d	Could not format ( ph -> ( ( 2s x.s A ) ( A +s A ) ( ( 2s x.s A ) ( A +s A )
7	3 6	bitr4d	Could not format ( ph -> ( A ( 2s x.s A ) ( A ( 2s x.s A )
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 A ) = ( 2s x.s A ) : No typesetting found for |- ( ( 2s ^su 1s ) x.s A ) = ( 2s x.s A ) with typecode |-
12	11	breq1i	Could not format ( ( ( 2s ^su 1s ) x.s A ) ( 2s x.s A ) ( 2s x.s A )
13	7 12	bitr4di	Could not format ( ph -> ( A ( ( 2s ^su 1s ) x.s A ) ( A ( ( 2s ^su 1s ) x.s A )
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	1 14 16	pw2sltmuldiv2d	Could not format ( ph -> ( ( ( 2s ^su 1s ) x.s A ) A ( ( ( 2s ^su 1s ) x.s A ) A
18	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 |-
19	18	breq2i	Could not format ( A A A
20	17 19	bitrdi	Could not format ( ph -> ( ( ( 2s ^su 1s ) x.s A ) A ( ( ( 2s ^su 1s ) x.s A ) A
21	13 20	bitrd	Could not format ( ph -> ( A A ( A A