ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  addcmpblnq GIF version

Theorem addcmpblnq 7168
Description: Lemma showing compatibility of addition. (Contributed by NM, 27-Aug-1995.)
Assertion
Ref Expression
addcmpblnq ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → (((𝐴 ·N 𝐷) = (𝐵 ·N 𝐶) ∧ (𝐹 ·N 𝑆) = (𝐺 ·N 𝑅)) → ⟨((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)), (𝐵 ·N 𝐺)⟩ ~Q ⟨((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅)), (𝐷 ·N 𝑆)⟩))

Proof of Theorem addcmpblnq
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 distrpig 7134 . . . . . . . 8 ((𝑥N𝑦N𝑧N) → (𝑥 ·N (𝑦 +N 𝑧)) = ((𝑥 ·N 𝑦) +N (𝑥 ·N 𝑧)))
21adantl 275 . . . . . . 7 (((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) ∧ (𝑥N𝑦N𝑧N)) → (𝑥 ·N (𝑦 +N 𝑧)) = ((𝑥 ·N 𝑦) +N (𝑥 ·N 𝑧)))
3 simplll 522 . . . . . . . 8 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → 𝐴N)
4 simprlr 527 . . . . . . . 8 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → 𝐺N)
5 mulclpi 7129 . . . . . . . 8 ((𝐴N𝐺N) → (𝐴 ·N 𝐺) ∈ N)
63, 4, 5syl2anc 408 . . . . . . 7 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → (𝐴 ·N 𝐺) ∈ N)
7 simpllr 523 . . . . . . . 8 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → 𝐵N)
8 simprll 526 . . . . . . . 8 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → 𝐹N)
9 mulclpi 7129 . . . . . . . 8 ((𝐵N𝐹N) → (𝐵 ·N 𝐹) ∈ N)
107, 8, 9syl2anc 408 . . . . . . 7 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → (𝐵 ·N 𝐹) ∈ N)
11 mulclpi 7129 . . . . . . . . 9 ((𝐷N𝑆N) → (𝐷 ·N 𝑆) ∈ N)
1211ad2ant2l 499 . . . . . . . 8 (((𝐶N𝐷N) ∧ (𝑅N𝑆N)) → (𝐷 ·N 𝑆) ∈ N)
1312ad2ant2l 499 . . . . . . 7 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → (𝐷 ·N 𝑆) ∈ N)
14 addclpi 7128 . . . . . . . 8 ((𝑥N𝑦N) → (𝑥 +N 𝑦) ∈ N)
1514adantl 275 . . . . . . 7 (((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) ∧ (𝑥N𝑦N)) → (𝑥 +N 𝑦) ∈ N)
16 mulcompig 7132 . . . . . . . 8 ((𝑥N𝑦N) → (𝑥 ·N 𝑦) = (𝑦 ·N 𝑥))
1716adantl 275 . . . . . . 7 (((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) ∧ (𝑥N𝑦N)) → (𝑥 ·N 𝑦) = (𝑦 ·N 𝑥))
182, 6, 10, 13, 15, 17caovdir2d 5940 . . . . . 6 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → (((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)) ·N (𝐷 ·N 𝑆)) = (((𝐴 ·N 𝐺) ·N (𝐷 ·N 𝑆)) +N ((𝐵 ·N 𝐹) ·N (𝐷 ·N 𝑆))))
19 simplrr 525 . . . . . . . 8 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → 𝐷N)
20 mulasspig 7133 . . . . . . . . 9 ((𝑥N𝑦N𝑧N) → ((𝑥 ·N 𝑦) ·N 𝑧) = (𝑥 ·N (𝑦 ·N 𝑧)))
2120adantl 275 . . . . . . . 8 (((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) ∧ (𝑥N𝑦N𝑧N)) → ((𝑥 ·N 𝑦) ·N 𝑧) = (𝑥 ·N (𝑦 ·N 𝑧)))
22 simprrr 529 . . . . . . . 8 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → 𝑆N)
23 mulclpi 7129 . . . . . . . . 9 ((𝑥N𝑦N) → (𝑥 ·N 𝑦) ∈ N)
2423adantl 275 . . . . . . . 8 (((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) ∧ (𝑥N𝑦N)) → (𝑥 ·N 𝑦) ∈ N)
253, 4, 19, 17, 21, 22, 24caov4d 5948 . . . . . . 7 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → ((𝐴 ·N 𝐺) ·N (𝐷 ·N 𝑆)) = ((𝐴 ·N 𝐷) ·N (𝐺 ·N 𝑆)))
267, 8, 19, 17, 21, 22, 24caov4d 5948 . . . . . . 7 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → ((𝐵 ·N 𝐹) ·N (𝐷 ·N 𝑆)) = ((𝐵 ·N 𝐷) ·N (𝐹 ·N 𝑆)))
2725, 26oveq12d 5785 . . . . . 6 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → (((𝐴 ·N 𝐺) ·N (𝐷 ·N 𝑆)) +N ((𝐵 ·N 𝐹) ·N (𝐷 ·N 𝑆))) = (((𝐴 ·N 𝐷) ·N (𝐺 ·N 𝑆)) +N ((𝐵 ·N 𝐷) ·N (𝐹 ·N 𝑆))))
2818, 27eqtrd 2170 . . . . 5 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → (((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)) ·N (𝐷 ·N 𝑆)) = (((𝐴 ·N 𝐷) ·N (𝐺 ·N 𝑆)) +N ((𝐵 ·N 𝐷) ·N (𝐹 ·N 𝑆))))
29 oveq1 5774 . . . . . 6 ((𝐴 ·N 𝐷) = (𝐵 ·N 𝐶) → ((𝐴 ·N 𝐷) ·N (𝐺 ·N 𝑆)) = ((𝐵 ·N 𝐶) ·N (𝐺 ·N 𝑆)))
30 oveq2 5775 . . . . . 6 ((𝐹 ·N 𝑆) = (𝐺 ·N 𝑅) → ((𝐵 ·N 𝐷) ·N (𝐹 ·N 𝑆)) = ((𝐵 ·N 𝐷) ·N (𝐺 ·N 𝑅)))
3129, 30oveqan12d 5786 . . . . 5 (((𝐴 ·N 𝐷) = (𝐵 ·N 𝐶) ∧ (𝐹 ·N 𝑆) = (𝐺 ·N 𝑅)) → (((𝐴 ·N 𝐷) ·N (𝐺 ·N 𝑆)) +N ((𝐵 ·N 𝐷) ·N (𝐹 ·N 𝑆))) = (((𝐵 ·N 𝐶) ·N (𝐺 ·N 𝑆)) +N ((𝐵 ·N 𝐷) ·N (𝐺 ·N 𝑅))))
3228, 31sylan9eq 2190 . . . 4 (((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) ∧ ((𝐴 ·N 𝐷) = (𝐵 ·N 𝐶) ∧ (𝐹 ·N 𝑆) = (𝐺 ·N 𝑅))) → (((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)) ·N (𝐷 ·N 𝑆)) = (((𝐵 ·N 𝐶) ·N (𝐺 ·N 𝑆)) +N ((𝐵 ·N 𝐷) ·N (𝐺 ·N 𝑅))))
33 mulclpi 7129 . . . . . . . 8 ((𝐵N𝐺N) → (𝐵 ·N 𝐺) ∈ N)
347, 4, 33syl2anc 408 . . . . . . 7 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → (𝐵 ·N 𝐺) ∈ N)
35 simplrl 524 . . . . . . . 8 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → 𝐶N)
36 mulclpi 7129 . . . . . . . 8 ((𝐶N𝑆N) → (𝐶 ·N 𝑆) ∈ N)
3735, 22, 36syl2anc 408 . . . . . . 7 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → (𝐶 ·N 𝑆) ∈ N)
38 simprrl 528 . . . . . . . 8 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → 𝑅N)
39 mulclpi 7129 . . . . . . . 8 ((𝐷N𝑅N) → (𝐷 ·N 𝑅) ∈ N)
4019, 38, 39syl2anc 408 . . . . . . 7 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → (𝐷 ·N 𝑅) ∈ N)
41 distrpig 7134 . . . . . . 7 (((𝐵 ·N 𝐺) ∈ N ∧ (𝐶 ·N 𝑆) ∈ N ∧ (𝐷 ·N 𝑅) ∈ N) → ((𝐵 ·N 𝐺) ·N ((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅))) = (((𝐵 ·N 𝐺) ·N (𝐶 ·N 𝑆)) +N ((𝐵 ·N 𝐺) ·N (𝐷 ·N 𝑅))))
4234, 37, 40, 41syl3anc 1216 . . . . . 6 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → ((𝐵 ·N 𝐺) ·N ((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅))) = (((𝐵 ·N 𝐺) ·N (𝐶 ·N 𝑆)) +N ((𝐵 ·N 𝐺) ·N (𝐷 ·N 𝑅))))
437, 4, 35, 17, 21, 22, 24caov4d 5948 . . . . . . 7 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → ((𝐵 ·N 𝐺) ·N (𝐶 ·N 𝑆)) = ((𝐵 ·N 𝐶) ·N (𝐺 ·N 𝑆)))
447, 4, 19, 17, 21, 38, 24caov4d 5948 . . . . . . 7 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → ((𝐵 ·N 𝐺) ·N (𝐷 ·N 𝑅)) = ((𝐵 ·N 𝐷) ·N (𝐺 ·N 𝑅)))
4543, 44oveq12d 5785 . . . . . 6 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → (((𝐵 ·N 𝐺) ·N (𝐶 ·N 𝑆)) +N ((𝐵 ·N 𝐺) ·N (𝐷 ·N 𝑅))) = (((𝐵 ·N 𝐶) ·N (𝐺 ·N 𝑆)) +N ((𝐵 ·N 𝐷) ·N (𝐺 ·N 𝑅))))
4642, 45eqtrd 2170 . . . . 5 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → ((𝐵 ·N 𝐺) ·N ((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅))) = (((𝐵 ·N 𝐶) ·N (𝐺 ·N 𝑆)) +N ((𝐵 ·N 𝐷) ·N (𝐺 ·N 𝑅))))
4746adantr 274 . . . 4 (((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) ∧ ((𝐴 ·N 𝐷) = (𝐵 ·N 𝐶) ∧ (𝐹 ·N 𝑆) = (𝐺 ·N 𝑅))) → ((𝐵 ·N 𝐺) ·N ((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅))) = (((𝐵 ·N 𝐶) ·N (𝐺 ·N 𝑆)) +N ((𝐵 ·N 𝐷) ·N (𝐺 ·N 𝑅))))
4832, 47eqtr4d 2173 . . 3 (((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) ∧ ((𝐴 ·N 𝐷) = (𝐵 ·N 𝐶) ∧ (𝐹 ·N 𝑆) = (𝐺 ·N 𝑅))) → (((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)) ·N (𝐷 ·N 𝑆)) = ((𝐵 ·N 𝐺) ·N ((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅))))
49 addclpi 7128 . . . . . . . . . 10 (((𝐴 ·N 𝐺) ∈ N ∧ (𝐵 ·N 𝐹) ∈ N) → ((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)) ∈ N)
505, 9, 49syl2an 287 . . . . . . . . 9 (((𝐴N𝐺N) ∧ (𝐵N𝐹N)) → ((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)) ∈ N)
5150an42s 578 . . . . . . . 8 (((𝐴N𝐵N) ∧ (𝐹N𝐺N)) → ((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)) ∈ N)
5233ad2ant2l 499 . . . . . . . 8 (((𝐴N𝐵N) ∧ (𝐹N𝐺N)) → (𝐵 ·N 𝐺) ∈ N)
5351, 52jca 304 . . . . . . 7 (((𝐴N𝐵N) ∧ (𝐹N𝐺N)) → (((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)) ∈ N ∧ (𝐵 ·N 𝐺) ∈ N))
54 addclpi 7128 . . . . . . . . . 10 (((𝐶 ·N 𝑆) ∈ N ∧ (𝐷 ·N 𝑅) ∈ N) → ((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅)) ∈ N)
5536, 39, 54syl2an 287 . . . . . . . . 9 (((𝐶N𝑆N) ∧ (𝐷N𝑅N)) → ((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅)) ∈ N)
5655an42s 578 . . . . . . . 8 (((𝐶N𝐷N) ∧ (𝑅N𝑆N)) → ((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅)) ∈ N)
5756, 12jca 304 . . . . . . 7 (((𝐶N𝐷N) ∧ (𝑅N𝑆N)) → (((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅)) ∈ N ∧ (𝐷 ·N 𝑆) ∈ N))
5853, 57anim12i 336 . . . . . 6 ((((𝐴N𝐵N) ∧ (𝐹N𝐺N)) ∧ ((𝐶N𝐷N) ∧ (𝑅N𝑆N))) → ((((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)) ∈ N ∧ (𝐵 ·N 𝐺) ∈ N) ∧ (((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅)) ∈ N ∧ (𝐷 ·N 𝑆) ∈ N)))
5958an4s 577 . . . . 5 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → ((((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)) ∈ N ∧ (𝐵 ·N 𝐺) ∈ N) ∧ (((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅)) ∈ N ∧ (𝐷 ·N 𝑆) ∈ N)))
60 enqbreq 7157 . . . . 5 (((((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)) ∈ N ∧ (𝐵 ·N 𝐺) ∈ N) ∧ (((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅)) ∈ N ∧ (𝐷 ·N 𝑆) ∈ N)) → (⟨((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)), (𝐵 ·N 𝐺)⟩ ~Q ⟨((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅)), (𝐷 ·N 𝑆)⟩ ↔ (((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)) ·N (𝐷 ·N 𝑆)) = ((𝐵 ·N 𝐺) ·N ((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅)))))
6159, 60syl 14 . . . 4 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → (⟨((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)), (𝐵 ·N 𝐺)⟩ ~Q ⟨((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅)), (𝐷 ·N 𝑆)⟩ ↔ (((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)) ·N (𝐷 ·N 𝑆)) = ((𝐵 ·N 𝐺) ·N ((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅)))))
6261adantr 274 . . 3 (((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) ∧ ((𝐴 ·N 𝐷) = (𝐵 ·N 𝐶) ∧ (𝐹 ·N 𝑆) = (𝐺 ·N 𝑅))) → (⟨((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)), (𝐵 ·N 𝐺)⟩ ~Q ⟨((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅)), (𝐷 ·N 𝑆)⟩ ↔ (((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)) ·N (𝐷 ·N 𝑆)) = ((𝐵 ·N 𝐺) ·N ((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅)))))
6348, 62mpbird 166 . 2 (((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) ∧ ((𝐴 ·N 𝐷) = (𝐵 ·N 𝐶) ∧ (𝐹 ·N 𝑆) = (𝐺 ·N 𝑅))) → ⟨((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)), (𝐵 ·N 𝐺)⟩ ~Q ⟨((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅)), (𝐷 ·N 𝑆)⟩)
6463ex 114 1 ((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → (((𝐴 ·N 𝐷) = (𝐵 ·N 𝐶) ∧ (𝐹 ·N 𝑆) = (𝐺 ·N 𝑅)) → ⟨((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)), (𝐵 ·N 𝐺)⟩ ~Q ⟨((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅)), (𝐷 ·N 𝑆)⟩))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  w3a 962   = wceq 1331  wcel 1480  cop 3525   class class class wbr 3924  (class class class)co 5767  Ncnpi 7073   +N cpli 7074   ·N cmi 7075   ~Q ceq 7080
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-coll 4038  ax-sep 4041  ax-nul 4049  ax-pow 4093  ax-pr 4126  ax-un 4350  ax-setind 4447  ax-iinf 4497
This theorem depends on definitions:  df-bi 116  df-dc 820  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2000  df-mo 2001  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ne 2307  df-ral 2419  df-rex 2420  df-reu 2421  df-rab 2423  df-v 2683  df-sbc 2905  df-csb 2999  df-dif 3068  df-un 3070  df-in 3072  df-ss 3079  df-nul 3359  df-pw 3507  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-int 3767  df-iun 3810  df-br 3925  df-opab 3985  df-mpt 3986  df-tr 4022  df-id 4210  df-iord 4283  df-on 4285  df-suc 4288  df-iom 4500  df-xp 4540  df-rel 4541  df-cnv 4542  df-co 4543  df-dm 4544  df-rn 4545  df-res 4546  df-ima 4547  df-iota 5083  df-fun 5120  df-fn 5121  df-f 5122  df-f1 5123  df-fo 5124  df-f1o 5125  df-fv 5126  df-ov 5770  df-oprab 5771  df-mpo 5772  df-1st 6031  df-2nd 6032  df-recs 6195  df-irdg 6260  df-oadd 6310  df-omul 6311  df-ni 7105  df-pli 7106  df-mi 7107  df-enq 7148
This theorem is referenced by:  addpipqqs  7171
  Copyright terms: Public domain W3C validator