MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pw2cut Structured version   Visualization version   GIF version

Theorem pw2cut 28429
Description: Extend halfcut 28425 to arbitrary powers of two. Part of theorem 4.2 of [Gonshor] p. 28. (Contributed by Scott Fenton, 18-Aug-2025.)
Hypotheses
Ref Expression
pw2cut.1 (𝜑𝐴 No )
pw2cut.2 (𝜑𝐵 No )
pw2cut.3 (𝜑𝑁 ∈ ℕ0s)
pw2cut.4 (𝜑𝐴 <s 𝐵)
pw2cut.5 (𝜑 → ({(2s ·s 𝐴)} |s {(2s ·s 𝐵)}) = (𝐴 +s 𝐵))
Assertion
Ref Expression
pw2cut (𝜑 → ({(𝐴 /su (2ss𝑁))} |s {(𝐵 /su (2ss𝑁))}) = ((𝐴 +s 𝐵) /su (2ss(𝑁 +s 1s ))))

Proof of Theorem pw2cut
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pw2cut.3 . 2 (𝜑𝑁 ∈ ℕ0s)
2 oveq2 7453 . . . . . . . . 9 (𝑥 = 0s → (2ss𝑥) = (2ss 0s ))
3 2sno 28412 . . . . . . . . . 10 2s No
4 exps0 28419 . . . . . . . . . 10 (2s No → (2ss 0s ) = 1s )
53, 4ax-mp 5 . . . . . . . . 9 (2ss 0s ) = 1s
62, 5eqtrdi 2790 . . . . . . . 8 (𝑥 = 0s → (2ss𝑥) = 1s )
76oveq2d 7461 . . . . . . 7 (𝑥 = 0s → (𝐴 /su (2ss𝑥)) = (𝐴 /su 1s ))
87sneqd 4660 . . . . . 6 (𝑥 = 0s → {(𝐴 /su (2ss𝑥))} = {(𝐴 /su 1s )})
96oveq2d 7461 . . . . . . 7 (𝑥 = 0s → (𝐵 /su (2ss𝑥)) = (𝐵 /su 1s ))
109sneqd 4660 . . . . . 6 (𝑥 = 0s → {(𝐵 /su (2ss𝑥))} = {(𝐵 /su 1s )})
118, 10oveq12d 7463 . . . . 5 (𝑥 = 0s → ({(𝐴 /su (2ss𝑥))} |s {(𝐵 /su (2ss𝑥))}) = ({(𝐴 /su 1s )} |s {(𝐵 /su 1s )}))
12 oveq1 7452 . . . . . . . . 9 (𝑥 = 0s → (𝑥 +s 1s ) = ( 0s +s 1s ))
13 1sno 27881 . . . . . . . . . 10 1s No
14 addslid 28010 . . . . . . . . . 10 ( 1s No → ( 0s +s 1s ) = 1s )
1513, 14ax-mp 5 . . . . . . . . 9 ( 0s +s 1s ) = 1s
1612, 15eqtrdi 2790 . . . . . . . 8 (𝑥 = 0s → (𝑥 +s 1s ) = 1s )
1716oveq2d 7461 . . . . . . 7 (𝑥 = 0s → (2ss(𝑥 +s 1s )) = (2ss 1s ))
18 exps1 28420 . . . . . . . 8 (2s No → (2ss 1s ) = 2s)
193, 18ax-mp 5 . . . . . . 7 (2ss 1s ) = 2s
2017, 19eqtrdi 2790 . . . . . 6 (𝑥 = 0s → (2ss(𝑥 +s 1s )) = 2s)
2120oveq2d 7461 . . . . 5 (𝑥 = 0s → ((𝐴 +s 𝐵) /su (2ss(𝑥 +s 1s ))) = ((𝐴 +s 𝐵) /su 2s))
2211, 21eqeq12d 2750 . . . 4 (𝑥 = 0s → (({(𝐴 /su (2ss𝑥))} |s {(𝐵 /su (2ss𝑥))}) = ((𝐴 +s 𝐵) /su (2ss(𝑥 +s 1s ))) ↔ ({(𝐴 /su 1s )} |s {(𝐵 /su 1s )}) = ((𝐴 +s 𝐵) /su 2s)))
2322imbi2d 340 . . 3 (𝑥 = 0s → ((𝜑 → ({(𝐴 /su (2ss𝑥))} |s {(𝐵 /su (2ss𝑥))}) = ((𝐴 +s 𝐵) /su (2ss(𝑥 +s 1s )))) ↔ (𝜑 → ({(𝐴 /su 1s )} |s {(𝐵 /su 1s )}) = ((𝐴 +s 𝐵) /su 2s))))
24 oveq2 7453 . . . . . . . 8 (𝑥 = 𝑦 → (2ss𝑥) = (2ss𝑦))
2524oveq2d 7461 . . . . . . 7 (𝑥 = 𝑦 → (𝐴 /su (2ss𝑥)) = (𝐴 /su (2ss𝑦)))
2625sneqd 4660 . . . . . 6 (𝑥 = 𝑦 → {(𝐴 /su (2ss𝑥))} = {(𝐴 /su (2ss𝑦))})
2724oveq2d 7461 . . . . . . 7 (𝑥 = 𝑦 → (𝐵 /su (2ss𝑥)) = (𝐵 /su (2ss𝑦)))
2827sneqd 4660 . . . . . 6 (𝑥 = 𝑦 → {(𝐵 /su (2ss𝑥))} = {(𝐵 /su (2ss𝑦))})
2926, 28oveq12d 7463 . . . . 5 (𝑥 = 𝑦 → ({(𝐴 /su (2ss𝑥))} |s {(𝐵 /su (2ss𝑥))}) = ({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}))
30 oveq1 7452 . . . . . . 7 (𝑥 = 𝑦 → (𝑥 +s 1s ) = (𝑦 +s 1s ))
3130oveq2d 7461 . . . . . 6 (𝑥 = 𝑦 → (2ss(𝑥 +s 1s )) = (2ss(𝑦 +s 1s )))
3231oveq2d 7461 . . . . 5 (𝑥 = 𝑦 → ((𝐴 +s 𝐵) /su (2ss(𝑥 +s 1s ))) = ((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s ))))
3329, 32eqeq12d 2750 . . . 4 (𝑥 = 𝑦 → (({(𝐴 /su (2ss𝑥))} |s {(𝐵 /su (2ss𝑥))}) = ((𝐴 +s 𝐵) /su (2ss(𝑥 +s 1s ))) ↔ ({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}) = ((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s )))))
3433imbi2d 340 . . 3 (𝑥 = 𝑦 → ((𝜑 → ({(𝐴 /su (2ss𝑥))} |s {(𝐵 /su (2ss𝑥))}) = ((𝐴 +s 𝐵) /su (2ss(𝑥 +s 1s )))) ↔ (𝜑 → ({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}) = ((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s ))))))
35 oveq2 7453 . . . . . . . 8 (𝑥 = (𝑦 +s 1s ) → (2ss𝑥) = (2ss(𝑦 +s 1s )))
3635oveq2d 7461 . . . . . . 7 (𝑥 = (𝑦 +s 1s ) → (𝐴 /su (2ss𝑥)) = (𝐴 /su (2ss(𝑦 +s 1s ))))
3736sneqd 4660 . . . . . 6 (𝑥 = (𝑦 +s 1s ) → {(𝐴 /su (2ss𝑥))} = {(𝐴 /su (2ss(𝑦 +s 1s )))})
3835oveq2d 7461 . . . . . . 7 (𝑥 = (𝑦 +s 1s ) → (𝐵 /su (2ss𝑥)) = (𝐵 /su (2ss(𝑦 +s 1s ))))
3938sneqd 4660 . . . . . 6 (𝑥 = (𝑦 +s 1s ) → {(𝐵 /su (2ss𝑥))} = {(𝐵 /su (2ss(𝑦 +s 1s )))})
4037, 39oveq12d 7463 . . . . 5 (𝑥 = (𝑦 +s 1s ) → ({(𝐴 /su (2ss𝑥))} |s {(𝐵 /su (2ss𝑥))}) = ({(𝐴 /su (2ss(𝑦 +s 1s )))} |s {(𝐵 /su (2ss(𝑦 +s 1s )))}))
41 oveq1 7452 . . . . . . 7 (𝑥 = (𝑦 +s 1s ) → (𝑥 +s 1s ) = ((𝑦 +s 1s ) +s 1s ))
4241oveq2d 7461 . . . . . 6 (𝑥 = (𝑦 +s 1s ) → (2ss(𝑥 +s 1s )) = (2ss((𝑦 +s 1s ) +s 1s )))
4342oveq2d 7461 . . . . 5 (𝑥 = (𝑦 +s 1s ) → ((𝐴 +s 𝐵) /su (2ss(𝑥 +s 1s ))) = ((𝐴 +s 𝐵) /su (2ss((𝑦 +s 1s ) +s 1s ))))
4440, 43eqeq12d 2750 . . . 4 (𝑥 = (𝑦 +s 1s ) → (({(𝐴 /su (2ss𝑥))} |s {(𝐵 /su (2ss𝑥))}) = ((𝐴 +s 𝐵) /su (2ss(𝑥 +s 1s ))) ↔ ({(𝐴 /su (2ss(𝑦 +s 1s )))} |s {(𝐵 /su (2ss(𝑦 +s 1s )))}) = ((𝐴 +s 𝐵) /su (2ss((𝑦 +s 1s ) +s 1s )))))
4544imbi2d 340 . . 3 (𝑥 = (𝑦 +s 1s ) → ((𝜑 → ({(𝐴 /su (2ss𝑥))} |s {(𝐵 /su (2ss𝑥))}) = ((𝐴 +s 𝐵) /su (2ss(𝑥 +s 1s )))) ↔ (𝜑 → ({(𝐴 /su (2ss(𝑦 +s 1s )))} |s {(𝐵 /su (2ss(𝑦 +s 1s )))}) = ((𝐴 +s 𝐵) /su (2ss((𝑦 +s 1s ) +s 1s ))))))
46 oveq2 7453 . . . . . . . 8 (𝑥 = 𝑁 → (2ss𝑥) = (2ss𝑁))
4746oveq2d 7461 . . . . . . 7 (𝑥 = 𝑁 → (𝐴 /su (2ss𝑥)) = (𝐴 /su (2ss𝑁)))
4847sneqd 4660 . . . . . 6 (𝑥 = 𝑁 → {(𝐴 /su (2ss𝑥))} = {(𝐴 /su (2ss𝑁))})
4946oveq2d 7461 . . . . . . 7 (𝑥 = 𝑁 → (𝐵 /su (2ss𝑥)) = (𝐵 /su (2ss𝑁)))
5049sneqd 4660 . . . . . 6 (𝑥 = 𝑁 → {(𝐵 /su (2ss𝑥))} = {(𝐵 /su (2ss𝑁))})
5148, 50oveq12d 7463 . . . . 5 (𝑥 = 𝑁 → ({(𝐴 /su (2ss𝑥))} |s {(𝐵 /su (2ss𝑥))}) = ({(𝐴 /su (2ss𝑁))} |s {(𝐵 /su (2ss𝑁))}))
52 oveq1 7452 . . . . . . 7 (𝑥 = 𝑁 → (𝑥 +s 1s ) = (𝑁 +s 1s ))
5352oveq2d 7461 . . . . . 6 (𝑥 = 𝑁 → (2ss(𝑥 +s 1s )) = (2ss(𝑁 +s 1s )))
5453oveq2d 7461 . . . . 5 (𝑥 = 𝑁 → ((𝐴 +s 𝐵) /su (2ss(𝑥 +s 1s ))) = ((𝐴 +s 𝐵) /su (2ss(𝑁 +s 1s ))))
5551, 54eqeq12d 2750 . . . 4 (𝑥 = 𝑁 → (({(𝐴 /su (2ss𝑥))} |s {(𝐵 /su (2ss𝑥))}) = ((𝐴 +s 𝐵) /su (2ss(𝑥 +s 1s ))) ↔ ({(𝐴 /su (2ss𝑁))} |s {(𝐵 /su (2ss𝑁))}) = ((𝐴 +s 𝐵) /su (2ss(𝑁 +s 1s )))))
5655imbi2d 340 . . 3 (𝑥 = 𝑁 → ((𝜑 → ({(𝐴 /su (2ss𝑥))} |s {(𝐵 /su (2ss𝑥))}) = ((𝐴 +s 𝐵) /su (2ss(𝑥 +s 1s )))) ↔ (𝜑 → ({(𝐴 /su (2ss𝑁))} |s {(𝐵 /su (2ss𝑁))}) = ((𝐴 +s 𝐵) /su (2ss(𝑁 +s 1s ))))))
57 pw2cut.1 . . . . . . 7 (𝜑𝐴 No )
58 divs1 28238 . . . . . . 7 (𝐴 No → (𝐴 /su 1s ) = 𝐴)
5957, 58syl 17 . . . . . 6 (𝜑 → (𝐴 /su 1s ) = 𝐴)
6059sneqd 4660 . . . . 5 (𝜑 → {(𝐴 /su 1s )} = {𝐴})
61 pw2cut.2 . . . . . . 7 (𝜑𝐵 No )
62 divs1 28238 . . . . . . 7 (𝐵 No → (𝐵 /su 1s ) = 𝐵)
6361, 62syl 17 . . . . . 6 (𝜑 → (𝐵 /su 1s ) = 𝐵)
6463sneqd 4660 . . . . 5 (𝜑 → {(𝐵 /su 1s )} = {𝐵})
6560, 64oveq12d 7463 . . . 4 (𝜑 → ({(𝐴 /su 1s )} |s {(𝐵 /su 1s )}) = ({𝐴} |s {𝐵}))
66 pw2cut.4 . . . . 5 (𝜑𝐴 <s 𝐵)
67 pw2cut.5 . . . . 5 (𝜑 → ({(2s ·s 𝐴)} |s {(2s ·s 𝐵)}) = (𝐴 +s 𝐵))
68 eqid 2734 . . . . 5 ({𝐴} |s {𝐵}) = ({𝐴} |s {𝐵})
6957, 61, 66, 67, 68halfcut 28425 . . . 4 (𝜑 → ({𝐴} |s {𝐵}) = ((𝐴 +s 𝐵) /su 2s))
7065, 69eqtrd 2774 . . 3 (𝜑 → ({(𝐴 /su 1s )} |s {(𝐵 /su 1s )}) = ((𝐴 +s 𝐵) /su 2s))
7157adantl 481 . . . . . . . . . 10 ((𝑦 ∈ ℕ0s𝜑) → 𝐴 No )
72 peano2n0s 28344 . . . . . . . . . . . 12 (𝑦 ∈ ℕ0s → (𝑦 +s 1s ) ∈ ℕ0s)
73 expscl 28422 . . . . . . . . . . . 12 ((2s No ∧ (𝑦 +s 1s ) ∈ ℕ0s) → (2ss(𝑦 +s 1s )) ∈ No )
743, 72, 73sylancr 586 . . . . . . . . . . 11 (𝑦 ∈ ℕ0s → (2ss(𝑦 +s 1s )) ∈ No )
7574adantr 480 . . . . . . . . . 10 ((𝑦 ∈ ℕ0s𝜑) → (2ss(𝑦 +s 1s )) ∈ No )
76 2ne0s 28413 . . . . . . . . . . . . 13 2s ≠ 0s
77 expsne0 28423 . . . . . . . . . . . . 13 ((2s No ∧ 2s ≠ 0s ∧ (𝑦 +s 1s ) ∈ ℕ0s) → (2ss(𝑦 +s 1s )) ≠ 0s )
783, 76, 77mp3an12 1451 . . . . . . . . . . . 12 ((𝑦 +s 1s ) ∈ ℕ0s → (2ss(𝑦 +s 1s )) ≠ 0s )
7972, 78syl 17 . . . . . . . . . . 11 (𝑦 ∈ ℕ0s → (2ss(𝑦 +s 1s )) ≠ 0s )
8079adantr 480 . . . . . . . . . 10 ((𝑦 ∈ ℕ0s𝜑) → (2ss(𝑦 +s 1s )) ≠ 0s )
8171, 75, 80divscld 28257 . . . . . . . . 9 ((𝑦 ∈ ℕ0s𝜑) → (𝐴 /su (2ss(𝑦 +s 1s ))) ∈ No )
82813adant3 1132 . . . . . . . 8 ((𝑦 ∈ ℕ0s𝜑 ∧ ({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}) = ((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s )))) → (𝐴 /su (2ss(𝑦 +s 1s ))) ∈ No )
8361adantl 481 . . . . . . . . . 10 ((𝑦 ∈ ℕ0s𝜑) → 𝐵 No )
8483, 75, 80divscld 28257 . . . . . . . . 9 ((𝑦 ∈ ℕ0s𝜑) → (𝐵 /su (2ss(𝑦 +s 1s ))) ∈ No )
85843adant3 1132 . . . . . . . 8 ((𝑦 ∈ ℕ0s𝜑 ∧ ({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}) = ((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s )))) → (𝐵 /su (2ss(𝑦 +s 1s ))) ∈ No )
8671, 75, 80divscan1d 28259 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0s𝜑) → ((𝐴 /su (2ss(𝑦 +s 1s ))) ·s (2ss(𝑦 +s 1s ))) = 𝐴)
8766adantl 481 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0s𝜑) → 𝐴 <s 𝐵)
8886, 87eqbrtrd 5191 . . . . . . . . . 10 ((𝑦 ∈ ℕ0s𝜑) → ((𝐴 /su (2ss(𝑦 +s 1s ))) ·s (2ss(𝑦 +s 1s ))) <s 𝐵)
89 2nns 28411 . . . . . . . . . . . . . . 15 2s ∈ ℕs
90 nnsgt0 28351 . . . . . . . . . . . . . . 15 (2s ∈ ℕs → 0s <s 2s)
9189, 90ax-mp 5 . . . . . . . . . . . . . 14 0s <s 2s
92 expsgt0 28424 . . . . . . . . . . . . . 14 ((2s No ∧ (𝑦 +s 1s ) ∈ ℕ0s ∧ 0s <s 2s) → 0s <s (2ss(𝑦 +s 1s )))
933, 91, 92mp3an13 1452 . . . . . . . . . . . . 13 ((𝑦 +s 1s ) ∈ ℕ0s → 0s <s (2ss(𝑦 +s 1s )))
9472, 93syl 17 . . . . . . . . . . . 12 (𝑦 ∈ ℕ0s → 0s <s (2ss(𝑦 +s 1s )))
9594adantr 480 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0s𝜑) → 0s <s (2ss(𝑦 +s 1s )))
9681, 83, 75, 95sltmuldivd 28262 . . . . . . . . . 10 ((𝑦 ∈ ℕ0s𝜑) → (((𝐴 /su (2ss(𝑦 +s 1s ))) ·s (2ss(𝑦 +s 1s ))) <s 𝐵 ↔ (𝐴 /su (2ss(𝑦 +s 1s ))) <s (𝐵 /su (2ss(𝑦 +s 1s )))))
9788, 96mpbid 232 . . . . . . . . 9 ((𝑦 ∈ ℕ0s𝜑) → (𝐴 /su (2ss(𝑦 +s 1s ))) <s (𝐵 /su (2ss(𝑦 +s 1s ))))
98973adant3 1132 . . . . . . . 8 ((𝑦 ∈ ℕ0s𝜑 ∧ ({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}) = ((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s )))) → (𝐴 /su (2ss(𝑦 +s 1s ))) <s (𝐵 /su (2ss(𝑦 +s 1s ))))
99 expsp1 28421 . . . . . . . . . . . . . . . . . . 19 ((2s No 𝑦 ∈ ℕ0s) → (2ss(𝑦 +s 1s )) = ((2ss𝑦) ·s 2s))
1003, 99mpan 689 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ0s → (2ss(𝑦 +s 1s )) = ((2ss𝑦) ·s 2s))
101100adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℕ0s𝜑) → (2ss(𝑦 +s 1s )) = ((2ss𝑦) ·s 2s))
102101oveq2d 7461 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ0s𝜑) → (𝐴 /su (2ss(𝑦 +s 1s ))) = (𝐴 /su ((2ss𝑦) ·s 2s)))
103 expscl 28422 . . . . . . . . . . . . . . . . . . 19 ((2s No 𝑦 ∈ ℕ0s) → (2ss𝑦) ∈ No )
1043, 103mpan 689 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ0s → (2ss𝑦) ∈ No )
105104adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℕ0s𝜑) → (2ss𝑦) ∈ No )
1063a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℕ0s𝜑) → 2s No )
107 expsne0 28423 . . . . . . . . . . . . . . . . . . 19 ((2s No ∧ 2s ≠ 0s𝑦 ∈ ℕ0s) → (2ss𝑦) ≠ 0s )
1083, 76, 107mp3an12 1451 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ0s → (2ss𝑦) ≠ 0s )
109108adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℕ0s𝜑) → (2ss𝑦) ≠ 0s )
11076a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℕ0s𝜑) → 2s ≠ 0s )
11171, 105, 106, 109, 110divdivs1d 28266 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ0s𝜑) → ((𝐴 /su (2ss𝑦)) /su 2s) = (𝐴 /su ((2ss𝑦) ·s 2s)))
112102, 111eqtr4d 2777 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0s𝜑) → (𝐴 /su (2ss(𝑦 +s 1s ))) = ((𝐴 /su (2ss𝑦)) /su 2s))
113112oveq2d 7461 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ0s𝜑) → (2s ·s (𝐴 /su (2ss(𝑦 +s 1s )))) = (2s ·s ((𝐴 /su (2ss𝑦)) /su 2s)))
11471, 105, 109divscld 28257 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0s𝜑) → (𝐴 /su (2ss𝑦)) ∈ No )
115114, 106, 110divscan2d 28258 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ0s𝜑) → (2s ·s ((𝐴 /su (2ss𝑦)) /su 2s)) = (𝐴 /su (2ss𝑦)))
116113, 115eqtrd 2774 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ0s𝜑) → (2s ·s (𝐴 /su (2ss(𝑦 +s 1s )))) = (𝐴 /su (2ss𝑦)))
117116sneqd 4660 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ0s𝜑) → {(2s ·s (𝐴 /su (2ss(𝑦 +s 1s ))))} = {(𝐴 /su (2ss𝑦))})
118101oveq2d 7461 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ0s𝜑) → (𝐵 /su (2ss(𝑦 +s 1s ))) = (𝐵 /su ((2ss𝑦) ·s 2s)))
11983, 105, 106, 109, 110divdivs1d 28266 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ0s𝜑) → ((𝐵 /su (2ss𝑦)) /su 2s) = (𝐵 /su ((2ss𝑦) ·s 2s)))
120118, 119eqtr4d 2777 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0s𝜑) → (𝐵 /su (2ss(𝑦 +s 1s ))) = ((𝐵 /su (2ss𝑦)) /su 2s))
121120oveq2d 7461 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ0s𝜑) → (2s ·s (𝐵 /su (2ss(𝑦 +s 1s )))) = (2s ·s ((𝐵 /su (2ss𝑦)) /su 2s)))
12283, 105, 109divscld 28257 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0s𝜑) → (𝐵 /su (2ss𝑦)) ∈ No )
123122, 106, 110divscan2d 28258 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ0s𝜑) → (2s ·s ((𝐵 /su (2ss𝑦)) /su 2s)) = (𝐵 /su (2ss𝑦)))
124121, 123eqtrd 2774 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ0s𝜑) → (2s ·s (𝐵 /su (2ss(𝑦 +s 1s )))) = (𝐵 /su (2ss𝑦)))
125124sneqd 4660 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ0s𝜑) → {(2s ·s (𝐵 /su (2ss(𝑦 +s 1s ))))} = {(𝐵 /su (2ss𝑦))})
126117, 125oveq12d 7463 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0s𝜑) → ({(2s ·s (𝐴 /su (2ss(𝑦 +s 1s ))))} |s {(2s ·s (𝐵 /su (2ss(𝑦 +s 1s ))))}) = ({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}))
127126eqcomd 2740 . . . . . . . . . 10 ((𝑦 ∈ ℕ0s𝜑) → ({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}) = ({(2s ·s (𝐴 /su (2ss(𝑦 +s 1s ))))} |s {(2s ·s (𝐵 /su (2ss(𝑦 +s 1s ))))}))
12871, 83, 75, 80divsdird 28268 . . . . . . . . . 10 ((𝑦 ∈ ℕ0s𝜑) → ((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s ))) = ((𝐴 /su (2ss(𝑦 +s 1s ))) +s (𝐵 /su (2ss(𝑦 +s 1s )))))
129127, 128eqeq12d 2750 . . . . . . . . 9 ((𝑦 ∈ ℕ0s𝜑) → (({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}) = ((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s ))) ↔ ({(2s ·s (𝐴 /su (2ss(𝑦 +s 1s ))))} |s {(2s ·s (𝐵 /su (2ss(𝑦 +s 1s ))))}) = ((𝐴 /su (2ss(𝑦 +s 1s ))) +s (𝐵 /su (2ss(𝑦 +s 1s ))))))
130129biimp3a 1469 . . . . . . . 8 ((𝑦 ∈ ℕ0s𝜑 ∧ ({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}) = ((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s )))) → ({(2s ·s (𝐴 /su (2ss(𝑦 +s 1s ))))} |s {(2s ·s (𝐵 /su (2ss(𝑦 +s 1s ))))}) = ((𝐴 /su (2ss(𝑦 +s 1s ))) +s (𝐵 /su (2ss(𝑦 +s 1s )))))
131 eqid 2734 . . . . . . . 8 ({(𝐴 /su (2ss(𝑦 +s 1s )))} |s {(𝐵 /su (2ss(𝑦 +s 1s )))}) = ({(𝐴 /su (2ss(𝑦 +s 1s )))} |s {(𝐵 /su (2ss(𝑦 +s 1s )))})
13282, 85, 98, 130, 131halfcut 28425 . . . . . . 7 ((𝑦 ∈ ℕ0s𝜑 ∧ ({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}) = ((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s )))) → ({(𝐴 /su (2ss(𝑦 +s 1s )))} |s {(𝐵 /su (2ss(𝑦 +s 1s )))}) = (((𝐴 /su (2ss(𝑦 +s 1s ))) +s (𝐵 /su (2ss(𝑦 +s 1s )))) /su 2s))
133128oveq1d 7460 . . . . . . . 8 ((𝑦 ∈ ℕ0s𝜑) → (((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s ))) /su 2s) = (((𝐴 /su (2ss(𝑦 +s 1s ))) +s (𝐵 /su (2ss(𝑦 +s 1s )))) /su 2s))
1341333adant3 1132 . . . . . . 7 ((𝑦 ∈ ℕ0s𝜑 ∧ ({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}) = ((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s )))) → (((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s ))) /su 2s) = (((𝐴 /su (2ss(𝑦 +s 1s ))) +s (𝐵 /su (2ss(𝑦 +s 1s )))) /su 2s))
135132, 134eqtr4d 2777 . . . . . 6 ((𝑦 ∈ ℕ0s𝜑 ∧ ({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}) = ((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s )))) → ({(𝐴 /su (2ss(𝑦 +s 1s )))} |s {(𝐵 /su (2ss(𝑦 +s 1s )))}) = (((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s ))) /su 2s))
136 expsp1 28421 . . . . . . . . . . 11 ((2s No ∧ (𝑦 +s 1s ) ∈ ℕ0s) → (2ss((𝑦 +s 1s ) +s 1s )) = ((2ss(𝑦 +s 1s )) ·s 2s))
1373, 72, 136sylancr 586 . . . . . . . . . 10 (𝑦 ∈ ℕ0s → (2ss((𝑦 +s 1s ) +s 1s )) = ((2ss(𝑦 +s 1s )) ·s 2s))
138137adantr 480 . . . . . . . . 9 ((𝑦 ∈ ℕ0s𝜑) → (2ss((𝑦 +s 1s ) +s 1s )) = ((2ss(𝑦 +s 1s )) ·s 2s))
139138oveq2d 7461 . . . . . . . 8 ((𝑦 ∈ ℕ0s𝜑) → ((𝐴 +s 𝐵) /su (2ss((𝑦 +s 1s ) +s 1s ))) = ((𝐴 +s 𝐵) /su ((2ss(𝑦 +s 1s )) ·s 2s)))
14071, 83addscld 28022 . . . . . . . . 9 ((𝑦 ∈ ℕ0s𝜑) → (𝐴 +s 𝐵) ∈ No )
141140, 75, 106, 80, 110divdivs1d 28266 . . . . . . . 8 ((𝑦 ∈ ℕ0s𝜑) → (((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s ))) /su 2s) = ((𝐴 +s 𝐵) /su ((2ss(𝑦 +s 1s )) ·s 2s)))
142139, 141eqtr4d 2777 . . . . . . 7 ((𝑦 ∈ ℕ0s𝜑) → ((𝐴 +s 𝐵) /su (2ss((𝑦 +s 1s ) +s 1s ))) = (((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s ))) /su 2s))
1431423adant3 1132 . . . . . 6 ((𝑦 ∈ ℕ0s𝜑 ∧ ({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}) = ((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s )))) → ((𝐴 +s 𝐵) /su (2ss((𝑦 +s 1s ) +s 1s ))) = (((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s ))) /su 2s))
144135, 143eqtr4d 2777 . . . . 5 ((𝑦 ∈ ℕ0s𝜑 ∧ ({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}) = ((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s )))) → ({(𝐴 /su (2ss(𝑦 +s 1s )))} |s {(𝐵 /su (2ss(𝑦 +s 1s )))}) = ((𝐴 +s 𝐵) /su (2ss((𝑦 +s 1s ) +s 1s ))))
1451443exp 1119 . . . 4 (𝑦 ∈ ℕ0s → (𝜑 → (({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}) = ((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s ))) → ({(𝐴 /su (2ss(𝑦 +s 1s )))} |s {(𝐵 /su (2ss(𝑦 +s 1s )))}) = ((𝐴 +s 𝐵) /su (2ss((𝑦 +s 1s ) +s 1s ))))))
146145a2d 29 . . 3 (𝑦 ∈ ℕ0s → ((𝜑 → ({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}) = ((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s )))) → (𝜑 → ({(𝐴 /su (2ss(𝑦 +s 1s )))} |s {(𝐵 /su (2ss(𝑦 +s 1s )))}) = ((𝐴 +s 𝐵) /su (2ss((𝑦 +s 1s ) +s 1s ))))))
14723, 34, 45, 56, 70, 146n0sind 28346 . 2 (𝑁 ∈ ℕ0s → (𝜑 → ({(𝐴 /su (2ss𝑁))} |s {(𝐵 /su (2ss𝑁))}) = ((𝐴 +s 𝐵) /su (2ss(𝑁 +s 1s )))))
1481, 147mpcom 38 1 (𝜑 → ({(𝐴 /su (2ss𝑁))} |s {(𝐵 /su (2ss𝑁))}) = ((𝐴 +s 𝐵) /su (2ss(𝑁 +s 1s ))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087   = wceq 1537  wcel 2103  wne 2942  {csn 4648   class class class wbr 5169  (class class class)co 7445   No csur 27693   <s cslt 27694   |s cscut 27836   0s c0s 27876   1s c1s 27877   +s cadds 28001   ·s cmuls 28141   /su cdivs 28222  0scnn0s 28327  scnns 28328  2sc2s 28403  scexps 28405
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705  ax-rep 5306  ax-sep 5320  ax-nul 5327  ax-pow 5386  ax-pr 5450  ax-un 7766  ax-dc 10511
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ne 2943  df-ral 3064  df-rex 3073  df-rmo 3383  df-reu 3384  df-rab 3439  df-v 3484  df-sbc 3799  df-csb 3916  df-dif 3973  df-un 3975  df-in 3977  df-ss 3987  df-pss 3990  df-nul 4348  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-ot 4657  df-uni 4932  df-int 4973  df-iun 5021  df-br 5170  df-opab 5232  df-mpt 5253  df-tr 5287  df-id 5597  df-eprel 5603  df-po 5611  df-so 5612  df-fr 5654  df-se 5655  df-we 5656  df-xp 5705  df-rel 5706  df-cnv 5707  df-co 5708  df-dm 5709  df-rn 5710  df-res 5711  df-ima 5712  df-pred 6331  df-ord 6397  df-on 6398  df-lim 6399  df-suc 6400  df-iota 6524  df-fun 6574  df-fn 6575  df-f 6576  df-f1 6577  df-fo 6578  df-f1o 6579  df-fv 6580  df-riota 7401  df-ov 7448  df-oprab 7449  df-mpo 7450  df-om 7900  df-1st 8026  df-2nd 8027  df-frecs 8318  df-wrecs 8349  df-recs 8423  df-rdg 8462  df-1o 8518  df-2o 8519  df-oadd 8522  df-nadd 8718  df-no 27696  df-slt 27697  df-bday 27698  df-sle 27799  df-sslt 27835  df-scut 27837  df-0s 27878  df-1s 27879  df-made 27895  df-old 27896  df-left 27898  df-right 27899  df-norec 27980  df-norec2 27991  df-adds 28002  df-negs 28062  df-subs 28063  df-muls 28142  df-divs 28223  df-seqs 28299  df-n0s 28329  df-nns 28330  df-zs 28374  df-2s 28404  df-exps 28406
This theorem is referenced by:  zs12bday  28433
  Copyright terms: Public domain W3C validator