Metamath Proof Explorer

Theorem oddprmdvds

Description: Every positive integer which is not a power of two is divisible by an odd prime number. (Contributed by AV, 6-Aug-2021)

Ref Expression
Assertion oddprmdvds 
|- ( ( K e. NN /\ -. E. n e. NN0 K = ( 2 ^ n ) ) -> E. p e. ( Prime \ { 2 } ) p || K )

Proof

Step Hyp Ref Expression
1 2prm 
 |-  2 e. Prime
2 pcndvds2 
 |-  ( ( 2 e. Prime /\ K e. NN ) -> -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) )
3 1 2 mpan 
 |-  ( K e. NN -> -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) )
4 pcdvds 
 |-  ( ( 2 e. Prime /\ K e. NN ) -> ( 2 ^ ( 2 pCnt K ) ) || K )
5 1 4 mpan 
 |-  ( K e. NN -> ( 2 ^ ( 2 pCnt K ) ) || K )
6 2nn 
 |-  2 e. NN
7 6 a1i 
 |-  ( K e. NN -> 2 e. NN )
8 1 a1i 
 |-  ( K e. NN -> 2 e. Prime )
9 id 
 |-  ( K e. NN -> K e. NN )
10 8 9 pccld 
 |-  ( K e. NN -> ( 2 pCnt K ) e. NN0 )
11 7 10 nnexpcld 
 |-  ( K e. NN -> ( 2 ^ ( 2 pCnt K ) ) e. NN )
12 nndivdvds 
 |-  ( ( K e. NN /\ ( 2 ^ ( 2 pCnt K ) ) e. NN ) -> ( ( 2 ^ ( 2 pCnt K ) ) || K <-> ( K / ( 2 ^ ( 2 pCnt K ) ) ) e. NN ) )
13 11 12 mpdan 
 |-  ( K e. NN -> ( ( 2 ^ ( 2 pCnt K ) ) || K <-> ( K / ( 2 ^ ( 2 pCnt K ) ) ) e. NN ) )
14 13 adantr 
 |-  ( ( K e. NN /\ -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) ) -> ( ( 2 ^ ( 2 pCnt K ) ) || K <-> ( K / ( 2 ^ ( 2 pCnt K ) ) ) e. NN ) )
