Metamath Proof Explorer

Theorem 2pwp1prm

Description: For ( ( 2 ^ k ) + 1 ) to be prime, k must be a power of 2, see Wikipedia "Fermat number", section "Other theorms about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number , 5-Aug-2021. (Contributed by AV, 7-Aug-2021)

Ref Expression
Assertion 2pwp1prm 
|- ( ( K e. NN /\ ( ( 2 ^ K ) + 1 ) e. Prime ) -> E. n e. NN0 K = ( 2 ^ n ) )

Proof

Step Hyp Ref Expression
1 oddprmdvds 
 |-  ( ( K e. NN /\ -. E. n e. NN0 K = ( 2 ^ n ) ) -> E. p e. ( Prime \ { 2 } ) p || K )
2 1 adantlr 
 |-  ( ( ( K e. NN /\ ( ( 2 ^ K ) + 1 ) e. Prime ) /\ -. E. n e. NN0 K = ( 2 ^ n ) ) -> E. p e. ( Prime \ { 2 } ) p || K )
3 eldifi 
 |-  ( p e. ( Prime \ { 2 } ) -> p e. Prime )
4 prmnn 
 |-  ( p e. Prime -> p e. NN )
5 3 4 syl 
 |-  ( p e. ( Prime \ { 2 } ) -> p e. NN )
6 simpl 
 |-  ( ( K e. NN /\ ( ( 2 ^ K ) + 1 ) e. Prime ) -> K e. NN )
7 nndivides 
 |-  ( ( p e. NN /\ K e. NN ) -> ( p || K <-> E. m e. NN ( m x. p ) = K ) )
8 5 6 7 syl2anr 
 |-  ( ( ( K e. NN /\ ( ( 2 ^ K ) + 1 ) e. Prime ) /\ p e. ( Prime \ { 2 } ) ) -> ( p || K <-> E. m e. NN ( m x. p ) = K ) )
9 2re 
 |-  2 e. RR
10 9 a1i 
 |-  ( m e. NN -> 2 e. RR )
11 nnnn0 
 |-  ( m e. NN -> m e. NN0 )
12 1le2 
 |-  1 <_ 2
13 12 a1i 
 |-  ( m e. NN -> 1 <_ 2 )
14 10 11 13 expge1d 
 |-  ( m e. NN -> 1 <_ ( 2 ^ m ) )
15 1zzd 
 |-  ( m e. NN -> 1 e. ZZ )
16 2nn 
 |-  2 e. NN
17 16 a1i 
 |-  ( m e. NN -> 2 e. NN )
18 17 11 nnexpcld 
 |-  ( m e. NN -> ( 2 ^ m ) e. NN )
19 18 nnzd 
 |-  ( m e. NN -> ( 2 ^ m ) e. ZZ )
20 zleltp1 
 |-  ( ( 1 e. ZZ /\ ( 2 ^ m ) e. ZZ ) -> ( 1 <_ ( 2 ^ m ) <-> 1 < ( ( 2 ^ m ) + 1 ) ) )
21 15 19 20 syl2anc 
 |-  ( m e. NN -> ( 1 <_ ( 2 ^ m ) <-> 1 < ( ( 2 ^ m ) + 1 ) ) )
22 14 21 mpbid 
 |-  ( m e. NN -> 1 < ( ( 2 ^ m ) + 1 ) )
23 18 nncnd 
 |-  ( m e. NN -> ( 2 ^ m ) e. CC )
24 1cnd 
 |-  ( m e. NN -> 1 e. CC )
25 subneg 
 |-  ( ( ( 2 ^ m ) e. CC /\ 1 e. CC ) -> ( ( 2 ^ m ) - -u 1 ) = ( ( 2 ^ m ) + 1 ) )
26 25 breq2d 
 |-  ( ( ( 2 ^ m ) e. CC /\ 1 e. CC ) -> ( 1 < ( ( 2 ^ m ) - -u 1 ) <-> 1 < ( ( 2 ^ m ) + 1 ) ) )
