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φψ
prmind.2 x=yφχ
prmind.3 x=zφθ
prmind.4 x=yzφτ
prmind.5 x=Aφη
prmind.6 ψ
prmind2.7 xy1x1χφ
prmind2.8 y2z2χθτ
Assertion prmind2 Aη

Proof

Step Hyp Ref Expression
1 prmind.1 x=1φψ
2 prmind.2 x=yφχ
3 prmind.3 x=zφθ
4 prmind.4 x=yzφτ
5 prmind.5 x=Aφη
6 prmind.6 ψ
7 prmind2.7 xy1x1χφ
8 prmind2.8 y2z2χθτ
9 oveq2 n=11n=11
10 9 raleqdv n=1x1nφx11φ
11 oveq2 n=k1n=1k
12 11 raleqdv n=kx1nφx1kφ
13 oveq2 n=k+11n=1k+1
14 13 raleqdv n=k+1x1nφx1k+1φ
15 oveq2 n=A1n=1A
16 15 raleqdv n=Ax1nφx1Aφ
17 elfz1eq x11x=1
18 17 1 syl x11φψ
19 6 18 mpbiri x11φ
20 19 rgen x11φ
21 peano2nn kk+1
22 21 ad2antrr kx1kφy2k+1-1yk+1k+1
23 22 nncnd kx1kφy2k+1-1yk+1k+1
24 elfzuz y2k+1-1y2
25 24 ad2antrl kx1kφy2k+1-1yk+1y2
26 eluz2nn y2y
27 25 26 syl kx1kφy2k+1-1yk+1y
28 27 nncnd kx1kφy2k+1-1yk+1y
29 27 nnne0d kx1kφy2k+1-1yk+1y0
30 23 28 29 divcan2d kx1kφy2k+1-1yk+1yk+1y=k+1
31 simprr kx1kφy2k+1-1yk+1yk+1
32 27 nnzd kx1kφy2k+1-1yk+1y
33 22 nnzd kx1kφy2k+1-1yk+1k+1
34 dvdsval2 yy0k+1yk+1k+1y
35 32 29 33 34 syl3anc kx1kφy2k+1-1yk+1yk+1k+1y
36 31 35 mpbid kx1kφy2k+1-1yk+1k+1y
37 28 mulid2d kx1kφy2k+1-1yk+11y=y
38 elfzle2 y2k+1-1yk+1-1
39 38 ad2antrl kx1kφy2k+1-1yk+1yk+1-1
40 nncn kk
41 40 ad2antrr kx1kφy2k+1-1yk+1k
42 ax-1cn 1
43 pncan k1k+1-1=k
44 41 42 43 sylancl kx1kφy2k+1-1yk+1k+1-1=k
45 39 44 breqtrd kx1kφy2k+1-1yk+1yk
46 nnz kk
47 46 ad2antrr kx1kφy2k+1-1yk+1k
48 zleltp1 ykyky<k+1
49 32 47 48 syl2anc kx1kφy2k+1-1yk+1yky<k+1
50 45 49 mpbid kx1kφy2k+1-1yk+1y<k+1
51 37 50 eqbrtrd kx1kφy2k+1-1yk+11y<k+1
52 1red kx1kφy2k+1-1yk+11
53 22 nnred kx1kφy2k+1-1yk+1k+1
54 27 nnred kx1kφy2k+1-1yk+1y
55 27 nngt0d kx1kφy2k+1-1yk+10<y
56 ltmuldiv 1k+1y0<y1y<k+11<k+1y
57 52 53 54 55 56 syl112anc kx1kφy2k+1-1yk+11y<k+11<k+1y
58 51 57 mpbid kx1kφy2k+1-1yk+11<k+1y
59 eluz2b1 k+1y2k+1y1<k+1y
60 36 58 59 sylanbrc kx1kφy2k+1-1yk+1k+1y2
61 simplr kx1kφy2k+1-1yk+1x1kφ
62 fznn ky1kyyk
63 47 62 syl kx1kφy2k+1-1yk+1y1kyyk
64 27 45 63 mpbir2and kx1kφy2k+1-1yk+1y1k
65 2 61 64 rspcdva kx1kφy2k+1-1yk+1χ
66 vex zV
67 66 3 sbcie [˙z/x]˙φθ
68 dfsbcq z=k+1y[˙z/x]˙φ[˙k+1y/x]˙φ
69 67 68 bitr3id z=k+1yθ[˙k+1y/x]˙φ
70 3 cbvralvw x1kφz1kθ
71 61 70 sylib kx1kφy2k+1-1yk+1z1kθ
72 22 nnrpd kx1kφy2k+1-1yk+1k+1+
73 27 nnrpd kx1kφy2k+1-1yk+1y+
74 72 73 rpdivcld kx1kφy2k+1-1yk+1k+1y+
75 74 rpgt0d kx1kφy2k+1-1yk+10<k+1y
76 elnnz k+1yk+1y0<k+1y
77 36 75 76 sylanbrc kx1kφy2k+1-1yk+1k+1y
78 22 nnne0d kx1kφy2k+1-1yk+1k+10
79 23 78 dividd kx1kφy2k+1-1yk+1k+1k+1=1
80 eluz2gt1 y21<y
81 25 80 syl kx1kφy2k+1-1yk+11<y
82 79 81 eqbrtrd kx1kφy2k+1-1yk+1k+1k+1<y
83 22 nngt0d kx1kφy2k+1-1yk+10<k+1
84 ltdiv23 k+1k+10<k+1y0<yk+1k+1<yk+1y<k+1
85 53 53 83 54 55 84 syl122anc kx1kφy2k+1-1yk+1k+1k+1<yk+1y<k+1
86 82 85 mpbid kx1kφy2k+1-1yk+1k+1y<k+1
87 zleltp1 k+1ykk+1ykk+1y<k+1
88 36 47 87 syl2anc kx1kφy2k+1-1yk+1k+1ykk+1y<k+1
89 86 88 mpbird kx1kφy2k+1-1yk+1k+1yk
90 fznn kk+1y1kk+1yk+1yk
91 47 90 syl kx1kφy2k+1-1yk+1k+1y1kk+1yk+1yk
92 77 89 91 mpbir2and kx1kφy2k+1-1yk+1k+1y1k
93 69 71 92 rspcdva kx1kφy2k+1-1yk+1[˙k+1y/x]˙φ
94 65 93 jca kx1kφy2k+1-1yk+1χ[˙k+1y/x]˙φ
95 69 anbi2d z=k+1yχθχ[˙k+1y/x]˙φ
96 ovex yzV
97 96 4 sbcie [˙yz/x]˙φτ
98 oveq2 z=k+1yyz=yk+1y
99 98 sbceq1d z=k+1y[˙yz/x]˙φ[˙yk+1y/x]˙φ
100 97 99 bitr3id z=k+1yτ[˙yk+1y/x]˙φ
101 95 100 imbi12d z=k+1yχθτχ[˙k+1y/x]˙φ[˙yk+1y/x]˙φ
102 101 imbi2d z=k+1yy2χθτy2χ[˙k+1y/x]˙φ[˙yk+1y/x]˙φ
103 8 expcom z2y2χθτ
104 102 103 vtoclga k+1y2y2χ[˙k+1y/x]˙φ[˙yk+1y/x]˙φ
105 60 25 94 104 syl3c kx1kφy2k+1-1yk+1[˙yk+1y/x]˙φ
106 30 105 sbceq1dd kx1kφy2k+1-1yk+1[˙k+1/x]˙φ
107 106 rexlimdvaa kx1kφy2k+1-1yk+1[˙k+1/x]˙φ
108 ralnex y2k+1-1¬yk+1¬y2k+1-1yk+1
109 simpl kx1kφk
110 elnnuz kk1
111 109 110 sylib kx1kφk1
112 eluzp1p1 k1k+11+1
113 111 112 syl kx1kφk+11+1
114 df-2 2=1+1
115 114 fveq2i 2=1+1
116 113 115 eleqtrrdi kx1kφk+12
117 isprm3 k+1k+12y2k+1-1¬yk+1
118 117 baibr k+12y2k+1-1¬yk+1k+1
119 116 118 syl kx1kφy2k+1-1¬yk+1k+1
120 simpr kx1kφx1kφ
121 2 cbvralvw x1kφy1kχ
122 120 121 sylib kx1kφy1kχ
123 109 nncnd kx1kφk
124 123 42 43 sylancl kx1kφk+1-1=k
125 124 oveq2d kx1kφ1k+1-1=1k
126 125 raleqdv kx1kφy1k+1-1χy1kχ
127 122 126 mpbird kx1kφy1k+1-1χ
128 nfcv _xk+1
129 nfv xy1k+1-1χ
130 nfsbc1v x[˙k+1/x]˙φ
131 129 130 nfim xy1k+1-1χ[˙k+1/x]˙φ
132 oveq1 x=k+1x1=k+1-1
133 132 oveq2d x=k+11x1=1k+1-1
134 133 raleqdv x=k+1y1x1χy1k+1-1χ
135 sbceq1a x=k+1φ[˙k+1/x]˙φ
136 134 135 imbi12d x=k+1y1x1χφy1k+1-1χ[˙k+1/x]˙φ
137 7 ex xy1x1χφ
138 128 131 136 137 vtoclgaf k+1y1k+1-1χ[˙k+1/x]˙φ
139 127 138 syl5com kx1kφk+1[˙k+1/x]˙φ
140 119 139 sylbid kx1kφy2k+1-1¬yk+1[˙k+1/x]˙φ
141 108 140 syl5bir kx1kφ¬y2k+1-1yk+1[˙k+1/x]˙φ
142 107 141 pm2.61d kx1kφ[˙k+1/x]˙φ
143 142 ex kx1kφ[˙k+1/x]˙φ
144 ralsnsg k+1xk+1φ[˙k+1/x]˙φ
145 21 144 syl kxk+1φ[˙k+1/x]˙φ
146 143 145 sylibrd kx1kφxk+1φ
147 146 ancld kx1kφx1kφxk+1φ
148 fzsuc k11k+1=1kk+1
149 110 148 sylbi k1k+1=1kk+1
150 149 raleqdv kx1k+1φx1kk+1φ
151 ralunb x1kk+1φx1kφxk+1φ
152 150 151 bitrdi kx1k+1φx1kφxk+1φ
153 147 152 sylibrd kx1kφx1k+1φ
154 10 12 14 16 20 153 nnind Ax1Aφ
155 elfz1end AA1A
156 155 biimpi AA1A
157 5 154 156 rspcdva Aη