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 ( 𝑥 = 1 → ( 𝜑𝜓 ) )
prmind.2 ( 𝑥 = 𝑦 → ( 𝜑𝜒 ) )
prmind.3 ( 𝑥 = 𝑧 → ( 𝜑𝜃 ) )
prmind.4 ( 𝑥 = ( 𝑦 · 𝑧 ) → ( 𝜑𝜏 ) )
prmind.5 ( 𝑥 = 𝐴 → ( 𝜑𝜂 ) )
prmind.6 𝜓
prmind2.7 ( ( 𝑥 ∈ ℙ ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑥 − 1 ) ) 𝜒 ) → 𝜑 )
prmind2.8 ( ( 𝑦 ∈ ( ℤ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ ‘ 2 ) ) → ( ( 𝜒𝜃 ) → 𝜏 ) )
Assertion prmind2 ( 𝐴 ∈ ℕ → 𝜂 )

Proof

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