Metamath Proof Explorer


Theorem zs12bdaylem1

Description: Lemma for zs12bday . Prove an inequality for birthday ordering. (Contributed by Scott Fenton, 22-Feb-2026)

Ref Expression
Hypotheses zs12bdaylem.1
|- ( ph -> N e. NN0_s )
zs12bdaylem.2
|- ( ph -> M e. NN0_s )
zs12bdaylem.3
|- ( ph -> P e. NN0_s )
zs12bdaylem.4
|- ( ph -> ( ( 2s x.s M ) +s 1s ) 
Assertion zs12bdaylem1
|- ( ph -> ( N +s ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) =/= ( N +s P ) )

Proof

Step Hyp Ref Expression
1 zs12bdaylem.1
 |-  ( ph -> N e. NN0_s )
2 zs12bdaylem.2
 |-  ( ph -> M e. NN0_s )
3 zs12bdaylem.3
 |-  ( ph -> P e. NN0_s )
4 zs12bdaylem.4
 |-  ( ph -> ( ( 2s x.s M ) +s 1s ) 
5 n0sge0
 |-  ( M e. NN0_s -> 0s <_s M )
6 2 5 syl
 |-  ( ph -> 0s <_s M )
7 0sno
 |-  0s e. No
8 7 a1i
 |-  ( ph -> 0s e. No )
9 2 n0snod
 |-  ( ph -> M e. No )
10 2sno
 |-  2s e. No
11 10 a1i
 |-  ( ph -> 2s e. No )
12 2nns
 |-  2s e. NN_s
13 nnsgt0
 |-  ( 2s e. NN_s -> 0s 
14 12 13 mp1i
 |-  ( ph -> 0s 
15 8 9 11 14 slemul2d
 |-  ( ph -> ( 0s <_s M <-> ( 2s x.s 0s ) <_s ( 2s x.s M ) ) )
16 muls01
 |-  ( 2s e. No -> ( 2s x.s 0s ) = 0s )
17 10 16 ax-mp
 |-  ( 2s x.s 0s ) = 0s
18 17 breq1i
 |-  ( ( 2s x.s 0s ) <_s ( 2s x.s M ) <-> 0s <_s ( 2s x.s M ) )
19 15 18 bitrdi
 |-  ( ph -> ( 0s <_s M <-> 0s <_s ( 2s x.s M ) ) )
20 11 9 mulscld
 |-  ( ph -> ( 2s x.s M ) e. No )
21 1sno
 |-  1s e. No
22 21 a1i
 |-  ( ph -> 1s e. No )
23 8 20 22 sleadd1d
 |-  ( ph -> ( 0s <_s ( 2s x.s M ) <-> ( 0s +s 1s ) <_s ( ( 2s x.s M ) +s 1s ) ) )
24 19 23 bitrd
 |-  ( ph -> ( 0s <_s M <-> ( 0s +s 1s ) <_s ( ( 2s x.s M ) +s 1s ) ) )
25 addslid
 |-  ( 1s e. No -> ( 0s +s 1s ) = 1s )
26 21 25 ax-mp
 |-  ( 0s +s 1s ) = 1s
27 26 breq1i
 |-  ( ( 0s +s 1s ) <_s ( ( 2s x.s M ) +s 1s ) <-> 1s <_s ( ( 2s x.s M ) +s 1s ) )
28 24 27 bitrdi
 |-  ( ph -> ( 0s <_s M <-> 1s <_s ( ( 2s x.s M ) +s 1s ) ) )
29 6 28 mpbid
 |-  ( ph -> 1s <_s ( ( 2s x.s M ) +s 1s ) )
30 20 22 addscld
 |-  ( ph -> ( ( 2s x.s M ) +s 1s ) e. No )
31 slenlt
 |-  ( ( 1s e. No /\ ( ( 2s x.s M ) +s 1s ) e. No ) -> ( 1s <_s ( ( 2s x.s M ) +s 1s ) <-> -. ( ( 2s x.s M ) +s 1s ) 
32 21 30 31 sylancr
 |-  ( ph -> ( 1s <_s ( ( 2s x.s M ) +s 1s ) <-> -. ( ( 2s x.s M ) +s 1s ) 
33 29 32 mpbid
 |-  ( ph -> -. ( ( 2s x.s M ) +s 1s ) 
34 4 adantr
 |-  ( ( ph /\ P = 0s ) -> ( ( 2s x.s M ) +s 1s ) 
35 oveq2
 |-  ( P = 0s -> ( 2s ^su P ) = ( 2s ^su 0s ) )
36 exps0
 |-  ( 2s e. No -> ( 2s ^su 0s ) = 1s )
37 10 36 ax-mp
 |-  ( 2s ^su 0s ) = 1s
38 35 37 eqtrdi
 |-  ( P = 0s -> ( 2s ^su P ) = 1s )
39 38 breq2d
 |-  ( P = 0s -> ( ( ( 2s x.s M ) +s 1s )  ( ( 2s x.s M ) +s 1s ) 
40 39 adantl
 |-  ( ( ph /\ P = 0s ) -> ( ( ( 2s x.s M ) +s 1s )  ( ( 2s x.s M ) +s 1s ) 
41 34 40 mpbid
 |-  ( ( ph /\ P = 0s ) -> ( ( 2s x.s M ) +s 1s ) 
42 33 41 mtand
 |-  ( ph -> -. P = 0s )
43 30 3 pw2divscld
 |-  ( ph -> ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) e. No )
44 3 n0snod
 |-  ( ph -> P e. No )
45 1 n0snod
 |-  ( ph -> N e. No )
46 43 44 45 addscan1d
 |-  ( ph -> ( ( N +s ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) = ( N +s P ) <-> ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) = P ) )
47 30 44 3 pw2divsmuld
 |-  ( ph -> ( ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) = P <-> ( ( 2s ^su P ) x.s P ) = ( ( 2s x.s M ) +s 1s ) ) )
48 breq1
 |-  ( ( ( 2s ^su P ) x.s P ) = ( ( 2s x.s M ) +s 1s ) -> ( ( ( 2s ^su P ) x.s P )  ( ( 2s x.s M ) +s 1s ) 
49 48 biimpar
 |-  ( ( ( ( 2s ^su P ) x.s P ) = ( ( 2s x.s M ) +s 1s ) /\ ( ( 2s x.s M ) +s 1s )  ( ( 2s ^su P ) x.s P ) 
50 nnexpscl
 |-  ( ( 2s e. NN_s /\ P e. NN0_s ) -> ( 2s ^su P ) e. NN_s )
51 12 3 50 sylancr
 |-  ( ph -> ( 2s ^su P ) e. NN_s )
52 51 nnsnod
 |-  ( ph -> ( 2s ^su P ) e. No )
53 nnsgt0
 |-  ( ( 2s ^su P ) e. NN_s -> 0s 
54 51 53 syl
 |-  ( ph -> 0s 
55 44 22 52 54 sltmul2d
 |-  ( ph -> ( P  ( ( 2s ^su P ) x.s P ) 
56 52 mulsridd
 |-  ( ph -> ( ( 2s ^su P ) x.s 1s ) = ( 2s ^su P ) )
57 56 breq2d
 |-  ( ph -> ( ( ( 2s ^su P ) x.s P )  ( ( 2s ^su P ) x.s P ) 
58 55 57 bitrd
 |-  ( ph -> ( P  ( ( 2s ^su P ) x.s P ) 
59 n0sge0
 |-  ( P e. NN0_s -> 0s <_s P )
60 3 59 syl
 |-  ( ph -> 0s <_s P )
61 sletri3
 |-  ( ( P e. No /\ 0s e. No ) -> ( P = 0s <-> ( P <_s 0s /\ 0s <_s P ) ) )
62 44 7 61 sylancl
 |-  ( ph -> ( P = 0s <-> ( P <_s 0s /\ 0s <_s P ) ) )
63 60 62 mpbiran2d
 |-  ( ph -> ( P = 0s <-> P <_s 0s ) )
64 0n0s
 |-  0s e. NN0_s
65 n0sleltp1
 |-  ( ( P e. NN0_s /\ 0s e. NN0_s ) -> ( P <_s 0s <-> P 
66 3 64 65 sylancl
 |-  ( ph -> ( P <_s 0s <-> P 
67 26 breq2i
 |-  ( P  P 
68 66 67 bitrdi
 |-  ( ph -> ( P <_s 0s <-> P 
69 63 68 bitr2d
 |-  ( ph -> ( P  P = 0s ) )
70 69 biimpd
 |-  ( ph -> ( P  P = 0s ) )
71 58 70 sylbird
 |-  ( ph -> ( ( ( 2s ^su P ) x.s P )  P = 0s ) )
72 49 71 syl5
 |-  ( ph -> ( ( ( ( 2s ^su P ) x.s P ) = ( ( 2s x.s M ) +s 1s ) /\ ( ( 2s x.s M ) +s 1s )  P = 0s ) )
73 4 72 mpan2d
 |-  ( ph -> ( ( ( 2s ^su P ) x.s P ) = ( ( 2s x.s M ) +s 1s ) -> P = 0s ) )
74 47 73 sylbid
 |-  ( ph -> ( ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) = P -> P = 0s ) )
75 46 74 sylbid
 |-  ( ph -> ( ( N +s ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) = ( N +s P ) -> P = 0s ) )
76 42 75 mtod
 |-  ( ph -> -. ( N +s ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) = ( N +s P ) )
77 76 neqned
 |-  ( ph -> ( N +s ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) =/= ( N +s P ) )