Metamath Proof Explorer

Theorem prmind2

Description: A variation on prmind assuming complete induction for primes. (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypotheses prmind.1 
|- ( x = 1 -> ( ph <-> ps ) )
prmind.2 
|- ( x = y -> ( ph <-> ch ) )
prmind.3 
|- ( x = z -> ( ph <-> th ) )
prmind.4 
|- ( x = ( y x. z ) -> ( ph <-> ta ) )
prmind.5 
|- ( x = A -> ( ph <-> et ) )
prmind.6 
|- ps
prmind2.7 
|- ( ( x e. Prime /\ A. y e. ( 1 ... ( x - 1 ) ) ch ) -> ph )
prmind2.8 
|- ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( ( ch /\ th ) -> ta ) )
Assertion prmind2 
|- ( A e. NN -> et )

Proof

Step Hyp Ref Expression
1 prmind.1 
 |-  ( x = 1 -> ( ph <-> ps ) )
2 prmind.2 
 |-  ( x = y -> ( ph <-> ch ) )
3 prmind.3 
 |-  ( x = z -> ( ph <-> th ) )
4 prmind.4 
 |-  ( x = ( y x. z ) -> ( ph <-> ta ) )
5 prmind.5 
 |-  ( x = A -> ( ph <-> et ) )
6 prmind.6 
 |-  ps
7 prmind2.7 
 |-  ( ( x e. Prime /\ A. y e. ( 1 ... ( x - 1 ) ) ch ) -> ph )
8 prmind2.8 
 |-  ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( ( ch /\ th ) -> ta ) )
9 oveq2 
 |-  ( n = 1 -> ( 1 ... n ) = ( 1 ... 1 ) )
10 9 raleqdv 
 |-  ( n = 1 -> ( A. x e. ( 1 ... n ) ph <-> A. x e. ( 1 ... 1 ) ph ) )
11 oveq2 
 |-  ( n = k -> ( 1 ... n ) = ( 1 ... k ) )
12 11 raleqdv 
 |-  ( n = k -> ( A. x e. ( 1 ... n ) ph <-> A. x e. ( 1 ... k ) ph ) )
13 oveq2 
 |-  ( n = ( k + 1 ) -> ( 1 ... n ) = ( 1 ... ( k + 1 ) ) )
14 13 raleqdv 
 |-  ( n = ( k + 1 ) -> ( A. x e. ( 1 ... n ) ph <-> A. x e. ( 1 ... ( k + 1 ) ) ph ) )
15 oveq2 
 |-  ( n = A -> ( 1 ... n ) = ( 1 ... A ) )
16 15 raleqdv 
 |-  ( n = A -> ( A. x e. ( 1 ... n ) ph <-> A. x e. ( 1 ... A ) ph ) )
17 elfz1eq 
 |-  ( x e. ( 1 ... 1 ) -> x = 1 )
18 17 1 syl 
 |-  ( x e. ( 1 ... 1 ) -> ( ph <-> ps ) )
19 6 18 mpbiri 
 |-  ( x e. ( 1 ... 1 ) -> ph )
20 19 rgen 
 |-  A. x e. ( 1 ... 1 ) ph
21 peano2nn 
 |-  ( k e. NN -> ( k + 1 ) e. NN )
