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

Theorem pw2cut 28438
Description: Extend halfcut 28434 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 7456 . . . . . . . . 9 (𝑥 = 0s → (2ss𝑥) = (2ss 0s ))
3 2sno 28421 . . . . . . . . . 10 2s No
4 exps0 28428 . . . . . . . . . 10 (2s No → (2ss 0s ) = 1s )
53, 4ax-mp 5 . . . . . . . . 9 (2ss 0s ) = 1s
62, 5eqtrdi 2796 . . . . . . . 8 (𝑥 = 0s → (2ss𝑥) = 1s )
76oveq2d 7464 . . . . . . 7 (𝑥 = 0s → (𝐴 /su (2ss𝑥)) = (𝐴 /su 1s ))
87sneqd 4660 . . . . . 6 (𝑥 = 0s → {(𝐴 /su (2ss𝑥))} = {(𝐴 /su 1s )})
96oveq2d 7464 . . . . . . 7 (𝑥 = 0s → (𝐵 /su (2ss𝑥)) = (𝐵 /su 1s ))
109sneqd 4660 . . . . . 6 (𝑥 = 0s → {(𝐵 /su (2ss𝑥))} = {(𝐵 /su 1s )})
118, 10oveq12d 7466 . . . . 5 (𝑥 = 0s → ({(𝐴 /su (2ss𝑥))} |s {(𝐵 /su (2ss𝑥))}) = ({(𝐴 /su 1s )} |s {(𝐵 /su 1s )}))
12 oveq1 7455 . . . . . . . . 9 (𝑥 = 0s → (𝑥 +s 1s ) = ( 0s +s 1s ))
13 1sno 27890 . . . . . . . . . 10 1s No
14 addslid 28019 . . . . . . . . . 10 ( 1s No → ( 0s +s 1s ) = 1s )
1513, 14ax-mp 5 . . . . . . . . 9 ( 0s +s 1s ) = 1s
1612, 15eqtrdi 2796 . . . . . . . 8 (𝑥 = 0s → (𝑥 +s 1s ) = 1s )
1716oveq2d 7464 . . . . . . 7 (𝑥 = 0s → (2ss(𝑥 +s 1s )) = (2ss 1s ))
18 exps1 28429 . . . . . . . 8 (2s No → (2ss 1s ) = 2s)
193, 18ax-mp 5 . . . . . . 7 (2ss 1s ) = 2s
2017, 19eqtrdi 2796 . . . . . 6 (𝑥 = 0s → (2ss(𝑥 +s 1s )) = 2s)
2120oveq2d 7464 . . . . 5 (𝑥 = 0s → ((𝐴 +s 𝐵) /su (2ss(𝑥 +s 1s ))) = ((𝐴 +s 𝐵) /su 2s))
2211, 21eqeq12d 2756 . . . 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 7456 . . . . . . . 8 (𝑥 = 𝑦 → (2ss𝑥) = (2ss𝑦))
2524oveq2d 7464 . . . . . . 7 (𝑥 = 𝑦 → (𝐴 /su (2ss𝑥)) = (𝐴 /su (2ss𝑦)))
2625sneqd 4660 . . . . . 6 (𝑥 = 𝑦 → {(𝐴 /su (2ss𝑥))} = {(𝐴 /su (2ss𝑦))})
2724oveq2d 7464 . . . . . . 7 (𝑥 = 𝑦 → (𝐵 /su (2ss𝑥)) = (𝐵 /su (2ss𝑦)))
2827sneqd 4660 . . . . . 6 (𝑥 = 𝑦 → {(𝐵 /su (2ss𝑥))} = {(𝐵 /su (2ss𝑦))})
2926, 28oveq12d 7466 . . . . 5 (𝑥 = 𝑦 → ({(𝐴 /su (2ss𝑥))} |s {(𝐵 /su (2ss𝑥))}) = ({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}))
30 oveq1 7455 . . . . . . 7 (𝑥 = 𝑦 → (𝑥 +s 1s ) = (𝑦 +s 1s ))
3130oveq2d 7464 . . . . . 6 (𝑥 = 𝑦 → (2ss(𝑥 +s 1s )) = (2ss(𝑦 +s 1s )))
3231oveq2d 7464 . . . . 5 (𝑥 = 𝑦 → ((𝐴 +s 𝐵) /su (2ss(𝑥 +s 1s ))) = ((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s ))))
3329, 32eqeq12d 2756 . . . 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 7456 . . . . . . . 8 (𝑥 = (𝑦 +s 1s ) → (2ss𝑥) = (2ss(𝑦 +s 1s )))
3635oveq2d 7464 . . . . . . 7 (𝑥 = (𝑦 +s 1s ) → (𝐴 /su (2ss𝑥)) = (𝐴 /su (2ss(𝑦 +s 1s ))))
3736sneqd 4660 . . . . . 6 (𝑥 = (𝑦 +s 1s ) → {(𝐴 /su (2ss𝑥))} = {(𝐴 /su (2ss(𝑦 +s 1s )))})
3835oveq2d 7464 . . . . . . 7 (𝑥 = (𝑦 +s 1s ) → (𝐵 /su (2ss𝑥)) = (𝐵 /su (2ss(𝑦 +s 1s ))))
3938sneqd 4660 . . . . . 6 (𝑥 = (𝑦 +s 1s ) → {(𝐵 /su (2ss𝑥))} = {(𝐵 /su (2ss(𝑦 +s 1s )))})
4037, 39oveq12d 7466 . . . . 5 (𝑥 = (𝑦 +s 1s ) → ({(𝐴 /su (2ss𝑥))} |s {(𝐵 /su (2ss𝑥))}) = ({(𝐴 /su (2ss(𝑦 +s 1s )))} |s {(𝐵 /su (2ss(𝑦 +s 1s )))}))
41 oveq1 7455 . . . . . . 7 (𝑥 = (𝑦 +s 1s ) → (𝑥 +s 1s ) = ((𝑦 +s 1s ) +s 1s ))
4241oveq2d 7464 . . . . . 6 (𝑥 = (𝑦 +s 1s ) → (2ss(𝑥 +s 1s )) = (2ss((𝑦 +s 1s ) +s 1s )))
4342oveq2d 7464 . . . . 5 (𝑥 = (𝑦 +s 1s ) → ((𝐴 +s 𝐵) /su (2ss(𝑥 +s 1s ))) = ((𝐴 +s 𝐵) /su (2ss((𝑦 +s 1s ) +s 1s ))))
4440, 43eqeq12d 2756 . . . 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 7456 . . . . . . . 8 (𝑥 = 𝑁 → (2ss𝑥) = (2ss𝑁))
4746oveq2d 7464 . . . . . . 7 (𝑥 = 𝑁 → (𝐴 /su (2ss𝑥)) = (𝐴 /su (2ss𝑁)))
4847sneqd 4660 . . . . . 6 (𝑥 = 𝑁 → {(𝐴 /su (2ss𝑥))} = {(𝐴 /su (2ss𝑁))})
4946oveq2d 7464 . . . . . . 7 (𝑥 = 𝑁 → (𝐵 /su (2ss𝑥)) = (𝐵 /su (2ss𝑁)))
5049sneqd 4660 . . . . . 6 (𝑥 = 𝑁 → {(𝐵 /su (2ss𝑥))} = {(𝐵 /su (2ss𝑁))})
5148, 50oveq12d 7466 . . . . 5 (𝑥 = 𝑁 → ({(𝐴 /su (2ss𝑥))} |s {(𝐵 /su (2ss𝑥))}) = ({(𝐴 /su (2ss𝑁))} |s {(𝐵 /su (2ss𝑁))}))
52 oveq1 7455 . . . . . . 7 (𝑥 = 𝑁 → (𝑥 +s 1s ) = (𝑁 +s 1s ))
5352oveq2d 7464 . . . . . 6 (𝑥 = 𝑁 → (2ss(𝑥 +s 1s )) = (2ss(𝑁 +s 1s )))
5453oveq2d 7464 . . . . 5 (𝑥 = 𝑁 → ((𝐴 +s 𝐵) /su (2ss(𝑥 +s 1s ))) = ((𝐴 +s 𝐵) /su (2ss(𝑁 +s 1s ))))
5551, 54eqeq12d 2756 . . . 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 28247 . . . . . . 7 (𝐴 No → (𝐴 /su 1s ) = 𝐴)
5957, 58syl 17 . . . . . 6 (𝜑 → (𝐴 /su 1s ) = 𝐴)
6059sneqd 4660 . . . . 5 (𝜑 → {(𝐴 /su 1s )} = {𝐴})
61 pw2cut.2 . . . . . . 7 (𝜑𝐵 No )
62 divs1 28247 . . . . . . 7 (𝐵 No → (𝐵 /su 1s ) = 𝐵)
6361, 62syl 17 . . . . . 6 (𝜑 → (𝐵 /su 1s ) = 𝐵)
6463sneqd 4660 . . . . 5 (𝜑 → {(𝐵 /su 1s )} = {𝐵})
6560, 64oveq12d 7466 . . . 4 (𝜑 → ({(𝐴 /su 1s )} |s {(𝐵 /su 1s )}) = ({𝐴} |s {𝐵}))
66 pw2cut.4 . . . . 5 (𝜑𝐴 <s 𝐵)
67 pw2cut.5 . . . . 5 (𝜑 → ({(2s ·s 𝐴)} |s {(2s ·s 𝐵)}) = (𝐴 +s 𝐵))
68 eqid 2740 . . . . 5 ({𝐴} |s {𝐵}) = ({𝐴} |s {𝐵})
6957, 61, 66, 67, 68halfcut 28434 . . . 4 (𝜑 → ({𝐴} |s {𝐵}) = ((𝐴 +s 𝐵) /su 2s))
7065, 69eqtrd 2780 . . 3 (𝜑 → ({(𝐴 /su 1s )} |s {(𝐵 /su 1s )}) = ((𝐴 +s 𝐵) /su 2s))
7157adantl 481 . . . . . . . . . 10 ((𝑦 ∈ ℕ0s𝜑) → 𝐴 No )
72 peano2n0s 28353 . . . . . . . . . . . 12 (𝑦 ∈ ℕ0s → (𝑦 +s 1s ) ∈ ℕ0s)
73 expscl 28431 . . . . . . . . . . . 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 28422 . . . . . . . . . . . . 13 2s ≠ 0s
77 expsne0 28432 . . . . . . . . . . . . 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 28266 . . . . . . . . 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 28266 . . . . . . . . 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 28268 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0s𝜑) → ((𝐴 /su (2ss(𝑦 +s 1s ))) ·s (2ss(𝑦 +s 1s ))) = 𝐴)
8766adantl 481 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0s𝜑) → 𝐴 <s 𝐵)
8886, 87eqbrtrd 5188 . . . . . . . . . 10 ((𝑦 ∈ ℕ0s𝜑) → ((𝐴 /su (2ss(𝑦 +s 1s ))) ·s (2ss(𝑦 +s 1s ))) <s 𝐵)
89 2nns 28420 . . . . . . . . . . . . . . 15 2s ∈ ℕs
90 nnsgt0 28360 . . . . . . . . . . . . . . 15 (2s ∈ ℕs → 0s <s 2s)
9189, 90ax-mp 5 . . . . . . . . . . . . . 14 0s <s 2s
92 expsgt0 28433 . . . . . . . . . . . . . 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 28271 . . . . . . . . . 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 28430 . . . . . . . . . . . . . . . . . . 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 7464 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ0s𝜑) → (𝐴 /su (2ss(𝑦 +s 1s ))) = (𝐴 /su ((2ss𝑦) ·s 2s)))
103 expscl 28431 . . . . . . . . . . . . . . . . . . 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 28432 . . . . . . . . . . . . . . . . . . 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 28275 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ0s𝜑) → ((𝐴 /su (2ss𝑦)) /su 2s) = (𝐴 /su ((2ss𝑦) ·s 2s)))
112102, 111eqtr4d 2783 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0s𝜑) → (𝐴 /su (2ss(𝑦 +s 1s ))) = ((𝐴 /su (2ss𝑦)) /su 2s))
113112oveq2d 7464 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ0s𝜑) → (2s ·s (𝐴 /su (2ss(𝑦 +s 1s )))) = (2s ·s ((𝐴 /su (2ss𝑦)) /su 2s)))
11471, 105, 109divscld 28266 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0s𝜑) → (𝐴 /su (2ss𝑦)) ∈ No )
115114, 106, 110divscan2d 28267 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ0s𝜑) → (2s ·s ((𝐴 /su (2ss𝑦)) /su 2s)) = (𝐴 /su (2ss𝑦)))
116113, 115eqtrd 2780 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ0s𝜑) → (2s ·s (𝐴 /su (2ss(𝑦 +s 1s )))) = (𝐴 /su (2ss𝑦)))
117116sneqd 4660 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ0s𝜑) → {(2s ·s (𝐴 /su (2ss(𝑦 +s 1s ))))} = {(𝐴 /su (2ss𝑦))})
118101oveq2d 7464 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ0s𝜑) → (𝐵 /su (2ss(𝑦 +s 1s ))) = (𝐵 /su ((2ss𝑦) ·s 2s)))
11983, 105, 106, 109, 110divdivs1d 28275 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ0s𝜑) → ((𝐵 /su (2ss𝑦)) /su 2s) = (𝐵 /su ((2ss𝑦) ·s 2s)))
120118, 119eqtr4d 2783 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0s𝜑) → (𝐵 /su (2ss(𝑦 +s 1s ))) = ((𝐵 /su (2ss𝑦)) /su 2s))
121120oveq2d 7464 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ0s𝜑) → (2s ·s (𝐵 /su (2ss(𝑦 +s 1s )))) = (2s ·s ((𝐵 /su (2ss𝑦)) /su 2s)))
12283, 105, 109divscld 28266 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0s𝜑) → (𝐵 /su (2ss𝑦)) ∈ No )
123122, 106, 110divscan2d 28267 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ0s𝜑) → (2s ·s ((𝐵 /su (2ss𝑦)) /su 2s)) = (𝐵 /su (2ss𝑦)))
124121, 123eqtrd 2780 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ0s𝜑) → (2s ·s (𝐵 /su (2ss(𝑦 +s 1s )))) = (𝐵 /su (2ss𝑦)))
125124sneqd 4660 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ0s𝜑) → {(2s ·s (𝐵 /su (2ss(𝑦 +s 1s ))))} = {(𝐵 /su (2ss𝑦))})
126117, 125oveq12d 7466 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0s𝜑) → ({(2s ·s (𝐴 /su (2ss(𝑦 +s 1s ))))} |s {(2s ·s (𝐵 /su (2ss(𝑦 +s 1s ))))}) = ({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}))
127126eqcomd 2746 . . . . . . . . . 10 ((𝑦 ∈ ℕ0s𝜑) → ({(𝐴 /su (2ss𝑦))} |s {(𝐵 /su (2ss𝑦))}) = ({(2s ·s (𝐴 /su (2ss(𝑦 +s 1s ))))} |s {(2s ·s (𝐵 /su (2ss(𝑦 +s 1s ))))}))
12871, 83, 75, 80divsdird 28277 . . . . . . . . . 10 ((𝑦 ∈ ℕ0s𝜑) → ((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s ))) = ((𝐴 /su (2ss(𝑦 +s 1s ))) +s (𝐵 /su (2ss(𝑦 +s 1s )))))
129127, 128eqeq12d 2756 . . . . . . . . 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 2740 . . . . . . . 8 ({(𝐴 /su (2ss(𝑦 +s 1s )))} |s {(𝐵 /su (2ss(𝑦 +s 1s )))}) = ({(𝐴 /su (2ss(𝑦 +s 1s )))} |s {(𝐵 /su (2ss(𝑦 +s 1s )))})
13282, 85, 98, 130, 131halfcut 28434 . . . . . . 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 7463 . . . . . . . 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 2783 . . . . . 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 28430 . . . . . . . . . . 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 7464 . . . . . . . 8 ((𝑦 ∈ ℕ0s𝜑) → ((𝐴 +s 𝐵) /su (2ss((𝑦 +s 1s ) +s 1s ))) = ((𝐴 +s 𝐵) /su ((2ss(𝑦 +s 1s )) ·s 2s)))
14071, 83addscld 28031 . . . . . . . . 9 ((𝑦 ∈ ℕ0s𝜑) → (𝐴 +s 𝐵) ∈ No )
141140, 75, 106, 80, 110divdivs1d 28275 . . . . . . . 8 ((𝑦 ∈ ℕ0s𝜑) → (((𝐴 +s 𝐵) /su (2ss(𝑦 +s 1s ))) /su 2s) = ((𝐴 +s 𝐵) /su ((2ss(𝑦 +s 1s )) ·s 2s)))
142139, 141eqtr4d 2783 . . . . . . 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 2783 . . . . 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 28355 . 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 2108  wne 2946  {csn 4648   class class class wbr 5166  (class class class)co 7448   No csur 27702   <s cslt 27703   |s cscut 27845   0s c0s 27885   1s c1s 27886   +s cadds 28010   ·s cmuls 28150   /su cdivs 28231  0scnn0s 28336  scnns 28337  2sc2s 28412  scexps 28414
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 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-dc 10515
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 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  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 4971  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-2o 8523  df-oadd 8526  df-nadd 8722  df-no 27705  df-slt 27706  df-bday 27707  df-sle 27808  df-sslt 27844  df-scut 27846  df-0s 27887  df-1s 27888  df-made 27904  df-old 27905  df-left 27907  df-right 27908  df-norec 27989  df-norec2 28000  df-adds 28011  df-negs 28071  df-subs 28072  df-muls 28151  df-divs 28232  df-seqs 28308  df-n0s 28338  df-nns 28339  df-zs 28383  df-2s 28413  df-exps 28415
This theorem is referenced by:  zs12bday  28442
  Copyright terms: Public domain W3C validator