:: FIB_NUM4  semantic presentation begin  
theorem :: FIB_NUM4:1 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "c")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k13_complex1 :::"/"::: )  (Set (Var "b")) ")" )  ($#k3_power :::"to_power"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "c")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k3_power :::"to_power"::: )  (Set (Var "c")) ")" ))))) ; 
 
theorem :: FIB_NUM4:2 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_int_1 :::"integer"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set  "(" (Set (Var "b"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "c")) ")" ))))) ; 
 
theorem :: FIB_NUM4:3 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "n")) "is"   ($#v1_abian :::"even"::: )  ) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k3_power :::"to_power"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "n")))))) ; 
 
theorem :: FIB_NUM4:4 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  ) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k3_power :::"to_power"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" ))))) ; 
 
theorem :: FIB_NUM4:5 (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  ($#k2_fib_num :::"tau_bar"::: ) ))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) ; 
 
theorem :: FIB_NUM4:6 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "n")) "is"   ($#v1_abian :::"even"::: )  )) "holds"  (Bool (Set (Set (Var "r"))  ($#k3_power :::"to_power"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: FIB_NUM4:7 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "r"))  ($#k3_power :::"to_power"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: FIB_NUM4:8 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  ($#k2_fib_num :::"tau_bar"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2)))) ; 
 
theorem :: FIB_NUM4:9 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "m")) "is"   ($#v1_abian :::"odd"::: )  ) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "m"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1)))) "holds"  (Bool (Set (Set (Var "r"))  ($#k3_power :::"to_power"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "r"))  ($#k3_power :::"to_power"::: )  (Set (Var "m")))))) ; 
 
theorem :: FIB_NUM4:10 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m")) "is"   ($#v1_abian :::"odd"::: )  ) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set  ($#k2_fib_num :::"tau_bar"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  ($#k2_fib_num :::"tau_bar"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "m"))))) ; 
 
theorem :: FIB_NUM4:11 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n")) "is"   ($#v1_abian :::"even"::: )  ) & (Bool (Set (Var "m")) "is"   ($#v1_abian :::"even"::: )  ) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set  ($#k2_fib_num :::"tau_bar"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k2_fib_num :::"tau_bar"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "m"))))) ; 
 
theorem :: FIB_NUM4:12 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k1_fib_num3 :::"Lucas"::: )  (Set (Var "m")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k1_fib_num3 :::"Lucas"::: )  (Set (Var "n"))))) ; 
 
