Metamath Proof Explorer

Theorem prmreclem1

Description: Lemma for prmrec . Properties of the "square part" function, which extracts the m of the decomposition N = r m ^ 2 , with m maximal and r squarefree. (Contributed by Mario Carneiro, 5-Aug-2014)

Ref Expression
Hypothesis prmreclem1.1 
|- Q = ( n e. NN |-> sup ( { r e. NN | ( r ^ 2 ) || n } , RR , < ) )
Assertion prmreclem1 
|- ( N e. NN -> ( ( Q ` N ) e. NN /\ ( ( Q ` N ) ^ 2 ) || N /\ ( K e. ( ZZ>= ` 2 ) -> -. ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 prmreclem1.1 
 |-  Q = ( n e. NN |-> sup ( { r e. NN | ( r ^ 2 ) || n } , RR , < ) )
2 ssrab2 
 |-  { r e. NN | ( r ^ 2 ) || N } C_ NN
3 breq2 
 |-  ( n = N -> ( ( r ^ 2 ) || n <-> ( r ^ 2 ) || N ) )
4 3 rabbidv 
 |-  ( n = N -> { r e. NN | ( r ^ 2 ) || n } = { r e. NN | ( r ^ 2 ) || N } )
5 4 supeq1d 
 |-  ( n = N -> sup ( { r e. NN | ( r ^ 2 ) || n } , RR , < ) = sup ( { r e. NN | ( r ^ 2 ) || N } , RR , < ) )
6 ltso 
 |-  < Or RR
7 6 supex 
 |-  sup ( { r e. NN | ( r ^ 2 ) || N } , RR , < ) e. _V
8 5 1 7 fvmpt 
 |-  ( N e. NN -> ( Q ` N ) = sup ( { r e. NN | ( r ^ 2 ) || N } , RR , < ) )
9 nnssz 
 |-  NN C_ ZZ
10 2 9 sstri 
 |-  { r e. NN | ( r ^ 2 ) || N } C_ ZZ
11 oveq1 
 |-  ( r = 1 -> ( r ^ 2 ) = ( 1 ^ 2 ) )
12 sq1 
 |-  ( 1 ^ 2 ) = 1
13 11 12 eqtrdi 
 |-  ( r = 1 -> ( r ^ 2 ) = 1 )
14 13 breq1d 
 |-  ( r = 1 -> ( ( r ^ 2 ) || N <-> 1 || N ) )
15 1nn 
 |-  1 e. NN
16 15 a1i 
 |-  ( N e. NN -> 1 e. NN )
17 nnz 
 |-  ( N e. NN -> N e. ZZ )
18 1dvds 
 |-  ( N e. ZZ -> 1 || N )
19 17 18 syl 
 |-  ( N e. NN -> 1 || N )
20 14 16 19 elrabd 
 |-  ( N e. NN -> 1 e. { r e. NN | ( r ^ 2 ) || N } )
21 20 ne0d 
 |-  ( N e. NN -> { r e. NN | ( r ^ 2 ) || N } =/= (/) )
22 nnz 
 |-  ( z e. NN -> z e. ZZ )
23 zsqcl 
 |-  ( z e. ZZ -> ( z ^ 2 ) e. ZZ )
24 22 23 syl 
 |-  ( z e. NN -> ( z ^ 2 ) e. ZZ )
25 id 
 |-  ( N e. NN -> N e. NN )
26 dvdsle 
 |-  ( ( ( z ^ 2 ) e. ZZ /\ N e. NN ) -> ( ( z ^ 2 ) || N -> ( z ^ 2 ) <_ N ) )
27 24 25 26 syl2anr 
 |-  ( ( N e. NN /\ z e. NN ) -> ( ( z ^ 2 ) || N -> ( z ^ 2 ) <_ N ) )
28 nnlesq 
 |-  ( z e. NN -> z <_ ( z ^ 2 ) )
29 28 adantl 
 |-  ( ( N e. NN /\ z e. NN ) -> z <_ ( z ^ 2 ) )
30 nnre 
 |-  ( z e. NN -> z e. RR )
31 30 adantl 
 |-  ( ( N e. NN /\ z e. NN ) -> z e. RR )
32 31 resqcld 
 |-  ( ( N e. NN /\ z e. NN ) -> ( z ^ 2 ) e. RR )
33 nnre 
 |-  ( N e. NN -> N e. RR )
34 33 adantr 
 |-  ( ( N e. NN /\ z e. NN ) -> N e. RR )
35 letr 
 |-  ( ( z e. RR /\ ( z ^ 2 ) e. RR /\ N e. RR ) -> ( ( z <_ ( z ^ 2 ) /\ ( z ^ 2 ) <_ N ) -> z <_ N ) )
36 31 32 34 35 syl3anc 
 |-  ( ( N e. NN /\ z e. NN ) -> ( ( z <_ ( z ^ 2 ) /\ ( z ^ 2 ) <_ N ) -> z <_ N ) )
37 29 36 mpand 
 |-  ( ( N e. NN /\ z e. NN ) -> ( ( z ^ 2 ) <_ N -> z <_ N ) )
38 27 37 syld 
 |-  ( ( N e. NN /\ z e. NN ) -> ( ( z ^ 2 ) || N -> z <_ N ) )
39 38 ralrimiva 
 |-  ( N e. NN -> A. z e. NN ( ( z ^ 2 ) || N -> z <_ N ) )
40 oveq1 
 |-  ( r = z -> ( r ^ 2 ) = ( z ^ 2 ) )
41 40 breq1d 
 |-  ( r = z -> ( ( r ^ 2 ) || N <-> ( z ^ 2 ) || N ) )
42 41 ralrab 
 |-  ( A. z e. { r e. NN | ( r ^ 2 ) || N } z <_ N <-> A. z e. NN ( ( z ^ 2 ) || N -> z <_ N ) )
43 39 42 sylibr 
 |-  ( N e. NN -> A. z e. { r e. NN | ( r ^ 2 ) || N } z <_ N )
44 brralrspcev 
 |-  ( ( N e. ZZ /\ A. z e. { r e. NN | ( r ^ 2 ) || N } z <_ N ) -> E. x e. ZZ A. z e. { r e. NN | ( r ^ 2 ) || N } z <_ x )
45 17 43 44 syl2anc 
 |-  ( N e. NN -> E. x e. ZZ A. z e. { r e. NN | ( r ^ 2 ) || N } z <_ x )
46 suprzcl2 
 |-  ( ( { r e. NN | ( r ^ 2 ) || N } C_ ZZ /\ { r e. NN | ( r ^ 2 ) || N } =/= (/) /\ E. x e. ZZ A. z e. { r e. NN | ( r ^ 2 ) || N } z <_ x ) -> sup ( { r e. NN | ( r ^ 2 ) || N } , RR , < ) e. { r e. NN | ( r ^ 2 ) || N } )
47 10 21 45 46 mp3an2i 
 |-  ( N e. NN -> sup ( { r e. NN | ( r ^ 2 ) || N } , RR , < ) e. { r e. NN | ( r ^ 2 ) || N } )
48 8 47 eqeltrd 
 |-  ( N e. NN -> ( Q ` N ) e. { r e. NN | ( r ^ 2 ) || N } )
49 2 48 sseldi 
 |-  ( N e. NN -> ( Q ` N ) e. NN )
50 oveq1 
 |-  ( z = ( Q ` N ) -> ( z ^ 2 ) = ( ( Q ` N ) ^ 2 ) )