15 elnn1uz2 
 |-  ( ( K / ( 2 ^ ( 2 pCnt K ) ) ) e. NN <-> ( ( K / ( 2 ^ ( 2 pCnt K ) ) ) = 1 \/ ( K / ( 2 ^ ( 2 pCnt K ) ) ) e. ( ZZ>= ` 2 ) ) )
16 nncn 
 |-  ( K e. NN -> K e. CC )
17 nncn 
 |-  ( ( 2 ^ ( 2 pCnt K ) ) e. NN -> ( 2 ^ ( 2 pCnt K ) ) e. CC )
18 nnne0 
 |-  ( ( 2 ^ ( 2 pCnt K ) ) e. NN -> ( 2 ^ ( 2 pCnt K ) ) =/= 0 )
19 17 18 jca 
 |-  ( ( 2 ^ ( 2 pCnt K ) ) e. NN -> ( ( 2 ^ ( 2 pCnt K ) ) e. CC /\ ( 2 ^ ( 2 pCnt K ) ) =/= 0 ) )
20 11 19 syl 
 |-  ( K e. NN -> ( ( 2 ^ ( 2 pCnt K ) ) e. CC /\ ( 2 ^ ( 2 pCnt K ) ) =/= 0 ) )
21 3anass 
 |-  ( ( K e. CC /\ ( 2 ^ ( 2 pCnt K ) ) e. CC /\ ( 2 ^ ( 2 pCnt K ) ) =/= 0 ) <-> ( K e. CC /\ ( ( 2 ^ ( 2 pCnt K ) ) e. CC /\ ( 2 ^ ( 2 pCnt K ) ) =/= 0 ) ) )
22 16 20 21 sylanbrc 
 |-  ( K e. NN -> ( K e. CC /\ ( 2 ^ ( 2 pCnt K ) ) e. CC /\ ( 2 ^ ( 2 pCnt K ) ) =/= 0 ) )
23 22 adantr 
 |-  ( ( K e. NN /\ -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) ) -> ( K e. CC /\ ( 2 ^ ( 2 pCnt K ) ) e. CC /\ ( 2 ^ ( 2 pCnt K ) ) =/= 0 ) )
24 diveq1 
 |-  ( ( K e. CC /\ ( 2 ^ ( 2 pCnt K ) ) e. CC /\ ( 2 ^ ( 2 pCnt K ) ) =/= 0 ) -> ( ( K / ( 2 ^ ( 2 pCnt K ) ) ) = 1 <-> K = ( 2 ^ ( 2 pCnt K ) ) ) )
25 23 24 syl 
 |-  ( ( K e. NN /\ -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) ) -> ( ( K / ( 2 ^ ( 2 pCnt K ) ) ) = 1 <-> K = ( 2 ^ ( 2 pCnt K ) ) ) )
26 10 adantr 
 |-  ( ( K e. NN /\ K = ( 2 ^ ( 2 pCnt K ) ) ) -> ( 2 pCnt K ) e. NN0 )
27 oveq2 
 |-  ( n = ( 2 pCnt K ) -> ( 2 ^ n ) = ( 2 ^ ( 2 pCnt K ) ) )
28 27 eqeq2d 
 |-  ( n = ( 2 pCnt K ) -> ( K = ( 2 ^ n ) <-> K = ( 2 ^ ( 2 pCnt K ) ) ) )
29 28 adantl 
 |-  ( ( ( K e. NN /\ K = ( 2 ^ ( 2 pCnt K ) ) ) /\ n = ( 2 pCnt K ) ) -> ( K = ( 2 ^ n ) <-> K = ( 2 ^ ( 2 pCnt K ) ) ) )
30 simpr 
 |-  ( ( K e. NN /\ K = ( 2 ^ ( 2 pCnt K ) ) ) -> K = ( 2 ^ ( 2 pCnt K ) ) )
31 26 29 30 rspcedvd 
 |-  ( ( K e. NN /\ K = ( 2 ^ ( 2 pCnt K ) ) ) -> E. n e. NN0 K = ( 2 ^ n ) )
32 31 ex 
 |-  ( K e. NN -> ( K = ( 2 ^ ( 2 pCnt K ) ) -> E. n e. NN0 K = ( 2 ^ n ) ) )
33 pm2.24 
 |-  ( E. n e. NN0 K = ( 2 ^ n ) -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) )
34 32 33 syl6 
 |-  ( K e. NN -> ( K = ( 2 ^ ( 2 pCnt K ) ) -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) ) )
35 34 adantr 
 |-  ( ( K e. NN /\ -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) ) -> ( K = ( 2 ^ ( 2 pCnt K ) ) -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) ) )
36 25 35 sylbid 
 |-  ( ( K e. NN /\ -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) ) -> ( ( K / ( 2 ^ ( 2 pCnt K ) ) ) = 1 -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) ) )
37 36 com12 
 |-  ( ( K / ( 2 ^ ( 2 pCnt K ) ) ) = 1 -> ( ( K e. NN /\ -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) ) -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) ) )
38 exprmfct 
 |-  ( ( K / ( 2 ^ ( 2 pCnt K ) ) ) e. ( ZZ>= ` 2 ) -> E. q e. Prime q || ( K / ( 2 ^ ( 2 pCnt K ) ) ) )
39 breq1 
 |-  ( q = 2 -> ( q || ( K / ( 2 ^ ( 2 pCnt K ) ) ) <-> 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) ) )
40 39 biimpcd 
 |-  ( q || ( K / ( 2 ^ ( 2 pCnt K ) ) ) -> ( q = 2 -> 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) ) )
41 40 adantl 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ q || ( K / ( 2 ^ ( 2 pCnt K ) ) ) ) -> ( q = 2 -> 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) ) )
42 41 necon3bd 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ q || ( K / ( 2 ^ ( 2 pCnt K ) ) ) ) -> ( -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) -> q =/= 2 ) )
43 42 ex 
 |-  ( ( K e. NN /\ q e. Prime ) -> ( q || ( K / ( 2 ^ ( 2 pCnt K ) ) ) -> ( -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) -> q =/= 2 ) ) )