22 21 ad2antrr 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( k + 1 ) e. NN )
23 22 nncnd 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( k + 1 ) e. CC )
24 elfzuz 
 |-  ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) -> y e. ( ZZ>= ` 2 ) )
25 24 ad2antrl 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> y e. ( ZZ>= ` 2 ) )
26 eluz2nn 
 |-  ( y e. ( ZZ>= ` 2 ) -> y e. NN )
27 25 26 syl 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> y e. NN )
28 27 nncnd 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> y e. CC )
29 27 nnne0d 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> y =/= 0 )
30 23 28 29 divcan2d 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( y x. ( ( k + 1 ) / y ) ) = ( k + 1 ) )
31 simprr 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> y || ( k + 1 ) )
32 27 nnzd 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> y e. ZZ )
33 22 nnzd 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( k + 1 ) e. ZZ )
34 dvdsval2 
 |-  ( ( y e. ZZ /\ y =/= 0 /\ ( k + 1 ) e. ZZ ) -> ( y || ( k + 1 ) <-> ( ( k + 1 ) / y ) e. ZZ ) )
35 32 29 33 34 syl3anc 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( y || ( k + 1 ) <-> ( ( k + 1 ) / y ) e. ZZ ) )
36 31 35 mpbid 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( ( k + 1 ) / y ) e. ZZ )
37 28 mulid2d 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( 1 x. y ) = y )
38 elfzle2 
 |-  ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) -> y <_ ( ( k + 1 ) - 1 ) )
39 38 ad2antrl 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> y <_ ( ( k + 1 ) - 1 ) )
40 nncn 
 |-  ( k e. NN -> k e. CC )
41 40 ad2antrr 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> k e. CC )
42 ax-1cn 
 |-  1 e. CC
43 pncan 
 |-  ( ( k e. CC /\ 1 e. CC ) -> ( ( k + 1 ) - 1 ) = k )
44 41 42 43 sylancl 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( ( k + 1 ) - 1 ) = k )
45 39 44 breqtrd 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> y <_ k )
46 nnz 
 |-  ( k e. NN -> k e. ZZ )
47 46 ad2antrr 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> k e. ZZ )
48 zleltp1 
 |-  ( ( y e. ZZ /\ k e. ZZ ) -> ( y <_ k <-> y < ( k + 1 ) ) )
49 32 47 48 syl2anc 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( y <_ k <-> y < ( k + 1 ) ) )
50 45 49 mpbid 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> y < ( k + 1 ) )
51 37 50 eqbrtrd 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( 1 x. y ) < ( k + 1 ) )
52 1red 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> 1 e. RR )
53 22 nnred 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( k + 1 ) e. RR )
54 27 nnred 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> y e. RR )
55 27 nngt0d 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> 0 < y )
56 ltmuldiv 
 |-  ( ( 1 e. RR /\ ( k + 1 ) e. RR /\ ( y e. RR /\ 0 < y ) ) -> ( ( 1 x. y ) < ( k + 1 ) <-> 1 < ( ( k + 1 ) / y ) ) )
57 52 53 54 55 56 syl112anc 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( ( 1 x. y ) < ( k + 1 ) <-> 1 < ( ( k + 1 ) / y ) ) )
58 51 57 mpbid 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> 1 < ( ( k + 1 ) / y ) )
59 eluz2b1 
 |-  ( ( ( k + 1 ) / y ) e. ( ZZ>= ` 2 ) <-> ( ( ( k + 1 ) / y ) e. ZZ /\ 1 < ( ( k + 1 ) / y ) ) )
60 36 58 59 sylanbrc 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( ( k + 1 ) / y ) e. ( ZZ>= ` 2 ) )
61 simplr 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> A. x e. ( 1 ... k ) ph )
62 fznn 
 |-  ( k e. ZZ -> ( y e. ( 1 ... k ) <-> ( y e. NN /\ y <_ k ) ) )
63 47 62 syl 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( y e. ( 1 ... k ) <-> ( y e. NN /\ y <_ k ) ) )
64 27 45 63 mpbir2and 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> y e. ( 1 ... k ) )
65 2 61 64 rspcdva 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ch )
66 vex 
 |-  z e. _V
67 66 3 sbcie 
 |-  ( [. z / x ]. ph <-> th )
68 dfsbcq 
 |-  ( z = ( ( k + 1 ) / y ) -> ( [. z / x ]. ph <-> [. ( ( k + 1 ) / y ) / x ]. ph ) )
69 67 68 bitr3id 
 |-  ( z = ( ( k + 1 ) / y ) -> ( th <-> [. ( ( k + 1 ) / y ) / x ]. ph ) )
70 3 cbvralvw 
 |-  ( A. x e. ( 1 ... k ) ph <-> A. z e. ( 1 ... k ) th )
71 61 70 sylib 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> A. z e. ( 1 ... k ) th )
72 22 nnrpd 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( k + 1 ) e. RR+ )
73 27 nnrpd 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> y e. RR+ )
74 72 73 rpdivcld 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( ( k + 1 ) / y ) e. RR+ )
75 74 rpgt0d 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> 0 < ( ( k + 1 ) / y ) )
76 elnnz 
 |-  ( ( ( k + 1 ) / y ) e. NN <-> ( ( ( k + 1 ) / y ) e. ZZ /\ 0 < ( ( k + 1 ) / y ) ) )
77 36 75 76 sylanbrc 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( ( k + 1 ) / y ) e. NN )
78 22 nnne0d 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( k + 1 ) =/= 0 )
79 23 78 dividd 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( ( k + 1 ) / ( k + 1 ) ) = 1 )
80 eluz2gt1 
 |-  ( y e. ( ZZ>= ` 2 ) -> 1 < y )
