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 16889

Description: A variation on prmind 16890 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 7451	. . . 4 ⊢ (𝑛 = 1 → (1...𝑛) = (1...1))
3	2	raleqdv 3323	. . 3 ⊢ (𝑛 = 1 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...1)𝜑))
4		oveq2 7451	. . . 4 ⊢ (𝑛 = 𝑘 → (1...𝑛) = (1...𝑘))
5	4	raleqdv 3323	. . 3 ⊢ (𝑛 = 𝑘 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...𝑘)𝜑))
6		oveq2 7451	. . . 4 ⊢ (𝑛 = (𝑘 + 1) → (1...𝑛) = (1...(𝑘 + 1)))
7	6	raleqdv 3323	. . 3 ⊢ (𝑛 = (𝑘 + 1) → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...(𝑘 + 1))𝜑))
8		oveq2 7451	. . . 4 ⊢ (𝑛 = 𝐴 → (1...𝑛) = (1...𝐴))
9	8	raleqdv 3323	. . 3 ⊢ (𝑛 = 𝐴 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...𝐴)𝜑))
10		prmind.6	. . . . 5 ⊢ 𝜓
11		elfz1eq 13695	. . . . . 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 3082	. . 3 ⊢ ∀𝑥 ∈ (1...1)𝜑
16		peano2nn 12374	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
17	16	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℕ)
18	17	nncnd 12378	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℂ)
19		elfzuz 13679	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ∈ (ℤ_≥‘2))
20	19	ad2antrl 741	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ (ℤ_≥‘2))
21		eluz2nn 13042	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (ℤ_≥‘2) → 𝑦 ∈ ℕ)
22	20, 21	syl 18	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℕ)
23	22	nncnd 12378	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℂ)
24	22	nnne0d 12415	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≠ 0)
25	18, 23, 24	divcan2d 12122	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 · ((𝑘 + 1) / 𝑦)) = (𝑘 + 1))
26		simprr 785	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∥ (𝑘 + 1))
27	22	nnzd 12746	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℤ)
28	17	nnzd 12746	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℤ)
29		dvdsval2 16454	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ∧ (𝑘 + 1) ∈ ℤ) → (𝑦 ∥ (𝑘 + 1) ↔ ((𝑘 + 1) / 𝑦) ∈ ℤ))
30	27, 24, 28, 29	syl3anc 1399	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ∥ (𝑘 + 1) ↔ ((𝑘 + 1) / 𝑦) ∈ ℤ))
31	26, 30	mpbid 235	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℤ)
32	23	mullidd 11354	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (1 · 𝑦) = 𝑦)
33		elfzle2 13688	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ≤ ((𝑘 + 1) − 1))
34	33	ad2antrl 741	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≤ ((𝑘 + 1) − 1))
35		nncn 12370	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
36	35	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑘 ∈ ℂ)
37		ax-1cn 11285	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
38		pncan 11590	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
39	36, 37, 38	sylancl 598	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) − 1) = 𝑘)
40	34, 39	breqtrd 5134	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≤ 𝑘)
41		nnz 12741	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
42	41	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑘 ∈ ℤ)
43		zleltp1 12774	. . . . . . . . . . . . . . . 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 5130	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (1 · 𝑦) < (𝑘 + 1))
47		1red 11336	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 ∈ ℝ)
48	17	nnred 12377	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℝ)
49	22	nnred 12377	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℝ)
50	22	nngt0d 12414	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < 𝑦)
51		ltmuldiv 12217	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → ((1 · 𝑦) < (𝑘 + 1) ↔ 1 < ((𝑘 + 1) / 𝑦)))
52	47, 48, 49, 50, 51	syl112anc 1402	. . . . . . . . . . . . 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 13073	. . . . . . . . . . . 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 13753	. . . . . . . . . . . . . . 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 3581	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝜒)
62		vex 3458	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
63		prmind.3	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜃))
64	62, 63	sbcie 3783	. . . . . . . . . . . . . 14 ⊢ ([𝑧 / 𝑥]𝜑 ↔ 𝜃)
65		dfsbcq 3744	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ([𝑧 / 𝑥]𝜑 ↔ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑))
66	64, 65	bitr3id 288	. . . . . . . . . . . . 13 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (𝜃 ↔ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑))
67	63	cbvralvw 3244	. . . . . . . . . . . . . 14 ⊢ (∀𝑥 ∈ (1...𝑘)𝜑 ↔ ∀𝑧 ∈ (1...𝑘)𝜃)
68	57, 67	sylib 221	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ∀𝑧 ∈ (1...𝑘)𝜃)
69	17	nnrpd 13189	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℝ⁺)
70	22	nnrpd 13189	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℝ⁺)
71	69, 70	rpdivcld 13208	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℝ⁺)
72	71	rpgt0d 13194	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < ((𝑘 + 1) / 𝑦))
73		elnnz 12730	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 + 1) / 𝑦) ∈ ℕ ↔ (((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 0 < ((𝑘 + 1) / 𝑦)))
74	31, 72, 73	sylanbrc 595	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℕ)
75	17	nnne0d 12415	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ≠ 0)
76	18, 75	dividd 12118	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / (𝑘 + 1)) = 1)
77		eluz2gt1 13074	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (ℤ_≥‘2) → 1 < 𝑦)
78	20, 77	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 < 𝑦)
79	76, 78	eqbrtrd 5130	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / (𝑘 + 1)) < 𝑦)
80	17	nngt0d 12414	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < (𝑘 + 1))
81		ltdiv23 12235	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 + 1) ∈ ℝ ∧ ((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1)) ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → (((𝑘 + 1) / (𝑘 + 1)) < 𝑦 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1)))
82	48, 48, 80, 49, 50, 81	syl122anc 1407	. . . . . . . . . . . . . . . 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 12774	. . . . . . . . . . . . . . . 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 13753	. . . . . . . . . . . . . . 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 3581	. . . . . . . . . . . 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 7476	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 · 𝑧) ∈ V
94		prmind.4	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝜑 ↔ 𝜏))
95	93, 94	sbcie 3783	. . . . . . . . . . . . . . 15 ⊢ ([(𝑦 · 𝑧) / 𝑥]𝜑 ↔ 𝜏)
96		oveq2 7451	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (𝑦 · 𝑧) = (𝑦 · ((𝑘 + 1) / 𝑦)))
97	96	sbceq1d 3747	. . . . . . . . . . . . . . 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 3540	. . . . . . . . . . 11 ⊢ (((𝑘 + 1) / 𝑦) ∈ (ℤ_≥‘2) → (𝑦 ∈ (ℤ_≥‘2) → ((𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)))
104	55, 20, 91, 103	syl3c 67	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)
105	25, 104	sbceq1dd 3748	. . . . . . . . 9 ⊢ (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [(𝑘 + 1) / 𝑥]𝜑)
106	105	rexlimdvaa 3168	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑))
107		ralnex 3092	. . . . . . . . 9 ⊢ (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) ↔ ¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1))
108		simpl 488	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℕ)
109		elnnuz 13032	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ_≥‘1))
110	108, 109	sylib 221	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ (ℤ_≥‘1))
111		eluzp1p1 13020	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (𝑘 + 1) ∈ (ℤ_≥‘(1 + 1)))
112	110, 111	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈ (ℤ_≥‘(1 + 1)))
113		df-2 12432	. . . . . . . . . . . . 13 ⊢ 2 = (1 + 1)
114	113	fveq2i 6911	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘2) = (ℤ_≥‘(1 + 1))
115	112, 114	eleqtrrdi 2875	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈ (ℤ_≥‘2))
116		isprm3 16887	. . . . . . . . . . . 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 3244	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ (1...𝑘)𝜑 ↔ ∀𝑦 ∈ (1...𝑘)𝜒)
120	119	bilani 510	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑦 ∈ (1...𝑘)𝜒)
121	108	nncnd 12378	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℂ)
122	121, 37, 38	sylancl 598	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ((𝑘 + 1) − 1) = 𝑘)
123	122	oveq2d 7459	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (1...((𝑘 + 1) − 1)) = (1...𝑘))
124	120, 123	raleqtrrdv 3327	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒)
125		nfcv 2926	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝑘 + 1)
126		nfv 1949	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒
127		nfsbc1v 3762	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥[(𝑘 + 1) / 𝑥]𝜑
128	126, 127	nfim 1931	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 → [(𝑘 + 1) / 𝑥]𝜑)
129		oveq1 7450	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑘 + 1) → (𝑥 − 1) = ((𝑘 + 1) − 1))
130	129	oveq2d 7459	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑘 + 1) → (1...(𝑥 − 1)) = (1...((𝑘 + 1) − 1)))
131	130	raleqdv 3323	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑘 + 1) → (∀𝑦 ∈ (1...(𝑥 − 1))𝜒 ↔ ∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒))
132		sbceq1a 3753	. . . . . . . . . . . . 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 3539	. . . . . . . . . . 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 4631	. . . . . . 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 13732	. . . . . . 7 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)}))
147	109, 146	sylbi 220	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)}))
148	147	raleqdv 3323	. . . . 5 ⊢ (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...(𝑘 + 1))𝜑 ↔ ∀𝑥 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})𝜑))
149		ralunb 4198	. . . . 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 12380	. 2 ⊢ (𝐴 ∈ ℕ → ∀𝑥 ∈ (1...𝐴)𝜑)
153		elfz1end 13715	. . 3 ⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈ (1...𝐴))
154	153	biimpi 219	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ (1...𝐴))
155	1, 152, 154	rspcdva 3581	1 ⊢ (𝐴 ∈ ℕ → 𝜂)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 [wsbc 3742 ∪ cun 4152 {csn 4588 class class class wbr 5106 ‘cfv 6558 (class class class)co 7443 ℂcc 11225 ℝcr 11226 0cc0 11227 1c1 11228 + caddc 11230 · cmul 11232 < clt 11370 ≤ cle 11371 − cmin 11568 / cdiv 12000 ℕcn 12362 2c2 12424 ℤcz 12720 ℤ_≥cuz 12992 ...cfz 13666 ∥ cdvds 16451 ℙcprime 16875

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775 ax-cnex 11283 ax-resscn 11284 ax-1cn 11285 ax-icn 11286 ax-addcl 11287 ax-addrcl 11288 ax-mulcl 11289 ax-mulrcl 11290 ax-mulcom 11291 ax-addass 11292 ax-mulass 11293 ax-distr 11294 ax-i2m1 11295 ax-1ne0 11296 ax-1rid 11297 ax-rnegex 11298 ax-rrecex 11299 ax-cnre 11300 ax-pre-lttri 11301 ax-pre-lttrn 11302 ax-pre-ltadd 11303 ax-pre-mulgt0 11304 ax-pre-sup 11305

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6322 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-riota 7400 df-ov 7446 df-oprab 7447 df-mpo 7448 df-om 7902 df-1st 8025 df-2nd 8026 df-frecs 8327 df-wrecs 8358 df-recs 8407 df-rdg 8446 df-1o 8504 df-2o 8505 df-er 8745 df-en 9002 df-dom 9003 df-sdom 9004 df-fin 9005 df-sup 9461 df-pnf 11372 df-mnf 11373 df-xr 11374 df-ltxr 11375 df-le 11376 df-sub 11570 df-neg 11571 df-div 12001 df-nn 12363 df-2 12432 df-3 12433 df-n0 12634 df-z 12721 df-uz 12993 df-rp 13148 df-fz 13667 df-seq 14172 df-exp 14232 df-cj 15295 df-re 15296 df-im 15297 df-sqrt 15431 df-abs 15432 df-dvds 16452 df-prm 16876

This theorem is used by: prmind 16890 4sqlem19 17170

W3C validator