Metamath Proof Explorer

Theorem nn0prpwlem

Description: Lemma for nn0prpw . Use strong induction to show that every positive integer has unique prime power divisors. (Contributed by Jeff Hankins, 28-Sep-2013)

Ref Expression
Assertion nn0prpwlem 
|- ( A e. NN -> A. k e. NN ( k < A -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || A ) ) )

Proof

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