vdwapun

Description: Remove the first element of an arithmetic progression. (Contributed by Mario Carneiro, 11-Sep-2014)

		Ref	Expression
	Assertion	vdwapun	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to A AP (K + 1) D = \{A\} \cup ((A + D) AP (K) D)$

Proof

Step	Hyp	Ref	Expression
1		peano2nn0	$⊢ K \in ℕ_{0} \to K + 1 \in ℕ_{0}$
2		vdwapval	$⊢ (K + 1 \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (x \in (A AP (K + 1) D) \leftrightarrow \exists n \in (0 \dots K + 1 - 1) x = A + n D)$
3	1 2	syl3an1	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (x \in (A AP (K + 1) D) \leftrightarrow \exists n \in (0 \dots K + 1 - 1) x = A + n D)$
4		simp1	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to K \in ℕ_{0}$
5	4	nn0cnd	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to K \in ℂ$
6		ax-1cn	$⊢ 1 \in ℂ$
7		pncan	$⊢ (K \in ℂ \land 1 \in ℂ) \to K + 1 - 1 = K$
8	5 6 7	sylancl	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to K + 1 - 1 = K$
9	8	oveq2d	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (0 \dots K + 1 - 1) = (0 \dots K)$
10	9	eleq2d	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (n \in (0 \dots K + 1 - 1) \leftrightarrow n \in (0 \dots K))$
11		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
12	4 11	eleqtrdi	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to K \in ℤ_{\geq 0}$
13		elfzp12	$⊢ K \in ℤ_{\geq 0} \to (n \in (0 \dots K) \leftrightarrow (n = 0 \lor n \in (0 + 1 \dots K)))$
14	12 13	syl	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (n \in (0 \dots K) \leftrightarrow (n = 0 \lor n \in (0 + 1 \dots K)))$
15	10 14	bitrd	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (n \in (0 \dots K + 1 - 1) \leftrightarrow (n = 0 \lor n \in (0 + 1 \dots K)))$
16	15	anbi1d	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to ((n \in (0 \dots K + 1 - 1) \land x = A + n D) \leftrightarrow ((n = 0 \lor n \in (0 + 1 \dots K)) \land x = A + n D))$
17		andir	$⊢ ((n = 0 \lor n \in (0 + 1 \dots K)) \land x = A + n D) \leftrightarrow ((n = 0 \land x = A + n D) \lor (n \in (0 + 1 \dots K) \land x = A + n D))$
18	16 17	bitrdi	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to ((n \in (0 \dots K + 1 - 1) \land x = A + n D) \leftrightarrow ((n = 0 \land x = A + n D) \lor (n \in (0 + 1 \dots K) \land x = A + n D)))$
19	18	exbidv	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (\exists n (n \in (0 \dots K + 1 - 1) \land x = A + n D) \leftrightarrow \exists n ((n = 0 \land x = A + n D) \lor (n \in (0 + 1 \dots K) \land x = A + n D)))$
20		df-rex	$⊢ \exists n \in (0 \dots K + 1 - 1) x = A + n D \leftrightarrow \exists n (n \in (0 \dots K + 1 - 1) \land x = A + n D)$
21		19.43	$⊢ \exists n ((n = 0 \land x = A + n D) \lor (n \in (0 + 1 \dots K) \land x = A + n D)) \leftrightarrow (\exists n (n = 0 \land x = A + n D) \lor \exists n (n \in (0 + 1 \dots K) \land x = A + n D))$
22	21	bicomi	$⊢ (\exists n (n = 0 \land x = A + n D) \lor \exists n (n \in (0 + 1 \dots K) \land x = A + n D)) \leftrightarrow \exists n ((n = 0 \land x = A + n D) \lor (n \in (0 + 1 \dots K) \land x = A + n D))$
23	19 20 22	3bitr4g	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (\exists n \in (0 \dots K + 1 - 1) x = A + n D \leftrightarrow (\exists n (n = 0 \land x = A + n D) \lor \exists n (n \in (0 + 1 \dots K) \land x = A + n D)))$
24	3 23	bitrd	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (x \in (A AP (K + 1) D) \leftrightarrow (\exists n (n = 0 \land x = A + n D) \lor \exists n (n \in (0 + 1 \dots K) \land x = A + n D)))$
25		nncn	$⊢ D \in ℕ \to D \in ℂ$
26	25	3ad2ant3	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to D \in ℂ$
27	26	mul02d	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to 0 \cdot D = 0$
28	27	oveq2d	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to A + 0 \cdot D = A + 0$
29		nncn	$⊢ A \in ℕ \to A \in ℂ$
30	29	3ad2ant2	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to A \in ℂ$
31	30	addridd	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to A + 0 = A$
32	28 31	eqtrd	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to A + 0 \cdot D = A$
33	32	eqeq2d	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (x = A + 0 \cdot D \leftrightarrow x = A)$
34		c0ex	$⊢ 0 \in V$
35		oveq1	$⊢ n = 0 \to n D = 0 \cdot D$
36	35	oveq2d	$⊢ n = 0 \to A + n D = A + 0 \cdot D$
37	36	eqeq2d	$⊢ n = 0 \to (x = A + n D \leftrightarrow x = A + 0 \cdot D)$
38	34 37	ceqsexv	$⊢ \exists n (n = 0 \land x = A + n D) \leftrightarrow x = A + 0 \cdot D$
39		velsn	$⊢ x \in \{A\} \leftrightarrow x = A$
40	33 38 39	3bitr4g	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (\exists n (n = 0 \land x = A + n D) \leftrightarrow x \in \{A\})$
41		simpr	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to n \in (0 + 1 \dots K)$
42		0p1e1	$⊢ 0 + 1 = 1$
43	42	oveq1i	$⊢ (0 + 1 \dots K) = (1 \dots K)$
44	41 43	eleqtrdi	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to n \in (1 \dots K)$
45		1zzd	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to 1 \in ℤ$
46	4	adantr	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to K \in ℕ_{0}$
47	46	nn0zd	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to K \in ℤ$
48		elfzelz	$⊢ n \in (0 + 1 \dots K) \to n \in ℤ$
49	48	adantl	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to n \in ℤ$
50		fzsubel	$⊢ ((1 \in ℤ \land K \in ℤ) \land (n \in ℤ \land 1 \in ℤ)) \to (n \in (1 \dots K) \leftrightarrow n - 1 \in (1 - 1 \dots K - 1))$
51	45 47 49 45 50	syl22anc	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to (n \in (1 \dots K) \leftrightarrow n - 1 \in (1 - 1 \dots K - 1))$
52	44 51	mpbid	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to n - 1 \in (1 - 1 \dots K - 1)$
53		1m1e0	$⊢ 1 - 1 = 0$
54	53	oveq1i	$⊢ (1 - 1 \dots K - 1) = (0 \dots K - 1)$
55	52 54	eleqtrdi	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to n - 1 \in (0 \dots K - 1)$
56	49	zcnd	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to n \in ℂ$
57		1cnd	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to 1 \in ℂ$
58	26	adantr	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to D \in ℂ$
59	56 57 58	subdird	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to (n - 1) D = n D - 1 D$
60	58	mullidd	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to 1 D = D$
61	60	oveq2d	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to n D - 1 D = n D - D$
62	59 61	eqtrd	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to (n - 1) D = n D - D$
63	62	oveq2d	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to D + (n - 1) D = D + n D - D$
64	56 58	mulcld	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to n D \in ℂ$
65	58 64	pncan3d	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to D + n D - D = n D$
66	63 65	eqtr2d	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to n D = D + (n - 1) D$
67	66	oveq2d	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to A + n D = A + D + (n - 1) D$
68	30	adantr	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to A \in ℂ$
69		subcl	$⊢ (n \in ℂ \land 1 \in ℂ) \to n - 1 \in ℂ$
70	56 6 69	sylancl	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to n - 1 \in ℂ$
71	70 58	mulcld	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to (n - 1) D \in ℂ$
72	68 58 71	addassd	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to A + D + (n - 1) D = A + D + (n - 1) D$
73	67 72	eqtr4d	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to A + n D = A + D + (n - 1) D$
74		oveq1	$⊢ m = n - 1 \to m D = (n - 1) D$
75	74	oveq2d	$⊢ m = n - 1 \to A + D + m D = A + D + (n - 1) D$
76	75	rspceeqv	$⊢ (n - 1 \in (0 \dots K - 1) \land A + n D = A + D + (n - 1) D) \to \exists m \in (0 \dots K - 1) A + n D = A + D + m D$
77	55 73 76	syl2anc	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to \exists m \in (0 \dots K - 1) A + n D = A + D + m D$
78		eqeq1	$⊢ x = A + n D \to (x = A + D + m D \leftrightarrow A + n D = A + D + m D)$
79	78	rexbidv	$⊢ x = A + n D \to (\exists m \in (0 \dots K - 1) x = A + D + m D \leftrightarrow \exists m \in (0 \dots K - 1) A + n D = A + D + m D)$
80	77 79	syl5ibrcom	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land n \in (0 + 1 \dots K)) \to (x = A + n D \to \exists m \in (0 \dots K - 1) x = A + D + m D)$
81	80	expimpd	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to ((n \in (0 + 1 \dots K) \land x = A + n D) \to \exists m \in (0 \dots K - 1) x = A + D + m D)$
82	81	exlimdv	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (\exists n (n \in (0 + 1 \dots K) \land x = A + n D) \to \exists m \in (0 \dots K - 1) x = A + D + m D)$
83		simpr	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to m \in (0 \dots K - 1)$
84		0zd	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to 0 \in ℤ$
85	4	adantr	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to K \in ℕ_{0}$
86	85	nn0zd	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to K \in ℤ$
87		peano2zm	$⊢ K \in ℤ \to K - 1 \in ℤ$
88	86 87	syl	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to K - 1 \in ℤ$
89		elfzelz	$⊢ m \in (0 \dots K - 1) \to m \in ℤ$
90	89	adantl	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to m \in ℤ$
91		1zzd	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to 1 \in ℤ$
92		fzaddel	$⊢ ((0 \in ℤ \land K - 1 \in ℤ) \land (m \in ℤ \land 1 \in ℤ)) \to (m \in (0 \dots K - 1) \leftrightarrow m + 1 \in (0 + 1 \dots K - 1 + 1))$
93	84 88 90 91 92	syl22anc	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to (m \in (0 \dots K - 1) \leftrightarrow m + 1 \in (0 + 1 \dots K - 1 + 1))$
94	83 93	mpbid	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to m + 1 \in (0 + 1 \dots K - 1 + 1)$
95	85	nn0cnd	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to K \in ℂ$
96		npcan	$⊢ (K \in ℂ \land 1 \in ℂ) \to K - 1 + 1 = K$
97	95 6 96	sylancl	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to K - 1 + 1 = K$
98	97	oveq2d	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to (0 + 1 \dots K - 1 + 1) = (0 + 1 \dots K)$
99	94 98	eleqtrd	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to m + 1 \in (0 + 1 \dots K)$
100	30	adantr	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to A \in ℂ$
101	26	adantr	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to D \in ℂ$
102	90	zcnd	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to m \in ℂ$
103	102 101	mulcld	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to m D \in ℂ$
104	100 101 103	addassd	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to A + D + m D = A + D + m D$
105		1cnd	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to 1 \in ℂ$
106	102 105 101	adddird	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to (m + 1) D = m D + 1 D$
107	101 103	addcomd	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to D + m D = m D + D$
108	101	mullidd	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to 1 D = D$
109	108	oveq2d	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to m D + 1 D = m D + D$
110	107 109	eqtr4d	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to D + m D = m D + 1 D$
111	106 110	eqtr4d	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to (m + 1) D = D + m D$
112	111	oveq2d	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to A + (m + 1) D = A + D + m D$
113	104 112	eqtr4d	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to A + D + m D = A + (m + 1) D$
114		ovex	$⊢ m + 1 \in V$
115		eleq1	$⊢ n = m + 1 \to (n \in (0 + 1 \dots K) \leftrightarrow m + 1 \in (0 + 1 \dots K))$
116		oveq1	$⊢ n = m + 1 \to n D = (m + 1) D$
117	116	oveq2d	$⊢ n = m + 1 \to A + n D = A + (m + 1) D$
118	117	eqeq2d	$⊢ n = m + 1 \to (A + D + m D = A + n D \leftrightarrow A + D + m D = A + (m + 1) D)$
119	115 118	anbi12d	$⊢ n = m + 1 \to ((n \in (0 + 1 \dots K) \land A + D + m D = A + n D) \leftrightarrow (m + 1 \in (0 + 1 \dots K) \land A + D + m D = A + (m + 1) D))$
120	114 119	spcev	$⊢ (m + 1 \in (0 + 1 \dots K) \land A + D + m D = A + (m + 1) D) \to \exists n (n \in (0 + 1 \dots K) \land A + D + m D = A + n D)$
121	99 113 120	syl2anc	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to \exists n (n \in (0 + 1 \dots K) \land A + D + m D = A + n D)$
122		eqeq1	$⊢ x = A + D + m D \to (x = A + n D \leftrightarrow A + D + m D = A + n D)$
123	122	anbi2d	$⊢ x = A + D + m D \to ((n \in (0 + 1 \dots K) \land x = A + n D) \leftrightarrow (n \in (0 + 1 \dots K) \land A + D + m D = A + n D))$
124	123	exbidv	$⊢ x = A + D + m D \to (\exists n (n \in (0 + 1 \dots K) \land x = A + n D) \leftrightarrow \exists n (n \in (0 + 1 \dots K) \land A + D + m D = A + n D))$
125	121 124	syl5ibrcom	$⊢ ((K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \land m \in (0 \dots K - 1)) \to (x = A + D + m D \to \exists n (n \in (0 + 1 \dots K) \land x = A + n D))$
126	125	rexlimdva	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (\exists m \in (0 \dots K - 1) x = A + D + m D \to \exists n (n \in (0 + 1 \dots K) \land x = A + n D))$
127	82 126	impbid	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (\exists n (n \in (0 + 1 \dots K) \land x = A + n D) \leftrightarrow \exists m \in (0 \dots K - 1) x = A + D + m D)$
128		nnaddcl	$⊢ (A \in ℕ \land D \in ℕ) \to A + D \in ℕ$
129	128	3adant1	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to A + D \in ℕ$
130		vdwapval	$⊢ (K \in ℕ_{0} \land A + D \in ℕ \land D \in ℕ) \to (x \in ((A + D) AP (K) D) \leftrightarrow \exists m \in (0 \dots K - 1) x = A + D + m D)$
131	129 130	syld3an2	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (x \in ((A + D) AP (K) D) \leftrightarrow \exists m \in (0 \dots K - 1) x = A + D + m D)$
132	127 131	bitr4d	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (\exists n (n \in (0 + 1 \dots K) \land x = A + n D) \leftrightarrow x \in ((A + D) AP (K) D))$
133	40 132	orbi12d	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to ((\exists n (n = 0 \land x = A + n D) \lor \exists n (n \in (0 + 1 \dots K) \land x = A + n D)) \leftrightarrow (x \in \{A\} \lor x \in ((A + D) AP (K) D)))$
134		elun	$⊢ x \in (\{A\} \cup ((A + D) AP (K) D)) \leftrightarrow (x \in \{A\} \lor x \in ((A + D) AP (K) D))$
135	133 134	bitr4di	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to ((\exists n (n = 0 \land x = A + n D) \lor \exists n (n \in (0 + 1 \dots K) \land x = A + n D)) \leftrightarrow x \in (\{A\} \cup ((A + D) AP (K) D)))$
136	24 135	bitrd	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (x \in (A AP (K + 1) D) \leftrightarrow x \in (\{A\} \cup ((A + D) AP (K) D)))$
137	136	eqrdv	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to A AP (K + 1) D = \{A\} \cup ((A + D) AP (K) D)$

Metamath Proof Explorer

Theorem vdwapun

Proof