44 prmnn 
 |-  ( q e. Prime -> q e. NN )
45 5 13 mpbid 
 |-  ( K e. NN -> ( K / ( 2 ^ ( 2 pCnt K ) ) ) e. NN )
46 nndivides 
 |-  ( ( q e. NN /\ ( K / ( 2 ^ ( 2 pCnt K ) ) ) e. NN ) -> ( q || ( K / ( 2 ^ ( 2 pCnt K ) ) ) <-> E. m e. NN ( m x. q ) = ( K / ( 2 ^ ( 2 pCnt K ) ) ) ) )
47 44 45 46 syl2anr 
 |-  ( ( K e. NN /\ q e. Prime ) -> ( q || ( K / ( 2 ^ ( 2 pCnt K ) ) ) <-> E. m e. NN ( m x. q ) = ( K / ( 2 ^ ( 2 pCnt K ) ) ) ) )
48 eqcom 
 |-  ( ( m x. q ) = ( K / ( 2 ^ ( 2 pCnt K ) ) ) <-> ( K / ( 2 ^ ( 2 pCnt K ) ) ) = ( m x. q ) )
49 16 ad2antrr 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> K e. CC )
50 simpr 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> m e. NN )
51 44 ad2antlr 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> q e. NN )
52 50 51 nnmulcld 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> ( m x. q ) e. NN )
53 52 nncnd 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> ( m x. q ) e. CC )
54 11 ad2antrr 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> ( 2 ^ ( 2 pCnt K ) ) e. NN )
55 54 19 syl 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> ( ( 2 ^ ( 2 pCnt K ) ) e. CC /\ ( 2 ^ ( 2 pCnt K ) ) =/= 0 ) )
56 divmul 
 |-  ( ( K e. CC /\ ( m x. q ) e. CC /\ ( ( 2 ^ ( 2 pCnt K ) ) e. CC /\ ( 2 ^ ( 2 pCnt K ) ) =/= 0 ) ) -> ( ( K / ( 2 ^ ( 2 pCnt K ) ) ) = ( m x. q ) <-> ( ( 2 ^ ( 2 pCnt K ) ) x. ( m x. q ) ) = K ) )
57 49 53 55 56 syl3anc 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> ( ( K / ( 2 ^ ( 2 pCnt K ) ) ) = ( m x. q ) <-> ( ( 2 ^ ( 2 pCnt K ) ) x. ( m x. q ) ) = K ) )
58 48 57 bitrid 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> ( ( m x. q ) = ( K / ( 2 ^ ( 2 pCnt K ) ) ) <-> ( ( 2 ^ ( 2 pCnt K ) ) x. ( m x. q ) ) = K ) )
59 simpr 
 |-  ( ( K e. NN /\ q e. Prime ) -> q e. Prime )
60 59 adantr 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> q e. Prime )
61 60 anim1i 
 |-  ( ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) /\ q =/= 2 ) -> ( q e. Prime /\ q =/= 2 ) )
62 eldifsn 
 |-  ( q e. ( Prime \ { 2 } ) <-> ( q e. Prime /\ q =/= 2 ) )
63 61 62 sylibr 
 |-  ( ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) /\ q =/= 2 ) -> q e. ( Prime \ { 2 } ) )
64 63 adantr 
 |-  ( ( ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) /\ q =/= 2 ) /\ ( ( 2 ^ ( 2 pCnt K ) ) x. ( m x. q ) ) = K ) -> q e. ( Prime \ { 2 } ) )
65 breq1 
 |-  ( p = q -> ( p || K <-> q || K ) )
66 65 adantl 
 |-  ( ( ( ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) /\ q =/= 2 ) /\ ( ( 2 ^ ( 2 pCnt K ) ) x. ( m x. q ) ) = K ) /\ p = q ) -> ( p || K <-> q || K ) )