81 25 80 syl 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> 1 < y )
82 79 81 eqbrtrd 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( ( k + 1 ) / ( k + 1 ) ) < y )
83 22 nngt0d 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> 0 < ( k + 1 ) )
84 ltdiv23 
 |-  ( ( ( k + 1 ) e. RR /\ ( ( k + 1 ) e. RR /\ 0 < ( k + 1 ) ) /\ ( y e. RR /\ 0 < y ) ) -> ( ( ( k + 1 ) / ( k + 1 ) ) < y <-> ( ( k + 1 ) / y ) < ( k + 1 ) ) )
85 53 53 83 54 55 84 syl122anc 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( ( ( k + 1 ) / ( k + 1 ) ) < y <-> ( ( k + 1 ) / y ) < ( k + 1 ) ) )
86 82 85 mpbid 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( ( k + 1 ) / y ) < ( k + 1 ) )
87 zleltp1 
 |-  ( ( ( ( k + 1 ) / y ) e. ZZ /\ k e. ZZ ) -> ( ( ( k + 1 ) / y ) <_ k <-> ( ( k + 1 ) / y ) < ( k + 1 ) ) )
88 36 47 87 syl2anc 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( ( ( k + 1 ) / y ) <_ k <-> ( ( k + 1 ) / y ) < ( k + 1 ) ) )
89 86 88 mpbird 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( ( k + 1 ) / y ) <_ k )
90 fznn 
 |-  ( k e. ZZ -> ( ( ( k + 1 ) / y ) e. ( 1 ... k ) <-> ( ( ( k + 1 ) / y ) e. NN /\ ( ( k + 1 ) / y ) <_ k ) ) )
91 47 90 syl 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( ( ( k + 1 ) / y ) e. ( 1 ... k ) <-> ( ( ( k + 1 ) / y ) e. NN /\ ( ( k + 1 ) / y ) <_ k ) ) )
92 77 89 91 mpbir2and 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( ( k + 1 ) / y ) e. ( 1 ... k ) )
93 69 71 92 rspcdva 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> [. ( ( k + 1 ) / y ) / x ]. ph )
94 65 93 jca 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> ( ch /\ [. ( ( k + 1 ) / y ) / x ]. ph ) )
95 69 anbi2d 
 |-  ( z = ( ( k + 1 ) / y ) -> ( ( ch /\ th ) <-> ( ch /\ [. ( ( k + 1 ) / y ) / x ]. ph ) ) )
96 ovex 
 |-  ( y x. z ) e. _V
97 96 4 sbcie 
 |-  ( [. ( y x. z ) / x ]. ph <-> ta )
98 oveq2 
 |-  ( z = ( ( k + 1 ) / y ) -> ( y x. z ) = ( y x. ( ( k + 1 ) / y ) ) )
99 98 sbceq1d 
 |-  ( z = ( ( k + 1 ) / y ) -> ( [. ( y x. z ) / x ]. ph <-> [. ( y x. ( ( k + 1 ) / y ) ) / x ]. ph ) )
100 97 99 bitr3id 
 |-  ( z = ( ( k + 1 ) / y ) -> ( ta <-> [. ( y x. ( ( k + 1 ) / y ) ) / x ]. ph ) )
101 95 100 imbi12d 
 |-  ( z = ( ( k + 1 ) / y ) -> ( ( ( ch /\ th ) -> ta ) <-> ( ( ch /\ [. ( ( k + 1 ) / y ) / x ]. ph ) -> [. ( y x. ( ( k + 1 ) / y ) ) / x ]. ph ) ) )
102 101 imbi2d 
 |-  ( z = ( ( k + 1 ) / y ) -> ( ( y e. ( ZZ>= ` 2 ) -> ( ( ch /\ th ) -> ta ) ) <-> ( y e. ( ZZ>= ` 2 ) -> ( ( ch /\ [. ( ( k + 1 ) / y ) / x ]. ph ) -> [. ( y x. ( ( k + 1 ) / y ) ) / x ]. ph ) ) ) )
103 8 expcom 
 |-  ( z e. ( ZZ>= ` 2 ) -> ( y e. ( ZZ>= ` 2 ) -> ( ( ch /\ th ) -> ta ) ) )
