Metamath Proof Explorer

Theorem remulscllem1

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

Ref Expression
Assertion remulscllem1 ⊢ ∃ p ∈ ℕ s ∃ q ∈ ℕ s A = B F 1 s / su p ⋅ s 1 s / su q ↔ ∃ n ∈ ℕ s A = B F 1 s / su n

Proof

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