67 54 50 nnmulcld 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> ( ( 2 ^ ( 2 pCnt K ) ) x. m ) e. NN )
68 67 nnzd 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> ( ( 2 ^ ( 2 pCnt K ) ) x. m ) e. ZZ )
69 44 nnzd 
 |-  ( q e. Prime -> q e. ZZ )
70 69 ad2antlr 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> q e. ZZ )
71 68 70 jca 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> ( ( ( 2 ^ ( 2 pCnt K ) ) x. m ) e. ZZ /\ q e. ZZ ) )
72 71 adantr 
 |-  ( ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) /\ q =/= 2 ) -> ( ( ( 2 ^ ( 2 pCnt K ) ) x. m ) e. ZZ /\ q e. ZZ ) )
73 dvdsmul2 
 |-  ( ( ( ( 2 ^ ( 2 pCnt K ) ) x. m ) e. ZZ /\ q e. ZZ ) -> q || ( ( ( 2 ^ ( 2 pCnt K ) ) x. m ) x. q ) )
74 72 73 syl 
 |-  ( ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) /\ q =/= 2 ) -> q || ( ( ( 2 ^ ( 2 pCnt K ) ) x. m ) x. q ) )
75 2nn0 
 |-  2 e. NN0
76 75 a1i 
 |-  ( K e. NN -> 2 e. NN0 )
77 76 10 nn0expcld 
 |-  ( K e. NN -> ( 2 ^ ( 2 pCnt K ) ) e. NN0 )
78 77 ad2antrr 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> ( 2 ^ ( 2 pCnt K ) ) e. NN0 )
79 78 nn0cnd 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> ( 2 ^ ( 2 pCnt K ) ) e. CC )
80 nncn 
 |-  ( m e. NN -> m e. CC )
81 80 adantl 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> m e. CC )
82 44 nncnd 
 |-  ( q e. Prime -> q e. CC )
83 82 ad2antlr 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> q e. CC )
84 79 81 83 3jca 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> ( ( 2 ^ ( 2 pCnt K ) ) e. CC /\ m e. CC /\ q e. CC ) )
85 84 adantr 
 |-  ( ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) /\ q =/= 2 ) -> ( ( 2 ^ ( 2 pCnt K ) ) e. CC /\ m e. CC /\ q e. CC ) )
86 mulass 
 |-  ( ( ( 2 ^ ( 2 pCnt K ) ) e. CC /\ m e. CC /\ q e. CC ) -> ( ( ( 2 ^ ( 2 pCnt K ) ) x. m ) x. q ) = ( ( 2 ^ ( 2 pCnt K ) ) x. ( m x. q ) ) )
87 85 86 syl 
 |-  ( ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) /\ q =/= 2 ) -> ( ( ( 2 ^ ( 2 pCnt K ) ) x. m ) x. q ) = ( ( 2 ^ ( 2 pCnt K ) ) x. ( m x. q ) ) )
88 74 87 breqtrd 
 |-  ( ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) /\ q =/= 2 ) -> q || ( ( 2 ^ ( 2 pCnt K ) ) x. ( m x. q ) ) )
89 88 adantr 
 |-  ( ( ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) /\ q =/= 2 ) /\ ( ( 2 ^ ( 2 pCnt K ) ) x. ( m x. q ) ) = K ) -> q || ( ( 2 ^ ( 2 pCnt K ) ) x. ( m x. q ) ) )
90 breq2 
 |-  ( ( ( 2 ^ ( 2 pCnt K ) ) x. ( m x. q ) ) = K -> ( q || ( ( 2 ^ ( 2 pCnt K ) ) x. ( m x. q ) ) <-> q || K ) )
91 90 adantl 
 |-  ( ( ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) /\ q =/= 2 ) /\ ( ( 2 ^ ( 2 pCnt K ) ) x. ( m x. q ) ) = K ) -> ( q || ( ( 2 ^ ( 2 pCnt K ) ) x. ( m x. q ) ) <-> q || K ) )
92 89 91 mpbid 
 |-  ( ( ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) /\ q =/= 2 ) /\ ( ( 2 ^ ( 2 pCnt K ) ) x. ( m x. q ) ) = K ) -> q || K )
