Theorem remulscllem1

Description: Lemma for remulscl . Split a product of reciprocals of naturals. (Contributed by Scott Fenton, 16-Apr-2025)

	Ref	Expression
Assertion	remulscllem1	⊢ ( ∃ 𝑝 ∈ ℕs ∃ 𝑞 ∈ ℕs 𝐴 = ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) ↔ ∃ 𝑛 ∈ ℕs 𝐴 = ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑛 = ( 𝑝 ·s 𝑞 ) → ( 1s /su 𝑛 ) = ( 1s /su ( 𝑝 ·s 𝑞 ) ) )
2	1	oveq2d	⊢ ( 𝑛 = ( 𝑝 ·s 𝑞 ) → ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) = ( 𝐵 𝐹 ( 1s /su ( 𝑝 ·s 𝑞 ) ) ) )
3	2	eqeq2d	⊢ ( 𝑛 = ( 𝑝 ·s 𝑞 ) → ( ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) = ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) ↔ ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) = ( 𝐵 𝐹 ( 1s /su ( 𝑝 ·s 𝑞 ) ) ) ) )
4		nnmulscl	⊢ ( ( 𝑝 ∈ ℕs ∧ 𝑞 ∈ ℕs ) → ( 𝑝 ·s 𝑞 ) ∈ ℕs )
5		1sno	⊢ 1s ∈ No
6	5	a1i	⊢ ( ( 𝑝 ∈ ℕs ∧ 𝑞 ∈ ℕs ) → 1s ∈ No )
7		nnsno	⊢ ( 𝑝 ∈ ℕs → 𝑝 ∈ No )
8	7	adantr	⊢ ( ( 𝑝 ∈ ℕs ∧ 𝑞 ∈ ℕs ) → 𝑝 ∈ No )
9		nnsno	⊢ ( 𝑞 ∈ ℕs → 𝑞 ∈ No )
10	9	adantl	⊢ ( ( 𝑝 ∈ ℕs ∧ 𝑞 ∈ ℕs ) → 𝑞 ∈ No )
11		nnne0s	⊢ ( 𝑝 ∈ ℕs → 𝑝 ≠ 0s )
12	11	adantr	⊢ ( ( 𝑝 ∈ ℕs ∧ 𝑞 ∈ ℕs ) → 𝑝 ≠ 0s )
13		nnne0s	⊢ ( 𝑞 ∈ ℕs → 𝑞 ≠ 0s )
14	13	adantl	⊢ ( ( 𝑝 ∈ ℕs ∧ 𝑞 ∈ ℕs ) → 𝑞 ≠ 0s )
15	6 8 6 10 12 14	divmuldivsd	⊢ ( ( 𝑝 ∈ ℕs ∧ 𝑞 ∈ ℕs ) → ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) = ( ( 1s ·s 1s ) /su ( 𝑝 ·s 𝑞 ) ) )
16		mulsrid	⊢ ( 1s ∈ No → ( 1s ·s 1s ) = 1s )
17	5 16	ax-mp	⊢ ( 1s ·s 1s ) = 1s
18	17	oveq1i	⊢ ( ( 1s ·s 1s ) /su ( 𝑝 ·s 𝑞 ) ) = ( 1s /su ( 𝑝 ·s 𝑞 ) )
19	15 18	eqtrdi	⊢ ( ( 𝑝 ∈ ℕs ∧ 𝑞 ∈ ℕs ) → ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) = ( 1s /su ( 𝑝 ·s 𝑞 ) ) )
20	19	oveq2d	⊢ ( ( 𝑝 ∈ ℕs ∧ 𝑞 ∈ ℕs ) → ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) = ( 𝐵 𝐹 ( 1s /su ( 𝑝 ·s 𝑞 ) ) ) )
21	3 4 20	rspcedvdw	⊢ ( ( 𝑝 ∈ ℕs ∧ 𝑞 ∈ ℕs ) → ∃ 𝑛 ∈ ℕs ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) = ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) )
22		eqeq1	⊢ ( 𝐴 = ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) → ( 𝐴 = ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) ↔ ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) = ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) ) )
23	22	rexbidv	⊢ ( 𝐴 = ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) → ( ∃ 𝑛 ∈ ℕs 𝐴 = ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) ↔ ∃ 𝑛 ∈ ℕs ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) = ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) ) )
24	21 23	syl5ibrcom	⊢ ( ( 𝑝 ∈ ℕs ∧ 𝑞 ∈ ℕs ) → ( 𝐴 = ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) → ∃ 𝑛 ∈ ℕs 𝐴 = ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) ) )
25	24	rexlimivv	⊢ ( ∃ 𝑝 ∈ ℕs ∃ 𝑞 ∈ ℕs 𝐴 = ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) → ∃ 𝑛 ∈ ℕs 𝐴 = ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) )
26	5	a1i	⊢ ( 𝑛 ∈ ℕs → 1s ∈ No )
27		nnsno	⊢ ( 𝑛 ∈ ℕs → 𝑛 ∈ No )
28		nnne0s	⊢ ( 𝑛 ∈ ℕs → 𝑛 ≠ 0s )
29	26 27 28	divscld	⊢ ( 𝑛 ∈ ℕs → ( 1s /su 𝑛 ) ∈ No )
30	29	mulsridd	⊢ ( 𝑛 ∈ ℕs → ( ( 1s /su 𝑛 ) ·s 1s ) = ( 1s /su 𝑛 ) )
31	30	eqcomd	⊢ ( 𝑛 ∈ ℕs → ( 1s /su 𝑛 ) = ( ( 1s /su 𝑛 ) ·s 1s ) )
32	31	oveq2d	⊢ ( 𝑛 ∈ ℕs → ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) = ( 𝐵 𝐹 ( ( 1s /su 𝑛 ) ·s 1s ) ) )
33		1nns	⊢ 1s ∈ ℕs
34		oveq2	⊢ ( 𝑝 = 𝑛 → ( 1s /su 𝑝 ) = ( 1s /su 𝑛 ) )
35	34	oveq1d	⊢ ( 𝑝 = 𝑛 → ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) = ( ( 1s /su 𝑛 ) ·s ( 1s /su 𝑞 ) ) )
36	35	oveq2d	⊢ ( 𝑝 = 𝑛 → ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) = ( 𝐵 𝐹 ( ( 1s /su 𝑛 ) ·s ( 1s /su 𝑞 ) ) ) )
37	36	eqeq2d	⊢ ( 𝑝 = 𝑛 → ( ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) = ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) ↔ ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) = ( 𝐵 𝐹 ( ( 1s /su 𝑛 ) ·s ( 1s /su 𝑞 ) ) ) ) )
38		oveq2	⊢ ( 𝑞 = 1s → ( 1s /su 𝑞 ) = ( 1s /su 1s ) )
39		divs1	⊢ ( 1s ∈ No → ( 1s /su 1s ) = 1s )
40	5 39	ax-mp	⊢ ( 1s /su 1s ) = 1s
41	38 40	eqtrdi	⊢ ( 𝑞 = 1s → ( 1s /su 𝑞 ) = 1s )
42	41	oveq2d	⊢ ( 𝑞 = 1s → ( ( 1s /su 𝑛 ) ·s ( 1s /su 𝑞 ) ) = ( ( 1s /su 𝑛 ) ·s 1s ) )
43	42	oveq2d	⊢ ( 𝑞 = 1s → ( 𝐵 𝐹 ( ( 1s /su 𝑛 ) ·s ( 1s /su 𝑞 ) ) ) = ( 𝐵 𝐹 ( ( 1s /su 𝑛 ) ·s 1s ) ) )
44	43	eqeq2d	⊢ ( 𝑞 = 1s → ( ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) = ( 𝐵 𝐹 ( ( 1s /su 𝑛 ) ·s ( 1s /su 𝑞 ) ) ) ↔ ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) = ( 𝐵 𝐹 ( ( 1s /su 𝑛 ) ·s 1s ) ) ) )
45	37 44	rspc2ev	⊢ ( ( 𝑛 ∈ ℕs ∧ 1s ∈ ℕs ∧ ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) = ( 𝐵 𝐹 ( ( 1s /su 𝑛 ) ·s 1s ) ) ) → ∃ 𝑝 ∈ ℕs ∃ 𝑞 ∈ ℕs ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) = ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) )
46	33 45	mp3an2	⊢ ( ( 𝑛 ∈ ℕs ∧ ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) = ( 𝐵 𝐹 ( ( 1s /su 𝑛 ) ·s 1s ) ) ) → ∃ 𝑝 ∈ ℕs ∃ 𝑞 ∈ ℕs ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) = ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) )
47	32 46	mpdan	⊢ ( 𝑛 ∈ ℕs → ∃ 𝑝 ∈ ℕs ∃ 𝑞 ∈ ℕs ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) = ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) )
48		eqeq1	⊢ ( 𝐴 = ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) → ( 𝐴 = ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) ↔ ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) = ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) ) )
49	48	2rexbidv	⊢ ( 𝐴 = ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) → ( ∃ 𝑝 ∈ ℕs ∃ 𝑞 ∈ ℕs 𝐴 = ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) ↔ ∃ 𝑝 ∈ ℕs ∃ 𝑞 ∈ ℕs ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) = ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) ) )
50	47 49	syl5ibrcom	⊢ ( 𝑛 ∈ ℕs → ( 𝐴 = ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) → ∃ 𝑝 ∈ ℕs ∃ 𝑞 ∈ ℕs 𝐴 = ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) ) )
51	50	rexlimiv	⊢ ( ∃ 𝑛 ∈ ℕs 𝐴 = ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) → ∃ 𝑝 ∈ ℕs ∃ 𝑞 ∈ ℕs 𝐴 = ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) )
52	25 51	impbii	⊢ ( ∃ 𝑝 ∈ ℕs ∃ 𝑞 ∈ ℕs 𝐴 = ( 𝐵 𝐹 ( ( 1s /su 𝑝 ) ·s ( 1s /su 𝑞 ) ) ) ↔ ∃ 𝑛 ∈ ℕs 𝐴 = ( 𝐵 𝐹 ( 1s /su 𝑛 ) ) )