27 23 24 26 syl2anc 
 |-  ( m e. NN -> ( 1 < ( ( 2 ^ m ) - -u 1 ) <-> 1 < ( ( 2 ^ m ) + 1 ) ) )
28 22 27 mpbird 
 |-  ( m e. NN -> 1 < ( ( 2 ^ m ) - -u 1 ) )
29 28 adantl 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> 1 < ( ( 2 ^ m ) - -u 1 ) )
30 29 ad2antlr 
 |-  ( ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) /\ ( m x. p ) = K ) -> 1 < ( ( 2 ^ m ) - -u 1 ) )
31 18 nnred 
 |-  ( m e. NN -> ( 2 ^ m ) e. RR )
32 31 adantl 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> ( 2 ^ m ) e. RR )
33 16 a1i 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> 2 e. NN )
34 11 adantl 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> m e. NN0 )
35 5 nnnn0d 
 |-  ( p e. ( Prime \ { 2 } ) -> p e. NN0 )
36 35 adantr 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> p e. NN0 )
37 34 36 nn0mulcld 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> ( m x. p ) e. NN0 )
38 33 37 nnexpcld 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> ( 2 ^ ( m x. p ) ) e. NN )
39 38 nnred 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> ( 2 ^ ( m x. p ) ) e. RR )
40 1red 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> 1 e. RR )
41 9 a1i 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> 2 e. RR )
42 nnz 
 |-  ( m e. NN -> m e. ZZ )
43 42 adantl 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> m e. ZZ )
44 5 nnzd 
 |-  ( p e. ( Prime \ { 2 } ) -> p e. ZZ )
45 44 adantr 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> p e. ZZ )
46 43 45 zmulcld 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> ( m x. p ) e. ZZ )
47 1lt2 
 |-  1 < 2
48 47 a1i 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> 1 < 2 )
49 prmgt1 
 |-  ( p e. Prime -> 1 < p )
50 3 49 syl 
 |-  ( p e. ( Prime \ { 2 } ) -> 1 < p )
51 50 adantr 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> 1 < p )
52 nnre 
 |-  ( m e. NN -> m e. RR )
53 52 adantl 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> m e. RR )
54 5 nnred 
 |-  ( p e. ( Prime \ { 2 } ) -> p e. RR )
55 54 adantr 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> p e. RR )
56 nngt0 
 |-  ( m e. NN -> 0 < m )
57 56 adantl 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> 0 < m )
58 ltmulgt11 
 |-  ( ( m e. RR /\ p e. RR /\ 0 < m ) -> ( 1 < p <-> m < ( m x. p ) ) )
59 53 55 57 58 syl3anc 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> ( 1 < p <-> m < ( m x. p ) ) )
60 51 59 mpbid 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> m < ( m x. p ) )
61 ltexp2a 
 |-  ( ( ( 2 e. RR /\ m e. ZZ /\ ( m x. p ) e. ZZ ) /\ ( 1 < 2 /\ m < ( m x. p ) ) ) -> ( 2 ^ m ) < ( 2 ^ ( m x. p ) ) )
62 41 43 46 48 60 61 syl32anc 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> ( 2 ^ m ) < ( 2 ^ ( m x. p ) ) )
63 32 39 40 62 ltadd1dd 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> ( ( 2 ^ m ) + 1 ) < ( ( 2 ^ ( m x. p ) ) + 1 ) )
64 63 ad2antlr 
 |-  ( ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) /\ ( m x. p ) = K ) -> ( ( 2 ^ m ) + 1 ) < ( ( 2 ^ ( m x. p ) ) + 1 ) )
65 23 24 subnegd 
 |-  ( m e. NN -> ( ( 2 ^ m ) - -u 1 ) = ( ( 2 ^ m ) + 1 ) )
66 65 eqcomd 
 |-  ( m e. NN -> ( ( 2 ^ m ) + 1 ) = ( ( 2 ^ m ) - -u 1 ) )