104 102 103 vtoclga 
 |-  ( ( ( k + 1 ) / y ) e. ( ZZ>= ` 2 ) -> ( y e. ( ZZ>= ` 2 ) -> ( ( ch /\ [. ( ( k + 1 ) / y ) / x ]. ph ) -> [. ( y x. ( ( k + 1 ) / y ) ) / x ]. ph ) ) )
105 60 25 94 104 syl3c 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> [. ( y x. ( ( k + 1 ) / y ) ) / x ]. ph )
106 30 105 sbceq1dd 
 |-  ( ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) /\ ( y e. ( 2 ... ( ( k + 1 ) - 1 ) ) /\ y || ( k + 1 ) ) ) -> [. ( k + 1 ) / x ]. ph )
107 106 rexlimdvaa 
 |-  ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) -> ( E. y e. ( 2 ... ( ( k + 1 ) - 1 ) ) y || ( k + 1 ) -> [. ( k + 1 ) / x ]. ph ) )
108 ralnex 
 |-  ( A. y e. ( 2 ... ( ( k + 1 ) - 1 ) ) -. y || ( k + 1 ) <-> -. E. y e. ( 2 ... ( ( k + 1 ) - 1 ) ) y || ( k + 1 ) )
109 simpl 
 |-  ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) -> k e. NN )
110 elnnuz 
 |-  ( k e. NN <-> k e. ( ZZ>= ` 1 ) )
111 109 110 sylib 
 |-  ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) -> k e. ( ZZ>= ` 1 ) )
112 eluzp1p1 
 |-  ( k e. ( ZZ>= ` 1 ) -> ( k + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
113 111 112 syl 
 |-  ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) -> ( k + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
114 df-2 
 |-  2 = ( 1 + 1 )
115 114 fveq2i 
 |-  ( ZZ>= ` 2 ) = ( ZZ>= ` ( 1 + 1 ) )
116 113 115 eleqtrrdi 
 |-  ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) -> ( k + 1 ) e. ( ZZ>= ` 2 ) )
117 isprm3 
 |-  ( ( k + 1 ) e. Prime <-> ( ( k + 1 ) e. ( ZZ>= ` 2 ) /\ A. y e. ( 2 ... ( ( k + 1 ) - 1 ) ) -. y || ( k + 1 ) ) )
118 117 baibr 
 |-  ( ( k + 1 ) e. ( ZZ>= ` 2 ) -> ( A. y e. ( 2 ... ( ( k + 1 ) - 1 ) ) -. y || ( k + 1 ) <-> ( k + 1 ) e. Prime ) )
119 116 118 syl 
 |-  ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) -> ( A. y e. ( 2 ... ( ( k + 1 ) - 1 ) ) -. y || ( k + 1 ) <-> ( k + 1 ) e. Prime ) )
120 simpr 
 |-  ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) -> A. x e. ( 1 ... k ) ph )
121 2 cbvralvw 
 |-  ( A. x e. ( 1 ... k ) ph <-> A. y e. ( 1 ... k ) ch )
122 120 121 sylib 
 |-  ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) -> A. y e. ( 1 ... k ) ch )
123 109 nncnd 
 |-  ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) -> k e. CC )
124 123 42 43 sylancl 
 |-  ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) -> ( ( k + 1 ) - 1 ) = k )
125 124 oveq2d 
 |-  ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) -> ( 1 ... ( ( k + 1 ) - 1 ) ) = ( 1 ... k ) )
126 125 raleqdv 
 |-  ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) -> ( A. y e. ( 1 ... ( ( k + 1 ) - 1 ) ) ch <-> A. y e. ( 1 ... k ) ch ) )
127 122 126 mpbird 
 |-  ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) -> A. y e. ( 1 ... ( ( k + 1 ) - 1 ) ) ch )
128 nfcv 
 |-  F/_ x ( k + 1 )
129 nfv 
 |-  F/ x A. y e. ( 1 ... ( ( k + 1 ) - 1 ) ) ch
130 nfsbc1v 
 |-  F/ x [. ( k + 1 ) / x ]. ph
131 129 130 nfim 
 |-  F/ x ( A. y e. ( 1 ... ( ( k + 1 ) - 1 ) ) ch -> [. ( k + 1 ) / x ]. ph )
132 oveq1 
 |-  ( x = ( k + 1 ) -> ( x - 1 ) = ( ( k + 1 ) - 1 ) )
133 132 oveq2d 
 |-  ( x = ( k + 1 ) -> ( 1 ... ( x - 1 ) ) = ( 1 ... ( ( k + 1 ) - 1 ) ) )
