Theorem z12bdaylem1

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

	Ref	Expression
Hypotheses	z12bdaylem.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
	z12bdaylem.2	⊢ ( 𝜑 → 𝑀 ∈ ℕ0s )
	z12bdaylem.3	⊢ ( 𝜑 → 𝑃 ∈ ℕ0s )
	z12bdaylem.4	⊢ ( 𝜑 → ( ( 2s ·s 𝑀 ) +s 1s ) <s ( 2s ↑s 𝑃 ) )
Assertion	z12bdaylem1	⊢ ( 𝜑 → ( 𝑁 +s ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) ≠ ( 𝑁 +s 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		z12bdaylem.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
2		z12bdaylem.2	⊢ ( 𝜑 → 𝑀 ∈ ℕ0s )
3		z12bdaylem.3	⊢ ( 𝜑 → 𝑃 ∈ ℕ0s )
4		z12bdaylem.4	⊢ ( 𝜑 → ( ( 2s ·s 𝑀 ) +s 1s ) <s ( 2s ↑s 𝑃 ) )
5		n0sge0	⊢ ( 𝑀 ∈ ℕ0s → 0s ≤s 𝑀 )
6	2 5	syl	⊢ ( 𝜑 → 0s ≤s 𝑀 )
7		0no	⊢ 0s ∈ No
8	7	a1i	⊢ ( 𝜑 → 0s ∈ No )
9	2	n0nod	⊢ ( 𝜑 → 𝑀 ∈ No )
10		2no	⊢ 2s ∈ No
11	10	a1i	⊢ ( 𝜑 → 2s ∈ No )
12		2nns	⊢ 2s ∈ ℕs
13		nnsgt0	⊢ ( 2s ∈ ℕs → 0s <s 2s )
14	12 13	mp1i	⊢ ( 𝜑 → 0s <s 2s )
15	8 9 11 14	lemuls2d	⊢ ( 𝜑 → ( 0s ≤s 𝑀 ↔ ( 2s ·s 0s ) ≤s ( 2s ·s 𝑀 ) ) )
16		muls01	⊢ ( 2s ∈ No → ( 2s ·s 0s ) = 0s )
17	10 16	ax-mp	⊢ ( 2s ·s 0s ) = 0s
18	17	breq1i	⊢ ( ( 2s ·s 0s ) ≤s ( 2s ·s 𝑀 ) ↔ 0s ≤s ( 2s ·s 𝑀 ) )
19	15 18	bitrdi	⊢ ( 𝜑 → ( 0s ≤s 𝑀 ↔ 0s ≤s ( 2s ·s 𝑀 ) ) )
20	11 9	mulscld	⊢ ( 𝜑 → ( 2s ·s 𝑀 ) ∈ No )
21		1no	⊢ 1s ∈ No
22	21	a1i	⊢ ( 𝜑 → 1s ∈ No )
23	8 20 22	leadds1d	⊢ ( 𝜑 → ( 0s ≤s ( 2s ·s 𝑀 ) ↔ ( 0s +s 1s ) ≤s ( ( 2s ·s 𝑀 ) +s 1s ) ) )
24	19 23	bitrd	⊢ ( 𝜑 → ( 0s ≤s 𝑀 ↔ ( 0s +s 1s ) ≤s ( ( 2s ·s 𝑀 ) +s 1s ) ) )
25		addslid	⊢ ( 1s ∈ No → ( 0s +s 1s ) = 1s )
26	21 25	ax-mp	⊢ ( 0s +s 1s ) = 1s
27	26	breq1i	⊢ ( ( 0s +s 1s ) ≤s ( ( 2s ·s 𝑀 ) +s 1s ) ↔ 1s ≤s ( ( 2s ·s 𝑀 ) +s 1s ) )
28	24 27	bitrdi	⊢ ( 𝜑 → ( 0s ≤s 𝑀 ↔ 1s ≤s ( ( 2s ·s 𝑀 ) +s 1s ) ) )
29	6 28	mpbid	⊢ ( 𝜑 → 1s ≤s ( ( 2s ·s 𝑀 ) +s 1s ) )
30	20 22	addscld	⊢ ( 𝜑 → ( ( 2s ·s 𝑀 ) +s 1s ) ∈ No )
31		lenlts	⊢ ( ( 1s ∈ No ∧ ( ( 2s ·s 𝑀 ) +s 1s ) ∈ No ) → ( 1s ≤s ( ( 2s ·s 𝑀 ) +s 1s ) ↔ ¬ ( ( 2s ·s 𝑀 ) +s 1s ) <s 1s ) )
32	21 30 31	sylancr	⊢ ( 𝜑 → ( 1s ≤s ( ( 2s ·s 𝑀 ) +s 1s ) ↔ ¬ ( ( 2s ·s 𝑀 ) +s 1s ) <s 1s ) )
33	29 32	mpbid	⊢ ( 𝜑 → ¬ ( ( 2s ·s 𝑀 ) +s 1s ) <s 1s )
34	4	adantr	⊢ ( ( 𝜑 ∧ 𝑃 = 0s ) → ( ( 2s ·s 𝑀 ) +s 1s ) <s ( 2s ↑s 𝑃 ) )
35		oveq2	⊢ ( 𝑃 = 0s → ( 2s ↑s 𝑃 ) = ( 2s ↑s 0s ) )
36		exps0	⊢ ( 2s ∈ No → ( 2s ↑s 0s ) = 1s )
37	10 36	ax-mp	⊢ ( 2s ↑s 0s ) = 1s
38	35 37	eqtrdi	⊢ ( 𝑃 = 0s → ( 2s ↑s 𝑃 ) = 1s )
39	38	breq2d	⊢ ( 𝑃 = 0s → ( ( ( 2s ·s 𝑀 ) +s 1s ) <s ( 2s ↑s 𝑃 ) ↔ ( ( 2s ·s 𝑀 ) +s 1s ) <s 1s ) )
40	39	adantl	⊢ ( ( 𝜑 ∧ 𝑃 = 0s ) → ( ( ( 2s ·s 𝑀 ) +s 1s ) <s ( 2s ↑s 𝑃 ) ↔ ( ( 2s ·s 𝑀 ) +s 1s ) <s 1s ) )
41	34 40	mpbid	⊢ ( ( 𝜑 ∧ 𝑃 = 0s ) → ( ( 2s ·s 𝑀 ) +s 1s ) <s 1s )
42	33 41	mtand	⊢ ( 𝜑 → ¬ 𝑃 = 0s )
43	30 3	pw2divscld	⊢ ( 𝜑 → ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ∈ No )
44	3	n0nod	⊢ ( 𝜑 → 𝑃 ∈ No )
45	1	n0nod	⊢ ( 𝜑 → 𝑁 ∈ No )
46	43 44 45	addscan1d	⊢ ( 𝜑 → ( ( 𝑁 +s ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) = ( 𝑁 +s 𝑃 ) ↔ ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) = 𝑃 ) )
47	30 44 3	pw2divmulsd	⊢ ( 𝜑 → ( ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) = 𝑃 ↔ ( ( 2s ↑s 𝑃 ) ·s 𝑃 ) = ( ( 2s ·s 𝑀 ) +s 1s ) ) )
48		breq1	⊢ ( ( ( 2s ↑s 𝑃 ) ·s 𝑃 ) = ( ( 2s ·s 𝑀 ) +s 1s ) → ( ( ( 2s ↑s 𝑃 ) ·s 𝑃 ) <s ( 2s ↑s 𝑃 ) ↔ ( ( 2s ·s 𝑀 ) +s 1s ) <s ( 2s ↑s 𝑃 ) ) )
49	48	biimpar	⊢ ( ( ( ( 2s ↑s 𝑃 ) ·s 𝑃 ) = ( ( 2s ·s 𝑀 ) +s 1s ) ∧ ( ( 2s ·s 𝑀 ) +s 1s ) <s ( 2s ↑s 𝑃 ) ) → ( ( 2s ↑s 𝑃 ) ·s 𝑃 ) <s ( 2s ↑s 𝑃 ) )
50		nnexpscl	⊢ ( ( 2s ∈ ℕs ∧ 𝑃 ∈ ℕ0s ) → ( 2s ↑s 𝑃 ) ∈ ℕs )
51	12 3 50	sylancr	⊢ ( 𝜑 → ( 2s ↑s 𝑃 ) ∈ ℕs )
52	51	nnnod	⊢ ( 𝜑 → ( 2s ↑s 𝑃 ) ∈ No )
53		nnsgt0	⊢ ( ( 2s ↑s 𝑃 ) ∈ ℕs → 0s <s ( 2s ↑s 𝑃 ) )
54	51 53	syl	⊢ ( 𝜑 → 0s <s ( 2s ↑s 𝑃 ) )
55	44 22 52 54	ltmuls2d	⊢ ( 𝜑 → ( 𝑃 <s 1s ↔ ( ( 2s ↑s 𝑃 ) ·s 𝑃 ) <s ( ( 2s ↑s 𝑃 ) ·s 1s ) ) )
56	52	mulsridd	⊢ ( 𝜑 → ( ( 2s ↑s 𝑃 ) ·s 1s ) = ( 2s ↑s 𝑃 ) )
57	56	breq2d	⊢ ( 𝜑 → ( ( ( 2s ↑s 𝑃 ) ·s 𝑃 ) <s ( ( 2s ↑s 𝑃 ) ·s 1s ) ↔ ( ( 2s ↑s 𝑃 ) ·s 𝑃 ) <s ( 2s ↑s 𝑃 ) ) )
58	55 57	bitrd	⊢ ( 𝜑 → ( 𝑃 <s 1s ↔ ( ( 2s ↑s 𝑃 ) ·s 𝑃 ) <s ( 2s ↑s 𝑃 ) ) )
59		n0sge0	⊢ ( 𝑃 ∈ ℕ0s → 0s ≤s 𝑃 )
60	3 59	syl	⊢ ( 𝜑 → 0s ≤s 𝑃 )
61		lestri3	⊢ ( ( 𝑃 ∈ No ∧ 0s ∈ No ) → ( 𝑃 = 0s ↔ ( 𝑃 ≤s 0s ∧ 0s ≤s 𝑃 ) ) )
62	44 7 61	sylancl	⊢ ( 𝜑 → ( 𝑃 = 0s ↔ ( 𝑃 ≤s 0s ∧ 0s ≤s 𝑃 ) ) )
63	60 62	mpbiran2d	⊢ ( 𝜑 → ( 𝑃 = 0s ↔ 𝑃 ≤s 0s ) )
64		0n0s	⊢ 0s ∈ ℕ0s
65		n0lesltp1	⊢ ( ( 𝑃 ∈ ℕ0s ∧ 0s ∈ ℕ0s ) → ( 𝑃 ≤s 0s ↔ 𝑃 <s ( 0s +s 1s ) ) )
66	3 64 65	sylancl	⊢ ( 𝜑 → ( 𝑃 ≤s 0s ↔ 𝑃 <s ( 0s +s 1s ) ) )
67	26	breq2i	⊢ ( 𝑃 <s ( 0s +s 1s ) ↔ 𝑃 <s 1s )
68	66 67	bitrdi	⊢ ( 𝜑 → ( 𝑃 ≤s 0s ↔ 𝑃 <s 1s ) )
69	63 68	bitr2d	⊢ ( 𝜑 → ( 𝑃 <s 1s ↔ 𝑃 = 0s ) )
70	69	biimpd	⊢ ( 𝜑 → ( 𝑃 <s 1s → 𝑃 = 0s ) )
71	58 70	sylbird	⊢ ( 𝜑 → ( ( ( 2s ↑s 𝑃 ) ·s 𝑃 ) <s ( 2s ↑s 𝑃 ) → 𝑃 = 0s ) )
72	49 71	syl5	⊢ ( 𝜑 → ( ( ( ( 2s ↑s 𝑃 ) ·s 𝑃 ) = ( ( 2s ·s 𝑀 ) +s 1s ) ∧ ( ( 2s ·s 𝑀 ) +s 1s ) <s ( 2s ↑s 𝑃 ) ) → 𝑃 = 0s ) )
73	4 72	mpan2d	⊢ ( 𝜑 → ( ( ( 2s ↑s 𝑃 ) ·s 𝑃 ) = ( ( 2s ·s 𝑀 ) +s 1s ) → 𝑃 = 0s ) )
74	47 73	sylbid	⊢ ( 𝜑 → ( ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) = 𝑃 → 𝑃 = 0s ) )
75	46 74	sylbid	⊢ ( 𝜑 → ( ( 𝑁 +s ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) = ( 𝑁 +s 𝑃 ) → 𝑃 = 0s ) )
76	42 75	mtod	⊢ ( 𝜑 → ¬ ( 𝑁 +s ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) = ( 𝑁 +s 𝑃 ) )
77	76	neqned	⊢ ( 𝜑 → ( 𝑁 +s ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) ≠ ( 𝑁 +s 𝑃 ) )