51 50 breq1d 
 |-  ( z = ( Q ` N ) -> ( ( z ^ 2 ) || N <-> ( ( Q ` N ) ^ 2 ) || N ) )
52 41 cbvrabv 
 |-  { r e. NN | ( r ^ 2 ) || N } = { z e. NN | ( z ^ 2 ) || N }
53 51 52 elrab2 
 |-  ( ( Q ` N ) e. { r e. NN | ( r ^ 2 ) || N } <-> ( ( Q ` N ) e. NN /\ ( ( Q ` N ) ^ 2 ) || N ) )
54 48 53 sylib 
 |-  ( N e. NN -> ( ( Q ` N ) e. NN /\ ( ( Q ` N ) ^ 2 ) || N ) )
55 54 simprd 
 |-  ( N e. NN -> ( ( Q ` N ) ^ 2 ) || N )
56 49 adantr 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) -> ( Q ` N ) e. NN )
57 56 nncnd 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) -> ( Q ` N ) e. CC )
58 57 mulid1d 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) -> ( ( Q ` N ) x. 1 ) = ( Q ` N ) )
59 eluz2gt1 
 |-  ( K e. ( ZZ>= ` 2 ) -> 1 < K )
60 59 adantl 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) -> 1 < K )
61 1red 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) -> 1 e. RR )
62 eluz2nn 
 |-  ( K e. ( ZZ>= ` 2 ) -> K e. NN )
