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

Theorem prmind2 15598
Description: A variation on prmind 15599 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.
StepHypRef Expression
1 prmind.5 . 2 (𝑥 = 𝐴 → (𝜑𝜂))
2 oveq2 6799 . . . 4 (𝑛 = 1 → (1...𝑛) = (1...1))
32raleqdv 3293 . . 3 (𝑛 = 1 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...1)𝜑))
4 oveq2 6799 . . . 4 (𝑛 = 𝑘 → (1...𝑛) = (1...𝑘))
54raleqdv 3293 . . 3 (𝑛 = 𝑘 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...𝑘)𝜑))
6 oveq2 6799 . . . 4 (𝑛 = (𝑘 + 1) → (1...𝑛) = (1...(𝑘 + 1)))
76raleqdv 3293 . . 3 (𝑛 = (𝑘 + 1) → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...(𝑘 + 1))𝜑))
8 oveq2 6799 . . . 4 (𝑛 = 𝐴 → (1...𝑛) = (1...𝐴))
98raleqdv 3293 . . 3 (𝑛 = 𝐴 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...𝐴)𝜑))
10 prmind.6 . . . . 5 𝜓
11 elfz1eq 12552 . . . . . 6 (𝑥 ∈ (1...1) → 𝑥 = 1)
12 prmind.1 . . . . . 6 (𝑥 = 1 → (𝜑𝜓))
1311, 12syl 17 . . . . 5 (𝑥 ∈ (1...1) → (𝜑𝜓))
1410, 13mpbiri 248 . . . 4 (𝑥 ∈ (1...1) → 𝜑)
1514rgen 3071 . . 3 𝑥 ∈ (1...1)𝜑
16 peano2nn 11232 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
1716ad2antrr 705 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℕ)
1817nncnd 11236 . . . . . . . . . . 11 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℂ)
19 elfzuz 12538 . . . . . . . . . . . . . 14 (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ∈ (ℤ‘2))
2019ad2antrl 707 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ (ℤ‘2))
21 eluz2nn 11926 . . . . . . . . . . . . 13 (𝑦 ∈ (ℤ‘2) → 𝑦 ∈ ℕ)
2220, 21syl 17 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℕ)
2322nncnd 11236 . . . . . . . . . . 11 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℂ)
2422nnne0d 11265 . . . . . . . . . . 11 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≠ 0)
2518, 23, 24divcan2d 11003 . . . . . . . . . 10 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 · ((𝑘 + 1) / 𝑦)) = (𝑘 + 1))
26 simprr 756 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∥ (𝑘 + 1))
2722nnzd 11681 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℤ)
2817nnzd 11681 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℤ)
29 dvdsval2 15185 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ∧ (𝑘 + 1) ∈ ℤ) → (𝑦 ∥ (𝑘 + 1) ↔ ((𝑘 + 1) / 𝑦) ∈ ℤ))
3027, 24, 28, 29syl3anc 1476 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ∥ (𝑘 + 1) ↔ ((𝑘 + 1) / 𝑦) ∈ ℤ))
3126, 30mpbid 222 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℤ)
3223mulid2d 10258 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (1 · 𝑦) = 𝑦)
33 elfzle2 12545 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ≤ ((𝑘 + 1) − 1))
3433ad2antrl 707 . . . . . . . . . . . . . . . 16 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≤ ((𝑘 + 1) − 1))
35 nncn 11228 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
3635ad2antrr 705 . . . . . . . . . . . . . . . . 17 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑘 ∈ ℂ)
37 ax-1cn 10194 . . . . . . . . . . . . . . . . 17 1 ∈ ℂ
38 pncan 10487 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
3936, 37, 38sylancl 574 . . . . . . . . . . . . . . . 16 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) − 1) = 𝑘)
4034, 39breqtrd 4812 . . . . . . . . . . . . . . 15 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦𝑘)
41 nnz 11599 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
4241ad2antrr 705 . . . . . . . . . . . . . . . 16 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑘 ∈ ℤ)
43 zleltp1 11628 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑦𝑘𝑦 < (𝑘 + 1)))
4427, 42, 43syl2anc 573 . . . . . . . . . . . . . . 15 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦𝑘𝑦 < (𝑘 + 1)))
4540, 44mpbid 222 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 < (𝑘 + 1))
4632, 45eqbrtrd 4808 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (1 · 𝑦) < (𝑘 + 1))
47 1red 10255 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 ∈ ℝ)
4817nnred 11235 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℝ)
4922nnred 11235 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℝ)
5022nngt0d 11264 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < 𝑦)
51 ltmuldiv 11096 . . . . . . . . . . . . . 14 ((1 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → ((1 · 𝑦) < (𝑘 + 1) ↔ 1 < ((𝑘 + 1) / 𝑦)))
5247, 48, 49, 50, 51syl112anc 1480 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((1 · 𝑦) < (𝑘 + 1) ↔ 1 < ((𝑘 + 1) / 𝑦)))
5346, 52mpbid 222 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 < ((𝑘 + 1) / 𝑦))
54 eluz2b1 11960 . . . . . . . . . . . 12 (((𝑘 + 1) / 𝑦) ∈ (ℤ‘2) ↔ (((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 1 < ((𝑘 + 1) / 𝑦)))
5531, 53, 54sylanbrc 572 . . . . . . . . . . 11 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ (ℤ‘2))
56 prmind.2 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝜑𝜒))
57 simplr 752 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ∀𝑥 ∈ (1...𝑘)𝜑)
58 fznn 12608 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℤ → (𝑦 ∈ (1...𝑘) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑘)))
5942, 58syl 17 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ∈ (1...𝑘) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑘)))
6022, 40, 59mpbir2and 692 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ (1...𝑘))
6156, 57, 60rspcdva 3466 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝜒)
62 vex 3354 . . . . . . . . . . . . . . 15 𝑧 ∈ V
63 prmind.3 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → (𝜑𝜃))
6462, 63sbcie 3622 . . . . . . . . . . . . . 14 ([𝑧 / 𝑥]𝜑𝜃)
65 dfsbcq 3589 . . . . . . . . . . . . . 14 (𝑧 = ((𝑘 + 1) / 𝑦) → ([𝑧 / 𝑥]𝜑[((𝑘 + 1) / 𝑦) / 𝑥]𝜑))
6664, 65syl5bbr 274 . . . . . . . . . . . . 13 (𝑧 = ((𝑘 + 1) / 𝑦) → (𝜃[((𝑘 + 1) / 𝑦) / 𝑥]𝜑))
6763cbvralv 3320 . . . . . . . . . . . . . 14 (∀𝑥 ∈ (1...𝑘)𝜑 ↔ ∀𝑧 ∈ (1...𝑘)𝜃)
6857, 67sylib 208 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ∀𝑧 ∈ (1...𝑘)𝜃)
6917nnrpd 12066 . . . . . . . . . . . . . . . . 17 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℝ+)
7022nnrpd 12066 . . . . . . . . . . . . . . . . 17 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℝ+)
7169, 70rpdivcld 12085 . . . . . . . . . . . . . . . 16 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℝ+)
7271rpgt0d 12071 . . . . . . . . . . . . . . 15 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < ((𝑘 + 1) / 𝑦))
73 elnnz 11587 . . . . . . . . . . . . . . 15 (((𝑘 + 1) / 𝑦) ∈ ℕ ↔ (((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 0 < ((𝑘 + 1) / 𝑦)))
7431, 72, 73sylanbrc 572 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℕ)
7517nnne0d 11265 . . . . . . . . . . . . . . . . . 18 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ≠ 0)
7618, 75dividd 10999 . . . . . . . . . . . . . . . . 17 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / (𝑘 + 1)) = 1)
77 eluz2b2 11962 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (ℤ‘2) ↔ (𝑦 ∈ ℕ ∧ 1 < 𝑦))
7877simprbi 484 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (ℤ‘2) → 1 < 𝑦)
7920, 78syl 17 . . . . . . . . . . . . . . . . 17 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 < 𝑦)
8076, 79eqbrtrd 4808 . . . . . . . . . . . . . . . 16 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / (𝑘 + 1)) < 𝑦)
8117nngt0d 11264 . . . . . . . . . . . . . . . . 17 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < (𝑘 + 1))
82 ltdiv23 11114 . . . . . . . . . . . . . . . . 17 (((𝑘 + 1) ∈ ℝ ∧ ((𝑘 + 1) ∈ ℝ ∧ 0 < (𝑘 + 1)) ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → (((𝑘 + 1) / (𝑘 + 1)) < 𝑦 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1)))
8348, 48, 81, 49, 50, 82syl122anc 1485 . . . . . . . . . . . . . . . 16 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (((𝑘 + 1) / (𝑘 + 1)) < 𝑦 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1)))
8480, 83mpbid 222 . . . . . . . . . . . . . . 15 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) < (𝑘 + 1))
85 zleltp1 11628 . . . . . . . . . . . . . . . 16 ((((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((𝑘 + 1) / 𝑦) ≤ 𝑘 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1)))
8631, 42, 85syl2anc 573 . . . . . . . . . . . . . . 15 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (((𝑘 + 1) / 𝑦) ≤ 𝑘 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1)))
8784, 86mpbird 247 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ≤ 𝑘)
88 fznn 12608 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℤ → (((𝑘 + 1) / 𝑦) ∈ (1...𝑘) ↔ (((𝑘 + 1) / 𝑦) ∈ ℕ ∧ ((𝑘 + 1) / 𝑦) ≤ 𝑘)))
8942, 88syl 17 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (((𝑘 + 1) / 𝑦) ∈ (1...𝑘) ↔ (((𝑘 + 1) / 𝑦) ∈ ℕ ∧ ((𝑘 + 1) / 𝑦) ≤ 𝑘)))
9074, 87, 89mpbir2and 692 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ (1...𝑘))
9166, 68, 90rspcdva 3466 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [((𝑘 + 1) / 𝑦) / 𝑥]𝜑)
9261, 91jca 501 . . . . . . . . . . 11 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝜒[((𝑘 + 1) / 𝑦) / 𝑥]𝜑))
9366anbi2d 614 . . . . . . . . . . . . . 14 (𝑧 = ((𝑘 + 1) / 𝑦) → ((𝜒𝜃) ↔ (𝜒[((𝑘 + 1) / 𝑦) / 𝑥]𝜑)))
94 ovex 6821 . . . . . . . . . . . . . . . 16 (𝑦 · 𝑧) ∈ V
95 prmind.4 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑦 · 𝑧) → (𝜑𝜏))
9694, 95sbcie 3622 . . . . . . . . . . . . . . 15 ([(𝑦 · 𝑧) / 𝑥]𝜑𝜏)
97 oveq2 6799 . . . . . . . . . . . . . . . 16 (𝑧 = ((𝑘 + 1) / 𝑦) → (𝑦 · 𝑧) = (𝑦 · ((𝑘 + 1) / 𝑦)))
9897sbceq1d 3592 . . . . . . . . . . . . . . 15 (𝑧 = ((𝑘 + 1) / 𝑦) → ([(𝑦 · 𝑧) / 𝑥]𝜑[(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑))
9996, 98syl5bbr 274 . . . . . . . . . . . . . 14 (𝑧 = ((𝑘 + 1) / 𝑦) → (𝜏[(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑))
10093, 99imbi12d 333 . . . . . . . . . . . . 13 (𝑧 = ((𝑘 + 1) / 𝑦) → (((𝜒𝜃) → 𝜏) ↔ ((𝜒[((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)))
101100imbi2d 329 . . . . . . . . . . . 12 (𝑧 = ((𝑘 + 1) / 𝑦) → ((𝑦 ∈ (ℤ‘2) → ((𝜒𝜃) → 𝜏)) ↔ (𝑦 ∈ (ℤ‘2) → ((𝜒[((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑))))
102 prmind2.8 . . . . . . . . . . . . 13 ((𝑦 ∈ (ℤ‘2) ∧ 𝑧 ∈ (ℤ‘2)) → ((𝜒𝜃) → 𝜏))
103102expcom 398 . . . . . . . . . . . 12 (𝑧 ∈ (ℤ‘2) → (𝑦 ∈ (ℤ‘2) → ((𝜒𝜃) → 𝜏)))
104101, 103vtoclga 3423 . . . . . . . . . . 11 (((𝑘 + 1) / 𝑦) ∈ (ℤ‘2) → (𝑦 ∈ (ℤ‘2) → ((𝜒[((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)))
10555, 20, 92, 104syl3c 66 . . . . . . . . . 10 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)
10625, 105sbceq1dd 3593 . . . . . . . . 9 (((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [(𝑘 + 1) / 𝑥]𝜑)
107106rexlimdvaa 3180 . . . . . . . 8 ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑))
108 ralnex 3141 . . . . . . . . 9 (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) ↔ ¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1))
109 simpl 468 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℕ)
110 elnnuz 11924 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ‘1))
111109, 110sylib 208 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ (ℤ‘1))
112 eluzp1p1 11912 . . . . . . . . . . . . 13 (𝑘 ∈ (ℤ‘1) → (𝑘 + 1) ∈ (ℤ‘(1 + 1)))
113111, 112syl 17 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈ (ℤ‘(1 + 1)))
114 df-2 11279 . . . . . . . . . . . . 13 2 = (1 + 1)
115114fveq2i 6333 . . . . . . . . . . . 12 (ℤ‘2) = (ℤ‘(1 + 1))
116113, 115syl6eleqr 2861 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈ (ℤ‘2))
117 isprm3 15596 . . . . . . . . . . . 12 ((𝑘 + 1) ∈ ℙ ↔ ((𝑘 + 1) ∈ (ℤ‘2) ∧ ∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1)))
118117baibr 526 . . . . . . . . . . 11 ((𝑘 + 1) ∈ (ℤ‘2) → (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) ↔ (𝑘 + 1) ∈ ℙ))
119116, 118syl 17 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) ↔ (𝑘 + 1) ∈ ℙ))
120 simpr 471 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑥 ∈ (1...𝑘)𝜑)
12156cbvralv 3320 . . . . . . . . . . . . 13 (∀𝑥 ∈ (1...𝑘)𝜑 ↔ ∀𝑦 ∈ (1...𝑘)𝜒)
122120, 121sylib 208 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑦 ∈ (1...𝑘)𝜒)
123109nncnd 11236 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℂ)
124123, 37, 38sylancl 574 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ((𝑘 + 1) − 1) = 𝑘)
125124oveq2d 6807 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (1...((𝑘 + 1) − 1)) = (1...𝑘))
126125raleqdv 3293 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 ↔ ∀𝑦 ∈ (1...𝑘)𝜒))
127122, 126mpbird 247 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒)
128 nfcv 2913 . . . . . . . . . . . 12 𝑥(𝑘 + 1)
129 nfv 1995 . . . . . . . . . . . . 13 𝑥𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒
130 nfsbc1v 3607 . . . . . . . . . . . . 13 𝑥[(𝑘 + 1) / 𝑥]𝜑
131129, 130nfim 1977 . . . . . . . . . . . 12 𝑥(∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒[(𝑘 + 1) / 𝑥]𝜑)
132 oveq1 6798 . . . . . . . . . . . . . . 15 (𝑥 = (𝑘 + 1) → (𝑥 − 1) = ((𝑘 + 1) − 1))
133132oveq2d 6807 . . . . . . . . . . . . . 14 (𝑥 = (𝑘 + 1) → (1...(𝑥 − 1)) = (1...((𝑘 + 1) − 1)))
134133raleqdv 3293 . . . . . . . . . . . . 13 (𝑥 = (𝑘 + 1) → (∀𝑦 ∈ (1...(𝑥 − 1))𝜒 ↔ ∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒))
135 sbceq1a 3598 . . . . . . . . . . . . 13 (𝑥 = (𝑘 + 1) → (𝜑[(𝑘 + 1) / 𝑥]𝜑))
136134, 135imbi12d 333 . . . . . . . . . . . 12 (𝑥 = (𝑘 + 1) → ((∀𝑦 ∈ (1...(𝑥 − 1))𝜒𝜑) ↔ (∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒[(𝑘 + 1) / 𝑥]𝜑)))
137 prmind2.7 . . . . . . . . . . . . 13 ((𝑥 ∈ ℙ ∧ ∀𝑦 ∈ (1...(𝑥 − 1))𝜒) → 𝜑)
138137ex 397 . . . . . . . . . . . 12 (𝑥 ∈ ℙ → (∀𝑦 ∈ (1...(𝑥 − 1))𝜒𝜑))
139128, 131, 136, 138vtoclgaf 3422 . . . . . . . . . . 11 ((𝑘 + 1) ∈ ℙ → (∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒[(𝑘 + 1) / 𝑥]𝜑))
140127, 139syl5com 31 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → ((𝑘 + 1) ∈ ℙ → [(𝑘 + 1) / 𝑥]𝜑))
141119, 140sylbid 230 . . . . . . . . 9 ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑))
142108, 141syl5bir 233 . . . . . . . 8 ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → (¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑))
143107, 142pm2.61d 171 . . . . . . 7 ((𝑘 ∈ ℕ ∧ ∀𝑥 ∈ (1...𝑘)𝜑) → [(𝑘 + 1) / 𝑥]𝜑)
144143ex 397 . . . . . 6 (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...𝑘)𝜑[(𝑘 + 1) / 𝑥]𝜑))
145 ralsnsg 4354 . . . . . . 7 ((𝑘 + 1) ∈ ℕ → (∀𝑥 ∈ {(𝑘 + 1)}𝜑[(𝑘 + 1) / 𝑥]𝜑))
14616, 145syl 17 . . . . . 6 (𝑘 ∈ ℕ → (∀𝑥 ∈ {(𝑘 + 1)}𝜑[(𝑘 + 1) / 𝑥]𝜑))
147144, 146sylibrd 249 . . . . 5 (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...𝑘)𝜑 → ∀𝑥 ∈ {(𝑘 + 1)}𝜑))
148147ancld 540 . . . 4 (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...𝑘)𝜑 → (∀𝑥 ∈ (1...𝑘)𝜑 ∧ ∀𝑥 ∈ {(𝑘 + 1)}𝜑)))
149 fzsuc 12588 . . . . . . 7 (𝑘 ∈ (ℤ‘1) → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)}))
150110, 149sylbi 207 . . . . . 6 (𝑘 ∈ ℕ → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)}))
151150raleqdv 3293 . . . . 5 (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...(𝑘 + 1))𝜑 ↔ ∀𝑥 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})𝜑))
152 ralunb 3945 . . . . 5 (∀𝑥 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})𝜑 ↔ (∀𝑥 ∈ (1...𝑘)𝜑 ∧ ∀𝑥 ∈ {(𝑘 + 1)}𝜑))
153151, 152syl6bb 276 . . . 4 (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...(𝑘 + 1))𝜑 ↔ (∀𝑥 ∈ (1...𝑘)𝜑 ∧ ∀𝑥 ∈ {(𝑘 + 1)}𝜑)))
154148, 153sylibrd 249 . . 3 (𝑘 ∈ ℕ → (∀𝑥 ∈ (1...𝑘)𝜑 → ∀𝑥 ∈ (1...(𝑘 + 1))𝜑))
1553, 5, 7, 9, 15, 154nnind 11238 . 2 (𝐴 ∈ ℕ → ∀𝑥 ∈ (1...𝐴)𝜑)
156 elfz1end 12571 . . 3 (𝐴 ∈ ℕ ↔ 𝐴 ∈ (1...𝐴))
157156biimpi 206 . 2 (𝐴 ∈ ℕ → 𝐴 ∈ (1...𝐴))
1581, 155, 157rspcdva 3466 1 (𝐴 ∈ ℕ → 𝜂)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  [wsbc 3587  cun 3721  {csn 4316   class class class wbr 4786  cfv 6029  (class class class)co 6791  cc 10134  cr 10135  0cc0 10136  1c1 10137   + caddc 10139   · cmul 10141   < clt 10274  cle 10275  cmin 10466   / cdiv 10884  cn 11220  2c2 11270  cz 11577  cuz 11886  ...cfz 12526  cdvds 15182  cprime 15585
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7094  ax-cnex 10192  ax-resscn 10193  ax-1cn 10194  ax-icn 10195  ax-addcl 10196  ax-addrcl 10197  ax-mulcl 10198  ax-mulrcl 10199  ax-mulcom 10200  ax-addass 10201  ax-mulass 10202  ax-distr 10203  ax-i2m1 10204  ax-1ne0 10205  ax-1rid 10206  ax-rnegex 10207  ax-rrecex 10208  ax-cnre 10209  ax-pre-lttri 10210  ax-pre-lttrn 10211  ax-pre-ltadd 10212  ax-pre-mulgt0 10213  ax-pre-sup 10214
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5821  df-ord 5867  df-on 5868  df-lim 5869  df-suc 5870  df-iota 5992  df-fun 6031  df-fn 6032  df-f 6033  df-f1 6034  df-fo 6035  df-f1o 6036  df-fv 6037  df-riota 6752  df-ov 6794  df-oprab 6795  df-mpt2 6796  df-om 7211  df-1st 7313  df-2nd 7314  df-wrecs 7557  df-recs 7619  df-rdg 7657  df-1o 7711  df-2o 7712  df-er 7894  df-en 8108  df-dom 8109  df-sdom 8110  df-fin 8111  df-sup 8502  df-pnf 10276  df-mnf 10277  df-xr 10278  df-ltxr 10279  df-le 10280  df-sub 10468  df-neg 10469  df-div 10885  df-nn 11221  df-2 11279  df-3 11280  df-n0 11493  df-z 11578  df-uz 11887  df-rp 12029  df-fz 12527  df-seq 13002  df-exp 13061  df-cj 14040  df-re 14041  df-im 14042  df-sqrt 14176  df-abs 14177  df-dvds 15183  df-prm 15586
This theorem is referenced by:  prmind  15599  4sqlem19  15867
  Copyright terms: Public domain W3C validator