Theorem zs12bdaylem1

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

	Ref	Expression
Hypotheses	zs12bdaylem.1	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
	zs12bdaylem.2	$$⊢\phi \to M\in {\mathbb{N}}_{\mathrm{0s}}$$
	zs12bdaylem.3	$$⊢\phi \to P\in {\mathbb{N}}_{\mathrm{0s}}$$
	zs12bdaylem.4	No typesetting found for |- ( ph -> ( ( 2s x.s M ) +s 1s )
Assertion	zs12bdaylem1	Could not format assertion : No typesetting found for |- ( ph -> ( N +s ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) =/= ( N +s P ) ) with typecode |-

Proof

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