prmind2 - Intuitionistic Logic Explorer

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

Theorem prmind2 12813

Description: A variation on prmind 12814 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 6057	. . . 4 ⊢ (𝑛 = 1 → (1...𝑛) = (1...1))
3	2	raleqdv 2746	. . 3 ⊢ (𝑛 = 1 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...1)𝜑))
4		oveq2 6057	. . . 4 ⊢ (𝑛 = 𝑘 → (1...𝑛) = (1...𝑘))
5	4	raleqdv 2746	. . 3 ⊢ (𝑛 = 𝑘 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...𝑘)𝜑))
6		oveq2 6057	. . . 4 ⊢ (𝑛 = (𝑘 + 1) → (1...𝑛) = (1...(𝑘 + 1)))
7	6	raleqdv 2746	. . 3 ⊢ (𝑛 = (𝑘 + 1) → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...(𝑘 + 1))𝜑))
8		oveq2 6057	. . . 4 ⊢ (𝑛 = 𝐴 → (1...𝑛) = (1...𝐴))
9	8	raleqdv 2746	. . 3 ⊢ (𝑛 = 𝐴 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...𝐴)𝜑))
10		prmind.6	. . . . 5 ⊢ 𝜓
11		elfz1eq 10368	. . . . . 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 2595	. . 3 ⊢ ∀𝑥 ∈ (1...1)𝜑
16		peano2nn 9248	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
17	16	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℕ)
18	17	nncnd 9250	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℂ)
19		elfzuz 10354	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ∈ (ℤ_≥‘2))
20	19	ad2antrl 490	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ (ℤ_≥‘2))
21		eluz2nn 9897	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (ℤ_≥‘2) → 𝑦 ∈ ℕ)
22	20, 21	syl 14	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℕ)
23	22	nncnd 9250	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℂ)
24	22	nnap0d 9282	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 # 0)
25	18, 23, 24	divcanap2d 9065	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 · ((𝑘 + 1) / 𝑦)) = (𝑘 + 1))
26		simprr 533	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∥ (𝑘 + 1))
27	22	nnzd 9698	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℤ)
28	22	nnne0d 9281	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≠ 0)
29	17	nnzd 9698	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℤ)
30		dvdsval2 12472	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ∧ (𝑘 + 1) ∈ ℤ) → (𝑦 ∥ (𝑘 + 1) ↔ ((𝑘 + 1) / 𝑦) ∈ ℤ))
31	27, 28, 29, 30	syl3anc 1274	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ∥ (𝑘 + 1) ↔ ((𝑘 + 1) / 𝑦) ∈ ℤ))
32	26, 31	mpbid 147	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℤ)
33	23	mullidd 8291	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (1 · 𝑦) = 𝑦)
34		elfzle2 10361	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ≤ ((𝑘 + 1) − 1))
35	34	ad2antrl 490	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≤ ((𝑘 + 1) − 1))
36		nncn 9244	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
37	36	ad2antrr 488	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑘 ∈ ℂ)
38		ax-1cn 8219	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
39		pncan 8478	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
40	37, 38, 39	sylancl 413	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) − 1) = 𝑘)
41	35, 40	breqtrd 4134	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≤ 𝑘)
42		nnz 9595	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
43	42	ad2antrr 488	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑘 ∈ ℤ)
44		zleltp1 9632	. . . . . . . . . . . . . . . 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 4130	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (1 · 𝑦) < (𝑘 + 1))
48		1red 8288	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 ∈ ℝ)
49	17	nnred 9249	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℝ)
50	22	nnred 9249	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℝ)
51	22	nngt0d 9280	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < 𝑦)
52		ltmuldiv 9147	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → ((1 · 𝑦) < (𝑘 + 1) ↔ 1 < ((𝑘 + 1) / 𝑦)))
53	48, 49, 50, 51, 52	syl112anc 1278	. . . . . . . . . . . . 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 9932	. . . . . . . . . . . 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 529	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ∀𝑥 ∈ (1...𝑘)𝜑)
59		fznn 10422	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℤ → (𝑦 ∈ (1...𝑘) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑘)))
60	43, 59	syl 14	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ∈ (1...𝑘) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑘)))
61	22, 41, 60	mpbir2and 953	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ (1...𝑘))
62	57, 58, 61	rspcdva 2925	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝜒)
63		vex 2815	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
64		prmind.3	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜃))
65	63, 64	sbcie 3076	. . . . . . . . . . . . . 14 ⊢ ([𝑧 / 𝑥]𝜑 ↔ 𝜃)
66		dfsbcq 3043	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ([𝑧 / 𝑥]𝜑 ↔ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑))
67	65, 66	bitr3id 194	. . . . . . . . . . . . 13 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (𝜃 ↔ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑))
68	64	cbvralv 2777	. . . . . . . . . . . . . 14 ⊢ (∀𝑥 ∈ (1...𝑘)𝜑 ↔ ∀𝑧 ∈ (1...𝑘)𝜃)
69	58, 68	sylib 122	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ∀𝑧 ∈ (1...𝑘)𝜃)
70	17	nnrpd 10026	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℝ⁺)
71	22	nnrpd 10026	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℝ⁺)
72	70, 71	rpdivcld 10046	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℝ⁺)
73	72	rpgt0d 10031	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < ((𝑘 + 1) / 𝑦))
74		elnnz 9586	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 + 1) / 𝑦) ∈ ℕ ↔ (((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 0 < ((𝑘 + 1) / 𝑦)))
75	32, 73, 74	sylanbrc 417	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℕ)
76	17	nnap0d 9282	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) # 0)
77	18, 76	dividapd 9059	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / (𝑘 + 1)) = 1)
78		eluz2gt1 9933	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (ℤ_≥‘2) → 1 < 𝑦)
79	20, 78	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 < 𝑦)
80	77, 79	eqbrtrd 4130	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / (𝑘 + 1)) < 𝑦)
81	17	nngt0d 9280	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < (𝑘 + 1))
82		ltdiv23 9165	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 + 1) ∈ ℝ ∧ ((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1)) ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → (((𝑘 + 1) / (𝑘 + 1)) < 𝑦 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1)))
83	49, 49, 81, 50, 51, 82	syl122anc 1283	. . . . . . . . . . . . . . . 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 9632	. . . . . . . . . . . . . . . 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 10422	. . . . . . . . . . . . . . 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 953	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ (1...𝑘))
91	67, 69, 90	rspcdva 2925	. . . . . . . . . . . 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 6057	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (𝑦 · 𝑧) = (𝑦 · ((𝑘 + 1) / 𝑦)))
95	94	sbceq1d 3046	. . . . . . . . . . . . . 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 9862	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (ℤ_≥‘2) → 𝑦 ∈ ℤ)
101	100	adantl 277	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ (ℤ_≥‘2) ∧ 𝑦 ∈ (ℤ_≥‘2)) → 𝑦 ∈ ℤ)
102		eluzelz 9862	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (ℤ_≥‘2) → 𝑧 ∈ ℤ)
103	102	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ (ℤ_≥‘2) ∧ 𝑦 ∈ (ℤ_≥‘2)) → 𝑧 ∈ ℤ)
104	101, 103	zmulcld 9705	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ (ℤ_≥‘2) ∧ 𝑦 ∈ (ℤ_≥‘2)) → (𝑦 · 𝑧) ∈ ℤ)
105		prmind.4	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝜑 ↔ 𝜏))
106	105	sbcieg 3074	. . . . . . . . . . . . . . 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 2880	. . . . . . . . . . 11 ⊢ (((𝑘 + 1) / 𝑦) ∈ (ℤ_≥‘2) → (𝑦 ∈ (ℤ_≥‘2) → ((𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)))
111	56, 20, 92, 110	syl3c 63	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)
112	25, 111	sbceq1dd 3047	. . . . . . . . 9 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [(𝑘 + 1) / 𝑥]𝜑)
113	112	rexlimdvaa 2661	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑))
114		ralnex 2530	. . . . . . . . 9 ⊢ (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) ↔ ¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1))
115		simpl 109	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℕ)
116		elnnuz 9890	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ_≥‘1))
117	115, 116	sylib 122	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ (ℤ_≥‘1))
118		eluzp1p1 9879	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (𝑘 + 1) ∈ (ℤ_≥‘(1 + 1)))
119	117, 118	syl 14	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈ (ℤ_≥‘(1 + 1)))
120		df-2 9295	. . . . . . . . . . . . 13 ⊢ 2 = (1 + 1)
121	120	fveq2i 5672	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘2) = (ℤ_≥‘(1 + 1))
122	119, 121	eleqtrrdi 2326	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈ (ℤ_≥‘2))
123		isprm3 12811	. . . . . . . . . . . 12 ⊢ ((𝑘 + 1) ∈ ℙ ↔ ((𝑘 + 1) ∈ (ℤ_≥‘2) ∧ ∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1)))
124	123	baibr 928	. . . . . . . . . . 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 2777	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ (1...𝑘)𝜑 ↔ ∀𝑦 ∈ (1...𝑘)𝜒)
128	126, 127	sylib 122	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑦 ∈ (1...𝑘)𝜒)
129	115	nncnd 9250	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℂ)
130	129, 38, 39	sylancl 413	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ((𝑘 + 1) − 1) = 𝑘)
131	130	oveq2d 6065	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (1...((𝑘 + 1) − 1)) = (1...𝑘))
132	131	raleqdv 2746	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 ↔ ∀𝑦 ∈ (1...𝑘)𝜒))
133	128, 132	mpbird 167	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒)
134		nfcv 2384	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝑘 + 1)
135		nfv 1577	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒
136		nfsbc1v 3060	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥[(𝑘 + 1) / 𝑥]𝜑
137	135, 136	nfim 1621	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 → [(𝑘 + 1) / 𝑥]𝜑)
138		oveq1 6056	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑘 + 1) → (𝑥 − 1) = ((𝑘 + 1) − 1))
139	138	oveq2d 6065	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑘 + 1) → (1...(𝑥 − 1)) = (1...((𝑘 + 1) − 1)))
140	139	raleqdv 2746	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑘 + 1) → (∀𝑦 ∈ (1...(𝑥 − 1))𝜒 ↔ ∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒))
141		sbceq1a 3051	. . . . . . . . . . . . 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 2879	. . . . . . . . . . 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 9604	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
150	149	a1i 9	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 2 ∈ ℤ)
151	115	nnzd 9698	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℤ)
152	151	peano2zd 9702	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈ ℤ)
153		1zzd 9603	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 1 ∈ ℤ)
154	152, 153	zsubcld 9704	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ((𝑘 + 1) − 1) ∈ ℤ)
155	19, 21	syl 14	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ∈ ℕ)
156		dvdsdc 12480	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ (𝑘 + 1) ∈ ℤ) → DECID 𝑦 ∥ (𝑘 + 1))
157	155, 152, 156	syl2anr 290	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ 𝑦 ∈ (2...((𝑘 + 1) − 1))) → DECID 𝑦 ∥ (𝑘 + 1))
158	150, 154, 157	exfzdc 10585	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → DECID ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1))
159		exmiddc 844	. . . . . . . . 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 726	. . . . . . 7 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → [(𝑘 + 1) / 𝑥]𝜑)
162	161	ex 115	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...𝑘)𝜑 → [(𝑘 + 1) / 𝑥]𝜑))
163		ralsnsg 3725	. . . . . . 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 10402	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)}))
168	116, 167	sylbi 121	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)}))
169	168	raleqdv 2746	. . . . 5 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...(𝑘 + 1))𝜑 ↔ ∀𝑥 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})𝜑))
170		ralunb 3399	. . . . 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 9252	. 2 ⊢ (𝐴 ∈ ℕ → ∀𝑥 ∈ (1...𝐴)𝜑)
174		elfz1end 10388	. . 3 ⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈ (1...𝐴))
175	174	biimpi 120	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ (1...𝐴))
176	1, 173, 175	rspcdva 2925	1 ⊢ (𝐴 ∈ ℕ → 𝜂)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 716 DECID wdc 842 = wceq 1398 ∈ wcel 2203 ≠ wne 2412 ∀wral 2520 ∃wrex 2521 [wsbc 3041 ∪ cun 3208 {csn 3688 class class class wbr 4108 ‘cfv 5351 (class class class)co 6049 ℂcc 8124 ℝcr 8125 0cc0 8126 1c1 8127 + caddc 8129 · cmul 8131 < clt 8307 ≤ cle 8308 − cmin 8443 / cdiv 8945 ℕcn 9236 2c2 9287 ℤcz 9576 ℤ_≥cuz 9852 ...cfz 10341 ∥ cdvds 12469 ℙcprime 12800

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2205 ax-14 2206 ax-ext 2214 ax-coll 4224 ax-sep 4227 ax-nul 4235 ax-pow 4286 ax-pr 4321 ax-un 4553 ax-setind 4658 ax-iinf 4709 ax-cnex 8217 ax-resscn 8218 ax-1cn 8219 ax-1re 8220 ax-icn 8221 ax-addcl 8222 ax-addrcl 8223 ax-mulcl 8224 ax-mulrcl 8225 ax-addcom 8226 ax-mulcom 8227 ax-addass 8228 ax-mulass 8229 ax-distr 8230 ax-i2m1 8231 ax-0lt1 8232 ax-1rid 8233 ax-0id 8234 ax-rnegex 8235 ax-precex 8236 ax-cnre 8237 ax-pre-ltirr 8238 ax-pre-ltwlin 8239 ax-pre-lttrn 8240 ax-pre-apti 8241 ax-pre-ltadd 8242 ax-pre-mulgt0 8243 ax-pre-mulext 8244 ax-arch 8245 ax-caucvg 8246

This theorem depends on definitions: df-bi 117 df-stab 839 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2083 df-mo 2084 df-clab 2219 df-cleq 2225 df-clel 2228 df-nfc 2373 df-ne 2413 df-nel 2508 df-ral 2525 df-rex 2526 df-reu 2527 df-rmo 2528 df-rab 2529 df-v 2814 df-sbc 3042 df-csb 3138 df-dif 3212 df-un 3214 df-in 3216 df-ss 3223 df-nul 3508 df-if 3620 df-pw 3670 df-sn 3694 df-pr 3695 df-op 3697 df-uni 3914 df-int 3949 df-iun 3992 df-br 4109 df-opab 4171 df-mpt 4172 df-tr 4208 df-id 4413 df-po 4416 df-iso 4417 df-iord 4486 df-on 4488 df-ilim 4489 df-suc 4491 df-iom 4712 df-xp 4754 df-rel 4755 df-cnv 4756 df-co 4757 df-dm 4758 df-rn 4759 df-res 4760 df-ima 4761 df-iota 5311 df-fun 5353 df-fn 5354 df-f 5355 df-f1 5356 df-fo 5357 df-f1o 5358 df-fv 5359 df-riota 6002 df-ov 6052 df-oprab 6053 df-mpo 6054 df-1st 6333 df-2nd 6334 df-recs 6535 df-frec 6621 df-1o 6646 df-2o 6647 df-er 6766 df-en 6975 df-pnf 8309 df-mnf 8310 df-xr 8311 df-ltxr 8312 df-le 8313 df-sub 8445 df-neg 8446 df-reap 8848 df-ap 8855 df-div 8946 df-inn 9237 df-2 9295 df-3 9296 df-4 9297 df-n0 9496 df-z 9577 df-uz 9853 df-q 9951 df-rp 9986 df-fz 10342 df-fzo 10476 df-fl 10629 df-mod 10684 df-seqfrec 10809 df-exp 10900 df-cj 11523 df-re 11524 df-im 11525 df-rsqrt 11679 df-abs 11680 df-dvds 12470 df-prm 12801

This theorem is referenced by: prmind 12814 4sqlem19 13103

W3C validator