Step |
Hyp |
Ref |
Expression |
1 |
|
breq2 |
|- ( x = A -> ( k < x <-> k < A ) ) |
2 |
|
breq2 |
|- ( x = A -> ( ( p ^ n ) || x <-> ( p ^ n ) || A ) ) |
3 |
2
|
bibi2d |
|- ( x = A -> ( ( ( p ^ n ) || k <-> ( p ^ n ) || x ) <-> ( ( p ^ n ) || k <-> ( p ^ n ) || A ) ) ) |
4 |
3
|
notbid |
|- ( x = A -> ( -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) <-> -. ( ( p ^ n ) || k <-> ( p ^ n ) || A ) ) ) |
5 |
4
|
2rexbidv |
|- ( x = A -> ( E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) <-> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || A ) ) ) |
6 |
1 5
|
imbi12d |
|- ( x = A -> ( ( k < x -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) ) <-> ( k < A -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || A ) ) ) ) |
7 |
6
|
ralbidv |
|- ( x = A -> ( A. k e. NN ( k < x -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) ) <-> A. k e. NN ( k < A -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || A ) ) ) ) |
8 |
|
breq2 |
|- ( x = 1 -> ( k < x <-> k < 1 ) ) |
9 |
|
breq2 |
|- ( x = 1 -> ( ( p ^ n ) || x <-> ( p ^ n ) || 1 ) ) |
10 |
9
|
bibi2d |
|- ( x = 1 -> ( ( ( p ^ n ) || k <-> ( p ^ n ) || x ) <-> ( ( p ^ n ) || k <-> ( p ^ n ) || 1 ) ) ) |
11 |
10
|
notbid |
|- ( x = 1 -> ( -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) <-> -. ( ( p ^ n ) || k <-> ( p ^ n ) || 1 ) ) ) |
12 |
11
|
2rexbidv |
|- ( x = 1 -> ( E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) <-> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || 1 ) ) ) |
13 |
8 12
|
imbi12d |
|- ( x = 1 -> ( ( k < x -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) ) <-> ( k < 1 -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || 1 ) ) ) ) |
14 |
13
|
ralbidv |
|- ( x = 1 -> ( A. k e. NN ( k < x -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) ) <-> A. k e. NN ( k < 1 -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || 1 ) ) ) ) |
15 |
|
breq2 |
|- ( x = y -> ( k < x <-> k < y ) ) |
16 |
|
breq2 |
|- ( x = y -> ( ( p ^ n ) || x <-> ( p ^ n ) || y ) ) |
17 |
16
|
bibi2d |
|- ( x = y -> ( ( ( p ^ n ) || k <-> ( p ^ n ) || x ) <-> ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) |
18 |
17
|
notbid |
|- ( x = y -> ( -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) <-> -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) |
19 |
18
|
2rexbidv |
|- ( x = y -> ( E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) <-> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) |
20 |
15 19
|
imbi12d |
|- ( x = y -> ( ( k < x -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) ) <-> ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) ) |
21 |
20
|
ralbidv |
|- ( x = y -> ( A. k e. NN ( k < x -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) ) <-> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) ) |
22 |
|
nnnlt1 |
|- ( k e. NN -> -. k < 1 ) |
23 |
22
|
pm2.21d |
|- ( k e. NN -> ( k < 1 -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || 1 ) ) ) |
24 |
23
|
rgen |
|- A. k e. NN ( k < 1 -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || 1 ) ) |
25 |
|
exprmfct |
|- ( x e. ( ZZ>= ` 2 ) -> E. q e. Prime q || x ) |
26 |
|
prmz |
|- ( q e. Prime -> q e. ZZ ) |
27 |
26
|
adantr |
|- ( ( q e. Prime /\ t e. NN ) -> q e. ZZ ) |
28 |
|
prmnn |
|- ( q e. Prime -> q e. NN ) |
29 |
28
|
nnne0d |
|- ( q e. Prime -> q =/= 0 ) |
30 |
29
|
adantr |
|- ( ( q e. Prime /\ t e. NN ) -> q =/= 0 ) |
31 |
|
nnz |
|- ( t e. NN -> t e. ZZ ) |
32 |
31
|
adantl |
|- ( ( q e. Prime /\ t e. NN ) -> t e. ZZ ) |
33 |
|
dvdsval2 |
|- ( ( q e. ZZ /\ q =/= 0 /\ t e. ZZ ) -> ( q || t <-> ( t / q ) e. ZZ ) ) |
34 |
27 30 32 33
|
syl3anc |
|- ( ( q e. Prime /\ t e. NN ) -> ( q || t <-> ( t / q ) e. ZZ ) ) |
35 |
34
|
biimpd |
|- ( ( q e. Prime /\ t e. NN ) -> ( q || t -> ( t / q ) e. ZZ ) ) |
36 |
35
|
3ad2antl2 |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ t e. NN ) -> ( q || t -> ( t / q ) e. ZZ ) ) |
37 |
36
|
adantrl |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ ( A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) /\ t e. NN ) ) -> ( q || t -> ( t / q ) e. ZZ ) ) |
38 |
|
simprr |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ ( t e. NN /\ ( t / q ) e. ZZ ) ) -> ( t / q ) e. ZZ ) |
39 |
|
nnre |
|- ( t e. NN -> t e. RR ) |
40 |
|
nngt0 |
|- ( t e. NN -> 0 < t ) |
41 |
39 40
|
jca |
|- ( t e. NN -> ( t e. RR /\ 0 < t ) ) |
42 |
|
nnre |
|- ( q e. NN -> q e. RR ) |
43 |
|
nngt0 |
|- ( q e. NN -> 0 < q ) |
44 |
42 43
|
jca |
|- ( q e. NN -> ( q e. RR /\ 0 < q ) ) |
45 |
28 44
|
syl |
|- ( q e. Prime -> ( q e. RR /\ 0 < q ) ) |
46 |
|
divgt0 |
|- ( ( ( t e. RR /\ 0 < t ) /\ ( q e. RR /\ 0 < q ) ) -> 0 < ( t / q ) ) |
47 |
41 45 46
|
syl2anr |
|- ( ( q e. Prime /\ t e. NN ) -> 0 < ( t / q ) ) |
48 |
47
|
3ad2antl2 |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ t e. NN ) -> 0 < ( t / q ) ) |
49 |
48
|
adantrr |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ ( t e. NN /\ ( t / q ) e. ZZ ) ) -> 0 < ( t / q ) ) |
50 |
|
elnnz |
|- ( ( t / q ) e. NN <-> ( ( t / q ) e. ZZ /\ 0 < ( t / q ) ) ) |
51 |
38 49 50
|
sylanbrc |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ ( t e. NN /\ ( t / q ) e. ZZ ) ) -> ( t / q ) e. NN ) |
52 |
51
|
expr |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ t e. NN ) -> ( ( t / q ) e. ZZ -> ( t / q ) e. NN ) ) |
53 |
52
|
adantrl |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ ( A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) /\ t e. NN ) ) -> ( ( t / q ) e. ZZ -> ( t / q ) e. NN ) ) |
54 |
26
|
adantr |
|- ( ( q e. Prime /\ x e. ( ZZ>= ` 2 ) ) -> q e. ZZ ) |
55 |
29
|
adantr |
|- ( ( q e. Prime /\ x e. ( ZZ>= ` 2 ) ) -> q =/= 0 ) |
56 |
|
eluzelz |
|- ( x e. ( ZZ>= ` 2 ) -> x e. ZZ ) |
57 |
56
|
adantl |
|- ( ( q e. Prime /\ x e. ( ZZ>= ` 2 ) ) -> x e. ZZ ) |
58 |
|
dvdsval2 |
|- ( ( q e. ZZ /\ q =/= 0 /\ x e. ZZ ) -> ( q || x <-> ( x / q ) e. ZZ ) ) |
59 |
54 55 57 58
|
syl3anc |
|- ( ( q e. Prime /\ x e. ( ZZ>= ` 2 ) ) -> ( q || x <-> ( x / q ) e. ZZ ) ) |
60 |
|
eluzelre |
|- ( x e. ( ZZ>= ` 2 ) -> x e. RR ) |
61 |
|
2z |
|- 2 e. ZZ |
62 |
61
|
eluz1i |
|- ( x e. ( ZZ>= ` 2 ) <-> ( x e. ZZ /\ 2 <_ x ) ) |
63 |
|
2pos |
|- 0 < 2 |
64 |
|
zre |
|- ( x e. ZZ -> x e. RR ) |
65 |
|
0re |
|- 0 e. RR |
66 |
|
2re |
|- 2 e. RR |
67 |
|
ltletr |
|- ( ( 0 e. RR /\ 2 e. RR /\ x e. RR ) -> ( ( 0 < 2 /\ 2 <_ x ) -> 0 < x ) ) |
68 |
65 66 67
|
mp3an12 |
|- ( x e. RR -> ( ( 0 < 2 /\ 2 <_ x ) -> 0 < x ) ) |
69 |
64 68
|
syl |
|- ( x e. ZZ -> ( ( 0 < 2 /\ 2 <_ x ) -> 0 < x ) ) |
70 |
63 69
|
mpani |
|- ( x e. ZZ -> ( 2 <_ x -> 0 < x ) ) |
71 |
70
|
imp |
|- ( ( x e. ZZ /\ 2 <_ x ) -> 0 < x ) |
72 |
62 71
|
sylbi |
|- ( x e. ( ZZ>= ` 2 ) -> 0 < x ) |
73 |
60 72
|
jca |
|- ( x e. ( ZZ>= ` 2 ) -> ( x e. RR /\ 0 < x ) ) |
74 |
|
divgt0 |
|- ( ( ( x e. RR /\ 0 < x ) /\ ( q e. RR /\ 0 < q ) ) -> 0 < ( x / q ) ) |
75 |
73 45 74
|
syl2anr |
|- ( ( q e. Prime /\ x e. ( ZZ>= ` 2 ) ) -> 0 < ( x / q ) ) |
76 |
75
|
a1d |
|- ( ( q e. Prime /\ x e. ( ZZ>= ` 2 ) ) -> ( ( x / q ) e. ZZ -> 0 < ( x / q ) ) ) |
77 |
76
|
ancld |
|- ( ( q e. Prime /\ x e. ( ZZ>= ` 2 ) ) -> ( ( x / q ) e. ZZ -> ( ( x / q ) e. ZZ /\ 0 < ( x / q ) ) ) ) |
78 |
|
elnnz |
|- ( ( x / q ) e. NN <-> ( ( x / q ) e. ZZ /\ 0 < ( x / q ) ) ) |
79 |
77 78
|
syl6ibr |
|- ( ( q e. Prime /\ x e. ( ZZ>= ` 2 ) ) -> ( ( x / q ) e. ZZ -> ( x / q ) e. NN ) ) |
80 |
59 79
|
sylbid |
|- ( ( q e. Prime /\ x e. ( ZZ>= ` 2 ) ) -> ( q || x -> ( x / q ) e. NN ) ) |
81 |
80
|
ancoms |
|- ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) -> ( q || x -> ( x / q ) e. NN ) ) |
82 |
|
breq1 |
|- ( y = ( x / q ) -> ( y < x <-> ( x / q ) < x ) ) |
83 |
|
breq2 |
|- ( y = ( x / q ) -> ( k < y <-> k < ( x / q ) ) ) |
84 |
|
breq2 |
|- ( y = ( x / q ) -> ( ( p ^ n ) || y <-> ( p ^ n ) || ( x / q ) ) ) |
85 |
84
|
bibi2d |
|- ( y = ( x / q ) -> ( ( ( p ^ n ) || k <-> ( p ^ n ) || y ) <-> ( ( p ^ n ) || k <-> ( p ^ n ) || ( x / q ) ) ) ) |
86 |
85
|
notbid |
|- ( y = ( x / q ) -> ( -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) <-> -. ( ( p ^ n ) || k <-> ( p ^ n ) || ( x / q ) ) ) ) |
87 |
86
|
2rexbidv |
|- ( y = ( x / q ) -> ( E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) <-> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || ( x / q ) ) ) ) |
88 |
83 87
|
imbi12d |
|- ( y = ( x / q ) -> ( ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) <-> ( k < ( x / q ) -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || ( x / q ) ) ) ) ) |
89 |
88
|
ralbidv |
|- ( y = ( x / q ) -> ( A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) <-> A. k e. NN ( k < ( x / q ) -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || ( x / q ) ) ) ) ) |
90 |
82 89
|
imbi12d |
|- ( y = ( x / q ) -> ( ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) <-> ( ( x / q ) < x -> A. k e. NN ( k < ( x / q ) -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || ( x / q ) ) ) ) ) ) |
91 |
90
|
rspcv |
|- ( ( x / q ) e. NN -> ( A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) -> ( ( x / q ) < x -> A. k e. NN ( k < ( x / q ) -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || ( x / q ) ) ) ) ) ) |
92 |
91
|
3ad2ant1 |
|- ( ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) -> ( A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) -> ( ( x / q ) < x -> A. k e. NN ( k < ( x / q ) -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || ( x / q ) ) ) ) ) ) |
93 |
92
|
adantl |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> ( A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) -> ( ( x / q ) < x -> A. k e. NN ( k < ( x / q ) -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || ( x / q ) ) ) ) ) ) |
94 |
|
eluzelcn |
|- ( x e. ( ZZ>= ` 2 ) -> x e. CC ) |
95 |
94
|
mulid2d |
|- ( x e. ( ZZ>= ` 2 ) -> ( 1 x. x ) = x ) |
96 |
95
|
ad2antrr |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> ( 1 x. x ) = x ) |
97 |
|
prmgt1 |
|- ( q e. Prime -> 1 < q ) |
98 |
97
|
ad2antlr |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> 1 < q ) |
99 |
|
1red |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> 1 e. RR ) |
100 |
28
|
nnred |
|- ( q e. Prime -> q e. RR ) |
101 |
100
|
ad2antlr |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> q e. RR ) |
102 |
60
|
ad2antrr |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> x e. RR ) |
103 |
72
|
ad2antrr |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> 0 < x ) |
104 |
|
ltmul1 |
|- ( ( 1 e. RR /\ q e. RR /\ ( x e. RR /\ 0 < x ) ) -> ( 1 < q <-> ( 1 x. x ) < ( q x. x ) ) ) |
105 |
99 101 102 103 104
|
syl112anc |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> ( 1 < q <-> ( 1 x. x ) < ( q x. x ) ) ) |
106 |
98 105
|
mpbid |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> ( 1 x. x ) < ( q x. x ) ) |
107 |
96 106
|
eqbrtrrd |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> x < ( q x. x ) ) |
108 |
28 43
|
syl |
|- ( q e. Prime -> 0 < q ) |
109 |
108
|
ad2antlr |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> 0 < q ) |
110 |
|
ltdivmul |
|- ( ( x e. RR /\ x e. RR /\ ( q e. RR /\ 0 < q ) ) -> ( ( x / q ) < x <-> x < ( q x. x ) ) ) |
111 |
102 102 101 109 110
|
syl112anc |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> ( ( x / q ) < x <-> x < ( q x. x ) ) ) |
112 |
107 111
|
mpbird |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> ( x / q ) < x ) |
113 |
|
breq1 |
|- ( k = ( t / q ) -> ( k < ( x / q ) <-> ( t / q ) < ( x / q ) ) ) |
114 |
|
breq2 |
|- ( k = ( t / q ) -> ( ( p ^ n ) || k <-> ( p ^ n ) || ( t / q ) ) ) |
115 |
114
|
bibi1d |
|- ( k = ( t / q ) -> ( ( ( p ^ n ) || k <-> ( p ^ n ) || ( x / q ) ) <-> ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) ) |
116 |
115
|
notbid |
|- ( k = ( t / q ) -> ( -. ( ( p ^ n ) || k <-> ( p ^ n ) || ( x / q ) ) <-> -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) ) |
117 |
116
|
2rexbidv |
|- ( k = ( t / q ) -> ( E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || ( x / q ) ) <-> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) ) |
118 |
113 117
|
imbi12d |
|- ( k = ( t / q ) -> ( ( k < ( x / q ) -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || ( x / q ) ) ) <-> ( ( t / q ) < ( x / q ) -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) ) ) |
119 |
118
|
rspcv |
|- ( ( t / q ) e. NN -> ( A. k e. NN ( k < ( x / q ) -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || ( x / q ) ) ) -> ( ( t / q ) < ( x / q ) -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) ) ) |
120 |
119
|
3ad2ant2 |
|- ( ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) -> ( A. k e. NN ( k < ( x / q ) -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || ( x / q ) ) ) -> ( ( t / q ) < ( x / q ) -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) ) ) |
121 |
120
|
adantl |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> ( A. k e. NN ( k < ( x / q ) -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || ( x / q ) ) ) -> ( ( t / q ) < ( x / q ) -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) ) ) |
122 |
39
|
3ad2ant3 |
|- ( ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) -> t e. RR ) |
123 |
122
|
adantl |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> t e. RR ) |
124 |
|
ltdiv1 |
|- ( ( t e. RR /\ x e. RR /\ ( q e. RR /\ 0 < q ) ) -> ( t < x <-> ( t / q ) < ( x / q ) ) ) |
125 |
123 102 101 109 124
|
syl112anc |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> ( t < x <-> ( t / q ) < ( x / q ) ) ) |
126 |
125
|
biimpa |
|- ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) -> ( t / q ) < ( x / q ) ) |
127 |
|
simprll |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) ) -> p e. Prime ) |
128 |
|
peano2nn |
|- ( n e. NN -> ( n + 1 ) e. NN ) |
129 |
128
|
adantl |
|- ( ( p e. Prime /\ n e. NN ) -> ( n + 1 ) e. NN ) |
130 |
129
|
ad2antrl |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. ( ( q ^ n ) || ( t / q ) <-> ( q ^ n ) || ( x / q ) ) ) ) -> ( n + 1 ) e. NN ) |
131 |
26
|
ad4antlr |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> q e. ZZ ) |
132 |
|
nnnn0 |
|- ( n e. NN -> n e. NN0 ) |
133 |
132
|
ad2antll |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> n e. NN0 ) |
134 |
|
zexpcl |
|- ( ( q e. ZZ /\ n e. NN0 ) -> ( q ^ n ) e. ZZ ) |
135 |
131 133 134
|
syl2anc |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( q ^ n ) e. ZZ ) |
136 |
|
nnz |
|- ( ( t / q ) e. NN -> ( t / q ) e. ZZ ) |
137 |
136
|
3ad2ant2 |
|- ( ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) -> ( t / q ) e. ZZ ) |
138 |
137
|
ad3antlr |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( t / q ) e. ZZ ) |
139 |
29
|
ad4antlr |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> q =/= 0 ) |
140 |
|
dvdsmulcr |
|- ( ( ( q ^ n ) e. ZZ /\ ( t / q ) e. ZZ /\ ( q e. ZZ /\ q =/= 0 ) ) -> ( ( ( q ^ n ) x. q ) || ( ( t / q ) x. q ) <-> ( q ^ n ) || ( t / q ) ) ) |
141 |
135 138 131 139 140
|
syl112anc |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( ( ( q ^ n ) x. q ) || ( ( t / q ) x. q ) <-> ( q ^ n ) || ( t / q ) ) ) |
142 |
28
|
nncnd |
|- ( q e. Prime -> q e. CC ) |
143 |
142
|
ad4antlr |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> q e. CC ) |
144 |
143 133
|
expp1d |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( q ^ ( n + 1 ) ) = ( ( q ^ n ) x. q ) ) |
145 |
144
|
eqcomd |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( ( q ^ n ) x. q ) = ( q ^ ( n + 1 ) ) ) |
146 |
|
nncn |
|- ( t e. NN -> t e. CC ) |
147 |
146
|
3ad2ant3 |
|- ( ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) -> t e. CC ) |
148 |
147
|
ad3antlr |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> t e. CC ) |
149 |
148 143 139
|
divcan1d |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( ( t / q ) x. q ) = t ) |
150 |
145 149
|
breq12d |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( ( ( q ^ n ) x. q ) || ( ( t / q ) x. q ) <-> ( q ^ ( n + 1 ) ) || t ) ) |
151 |
141 150
|
bitr3d |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( ( q ^ n ) || ( t / q ) <-> ( q ^ ( n + 1 ) ) || t ) ) |
152 |
|
nnz |
|- ( ( x / q ) e. NN -> ( x / q ) e. ZZ ) |
153 |
152
|
3ad2ant1 |
|- ( ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) -> ( x / q ) e. ZZ ) |
154 |
153
|
ad3antlr |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( x / q ) e. ZZ ) |
155 |
|
dvdsmulcr |
|- ( ( ( q ^ n ) e. ZZ /\ ( x / q ) e. ZZ /\ ( q e. ZZ /\ q =/= 0 ) ) -> ( ( ( q ^ n ) x. q ) || ( ( x / q ) x. q ) <-> ( q ^ n ) || ( x / q ) ) ) |
156 |
135 154 131 139 155
|
syl112anc |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( ( ( q ^ n ) x. q ) || ( ( x / q ) x. q ) <-> ( q ^ n ) || ( x / q ) ) ) |
157 |
94
|
ad4antr |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> x e. CC ) |
158 |
157 143 139
|
divcan1d |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( ( x / q ) x. q ) = x ) |
159 |
145 158
|
breq12d |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( ( ( q ^ n ) x. q ) || ( ( x / q ) x. q ) <-> ( q ^ ( n + 1 ) ) || x ) ) |
160 |
156 159
|
bitr3d |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( ( q ^ n ) || ( x / q ) <-> ( q ^ ( n + 1 ) ) || x ) ) |
161 |
151 160
|
bibi12d |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( ( ( q ^ n ) || ( t / q ) <-> ( q ^ n ) || ( x / q ) ) <-> ( ( q ^ ( n + 1 ) ) || t <-> ( q ^ ( n + 1 ) ) || x ) ) ) |
162 |
161
|
notbid |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( -. ( ( q ^ n ) || ( t / q ) <-> ( q ^ n ) || ( x / q ) ) <-> -. ( ( q ^ ( n + 1 ) ) || t <-> ( q ^ ( n + 1 ) ) || x ) ) ) |
163 |
162
|
biimpd |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( -. ( ( q ^ n ) || ( t / q ) <-> ( q ^ n ) || ( x / q ) ) -> -. ( ( q ^ ( n + 1 ) ) || t <-> ( q ^ ( n + 1 ) ) || x ) ) ) |
164 |
163
|
impr |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. ( ( q ^ n ) || ( t / q ) <-> ( q ^ n ) || ( x / q ) ) ) ) -> -. ( ( q ^ ( n + 1 ) ) || t <-> ( q ^ ( n + 1 ) ) || x ) ) |
165 |
|
oveq2 |
|- ( m = ( n + 1 ) -> ( q ^ m ) = ( q ^ ( n + 1 ) ) ) |
166 |
165
|
breq1d |
|- ( m = ( n + 1 ) -> ( ( q ^ m ) || t <-> ( q ^ ( n + 1 ) ) || t ) ) |
167 |
165
|
breq1d |
|- ( m = ( n + 1 ) -> ( ( q ^ m ) || x <-> ( q ^ ( n + 1 ) ) || x ) ) |
168 |
166 167
|
bibi12d |
|- ( m = ( n + 1 ) -> ( ( ( q ^ m ) || t <-> ( q ^ m ) || x ) <-> ( ( q ^ ( n + 1 ) ) || t <-> ( q ^ ( n + 1 ) ) || x ) ) ) |
169 |
168
|
notbid |
|- ( m = ( n + 1 ) -> ( -. ( ( q ^ m ) || t <-> ( q ^ m ) || x ) <-> -. ( ( q ^ ( n + 1 ) ) || t <-> ( q ^ ( n + 1 ) ) || x ) ) ) |
170 |
169
|
rspcev |
|- ( ( ( n + 1 ) e. NN /\ -. ( ( q ^ ( n + 1 ) ) || t <-> ( q ^ ( n + 1 ) ) || x ) ) -> E. m e. NN -. ( ( q ^ m ) || t <-> ( q ^ m ) || x ) ) |
171 |
130 164 170
|
syl2anc |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. ( ( q ^ n ) || ( t / q ) <-> ( q ^ n ) || ( x / q ) ) ) ) -> E. m e. NN -. ( ( q ^ m ) || t <-> ( q ^ m ) || x ) ) |
172 |
|
oveq1 |
|- ( p = q -> ( p ^ n ) = ( q ^ n ) ) |
173 |
172
|
breq1d |
|- ( p = q -> ( ( p ^ n ) || ( t / q ) <-> ( q ^ n ) || ( t / q ) ) ) |
174 |
172
|
breq1d |
|- ( p = q -> ( ( p ^ n ) || ( x / q ) <-> ( q ^ n ) || ( x / q ) ) ) |
175 |
173 174
|
bibi12d |
|- ( p = q -> ( ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) <-> ( ( q ^ n ) || ( t / q ) <-> ( q ^ n ) || ( x / q ) ) ) ) |
176 |
175
|
notbid |
|- ( p = q -> ( -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) <-> -. ( ( q ^ n ) || ( t / q ) <-> ( q ^ n ) || ( x / q ) ) ) ) |
177 |
176
|
anbi2d |
|- ( p = q -> ( ( ( p e. Prime /\ n e. NN ) /\ -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) <-> ( ( p e. Prime /\ n e. NN ) /\ -. ( ( q ^ n ) || ( t / q ) <-> ( q ^ n ) || ( x / q ) ) ) ) ) |
178 |
177
|
anbi2d |
|- ( p = q -> ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) ) <-> ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. ( ( q ^ n ) || ( t / q ) <-> ( q ^ n ) || ( x / q ) ) ) ) ) ) |
179 |
|
oveq1 |
|- ( p = q -> ( p ^ m ) = ( q ^ m ) ) |
180 |
179
|
breq1d |
|- ( p = q -> ( ( p ^ m ) || t <-> ( q ^ m ) || t ) ) |
181 |
179
|
breq1d |
|- ( p = q -> ( ( p ^ m ) || x <-> ( q ^ m ) || x ) ) |
182 |
180 181
|
bibi12d |
|- ( p = q -> ( ( ( p ^ m ) || t <-> ( p ^ m ) || x ) <-> ( ( q ^ m ) || t <-> ( q ^ m ) || x ) ) ) |
183 |
182
|
notbid |
|- ( p = q -> ( -. ( ( p ^ m ) || t <-> ( p ^ m ) || x ) <-> -. ( ( q ^ m ) || t <-> ( q ^ m ) || x ) ) ) |
184 |
183
|
rexbidv |
|- ( p = q -> ( E. m e. NN -. ( ( p ^ m ) || t <-> ( p ^ m ) || x ) <-> E. m e. NN -. ( ( q ^ m ) || t <-> ( q ^ m ) || x ) ) ) |
185 |
178 184
|
imbi12d |
|- ( p = q -> ( ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) ) -> E. m e. NN -. ( ( p ^ m ) || t <-> ( p ^ m ) || x ) ) <-> ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. ( ( q ^ n ) || ( t / q ) <-> ( q ^ n ) || ( x / q ) ) ) ) -> E. m e. NN -. ( ( q ^ m ) || t <-> ( q ^ m ) || x ) ) ) ) |
186 |
171 185
|
mpbiri |
|- ( p = q -> ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) ) -> E. m e. NN -. ( ( p ^ m ) || t <-> ( p ^ m ) || x ) ) ) |
187 |
186
|
com12 |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) ) -> ( p = q -> E. m e. NN -. ( ( p ^ m ) || t <-> ( p ^ m ) || x ) ) ) |
188 |
|
simplr |
|- ( ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) -> n e. NN ) |
189 |
188
|
ad2antlr |
|- ( ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) /\ -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) -> n e. NN ) |
190 |
|
prmz |
|- ( p e. Prime -> p e. ZZ ) |
191 |
190
|
adantr |
|- ( ( p e. Prime /\ n e. NN ) -> p e. ZZ ) |
192 |
191
|
ad2antrl |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> p e. ZZ ) |
193 |
132
|
adantl |
|- ( ( p e. Prime /\ n e. NN ) -> n e. NN0 ) |
194 |
193
|
ad2antrl |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> n e. NN0 ) |
195 |
|
zexpcl |
|- ( ( p e. ZZ /\ n e. NN0 ) -> ( p ^ n ) e. ZZ ) |
196 |
192 194 195
|
syl2anc |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( p ^ n ) e. ZZ ) |
197 |
26
|
ad4antlr |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> q e. ZZ ) |
198 |
137
|
ad3antlr |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( t / q ) e. ZZ ) |
199 |
|
dvdsmultr2 |
|- ( ( ( p ^ n ) e. ZZ /\ q e. ZZ /\ ( t / q ) e. ZZ ) -> ( ( p ^ n ) || ( t / q ) -> ( p ^ n ) || ( q x. ( t / q ) ) ) ) |
200 |
196 197 198 199
|
syl3anc |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( ( p ^ n ) || ( t / q ) -> ( p ^ n ) || ( q x. ( t / q ) ) ) ) |
201 |
196 197
|
gcdcomd |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( ( p ^ n ) gcd q ) = ( q gcd ( p ^ n ) ) ) |
202 |
|
simp-4r |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> q e. Prime ) |
203 |
|
simprl |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> p e. Prime ) |
204 |
|
simprr |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> n e. NN ) |
205 |
|
prmdvdsexpb |
|- ( ( q e. Prime /\ p e. Prime /\ n e. NN ) -> ( q || ( p ^ n ) <-> q = p ) ) |
206 |
|
equcom |
|- ( q = p <-> p = q ) |
207 |
205 206
|
syl6bb |
|- ( ( q e. Prime /\ p e. Prime /\ n e. NN ) -> ( q || ( p ^ n ) <-> p = q ) ) |
208 |
207
|
biimpd |
|- ( ( q e. Prime /\ p e. Prime /\ n e. NN ) -> ( q || ( p ^ n ) -> p = q ) ) |
209 |
202 203 204 208
|
syl3anc |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( q || ( p ^ n ) -> p = q ) ) |
210 |
209
|
con3d |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( -. p = q -> -. q || ( p ^ n ) ) ) |
211 |
210
|
impr |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> -. q || ( p ^ n ) ) |
212 |
|
simp-4r |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> q e. Prime ) |
213 |
|
coprm |
|- ( ( q e. Prime /\ ( p ^ n ) e. ZZ ) -> ( -. q || ( p ^ n ) <-> ( q gcd ( p ^ n ) ) = 1 ) ) |
214 |
212 196 213
|
syl2anc |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( -. q || ( p ^ n ) <-> ( q gcd ( p ^ n ) ) = 1 ) ) |
215 |
211 214
|
mpbid |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( q gcd ( p ^ n ) ) = 1 ) |
216 |
201 215
|
eqtrd |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( ( p ^ n ) gcd q ) = 1 ) |
217 |
|
coprmdvds |
|- ( ( ( p ^ n ) e. ZZ /\ q e. ZZ /\ ( t / q ) e. ZZ ) -> ( ( ( p ^ n ) || ( q x. ( t / q ) ) /\ ( ( p ^ n ) gcd q ) = 1 ) -> ( p ^ n ) || ( t / q ) ) ) |
218 |
196 197 198 217
|
syl3anc |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( ( ( p ^ n ) || ( q x. ( t / q ) ) /\ ( ( p ^ n ) gcd q ) = 1 ) -> ( p ^ n ) || ( t / q ) ) ) |
219 |
216 218
|
mpan2d |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( ( p ^ n ) || ( q x. ( t / q ) ) -> ( p ^ n ) || ( t / q ) ) ) |
220 |
200 219
|
impbid |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( q x. ( t / q ) ) ) ) |
221 |
147
|
ad3antlr |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> t e. CC ) |
222 |
142
|
ad4antlr |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> q e. CC ) |
223 |
29
|
ad4antlr |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> q =/= 0 ) |
224 |
221 222 223
|
divcan2d |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( q x. ( t / q ) ) = t ) |
225 |
224
|
breq2d |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( ( p ^ n ) || ( q x. ( t / q ) ) <-> ( p ^ n ) || t ) ) |
226 |
220 225
|
bitrd |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || t ) ) |
227 |
153
|
ad3antlr |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( x / q ) e. ZZ ) |
228 |
|
dvdsmultr2 |
|- ( ( ( p ^ n ) e. ZZ /\ q e. ZZ /\ ( x / q ) e. ZZ ) -> ( ( p ^ n ) || ( x / q ) -> ( p ^ n ) || ( q x. ( x / q ) ) ) ) |
229 |
196 197 227 228
|
syl3anc |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( ( p ^ n ) || ( x / q ) -> ( p ^ n ) || ( q x. ( x / q ) ) ) ) |
230 |
|
coprmdvds |
|- ( ( ( p ^ n ) e. ZZ /\ q e. ZZ /\ ( x / q ) e. ZZ ) -> ( ( ( p ^ n ) || ( q x. ( x / q ) ) /\ ( ( p ^ n ) gcd q ) = 1 ) -> ( p ^ n ) || ( x / q ) ) ) |
231 |
196 197 227 230
|
syl3anc |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( ( ( p ^ n ) || ( q x. ( x / q ) ) /\ ( ( p ^ n ) gcd q ) = 1 ) -> ( p ^ n ) || ( x / q ) ) ) |
232 |
216 231
|
mpan2d |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( ( p ^ n ) || ( q x. ( x / q ) ) -> ( p ^ n ) || ( x / q ) ) ) |
233 |
229 232
|
impbid |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( ( p ^ n ) || ( x / q ) <-> ( p ^ n ) || ( q x. ( x / q ) ) ) ) |
234 |
94
|
ad4antr |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> x e. CC ) |
235 |
234 222 223
|
divcan2d |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( q x. ( x / q ) ) = x ) |
236 |
235
|
breq2d |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( ( p ^ n ) || ( q x. ( x / q ) ) <-> ( p ^ n ) || x ) ) |
237 |
233 236
|
bitrd |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( ( p ^ n ) || ( x / q ) <-> ( p ^ n ) || x ) ) |
238 |
226 237
|
bibi12d |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) <-> ( ( p ^ n ) || t <-> ( p ^ n ) || x ) ) ) |
239 |
238
|
notbid |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) <-> -. ( ( p ^ n ) || t <-> ( p ^ n ) || x ) ) ) |
240 |
239
|
biimpa |
|- ( ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) /\ -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) -> -. ( ( p ^ n ) || t <-> ( p ^ n ) || x ) ) |
241 |
|
oveq2 |
|- ( m = n -> ( p ^ m ) = ( p ^ n ) ) |
242 |
241
|
breq1d |
|- ( m = n -> ( ( p ^ m ) || t <-> ( p ^ n ) || t ) ) |
243 |
241
|
breq1d |
|- ( m = n -> ( ( p ^ m ) || x <-> ( p ^ n ) || x ) ) |
244 |
242 243
|
bibi12d |
|- ( m = n -> ( ( ( p ^ m ) || t <-> ( p ^ m ) || x ) <-> ( ( p ^ n ) || t <-> ( p ^ n ) || x ) ) ) |
245 |
244
|
notbid |
|- ( m = n -> ( -. ( ( p ^ m ) || t <-> ( p ^ m ) || x ) <-> -. ( ( p ^ n ) || t <-> ( p ^ n ) || x ) ) ) |
246 |
245
|
rspcev |
|- ( ( n e. NN /\ -. ( ( p ^ n ) || t <-> ( p ^ n ) || x ) ) -> E. m e. NN -. ( ( p ^ m ) || t <-> ( p ^ m ) || x ) ) |
247 |
189 240 246
|
syl2anc |
|- ( ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) /\ -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) -> E. m e. NN -. ( ( p ^ m ) || t <-> ( p ^ m ) || x ) ) |
248 |
247
|
ex |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. p = q ) ) -> ( -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) -> E. m e. NN -. ( ( p ^ m ) || t <-> ( p ^ m ) || x ) ) ) |
249 |
248
|
expr |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( -. p = q -> ( -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) -> E. m e. NN -. ( ( p ^ m ) || t <-> ( p ^ m ) || x ) ) ) ) |
250 |
249
|
com23 |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( p e. Prime /\ n e. NN ) ) -> ( -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) -> ( -. p = q -> E. m e. NN -. ( ( p ^ m ) || t <-> ( p ^ m ) || x ) ) ) ) |
251 |
250
|
impr |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) ) -> ( -. p = q -> E. m e. NN -. ( ( p ^ m ) || t <-> ( p ^ m ) || x ) ) ) |
252 |
187 251
|
pm2.61d |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) ) -> E. m e. NN -. ( ( p ^ m ) || t <-> ( p ^ m ) || x ) ) |
253 |
|
oveq1 |
|- ( r = p -> ( r ^ m ) = ( p ^ m ) ) |
254 |
253
|
breq1d |
|- ( r = p -> ( ( r ^ m ) || t <-> ( p ^ m ) || t ) ) |
255 |
253
|
breq1d |
|- ( r = p -> ( ( r ^ m ) || x <-> ( p ^ m ) || x ) ) |
256 |
254 255
|
bibi12d |
|- ( r = p -> ( ( ( r ^ m ) || t <-> ( r ^ m ) || x ) <-> ( ( p ^ m ) || t <-> ( p ^ m ) || x ) ) ) |
257 |
256
|
notbid |
|- ( r = p -> ( -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) <-> -. ( ( p ^ m ) || t <-> ( p ^ m ) || x ) ) ) |
258 |
257
|
rexbidv |
|- ( r = p -> ( E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) <-> E. m e. NN -. ( ( p ^ m ) || t <-> ( p ^ m ) || x ) ) ) |
259 |
258
|
rspcev |
|- ( ( p e. Prime /\ E. m e. NN -. ( ( p ^ m ) || t <-> ( p ^ m ) || x ) ) -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) |
260 |
127 252 259
|
syl2anc |
|- ( ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) /\ ( ( p e. Prime /\ n e. NN ) /\ -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) ) -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) |
261 |
260
|
exp32 |
|- ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) -> ( ( p e. Prime /\ n e. NN ) -> ( -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) ) |
262 |
261
|
rexlimdvv |
|- ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) -> ( E. p e. Prime E. n e. NN -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) |
263 |
126 262
|
embantd |
|- ( ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) /\ t < x ) -> ( ( ( t / q ) < ( x / q ) -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) |
264 |
263
|
ex |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> ( t < x -> ( ( ( t / q ) < ( x / q ) -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) ) |
265 |
264
|
com23 |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> ( ( ( t / q ) < ( x / q ) -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || ( t / q ) <-> ( p ^ n ) || ( x / q ) ) ) -> ( t < x -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) ) |
266 |
121 265
|
syld |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> ( A. k e. NN ( k < ( x / q ) -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || ( x / q ) ) ) -> ( t < x -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) ) |
267 |
112 266
|
embantd |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> ( ( ( x / q ) < x -> A. k e. NN ( k < ( x / q ) -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || ( x / q ) ) ) ) -> ( t < x -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) ) |
268 |
93 267
|
syld |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) /\ ( ( x / q ) e. NN /\ ( t / q ) e. NN /\ t e. NN ) ) -> ( A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) -> ( t < x -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) ) |
269 |
268
|
3exp2 |
|- ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) -> ( ( x / q ) e. NN -> ( ( t / q ) e. NN -> ( t e. NN -> ( A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) -> ( t < x -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) ) ) ) ) |
270 |
81 269
|
syld |
|- ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime ) -> ( q || x -> ( ( t / q ) e. NN -> ( t e. NN -> ( A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) -> ( t < x -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) ) ) ) ) |
271 |
270
|
3impia |
|- ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) -> ( ( t / q ) e. NN -> ( t e. NN -> ( A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) -> ( t < x -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) ) ) ) |
272 |
271
|
com24 |
|- ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) -> ( A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) -> ( t e. NN -> ( ( t / q ) e. NN -> ( t < x -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) ) ) ) |
273 |
272
|
imp32 |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ ( A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) /\ t e. NN ) ) -> ( ( t / q ) e. NN -> ( t < x -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) ) |
274 |
37 53 273
|
3syld |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ ( A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) /\ t e. NN ) ) -> ( q || t -> ( t < x -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) ) |
275 |
|
simpl2 |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ ( t e. NN /\ ( -. q || t /\ t < x ) ) ) -> q e. Prime ) |
276 |
|
1nn |
|- 1 e. NN |
277 |
276
|
a1i |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ ( t e. NN /\ ( -. q || t /\ t < x ) ) ) -> 1 e. NN ) |
278 |
142
|
exp1d |
|- ( q e. Prime -> ( q ^ 1 ) = q ) |
279 |
278
|
breq1d |
|- ( q e. Prime -> ( ( q ^ 1 ) || t <-> q || t ) ) |
280 |
279
|
notbid |
|- ( q e. Prime -> ( -. ( q ^ 1 ) || t <-> -. q || t ) ) |
281 |
280
|
biimpar |
|- ( ( q e. Prime /\ -. q || t ) -> -. ( q ^ 1 ) || t ) |
282 |
281
|
3ad2antl2 |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ -. q || t ) -> -. ( q ^ 1 ) || t ) |
283 |
282
|
adantrr |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ ( -. q || t /\ t < x ) ) -> -. ( q ^ 1 ) || t ) |
284 |
283
|
adantrl |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ ( t e. NN /\ ( -. q || t /\ t < x ) ) ) -> -. ( q ^ 1 ) || t ) |
285 |
278
|
breq1d |
|- ( q e. Prime -> ( ( q ^ 1 ) || x <-> q || x ) ) |
286 |
285
|
biimpar |
|- ( ( q e. Prime /\ q || x ) -> ( q ^ 1 ) || x ) |
287 |
286
|
3adant1 |
|- ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) -> ( q ^ 1 ) || x ) |
288 |
|
idd |
|- ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) -> ( ( ( q ^ 1 ) || x -> ( q ^ 1 ) || t ) -> ( ( q ^ 1 ) || x -> ( q ^ 1 ) || t ) ) ) |
289 |
287 288
|
mpid |
|- ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) -> ( ( ( q ^ 1 ) || x -> ( q ^ 1 ) || t ) -> ( q ^ 1 ) || t ) ) |
290 |
289
|
adantr |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ ( t e. NN /\ ( -. q || t /\ t < x ) ) ) -> ( ( ( q ^ 1 ) || x -> ( q ^ 1 ) || t ) -> ( q ^ 1 ) || t ) ) |
291 |
284 290
|
mtod |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ ( t e. NN /\ ( -. q || t /\ t < x ) ) ) -> -. ( ( q ^ 1 ) || x -> ( q ^ 1 ) || t ) ) |
292 |
|
biimpr |
|- ( ( ( q ^ 1 ) || t <-> ( q ^ 1 ) || x ) -> ( ( q ^ 1 ) || x -> ( q ^ 1 ) || t ) ) |
293 |
291 292
|
nsyl |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ ( t e. NN /\ ( -. q || t /\ t < x ) ) ) -> -. ( ( q ^ 1 ) || t <-> ( q ^ 1 ) || x ) ) |
294 |
|
oveq1 |
|- ( r = q -> ( r ^ m ) = ( q ^ m ) ) |
295 |
294
|
breq1d |
|- ( r = q -> ( ( r ^ m ) || t <-> ( q ^ m ) || t ) ) |
296 |
294
|
breq1d |
|- ( r = q -> ( ( r ^ m ) || x <-> ( q ^ m ) || x ) ) |
297 |
295 296
|
bibi12d |
|- ( r = q -> ( ( ( r ^ m ) || t <-> ( r ^ m ) || x ) <-> ( ( q ^ m ) || t <-> ( q ^ m ) || x ) ) ) |
298 |
297
|
notbid |
|- ( r = q -> ( -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) <-> -. ( ( q ^ m ) || t <-> ( q ^ m ) || x ) ) ) |
299 |
|
oveq2 |
|- ( m = 1 -> ( q ^ m ) = ( q ^ 1 ) ) |
300 |
299
|
breq1d |
|- ( m = 1 -> ( ( q ^ m ) || t <-> ( q ^ 1 ) || t ) ) |
301 |
299
|
breq1d |
|- ( m = 1 -> ( ( q ^ m ) || x <-> ( q ^ 1 ) || x ) ) |
302 |
300 301
|
bibi12d |
|- ( m = 1 -> ( ( ( q ^ m ) || t <-> ( q ^ m ) || x ) <-> ( ( q ^ 1 ) || t <-> ( q ^ 1 ) || x ) ) ) |
303 |
302
|
notbid |
|- ( m = 1 -> ( -. ( ( q ^ m ) || t <-> ( q ^ m ) || x ) <-> -. ( ( q ^ 1 ) || t <-> ( q ^ 1 ) || x ) ) ) |
304 |
298 303
|
rspc2ev |
|- ( ( q e. Prime /\ 1 e. NN /\ -. ( ( q ^ 1 ) || t <-> ( q ^ 1 ) || x ) ) -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) |
305 |
275 277 293 304
|
syl3anc |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ ( t e. NN /\ ( -. q || t /\ t < x ) ) ) -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) |
306 |
305
|
expr |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ t e. NN ) -> ( ( -. q || t /\ t < x ) -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) |
307 |
306
|
expd |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ t e. NN ) -> ( -. q || t -> ( t < x -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) ) |
308 |
307
|
adantrl |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ ( A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) /\ t e. NN ) ) -> ( -. q || t -> ( t < x -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) ) |
309 |
274 308
|
pm2.61d |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ ( A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) /\ t e. NN ) ) -> ( t < x -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) |
310 |
309
|
expr |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) ) -> ( t e. NN -> ( t < x -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) ) |
311 |
310
|
ralrimiv |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) ) -> A. t e. NN ( t < x -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) ) |
312 |
|
breq1 |
|- ( t = k -> ( t < x <-> k < x ) ) |
313 |
|
breq2 |
|- ( t = k -> ( ( r ^ m ) || t <-> ( r ^ m ) || k ) ) |
314 |
313
|
bibi1d |
|- ( t = k -> ( ( ( r ^ m ) || t <-> ( r ^ m ) || x ) <-> ( ( r ^ m ) || k <-> ( r ^ m ) || x ) ) ) |
315 |
314
|
notbid |
|- ( t = k -> ( -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) <-> -. ( ( r ^ m ) || k <-> ( r ^ m ) || x ) ) ) |
316 |
315
|
2rexbidv |
|- ( t = k -> ( E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) <-> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || k <-> ( r ^ m ) || x ) ) ) |
317 |
253
|
breq1d |
|- ( r = p -> ( ( r ^ m ) || k <-> ( p ^ m ) || k ) ) |
318 |
317 255
|
bibi12d |
|- ( r = p -> ( ( ( r ^ m ) || k <-> ( r ^ m ) || x ) <-> ( ( p ^ m ) || k <-> ( p ^ m ) || x ) ) ) |
319 |
318
|
notbid |
|- ( r = p -> ( -. ( ( r ^ m ) || k <-> ( r ^ m ) || x ) <-> -. ( ( p ^ m ) || k <-> ( p ^ m ) || x ) ) ) |
320 |
241
|
breq1d |
|- ( m = n -> ( ( p ^ m ) || k <-> ( p ^ n ) || k ) ) |
321 |
320 243
|
bibi12d |
|- ( m = n -> ( ( ( p ^ m ) || k <-> ( p ^ m ) || x ) <-> ( ( p ^ n ) || k <-> ( p ^ n ) || x ) ) ) |
322 |
321
|
notbid |
|- ( m = n -> ( -. ( ( p ^ m ) || k <-> ( p ^ m ) || x ) <-> -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) ) ) |
323 |
319 322
|
cbvrex2vw |
|- ( E. r e. Prime E. m e. NN -. ( ( r ^ m ) || k <-> ( r ^ m ) || x ) <-> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) ) |
324 |
316 323
|
syl6bb |
|- ( t = k -> ( E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) <-> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) ) ) |
325 |
312 324
|
imbi12d |
|- ( t = k -> ( ( t < x -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) <-> ( k < x -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) ) ) ) |
326 |
325
|
cbvralvw |
|- ( A. t e. NN ( t < x -> E. r e. Prime E. m e. NN -. ( ( r ^ m ) || t <-> ( r ^ m ) || x ) ) <-> A. k e. NN ( k < x -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) ) ) |
327 |
311 326
|
sylib |
|- ( ( ( x e. ( ZZ>= ` 2 ) /\ q e. Prime /\ q || x ) /\ A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) ) -> A. k e. NN ( k < x -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) ) ) |
328 |
327
|
3exp1 |
|- ( x e. ( ZZ>= ` 2 ) -> ( q e. Prime -> ( q || x -> ( A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) -> A. k e. NN ( k < x -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) ) ) ) ) ) |
329 |
328
|
rexlimdv |
|- ( x e. ( ZZ>= ` 2 ) -> ( E. q e. Prime q || x -> ( A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) -> A. k e. NN ( k < x -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) ) ) ) ) |
330 |
25 329
|
mpd |
|- ( x e. ( ZZ>= ` 2 ) -> ( A. y e. NN ( y < x -> A. k e. NN ( k < y -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || y ) ) ) -> A. k e. NN ( k < x -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) ) ) ) |
331 |
14 21 24 330
|
indstr2 |
|- ( x e. NN -> A. k e. NN ( k < x -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || x ) ) ) |
332 |
7 331
|
vtoclga |
|- ( A e. NN -> A. k e. NN ( k < A -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || A ) ) ) |