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 ) ) ) ) ) |