prmind2

Description: A variation on prmind assuming complete induction for primes. (Contributed by Mario Carneiro, 20-Jun-2015)

	Ref	Expression
Hypotheses	prmind.1	$⊢ x = 1 \to (φ \leftrightarrow ψ)$
	prmind.2	$⊢ x = y \to (φ \leftrightarrow χ)$
	prmind.3	$⊢ x = z \to (φ \leftrightarrow θ)$
	prmind.4	$⊢ x = y z \to (φ \leftrightarrow τ)$
	prmind.5	$⊢ x = A \to (φ \leftrightarrow η)$
	prmind.6	$⊢ ψ$
	prmind2.7	$⊢ (x \in ℙ \land \forall y \in (1 \dots x - 1) χ) \to φ$
	prmind2.8	$⊢ (y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to ((χ \land θ) \to τ)$
Assertion	prmind2	$⊢ A \in ℕ \to η$

Proof

Step	Hyp	Ref	Expression
1		prmind.1	$⊢ x = 1 \to (φ \leftrightarrow ψ)$
2		prmind.2	$⊢ x = y \to (φ \leftrightarrow χ)$
3		prmind.3	$⊢ x = z \to (φ \leftrightarrow θ)$
4		prmind.4	$⊢ x = y z \to (φ \leftrightarrow τ)$
5		prmind.5	$⊢ x = A \to (φ \leftrightarrow η)$
6		prmind.6	$⊢ ψ$
7		prmind2.7	$⊢ (x \in ℙ \land \forall y \in (1 \dots x - 1) χ) \to φ$
8		prmind2.8	$⊢ (y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to ((χ \land θ) \to τ)$
9		oveq2	$⊢ n = 1 \to (1 \dots n) = (1 \dots 1)$
10	9	raleqdv	$⊢ n = 1 \to (\forall x \in (1 \dots n) φ \leftrightarrow \forall x \in (1 \dots 1) φ)$
11		oveq2	$⊢ n = k \to (1 \dots n) = (1 \dots k)$
12	11	raleqdv	$⊢ n = k \to (\forall x \in (1 \dots n) φ \leftrightarrow \forall x \in (1 \dots k) φ)$
13		oveq2	$⊢ n = k + 1 \to (1 \dots n) = (1 \dots k + 1)$
14	13	raleqdv	$⊢ n = k + 1 \to (\forall x \in (1 \dots n) φ \leftrightarrow \forall x \in (1 \dots k + 1) φ)$
15		oveq2	$⊢ n = A \to (1 \dots n) = (1 \dots A)$
16	15	raleqdv	$⊢ n = A \to (\forall x \in (1 \dots n) φ \leftrightarrow \forall x \in (1 \dots A) φ)$
17		elfz1eq	$⊢ x \in (1 \dots 1) \to x = 1$
18	17 1	syl	$⊢ x \in (1 \dots 1) \to (φ \leftrightarrow ψ)$
19	6 18	mpbiri	$⊢ x \in (1 \dots 1) \to φ$
20	19	rgen	$⊢ \forall x \in (1 \dots 1) φ$
21		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
22	21	ad2antrr	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to k + 1 \in ℕ$
23	22	nncnd	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to k + 1 \in ℂ$
24		elfzuz	$⊢ y \in (2 \dots k + 1 - 1) \to y \in ℤ_{\geq 2}$
25	24	ad2antrl	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to y \in ℤ_{\geq 2}$
26		eluz2nn	$⊢ y \in ℤ_{\geq 2} \to y \in ℕ$
27	25 26	syl	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to y \in ℕ$
28	27	nncnd	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to y \in ℂ$
29	27	nnne0d	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to y \neq 0$
30	23 28 29	divcan2d	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to y (\frac{k + 1}{y}) = k + 1$
31		simprr	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to y ∥ (k + 1)$
32	27	nnzd	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to y \in ℤ$
33	22	nnzd	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to k + 1 \in ℤ$
34		dvdsval2	$⊢ (y \in ℤ \land y \neq 0 \land k + 1 \in ℤ) \to (y ∥ (k + 1) \leftrightarrow \frac{k + 1}{y} \in ℤ)$
35	32 29 33 34	syl3anc	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to (y ∥ (k + 1) \leftrightarrow \frac{k + 1}{y} \in ℤ)$
36	31 35	mpbid	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to \frac{k + 1}{y} \in ℤ$
37	28	mullidd	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to 1 y = y$
38		elfzle2	$⊢ y \in (2 \dots k + 1 - 1) \to y \leq k + 1 - 1$
39	38	ad2antrl	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to y \leq k + 1 - 1$
40		nncn	$⊢ k \in ℕ \to k \in ℂ$
41	40	ad2antrr	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to k \in ℂ$
42		ax-1cn	$⊢ 1 \in ℂ$
43		pncan	$⊢ (k \in ℂ \land 1 \in ℂ) \to k + 1 - 1 = k$
44	41 42 43	sylancl	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to k + 1 - 1 = k$
45	39 44	breqtrd	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to y \leq k$
46		nnz	$⊢ k \in ℕ \to k \in ℤ$
47	46	ad2antrr	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to k \in ℤ$
48		zleltp1	$⊢ (y \in ℤ \land k \in ℤ) \to (y \leq k \leftrightarrow y < k + 1)$
49	32 47 48	syl2anc	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to (y \leq k \leftrightarrow y < k + 1)$
50	45 49	mpbid	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to y < k + 1$
51	37 50	eqbrtrd	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to 1 y < k + 1$
52		1red	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to 1 \in ℝ$
53	22	nnred	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to k + 1 \in ℝ$
54	27	nnred	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to y \in ℝ$
55	27	nngt0d	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to 0 < y$
56		ltmuldiv	$⊢ (1 \in ℝ \land k + 1 \in ℝ \land (y \in ℝ \land 0 < y)) \to (1 y < k + 1 \leftrightarrow 1 < \frac{k + 1}{y})$
57	52 53 54 55 56	syl112anc	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to (1 y < k + 1 \leftrightarrow 1 < \frac{k + 1}{y})$
58	51 57	mpbid	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to 1 < \frac{k + 1}{y}$
59		eluz2b1	$⊢ \frac{k + 1}{y} \in ℤ_{\geq 2} \leftrightarrow (\frac{k + 1}{y} \in ℤ \land 1 < \frac{k + 1}{y})$
60	36 58 59	sylanbrc	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to \frac{k + 1}{y} \in ℤ_{\geq 2}$
61		simplr	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to \forall x \in (1 \dots k) φ$
62		fznn	$⊢ k \in ℤ \to (y \in (1 \dots k) \leftrightarrow (y \in ℕ \land y \leq k))$
63	47 62	syl	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to (y \in (1 \dots k) \leftrightarrow (y \in ℕ \land y \leq k))$
64	27 45 63	mpbir2and	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to y \in (1 \dots k)$
65	2 61 64	rspcdva	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to χ$
66		vex	$⊢ z \in V$
67	66 3	sbcie	$⊢ \underset{˙}{[} z / x \underset{˙}{]} φ \leftrightarrow θ$
68		dfsbcq	$⊢ z = \frac{k + 1}{y} \to (\underset{˙}{[} z / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (\frac{k + 1}{y}) / x \underset{˙}{]} φ)$
69	67 68	bitr3id	$⊢ z = \frac{k + 1}{y} \to (θ \leftrightarrow \underset{˙}{[} (\frac{k + 1}{y}) / x \underset{˙}{]} φ)$
70	3	cbvralvw	$⊢ \forall x \in (1 \dots k) φ \leftrightarrow \forall z \in (1 \dots k) θ$
71	61 70	sylib	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to \forall z \in (1 \dots k) θ$
72	22	nnrpd	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to k + 1 \in ℝ^{+}$
73	27	nnrpd	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to y \in ℝ^{+}$
74	72 73	rpdivcld	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to \frac{k + 1}{y} \in ℝ^{+}$
75	74	rpgt0d	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to 0 < \frac{k + 1}{y}$
76		elnnz	$⊢ \frac{k + 1}{y} \in ℕ \leftrightarrow (\frac{k + 1}{y} \in ℤ \land 0 < \frac{k + 1}{y})$
77	36 75 76	sylanbrc	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to \frac{k + 1}{y} \in ℕ$
78	22	nnne0d	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to k + 1 \neq 0$
79	23 78	dividd	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to \frac{k + 1}{k + 1} = 1$
80		eluz2gt1	$⊢ y \in ℤ_{\geq 2} \to 1 < y$
81	25 80	syl	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to 1 < y$
82	79 81	eqbrtrd	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to \frac{k + 1}{k + 1} < y$
83	22	nngt0d	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to 0 < k + 1$
84		ltdiv23	$⊢ (k + 1 \in ℝ \land (k + 1 \in ℝ \land 0 < k + 1) \land (y \in ℝ \land 0 < y)) \to (\frac{k + 1}{k + 1} < y \leftrightarrow \frac{k + 1}{y} < k + 1)$
85	53 53 83 54 55 84	syl122anc	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to (\frac{k + 1}{k + 1} < y \leftrightarrow \frac{k + 1}{y} < k + 1)$
86	82 85	mpbid	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to \frac{k + 1}{y} < k + 1$
87		zleltp1	$⊢ (\frac{k + 1}{y} \in ℤ \land k \in ℤ) \to (\frac{k + 1}{y} \leq k \leftrightarrow \frac{k + 1}{y} < k + 1)$
88	36 47 87	syl2anc	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to (\frac{k + 1}{y} \leq k \leftrightarrow \frac{k + 1}{y} < k + 1)$
89	86 88	mpbird	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to \frac{k + 1}{y} \leq k$
90		fznn	$⊢ k \in ℤ \to (\frac{k + 1}{y} \in (1 \dots k) \leftrightarrow (\frac{k + 1}{y} \in ℕ \land \frac{k + 1}{y} \leq k))$
91	47 90	syl	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to (\frac{k + 1}{y} \in (1 \dots k) \leftrightarrow (\frac{k + 1}{y} \in ℕ \land \frac{k + 1}{y} \leq k))$
92	77 89 91	mpbir2and	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to \frac{k + 1}{y} \in (1 \dots k)$
93	69 71 92	rspcdva	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to \underset{˙}{[} (\frac{k + 1}{y}) / x \underset{˙}{]} φ$
94	65 93	jca	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to (χ \land \underset{˙}{[} (\frac{k + 1}{y}) / x \underset{˙}{]} φ)$
95	69	anbi2d	$⊢ z = \frac{k + 1}{y} \to ((χ \land θ) \leftrightarrow (χ \land \underset{˙}{[} (\frac{k + 1}{y}) / x \underset{˙}{]} φ))$
96		ovex	$⊢ y z \in V$
97	96 4	sbcie	$⊢ \underset{˙}{[} y z / x \underset{˙}{]} φ \leftrightarrow τ$
98		oveq2	$⊢ z = \frac{k + 1}{y} \to y z = y (\frac{k + 1}{y})$
99	98	sbceq1d	$⊢ z = \frac{k + 1}{y} \to (\underset{˙}{[} y z / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} y (\frac{k + 1}{y}) / x \underset{˙}{]} φ)$
100	97 99	bitr3id	$⊢ z = \frac{k + 1}{y} \to (τ \leftrightarrow \underset{˙}{[} y (\frac{k + 1}{y}) / x \underset{˙}{]} φ)$
101	95 100	imbi12d	$⊢ z = \frac{k + 1}{y} \to (((χ \land θ) \to τ) \leftrightarrow ((χ \land \underset{˙}{[} (\frac{k + 1}{y}) / x \underset{˙}{]} φ) \to \underset{˙}{[} y (\frac{k + 1}{y}) / x \underset{˙}{]} φ))$
102	101	imbi2d	$⊢ z = \frac{k + 1}{y} \to ((y \in ℤ_{\geq 2} \to ((χ \land θ) \to τ)) \leftrightarrow (y \in ℤ_{\geq 2} \to ((χ \land \underset{˙}{[} (\frac{k + 1}{y}) / x \underset{˙}{]} φ) \to \underset{˙}{[} y (\frac{k + 1}{y}) / x \underset{˙}{]} φ)))$
103	8	expcom	$⊢ z \in ℤ_{\geq 2} \to (y \in ℤ_{\geq 2} \to ((χ \land θ) \to τ))$
104	102 103	vtoclga	$⊢ \frac{k + 1}{y} \in ℤ_{\geq 2} \to (y \in ℤ_{\geq 2} \to ((χ \land \underset{˙}{[} (\frac{k + 1}{y}) / x \underset{˙}{]} φ) \to \underset{˙}{[} y (\frac{k + 1}{y}) / x \underset{˙}{]} φ))$
105	60 25 94 104	syl3c	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to \underset{˙}{[} y (\frac{k + 1}{y}) / x \underset{˙}{]} φ$
106	30 105	sbceq1dd	$⊢ ((k \in ℕ \land \forall x \in (1 \dots k) φ) \land (y \in (2 \dots k + 1 - 1) \land y ∥ (k + 1))) \to \underset{˙}{[} (k + 1) / x \underset{˙}{]} φ$
107	106	rexlimdvaa	$⊢ (k \in ℕ \land \forall x \in (1 \dots k) φ) \to (\exists y \in (2 \dots k + 1 - 1) y ∥ (k + 1) \to \underset{˙}{[} (k + 1) / x \underset{˙}{]} φ)$
108		ralnex	$⊢ \forall y \in (2 \dots k + 1 - 1) \neg y ∥ (k + 1) \leftrightarrow \neg \exists y \in (2 \dots k + 1 - 1) y ∥ (k + 1)$
109		simpl	$⊢ (k \in ℕ \land \forall x \in (1 \dots k) φ) \to k \in ℕ$
110		elnnuz	$⊢ k \in ℕ \leftrightarrow k \in ℤ_{\geq 1}$
111	109 110	sylib	$⊢ (k \in ℕ \land \forall x \in (1 \dots k) φ) \to k \in ℤ_{\geq 1}$
112		eluzp1p1	$⊢ k \in ℤ_{\geq 1} \to k + 1 \in ℤ_{\geq (1 + 1)}$
113	111 112	syl	$⊢ (k \in ℕ \land \forall x \in (1 \dots k) φ) \to k + 1 \in ℤ_{\geq (1 + 1)}$
114		df-2	$⊢ 2 = 1 + 1$
115	114	fveq2i	$⊢ ℤ_{\geq 2} = ℤ_{\geq (1 + 1)}$
116	113 115	eleqtrrdi	$⊢ (k \in ℕ \land \forall x \in (1 \dots k) φ) \to k + 1 \in ℤ_{\geq 2}$
117		isprm3	$⊢ k + 1 \in ℙ \leftrightarrow (k + 1 \in ℤ_{\geq 2} \land \forall y \in (2 \dots k + 1 - 1) \neg y ∥ (k + 1))$
118	117	baibr	$⊢ k + 1 \in ℤ_{\geq 2} \to (\forall y \in (2 \dots k + 1 - 1) \neg y ∥ (k + 1) \leftrightarrow k + 1 \in ℙ)$
119	116 118	syl	$⊢ (k \in ℕ \land \forall x \in (1 \dots k) φ) \to (\forall y \in (2 \dots k + 1 - 1) \neg y ∥ (k + 1) \leftrightarrow k + 1 \in ℙ)$
120	2	cbvralvw	$⊢ \forall x \in (1 \dots k) φ \leftrightarrow \forall y \in (1 \dots k) χ$
121	120	bilani	$⊢ (k \in ℕ \land \forall x \in (1 \dots k) φ) \to \forall y \in (1 \dots k) χ$
122	109	nncnd	$⊢ (k \in ℕ \land \forall x \in (1 \dots k) φ) \to k \in ℂ$
123	122 42 43	sylancl	$⊢ (k \in ℕ \land \forall x \in (1 \dots k) φ) \to k + 1 - 1 = k$
124	123	oveq2d	$⊢ (k \in ℕ \land \forall x \in (1 \dots k) φ) \to (1 \dots k + 1 - 1) = (1 \dots k)$
125	121 124	raleqtrrdv	$⊢ (k \in ℕ \land \forall x \in (1 \dots k) φ) \to \forall y \in (1 \dots k + 1 - 1) χ$
126		nfcv	$⊢ \underline{Ⅎ} x (k + 1)$
127		nfv	$⊢ Ⅎ x \forall y \in (1 \dots k + 1 - 1) χ$
128		nfsbc1v	$⊢ Ⅎ x \underset{˙}{[} (k + 1) / x \underset{˙}{]} φ$
129	127 128	nfim	$⊢ Ⅎ x (\forall y \in (1 \dots k + 1 - 1) χ \to \underset{˙}{[} (k + 1) / x \underset{˙}{]} φ)$
130		oveq1	$⊢ x = k + 1 \to x - 1 = k + 1 - 1$
131	130	oveq2d	$⊢ x = k + 1 \to (1 \dots x - 1) = (1 \dots k + 1 - 1)$
132	131	raleqdv	$⊢ x = k + 1 \to (\forall y \in (1 \dots x - 1) χ \leftrightarrow \forall y \in (1 \dots k + 1 - 1) χ)$
133		sbceq1a	$⊢ x = k + 1 \to (φ \leftrightarrow \underset{˙}{[} (k + 1) / x \underset{˙}{]} φ)$
134	132 133	imbi12d	$⊢ x = k + 1 \to ((\forall y \in (1 \dots x - 1) χ \to φ) \leftrightarrow (\forall y \in (1 \dots k + 1 - 1) χ \to \underset{˙}{[} (k + 1) / x \underset{˙}{]} φ))$
135	7	ex	$⊢ x \in ℙ \to (\forall y \in (1 \dots x - 1) χ \to φ)$
136	126 129 134 135	vtoclgaf	$⊢ k + 1 \in ℙ \to (\forall y \in (1 \dots k + 1 - 1) χ \to \underset{˙}{[} (k + 1) / x \underset{˙}{]} φ)$
137	125 136	syl5com	$⊢ (k \in ℕ \land \forall x \in (1 \dots k) φ) \to (k + 1 \in ℙ \to \underset{˙}{[} (k + 1) / x \underset{˙}{]} φ)$
138	119 137	sylbid	$⊢ (k \in ℕ \land \forall x \in (1 \dots k) φ) \to (\forall y \in (2 \dots k + 1 - 1) \neg y ∥ (k + 1) \to \underset{˙}{[} (k + 1) / x \underset{˙}{]} φ)$
139	108 138	biimtrrid	$⊢ (k \in ℕ \land \forall x \in (1 \dots k) φ) \to (\neg \exists y \in (2 \dots k + 1 - 1) y ∥ (k + 1) \to \underset{˙}{[} (k + 1) / x \underset{˙}{]} φ)$
140	107 139	pm2.61d	$⊢ (k \in ℕ \land \forall x \in (1 \dots k) φ) \to \underset{˙}{[} (k + 1) / x \underset{˙}{]} φ$
141	140	ex	$⊢ k \in ℕ \to (\forall x \in (1 \dots k) φ \to \underset{˙}{[} (k + 1) / x \underset{˙}{]} φ)$
142		ralsnsg	$⊢ k + 1 \in ℕ \to (\forall x \in \{k + 1\} φ \leftrightarrow \underset{˙}{[} (k + 1) / x \underset{˙}{]} φ)$
143	21 142	syl	$⊢ k \in ℕ \to (\forall x \in \{k + 1\} φ \leftrightarrow \underset{˙}{[} (k + 1) / x \underset{˙}{]} φ)$
144	141 143	sylibrd	$⊢ k \in ℕ \to (\forall x \in (1 \dots k) φ \to \forall x \in \{k + 1\} φ)$
145	144	ancld	$⊢ k \in ℕ \to (\forall x \in (1 \dots k) φ \to (\forall x \in (1 \dots k) φ \land \forall x \in \{k + 1\} φ))$
146		fzsuc	$⊢ k \in ℤ_{\geq 1} \to (1 \dots k + 1) = (1 \dots k) \cup \{k + 1\}$
147	110 146	sylbi	$⊢ k \in ℕ \to (1 \dots k + 1) = (1 \dots k) \cup \{k + 1\}$
148	147	raleqdv	$⊢ k \in ℕ \to (\forall x \in (1 \dots k + 1) φ \leftrightarrow \forall x \in ((1 \dots k) \cup \{k + 1\}) φ)$
149		ralunb	$⊢ \forall x \in ((1 \dots k) \cup \{k + 1\}) φ \leftrightarrow (\forall x \in (1 \dots k) φ \land \forall x \in \{k + 1\} φ)$
150	148 149	bitrdi	$⊢ k \in ℕ \to (\forall x \in (1 \dots k + 1) φ \leftrightarrow (\forall x \in (1 \dots k) φ \land \forall x \in \{k + 1\} φ))$
151	145 150	sylibrd	$⊢ k \in ℕ \to (\forall x \in (1 \dots k) φ \to \forall x \in (1 \dots k + 1) φ)$
152	10 12 14 16 20 151	nnind	$⊢ A \in ℕ \to \forall x \in (1 \dots A) φ$
153		elfz1end	$⊢ A \in ℕ \leftrightarrow A \in (1 \dots A)$
154	153	biimpi	$⊢ A \in ℕ \to A \in (1 \dots A)$
155	5 152 154	rspcdva	$⊢ A \in ℕ \to η$

Metamath Proof Explorer

Theorem prmind2

Proof