67 66 adantl 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> ( ( 2 ^ m ) + 1 ) = ( ( 2 ^ m ) - -u 1 ) )
68 67 ad2antlr 
 |-  ( ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) /\ ( m x. p ) = K ) -> ( ( 2 ^ m ) + 1 ) = ( ( 2 ^ m ) - -u 1 ) )
69 oveq2 
 |-  ( ( m x. p ) = K -> ( 2 ^ ( m x. p ) ) = ( 2 ^ K ) )
70 69 oveq1d 
 |-  ( ( m x. p ) = K -> ( ( 2 ^ ( m x. p ) ) + 1 ) = ( ( 2 ^ K ) + 1 ) )
71 70 adantl 
 |-  ( ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) /\ ( m x. p ) = K ) -> ( ( 2 ^ ( m x. p ) ) + 1 ) = ( ( 2 ^ K ) + 1 ) )
72 64 68 71 3brtr3d 
 |-  ( ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) /\ ( m x. p ) = K ) -> ( ( 2 ^ m ) - -u 1 ) < ( ( 2 ^ K ) + 1 ) )
73 neg1z 
 |-  -u 1 e. ZZ
74 73 a1i 
 |-  ( m e. NN -> -u 1 e. ZZ )
75 19 74 zsubcld 
 |-  ( m e. NN -> ( ( 2 ^ m ) - -u 1 ) e. ZZ )
76 75 adantl 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> ( ( 2 ^ m ) - -u 1 ) e. ZZ )
77 fzofi 
 |-  ( 0 ..^ p ) e. Fin
78 77 a1i 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> ( 0 ..^ p ) e. Fin )
79 19 adantl 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> ( 2 ^ m ) e. ZZ )
80 elfzonn0 
 |-  ( k e. ( 0 ..^ p ) -> k e. NN0 )
81 zexpcl 
 |-  ( ( ( 2 ^ m ) e. ZZ /\ k e. NN0 ) -> ( ( 2 ^ m ) ^ k ) e. ZZ )
82 79 80 81 syl2an 
 |-  ( ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) /\ k e. ( 0 ..^ p ) ) -> ( ( 2 ^ m ) ^ k ) e. ZZ )
83 73 a1i 
 |-  ( ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) /\ k e. ( 0 ..^ p ) ) -> -u 1 e. ZZ )
84 fzonnsub 
 |-  ( k e. ( 0 ..^ p ) -> ( p - k ) e. NN )
85 84 adantl 
 |-  ( ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) /\ k e. ( 0 ..^ p ) ) -> ( p - k ) e. NN )
86 nnm1nn0 
 |-  ( ( p - k ) e. NN -> ( ( p - k ) - 1 ) e. NN0 )
87 85 86 syl 
 |-  ( ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) /\ k e. ( 0 ..^ p ) ) -> ( ( p - k ) - 1 ) e. NN0 )
88 zexpcl 
 |-  ( ( -u 1 e. ZZ /\ ( ( p - k ) - 1 ) e. NN0 ) -> ( -u 1 ^ ( ( p - k ) - 1 ) ) e. ZZ )
89 83 87 88 syl2anc 
 |-  ( ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) /\ k e. ( 0 ..^ p ) ) -> ( -u 1 ^ ( ( p - k ) - 1 ) ) e. ZZ )
90 82 89 zmulcld 
 |-  ( ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) /\ k e. ( 0 ..^ p ) ) -> ( ( ( 2 ^ m ) ^ k ) x. ( -u 1 ^ ( ( p - k ) - 1 ) ) ) e. ZZ )
