Metamath Proof Explorer

Theorem avgslt1d

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

Ref Expression
Hypotheses avgs.1 
|- ( ph -> A e. No )
avgs.2 
|- ( ph -> B e. No )
Assertion avgslt1d 
|- ( ph -> ( A  A

Proof

Step Hyp Ref Expression
1 avgs.1 
 |-  ( ph -> A e. No )
2 avgs.2 
 |-  ( ph -> B e. No )
3 1 2 1 sltadd2d 
 |-  ( ph -> ( A  ( A +s A )
4 no2times 
 |-  ( A e. No -> ( 2s x.s A ) = ( A +s A ) )
5 1 4 syl 
 |-  ( ph -> ( 2s x.s A ) = ( A +s A ) )
6 5 breq1d 
 |-  ( ph -> ( ( 2s x.s A )  ( A +s A )
7 3 6 bitr4d 
 |-  ( ph -> ( A  ( 2s x.s A )
8 2sno 
 |-  2s e. No
9 exps1 
 |-  ( 2s e. No -> ( 2s ^su 1s ) = 2s )
10 8 9 ax-mp 
 |-  ( 2s ^su 1s ) = 2s
11 10 oveq1i 
 |-  ( ( 2s ^su 1s ) x.s A ) = ( 2s x.s A )
12 11 breq1i 
 |-  ( ( ( 2s ^su 1s ) x.s A )  ( 2s x.s A )
13 7 12 bitr4di 
 |-  ( ph -> ( A  ( ( 2s ^su 1s ) x.s A )
14 1 2 addscld 
 |-  ( ph -> ( A +s B ) e. No )
15 1n0s 
 |-  1s e. NN0_s
16 15 a1i 
 |-  ( ph -> 1s e. NN0_s )
17 1 14 16 pw2sltmuldiv2d 
 |-  ( ph -> ( ( ( 2s ^su 1s ) x.s A )  A
18 10 oveq2i 
 |-  ( ( A +s B ) /su ( 2s ^su 1s ) ) = ( ( A +s B ) /su 2s )
19 18 breq2i 
 |-  ( A  A
20 17 19 bitrdi 
 |-  ( ph -> ( ( ( 2s ^su 1s ) x.s A )  A
21 13 20 bitrd 
 |-  ( ph -> ( A  A