Theorem pw2recs

Description: Any power of two has a multiplicative inverse. Note that this theorem does not require the axiom of infinity. (Contributed by Scott Fenton, 5-Sep-2025)

	Ref	Expression
Assertion	pw2recs	⊢ ( 𝑁 ∈ ℕ0s → ∃ 𝑥 ∈ No ( ( 2s ↑s 𝑁 ) ·s 𝑥 ) = 1s )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑚 = 0s → ( 2s ↑s 𝑚 ) = ( 2s ↑s 0s ) )
2		2sno	⊢ 2s ∈ No
3		exps0	⊢ ( 2s ∈ No → ( 2s ↑s 0s ) = 1s )
4	2 3	ax-mp	⊢ ( 2s ↑s 0s ) = 1s
5	1 4	eqtrdi	⊢ ( 𝑚 = 0s → ( 2s ↑s 𝑚 ) = 1s )
6	5	oveq1d	⊢ ( 𝑚 = 0s → ( ( 2s ↑s 𝑚 ) ·s 𝑥 ) = ( 1s ·s 𝑥 ) )
7	6	eqeq1d	⊢ ( 𝑚 = 0s → ( ( ( 2s ↑s 𝑚 ) ·s 𝑥 ) = 1s ↔ ( 1s ·s 𝑥 ) = 1s ) )
8	7	rexbidv	⊢ ( 𝑚 = 0s → ( ∃ 𝑥 ∈ No ( ( 2s ↑s 𝑚 ) ·s 𝑥 ) = 1s ↔ ∃ 𝑥 ∈ No ( 1s ·s 𝑥 ) = 1s ) )
9		oveq2	⊢ ( 𝑚 = 𝑛 → ( 2s ↑s 𝑚 ) = ( 2s ↑s 𝑛 ) )
10	9	oveq1d	⊢ ( 𝑚 = 𝑛 → ( ( 2s ↑s 𝑚 ) ·s 𝑥 ) = ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) )
11	10	eqeq1d	⊢ ( 𝑚 = 𝑛 → ( ( ( 2s ↑s 𝑚 ) ·s 𝑥 ) = 1s ↔ ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) )
12	11	rexbidv	⊢ ( 𝑚 = 𝑛 → ( ∃ 𝑥 ∈ No ( ( 2s ↑s 𝑚 ) ·s 𝑥 ) = 1s ↔ ∃ 𝑥 ∈ No ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) )
13		oveq2	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 2s ↑s 𝑚 ) = ( 2s ↑s ( 𝑛 +s 1s ) ) )
14	13	oveq1d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( 2s ↑s 𝑚 ) ·s 𝑥 ) = ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 𝑥 ) )
15	14	eqeq1d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( ( 2s ↑s 𝑚 ) ·s 𝑥 ) = 1s ↔ ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 𝑥 ) = 1s ) )
16	15	rexbidv	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ∃ 𝑥 ∈ No ( ( 2s ↑s 𝑚 ) ·s 𝑥 ) = 1s ↔ ∃ 𝑥 ∈ No ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 𝑥 ) = 1s ) )
17		oveq2	⊢ ( 𝑥 = 𝑦 → ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 𝑥 ) = ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 𝑦 ) )
18	17	eqeq1d	⊢ ( 𝑥 = 𝑦 → ( ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 𝑥 ) = 1s ↔ ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 𝑦 ) = 1s ) )
19	18	cbvrexvw	⊢ ( ∃ 𝑥 ∈ No ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 𝑥 ) = 1s ↔ ∃ 𝑦 ∈ No ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 𝑦 ) = 1s )
20	16 19	bitrdi	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ∃ 𝑥 ∈ No ( ( 2s ↑s 𝑚 ) ·s 𝑥 ) = 1s ↔ ∃ 𝑦 ∈ No ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 𝑦 ) = 1s ) )
21		oveq2	⊢ ( 𝑚 = 𝑁 → ( 2s ↑s 𝑚 ) = ( 2s ↑s 𝑁 ) )
22	21	oveq1d	⊢ ( 𝑚 = 𝑁 → ( ( 2s ↑s 𝑚 ) ·s 𝑥 ) = ( ( 2s ↑s 𝑁 ) ·s 𝑥 ) )
23	22	eqeq1d	⊢ ( 𝑚 = 𝑁 → ( ( ( 2s ↑s 𝑚 ) ·s 𝑥 ) = 1s ↔ ( ( 2s ↑s 𝑁 ) ·s 𝑥 ) = 1s ) )
24	23	rexbidv	⊢ ( 𝑚 = 𝑁 → ( ∃ 𝑥 ∈ No ( ( 2s ↑s 𝑚 ) ·s 𝑥 ) = 1s ↔ ∃ 𝑥 ∈ No ( ( 2s ↑s 𝑁 ) ·s 𝑥 ) = 1s ) )
25		1sno	⊢ 1s ∈ No
26		mulsrid	⊢ ( 1s ∈ No → ( 1s ·s 1s ) = 1s )
27	25 26	ax-mp	⊢ ( 1s ·s 1s ) = 1s
28		oveq2	⊢ ( 𝑥 = 1s → ( 1s ·s 𝑥 ) = ( 1s ·s 1s ) )
29	28	eqeq1d	⊢ ( 𝑥 = 1s → ( ( 1s ·s 𝑥 ) = 1s ↔ ( 1s ·s 1s ) = 1s ) )
30	29	rspcev	⊢ ( ( 1s ∈ No ∧ ( 1s ·s 1s ) = 1s ) → ∃ 𝑥 ∈ No ( 1s ·s 𝑥 ) = 1s )
31	25 27 30	mp2an	⊢ ∃ 𝑥 ∈ No ( 1s ·s 𝑥 ) = 1s
32		oveq2	⊢ ( 𝑦 = ( 𝑥 ·s ( { 0s } |s { 1s } ) ) → ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 𝑦 ) = ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s ( 𝑥 ·s ( { 0s } |s { 1s } ) ) ) )
33	32	eqeq1d	⊢ ( 𝑦 = ( 𝑥 ·s ( { 0s } |s { 1s } ) ) → ( ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 𝑦 ) = 1s ↔ ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s ( 𝑥 ·s ( { 0s } |s { 1s } ) ) ) = 1s ) )
34		simprl	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝑥 ∈ No ∧ ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) ) → 𝑥 ∈ No )
35		0sno	⊢ 0s ∈ No
36	35	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝑥 ∈ No ∧ ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) ) → 0s ∈ No )
37	25	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝑥 ∈ No ∧ ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) ) → 1s ∈ No )
38		0slt1s	⊢ 0s <s 1s
39	38	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝑥 ∈ No ∧ ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) ) → 0s <s 1s )
40	36 37 39	ssltsn	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝑥 ∈ No ∧ ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) ) → { 0s } <<s { 1s } )
41	40	scutcld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝑥 ∈ No ∧ ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) ) → ( { 0s } |s { 1s } ) ∈ No )
42	34 41	mulscld	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝑥 ∈ No ∧ ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) ) → ( 𝑥 ·s ( { 0s } |s { 1s } ) ) ∈ No )
43		expsp1	⊢ ( ( 2s ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( 2s ↑s ( 𝑛 +s 1s ) ) = ( ( 2s ↑s 𝑛 ) ·s 2s ) )
44	2 43	mpan	⊢ ( 𝑛 ∈ ℕ0s → ( 2s ↑s ( 𝑛 +s 1s ) ) = ( ( 2s ↑s 𝑛 ) ·s 2s ) )
45	44	adantr	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝑥 ∈ No ∧ ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) ) → ( 2s ↑s ( 𝑛 +s 1s ) ) = ( ( 2s ↑s 𝑛 ) ·s 2s ) )
46	45	oveq1d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝑥 ∈ No ∧ ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) ) → ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s ( 𝑥 ·s ( { 0s } |s { 1s } ) ) ) = ( ( ( 2s ↑s 𝑛 ) ·s 2s ) ·s ( 𝑥 ·s ( { 0s } |s { 1s } ) ) ) )
47		expscl	⊢ ( ( 2s ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( 2s ↑s 𝑛 ) ∈ No )
48	2 47	mpan	⊢ ( 𝑛 ∈ ℕ0s → ( 2s ↑s 𝑛 ) ∈ No )
49	48	adantr	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝑥 ∈ No ∧ ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) ) → ( 2s ↑s 𝑛 ) ∈ No )
50	2	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝑥 ∈ No ∧ ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) ) → 2s ∈ No )
51	49 50 34 41	muls4d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝑥 ∈ No ∧ ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) ) → ( ( ( 2s ↑s 𝑛 ) ·s 2s ) ·s ( 𝑥 ·s ( { 0s } |s { 1s } ) ) ) = ( ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) ·s ( 2s ·s ( { 0s } |s { 1s } ) ) ) )
52		simprr	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝑥 ∈ No ∧ ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) ) → ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s )
53		twocut	⊢ ( 2s ·s ( { 0s } |s { 1s } ) ) = 1s
54	53	a1i	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝑥 ∈ No ∧ ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) ) → ( 2s ·s ( { 0s } |s { 1s } ) ) = 1s )
55	52 54	oveq12d	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝑥 ∈ No ∧ ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) ) → ( ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) ·s ( 2s ·s ( { 0s } |s { 1s } ) ) ) = ( 1s ·s 1s ) )
56	55 27	eqtrdi	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝑥 ∈ No ∧ ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) ) → ( ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) ·s ( 2s ·s ( { 0s } |s { 1s } ) ) ) = 1s )
57	46 51 56	3eqtrd	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝑥 ∈ No ∧ ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) ) → ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s ( 𝑥 ·s ( { 0s } |s { 1s } ) ) ) = 1s )
58	33 42 57	rspcedvdw	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( 𝑥 ∈ No ∧ ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s ) ) → ∃ 𝑦 ∈ No ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 𝑦 ) = 1s )
59	58	rexlimdvaa	⊢ ( 𝑛 ∈ ℕ0s → ( ∃ 𝑥 ∈ No ( ( 2s ↑s 𝑛 ) ·s 𝑥 ) = 1s → ∃ 𝑦 ∈ No ( ( 2s ↑s ( 𝑛 +s 1s ) ) ·s 𝑦 ) = 1s ) )
60	8 12 20 24 31 59	n0sind	⊢ ( 𝑁 ∈ ℕ0s → ∃ 𝑥 ∈ No ( ( 2s ↑s 𝑁 ) ·s 𝑥 ) = 1s )