91 78 90 fsumzcl 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> sum_ k e. ( 0 ..^ p ) ( ( ( 2 ^ m ) ^ k ) x. ( -u 1 ^ ( ( p - k ) - 1 ) ) ) e. ZZ )
92 dvdsmul1 
 |-  ( ( ( ( 2 ^ m ) - -u 1 ) e. ZZ /\ sum_ k e. ( 0 ..^ p ) ( ( ( 2 ^ m ) ^ k ) x. ( -u 1 ^ ( ( p - k ) - 1 ) ) ) e. ZZ ) -> ( ( 2 ^ m ) - -u 1 ) || ( ( ( 2 ^ m ) - -u 1 ) x. sum_ k e. ( 0 ..^ p ) ( ( ( 2 ^ m ) ^ k ) x. ( -u 1 ^ ( ( p - k ) - 1 ) ) ) ) )
93 76 91 92 syl2anc 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> ( ( 2 ^ m ) - -u 1 ) || ( ( ( 2 ^ m ) - -u 1 ) x. sum_ k e. ( 0 ..^ p ) ( ( ( 2 ^ m ) ^ k ) x. ( -u 1 ^ ( ( p - k ) - 1 ) ) ) ) )
94 93 ad2antlr 
 |-  ( ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) /\ ( m x. p ) = K ) -> ( ( 2 ^ m ) - -u 1 ) || ( ( ( 2 ^ m ) - -u 1 ) x. sum_ k e. ( 0 ..^ p ) ( ( ( 2 ^ m ) ^ k ) x. ( -u 1 ^ ( ( p - k ) - 1 ) ) ) ) )
95 23 adantl 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> ( 2 ^ m ) e. CC )
96 neg1cn 
 |-  -u 1 e. CC
97 96 a1i 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> -u 1 e. CC )
98 pwdif 
 |-  ( ( p e. NN0 /\ ( 2 ^ m ) e. CC /\ -u 1 e. CC ) -> ( ( ( 2 ^ m ) ^ p ) - ( -u 1 ^ p ) ) = ( ( ( 2 ^ m ) - -u 1 ) x. sum_ k e. ( 0 ..^ p ) ( ( ( 2 ^ m ) ^ k ) x. ( -u 1 ^ ( ( p - k ) - 1 ) ) ) ) )
99 36 95 97 98 syl3anc 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> ( ( ( 2 ^ m ) ^ p ) - ( -u 1 ^ p ) ) = ( ( ( 2 ^ m ) - -u 1 ) x. sum_ k e. ( 0 ..^ p ) ( ( ( 2 ^ m ) ^ k ) x. ( -u 1 ^ ( ( p - k ) - 1 ) ) ) ) )
100 99 breq2d 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> ( ( ( 2 ^ m ) - -u 1 ) || ( ( ( 2 ^ m ) ^ p ) - ( -u 1 ^ p ) ) <-> ( ( 2 ^ m ) - -u 1 ) || ( ( ( 2 ^ m ) - -u 1 ) x. sum_ k e. ( 0 ..^ p ) ( ( ( 2 ^ m ) ^ k ) x. ( -u 1 ^ ( ( p - k ) - 1 ) ) ) ) ) )
101 100 ad2antlr 
 |-  ( ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) /\ ( m x. p ) = K ) -> ( ( ( 2 ^ m ) - -u 1 ) || ( ( ( 2 ^ m ) ^ p ) - ( -u 1 ^ p ) ) <-> ( ( 2 ^ m ) - -u 1 ) || ( ( ( 2 ^ m ) - -u 1 ) x. sum_ k e. ( 0 ..^ p ) ( ( ( 2 ^ m ) ^ k ) x. ( -u 1 ^ ( ( p - k ) - 1 ) ) ) ) ) )
102 94 101 mpbird 
 |-  ( ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) /\ ( m x. p ) = K ) -> ( ( 2 ^ m ) - -u 1 ) || ( ( ( 2 ^ m ) ^ p ) - ( -u 1 ^ p ) ) )
103 2cnd 
 |-  ( K e. NN -> 2 e. CC )
104 nnnn0 
 |-  ( K e. NN -> K e. NN0 )
105 103 104 expcld 
 |-  ( K e. NN -> ( 2 ^ K ) e. CC )
