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 
|- ( E. p e. NN_s E. q e. NN_s A = ( B F ( ( 1s /su p ) x.s ( 1s /su q ) ) ) <-> E. n e. NN_s A = ( B F ( 1s /su n ) ) )

Proof

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