93 64 66 92 rspcedvd 
 |-  ( ( ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) /\ q =/= 2 ) /\ ( ( 2 ^ ( 2 pCnt K ) ) x. ( m x. q ) ) = K ) -> E. p e. ( Prime \ { 2 } ) p || K )
94 93 a1d 
 |-  ( ( ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) /\ q =/= 2 ) /\ ( ( 2 ^ ( 2 pCnt K ) ) x. ( m x. q ) ) = K ) -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) )
95 94 exp31 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> ( q =/= 2 -> ( ( ( 2 ^ ( 2 pCnt K ) ) x. ( m x. q ) ) = K -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) ) ) )
96 95 com23 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> ( ( ( 2 ^ ( 2 pCnt K ) ) x. ( m x. q ) ) = K -> ( q =/= 2 -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) ) ) )
97 58 96 sylbid 
 |-  ( ( ( K e. NN /\ q e. Prime ) /\ m e. NN ) -> ( ( m x. q ) = ( K / ( 2 ^ ( 2 pCnt K ) ) ) -> ( q =/= 2 -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) ) ) )
98 97 rexlimdva 
 |-  ( ( K e. NN /\ q e. Prime ) -> ( E. m e. NN ( m x. q ) = ( K / ( 2 ^ ( 2 pCnt K ) ) ) -> ( q =/= 2 -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) ) ) )
99 47 98 sylbid 
 |-  ( ( K e. NN /\ q e. Prime ) -> ( q || ( K / ( 2 ^ ( 2 pCnt K ) ) ) -> ( q =/= 2 -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) ) ) )
100 43 99 syldd 
 |-  ( ( K e. NN /\ q e. Prime ) -> ( q || ( K / ( 2 ^ ( 2 pCnt K ) ) ) -> ( -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) ) ) )
101 100 rexlimdva 
 |-  ( K e. NN -> ( E. q e. Prime q || ( K / ( 2 ^ ( 2 pCnt K ) ) ) -> ( -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) ) ) )
102 101 com12 
 |-  ( E. q e. Prime q || ( K / ( 2 ^ ( 2 pCnt K ) ) ) -> ( K e. NN -> ( -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) ) ) )
103 102 impd 
 |-  ( E. q e. Prime q || ( K / ( 2 ^ ( 2 pCnt K ) ) ) -> ( ( K e. NN /\ -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) ) -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) ) )
104 38 103 syl 
 |-  ( ( K / ( 2 ^ ( 2 pCnt K ) ) ) e. ( ZZ>= ` 2 ) -> ( ( K e. NN /\ -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) ) -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) ) )
105 37 104 jaoi 
 |-  ( ( ( K / ( 2 ^ ( 2 pCnt K ) ) ) = 1 \/ ( K / ( 2 ^ ( 2 pCnt K ) ) ) e. ( ZZ>= ` 2 ) ) -> ( ( K e. NN /\ -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) ) -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) ) )
106 15 105 sylbi 
 |-  ( ( K / ( 2 ^ ( 2 pCnt K ) ) ) e. NN -> ( ( K e. NN /\ -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) ) -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) ) )
107 106 com12 
 |-  ( ( K e. NN /\ -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) ) -> ( ( K / ( 2 ^ ( 2 pCnt K ) ) ) e. NN -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) ) )
108 14 107 sylbid 
 |-  ( ( K e. NN /\ -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) ) -> ( ( 2 ^ ( 2 pCnt K ) ) || K -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) ) )
109 108 ex 
 |-  ( K e. NN -> ( -. 2 || ( K / ( 2 ^ ( 2 pCnt K ) ) ) -> ( ( 2 ^ ( 2 pCnt K ) ) || K -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) ) ) )
110 3 5 109 mp2d 
 |-  ( K e. NN -> ( -. E. n e. NN0 K = ( 2 ^ n ) -> E. p e. ( Prime \ { 2 } ) p || K ) )
111 110 imp 
 |-  ( ( K e. NN /\ -. E. n e. NN0 K = ( 2 ^ n ) ) -> E. p e. ( Prime \ { 2 } ) p || K )