paddasslem17 - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > paddasslem17		Structured version Visualization version GIF version

Theorem paddasslem17 36966

Description: Lemma for paddass 36968. The case when at least one sum argument is empty. (Contributed by NM, 12-Jan-2012.)

**Hypotheses**
Ref	Expression
paddass.a	⊢ 𝐴 = (Atoms‘𝐾)
paddass.p	⊢ + = (+_𝑃‘𝐾)

**Assertion**
Ref	Expression
paddasslem17	⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ¬ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍))

**Proof of Theorem paddasslem17**
Step	Hyp	Ref	Expression
1		ianor 978	. . . 4 ⊢ (¬ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅)) ↔ (¬ (𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∨ ¬ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅)))
2		ianor 978	. . . . . 6 ⊢ (¬ (𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ↔ (¬ 𝑋 ≠ ∅ ∨ ¬ (𝑌 + 𝑍) ≠ ∅))
3		nne 3020	. . . . . . 7 ⊢ (¬ 𝑋 ≠ ∅ ↔ 𝑋 = ∅)
4		nne 3020	. . . . . . 7 ⊢ (¬ (𝑌 + 𝑍) ≠ ∅ ↔ (𝑌 + 𝑍) = ∅)
5	3, 4	orbi12i 911	. . . . . 6 ⊢ ((¬ 𝑋 ≠ ∅ ∨ ¬ (𝑌 + 𝑍) ≠ ∅) ↔ (𝑋 = ∅ ∨ (𝑌 + 𝑍) = ∅))
6	2, 5	bitri 277	. . . . 5 ⊢ (¬ (𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ↔ (𝑋 = ∅ ∨ (𝑌 + 𝑍) = ∅))
7		ianor 978	. . . . . 6 ⊢ (¬ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅) ↔ (¬ 𝑌 ≠ ∅ ∨ ¬ 𝑍 ≠ ∅))
8		nne 3020	. . . . . . 7 ⊢ (¬ 𝑌 ≠ ∅ ↔ 𝑌 = ∅)
9		nne 3020	. . . . . . 7 ⊢ (¬ 𝑍 ≠ ∅ ↔ 𝑍 = ∅)
10	8, 9	orbi12i 911	. . . . . 6 ⊢ ((¬ 𝑌 ≠ ∅ ∨ ¬ 𝑍 ≠ ∅) ↔ (𝑌 = ∅ ∨ 𝑍 = ∅))
11	7, 10	bitri 277	. . . . 5 ⊢ (¬ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅) ↔ (𝑌 = ∅ ∨ 𝑍 = ∅))
12	6, 11	orbi12i 911	. . . 4 ⊢ ((¬ (𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∨ ¬ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅)) ↔ ((𝑋 = ∅ ∨ (𝑌 + 𝑍) = ∅) ∨ (𝑌 = ∅ ∨ 𝑍 = ∅)))
13	1, 12	bitri 277	. . 3 ⊢ (¬ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅)) ↔ ((𝑋 = ∅ ∨ (𝑌 + 𝑍) = ∅) ∨ (𝑌 = ∅ ∨ 𝑍 = ∅)))
14		paddass.a	. . . . . . . . . . 11 ⊢ 𝐴 = (Atoms‘𝐾)
15		paddass.p	. . . . . . . . . . 11 ⊢ + = (+_𝑃‘𝐾)
16	14, 15	paddssat 36944	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → (𝑌 + 𝑍) ⊆ 𝐴)
17	16	3adant3r1 1178	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑌 + 𝑍) ⊆ 𝐴)
18	14, 15	padd02 36942	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑌 + 𝑍) ⊆ 𝐴) → (∅ + (𝑌 + 𝑍)) = (𝑌 + 𝑍))
19	17, 18	syldan 593	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (∅ + (𝑌 + 𝑍)) = (𝑌 + 𝑍))
20	14, 15	padd02 36942	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴) → (∅ + 𝑌) = 𝑌)
21	20	3ad2antr2 1185	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (∅ + 𝑌) = 𝑌)
22	21	oveq1d 7165	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((∅ + 𝑌) + 𝑍) = (𝑌 + 𝑍))
23	19, 22	eqtr4d 2859	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (∅ + (𝑌 + 𝑍)) = ((∅ + 𝑌) + 𝑍))
24		oveq1 7157	. . . . . . . 8 ⊢ (𝑋 = ∅ → (𝑋 + (𝑌 + 𝑍)) = (∅ + (𝑌 + 𝑍)))
25		oveq1 7157	. . . . . . . . 9 ⊢ (𝑋 = ∅ → (𝑋 + 𝑌) = (∅ + 𝑌))
26	25	oveq1d 7165	. . . . . . . 8 ⊢ (𝑋 = ∅ → ((𝑋 + 𝑌) + 𝑍) = ((∅ + 𝑌) + 𝑍))
27	24, 26	eqeq12d 2837	. . . . . . 7 ⊢ (𝑋 = ∅ → ((𝑋 + (𝑌 + 𝑍)) = ((𝑋 + 𝑌) + 𝑍) ↔ (∅ + (𝑌 + 𝑍)) = ((∅ + 𝑌) + 𝑍)))
28	23, 27	syl5ibrcom 249	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 = ∅ → (𝑋 + (𝑌 + 𝑍)) = ((𝑋 + 𝑌) + 𝑍)))
29		eqimss 4023	. . . . . 6 ⊢ ((𝑋 + (𝑌 + 𝑍)) = ((𝑋 + 𝑌) + 𝑍) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍))
30	28, 29	syl6 35	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 = ∅ → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍)))
31	14, 15	padd01 36941	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑋 + ∅) = 𝑋)
32	31	3ad2antr1 1184	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + ∅) = 𝑋)
33	14, 15	sspadd1 36945	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → 𝑋 ⊆ (𝑋 + 𝑌))
34	33	3adant3r3 1180	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝑋 ⊆ (𝑋 + 𝑌))
35		simpl 485	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝐾 ∈ HL)
36	14, 15	paddssat 36944	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) ⊆ 𝐴)
37	36	3adant3r3 1180	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + 𝑌) ⊆ 𝐴)
38		simpr3 1192	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝑍 ⊆ 𝐴)
39	14, 15	sspadd1 36945	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 + 𝑌) ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → (𝑋 + 𝑌) ⊆ ((𝑋 + 𝑌) + 𝑍))
40	35, 37, 38, 39	syl3anc 1367	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + 𝑌) ⊆ ((𝑋 + 𝑌) + 𝑍))
41	34, 40	sstrd 3977	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝑋 ⊆ ((𝑋 + 𝑌) + 𝑍))
42	32, 41	eqsstrd 4005	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + ∅) ⊆ ((𝑋 + 𝑌) + 𝑍))
43		oveq2 7158	. . . . . . 7 ⊢ ((𝑌 + 𝑍) = ∅ → (𝑋 + (𝑌 + 𝑍)) = (𝑋 + ∅))
44	43	sseq1d 3998	. . . . . 6 ⊢ ((𝑌 + 𝑍) = ∅ → ((𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍) ↔ (𝑋 + ∅) ⊆ ((𝑋 + 𝑌) + 𝑍)))
45	42, 44	syl5ibrcom 249	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑌 + 𝑍) = ∅ → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍)))
46	30, 45	jaod 855	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 = ∅ ∨ (𝑌 + 𝑍) = ∅) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍)))
47	14, 15	padd02 36942	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑍 ⊆ 𝐴) → (∅ + 𝑍) = 𝑍)
48	47	3ad2antr3 1186	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (∅ + 𝑍) = 𝑍)
49	48	oveq2d 7166	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + (∅ + 𝑍)) = (𝑋 + 𝑍))
50	32	oveq1d 7165	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 + ∅) + 𝑍) = (𝑋 + 𝑍))
51	49, 50	eqtr4d 2859	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + (∅ + 𝑍)) = ((𝑋 + ∅) + 𝑍))
52		oveq1 7157	. . . . . . . . 9 ⊢ (𝑌 = ∅ → (𝑌 + 𝑍) = (∅ + 𝑍))
53	52	oveq2d 7166	. . . . . . . 8 ⊢ (𝑌 = ∅ → (𝑋 + (𝑌 + 𝑍)) = (𝑋 + (∅ + 𝑍)))
54		oveq2 7158	. . . . . . . . 9 ⊢ (𝑌 = ∅ → (𝑋 + 𝑌) = (𝑋 + ∅))
55	54	oveq1d 7165	. . . . . . . 8 ⊢ (𝑌 = ∅ → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + ∅) + 𝑍))
56	53, 55	eqeq12d 2837	. . . . . . 7 ⊢ (𝑌 = ∅ → ((𝑋 + (𝑌 + 𝑍)) = ((𝑋 + 𝑌) + 𝑍) ↔ (𝑋 + (∅ + 𝑍)) = ((𝑋 + ∅) + 𝑍)))
57	51, 56	syl5ibrcom 249	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑌 = ∅ → (𝑋 + (𝑌 + 𝑍)) = ((𝑋 + 𝑌) + 𝑍)))
58	14, 15	padd01 36941	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴) → (𝑌 + ∅) = 𝑌)
59	58	3ad2antr2 1185	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑌 + ∅) = 𝑌)
60	59	oveq2d 7166	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + (𝑌 + ∅)) = (𝑋 + 𝑌))
61	14, 15	padd01 36941	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 + 𝑌) ⊆ 𝐴) → ((𝑋 + 𝑌) + ∅) = (𝑋 + 𝑌))
62	37, 61	syldan 593	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 + 𝑌) + ∅) = (𝑋 + 𝑌))
63	60, 62	eqtr4d 2859	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + (𝑌 + ∅)) = ((𝑋 + 𝑌) + ∅))
64		oveq2 7158	. . . . . . . . 9 ⊢ (𝑍 = ∅ → (𝑌 + 𝑍) = (𝑌 + ∅))
65	64	oveq2d 7166	. . . . . . . 8 ⊢ (𝑍 = ∅ → (𝑋 + (𝑌 + 𝑍)) = (𝑋 + (𝑌 + ∅)))
66		oveq2 7158	. . . . . . . 8 ⊢ (𝑍 = ∅ → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) + ∅))
67	65, 66	eqeq12d 2837	. . . . . . 7 ⊢ (𝑍 = ∅ → ((𝑋 + (𝑌 + 𝑍)) = ((𝑋 + 𝑌) + 𝑍) ↔ (𝑋 + (𝑌 + ∅)) = ((𝑋 + 𝑌) + ∅)))
68	63, 67	syl5ibrcom 249	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑍 = ∅ → (𝑋 + (𝑌 + 𝑍)) = ((𝑋 + 𝑌) + 𝑍)))
69	57, 68	jaod 855	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑌 = ∅ ∨ 𝑍 = ∅) → (𝑋 + (𝑌 + 𝑍)) = ((𝑋 + 𝑌) + 𝑍)))
70	69, 29	syl6 35	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑌 = ∅ ∨ 𝑍 = ∅) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍)))
71	46, 70	jaod 855	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (((𝑋 = ∅ ∨ (𝑌 + 𝑍) = ∅) ∨ (𝑌 = ∅ ∨ 𝑍 = ∅)) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍)))
72	13, 71	syl5bi 244	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (¬ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅)) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍)))
73	72	3impia 1113	1 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ¬ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 398 ∨ wo 843 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ≠ wne 3016 ⊆ wss 3936 ∅c0 4291 ‘cfv 6350 (class class class)co 7150 Atomscatm 36393 HLchlt 36480 +_𝑃cpadd 36925

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-rep 5183 ax-sep 5196 ax-nul 5203 ax-pow 5259 ax-pr 5322 ax-un 7455

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3497 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4833 df-iun 4914 df-br 5060 df-opab 5122 df-mpt 5140 df-id 5455 df-xp 5556 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-rn 5561 df-res 5562 df-ima 5563 df-iota 6309 df-fun 6352 df-fn 6353 df-f 6354 df-f1 6355 df-fo 6356 df-f1o 6357 df-fv 6358 df-ov 7153 df-oprab 7154 df-mpo 7155 df-1st 7683 df-2nd 7684 df-padd 36926

This theorem is referenced by: paddasslem18 36967

W3C validator