Theorem Sumssd ≪ | index | src | ≫ 

theorem Sumssd (A1 A2 B1 B2: set) (G: wff):
  $ G -> A1 C_ A2 $ >
  $ G -> B1 C_ B2 $ >
  $ G -> Sum A1 B1 C_ Sum A2 B2 $;
StepHypRefExpression
1 ifppos 
odd a1 -> (ifp (odd a1) (a1 // 2 e. B1) (a1 // 2 e. A1) <-> a1 // 2 e. B1)
2 ifppos 
odd a1 -> (ifp (odd a1) (a1 // 2 e. B2) (a1 // 2 e. A2) <-> a1 // 2 e. B2)
3 1, 2 imeqd 
odd a1 -> (ifp (odd a1) (a1 // 2 e. B1) (a1 // 2 e. A1) -> ifp (odd a1) (a1 // 2 e. B2) (a1 // 2 e. A2) <-> a1 // 2 e. B1 -> a1 // 2 e. B2)
4 3 anwr 
G /\ odd a1 -> (ifp (odd a1) (a1 // 2 e. B1) (a1 // 2 e. A1) -> ifp (odd a1) (a1 // 2 e. B2) (a1 // 2 e. A2) <-> a1 // 2 e. B1 -> a1 // 2 e. B2)
5 ssel 
B1 C_ B2 -> a1 // 2 e. B1 -> a1 // 2 e. B2
6 hyp h2 
G -> B1 C_ B2
7 5, 6 syl 
G -> a1 // 2 e. B1 -> a1 // 2 e. B2
8 7 anwl 
G /\ odd a1 -> a1 // 2 e. B1 -> a1 // 2 e. B2
9 4, 8 mpbird 
G /\ odd a1 -> ifp (odd a1) (a1 // 2 e. B1) (a1 // 2 e. A1) -> ifp (odd a1) (a1 // 2 e. B2) (a1 // 2 e. A2)
10 ifpneg 
~odd a1 -> (ifp (odd a1) (a1 // 2 e. B1) (a1 // 2 e. A1) <-> a1 // 2 e. A1)
11 ifpneg 
~odd a1 -> (ifp (odd a1) (a1 // 2 e. B2) (a1 // 2 e. A2) <-> a1 // 2 e. A2)
12 10, 11 imeqd 
~odd a1 -> (ifp (odd a1) (a1 // 2 e. B1) (a1 // 2 e. A1) -> ifp (odd a1) (a1 // 2 e. B2) (a1 // 2 e. A2) <-> a1 // 2 e. A1 -> a1 // 2 e. A2)
13 12 anwr 
G /\ ~odd a1 -> (ifp (odd a1) (a1 // 2 e. B1) (a1 // 2 e. A1) -> ifp (odd a1) (a1 // 2 e. B2) (a1 // 2 e. A2) <-> a1 // 2 e. A1 -> a1 // 2 e. A2)
14 ssel 
A1 C_ A2 -> a1 // 2 e. A1 -> a1 // 2 e. A2
15 hyp h1 
G -> A1 C_ A2
16 14, 15 syl 
G -> a1 // 2 e. A1 -> a1 // 2 e. A2
17 16 anwl 
G /\ ~odd a1 -> a1 // 2 e. A1 -> a1 // 2 e. A2
18 13, 17 mpbird 
G /\ ~odd a1 -> ifp (odd a1) (a1 // 2 e. B1) (a1 // 2 e. A1) -> ifp (odd a1) (a1 // 2 e. B2) (a1 // 2 e. A2)
19 9, 18 casesda 
G -> ifp (odd a1) (a1 // 2 e. B1) (a1 // 2 e. A1) -> ifp (odd a1) (a1 // 2 e. B2) (a1 // 2 e. A2)
20 19 ssabd 
G -> {a1 | ifp (odd a1) (a1 // 2 e. B1) (a1 // 2 e. A1)} C_ {a1 | ifp (odd a1) (a1 // 2 e. B2) (a1 // 2 e. A2)}
21 20 conv Sum 
G -> Sum A1 B1 C_ Sum A2 B2

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8)