Metamath Proof Explorer

Theorem fmtnofac2lem

Description: Lemma for fmtnofac2 (Induction step). (Contributed by AV, 30-Jul-2021)

Ref Expression
Assertion fmtnofac2lem ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑦 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑦 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ∧ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑧 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑦 · 𝑧 ) ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 ( 𝑦 · 𝑧 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 eluzelz ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) → 𝑦 ∈ ℤ )
2 1 adantr ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑦 ∈ ℤ )
3 eluzelz ⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) → 𝑧 ∈ ℤ )
4 3 adantl ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑧 ∈ ℤ )
5 eluzge2nn0 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ0 )
6 fmtnonn ⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) ∈ ℕ )
7 6 nnzd ⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) ∈ ℤ )
8 5 7 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( FermatNo ‘ 𝑁 ) ∈ ℤ )
9 muldvds2 ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ( FermatNo ‘ 𝑁 ) ∈ ℤ ) → ( ( 𝑦 · 𝑧 ) ∥ ( FermatNo ‘ 𝑁 ) → 𝑧 ∥ ( FermatNo ‘ 𝑁 ) ) )
10 2 4 8 9 syl2an3an ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑦 · 𝑧 ) ∥ ( FermatNo ‘ 𝑁 ) → 𝑧 ∥ ( FermatNo ‘ 𝑁 ) ) )
11 muldvds1 ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ( FermatNo ‘ 𝑁 ) ∈ ℤ ) → ( ( 𝑦 · 𝑧 ) ∥ ( FermatNo ‘ 𝑁 ) → 𝑦 ∥ ( FermatNo ‘ 𝑁 ) ) )
12 2 4 8 11 syl2an3an ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑦 · 𝑧 ) ∥ ( FermatNo ‘ 𝑁 ) → 𝑦 ∥ ( FermatNo ‘ 𝑁 ) ) )
13 pm2.27 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑦 ∥ ( FermatNo ‘ 𝑁 ) ) → ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑦 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑦 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) → ∃ 𝑘 ∈ ℕ0 𝑦 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
14 13 ad2ant2lr ⊢ ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑦 ∥ ( FermatNo ‘ 𝑁 ) ∧ 𝑧 ∥ ( FermatNo ‘ 𝑁 ) ) ) → ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑦 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑦 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) → ∃ 𝑘 ∈ ℕ0 𝑦 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
15 pm2.27 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∥ ( FermatNo ‘ 𝑁 ) ) → ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑧 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) → ∃ 𝑘 ∈ ℕ0 𝑧 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
16 15 ad2ant2l ⊢ ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑦 ∥ ( FermatNo ‘ 𝑁 ) ∧ 𝑧 ∥ ( FermatNo ‘ 𝑁 ) ) ) → ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑧 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) → ∃ 𝑘 ∈ ℕ0 𝑧 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
17 oveq1 ⊢ ( 𝑘 = 𝑚 → ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) = ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) )
18 17 oveq1d ⊢ ( 𝑘 = 𝑚 → ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
19 18 eqeq2d ⊢ ( 𝑘 = 𝑚 → ( 𝑦 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ 𝑦 = ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
20 19 cbvrexvw ⊢ ( ∃ 𝑘 ∈ ℕ0 𝑦 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ ∃ 𝑚 ∈ ℕ0 𝑦 = ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
21 oveq1 ⊢ ( 𝑘 = 𝑛 → ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) = ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) )
22 21 oveq1d ⊢ ( 𝑘 = 𝑛 → ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
23 22 eqeq2d ⊢ ( 𝑘 = 𝑛 → ( 𝑧 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ 𝑧 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
24 23 cbvrexvw ⊢ ( ∃ 𝑘 ∈ ℕ0 𝑧 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ ∃ 𝑛 ∈ ℕ0 𝑧 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
25 simpl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 𝑚 ∈ ℕ0 )
26 25 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → 𝑚 ∈ ℕ0 )
27 2nn0 ⊢ 2 ∈ ℕ0
28 27 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℕ0 )
29 5 28 nn0addcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 + 2 ) ∈ ℕ0 )
30 28 29 nn0expcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 𝑁 + 2 ) ) ∈ ℕ0 )
31 30 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( 2 ↑ ( 𝑁 + 2 ) ) ∈ ℕ0 )
32 26 31 nn0mulcld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ∈ ℕ0 )
33 simpr ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
34 33 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → 𝑛 ∈ ℕ0 )
35 32 34 nn0mulcld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) ∈ ℕ0 )
36 nn0addcl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑚 + 𝑛 ) ∈ ℕ0 )
37 36 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( 𝑚 + 𝑛 ) ∈ ℕ0 )
38 35 37 nn0addcld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) ∈ ℕ0 )
39 oveq1 ⊢ ( 𝑘 = ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) → ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) = ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) )
40 39 oveq1d ⊢ ( 𝑘 = ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) → ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = ( ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
41 40 eqeq2d ⊢ ( 𝑘 = ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) → ( ( ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ ( ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = ( ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
42 41 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ 𝑘 = ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) ) → ( ( ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ ( ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = ( ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
43 eqidd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = ( ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
44 38 42 43 rspcedvd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ∃ 𝑘 ∈ ℕ0 ( ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
45 nn0cn ⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℂ )
46 45 adantr ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 𝑚 ∈ ℂ )
47 46 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → 𝑚 ∈ ℂ )
48 30 nn0cnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 𝑁 + 2 ) ) ∈ ℂ )
49 48 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( 2 ↑ ( 𝑁 + 2 ) ) ∈ ℂ )
50 47 49 mulcld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ∈ ℂ )
51 33 nn0cnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℂ )
52 51 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → 𝑛 ∈ ℂ )
53 52 49 mulcld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ∈ ℂ )
54 50 53 jca ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ∈ ℂ ∧ ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ∈ ℂ ) )
55 54 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ∈ ℂ ∧ ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ∈ ℂ ) )
56 muladd11r ⊢ ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ∈ ℂ ∧ ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ∈ ℂ ) → ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) · ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) = ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) + ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) ) + 1 ) )
57 55 56 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) · ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) = ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) + ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) ) + 1 ) )
58 25 nn0cnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 𝑚 ∈ ℂ )
59 58 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → 𝑚 ∈ ℂ )
60 59 52 49 3jca ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ ( 2 ↑ ( 𝑁 + 2 ) ) ∈ ℂ ) )
61 60 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ ( 2 ↑ ( 𝑁 + 2 ) ) ∈ ℂ ) )
62 adddir ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ ( 2 ↑ ( 𝑁 + 2 ) ) ∈ ℂ ) → ( ( 𝑚 + 𝑛 ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) = ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) )
63 61 62 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑚 + 𝑛 ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) = ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) )
64 63 eqcomd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) = ( ( 𝑚 + 𝑛 ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) )
65 64 oveq2d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) + ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) ) = ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) + ( ( 𝑚 + 𝑛 ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) )
66 50 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ∈ ℂ )
67 52 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑛 ∈ ℂ )
68 49 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 2 ↑ ( 𝑁 + 2 ) ) ∈ ℂ )
69 66 67 68 mulassd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) = ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) )
70 69 eqcomd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) = ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) )
71 70 oveq1d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) + ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) ) = ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) + ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) ) )
72 50 52 mulcld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) ∈ ℂ )
73 36 nn0cnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑚 + 𝑛 ) ∈ ℂ )
74 73 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( 𝑚 + 𝑛 ) ∈ ℂ )
75 72 74 49 3jca ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) ∈ ℂ ∧ ( 𝑚 + 𝑛 ) ∈ ℂ ∧ ( 2 ↑ ( 𝑁 + 2 ) ) ∈ ℂ ) )
76 75 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) ∈ ℂ ∧ ( 𝑚 + 𝑛 ) ∈ ℂ ∧ ( 2 ↑ ( 𝑁 + 2 ) ) ∈ ℂ ) )
77 adddir ⊢ ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) ∈ ℂ ∧ ( 𝑚 + 𝑛 ) ∈ ℂ ∧ ( 2 ↑ ( 𝑁 + 2 ) ) ∈ ℂ ) → ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) = ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) + ( ( 𝑚 + 𝑛 ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) )
78 76 77 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) = ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) + ( ( 𝑚 + 𝑛 ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) )
79 65 71 78 3eqtr4d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) + ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) ) = ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) )
80 79 oveq1d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) + ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) ) + 1 ) = ( ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
81 57 80 eqtrd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) · ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) = ( ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
82 81 eqeq1d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) · ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ ( ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
83 82 rexbidva ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( ∃ 𝑘 ∈ ℕ0 ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) · ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ ∃ 𝑘 ∈ ℕ0 ( ( ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) · 𝑛 ) + ( 𝑚 + 𝑛 ) ) · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
84 44 83 mpbird ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ∃ 𝑘 ∈ ℕ0 ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) · ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
85 84 adantll ⊢ ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ∃ 𝑘 ∈ ℕ0 ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) · ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
86 oveq12 ⊢ ( ( 𝑦 = ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ∧ 𝑧 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) → ( 𝑦 · 𝑧 ) = ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) · ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
87 86 ancoms ⊢ ( ( 𝑧 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ∧ 𝑦 = ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) → ( 𝑦 · 𝑧 ) = ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) · ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
88 87 eqeq1d ⊢ ( ( 𝑧 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ∧ 𝑦 = ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) → ( ( 𝑦 · 𝑧 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) · ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
89 88 rexbidv ⊢ ( ( 𝑧 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ∧ 𝑦 = ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) → ( ∃ 𝑘 ∈ ℕ0 ( 𝑦 · 𝑧 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ ∃ 𝑘 ∈ ℕ0 ( ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) · ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
90 85 89 syl5ibrcom ⊢ ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( ( 𝑧 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ∧ 𝑦 = ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) → ∃ 𝑘 ∈ ℕ0 ( 𝑦 · 𝑧 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
91 90 expd ⊢ ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( 𝑧 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) → ( 𝑦 = ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) → ∃ 𝑘 ∈ ℕ0 ( 𝑦 · 𝑧 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
92 91 anassrs ⊢ ( ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑧 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) → ( 𝑦 = ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) → ∃ 𝑘 ∈ ℕ0 ( 𝑦 · 𝑧 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
93 92 rexlimdva ⊢ ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑚 ∈ ℕ0 ) → ( ∃ 𝑛 ∈ ℕ0 𝑧 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) → ( 𝑦 = ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) → ∃ 𝑘 ∈ ℕ0 ( 𝑦 · 𝑧 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
94 24 93 biimtrid ⊢ ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑚 ∈ ℕ0 ) → ( ∃ 𝑘 ∈ ℕ0 𝑧 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) → ( 𝑦 = ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) → ∃ 𝑘 ∈ ℕ0 ( 𝑦 · 𝑧 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
95 94 com23 ⊢ ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝑦 = ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) → ( ∃ 𝑘 ∈ ℕ0 𝑧 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) → ∃ 𝑘 ∈ ℕ0 ( 𝑦 · 𝑧 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
96 95 rexlimdva ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ∃ 𝑚 ∈ ℕ0 𝑦 = ( ( 𝑚 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) → ( ∃ 𝑘 ∈ ℕ0 𝑧 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) → ∃ 𝑘 ∈ ℕ0 ( 𝑦 · 𝑧 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
97 20 96 biimtrid ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ∃ 𝑘 ∈ ℕ0 𝑦 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) → ( ∃ 𝑘 ∈ ℕ0 𝑧 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) → ∃ 𝑘 ∈ ℕ0 ( 𝑦 · 𝑧 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
98 97 impd ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ∃ 𝑘 ∈ ℕ0 𝑦 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ∧ ∃ 𝑘 ∈ ℕ0 𝑧 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) → ∃ 𝑘 ∈ ℕ0 ( 𝑦 · 𝑧 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
99 98 adantr ⊢ ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑦 ∥ ( FermatNo ‘ 𝑁 ) ∧ 𝑧 ∥ ( FermatNo ‘ 𝑁 ) ) ) → ( ( ∃ 𝑘 ∈ ℕ0 𝑦 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ∧ ∃ 𝑘 ∈ ℕ0 𝑧 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) → ∃ 𝑘 ∈ ℕ0 ( 𝑦 · 𝑧 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
100 14 16 99 syl2and ⊢ ( ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑦 ∥ ( FermatNo ‘ 𝑁 ) ∧ 𝑧 ∥ ( FermatNo ‘ 𝑁 ) ) ) → ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑦 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑦 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ∧ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑧 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) → ∃ 𝑘 ∈ ℕ0 ( 𝑦 · 𝑧 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
101 100 exp32 ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑦 ∥ ( FermatNo ‘ 𝑁 ) → ( 𝑧 ∥ ( FermatNo ‘ 𝑁 ) → ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑦 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑦 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ∧ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑧 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) → ∃ 𝑘 ∈ ℕ0 ( 𝑦 · 𝑧 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) ) )
102 12 101 syld ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑦 · 𝑧 ) ∥ ( FermatNo ‘ 𝑁 ) → ( 𝑧 ∥ ( FermatNo ‘ 𝑁 ) → ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑦 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑦 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ∧ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑧 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) → ∃ 𝑘 ∈ ℕ0 ( 𝑦 · 𝑧 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) ) )
103 10 102 mpdd ⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑦 · 𝑧 ) ∥ ( FermatNo ‘ 𝑁 ) → ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑦 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑦 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ∧ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑧 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) → ∃ 𝑘 ∈ ℕ0 ( 𝑦 · 𝑧 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
104 103 expimpd ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑦 · 𝑧 ) ∥ ( FermatNo ‘ 𝑁 ) ) → ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑦 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑦 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ∧ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑧 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) → ∃ 𝑘 ∈ ℕ0 ( 𝑦 · 𝑧 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
105 104 com23 ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑦 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑦 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ∧ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑧 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑦 · 𝑧 ) ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 ( 𝑦 · 𝑧 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )