| Step | Hyp | Ref
| Expression |
| 1 | | nnsex 28323 |
. . . 4
⊢
ℕs ∈ V |
| 2 | 1 | abrexex 7987 |
. . 3
⊢ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))}
∈ V |
| 3 | 2 | a1i 11 |
. 2
⊢ (𝐴 ∈
No → {𝑥
∣ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 -s (
1s /su 𝑛))} ∈ V) |
| 4 | 1 | abrexex 7987 |
. . 3
⊢ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}
∈ V |
| 5 | 4 | a1i 11 |
. 2
⊢ (𝐴 ∈
No → {𝑥
∣ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 +s (
1s /su 𝑛))} ∈ V) |
| 6 | | 1sno 27872 |
. . . . . . . 8
⊢
1s ∈ No |
| 7 | 6 | a1i 11 |
. . . . . . 7
⊢ (𝑛 ∈ ℕs
→ 1s ∈ No ) |
| 8 | | nnsno 28329 |
. . . . . . 7
⊢ (𝑛 ∈ ℕs
→ 𝑛 ∈ No ) |
| 9 | | nnne0s 28340 |
. . . . . . 7
⊢ (𝑛 ∈ ℕs
→ 𝑛 ≠ 0s
) |
| 10 | 7, 8, 9 | divscld 28248 |
. . . . . 6
⊢ (𝑛 ∈ ℕs
→ ( 1s /su 𝑛) ∈ No
) |
| 11 | | subscl 28092 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ ( 1s /su 𝑛) ∈ No )
→ (𝐴 -s (
1s /su 𝑛)) ∈ No
) |
| 12 | 10, 11 | sylan2 593 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (𝐴 -s ( 1s
/su 𝑛))
∈ No ) |
| 13 | | eleq1 2829 |
. . . . 5
⊢ (𝑥 = (𝐴 -s ( 1s
/su 𝑛))
→ (𝑥 ∈ No ↔ (𝐴 -s ( 1s
/su 𝑛))
∈ No )) |
| 14 | 12, 13 | syl5ibrcom 247 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (𝑥 = (𝐴 -s ( 1s
/su 𝑛))
→ 𝑥 ∈ No )) |
| 15 | 14 | rexlimdva 3155 |
. . 3
⊢ (𝐴 ∈
No → (∃𝑛
∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))
→ 𝑥 ∈ No )) |
| 16 | 15 | abssdv 4068 |
. 2
⊢ (𝐴 ∈
No → {𝑥
∣ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 -s (
1s /su 𝑛))} ⊆ No
) |
| 17 | | addscl 28014 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ ( 1s /su 𝑛) ∈ No )
→ (𝐴 +s (
1s /su 𝑛)) ∈ No
) |
| 18 | 10, 17 | sylan2 593 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (𝐴 +s ( 1s
/su 𝑛))
∈ No ) |
| 19 | | eleq1 2829 |
. . . . 5
⊢ (𝑥 = (𝐴 +s ( 1s
/su 𝑛))
→ (𝑥 ∈ No ↔ (𝐴 +s ( 1s
/su 𝑛))
∈ No )) |
| 20 | 18, 19 | syl5ibrcom 247 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (𝑥 = (𝐴 +s ( 1s
/su 𝑛))
→ 𝑥 ∈ No )) |
| 21 | 20 | rexlimdva 3155 |
. . 3
⊢ (𝐴 ∈
No → (∃𝑛
∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))
→ 𝑥 ∈ No )) |
| 22 | 21 | abssdv 4068 |
. 2
⊢ (𝐴 ∈
No → {𝑥
∣ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 +s (
1s /su 𝑛))} ⊆ No
) |
| 23 | | vex 3484 |
. . . . . . 7
⊢ 𝑦 ∈ V |
| 24 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 = (𝐴 -s ( 1s
/su 𝑛))
↔ 𝑦 = (𝐴 -s ( 1s
/su 𝑛)))) |
| 25 | 24 | rexbidv 3179 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))
↔ ∃𝑛 ∈
ℕs 𝑦 =
(𝐴 -s (
1s /su 𝑛)))) |
| 26 | 23, 25 | elab 3679 |
. . . . . 6
⊢ (𝑦 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}
↔ ∃𝑛 ∈
ℕs 𝑦 =
(𝐴 -s (
1s /su 𝑛))) |
| 27 | | vex 3484 |
. . . . . . 7
⊢ 𝑧 ∈ V |
| 28 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑥 = (𝐴 +s ( 1s
/su 𝑛))
↔ 𝑧 = (𝐴 +s ( 1s
/su 𝑛)))) |
| 29 | 28 | rexbidv 3179 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))
↔ ∃𝑛 ∈
ℕs 𝑧 =
(𝐴 +s (
1s /su 𝑛)))) |
| 30 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → ( 1s /su
𝑛) = ( 1s
/su 𝑚)) |
| 31 | 30 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (𝐴 +s ( 1s
/su 𝑛)) =
(𝐴 +s (
1s /su 𝑚))) |
| 32 | 31 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (𝑧 = (𝐴 +s ( 1s
/su 𝑛))
↔ 𝑧 = (𝐴 +s ( 1s
/su 𝑚)))) |
| 33 | 32 | cbvrexvw 3238 |
. . . . . . . 8
⊢
(∃𝑛 ∈
ℕs 𝑧 =
(𝐴 +s (
1s /su 𝑛)) ↔ ∃𝑚 ∈ ℕs 𝑧 = (𝐴 +s ( 1s
/su 𝑚))) |
| 34 | 29, 33 | bitrdi 287 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))
↔ ∃𝑚 ∈
ℕs 𝑧 =
(𝐴 +s (
1s /su 𝑚)))) |
| 35 | 27, 34 | elab 3679 |
. . . . . 6
⊢ (𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}
↔ ∃𝑚 ∈
ℕs 𝑧 =
(𝐴 +s (
1s /su 𝑚))) |
| 36 | 26, 35 | anbi12i 628 |
. . . . 5
⊢ ((𝑦 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}
∧ 𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})
↔ (∃𝑛 ∈
ℕs 𝑦 =
(𝐴 -s (
1s /su 𝑛)) ∧ ∃𝑚 ∈ ℕs 𝑧 = (𝐴 +s ( 1s
/su 𝑚)))) |
| 37 | | reeanv 3229 |
. . . . 5
⊢
(∃𝑛 ∈
ℕs ∃𝑚 ∈ ℕs (𝑦 = (𝐴 -s ( 1s
/su 𝑛))
∧ 𝑧 = (𝐴 +s ( 1s
/su 𝑚)))
↔ (∃𝑛 ∈
ℕs 𝑦 =
(𝐴 -s (
1s /su 𝑛)) ∧ ∃𝑚 ∈ ℕs 𝑧 = (𝐴 +s ( 1s
/su 𝑚)))) |
| 38 | 36, 37 | bitr4i 278 |
. . . 4
⊢ ((𝑦 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}
∧ 𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})
↔ ∃𝑛 ∈
ℕs ∃𝑚 ∈ ℕs (𝑦 = (𝐴 -s ( 1s
/su 𝑛))
∧ 𝑧 = (𝐴 +s ( 1s
/su 𝑚)))) |
| 39 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → 𝐴 ∈ No
) |
| 40 | 10 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( 1s /su 𝑛) ∈
No ) |
| 41 | 39, 40 | subsvald 28091 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (𝐴 -s ( 1s
/su 𝑛)) =
(𝐴 +s (
-us ‘( 1s /su 𝑛)))) |
| 42 | 41 | adantrr 717 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ (𝑛 ∈
ℕs ∧ 𝑚
∈ ℕs)) → (𝐴 -s ( 1s
/su 𝑛)) =
(𝐴 +s (
-us ‘( 1s /su 𝑛)))) |
| 43 | 10 | negscld 28069 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕs
→ ( -us ‘( 1s /su 𝑛)) ∈
No ) |
| 44 | 43 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → ( -us ‘( 1s
/su 𝑛))
∈ No ) |
| 45 | | 0sno 27871 |
. . . . . . . . . . 11
⊢
0s ∈ No |
| 46 | 45 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → 0s ∈ No
) |
| 47 | 6 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕs
→ 1s ∈ No ) |
| 48 | | nnsno 28329 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕs
→ 𝑚 ∈ No ) |
| 49 | | nnne0s 28340 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕs
→ 𝑚 ≠ 0s
) |
| 50 | 47, 48, 49 | divscld 28248 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕs
→ ( 1s /su 𝑚) ∈ No
) |
| 51 | 50 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → ( 1s /su 𝑚) ∈
No ) |
| 52 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕs
→ 𝑛 ∈
ℕs) |
| 53 | 52 | nnsrecgt0d 28356 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕs
→ 0s <s ( 1s /su 𝑛)) |
| 54 | 45 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕs
→ 0s ∈ No ) |
| 55 | 54, 10 | sltnegd 28079 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕs
→ ( 0s <s ( 1s /su 𝑛) ↔ ( -us
‘( 1s /su 𝑛)) <s ( -us ‘
0s ))) |
| 56 | 53, 55 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕs
→ ( -us ‘( 1s /su 𝑛)) <s ( -us
‘ 0s )) |
| 57 | | negs0s 28058 |
. . . . . . . . . . . 12
⊢ (
-us ‘ 0s ) = 0s |
| 58 | 56, 57 | breqtrdi 5184 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕs
→ ( -us ‘( 1s /su 𝑛)) <s 0s
) |
| 59 | 58 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → ( -us ‘( 1s
/su 𝑛))
<s 0s ) |
| 60 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕs
→ 𝑚 ∈
ℕs) |
| 61 | 60 | nnsrecgt0d 28356 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕs
→ 0s <s ( 1s /su 𝑚)) |
| 62 | 61 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → 0s <s ( 1s
/su 𝑚)) |
| 63 | 44, 46, 51, 59, 62 | slttrd 27804 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → ( -us ‘( 1s
/su 𝑛))
<s ( 1s /su 𝑚)) |
| 64 | 63 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ (𝑛 ∈
ℕs ∧ 𝑚
∈ ℕs)) → ( -us ‘( 1s
/su 𝑛))
<s ( 1s /su 𝑚)) |
| 65 | 44 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ (𝑛 ∈
ℕs ∧ 𝑚
∈ ℕs)) → ( -us ‘( 1s
/su 𝑛))
∈ No ) |
| 66 | 50 | ad2antll 729 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ (𝑛 ∈
ℕs ∧ 𝑚
∈ ℕs)) → ( 1s /su 𝑚) ∈
No ) |
| 67 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ (𝑛 ∈
ℕs ∧ 𝑚
∈ ℕs)) → 𝐴 ∈ No
) |
| 68 | 65, 66, 67 | sltadd2d 28030 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ (𝑛 ∈
ℕs ∧ 𝑚
∈ ℕs)) → (( -us ‘( 1s
/su 𝑛))
<s ( 1s /su 𝑚) ↔ (𝐴 +s ( -us ‘(
1s /su 𝑛))) <s (𝐴 +s ( 1s
/su 𝑚)))) |
| 69 | 64, 68 | mpbid 232 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ (𝑛 ∈
ℕs ∧ 𝑚
∈ ℕs)) → (𝐴 +s ( -us ‘(
1s /su 𝑛))) <s (𝐴 +s ( 1s
/su 𝑚))) |
| 70 | 42, 69 | eqbrtrd 5165 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ (𝑛 ∈
ℕs ∧ 𝑚
∈ ℕs)) → (𝐴 -s ( 1s
/su 𝑛))
<s (𝐴 +s (
1s /su 𝑚))) |
| 71 | | breq12 5148 |
. . . . . 6
⊢ ((𝑦 = (𝐴 -s ( 1s
/su 𝑛))
∧ 𝑧 = (𝐴 +s ( 1s
/su 𝑚)))
→ (𝑦 <s 𝑧 ↔ (𝐴 -s ( 1s
/su 𝑛))
<s (𝐴 +s (
1s /su 𝑚)))) |
| 72 | 70, 71 | syl5ibrcom 247 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ (𝑛 ∈
ℕs ∧ 𝑚
∈ ℕs)) → ((𝑦 = (𝐴 -s ( 1s
/su 𝑛))
∧ 𝑧 = (𝐴 +s ( 1s
/su 𝑚)))
→ 𝑦 <s 𝑧)) |
| 73 | 72 | rexlimdvva 3213 |
. . . 4
⊢ (𝐴 ∈
No → (∃𝑛
∈ ℕs ∃𝑚 ∈ ℕs (𝑦 = (𝐴 -s ( 1s
/su 𝑛))
∧ 𝑧 = (𝐴 +s ( 1s
/su 𝑚)))
→ 𝑦 <s 𝑧)) |
| 74 | 38, 73 | biimtrid 242 |
. . 3
⊢ (𝐴 ∈
No → ((𝑦
∈ {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 =
(𝐴 -s (
1s /su 𝑛))} ∧ 𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))})
→ 𝑦 <s 𝑧)) |
| 75 | 74 | 3impib 1117 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝑦 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))}
∧ 𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})
→ 𝑦 <s 𝑧) |
| 76 | 3, 5, 16, 22, 75 | ssltd 27836 |
1
⊢ (𝐴 ∈
No → {𝑥
∣ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 -s (
1s /su 𝑛))} <<s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}) |