106 1cnd 
 |-  ( K e. NN -> 1 e. CC )
107 105 106 subnegd 
 |-  ( K e. NN -> ( ( 2 ^ K ) - -u 1 ) = ( ( 2 ^ K ) + 1 ) )
108 107 eqcomd 
 |-  ( K e. NN -> ( ( 2 ^ K ) + 1 ) = ( ( 2 ^ K ) - -u 1 ) )
109 108 adantr 
 |-  ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) -> ( ( 2 ^ K ) + 1 ) = ( ( 2 ^ K ) - -u 1 ) )
110 109 adantr 
 |-  ( ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) /\ ( m x. p ) = K ) -> ( ( 2 ^ K ) + 1 ) = ( ( 2 ^ K ) - -u 1 ) )
111 oveq2 
 |-  ( K = ( m x. p ) -> ( 2 ^ K ) = ( 2 ^ ( m x. p ) ) )
112 111 eqcoms 
 |-  ( ( m x. p ) = K -> ( 2 ^ K ) = ( 2 ^ ( m x. p ) ) )
113 112 adantl 
 |-  ( ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) /\ ( m x. p ) = K ) -> ( 2 ^ K ) = ( 2 ^ ( m x. p ) ) )
114 2cnd 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> 2 e. CC )
115 114 36 34 expmuld 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> ( 2 ^ ( m x. p ) ) = ( ( 2 ^ m ) ^ p ) )
116 115 ad2antlr 
 |-  ( ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) /\ ( m x. p ) = K ) -> ( 2 ^ ( m x. p ) ) = ( ( 2 ^ m ) ^ p ) )
117 113 116 eqtrd 
 |-  ( ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) /\ ( m x. p ) = K ) -> ( 2 ^ K ) = ( ( 2 ^ m ) ^ p ) )
118 1exp 
 |-  ( p e. ZZ -> ( 1 ^ p ) = 1 )
119 44 118 syl 
 |-  ( p e. ( Prime \ { 2 } ) -> ( 1 ^ p ) = 1 )
120 119 eqcomd 
 |-  ( p e. ( Prime \ { 2 } ) -> 1 = ( 1 ^ p ) )
121 120 negeqd 
 |-  ( p e. ( Prime \ { 2 } ) -> -u 1 = -u ( 1 ^ p ) )
122 1cnd 
 |-  ( p e. ( Prime \ { 2 } ) -> 1 e. CC )
123 oddn2prm 
 |-  ( p e. ( Prime \ { 2 } ) -> -. 2 || p )
124 oexpneg 
 |-  ( ( 1 e. CC /\ p e. NN /\ -. 2 || p ) -> ( -u 1 ^ p ) = -u ( 1 ^ p ) )
125 122 5 123 124 syl3anc 
 |-  ( p e. ( Prime \ { 2 } ) -> ( -u 1 ^ p ) = -u ( 1 ^ p ) )
126 125 eqcomd 
 |-  ( p e. ( Prime \ { 2 } ) -> -u ( 1 ^ p ) = ( -u 1 ^ p ) )
127 121 126 eqtrd 
 |-  ( p e. ( Prime \ { 2 } ) -> -u 1 = ( -u 1 ^ p ) )
128 127 adantr 
 |-  ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> -u 1 = ( -u 1 ^ p ) )
129 128 ad2antlr 
 |-  ( ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) /\ ( m x. p ) = K ) -> -u 1 = ( -u 1 ^ p ) )
130 117 129 oveq12d 
 |-  ( ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) /\ ( m x. p ) = K ) -> ( ( 2 ^ K ) - -u 1 ) = ( ( ( 2 ^ m ) ^ p ) - ( -u 1 ^ p ) ) )
131 110 130 eqtrd 
 |-  ( ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) /\ ( m x. p ) = K ) -> ( ( 2 ^ K ) + 1 ) = ( ( ( 2 ^ m ) ^ p ) - ( -u 1 ^ p ) ) )
