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 mullidd ⊢ ( ( ( 𝑘 ∈ ℕ ∧ ∀ 𝑥 ∈ ( 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 2 cbvralvw ⊢ ( ∀ 𝑥 ∈ ( 1 ... 𝑘 ) 𝜑 ↔ ∀ 𝑦 ∈ ( 1 ... 𝑘 ) 𝜒 )
121 120 bilani ⊢ ( ( 𝑘 ∈ ℕ ∧ ∀ 𝑥 ∈ ( 1 ... 𝑘 ) 𝜑 ) → ∀ 𝑦 ∈ ( 1 ... 𝑘 ) 𝜒 )
122 109 nncnd ⊢ ( ( 𝑘 ∈ ℕ ∧ ∀ 𝑥 ∈ ( 1 ... 𝑘 ) 𝜑 ) → 𝑘 ∈ ℂ )
123 122 42 43 sylancl ⊢ ( ( 𝑘 ∈ ℕ ∧ ∀ 𝑥 ∈ ( 1 ... 𝑘 ) 𝜑 ) → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
124 123 oveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ ∀ 𝑥 ∈ ( 1 ... 𝑘 ) 𝜑 ) → ( 1 ... ( ( 𝑘 + 1 ) − 1 ) ) = ( 1 ... 𝑘 ) )
125 121 124 raleqtrrdv ⊢ ( ( 𝑘 ∈ ℕ ∧ ∀ 𝑥 ∈ ( 1 ... 𝑘 ) 𝜑 ) → ∀ 𝑦 ∈ ( 1 ... ( ( 𝑘 + 1 ) − 1 ) ) 𝜒 )
126 nfcv ⊢ Ⅎ 𝑥 ( 𝑘 + 1 )
127 nfv ⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ ( 1 ... ( ( 𝑘 + 1 ) − 1 ) ) 𝜒
128 nfsbc1v ⊢ Ⅎ 𝑥 [ ( 𝑘 + 1 ) / 𝑥 ] 𝜑
129 127 128 nfim ⊢ Ⅎ 𝑥 ( ∀ 𝑦 ∈ ( 1 ... ( ( 𝑘 + 1 ) − 1 ) ) 𝜒 → [ ( 𝑘 + 1 ) / 𝑥 ] 𝜑 )
130 oveq1 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝑥 − 1 ) = ( ( 𝑘 + 1 ) − 1 ) )
131 130 oveq2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 1 ... ( 𝑥 − 1 ) ) = ( 1 ... ( ( 𝑘 + 1 ) − 1 ) ) )
132 131 raleqdv ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑥 − 1 ) ) 𝜒 ↔ ∀ 𝑦 ∈ ( 1 ... ( ( 𝑘 + 1 ) − 1 ) ) 𝜒 ) )
133 sbceq1a ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝜑 ↔ [ ( 𝑘 + 1 ) / 𝑥 ] 𝜑 ) )
134 132 133 imbi12d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( ∀ 𝑦 ∈ ( 1 ... ( 𝑥 − 1 ) ) 𝜒 → 𝜑 ) ↔ ( ∀ 𝑦 ∈ ( 1 ... ( ( 𝑘 + 1 ) − 1 ) ) 𝜒 → [ ( 𝑘 + 1 ) / 𝑥 ] 𝜑 ) ) )
135 7 ex ⊢ ( 𝑥 ∈ ℙ → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑥 − 1 ) ) 𝜒 → 𝜑 ) )
136 126 129 134 135 vtoclgaf ⊢ ( ( 𝑘 + 1 ) ∈ ℙ → ( ∀ 𝑦 ∈ ( 1 ... ( ( 𝑘 + 1 ) − 1 ) ) 𝜒 → [ ( 𝑘 + 1 ) / 𝑥 ] 𝜑 ) )
137 125 136 syl5com ⊢ ( ( 𝑘 ∈ ℕ ∧ ∀ 𝑥 ∈ ( 1 ... 𝑘 ) 𝜑 ) → ( ( 𝑘 + 1 ) ∈ ℙ → [ ( 𝑘 + 1 ) / 𝑥 ] 𝜑 ) )
138 119 137 sylbid ⊢ ( ( 𝑘 ∈ ℕ ∧ ∀ 𝑥 ∈ ( 1 ... 𝑘 ) 𝜑 ) → ( ∀ 𝑦 ∈ ( 2 ... ( ( 𝑘 + 1 ) − 1 ) ) ¬ 𝑦 ∥ ( 𝑘 + 1 ) → [ ( 𝑘 + 1 ) / 𝑥 ] 𝜑 ) )
139 108 138 biimtrrid ⊢ ( ( 𝑘 ∈ ℕ ∧ ∀ 𝑥 ∈ ( 1 ... 𝑘 ) 𝜑 ) → ( ¬ ∃ 𝑦 ∈ ( 2 ... ( ( 𝑘 + 1 ) − 1 ) ) 𝑦 ∥ ( 𝑘 + 1 ) → [ ( 𝑘 + 1 ) / 𝑥 ] 𝜑 ) )
140 107 139 pm2.61d ⊢ ( ( 𝑘 ∈ ℕ ∧ ∀ 𝑥 ∈ ( 1 ... 𝑘 ) 𝜑 ) → [ ( 𝑘 + 1 ) / 𝑥 ] 𝜑 )
141 140 ex ⊢ ( 𝑘 ∈ ℕ → ( ∀ 𝑥 ∈ ( 1 ... 𝑘 ) 𝜑 → [ ( 𝑘 + 1 ) / 𝑥 ] 𝜑 ) )
142 ralsnsg ⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( ∀ 𝑥 ∈ { ( 𝑘 + 1 ) } 𝜑 ↔ [ ( 𝑘 + 1 ) / 𝑥 ] 𝜑 ) )
143 21 142 syl ⊢ ( 𝑘 ∈ ℕ → ( ∀ 𝑥 ∈ { ( 𝑘 + 1 ) } 𝜑 ↔ [ ( 𝑘 + 1 ) / 𝑥 ] 𝜑 ) )
144 141 143 sylibrd ⊢ ( 𝑘 ∈ ℕ → ( ∀ 𝑥 ∈ ( 1 ... 𝑘 ) 𝜑 → ∀ 𝑥 ∈ { ( 𝑘 + 1 ) } 𝜑 ) )
145 144 ancld ⊢ ( 𝑘 ∈ ℕ → ( ∀ 𝑥 ∈ ( 1 ... 𝑘 ) 𝜑 → ( ∀ 𝑥 ∈ ( 1 ... 𝑘 ) 𝜑 ∧ ∀ 𝑥 ∈ { ( 𝑘 + 1 ) } 𝜑 ) ) )
146 fzsuc ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) → ( 1 ... ( 𝑘 + 1 ) ) = ( ( 1 ... 𝑘 ) ∪ { ( 𝑘 + 1 ) } ) )
147 110 146 sylbi ⊢ ( 𝑘 ∈ ℕ → ( 1 ... ( 𝑘 + 1 ) ) = ( ( 1 ... 𝑘 ) ∪ { ( 𝑘 + 1 ) } ) )
148 147 raleqdv ⊢ ( 𝑘 ∈ ℕ → ( ∀ 𝑥 ∈ ( 1 ... ( 𝑘 + 1 ) ) 𝜑 ↔ ∀ 𝑥 ∈ ( ( 1 ... 𝑘 ) ∪ { ( 𝑘 + 1 ) } ) 𝜑 ) )
149 ralunb ⊢ ( ∀ 𝑥 ∈ ( ( 1 ... 𝑘 ) ∪ { ( 𝑘 + 1 ) } ) 𝜑 ↔ ( ∀ 𝑥 ∈ ( 1 ... 𝑘 ) 𝜑 ∧ ∀ 𝑥 ∈ { ( 𝑘 + 1 ) } 𝜑 ) )
150 148 149 bitrdi ⊢ ( 𝑘 ∈ ℕ → ( ∀ 𝑥 ∈ ( 1 ... ( 𝑘 + 1 ) ) 𝜑 ↔ ( ∀ 𝑥 ∈ ( 1 ... 𝑘 ) 𝜑 ∧ ∀ 𝑥 ∈ { ( 𝑘 + 1 ) } 𝜑 ) ) )
151 145 150 sylibrd ⊢ ( 𝑘 ∈ ℕ → ( ∀ 𝑥 ∈ ( 1 ... 𝑘 ) 𝜑 → ∀ 𝑥 ∈ ( 1 ... ( 𝑘 + 1 ) ) 𝜑 ) )
152 10 12 14 16 20 151 nnind ⊢ ( 𝐴 ∈ ℕ → ∀ 𝑥 ∈ ( 1 ... 𝐴 ) 𝜑 )
153 elfz1end ⊢ ( 𝐴 ∈ ℕ ↔ 𝐴 ∈ ( 1 ... 𝐴 ) )
154 153 biimpi ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ( 1 ... 𝐴 ) )
155 5 152 154 rspcdva ⊢ ( 𝐴 ∈ ℕ → 𝜂 )