63 62 adantl 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) -> K e. NN )
64 63 nnred 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) -> K e. RR )
65 56 nnred 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) -> ( Q ` N ) e. RR )
66 56 nngt0d 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) -> 0 < ( Q ` N ) )
67 ltmul2 
 |-  ( ( 1 e. RR /\ K e. RR /\ ( ( Q ` N ) e. RR /\ 0 < ( Q ` N ) ) ) -> ( 1 < K <-> ( ( Q ` N ) x. 1 ) < ( ( Q ` N ) x. K ) ) )
68 61 64 65 66 67 syl112anc 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) -> ( 1 < K <-> ( ( Q ` N ) x. 1 ) < ( ( Q ` N ) x. K ) ) )
69 60 68 mpbid 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) -> ( ( Q ` N ) x. 1 ) < ( ( Q ` N ) x. K ) )
70 58 69 eqbrtrrd 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) -> ( Q ` N ) < ( ( Q ` N ) x. K ) )
71 nnmulcl 
 |-  ( ( ( Q ` N ) e. NN /\ K e. NN ) -> ( ( Q ` N ) x. K ) e. NN )
72 49 62 71 syl2an 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) -> ( ( Q ` N ) x. K ) e. NN )
73 72 nnred 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) -> ( ( Q ` N ) x. K ) e. RR )
74 65 73 ltnled 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) -> ( ( Q ` N ) < ( ( Q ` N ) x. K ) <-> -. ( ( Q ` N ) x. K ) <_ ( Q ` N ) ) )
75 70 74 mpbid 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) -> -. ( ( Q ` N ) x. K ) <_ ( Q ` N ) )
76 45 ad2antrr 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> E. x e. ZZ A. z e. { r e. NN | ( r ^ 2 ) || N } z <_ x )
77 oveq1 
 |-  ( r = ( ( Q ` N ) x. K ) -> ( r ^ 2 ) = ( ( ( Q ` N ) x. K ) ^ 2 ) )
78 77 breq1d 
 |-  ( r = ( ( Q ` N ) x. K ) -> ( ( r ^ 2 ) || N <-> ( ( ( Q ` N ) x. K ) ^ 2 ) || N ) )
79 72 adantr 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( ( Q ` N ) x. K ) e. NN )
80 simpr 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) )
81 63 adantr 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> K e. NN )
82 81 nnsqcld 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( K ^ 2 ) e. NN )
83 nnz 
 |-  ( ( K ^ 2 ) e. NN -> ( K ^ 2 ) e. ZZ )
84 82 83 syl 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( K ^ 2 ) e. ZZ )
85 49 nnsqcld 
 |-  ( N e. NN -> ( ( Q ` N ) ^ 2 ) e. NN )
86 9 85 sseldi 
 |-  ( N e. NN -> ( ( Q ` N ) ^ 2 ) e. ZZ )
87 85 nnne0d 
 |-  ( N e. NN -> ( ( Q ` N ) ^ 2 ) =/= 0 )
88 dvdsval2 
 |-  ( ( ( ( Q ` N ) ^ 2 ) e. ZZ /\ ( ( Q ` N ) ^ 2 ) =/= 0 /\ N e. ZZ ) -> ( ( ( Q ` N ) ^ 2 ) || N <-> ( N / ( ( Q ` N ) ^ 2 ) ) e. ZZ ) )
89 86 87 17 88 syl3anc 
 |-  ( N e. NN -> ( ( ( Q ` N ) ^ 2 ) || N <-> ( N / ( ( Q ` N ) ^ 2 ) ) e. ZZ ) )
