prmind2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > prmind2		Structured version Visualization version GIF version

Theorem prmind2 16865

Description: A variation on prmind 16866 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 7428	. . . 4 ⊢ (𝑛 = 1 → (1...𝑛) = (1...1))
3	2	raleqdv 3319	. . 3 ⊢ (𝑛 = 1 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...1)𝜑))
4		oveq2 7428	. . . 4 ⊢ (𝑛 = 𝑘 → (1...𝑛) = (1...𝑘))
5	4	raleqdv 3319	. . 3 ⊢ (𝑛 = 𝑘 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...𝑘)𝜑))
6		oveq2 7428	. . . 4 ⊢ (𝑛 = (𝑘 + 1) → (1...𝑛) = (1...(𝑘 + 1)))
7	6	raleqdv 3319	. . 3 ⊢ (𝑛 = (𝑘 + 1) → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...(𝑘 + 1))𝜑))
8		oveq2 7428	. . . 4 ⊢ (𝑛 = 𝐴 → (1...𝑛) = (1...𝐴))
9	8	raleqdv 3319	. . 3 ⊢ (𝑛 = 𝐴 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...𝐴)𝜑))
10		prmind.6	. . . . 5 ⊢ 𝜓
11		elfz1eq 13671	. . . . . 6 ⊢ (𝑥 ∈ (1...1) → 𝑥 = 1)
12		prmind.1	. . . . . 6 ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓))
13	11, 12	syl 18	. . . . 5 ⊢ (𝑥 ∈ (1...1) → (𝜑 ↔ 𝜓))
14	10, 13	mpbiri 261	. . . 4 ⊢ (𝑥 ∈ (1...1) → 𝜑)
15	14	rgen 3078	. . 3 ⊢ ∀𝑥 ∈ (1...1)𝜑
16		peano2nn 12350	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
17	16	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℕ)
18	17	nncnd 12354	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℂ)
19		elfzuz 13655	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ∈ (ℤ_≥‘2))
20	19	ad2antrl 741	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ (ℤ_≥‘2))
21		eluz2nn 13018	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (ℤ_≥‘2) → 𝑦 ∈ ℕ)
22	20, 21	syl 18	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℕ)
23	22	nncnd 12354	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℂ)
24	22	nnne0d 12391	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≠ 0)
25	18, 23, 24	divcan2d 12098	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 · ((𝑘 + 1) / 𝑦)) = (𝑘 + 1))
26		simprr 785	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∥ (𝑘 + 1))
27	22	nnzd 12722	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℤ)
28	17	nnzd 12722	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℤ)
29		dvdsval2 16430	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ∧ (𝑘 + 1) ∈ ℤ) → (𝑦 ∥ (𝑘 + 1) ↔ ((𝑘 + 1) / 𝑦) ∈ ℤ))
30	27, 24, 28, 29	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ∥ (𝑘 + 1) ↔ ((𝑘 + 1) / 𝑦) ∈ ℤ))
31	26, 30	mpbid 235	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℤ)
32	23	mullidd 11330	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (1 · 𝑦) = 𝑦)
33		elfzle2 13664	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ≤ ((𝑘 + 1) − 1))
34	33	ad2antrl 741	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≤ ((𝑘 + 1) − 1))
35		nncn 12346	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
36	35	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑘 ∈ ℂ)
37		ax-1cn 11261	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
38		pncan 11566	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
39	36, 37, 38	sylancl 598	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) − 1) = 𝑘)
40	34, 39	breqtrd 5130	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≤ 𝑘)
41		nnz 12717	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
42	41	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑘 ∈ ℤ)
43		zleltp1 12750	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑦 ≤ 𝑘 ↔ 𝑦 < (𝑘 + 1)))
44	27, 42, 43	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ≤ 𝑘 ↔ 𝑦 < (𝑘 + 1)))
45	40, 44	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 < (𝑘 + 1))
46	32, 45	eqbrtrd 5126	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (1 · 𝑦) < (𝑘 + 1))
47		1red 11312	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 ∈ ℝ)
48	17	nnred 12353	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℝ)
49	22	nnred 12353	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℝ)
50	22	nngt0d 12390	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < 𝑦)
51		ltmuldiv 12193	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → ((1 · 𝑦) < (𝑘 + 1) ↔ 1 < ((𝑘 + 1) / 𝑦)))
52	47, 48, 49, 50, 51	syl112anc 1401	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((1 · 𝑦) < (𝑘 + 1) ↔ 1 < ((𝑘 + 1) / 𝑦)))
53	46, 52	mpbid 235	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 < ((𝑘 + 1) / 𝑦))
54		eluz2b1 13049	. . . . . . . . . . . 12 ⊢ (((𝑘 + 1) / 𝑦) ∈ (ℤ_≥‘2) ↔ (((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 1 < ((𝑘 + 1) / 𝑦)))
55	31, 53, 54	sylanbrc 595	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ (ℤ_≥‘2))
56		prmind.2	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
57		simplr 781	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ∀𝑥 ∈ (1...𝑘)𝜑)
58		fznn 13729	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℤ → (𝑦 ∈ (1...𝑘) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑘)))
59	42, 58	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ∈ (1...𝑘) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑘)))
60	22, 40, 59	mpbir2and 726	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ (1...𝑘))
61	56, 57, 60	rspcdva 3577	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝜒)
62		vex 3454	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
63		prmind.3	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜃))
64	62, 63	sbcie 3779	. . . . . . . . . . . . . 14 ⊢ ([𝑧 / 𝑥]𝜑 ↔ 𝜃)
65		dfsbcq 3740	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ([𝑧 / 𝑥]𝜑 ↔ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑))
66	64, 65	bitr3id 288	. . . . . . . . . . . . 13 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (𝜃 ↔ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑))
67	63	cbvralvw 3240	. . . . . . . . . . . . . 14 ⊢ (∀𝑥 ∈ (1...𝑘)𝜑 ↔ ∀𝑧 ∈ (1...𝑘)𝜃)
68	57, 67	sylib 221	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ∀𝑧 ∈ (1...𝑘)𝜃)
69	17	nnrpd 13165	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℝ⁺)
70	22	nnrpd 13165	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℝ⁺)
71	69, 70	rpdivcld 13184	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℝ⁺)
72	71	rpgt0d 13170	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < ((𝑘 + 1) / 𝑦))
73		elnnz 12706	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 + 1) / 𝑦) ∈ ℕ ↔ (((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 0 < ((𝑘 + 1) / 𝑦)))
74	31, 72, 73	sylanbrc 595	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℕ)
75	17	nnne0d 12391	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ≠ 0)
76	18, 75	dividd 12094	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / (𝑘 + 1)) = 1)
77		eluz2gt1 13050	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (ℤ_≥‘2) → 1 < 𝑦)
78	20, 77	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 < 𝑦)
79	76, 78	eqbrtrd 5126	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / (𝑘 + 1)) < 𝑦)
80	17	nngt0d 12390	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < (𝑘 + 1))
81		ltdiv23 12211	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 + 1) ∈ ℝ ∧ ((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1)) ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → (((𝑘 + 1) / (𝑘 + 1)) < 𝑦 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1)))
82	48, 48, 80, 49, 50, 81	syl122anc 1406	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (((𝑘 + 1) / (𝑘 + 1)) < 𝑦 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1)))
83	79, 82	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) < (𝑘 + 1))
84		zleltp1 12750	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((𝑘 + 1) / 𝑦) ≤ 𝑘 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1)))
85	31, 42, 84	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (((𝑘 + 1) / 𝑦) ≤ 𝑘 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1)))
86	83, 85	mpbird 260	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ≤ 𝑘)
87		fznn 13729	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℤ → (((𝑘 + 1) / 𝑦) ∈ (1...𝑘) ↔ (((𝑘 + 1) / 𝑦) ∈ ℕ ∧ ((𝑘 + 1) / 𝑦) ≤ 𝑘)))
88	42, 87	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (((𝑘 + 1) / 𝑦) ∈ (1...𝑘) ↔ (((𝑘 + 1) / 𝑦) ∈ ℕ ∧ ((𝑘 + 1) / 𝑦) ≤ 𝑘)))
89	74, 86, 88	mpbir2and 726	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ (1...𝑘))
90	66, 68, 89	rspcdva 3577	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [((𝑘 + 1) / 𝑦) / 𝑥]𝜑)
91	61, 90	jca 521	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑))
92	66	anbi2d 642	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ((𝜒 ∧ 𝜃) ↔ (𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑)))
93		ovex 7453	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 · 𝑧) ∈ V
94		prmind.4	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝜑 ↔ 𝜏))
95	93, 94	sbcie 3779	. . . . . . . . . . . . . . 15 ⊢ ([(𝑦 · 𝑧) / 𝑥]𝜑 ↔ 𝜏)
96		oveq2 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (𝑦 · 𝑧) = (𝑦 · ((𝑘 + 1) / 𝑦)))
97	96	sbceq1d 3743	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ([(𝑦 · 𝑧) / 𝑥]𝜑 ↔ [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑))
98	95, 97	bitr3id 288	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (𝜏 ↔ [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑))
99	92, 98	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (((𝜒 ∧ 𝜃) → 𝜏) ↔ ((𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)))
100	99	imbi2d 343	. . . . . . . . . . . 12 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ((𝑦 ∈ (ℤ_≥‘2) → ((𝜒 ∧ 𝜃) → 𝜏)) ↔ (𝑦 ∈ (ℤ_≥‘2) → ((𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑))))
101		prmind2.8	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → ((𝜒 ∧ 𝜃) → 𝜏))
102	101	expcom 419	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (ℤ_≥‘2) → (𝑦 ∈ (ℤ_≥‘2) → ((𝜒 ∧ 𝜃) → 𝜏)))
103	100, 102	vtoclga 3536	. . . . . . . . . . 11 ⊢ (((𝑘 + 1) / 𝑦) ∈ (ℤ_≥‘2) → (𝑦 ∈ (ℤ_≥‘2) → ((𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)))
104	55, 20, 91, 103	syl3c 67	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)
105	25, 104	sbceq1dd 3744	. . . . . . . . 9 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [(𝑘 + 1) / 𝑥]𝜑)
106	105	rexlimdvaa 3164	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑))
107		ralnex 3088	. . . . . . . . 9 ⊢ (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) ↔ ¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1))
108		simpl 488	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℕ)
109		elnnuz 13008	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ_≥‘1))
110	108, 109	sylib 221	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ (ℤ_≥‘1))
111		eluzp1p1 12996	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (𝑘 + 1) ∈ (ℤ_≥‘(1 + 1)))
112	110, 111	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈ (ℤ_≥‘(1 + 1)))
113		df-2 12408	. . . . . . . . . . . . 13 ⊢ 2 = (1 + 1)
114	113	fveq2i 6888	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘2) = (ℤ_≥‘(1 + 1))
115	112, 114	eleqtrrdi 2871	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈ (ℤ_≥‘2))
116		isprm3 16863	. . . . . . . . . . . 12 ⊢ ((𝑘 + 1) ∈ ℙ ↔ ((𝑘 + 1) ∈ (ℤ_≥‘2) ∧ ∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1)))
117	116	baibr 546	. . . . . . . . . . 11 ⊢ ((𝑘 + 1) ∈ (ℤ_≥‘2) → (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) ↔ (𝑘 + 1) ∈ ℙ))
118	115, 117	syl 18	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) ↔ (𝑘 + 1) ∈ ℙ))
119	56	cbvralvw 3240	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ (1...𝑘)𝜑 ↔ ∀𝑦 ∈ (1...𝑘)𝜒)
120	119	bilani 510	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑦 ∈ (1...𝑘)𝜒)
121	108	nncnd 12354	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℂ)
122	121, 37, 38	sylancl 598	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ((𝑘 + 1) − 1) = 𝑘)
123	122	oveq2d 7436	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (1...((𝑘 + 1) − 1)) = (1...𝑘))
124	120, 123	raleqtrrdv 3323	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒)
125		nfcv 2922	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝑘 + 1)
126		nfv 1946	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒
127		nfsbc1v 3758	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥[(𝑘 + 1) / 𝑥]𝜑
128	126, 127	nfim 1928	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 → [(𝑘 + 1) / 𝑥]𝜑)
129		oveq1 7427	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑘 + 1) → (𝑥 − 1) = ((𝑘 + 1) − 1))
130	129	oveq2d 7436	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑘 + 1) → (1...(𝑥 − 1)) = (1...((𝑘 + 1) − 1)))
131	130	raleqdv 3319	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑘 + 1) → (∀𝑦 ∈ (1...(𝑥 − 1))𝜒 ↔ ∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒))
132		sbceq1a 3749	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑘 + 1) → (𝜑 ↔ [(𝑘 + 1) / 𝑥]𝜑))
133	131, 132	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑘 + 1) → ((∀𝑦 ∈ (1...(𝑥 − 1))𝜒 → 𝜑) ↔ (∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 → [(𝑘 + 1) / 𝑥]𝜑)))
134		prmind2.7	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℙ ∧ ∀𝑦 ∈ (1...(𝑥 − 1))𝜒) → 𝜑)
135	134	ex 418	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℙ → (∀𝑦 ∈ (1...(𝑥 − 1))𝜒 → 𝜑))
136	125, 128, 133, 135	vtoclgaf 3535	. . . . . . . . . . 11 ⊢ ((𝑘 + 1) ∈ ℙ → (∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 → [(𝑘 + 1) / 𝑥]𝜑))
137	124, 136	syl5com 32	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ((𝑘 + 1) ∈ ℙ → [(𝑘 + 1) / 𝑥]𝜑))
138	118, 137	sylbid 243	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑))
139	107, 138	biimtrrid 246	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑))
140	106, 139	pm2.61d 181	. . . . . . 7 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → [(𝑘 + 1) / 𝑥]𝜑)
141	140	ex 418	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...𝑘)𝜑 → [(𝑘 + 1) / 𝑥]𝜑))
142		ralsnsg 4627	. . . . . . 7 ⊢ ((𝑘 + 1) ∈ ℕ → (∀𝑥 ∈ {(𝑘 + 1)}𝜑 ↔ [(𝑘 + 1) / 𝑥]𝜑))
143	16, 142	syl 18	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ {(𝑘 + 1)}𝜑 ↔ [(𝑘 + 1) / 𝑥]𝜑))
144	141, 143	sylibrd 262	. . . . 5 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...𝑘)𝜑 → ∀𝑥 ∈ {(𝑘 + 1)}𝜑))
145	144	ancld 560	. . . 4 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...𝑘)𝜑 → (∀𝑥 ∈ (1...𝑘)𝜑 ∧ ∀𝑥 ∈ {(𝑘 + 1)}𝜑)))
146		fzsuc 13708	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)}))
147	109, 146	sylbi 220	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)}))
148	147	raleqdv 3319	. . . . 5 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...(𝑘 + 1))𝜑 ↔ ∀𝑥 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})𝜑))
149		ralunb 4195	. . . . 5 ⊢ (∀𝑥 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})𝜑 ↔ (∀𝑥 ∈ (1...𝑘)𝜑 ∧ ∀𝑥 ∈ {(𝑘 + 1)}𝜑))
150	148, 149	bitrdi 290	. . . 4 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...(𝑘 + 1))𝜑 ↔ (∀𝑥 ∈ (1...𝑘)𝜑 ∧ ∀𝑥 ∈ {(𝑘 + 1)}𝜑)))
151	145, 150	sylibrd 262	. . 3 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...𝑘)𝜑 → ∀𝑥 ∈ (1...(𝑘 + 1))𝜑))
152	3, 5, 7, 9, 15, 151	nnind 12356	. 2 ⊢ (𝐴 ∈ ℕ → ∀𝑥 ∈ (1...𝐴)𝜑)
153		elfz1end 13691	. . 3 ⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈ (1...𝐴))
154	153	biimpi 219	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ (1...𝐴))
155	1, 152, 154	rspcdva 3577	1 ⊢ (𝐴 ∈ ℕ → 𝜂)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 [wsbc 3738 ∪ cun 4149 {csn 4584 class class class wbr 5102 ‘cfv 6538 (class class class)co 7420 ℂcc 11201 ℝcr 11202 0cc0 11203 1c1 11204 + caddc 11206 · cmul 11208 < clt 11346 ≤ cle 11347 − cmin 11544 / cdiv 11976 ℕcn 12338 2c2 12400 ℤcz 12696 ℤ_≥cuz 12968 ...cfz 13642 ∥ cdvds 16427 ℙcprime 16851

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11259 ax-resscn 11260 ax-1cn 11261 ax-icn 11262 ax-addcl 11263 ax-addrcl 11264 ax-mulcl 11265 ax-mulrcl 11266 ax-mulcom 11267 ax-addass 11268 ax-mulass 11269 ax-distr 11270 ax-i2m1 11271 ax-1ne0 11272 ax-1rid 11273 ax-rnegex 11274 ax-rrecex 11275 ax-cnre 11276 ax-pre-lttri 11277 ax-pre-lttrn 11278 ax-pre-ltadd 11279 ax-pre-mulgt0 11280 ax-pre-sup 11281

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8302 df-wrecs 8333 df-recs 8382 df-rdg 8421 df-1o 8479 df-2o 8480 df-er 8720 df-en 8977 df-dom 8978 df-sdom 8979 df-fin 8980 df-sup 9437 df-pnf 11348 df-mnf 11349 df-xr 11350 df-ltxr 11351 df-le 11352 df-sub 11546 df-neg 11547 df-div 11977 df-nn 12339 df-2 12408 df-3 12409 df-n0 12610 df-z 12697 df-uz 12969 df-rp 13124 df-fz 13643 df-seq 14148 df-exp 14208 df-cj 15271 df-re 15272 df-im 15273 df-sqrt 15407 df-abs 15408 df-dvds 16428 df-prm 16852

This theorem is used by: prmind 16866 4sqlem19 17146

W3C validator