prmind2 - Intuitionistic Logic Explorer

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

Theorem prmind2 12261

Description: A variation on prmind 12262 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 5927	. . . 4 ⊢ (𝑛 = 1 → (1...𝑛) = (1...1))
3	2	raleqdv 2696	. . 3 ⊢ (𝑛 = 1 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...1)𝜑))
4		oveq2 5927	. . . 4 ⊢ (𝑛 = 𝑘 → (1...𝑛) = (1...𝑘))
5	4	raleqdv 2696	. . 3 ⊢ (𝑛 = 𝑘 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...𝑘)𝜑))
6		oveq2 5927	. . . 4 ⊢ (𝑛 = (𝑘 + 1) → (1...𝑛) = (1...(𝑘 + 1)))
7	6	raleqdv 2696	. . 3 ⊢ (𝑛 = (𝑘 + 1) → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...(𝑘 + 1))𝜑))
8		oveq2 5927	. . . 4 ⊢ (𝑛 = 𝐴 → (1...𝑛) = (1...𝐴))
9	8	raleqdv 2696	. . 3 ⊢ (𝑛 = 𝐴 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...𝐴)𝜑))
10		prmind.6	. . . . 5 ⊢ 𝜓
11		elfz1eq 10104	. . . . . 6 ⊢ (𝑥 ∈ (1...1) → 𝑥 = 1)
12		prmind.1	. . . . . 6 ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓))
13	11, 12	syl 14	. . . . 5 ⊢ (𝑥 ∈ (1...1) → (𝜑 ↔ 𝜓))
14	10, 13	mpbiri 168	. . . 4 ⊢ (𝑥 ∈ (1...1) → 𝜑)
15	14	rgen 2547	. . 3 ⊢ ∀𝑥 ∈ (1...1)𝜑
16		peano2nn 8996	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
17	16	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℕ)
18	17	nncnd 8998	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℂ)
19		elfzuz 10090	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ∈ (ℤ_≥‘2))
20	19	ad2antrl 490	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ (ℤ_≥‘2))
21		eluz2nn 9634	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (ℤ_≥‘2) → 𝑦 ∈ ℕ)
22	20, 21	syl 14	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℕ)
23	22	nncnd 8998	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℂ)
24	22	nnap0d 9030	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 # 0)
25	18, 23, 24	divcanap2d 8813	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 · ((𝑘 + 1) / 𝑦)) = (𝑘 + 1))
26		simprr 531	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∥ (𝑘 + 1))
27	22	nnzd 9441	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℤ)
28	22	nnne0d 9029	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≠ 0)
29	17	nnzd 9441	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℤ)
30		dvdsval2 11936	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ∧ (𝑘 + 1) ∈ ℤ) → (𝑦 ∥ (𝑘 + 1) ↔ ((𝑘 + 1) / 𝑦) ∈ ℤ))
31	27, 28, 29, 30	syl3anc 1249	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ∥ (𝑘 + 1) ↔ ((𝑘 + 1) / 𝑦) ∈ ℤ))
32	26, 31	mpbid 147	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℤ)
33	23	mulid2d 8040	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (1 · 𝑦) = 𝑦)
34		elfzle2 10097	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ≤ ((𝑘 + 1) − 1))
35	34	ad2antrl 490	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≤ ((𝑘 + 1) − 1))
36		nncn 8992	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
37	36	ad2antrr 488	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑘 ∈ ℂ)
38		ax-1cn 7967	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
39		pncan 8227	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
40	37, 38, 39	sylancl 413	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) − 1) = 𝑘)
41	35, 40	breqtrd 4056	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≤ 𝑘)
42		nnz 9339	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
43	42	ad2antrr 488	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑘 ∈ ℤ)
44		zleltp1 9375	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑦 ≤ 𝑘 ↔ 𝑦 < (𝑘 + 1)))
45	27, 43, 44	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ≤ 𝑘 ↔ 𝑦 < (𝑘 + 1)))
46	41, 45	mpbid 147	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 < (𝑘 + 1))
47	33, 46	eqbrtrd 4052	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (1 · 𝑦) < (𝑘 + 1))
48		1red 8036	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 ∈ ℝ)
49	17	nnred 8997	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℝ)
50	22	nnred 8997	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℝ)
51	22	nngt0d 9028	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < 𝑦)
52		ltmuldiv 8895	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → ((1 · 𝑦) < (𝑘 + 1) ↔ 1 < ((𝑘 + 1) / 𝑦)))
53	48, 49, 50, 51, 52	syl112anc 1253	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((1 · 𝑦) < (𝑘 + 1) ↔ 1 < ((𝑘 + 1) / 𝑦)))
54	47, 53	mpbid 147	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 < ((𝑘 + 1) / 𝑦))
55		eluz2b1 9669	. . . . . . . . . . . 12 ⊢ (((𝑘 + 1) / 𝑦) ∈ (ℤ_≥‘2) ↔ (((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 1 < ((𝑘 + 1) / 𝑦)))
56	32, 54, 55	sylanbrc 417	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ (ℤ_≥‘2))
57		prmind.2	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
58		simplr 528	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ∀𝑥 ∈ (1...𝑘)𝜑)
59		fznn 10158	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℤ → (𝑦 ∈ (1...𝑘) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑘)))
60	43, 59	syl 14	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ∈ (1...𝑘) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑘)))
61	22, 41, 60	mpbir2and 946	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ (1...𝑘))
62	57, 58, 61	rspcdva 2870	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝜒)
63		vex 2763	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
64		prmind.3	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜃))
65	63, 64	sbcie 3021	. . . . . . . . . . . . . 14 ⊢ ([𝑧 / 𝑥]𝜑 ↔ 𝜃)
66		dfsbcq 2988	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ([𝑧 / 𝑥]𝜑 ↔ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑))
67	65, 66	bitr3id 194	. . . . . . . . . . . . 13 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (𝜃 ↔ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑))
68	64	cbvralv 2726	. . . . . . . . . . . . . 14 ⊢ (∀𝑥 ∈ (1...𝑘)𝜑 ↔ ∀𝑧 ∈ (1...𝑘)𝜃)
69	58, 68	sylib 122	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ∀𝑧 ∈ (1...𝑘)𝜃)
70	17	nnrpd 9763	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℝ⁺)
71	22	nnrpd 9763	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℝ⁺)
72	70, 71	rpdivcld 9783	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℝ⁺)
73	72	rpgt0d 9768	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < ((𝑘 + 1) / 𝑦))
74		elnnz 9330	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 + 1) / 𝑦) ∈ ℕ ↔ (((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 0 < ((𝑘 + 1) / 𝑦)))
75	32, 73, 74	sylanbrc 417	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℕ)
76	17	nnap0d 9030	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) # 0)
77	18, 76	dividapd 8807	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / (𝑘 + 1)) = 1)
78		eluz2gt1 9670	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (ℤ_≥‘2) → 1 < 𝑦)
79	20, 78	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 < 𝑦)
80	77, 79	eqbrtrd 4052	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / (𝑘 + 1)) < 𝑦)
81	17	nngt0d 9028	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < (𝑘 + 1))
82		ltdiv23 8913	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 + 1) ∈ ℝ ∧ ((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1)) ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → (((𝑘 + 1) / (𝑘 + 1)) < 𝑦 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1)))
83	49, 49, 81, 50, 51, 82	syl122anc 1258	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (((𝑘 + 1) / (𝑘 + 1)) < 𝑦 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1)))
84	80, 83	mpbid 147	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) < (𝑘 + 1))
85		zleltp1 9375	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((𝑘 + 1) / 𝑦) ≤ 𝑘 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1)))
86	32, 43, 85	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (((𝑘 + 1) / 𝑦) ≤ 𝑘 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1)))
87	84, 86	mpbird 167	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ≤ 𝑘)
88		fznn 10158	. . . . . . . . . . . . . . 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 946	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ (1...𝑘))
91	67, 69, 90	rspcdva 2870	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [((𝑘 + 1) / 𝑦) / 𝑥]𝜑)
92	62, 91	jca 306	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑))
93	67	anbi2d 464	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ((𝜒 ∧ 𝜃) ↔ (𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑)))
94		oveq2 5927	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (𝑦 · 𝑧) = (𝑦 · ((𝑘 + 1) / 𝑦)))
95	94	sbceq1d 2991	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ([(𝑦 · 𝑧) / 𝑥]𝜑 ↔ [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑))
96	93, 95	imbi12d 234	. . . . . . . . . . . . 13 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (((𝜒 ∧ 𝜃) → [(𝑦 · 𝑧) / 𝑥]𝜑) ↔ ((𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)))
97	96	imbi2d 230	. . . . . . . . . . . 12 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ((𝑦 ∈ (ℤ_≥‘2) → ((𝜒 ∧ 𝜃) → [(𝑦 · 𝑧) / 𝑥]𝜑)) ↔ (𝑦 ∈ (ℤ_≥‘2) → ((𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑))))
98		prmind2.8	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → ((𝜒 ∧ 𝜃) → 𝜏))
99	98	ancoms 268	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (ℤ_≥‘2) ∧ 𝑦 ∈ (ℤ_≥‘2)) → ((𝜒 ∧ 𝜃) → 𝜏))
100		eluzelz 9604	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (ℤ_≥‘2) → 𝑦 ∈ ℤ)
101	100	adantl 277	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ (ℤ_≥‘2) ∧ 𝑦 ∈ (ℤ_≥‘2)) → 𝑦 ∈ ℤ)
102		eluzelz 9604	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (ℤ_≥‘2) → 𝑧 ∈ ℤ)
103	102	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ (ℤ_≥‘2) ∧ 𝑦 ∈ (ℤ_≥‘2)) → 𝑧 ∈ ℤ)
104	101, 103	zmulcld 9448	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ (ℤ_≥‘2) ∧ 𝑦 ∈ (ℤ_≥‘2)) → (𝑦 · 𝑧) ∈ ℤ)
105		prmind.4	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝜑 ↔ 𝜏))
106	105	sbcieg 3019	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 · 𝑧) ∈ ℤ → ([(𝑦 · 𝑧) / 𝑥]𝜑 ↔ 𝜏))
107	104, 106	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (ℤ_≥‘2) ∧ 𝑦 ∈ (ℤ_≥‘2)) → ([(𝑦 · 𝑧) / 𝑥]𝜑 ↔ 𝜏))
108	99, 107	sylibrd 169	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ (ℤ_≥‘2) ∧ 𝑦 ∈ (ℤ_≥‘2)) → ((𝜒 ∧ 𝜃) → [(𝑦 · 𝑧) / 𝑥]𝜑))
109	108	ex 115	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (ℤ_≥‘2) → (𝑦 ∈ (ℤ_≥‘2) → ((𝜒 ∧ 𝜃) → [(𝑦 · 𝑧) / 𝑥]𝜑)))
110	97, 109	vtoclga 2827	. . . . . . . . . . 11 ⊢ (((𝑘 + 1) / 𝑦) ∈ (ℤ_≥‘2) → (𝑦 ∈ (ℤ_≥‘2) → ((𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)))
111	56, 20, 92, 110	syl3c 63	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)
112	25, 111	sbceq1dd 2992	. . . . . . . . 9 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [(𝑘 + 1) / 𝑥]𝜑)
113	112	rexlimdvaa 2612	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑))
114		ralnex 2482	. . . . . . . . 9 ⊢ (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) ↔ ¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1))
115		simpl 109	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℕ)
116		elnnuz 9632	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ_≥‘1))
117	115, 116	sylib 122	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ (ℤ_≥‘1))
118		eluzp1p1 9621	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (𝑘 + 1) ∈ (ℤ_≥‘(1 + 1)))
119	117, 118	syl 14	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈ (ℤ_≥‘(1 + 1)))
120		df-2 9043	. . . . . . . . . . . . 13 ⊢ 2 = (1 + 1)
121	120	fveq2i 5558	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘2) = (ℤ_≥‘(1 + 1))
122	119, 121	eleqtrrdi 2287	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈ (ℤ_≥‘2))
123		isprm3 12259	. . . . . . . . . . . 12 ⊢ ((𝑘 + 1) ∈ ℙ ↔ ((𝑘 + 1) ∈ (ℤ_≥‘2) ∧ ∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1)))
124	123	baibr 921	. . . . . . . . . . 11 ⊢ ((𝑘 + 1) ∈ (ℤ_≥‘2) → (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) ↔ (𝑘 + 1) ∈ ℙ))
125	122, 124	syl 14	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) ↔ (𝑘 + 1) ∈ ℙ))
126		simpr 110	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑥 ∈ (1...𝑘)𝜑)
127	57	cbvralv 2726	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ (1...𝑘)𝜑 ↔ ∀𝑦 ∈ (1...𝑘)𝜒)
128	126, 127	sylib 122	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑦 ∈ (1...𝑘)𝜒)
129	115	nncnd 8998	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℂ)
130	129, 38, 39	sylancl 413	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ((𝑘 + 1) − 1) = 𝑘)
131	130	oveq2d 5935	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (1...((𝑘 + 1) − 1)) = (1...𝑘))
132	131	raleqdv 2696	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 ↔ ∀𝑦 ∈ (1...𝑘)𝜒))
133	128, 132	mpbird 167	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒)
134		nfcv 2336	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝑘 + 1)
135		nfv 1539	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒
136		nfsbc1v 3005	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥[(𝑘 + 1) / 𝑥]𝜑
137	135, 136	nfim 1583	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 → [(𝑘 + 1) / 𝑥]𝜑)
138		oveq1 5926	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑘 + 1) → (𝑥 − 1) = ((𝑘 + 1) − 1))
139	138	oveq2d 5935	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑘 + 1) → (1...(𝑥 − 1)) = (1...((𝑘 + 1) − 1)))
140	139	raleqdv 2696	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑘 + 1) → (∀𝑦 ∈ (1...(𝑥 − 1))𝜒 ↔ ∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒))
141		sbceq1a 2996	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑘 + 1) → (𝜑 ↔ [(𝑘 + 1) / 𝑥]𝜑))
142	140, 141	imbi12d 234	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑘 + 1) → ((∀𝑦 ∈ (1...(𝑥 − 1))𝜒 → 𝜑) ↔ (∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 → [(𝑘 + 1) / 𝑥]𝜑)))
143		prmind2.7	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℙ ∧ ∀𝑦 ∈ (1...(𝑥 − 1))𝜒) → 𝜑)
144	143	ex 115	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℙ → (∀𝑦 ∈ (1...(𝑥 − 1))𝜒 → 𝜑))
145	134, 137, 142, 144	vtoclgaf 2826	. . . . . . . . . . 11 ⊢ ((𝑘 + 1) ∈ ℙ → (∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 → [(𝑘 + 1) / 𝑥]𝜑))
146	133, 145	syl5com 29	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ((𝑘 + 1) ∈ ℙ → [(𝑘 + 1) / 𝑥]𝜑))
147	125, 146	sylbid 150	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑))
148	114, 147	biimtrrid 153	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑))
149		2z 9348	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
150	149	a1i 9	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 2 ∈ ℤ)
151	115	nnzd 9441	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℤ)
152	151	peano2zd 9445	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈ ℤ)
153		1zzd 9347	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 1 ∈ ℤ)
154	152, 153	zsubcld 9447	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ((𝑘 + 1) − 1) ∈ ℤ)
155	19, 21	syl 14	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ∈ ℕ)
156		dvdsdc 11944	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ (𝑘 + 1) ∈ ℤ) → DECID 𝑦 ∥ (𝑘 + 1))
157	155, 152, 156	syl2anr 290	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ 𝑦 ∈ (2...((𝑘 + 1) − 1))) → DECID 𝑦 ∥ (𝑘 + 1))
158	150, 154, 157	exfzdc 10310	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → DECID ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1))
159		exmiddc 837	. . . . . . . . 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 719	. . . . . . 7 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → [(𝑘 + 1) / 𝑥]𝜑)
162	161	ex 115	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...𝑘)𝜑 → [(𝑘 + 1) / 𝑥]𝜑))
163		ralsnsg 3656	. . . . . . 7 ⊢ ((𝑘 + 1) ∈ ℕ → (∀𝑥 ∈ {(𝑘 + 1)}𝜑 ↔ [(𝑘 + 1) / 𝑥]𝜑))
164	16, 163	syl 14	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ {(𝑘 + 1)}𝜑 ↔ [(𝑘 + 1) / 𝑥]𝜑))
165	162, 164	sylibrd 169	. . . . 5 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...𝑘)𝜑 → ∀𝑥 ∈ {(𝑘 + 1)}𝜑))
166	165	ancld 325	. . . 4 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...𝑘)𝜑 → (∀𝑥 ∈ (1...𝑘)𝜑 ∧ ∀𝑥 ∈ {(𝑘 + 1)}𝜑)))
167		fzsuc 10138	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)}))
168	116, 167	sylbi 121	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)}))
169	168	raleqdv 2696	. . . . 5 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...(𝑘 + 1))𝜑 ↔ ∀𝑥 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})𝜑))
170		ralunb 3341	. . . . 5 ⊢ (∀𝑥 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})𝜑 ↔ (∀𝑥 ∈ (1...𝑘)𝜑 ∧ ∀𝑥 ∈ {(𝑘 + 1)}𝜑))
171	169, 170	bitrdi 196	. . . 4 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...(𝑘 + 1))𝜑 ↔ (∀𝑥 ∈ (1...𝑘)𝜑 ∧ ∀𝑥 ∈ {(𝑘 + 1)}𝜑)))
172	166, 171	sylibrd 169	. . 3 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...𝑘)𝜑 → ∀𝑥 ∈ (1...(𝑘 + 1))𝜑))
173	3, 5, 7, 9, 15, 172	nnind 9000	. 2 ⊢ (𝐴 ∈ ℕ → ∀𝑥 ∈ (1...𝐴)𝜑)
174		elfz1end 10124	. . 3 ⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈ (1...𝐴))
175	174	biimpi 120	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ (1...𝐴))
176	1, 173, 175	rspcdva 2870	1 ⊢ (𝐴 ∈ ℕ → 𝜂)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 709 DECID wdc 835 = wceq 1364 ∈ wcel 2164 ≠ wne 2364 ∀wral 2472 ∃wrex 2473 [wsbc 2986 ∪ cun 3152 {csn 3619 class class class wbr 4030 ‘cfv 5255 (class class class)co 5919 ℂcc 7872 ℝcr 7873 0cc0 7874 1c1 7875 + caddc 7877 · cmul 7879 < clt 8056 ≤ cle 8057 − cmin 8192 / cdiv 8693 ℕcn 8984 2c2 9035 ℤcz 9320 ℤ_≥cuz 9595 ...cfz 10077 ∥ cdvds 11933 ℙcprime 12248

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-coll 4145 ax-sep 4148 ax-nul 4156 ax-pow 4204 ax-pr 4239 ax-un 4465 ax-setind 4570 ax-iinf 4621 ax-cnex 7965 ax-resscn 7966 ax-1cn 7967 ax-1re 7968 ax-icn 7969 ax-addcl 7970 ax-addrcl 7971 ax-mulcl 7972 ax-mulrcl 7973 ax-addcom 7974 ax-mulcom 7975 ax-addass 7976 ax-mulass 7977 ax-distr 7978 ax-i2m1 7979 ax-0lt1 7980 ax-1rid 7981 ax-0id 7982 ax-rnegex 7983 ax-precex 7984 ax-cnre 7985 ax-pre-ltirr 7986 ax-pre-ltwlin 7987 ax-pre-lttrn 7988 ax-pre-apti 7989 ax-pre-ltadd 7990 ax-pre-mulgt0 7991 ax-pre-mulext 7992 ax-arch 7993 ax-caucvg 7994

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rmo 2480 df-rab 2481 df-v 2762 df-sbc 2987 df-csb 3082 df-dif 3156 df-un 3158 df-in 3160 df-ss 3167 df-nul 3448 df-if 3559 df-pw 3604 df-sn 3625 df-pr 3626 df-op 3628 df-uni 3837 df-int 3872 df-iun 3915 df-br 4031 df-opab 4092 df-mpt 4093 df-tr 4129 df-id 4325 df-po 4328 df-iso 4329 df-iord 4398 df-on 4400 df-ilim 4401 df-suc 4403 df-iom 4624 df-xp 4666 df-rel 4667 df-cnv 4668 df-co 4669 df-dm 4670 df-rn 4671 df-res 4672 df-ima 4673 df-iota 5216 df-fun 5257 df-fn 5258 df-f 5259 df-f1 5260 df-fo 5261 df-f1o 5262 df-fv 5263 df-riota 5874 df-ov 5922 df-oprab 5923 df-mpo 5924 df-1st 6195 df-2nd 6196 df-recs 6360 df-frec 6446 df-1o 6471 df-2o 6472 df-er 6589 df-en 6797 df-pnf 8058 df-mnf 8059 df-xr 8060 df-ltxr 8061 df-le 8062 df-sub 8194 df-neg 8195 df-reap 8596 df-ap 8603 df-div 8694 df-inn 8985 df-2 9043 df-3 9044 df-4 9045 df-n0 9244 df-z 9321 df-uz 9596 df-q 9688 df-rp 9723 df-fz 10078 df-fzo 10212 df-fl 10342 df-mod 10397 df-seqfrec 10522 df-exp 10613 df-cj 10989 df-re 10990 df-im 10991 df-rsqrt 11145 df-abs 11146 df-dvds 11934 df-prm 12249

This theorem is referenced by: prmind 12262 4sqlem19 12550

W3C validator