132 131 breq2d 
 |-  ( ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) /\ ( m x. p ) = K ) -> ( ( ( 2 ^ m ) - -u 1 ) || ( ( 2 ^ K ) + 1 ) <-> ( ( 2 ^ m ) - -u 1 ) || ( ( ( 2 ^ m ) ^ p ) - ( -u 1 ^ p ) ) ) )
133 102 132 mpbird 
 |-  ( ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) /\ ( m x. p ) = K ) -> ( ( 2 ^ m ) - -u 1 ) || ( ( 2 ^ K ) + 1 ) )
134 30 72 133 dvdsnprmd 
 |-  ( ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) /\ ( m x. p ) = K ) -> -. ( ( 2 ^ K ) + 1 ) e. Prime )
135 134 pm2.21d 
 |-  ( ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) /\ ( m x. p ) = K ) -> ( ( ( 2 ^ K ) + 1 ) e. Prime -> E. n e. NN0 K = ( 2 ^ n ) ) )
136 135 ex 
 |-  ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) -> ( ( m x. p ) = K -> ( ( ( 2 ^ K ) + 1 ) e. Prime -> E. n e. NN0 K = ( 2 ^ n ) ) ) )
137 136 com23 
 |-  ( ( K e. NN /\ ( p e. ( Prime \ { 2 } ) /\ m e. NN ) ) -> ( ( ( 2 ^ K ) + 1 ) e. Prime -> ( ( m x. p ) = K -> E. n e. NN0 K = ( 2 ^ n ) ) ) )
138 137 impancom 
 |-  ( ( K e. NN /\ ( ( 2 ^ K ) + 1 ) e. Prime ) -> ( ( p e. ( Prime \ { 2 } ) /\ m e. NN ) -> ( ( m x. p ) = K -> E. n e. NN0 K = ( 2 ^ n ) ) ) )
139 138 impl 
 |-  ( ( ( ( K e. NN /\ ( ( 2 ^ K ) + 1 ) e. Prime ) /\ p e. ( Prime \ { 2 } ) ) /\ m e. NN ) -> ( ( m x. p ) = K -> E. n e. NN0 K = ( 2 ^ n ) ) )
140 139 rexlimdva 
 |-  ( ( ( K e. NN /\ ( ( 2 ^ K ) + 1 ) e. Prime ) /\ p e. ( Prime \ { 2 } ) ) -> ( E. m e. NN ( m x. p ) = K -> E. n e. NN0 K = ( 2 ^ n ) ) )
141 8 140 sylbid 
 |-  ( ( ( K e. NN /\ ( ( 2 ^ K ) + 1 ) e. Prime ) /\ p e. ( Prime \ { 2 } ) ) -> ( p || K -> E. n e. NN0 K = ( 2 ^ n ) ) )
142 141 rexlimdva 
 |-  ( ( K e. NN /\ ( ( 2 ^ K ) + 1 ) e. Prime ) -> ( E. p e. ( Prime \ { 2 } ) p || K -> E. n e. NN0 K = ( 2 ^ n ) ) )
143 142 adantr 
 |-  ( ( ( K e. NN /\ ( ( 2 ^ K ) + 1 ) e. Prime ) /\ -. E. n e. NN0 K = ( 2 ^ n ) ) -> ( E. p e. ( Prime \ { 2 } ) p || K -> E. n e. NN0 K = ( 2 ^ n ) ) )
144 2 143 mpd 
 |-  ( ( ( K e. NN /\ ( ( 2 ^ K ) + 1 ) e. Prime ) /\ -. E. n e. NN0 K = ( 2 ^ n ) ) -> E. n e. NN0 K = ( 2 ^ n ) )
145 144 pm2.18da 
 |-  ( ( K e. NN /\ ( ( 2 ^ K ) + 1 ) e. Prime ) -> E. n e. NN0 K = ( 2 ^ n ) )