134 133 raleqdv 
 |-  ( x = ( k + 1 ) -> ( A. y e. ( 1 ... ( x - 1 ) ) ch <-> A. y e. ( 1 ... ( ( k + 1 ) - 1 ) ) ch ) )
135 sbceq1a 
 |-  ( x = ( k + 1 ) -> ( ph <-> [. ( k + 1 ) / x ]. ph ) )
136 134 135 imbi12d 
 |-  ( x = ( k + 1 ) -> ( ( A. y e. ( 1 ... ( x - 1 ) ) ch -> ph ) <-> ( A. y e. ( 1 ... ( ( k + 1 ) - 1 ) ) ch -> [. ( k + 1 ) / x ]. ph ) ) )
137 7 ex 
 |-  ( x e. Prime -> ( A. y e. ( 1 ... ( x - 1 ) ) ch -> ph ) )
138 128 131 136 137 vtoclgaf 
 |-  ( ( k + 1 ) e. Prime -> ( A. y e. ( 1 ... ( ( k + 1 ) - 1 ) ) ch -> [. ( k + 1 ) / x ]. ph ) )
139 127 138 syl5com 
 |-  ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) -> ( ( k + 1 ) e. Prime -> [. ( k + 1 ) / x ]. ph ) )
140 119 139 sylbid 
 |-  ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) -> ( A. y e. ( 2 ... ( ( k + 1 ) - 1 ) ) -. y || ( k + 1 ) -> [. ( k + 1 ) / x ]. ph ) )
141 108 140 syl5bir 
 |-  ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) -> ( -. E. y e. ( 2 ... ( ( k + 1 ) - 1 ) ) y || ( k + 1 ) -> [. ( k + 1 ) / x ]. ph ) )
142 107 141 pm2.61d 
 |-  ( ( k e. NN /\ A. x e. ( 1 ... k ) ph ) -> [. ( k + 1 ) / x ]. ph )
143 142 ex 
 |-  ( k e. NN -> ( A. x e. ( 1 ... k ) ph -> [. ( k + 1 ) / x ]. ph ) )
144 ralsnsg 
 |-  ( ( k + 1 ) e. NN -> ( A. x e. { ( k + 1 ) } ph <-> [. ( k + 1 ) / x ]. ph ) )
145 21 144 syl 
 |-  ( k e. NN -> ( A. x e. { ( k + 1 ) } ph <-> [. ( k + 1 ) / x ]. ph ) )
146 143 145 sylibrd 
 |-  ( k e. NN -> ( A. x e. ( 1 ... k ) ph -> A. x e. { ( k + 1 ) } ph ) )
147 146 ancld 
 |-  ( k e. NN -> ( A. x e. ( 1 ... k ) ph -> ( A. x e. ( 1 ... k ) ph /\ A. x e. { ( k + 1 ) } ph ) ) )
148 fzsuc 
 |-  ( k e. ( ZZ>= ` 1 ) -> ( 1 ... ( k + 1 ) ) = ( ( 1 ... k ) u. { ( k + 1 ) } ) )
149 110 148 sylbi 
 |-  ( k e. NN -> ( 1 ... ( k + 1 ) ) = ( ( 1 ... k ) u. { ( k + 1 ) } ) )
150 149 raleqdv 
 |-  ( k e. NN -> ( A. x e. ( 1 ... ( k + 1 ) ) ph <-> A. x e. ( ( 1 ... k ) u. { ( k + 1 ) } ) ph ) )
151 ralunb 
 |-  ( A. x e. ( ( 1 ... k ) u. { ( k + 1 ) } ) ph <-> ( A. x e. ( 1 ... k ) ph /\ A. x e. { ( k + 1 ) } ph ) )
152 150 151 bitrdi 
 |-  ( k e. NN -> ( A. x e. ( 1 ... ( k + 1 ) ) ph <-> ( A. x e. ( 1 ... k ) ph /\ A. x e. { ( k + 1 ) } ph ) ) )
153 147 152 sylibrd 
 |-  ( k e. NN -> ( A. x e. ( 1 ... k ) ph -> A. x e. ( 1 ... ( k + 1 ) ) ph ) )
154 10 12 14 16 20 153 nnind 
 |-  ( A e. NN -> A. x e. ( 1 ... A ) ph )
155 elfz1end 
 |-  ( A e. NN <-> A e. ( 1 ... A ) )
156 155 biimpi 
 |-  ( A e. NN -> A e. ( 1 ... A ) )
157 5 154 156 rspcdva 
 |-  ( A e. NN -> et )