theorem :: FIB_NUM4:13 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  ($#k1_fib_num :::"tau"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set (Set  ($#k2_fib_num :::"tau_bar"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "n"))))) ; 
 
theorem :: FIB_NUM4:14 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  ($#k2_fib_num :::"tau_bar"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "n"))))) ; 
 
theorem :: FIB_NUM4:15 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Num 2))) "holds"  (Bool (Set (Set  ($#k2_fib_num :::"tau_bar"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 5) ")" ) ")" )))) ; 
 
theorem :: FIB_NUM4:16 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set (Set  ($#k2_fib_num :::"tau_bar"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Num 1)  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 5) ")" )))) ; 
 
theorem :: FIB_NUM4:17 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Set  ($#k2_fib_num :::"tau_bar"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 5) ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" (Set  "(" (Set  ($#k2_fib_num :::"tau_bar"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 5) ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))  ")" )) ; 
 begin  
theorem :: FIB_NUM4:18 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set  "(" (Set  "(" (Set  ($#k1_fib_num :::"tau"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 5) ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" ) ($#k1_int_1 :::"/]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n"))))) ; 
 
theorem :: FIB_NUM4:19 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set  ($#k2_int_1 :::"[/"::: ) (Set  "(" (Set  "(" (Set  "(" (Set  ($#k1_fib_num :::"tau"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 5) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" ) ($#k2_int_1 :::"\]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n"))))) ; 
 
theorem :: FIB_NUM4:20 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set  "(" (Set  ($#k1_fib_num :::"tau"::: ) )  ($#k3_power :::"to_power"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 5) ")" ) ")" ) ($#k1_int_1 :::"/]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_pre_ff :::"Fib"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")) ")" )))) ; 
 
theorem :: FIB_NUM4:21 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set  ($#k2_int_1 :::"[/"::: ) (Set  "(" (Set  "(" (Set  ($#k1_fib_num :::"tau"::: ) )  ($#k3_power :::"to_power"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 5) ")" ) ")" ) ($#k2_int_1 :::"\]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_pre_ff :::"Fib"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )))) ; 
 
theorem :: FIB_NUM4:22 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) & (Bool (Set (Var "n")) "is"   ($#v1_abian :::"even"::: )  )) "holds"  (Bool (Set   ($#k1_pre_ff :::"Fib"::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set  "(" (Set  ($#k1_fib_num :::"tau"::: ) )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ($#k1_int_1 :::"/]"::: ) ))) ; 
 
theorem :: FIB_NUM4:23 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) & (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  )) "holds"  (Bool (Set   ($#k1_pre_ff :::"Fib"::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_int_1 :::"[/"::: ) (Set  "(" (Set  "(" (Set  ($#k1_fib_num :::"tau"::: ) )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ($#k2_int_1 :::"\]"::: ) ))) ; 
 
theorem :: FIB_NUM4:24 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set   ($#k1_pre_ff :::"Fib"::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 5) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n")) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ($#k1_int_1 :::"/]"::: ) ))) ; 
 
theorem :: FIB_NUM4:25 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set   ($#k1_pre_ff :::"Fib"::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_int_1 :::"[/"::: ) (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 5) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n")) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ($#k2_int_1 :::"\]"::: ) ))) ; 
 
theorem :: FIB_NUM4:26 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_pre_ff :::"Fib"::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Num 5)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n")) ")" )  ($#k1_pepin :::"^2"::: )  ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Num 1) ")" )  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2)))) ; 
 
theorem :: FIB_NUM4:27 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set   ($#k1_pre_ff :::"Fib"::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 5)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n")) ")" )  ($#k1_pepin :::"^2"::: )  ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n")) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ($#k1_int_1 :::"/]"::: ) ))) ; 
 
theorem :: FIB_NUM4:28 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set   ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Set  ($#k1_fib_num :::"tau"::: ) ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" ) ($#k1_int_1 :::"/]"::: ) ))) ; 
 
theorem :: FIB_NUM4:29 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool  "("  (Bool  "("  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))  ")" ) "or" (Bool  "("  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "k")))  ")" )  ")" )) "holds"  (Bool (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set  "(" (Set  "(" (Set  ($#k1_fib_num :::"tau"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "k")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_pre_ff :::"Fib"::: )  (Set (Var "n")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" ) ($#k1_int_1 :::"/]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_pre_ff :::"Fib"::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")) ")" )))) ; 
 begin  
theorem :: FIB_NUM4:30 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set   ($#k1_fib_num3 :::"Lucas"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set  "(" (Set  ($#k1_fib_num :::"tau"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" ) ($#k1_int_1 :::"/]"::: ) ))) ; 
 
theorem :: FIB_NUM4:31 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set   ($#k1_fib_num3 :::"Lucas"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_int_1 :::"[/"::: ) (Set  "(" (Set  "(" (Set  ($#k1_fib_num :::"tau"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" ) ($#k2_int_1 :::"\]"::: ) ))) ; 
 
theorem :: FIB_NUM4:32 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set   ($#k1_fib_num3 :::"Lucas"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_int_1 :::"[/"::: ) (Set  "(" (Set  ($#k1_fib_num :::"tau"::: ) )  ($#k3_power :::"to_power"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")) ")" ) ")" ) ($#k2_int_1 :::"\]"::: ) ))) ; 
 
theorem :: FIB_NUM4:33 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool (Set   ($#k1_fib_num3 :::"Lucas"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set  ($#k1_fib_num :::"tau"::: ) )  ($#k3_power :::"to_power"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")" ) ($#k1_int_1 :::"/]"::: ) ))) ; 
 
theorem :: FIB_NUM4:34 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) & (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  )) "holds"  (Bool (Set   ($#k1_fib_num3 :::"Lucas"::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set  "(" (Set  ($#k1_fib_num :::"tau"::: ) )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_fib_num3 :::"Lucas"::: )  (Set (Var "n")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ($#k1_int_1 :::"/]"::: ) ))) ; 
 
theorem :: FIB_NUM4:35 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) & (Bool (Set (Var "n")) "is"   ($#v1_abian :::"even"::: )  )) "holds"  (Bool (Set   ($#k1_fib_num3 :::"Lucas"::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_int_1 :::"[/"::: ) (Set  "(" (Set  "(" (Set  ($#k1_fib_num :::"tau"::: ) )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_fib_num3 :::"Lucas"::: )  (Set (Var "n")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ($#k2_int_1 :::"\]"::: ) ))) ; 
 
theorem :: FIB_NUM4:36 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Num 1))) "holds"  (Bool (Set   ($#k1_fib_num3 :::"Lucas"::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_fib_num3 :::"Lucas"::: )  (Set (Var "n")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Num 5)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k1_fib_num3 :::"Lucas"::: )  (Set (Var "n")) ")" )  ($#k1_pepin :::"^2"::: )  ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Num 1) ")" )  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" ) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2)))) ; 
 
theorem :: FIB_NUM4:37 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 4))) "holds"  (Bool (Set   ($#k1_fib_num3 :::"Lucas"::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k1_fib_num3 :::"Lucas"::: )  (Set (Var "n")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 5)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k1_fib_num3 :::"Lucas"::: )  (Set (Var "n")) ")" )  ($#k1_pepin :::"^2"::: )  ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_fib_num3 :::"Lucas"::: )  (Set (Var "n")) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ($#k1_int_1 :::"/]"::: ) ))) ; 
 
theorem :: FIB_NUM4:38 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Num 2))) "holds"  (Bool (Set   ($#k1_fib_num3 :::"Lucas"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Set  ($#k1_fib_num :::"tau"::: ) ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k1_fib_num3 :::"Lucas"::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" ) ($#k1_int_1 :::"/]"::: ) ))) ; 
 
theorem :: FIB_NUM4:39 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 4)) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "k"))) & (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  )) "holds"  (Bool (Set   ($#k1_fib_num3 :::"Lucas"::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set  "(" (Set  "(" (Set  ($#k1_fib_num :::"tau"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "k")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_fib_num3 :::"Lucas"::: )  (Set (Var "n")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ($#k1_int_1 :::"/]"::: ) ))) ;