90 55 89 mpbid 
 |-  ( N e. NN -> ( N / ( ( Q ` N ) ^ 2 ) ) e. ZZ )
91 90 ad2antrr 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( N / ( ( Q ` N ) ^ 2 ) ) e. ZZ )
92 86 ad2antrr 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( ( Q ` N ) ^ 2 ) e. ZZ )
93 dvdscmul 
 |-  ( ( ( K ^ 2 ) e. ZZ /\ ( N / ( ( Q ` N ) ^ 2 ) ) e. ZZ /\ ( ( Q ` N ) ^ 2 ) e. ZZ ) -> ( ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) -> ( ( ( Q ` N ) ^ 2 ) x. ( K ^ 2 ) ) || ( ( ( Q ` N ) ^ 2 ) x. ( N / ( ( Q ` N ) ^ 2 ) ) ) ) )
94 84 91 92 93 syl3anc 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) -> ( ( ( Q ` N ) ^ 2 ) x. ( K ^ 2 ) ) || ( ( ( Q ` N ) ^ 2 ) x. ( N / ( ( Q ` N ) ^ 2 ) ) ) ) )
95 80 94 mpd 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( ( ( Q ` N ) ^ 2 ) x. ( K ^ 2 ) ) || ( ( ( Q ` N ) ^ 2 ) x. ( N / ( ( Q ` N ) ^ 2 ) ) ) )
96 57 adantr 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( Q ` N ) e. CC )
97 81 nncnd 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> K e. CC )
98 96 97 sqmuld 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( ( ( Q ` N ) x. K ) ^ 2 ) = ( ( ( Q ` N ) ^ 2 ) x. ( K ^ 2 ) ) )
99 98 eqcomd 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( ( ( Q ` N ) ^ 2 ) x. ( K ^ 2 ) ) = ( ( ( Q ` N ) x. K ) ^ 2 ) )
100 nncn 
 |-  ( N e. NN -> N e. CC )
101 100 ad2antrr 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> N e. CC )
102 85 ad2antrr 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( ( Q ` N ) ^ 2 ) e. NN )
103 102 nncnd 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( ( Q ` N ) ^ 2 ) e. CC )
104 87 ad2antrr 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( ( Q ` N ) ^ 2 ) =/= 0 )
105 101 103 104 divcan2d 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( ( ( Q ` N ) ^ 2 ) x. ( N / ( ( Q ` N ) ^ 2 ) ) ) = N )
106 95 99 105 3brtr3d 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( ( ( Q ` N ) x. K ) ^ 2 ) || N )
107 78 79 106 elrabd 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( ( Q ` N ) x. K ) e. { r e. NN | ( r ^ 2 ) || N } )
108 suprzub 
 |-  ( ( { r e. NN | ( r ^ 2 ) || N } C_ ZZ /\ E. x e. ZZ A. z e. { r e. NN | ( r ^ 2 ) || N } z <_ x /\ ( ( Q ` N ) x. K ) e. { r e. NN | ( r ^ 2 ) || N } ) -> ( ( Q ` N ) x. K ) <_ sup ( { r e. NN | ( r ^ 2 ) || N } , RR , < ) )
109 10 76 107 108 mp3an2i 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( ( Q ` N ) x. K ) <_ sup ( { r e. NN | ( r ^ 2 ) || N } , RR , < ) )
110 8 ad2antrr 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( Q ` N ) = sup ( { r e. NN | ( r ^ 2 ) || N } , RR , < ) )
111 109 110 breqtrrd 
 |-  ( ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) /\ ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) -> ( ( Q ` N ) x. K ) <_ ( Q ` N ) )
112 75 111 mtand 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` 2 ) ) -> -. ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) )
113 112 ex 
 |-  ( N e. NN -> ( K e. ( ZZ>= ` 2 ) -> -. ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) )
114 49 55 113 3jca 
 |-  ( N e. NN -> ( ( Q ` N ) e. NN /\ ( ( Q ` N ) ^ 2 ) || N /\ ( K e. ( ZZ>= ` 2 ) -> -. ( K ^ 2 ) || ( N / ( ( Q ` N ) ^ 2 ) ) ) ) )