Metamath Proof Explorer

Theorem avgslt2d

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 avgslt2d 
|- ( ph -> ( A  ( ( A +s B ) /su 2s )

Proof

Step Hyp Ref Expression
1 avgs.1 
 |-  ( ph -> A e. No )
2 avgs.2 
 |-  ( ph -> B e. No )
3 1 2 2 sltadd1d 
 |-  ( ph -> ( A  ( A +s B )
4 no2times 
 |-  ( B e. No -> ( 2s x.s B ) = ( B +s B ) )
5 2 4 syl 
 |-  ( ph -> ( 2s x.s B ) = ( B +s B ) )
6 5 breq2d 
 |-  ( ph -> ( ( A +s B )  ( A +s B )
7 3 6 bitr4d 
 |-  ( ph -> ( A  ( A +s B )
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 B ) = ( 2s x.s B )
12 11 breq2i 
 |-  ( ( A +s B )  ( A +s B )
13 7 12 bitr4di 
 |-  ( ph -> ( A  ( A +s B )
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 14 2 16 pw2sltdivmuld 
 |-  ( ph -> ( ( ( A +s B ) /su ( 2s ^su 1s ) )  ( A +s B )
18 13 17 bitr4d 
 |-  ( ph -> ( A  ( ( A +s B ) /su ( 2s ^su 1s ) )
19 10 oveq2i 
 |-  ( ( A +s B ) /su ( 2s ^su 1s ) ) = ( ( A +s B ) /su 2s )
20 19 breq1i 
 |-  ( ( ( A +s B ) /su ( 2s ^su 1s ) )  ( ( A +s B ) /su 2s )
21 18 20 bitrdi 
 |-  ( ph -> ( A  ( ( A +s B ) /su 2s )