prmind2 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > prmind2		GIF version

Theorem prmind2 12074

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

**Hypotheses**
Ref	Expression
prmind.1	⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓))
prmind.2	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
prmind.3	⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜃))
prmind.4	⊢ (𝑥 = (𝑦 · 𝑧) → (𝜑 ↔ 𝜏))
prmind.5	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜂))
prmind.6	⊢ 𝜓
prmind2.7	⊢ ((𝑥 ∈ ℙ ∧ ∀𝑦 ∈ (1...(𝑥 − 1))𝜒) → 𝜑)
prmind2.8	⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → ((𝜒 ∧ 𝜃) → 𝜏))

**Assertion**
Ref	Expression
prmind2	⊢ (𝐴 ∈ ℕ → 𝜂)

Distinct variable groups: 𝑥,𝑦 𝑥,𝐴 𝑥,𝑧,𝜒 𝜂,𝑥 𝜏,𝑥 𝜃,𝑥 𝑦,𝑧,𝜑 Allowed substitution hints: 𝜑(𝑥) 𝜓(𝑥,𝑦,𝑧) 𝜒(𝑦) 𝜃(𝑦,𝑧) 𝜏(𝑦,𝑧) 𝜂(𝑦,𝑧) 𝐴(𝑦,𝑧)

Proof of Theorem prmind2 Dummy variables 𝑘 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prmind.5	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜂))
2		oveq2 5861	. . . 4 ⊢ (𝑛 = 1 → (1...𝑛) = (1...1))
3	2	raleqdv 2671	. . 3 ⊢ (𝑛 = 1 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...1)𝜑))
4		oveq2 5861	. . . 4 ⊢ (𝑛 = 𝑘 → (1...𝑛) = (1...𝑘))
5	4	raleqdv 2671	. . 3 ⊢ (𝑛 = 𝑘 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...𝑘)𝜑))
6		oveq2 5861	. . . 4 ⊢ (𝑛 = (𝑘 + 1) → (1...𝑛) = (1...(𝑘 + 1)))
7	6	raleqdv 2671	. . 3 ⊢ (𝑛 = (𝑘 + 1) → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...(𝑘 + 1))𝜑))
8		oveq2 5861	. . . 4 ⊢ (𝑛 = 𝐴 → (1...𝑛) = (1...𝐴))
9	8	raleqdv 2671	. . 3 ⊢ (𝑛 = 𝐴 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...𝐴)𝜑))
10		prmind.6	. . . . 5 ⊢ 𝜓
11		elfz1eq 9991	. . . . . 6 ⊢ (𝑥 ∈ (1...1) → 𝑥 = 1)
12		prmind.1	. . . . . 6 ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓))
13	11, 12	syl 14	. . . . 5 ⊢ (𝑥 ∈ (1...1) → (𝜑 ↔ 𝜓))
14	10, 13	mpbiri 167	. . . 4 ⊢ (𝑥 ∈ (1...1) → 𝜑)
15	14	rgen 2523	. . 3 ⊢ ∀𝑥 ∈ (1...1)𝜑
16		peano2nn 8890	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
17	16	ad2antrr 485	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℕ)
18	17	nncnd 8892	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℂ)
19		elfzuz 9977	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ∈ (ℤ_≥‘2))
20	19	ad2antrl 487	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ (ℤ_≥‘2))
21		eluz2nn 9525	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (ℤ_≥‘2) → 𝑦 ∈ ℕ)
22	20, 21	syl 14	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℕ)
23	22	nncnd 8892	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℂ)
24	22	nnap0d 8924	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 # 0)
25	18, 23, 24	divcanap2d 8709	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 · ((𝑘 + 1) / 𝑦)) = (𝑘 + 1))
26		simprr 527	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∥ (𝑘 + 1))
27	22	nnzd 9333	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℤ)
28	22	nnne0d 8923	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≠ 0)
29	17	nnzd 9333	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℤ)
30		dvdsval2 11752	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ∧ (𝑘 + 1) ∈ ℤ) → (𝑦 ∥ (𝑘 + 1) ↔ ((𝑘 + 1) / 𝑦) ∈ ℤ))
31	27, 28, 29, 30	syl3anc 1233	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ∥ (𝑘 + 1) ↔ ((𝑘 + 1) / 𝑦) ∈ ℤ))
32	26, 31	mpbid 146	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℤ)
33	23	mulid2d 7938	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (1 · 𝑦) = 𝑦)
34		elfzle2 9984	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ≤ ((𝑘 + 1) − 1))
35	34	ad2antrl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≤ ((𝑘 + 1) − 1))
36		nncn 8886	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
37	36	ad2antrr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑘 ∈ ℂ)
38		ax-1cn 7867	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
39		pncan 8125	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
40	37, 38, 39	sylancl 411	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) − 1) = 𝑘)
41	35, 40	breqtrd 4015	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≤ 𝑘)
42		nnz 9231	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
43	42	ad2antrr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑘 ∈ ℤ)
44		zleltp1 9267	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑦 ≤ 𝑘 ↔ 𝑦 < (𝑘 + 1)))
45	27, 43, 44	syl2anc 409	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ≤ 𝑘 ↔ 𝑦 < (𝑘 + 1)))
46	41, 45	mpbid 146	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 < (𝑘 + 1))
47	33, 46	eqbrtrd 4011	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (1 · 𝑦) < (𝑘 + 1))
48		1red 7935	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 ∈ ℝ)
49	17	nnred 8891	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℝ)
50	22	nnred 8891	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℝ)
51	22	nngt0d 8922	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < 𝑦)
52		ltmuldiv 8790	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → ((1 · 𝑦) < (𝑘 + 1) ↔ 1 < ((𝑘 + 1) / 𝑦)))
53	48, 49, 50, 51, 52	syl112anc 1237	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((1 · 𝑦) < (𝑘 + 1) ↔ 1 < ((𝑘 + 1) / 𝑦)))
54	47, 53	mpbid 146	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 < ((𝑘 + 1) / 𝑦))
55		eluz2b1 9560	. . . . . . . . . . . 12 ⊢ (((𝑘 + 1) / 𝑦) ∈ (ℤ_≥‘2) ↔ (((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 1 < ((𝑘 + 1) / 𝑦)))
56	32, 54, 55	sylanbrc 415	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ (ℤ_≥‘2))
57		prmind.2	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
58		simplr 525	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ∀𝑥 ∈ (1...𝑘)𝜑)
59		fznn 10045	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℤ → (𝑦 ∈ (1...𝑘) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑘)))
60	43, 59	syl 14	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ∈ (1...𝑘) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑘)))
61	22, 41, 60	mpbir2and 939	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ (1...𝑘))
62	57, 58, 61	rspcdva 2839	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝜒)
63		vex 2733	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
64		prmind.3	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜃))
65	63, 64	sbcie 2989	. . . . . . . . . . . . . 14 ⊢ ([𝑧 / 𝑥]𝜑 ↔ 𝜃)
66		dfsbcq 2957	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ([𝑧 / 𝑥]𝜑 ↔ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑))
67	65, 66	bitr3id 193	. . . . . . . . . . . . 13 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (𝜃 ↔ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑))
68	64	cbvralv 2696	. . . . . . . . . . . . . 14 ⊢ (∀𝑥 ∈ (1...𝑘)𝜑 ↔ ∀𝑧 ∈ (1...𝑘)𝜃)
69	58, 68	sylib 121	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ∀𝑧 ∈ (1...𝑘)𝜃)
70	17	nnrpd 9651	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℝ⁺)
71	22	nnrpd 9651	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℝ⁺)
72	70, 71	rpdivcld 9671	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℝ⁺)
73	72	rpgt0d 9656	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < ((𝑘 + 1) / 𝑦))
74		elnnz 9222	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 + 1) / 𝑦) ∈ ℕ ↔ (((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 0 < ((𝑘 + 1) / 𝑦)))
75	32, 73, 74	sylanbrc 415	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℕ)
76	17	nnap0d 8924	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) # 0)
77	18, 76	dividapd 8703	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / (𝑘 + 1)) = 1)
78		eluz2gt1 9561	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (ℤ_≥‘2) → 1 < 𝑦)
79	20, 78	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 < 𝑦)
80	77, 79	eqbrtrd 4011	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / (𝑘 + 1)) < 𝑦)
81	17	nngt0d 8922	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < (𝑘 + 1))
82		ltdiv23 8808	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 + 1) ∈ ℝ ∧ ((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1)) ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → (((𝑘 + 1) / (𝑘 + 1)) < 𝑦 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1)))
83	49, 49, 81, 50, 51, 82	syl122anc 1242	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (((𝑘 + 1) / (𝑘 + 1)) < 𝑦 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1)))
84	80, 83	mpbid 146	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) < (𝑘 + 1))
85		zleltp1 9267	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((𝑘 + 1) / 𝑦) ≤ 𝑘 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1)))
86	32, 43, 85	syl2anc 409	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (((𝑘 + 1) / 𝑦) ≤ 𝑘 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1)))
87	84, 86	mpbird 166	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ≤ 𝑘)
88		fznn 10045	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℤ → (((𝑘 + 1) / 𝑦) ∈ (1...𝑘) ↔ (((𝑘 + 1) / 𝑦) ∈ ℕ ∧ ((𝑘 + 1) / 𝑦) ≤ 𝑘)))
89	43, 88	syl 14	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (((𝑘 + 1) / 𝑦) ∈ (1...𝑘) ↔ (((𝑘 + 1) / 𝑦) ∈ ℕ ∧ ((𝑘 + 1) / 𝑦) ≤ 𝑘)))
90	75, 87, 89	mpbir2and 939	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ (1...𝑘))
91	67, 69, 90	rspcdva 2839	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [((𝑘 + 1) / 𝑦) / 𝑥]𝜑)
92	62, 91	jca 304	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑))
93	67	anbi2d 461	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ((𝜒 ∧ 𝜃) ↔ (𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑)))
94		oveq2 5861	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (𝑦 · 𝑧) = (𝑦 · ((𝑘 + 1) / 𝑦)))
95	94	sbceq1d 2960	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ([(𝑦 · 𝑧) / 𝑥]𝜑 ↔ [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑))
96	93, 95	imbi12d 233	. . . . . . . . . . . . 13 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (((𝜒 ∧ 𝜃) → [(𝑦 · 𝑧) / 𝑥]𝜑) ↔ ((𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)))
97	96	imbi2d 229	. . . . . . . . . . . 12 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ((𝑦 ∈ (ℤ_≥‘2) → ((𝜒 ∧ 𝜃) → [(𝑦 · 𝑧) / 𝑥]𝜑)) ↔ (𝑦 ∈ (ℤ_≥‘2) → ((𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑))))
98		prmind2.8	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → ((𝜒 ∧ 𝜃) → 𝜏))
99	98	ancoms 266	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (ℤ_≥‘2) ∧ 𝑦 ∈ (ℤ_≥‘2)) → ((𝜒 ∧ 𝜃) → 𝜏))
100		eluzelz 9496	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (ℤ_≥‘2) → 𝑦 ∈ ℤ)
101	100	adantl 275	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ (ℤ_≥‘2) ∧ 𝑦 ∈ (ℤ_≥‘2)) → 𝑦 ∈ ℤ)
102		eluzelz 9496	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (ℤ_≥‘2) → 𝑧 ∈ ℤ)
103	102	adantr 274	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ (ℤ_≥‘2) ∧ 𝑦 ∈ (ℤ_≥‘2)) → 𝑧 ∈ ℤ)
104	101, 103	zmulcld 9340	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ (ℤ_≥‘2) ∧ 𝑦 ∈ (ℤ_≥‘2)) → (𝑦 · 𝑧) ∈ ℤ)
105		prmind.4	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝜑 ↔ 𝜏))
106	105	sbcieg 2987	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 · 𝑧) ∈ ℤ → ([(𝑦 · 𝑧) / 𝑥]𝜑 ↔ 𝜏))
107	104, 106	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (ℤ_≥‘2) ∧ 𝑦 ∈ (ℤ_≥‘2)) → ([(𝑦 · 𝑧) / 𝑥]𝜑 ↔ 𝜏))
108	99, 107	sylibrd 168	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ (ℤ_≥‘2) ∧ 𝑦 ∈ (ℤ_≥‘2)) → ((𝜒 ∧ 𝜃) → [(𝑦 · 𝑧) / 𝑥]𝜑))
109	108	ex 114	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (ℤ_≥‘2) → (𝑦 ∈ (ℤ_≥‘2) → ((𝜒 ∧ 𝜃) → [(𝑦 · 𝑧) / 𝑥]𝜑)))
110	97, 109	vtoclga 2796	. . . . . . . . . . 11 ⊢ (((𝑘 + 1) / 𝑦) ∈ (ℤ_≥‘2) → (𝑦 ∈ (ℤ_≥‘2) → ((𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)))
111	56, 20, 92, 110	syl3c 63	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)
112	25, 111	sbceq1dd 2961	. . . . . . . . 9 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [(𝑘 + 1) / 𝑥]𝜑)
113	112	rexlimdvaa 2588	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑))
114		ralnex 2458	. . . . . . . . 9 ⊢ (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) ↔ ¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1))
115		simpl 108	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℕ)
116		elnnuz 9523	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ_≥‘1))
117	115, 116	sylib 121	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ (ℤ_≥‘1))
118		eluzp1p1 9512	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (𝑘 + 1) ∈ (ℤ_≥‘(1 + 1)))
119	117, 118	syl 14	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈ (ℤ_≥‘(1 + 1)))
120		df-2 8937	. . . . . . . . . . . . 13 ⊢ 2 = (1 + 1)
121	120	fveq2i 5499	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘2) = (ℤ_≥‘(1 + 1))
122	119, 121	eleqtrrdi 2264	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈ (ℤ_≥‘2))
123		isprm3 12072	. . . . . . . . . . . 12 ⊢ ((𝑘 + 1) ∈ ℙ ↔ ((𝑘 + 1) ∈ (ℤ_≥‘2) ∧ ∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1)))
124	123	baibr 915	. . . . . . . . . . 11 ⊢ ((𝑘 + 1) ∈ (ℤ_≥‘2) → (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) ↔ (𝑘 + 1) ∈ ℙ))
125	122, 124	syl 14	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) ↔ (𝑘 + 1) ∈ ℙ))
126		simpr 109	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑥 ∈ (1...𝑘)𝜑)
127	57	cbvralv 2696	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ (1...𝑘)𝜑 ↔ ∀𝑦 ∈ (1...𝑘)𝜒)
128	126, 127	sylib 121	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑦 ∈ (1...𝑘)𝜒)
129	115	nncnd 8892	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℂ)
130	129, 38, 39	sylancl 411	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ((𝑘 + 1) − 1) = 𝑘)
131	130	oveq2d 5869	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (1...((𝑘 + 1) − 1)) = (1...𝑘))
132	131	raleqdv 2671	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 ↔ ∀𝑦 ∈ (1...𝑘)𝜒))
133	128, 132	mpbird 166	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒)
134		nfcv 2312	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝑘 + 1)
135		nfv 1521	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒
136		nfsbc1v 2973	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥[(𝑘 + 1) / 𝑥]𝜑
137	135, 136	nfim 1565	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 → [(𝑘 + 1) / 𝑥]𝜑)
138		oveq1 5860	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑘 + 1) → (𝑥 − 1) = ((𝑘 + 1) − 1))
139	138	oveq2d 5869	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑘 + 1) → (1...(𝑥 − 1)) = (1...((𝑘 + 1) − 1)))
140	139	raleqdv 2671	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑘 + 1) → (∀𝑦 ∈ (1...(𝑥 − 1))𝜒 ↔ ∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒))
141		sbceq1a 2964	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑘 + 1) → (𝜑 ↔ [(𝑘 + 1) / 𝑥]𝜑))
142	140, 141	imbi12d 233	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑘 + 1) → ((∀𝑦 ∈ (1...(𝑥 − 1))𝜒 → 𝜑) ↔ (∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 → [(𝑘 + 1) / 𝑥]𝜑)))
143		prmind2.7	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℙ ∧ ∀𝑦 ∈ (1...(𝑥 − 1))𝜒) → 𝜑)
144	143	ex 114	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℙ → (∀𝑦 ∈ (1...(𝑥 − 1))𝜒 → 𝜑))
145	134, 137, 142, 144	vtoclgaf 2795	. . . . . . . . . . 11 ⊢ ((𝑘 + 1) ∈ ℙ → (∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 → [(𝑘 + 1) / 𝑥]𝜑))
146	133, 145	syl5com 29	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ((𝑘 + 1) ∈ ℙ → [(𝑘 + 1) / 𝑥]𝜑))
147	125, 146	sylbid 149	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑))
148	114, 147	syl5bir 152	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑))
149		2z 9240	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
150	149	a1i 9	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 2 ∈ ℤ)
151	115	nnzd 9333	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℤ)
152	151	peano2zd 9337	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈ ℤ)
153		1zzd 9239	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 1 ∈ ℤ)
154	152, 153	zsubcld 9339	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ((𝑘 + 1) − 1) ∈ ℤ)
155	19, 21	syl 14	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ∈ ℕ)
156		dvdsdc 11760	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ (𝑘 + 1) ∈ ℤ) → DECID 𝑦 ∥ (𝑘 + 1))
157	155, 152, 156	syl2anr 288	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ 𝑦 ∈ (2...((𝑘 + 1) − 1))) → DECID 𝑦 ∥ (𝑘 + 1))
158	150, 154, 157	exfzdc 10196	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → DECID ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1))
159		exmiddc 831	. . . . . . . . 9 ⊢ (DECID ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) → (∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) ∨ ¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1)))
160	158, 159	syl 14	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) ∨ ¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1)))
161	113, 148, 160	mpjaod 713	. . . . . . 7 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → [(𝑘 + 1) / 𝑥]𝜑)
162	161	ex 114	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...𝑘)𝜑 → [(𝑘 + 1) / 𝑥]𝜑))
163		ralsnsg 3620	. . . . . . 7 ⊢ ((𝑘 + 1) ∈ ℕ → (∀𝑥 ∈ {(𝑘 + 1)}𝜑 ↔ [(𝑘 + 1) / 𝑥]𝜑))
164	16, 163	syl 14	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ {(𝑘 + 1)}𝜑 ↔ [(𝑘 + 1) / 𝑥]𝜑))
165	162, 164	sylibrd 168	. . . . 5 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...𝑘)𝜑 → ∀𝑥 ∈ {(𝑘 + 1)}𝜑))
166	165	ancld 323	. . . 4 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...𝑘)𝜑 → (∀𝑥 ∈ (1...𝑘)𝜑 ∧ ∀𝑥 ∈ {(𝑘 + 1)}𝜑)))
167		fzsuc 10025	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)}))
168	116, 167	sylbi 120	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)}))
169	168	raleqdv 2671	. . . . 5 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...(𝑘 + 1))𝜑 ↔ ∀𝑥 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})𝜑))
170		ralunb 3308	. . . . 5 ⊢ (∀𝑥 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})𝜑 ↔ (∀𝑥 ∈ (1...𝑘)𝜑 ∧ ∀𝑥 ∈ {(𝑘 + 1)}𝜑))
171	169, 170	bitrdi 195	. . . 4 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...(𝑘 + 1))𝜑 ↔ (∀𝑥 ∈ (1...𝑘)𝜑 ∧ ∀𝑥 ∈ {(𝑘 + 1)}𝜑)))
172	166, 171	sylibrd 168	. . 3 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...𝑘)𝜑 → ∀𝑥 ∈ (1...(𝑘 + 1))𝜑))
173	3, 5, 7, 9, 15, 172	nnind 8894	. 2 ⊢ (𝐴 ∈ ℕ → ∀𝑥 ∈ (1...𝐴)𝜑)
174		elfz1end 10011	. . 3 ⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈ (1...𝐴))
175	174	biimpi 119	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ (1...𝐴))
176	1, 173, 175	rspcdva 2839	1 ⊢ (𝐴 ∈ ℕ → 𝜂)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 703 DECID wdc 829 = wceq 1348 ∈ wcel 2141 ≠ wne 2340 ∀wral 2448 ∃wrex 2449 [wsbc 2955 ∪ cun 3119 {csn 3583 class class class wbr 3989 ‘cfv 5198 (class class class)co 5853 ℂcc 7772 ℝcr 7773 0cc0 7774 1c1 7775 + caddc 7777 · cmul 7779 < clt 7954 ≤ cle 7955 − cmin 8090 / cdiv 8589 ℕcn 8878 2c2 8929 ℤcz 9212 ℤ_≥cuz 9487 ...cfz 9965 ∥ cdvds 11749 ℙcprime 12061

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-coll 4104 ax-sep 4107 ax-nul 4115 ax-pow 4160 ax-pr 4194 ax-un 4418 ax-setind 4521 ax-iinf 4572 ax-cnex 7865 ax-resscn 7866 ax-1cn 7867 ax-1re 7868 ax-icn 7869 ax-addcl 7870 ax-addrcl 7871 ax-mulcl 7872 ax-mulrcl 7873 ax-addcom 7874 ax-mulcom 7875 ax-addass 7876 ax-mulass 7877 ax-distr 7878 ax-i2m1 7879 ax-0lt1 7880 ax-1rid 7881 ax-0id 7882 ax-rnegex 7883 ax-precex 7884 ax-cnre 7885 ax-pre-ltirr 7886 ax-pre-ltwlin 7887 ax-pre-lttrn 7888 ax-pre-apti 7889 ax-pre-ltadd 7890 ax-pre-mulgt0 7891 ax-pre-mulext 7892 ax-arch 7893 ax-caucvg 7894

This theorem depends on definitions: df-bi 116 df-stab 826 df-dc 830 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-reu 2455 df-rmo 2456 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-nul 3415 df-if 3527 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-int 3832 df-iun 3875 df-br 3990 df-opab 4051 df-mpt 4052 df-tr 4088 df-id 4278 df-po 4281 df-iso 4282 df-iord 4351 df-on 4353 df-ilim 4354 df-suc 4356 df-iom 4575 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-rn 4622 df-res 4623 df-ima 4624 df-iota 5160 df-fun 5200 df-fn 5201 df-f 5202 df-f1 5203 df-fo 5204 df-f1o 5205 df-fv 5206 df-riota 5809 df-ov 5856 df-oprab 5857 df-mpo 5858 df-1st 6119 df-2nd 6120 df-recs 6284 df-frec 6370 df-1o 6395 df-2o 6396 df-er 6513 df-en 6719 df-pnf 7956 df-mnf 7957 df-xr 7958 df-ltxr 7959 df-le 7960 df-sub 8092 df-neg 8093 df-reap 8494 df-ap 8501 df-div 8590 df-inn 8879 df-2 8937 df-3 8938 df-4 8939 df-n0 9136 df-z 9213 df-uz 9488 df-q 9579 df-rp 9611 df-fz 9966 df-fzo 10099 df-fl 10226 df-mod 10279 df-seqfrec 10402 df-exp 10476 df-cj 10806 df-re 10807 df-im 10808 df-rsqrt 10962 df-abs 10963 df-dvds 11750 df-prm 12062

This theorem is referenced by: prmind 12075

W3C validator