Theorem mulcutlem

Description: Lemma for mulcut . State the theorem with extra DV conditions. (Contributed by Scott Fenton, 7-Mar-2025)

	Ref	Expression
Hypotheses	mulcutlem.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	mulcutlem.2	⊢ ( 𝜑 → 𝐵 ∈ No )
Assertion	mulcutlem	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) <<s { ( 𝐴 ·s 𝐵 ) } ∧ { ( 𝐴 ·s 𝐵 ) } <<s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulcutlem.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		mulcutlem.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		mulsprop	⊢ ( ( ( 𝑒 ∈ No ∧ 𝑓 ∈ No ) ∧ ( 𝑔 ∈ No ∧ ℎ ∈ No ) ∧ ( 𝑖 ∈ No ∧ 𝑗 ∈ No ) ) → ( ( 𝑒 ·s 𝑓 ) ∈ No ∧ ( ( 𝑔 <s ℎ ∧ 𝑖 <s 𝑗 ) → ( ( 𝑔 ·s 𝑗 ) -s ( 𝑔 ·s 𝑖 ) ) <s ( ( ℎ ·s 𝑗 ) -s ( ℎ ·s 𝑖 ) ) ) ) )
4	3	a1d	⊢ ( ( ( 𝑒 ∈ No ∧ 𝑓 ∈ No ) ∧ ( 𝑔 ∈ No ∧ ℎ ∈ No ) ∧ ( 𝑖 ∈ No ∧ 𝑗 ∈ No ) ) → ( ( ( ( bday ‘ 𝑒 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ 𝑖 ) ) ∪ ( ( bday ‘ ℎ ) +no ( bday ‘ 𝑗 ) ) ) ∪ ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ 𝑗 ) ) ∪ ( ( bday ‘ ℎ ) +no ( bday ‘ 𝑖 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ∪ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ) ) → ( ( 𝑒 ·s 𝑓 ) ∈ No ∧ ( ( 𝑔 <s ℎ ∧ 𝑖 <s 𝑗 ) → ( ( 𝑔 ·s 𝑗 ) -s ( 𝑔 ·s 𝑖 ) ) <s ( ( ℎ ·s 𝑗 ) -s ( ℎ ·s 𝑖 ) ) ) ) ) )
5	4	3expa	⊢ ( ( ( ( 𝑒 ∈ No ∧ 𝑓 ∈ No ) ∧ ( 𝑔 ∈ No ∧ ℎ ∈ No ) ) ∧ ( 𝑖 ∈ No ∧ 𝑗 ∈ No ) ) → ( ( ( ( bday ‘ 𝑒 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ 𝑖 ) ) ∪ ( ( bday ‘ ℎ ) +no ( bday ‘ 𝑗 ) ) ) ∪ ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ 𝑗 ) ) ∪ ( ( bday ‘ ℎ ) +no ( bday ‘ 𝑖 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ∪ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ) ) → ( ( 𝑒 ·s 𝑓 ) ∈ No ∧ ( ( 𝑔 <s ℎ ∧ 𝑖 <s 𝑗 ) → ( ( 𝑔 ·s 𝑗 ) -s ( 𝑔 ·s 𝑖 ) ) <s ( ( ℎ ·s 𝑗 ) -s ( ℎ ·s 𝑖 ) ) ) ) ) )
6	5	ralrimivva	⊢ ( ( ( 𝑒 ∈ No ∧ 𝑓 ∈ No ) ∧ ( 𝑔 ∈ No ∧ ℎ ∈ No ) ) → ∀ 𝑖 ∈ No ∀ 𝑗 ∈ No ( ( ( ( bday ‘ 𝑒 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ 𝑖 ) ) ∪ ( ( bday ‘ ℎ ) +no ( bday ‘ 𝑗 ) ) ) ∪ ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ 𝑗 ) ) ∪ ( ( bday ‘ ℎ ) +no ( bday ‘ 𝑖 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ∪ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ) ) → ( ( 𝑒 ·s 𝑓 ) ∈ No ∧ ( ( 𝑔 <s ℎ ∧ 𝑖 <s 𝑗 ) → ( ( 𝑔 ·s 𝑗 ) -s ( 𝑔 ·s 𝑖 ) ) <s ( ( ℎ ·s 𝑗 ) -s ( ℎ ·s 𝑖 ) ) ) ) ) )
7	6	ralrimivva	⊢ ( ( 𝑒 ∈ No ∧ 𝑓 ∈ No ) → ∀ 𝑔 ∈ No ∀ ℎ ∈ No ∀ 𝑖 ∈ No ∀ 𝑗 ∈ No ( ( ( ( bday ‘ 𝑒 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ 𝑖 ) ) ∪ ( ( bday ‘ ℎ ) +no ( bday ‘ 𝑗 ) ) ) ∪ ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ 𝑗 ) ) ∪ ( ( bday ‘ ℎ ) +no ( bday ‘ 𝑖 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ∪ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ) ) → ( ( 𝑒 ·s 𝑓 ) ∈ No ∧ ( ( 𝑔 <s ℎ ∧ 𝑖 <s 𝑗 ) → ( ( 𝑔 ·s 𝑗 ) -s ( 𝑔 ·s 𝑖 ) ) <s ( ( ℎ ·s 𝑗 ) -s ( ℎ ·s 𝑖 ) ) ) ) ) )
8	7	rgen2	⊢ ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ∀ 𝑔 ∈ No ∀ ℎ ∈ No ∀ 𝑖 ∈ No ∀ 𝑗 ∈ No ( ( ( ( bday ‘ 𝑒 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ 𝑖 ) ) ∪ ( ( bday ‘ ℎ ) +no ( bday ‘ 𝑗 ) ) ) ∪ ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ 𝑗 ) ) ∪ ( ( bday ‘ ℎ ) +no ( bday ‘ 𝑖 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ∪ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ) ) → ( ( 𝑒 ·s 𝑓 ) ∈ No ∧ ( ( 𝑔 <s ℎ ∧ 𝑖 <s 𝑗 ) → ( ( 𝑔 ·s 𝑗 ) -s ( 𝑔 ·s 𝑖 ) ) <s ( ( ℎ ·s 𝑗 ) -s ( ℎ ·s 𝑖 ) ) ) ) )
9	8	a1i	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ∀ 𝑔 ∈ No ∀ ℎ ∈ No ∀ 𝑖 ∈ No ∀ 𝑗 ∈ No ( ( ( ( bday ‘ 𝑒 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ 𝑖 ) ) ∪ ( ( bday ‘ ℎ ) +no ( bday ‘ 𝑗 ) ) ) ∪ ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ 𝑗 ) ) ∪ ( ( bday ‘ ℎ ) +no ( bday ‘ 𝑖 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ∪ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ) ) → ( ( 𝑒 ·s 𝑓 ) ∈ No ∧ ( ( 𝑔 <s ℎ ∧ 𝑖 <s 𝑗 ) → ( ( 𝑔 ·s 𝑗 ) -s ( 𝑔 ·s 𝑖 ) ) <s ( ( ℎ ·s 𝑗 ) -s ( ℎ ·s 𝑖 ) ) ) ) ) )
10		simpl	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝐴 ∈ No )
11		simpr	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝐵 ∈ No )
12	9 10 11	mulsproplem10	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) <<s { ( 𝐴 ·s 𝐵 ) } ∧ { ( 𝐴 ·s 𝐵 ) } <<s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) )
13	1 2 12	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) <<s { ( 𝐴 ·s 𝐵 ) } ∧ { ( 𝐴 ·s 𝐵 ) } <<s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) )