Step | Hyp | Ref
| Expression |
1 | | addsproplem1.2 |
. . 3
⊢ (𝜑 → 𝐴 ∈ No
) |
2 | | addsproplem1.3 |
. . 3
⊢ (𝜑 → 𝐵 ∈ No
) |
3 | | addsproplem1.4 |
. . 3
⊢ (𝜑 → 𝐶 ∈ No
) |
4 | 1, 2, 3 | 3jca 1129 |
. 2
⊢ (𝜑 → (𝐴 ∈ No
∧ 𝐵 ∈ No ∧ 𝐶 ∈ No
)) |
5 | | addsproplem.1 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
6 | | addsproplem1.5 |
. 2
⊢ (𝜑 → (((
bday ‘𝐴) +no
( bday ‘𝐵)) ∪ (( bday
‘𝐴) +no ( bday ‘𝐶))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
7 | | fveq2 6843 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ( bday
‘𝑥) = ( bday ‘𝐴)) |
8 | 7 | oveq1d 7373 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (( bday
‘𝑥) +no ( bday ‘𝑦)) = (( bday
‘𝐴) +no ( bday ‘𝑦))) |
9 | 7 | oveq1d 7373 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (( bday
‘𝑥) +no ( bday ‘𝑧)) = (( bday
‘𝐴) +no ( bday ‘𝑧))) |
10 | 8, 9 | uneq12d 4125 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((( bday
‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) = ((( bday
‘𝐴) +no ( bday ‘𝑦)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑧)))) |
11 | 10 | eleq1d 2823 |
. . . 4
⊢ (𝑥 = 𝐴 → (((( bday
‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍))) ↔ ((( bday
‘𝐴) +no ( bday ‘𝑦)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑧))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍))))) |
12 | | oveq1 7365 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 +s 𝑦) = (𝐴 +s 𝑦)) |
13 | 12 | eleq1d 2823 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝑥 +s 𝑦) ∈ No
↔ (𝐴 +s
𝑦) ∈ No )) |
14 | | oveq2 7366 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑦 +s 𝑥) = (𝑦 +s 𝐴)) |
15 | | oveq2 7366 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑧 +s 𝑥) = (𝑧 +s 𝐴)) |
16 | 14, 15 | breq12d 5119 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑦 +s 𝑥) <s (𝑧 +s 𝑥) ↔ (𝑦 +s 𝐴) <s (𝑧 +s 𝐴))) |
17 | 16 | imbi2d 341 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)) ↔ (𝑦 <s 𝑧 → (𝑦 +s 𝐴) <s (𝑧 +s 𝐴)))) |
18 | 13, 17 | anbi12d 632 |
. . . 4
⊢ (𝑥 = 𝐴 → (((𝑥 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))) ↔ ((𝐴 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝐴) <s (𝑧 +s 𝐴))))) |
19 | 11, 18 | imbi12d 345 |
. . 3
⊢ (𝑥 = 𝐴 → ((((( bday
‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍))) → ((𝑥 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) ↔ (((( bday
‘𝐴) +no ( bday ‘𝑦)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑧))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍))) → ((𝐴 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝐴) <s (𝑧 +s 𝐴)))))) |
20 | | fveq2 6843 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → ( bday
‘𝑦) = ( bday ‘𝐵)) |
21 | 20 | oveq2d 7374 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (( bday
‘𝐴) +no ( bday ‘𝑦)) = (( bday
‘𝐴) +no ( bday ‘𝐵))) |
22 | 21 | uneq1d 4123 |
. . . . 5
⊢ (𝑦 = 𝐵 → ((( bday
‘𝐴) +no ( bday ‘𝑦)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑧))) = ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑧)))) |
23 | 22 | eleq1d 2823 |
. . . 4
⊢ (𝑦 = 𝐵 → (((( bday
‘𝐴) +no ( bday ‘𝑦)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑧))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍))) ↔ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑧))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍))))) |
24 | | oveq2 7366 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝐴 +s 𝑦) = (𝐴 +s 𝐵)) |
25 | 24 | eleq1d 2823 |
. . . . 5
⊢ (𝑦 = 𝐵 → ((𝐴 +s 𝑦) ∈ No
↔ (𝐴 +s
𝐵) ∈ No )) |
26 | | breq1 5109 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝑦 <s 𝑧 ↔ 𝐵 <s 𝑧)) |
27 | | oveq1 7365 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑦 +s 𝐴) = (𝐵 +s 𝐴)) |
28 | 27 | breq1d 5116 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((𝑦 +s 𝐴) <s (𝑧 +s 𝐴) ↔ (𝐵 +s 𝐴) <s (𝑧 +s 𝐴))) |
29 | 26, 28 | imbi12d 345 |
. . . . 5
⊢ (𝑦 = 𝐵 → ((𝑦 <s 𝑧 → (𝑦 +s 𝐴) <s (𝑧 +s 𝐴)) ↔ (𝐵 <s 𝑧 → (𝐵 +s 𝐴) <s (𝑧 +s 𝐴)))) |
30 | 25, 29 | anbi12d 632 |
. . . 4
⊢ (𝑦 = 𝐵 → (((𝐴 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝐴) <s (𝑧 +s 𝐴))) ↔ ((𝐴 +s 𝐵) ∈ No
∧ (𝐵 <s 𝑧 → (𝐵 +s 𝐴) <s (𝑧 +s 𝐴))))) |
31 | 23, 30 | imbi12d 345 |
. . 3
⊢ (𝑦 = 𝐵 → ((((( bday
‘𝐴) +no ( bday ‘𝑦)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑧))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍))) → ((𝐴 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝐴) <s (𝑧 +s 𝐴)))) ↔ (((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑧))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍))) → ((𝐴 +s 𝐵) ∈ No
∧ (𝐵 <s 𝑧 → (𝐵 +s 𝐴) <s (𝑧 +s 𝐴)))))) |
32 | | fveq2 6843 |
. . . . . . 7
⊢ (𝑧 = 𝐶 → ( bday
‘𝑧) = ( bday ‘𝐶)) |
33 | 32 | oveq2d 7374 |
. . . . . 6
⊢ (𝑧 = 𝐶 → (( bday
‘𝐴) +no ( bday ‘𝑧)) = (( bday
‘𝐴) +no ( bday ‘𝐶))) |
34 | 33 | uneq2d 4124 |
. . . . 5
⊢ (𝑧 = 𝐶 → ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑧))) = ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (( bday
‘𝐴) +no ( bday ‘𝐶)))) |
35 | 34 | eleq1d 2823 |
. . . 4
⊢ (𝑧 = 𝐶 → (((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑧))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍))) ↔ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (( bday
‘𝐴) +no ( bday ‘𝐶))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍))))) |
36 | | breq2 5110 |
. . . . . 6
⊢ (𝑧 = 𝐶 → (𝐵 <s 𝑧 ↔ 𝐵 <s 𝐶)) |
37 | | oveq1 7365 |
. . . . . . 7
⊢ (𝑧 = 𝐶 → (𝑧 +s 𝐴) = (𝐶 +s 𝐴)) |
38 | 37 | breq2d 5118 |
. . . . . 6
⊢ (𝑧 = 𝐶 → ((𝐵 +s 𝐴) <s (𝑧 +s 𝐴) ↔ (𝐵 +s 𝐴) <s (𝐶 +s 𝐴))) |
39 | 36, 38 | imbi12d 345 |
. . . . 5
⊢ (𝑧 = 𝐶 → ((𝐵 <s 𝑧 → (𝐵 +s 𝐴) <s (𝑧 +s 𝐴)) ↔ (𝐵 <s 𝐶 → (𝐵 +s 𝐴) <s (𝐶 +s 𝐴)))) |
40 | 39 | anbi2d 630 |
. . . 4
⊢ (𝑧 = 𝐶 → (((𝐴 +s 𝐵) ∈ No
∧ (𝐵 <s 𝑧 → (𝐵 +s 𝐴) <s (𝑧 +s 𝐴))) ↔ ((𝐴 +s 𝐵) ∈ No
∧ (𝐵 <s 𝐶 → (𝐵 +s 𝐴) <s (𝐶 +s 𝐴))))) |
41 | 35, 40 | imbi12d 345 |
. . 3
⊢ (𝑧 = 𝐶 → ((((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑧))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍))) → ((𝐴 +s 𝐵) ∈ No
∧ (𝐵 <s 𝑧 → (𝐵 +s 𝐴) <s (𝑧 +s 𝐴)))) ↔ (((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (( bday
‘𝐴) +no ( bday ‘𝐶))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍))) → ((𝐴 +s 𝐵) ∈ No
∧ (𝐵 <s 𝐶 → (𝐵 +s 𝐴) <s (𝐶 +s 𝐴)))))) |
42 | 19, 31, 41 | rspc3v 3594 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐶 ∈ No )
→ (∀𝑥 ∈
No ∀𝑦 ∈ No
∀𝑧 ∈ No (((( bday ‘𝑥) +no (
bday ‘𝑦))
∪ (( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) → (((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (( bday
‘𝐴) +no ( bday ‘𝐶))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍))) → ((𝐴 +s 𝐵) ∈ No
∧ (𝐵 <s 𝐶 → (𝐵 +s 𝐴) <s (𝐶 +s 𝐴)))))) |
43 | 4, 5, 6, 42 | syl3c 66 |
1
⊢ (𝜑 → ((𝐴 +s 𝐵) ∈ No
∧ (𝐵 <s 𝐶 → (𝐵 +s 𝐴) <s (𝐶 +s 𝐴)))) |